proposition: Lemma cons_rw : forall a b n c, (n=0 /\ c=zero /\ (T2_2_term (gcons a b n c)= (Term ord_psi ((T2_2_term a)::(T2_2_term b)::nil)))) \/ (T2_2_term (gcons a b n c)= Term ord_cons ((Term ord_psi ((T2_2_term a)::(T2_2_term b)::nil)) ::(nat_2_term n)::(T2_2_term c)::nil)).
proof: Proof. destruct n. - destruct c. + left;simpl;auto with T2. + right;simpl;auto with T2. - right;simpl;auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)