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