F
M.a |= F & a |= q
r & FN.a |= F & Fconcl.a |
F
a |= r & FM.a |= F & FN.a |= F & Fconcl.a | F
FM.a |= F & FN.a |= F & a | q & Fconcl.a | F < M @ (qr.N),concl > a | < r.(M @ N),concl > a | < M @ N,q.concl > 
i.
Unfold `sequent_falsifiable` i THEN AbReduce i
THEN
Rewrite
(HigherC
(LemmaC
Thm* P:(T
Prop), L,M:T List.
x(L @ M).P(x) 
xL.P(x) & xM.P(x)))
i
THEN
AbReduce i)| 1 | 7. FM.a |= F & a |= qr & FN.a |= F & Fconcl.a | F a |= r & FM.a |= F & FN.a |= F & Fconcl.a | F
FM.a |= F & FN.a |= F & a | q & Fconcl.a | F |
About:
 |  |  |  |  |