fact: Fixpoint max_sequent_numb_hyps (l:list term) : nat := match l with nil => O | cons a m => let i := (sequent_numb_hyps a) in let j := (max_sequent_numb_hyps m) in match (pos_ineq (nat_pos i) (nat_pos j)) with i_lt => j | _ => i end end.