proposition: Lemma lt_irrefl (a : t): ~ lt a a.
proof: Proof. rewrite lt_ref; now apply T1.lt_irrefl. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )