M,N:Formula List, f:Formula. 
(f) > 0 & hyp = (M @ (f.N))
L:Sequent List.
s
L.((s) = 0) & (sL.|= s 
|= < hyp,concl > ) & (a:Assignment. sL.a |
s a | < hyp,concl > )S:Sequent.
(S) < ( < hyp,concl > )
(L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S))fhyp.((f) > 0) L:Sequent List.
sL.((s) = 0) & (sL.|= s |= < hyp,concl > ) & (a:Assignment. sL.a | s a | < hyp,concl > )P:(T
Prop), L:T List.
xL.P(x) 
(M,N:T List, x:T. P(x) & L = (M @ (x.N)))
[-1]| 1 | 5. M,N:Formula List, f:Formula. (f) > 0 & hyp = (M @ (f.N)) L:Sequent List.
sL.((s) = 0) & (sL.|= s |= < hyp,concl > ) & (a:Assignment. sL.a | s a | < hyp,concl > ) |
About:
 |  |  |  |  |  |
 |  |  |  |  |