proposition: Lemma lt_a_phi0_a : forall a, lt a (phi0 a).
proof: Proof. induction a;simpl. - auto with T1. - assert (H : leq lt (cons a1 0 zero) (cons a1 n a2)). { case n. - case a2. + apply le_refl. + intros; apply lt_incl_le. auto with T1 arith. - intros; apply lt_incl_le; auto with T1 arith. } apply head_lt. destruct H as [Hlt | ]. + eapply lt_trans; eauto. + assumption. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)