Goal:
    x : VSet.E.t  y : VSet.E.t
  ============================
   (y = y)


DEBUG:Going to execute:
done
DEBUG LTAC Evaluated term: (reflectP
                              (forall (x0 : ?T) (x1 : ?T0) (x2 : ?T1), ?P) 
                              ?y ?i ?y0 ?y1 ?y2)