proposition: Lemma lt_cons_phi0_inv alpha n beta gamma : cons alpha n beta t1< phi0 gamma <-> beta t1< phi0 alpha /\ alpha t1< gamma.
proof: Proof. split. - destruct 1 as [H [H0 H1]]; repeat split; eauto with T1. apply lt_a_phi0_b_inv in H0; auto. rewrite nf_LT_iff in H. destruct H; eauto with T1. destruct H2; eauto with T1. now apply lt_a_phi0_b_inv in H0. - destruct 1. apply LT2; auto. rewrite nf_LT_iff; eauto with T1. eauto with T1. 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)