proposition: Lemma length_psi : forall a b n c, length [a, b] <= length (cons a b n c).
proof: Proof. simpl. intros; apply le_lt_n_Sm. match goal with [ |- ?a <= ?b + ?c + ?d] => rewrite (plus_comm (b + c) d) end. apply le_plus_trans. replace (max (length b) 0) with (length b). repeat rewrite plus_0_r. apply plus_le_compat; apply max_le_regL; apply le_max_l. rewrite max_l;auto with arith. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP Gamma0_prelude