(S) == (S.H)+(S.C)
hyp,concl:Formula List. 
f
hyp.((f) > 0) 
fconcl.((f) > 0) ( < hyp,concl > ) = 0
| def | sequent_rank | (S) == (S.H)+(S.C) |
| THM | not_list_exists_rank_gt_0_rank_0 | hyp,concl:Formula List. fhyp.((f) > 0) fconcl.((f) > 0) ( < hyp,concl > ) = 0 |