PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
assignment
monotone
1
1
1
2
1
1.
f:
Formula
2.
x:
Var
3.
a:
Assignment
4.
a':
Assignment
5.
a' extends a
6.
a |
x
a(x) = 3
By:
UnfoldTopAb -1
THEN
Reduce -1
Generated subgoal:
1
6.
a(x) = 3
a(x) = 3
About:
x
a(x) = 3
