a:Assignment, q,r:Formula. a |
q
r 
a | q 
a | r
formula_and_falsifiable_lemma
q == inr(inr(inl( < p,q > )))
Thm* a:Assignment, q,r:Formula. a | qr a | q a | r
formula_and_falsifiable_lemma
Thm* a:Assignment, q,r:Formula. a |= qr 
a |= q & a |= r
formula_and_sat_lemma1
Thm* a:Assignment, q,r:Formula. a |= qr a |= q & a |= r
formula_and_sat_lemma