Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
p,q:
. p =
q = q =
p
Applied Tactic:
(Unfold `beq` 0 THEN RepD THENM BoolCases 1 THENM BoolCases 1 THENM Reduce 0 ...)
Generated subgoals:
None
p,q:
. p =
q = q = p