Goal:
  
  A : Type
  Aeq : ReflectEq A
  x : A
  y : A
  H : reflectProp (x = y) false
  H0 : option_extends (Some x) (Some y)
  t : A
  H2 : t = x
  H3 : x = y
  H1 : x <> y
  ============================
   False


DEBUG:Going to execute:
congruence