Definitions
bool
1
Doc
At:
assert
of
eq
bool
1
1
1.
p:
2.
q:
((p
q)
(
p
q))
p = q
By:
OnHyps [2;1] BoolCases
THEN
AbReduce 0
THEN
RW assert_pushdownC 0
Generated subgoals:
1
1.
false
= true
False
2
1.
true
= false
False
((p
q) 
(
pq)) 
p = q = true False = false False