Goal:
    z : Z
  ============================
   (False -> True -> Some z = None)


DEBUG:Going to execute:
symmetry; trivial
Level 1: Backtrace:

In environment
z : Z
H : False
H0 : True
Unable to unify "None" with "Some z".
Level 0: Backtrace:

In environment
z : Z
H : False
H0 : True
Unable to unify "None" with "Some z".