At: assignment monotone 1 1 5 1 1 2 1
1. f: Formula
2. y1: Formula
3. y2: Formula
4. a: Assignment
5. a': Assignment
6. a' extends a
7. a |= y1 
a' |= y1
8. a |
y1 a' | y1
9. a |= y2 a' |= y2
10. a | y2 a' | y2
11. a | y1
y2
12. a |= y1
13. a | y2
a' | y1y2
By: BackThru
Thm* 
a:Assignment, q,r:Formula. a | qr 
a |= q & a | r
Generated subgoal:| 1 | a' |= y1 & a' | y2 |
About:
