proposition: Lemma phi_of_any_cons : forall alpha beta1 beta2 n gamma, omega t2<= gamma \/ (0 < n)%nat -> phi alpha (gcons beta1 beta2 n gamma) = [alpha, (gcons beta1 beta2 n gamma)].
proof: Proof. cbn; intros until n; case n; destruct 1; auto with T2. generalize H; case gamma; auto with T2. - destruct 1. + discriminate H0. + lt_clean. - intro t;case t. + intro t0;case t0. * destruct 1. discriminate H0. inversion H0; lt_clean; auto with T2. * auto with T2. + auto with T2. - lt_clean; 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)