Definitions
bool
1
Doc
At:
eq
int
eq
true
elim
1
1
1.
i:
2.
j:
3.
(i=
j) = true
4.
i = j
i = j
By:
RWH (LemmaC
Thm*
i,j:
. i
j
(i=
j) = false
) 3
Generated subgoal:
1
3.
false
= true
4.
i = j
i = j