S:Sequent.
(S) < (G) 
(
L:Sequent List. s
L.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a |
s a | S))
L:Sequent List. sL.((s) = 0) & (sL.|= s |= G ) & (a:Assignment. sL.a | s a | G) L:Sequent List. sL.((s) = 0) & (sL.|= s |= G ) & (a:Assignment. sL.a | s a | G) 
CompNatInd 1)| 1 | 2. S:Sequent.
(S) < (G)
(L:Sequent List. sL.((s) = 0) & (sL.|= s |= S ) & (a:Assignment. sL.a | s a | S)) L:Sequent List. sL.((s) = 0) & (sL.|= s |= G ) & (a:Assignment. sL.a | s a | G) |
About:
 |  |  |  |  |
 |  |  |  |