Goal:
    x : VSet.E.t  y : VSet.E.t  p : VSet.E.lt y x
  ============================
   (reflectProp (x = y) false)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrapply@0> $1
DEBUG LTAC Evaluated term: (reflectF
                              (forall (x0 : ?T) (x1 : ?T0) (x2 : ?T1), ?P) 
                              ?n ?i ?y ?y0 ?y1)

Goals:
    x : VSet.E.t  y : VSet.E.t  p : VSet.E.lt x y  eq : x = y
  ============================
   False

    x : VSet.E.t  y : VSet.E.t  p : VSet.E.lt y x  eq : x = y
  ============================
   False


DEBUG:Going to execute:
move : p 
DEBUG LTAC Evaluated term: (reflectF
                              (forall (x0 : ?T) (x1 : ?T0) (x2 : ?T1), ?P) 
                              ?n ?i ?y ?y0 ?y1)