Fhyp.a | F FM.a |= F a |= q & a |= r FN.a |= F

Analyze 0
THEN
OnHyps [0] (i. UnfoldTopAb i THEN AbReduce i THEN Rewrite (HigherC (LemmaC Thm* P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) xM.P(x))) i THEN AbReduce i)
THEN
RepeatOrHD -1

1	7. Fhyp.a | F Fhyp.a | F a |= q FM.a |= F FN.a |= F
2	7. FM.a |= F Fhyp.a | F a |= q FM.a |= F FN.a |= F
3	7. a |= q & a |= r Fhyp.a | F a |= q FM.a |= F FN.a |= F
4	7. FN.a |= F Fhyp.a | F a |= q FM.a |= F FN.a |= F
5	7. Fhyp.a | F Fhyp.a | F a |= r FM.a |= F FN.a |= F
6	7. FM.a |= F Fhyp.a | F a |= r FM.a |= F FN.a |= F
7	7. a |= q & a |= r Fhyp.a | F a |= r FM.a |= F FN.a |= F
8	7. FN.a |= F Fhyp.a | F a |= r FM.a |= F FN.a |= F

About: