Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

p,q:. p = q = tt p = q

Applied Tactic: (Unfold `beq` 0 THEN GenRepD THENM BoolCases 1 THENM BoolCases 1 THENM Try (Reduce 0) THENM Try (Red uce (-1)) ...)
Generated subgoals:

None