a |
q 
F
M.a | F FN.a | F Fconcl.a |= F
& a | r FM.a | F FN.a | F Fconcl.a |= F
FM.a | F a | q & a | r FN.a | F Fconcl.a |= F a |= < q.(M @ N),concl > & a |= < r.(M @ N),concl > a |= < M @ (q
r.N),concl > 
P:(T
Prop), L,M:T List.
x(L @ M).P(x) xL.P(x) xM.P(x))
THENC
AbReduceC
THENC
HigherC
(LemmaC
Thm* a:Assignment, q,r:Formula.
a | qr a | q & a | r))
0| 1 | a | q FM.a | F FN.a | F Fconcl.a |= F
& a | r FM.a | F FN.a | F Fconcl.a |= F
FM.a | F a | q & a | r FN.a | F Fconcl.a |= F |
About:
 |  |  |  |  |
 |  |  |  |