At: assignment monotone 1 1 2 1 1 1 1 1
1. f: Formula
2. x: Formula
3. a: Assignment
4. a': Assignment
5. a' extends a
6. a |= x 
a' |= x
7. a |
x a' | x
8. a |= 
x
a | x
By: FwdThru
Thm* 
F:Formula, a:Assignment. a |= F 
a | F
[-1]
Generated subgoals:None
About:
