proposition: Lemma E0lt_wf : well_founded E0lt.
proof: Proof. split; intros [t Ht] H; apply (Acc_inverse_image _ _ LT (@cnf) {| cnf := t; cnf_ok := Ht |}); now apply T1.nf_Acc. Defined.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)