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