At: assignment monotone 1 1 4 1 1 1
1. f: Formula
2. x1: Formula
3. x2: Formula
4. a: Assignment
5. a': Assignment
6. a' extends a
7. a |= x1 
a' |= x1
8. a |
x1 a' | x1
9. a |= x2 a' |= x2
10. a | x2 a' | x2
11. a |= x1
x2
a' |= x1x2
By: BackThru
Thm* 
a:Assignment, q,r:Formula. a |= qr 
a |= q a |= r
Generated subgoal:| 1 | a' |= x1 a' |= x2 |
About:
