DISP	sequent_rank_df	==
ABS	sequent_rank	== S. S.H + S.C
ML	sequent_rank_unroll	let sequent_rank_unrollC = FwdMacroC `sequent_rank_pair_unrollC` (UnfoldC `sequent_rank` ANDTHENC ReduceC ) <x, y> ;; add_AbReduce_conv `sequent_rank` sequent_rank_unrollC ;;
ML	SequentRankReduce	let SequentRankReduce i = Rewrite (AllC [AbReduceC; TryC (HigherC list_rank_append_conv); AbReduceC]) i THENA Auto ;;
THM	sequent_rank_wf	Sequent
THM	sequent_rank_0_list_all_lemma	S:Sequent. S = 0 fS.H.(( f > 0)) fS.C.(( f > 0))
THM	not_list_exists_rank_gt_0_rank_0	hyp,concl:Formula List. fhyp.( f > 0) fconcl.( f > 0) <hyp, concl> = 0

the other theories