F
M.a |
F 
a | q & a | r FN.a | F Fconcl.a |= F 
r.N),concl > ) a |= < M @ (qr.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 | FM.a | F a | q & a | r FN.a | F Fconcl.a |= F |
About:
 |  |  |  |  |
 |  |  |  |