Goal:
    A : Type  HA : ReflectEq A  a : A
  ============================
   (reflectProp (Some a = None) false)


DEBUG:Going to execute:
solve [ constructor; easy ]
Level 0: Backtrace:

In environment
A : Type
HA : ReflectEq A
a, a0 : A
Unable to unify "reflectProp ?M1194 false" with
 "reflectProp (Some a = Some a0) (a == a0)".
Level 0: Backtrace:

In environment
A : Type
HA : ReflectEq A
a, a0 : A
Unable to unify "reflectProp ?M1194 false" with
 "reflectProp (Some a = Some a0) (a == a0)".
Level 0: Backtrace:

In environment
A : Type
HA : ReflectEq A
a, a0 : A
Unable to unify "reflectProp ?M1194 false" with
 "reflectProp (Some a = Some a0) (a == a0)".
Level 0: Backtrace:

No applicable tactic.