At: assignment monotone 1 1 2 1 1 2 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:
