proposition: Lemma lt_trans (a b c : t): lt a b -> lt b c -> lt a c.
proof: Proof. rewrite !lt_ref; apply T1.lt_trans. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )