a |= z
}}
s
L.(
(s) = 0)sL.(
disjoint(eqF;s.H;s.C))eqF) z.HeqF) z.CFz.H.a |= F Fz.C.a |
F a |= z
F. a |= F );`L',z.H;`z',x]
(FwdThru
Thm* eq:{T=}, P:(T
Prop), L:T List.
xL.P(x) 
(z:T. z(eq) L 
P(z))
[11])| 1 | 13. a |= x a |= z |
About:
 |  |  |  |  |  |