At: beq neq
p,q:
. p =
q = false
p = q
By:
Unfold `beq` 0
THEN
GenRepD
THEN
BoolCases 1
THEN
BoolCases 1
THEN
Try (Reduce 0)
THEN
Try (Reduce -1)
THEN
Inst
Thm* true = false
[]
THEN
Try (Analyze 1)
THEN
Analyze 0
THEN
Analyze 2
Generated subgoals:None
About:
