PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
assignment
monotone
1
1
1
1
2
1
1.
f:
Formula
2.
x:
Var
3.
a:
Assignment
4.
a':
Assignment
5.
a' extends a
6.
a(x) = 3
7.
a(x) = a'(x)
a'(x) = 3
By:
HypSubst -1 -2
Generated subgoals:
None
About:
a'(x) = 3
