Level: Lib Thy Top:
Hypotheses:None
Conclusion:
p,q:
. p =
q = ff 
p = q
Applied Tactic: ((Unfold `beq` 0 THEN GenRepD THENM BoolCases 1 THENM BoolCases 1 THENM Try (Reduce 0) THENM Try (Re
duce (-1))) THEN Auto THEN InstLemma `btrue_neq_bfalse` [] THEN Auto THEN Try (D 1) THEN Auto THEN D
0 THENM D 2 ...)
Generated subgoals: