proposition: Lemma lt_wf : well_founded lt.
proof: Proof. specialize (ON_Generic.wf_measure (B:= OO) embed); intro Hm; unfold ON_Generic.measure_lt in Hm; eapply wf_incl; [| eassumption]. intros x y Hxy; red; now apply lt_embed. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )