PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
not
falsifiable
lemma
2
1
1
1
1.
F:
Formula
2.
a:
Assignment
3.
(F under a) = 3
4.
x:
5.
(F under a) = x
x = 3
By:
HypSubst -3 -1
THEN
RevHypSubst -1 0
Generated subgoal:
1
5.
3
= x
3
= 3
About:
x = 3
