proposition: Lemma cons_lt_epsilon0 : forall a b n c, gcons a b n c t2< epsilon0 -> nf (gcons a b n c) -> a = zero /\ b t2< epsilon0 /\ c t2< epsilon0.
proof: Proof. intros a b n c H; inversion H using lt_02. - split. + apply lt_one_inv;auto with T2. + split. * exact H1. * apply lt_trans with (gcons a b n c);auto with T2. apply lt_tail;auto with T2. - inversion 1. - inversion 2. - inversion 1. - inversion 1. 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)