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