proposition: Lemma lt_embed (alpha beta : OO): lt alpha beta -> E0lt (embed alpha) (embed beta).
proof: Proof. destruct alpha, beta; unfold lt, E0lt, T1.LT; cbn; repeat split. - now apply nf_ref. - now apply lt_ref. - now apply nf_ref. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )