a |= q & a |= r & 
F
M.a |= F & FN.a |= F & Fconcl.a |
F
FM.a |= F & a |= q & a |= r & FN.a |= F & Fconcl.a | F a | < [q; 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 & 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:
 |  |  |  |