fact: Fixpoint length (t:T2) : nat := match t with zero => 0 | cons a b n v => nbterms (cons a b n v) + 2 * (max (length a) (max (length b) (length_aux v))) end with length_aux (t:T2) : nat := match t with zero => 0 | cons a b n v => max (length a) (max (length b) (length_aux v)) end.
imports: Arith Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP Gamma0_prelude