Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
Discrete{Var}
Applied Tactic:
Unfolds ``discrete Var`` 0 THEN UnivCD THENA Auto
Generated subgoals:
1
. Dec(x = y)
Discrete{Var}