PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

At: formula imp falsifiable lemma 1 2 1 1
1. a: Assignment
2. q: Formula
3. r: Formula
4. a |= q
5. a | r

(qr under a) = 3
By:
UnfoldTopAb -1
THEN
UnfoldTopAb -2
Generated subgoal:

14. (q under a) = 3
5. (r under a) = 3
(qr under a) = 3

About:
equal