( < hyp,concl > ) = 0( < hyp,concl > ) = 0 
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)fconcl.((f) > 0) L:Sequent List.
sL.((s) = 0) & (sL.|= s |= < hyp,concl > ) & (a:Assignment. sL.a | s a | < hyp,concl > )( < hyp,concl > ) = 0)| 1 | ( < hyp,concl > ) = 0 |
| 2 | 6. ( < hyp,concl > ) = 0 L:Sequent List.
sL.((s) = 0) & (sL.|= s |= < hyp,concl > ) & (a:Assignment. sL.a | s a | < hyp,concl > ) |
About:
 |  |  |  |  |  |
 |  |  |  |  |