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 r.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:
 |  |  |  |