proposition: Lemma phi_of_psi_plus_fin : forall a b1 b2 n, a t2< b1 -> phi a (gcons b1 b2 0 (fin n)) t2< [a ,gcons b1 b2 0 (fin n)].
proof: Proof. cbn; intros until n;case n. - cbn; intro H;rewrite (compare_rw_lt H);auto with T2. - cbn; intros n0 H;rewrite (compare_rw_lt H). case n0;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)