proposition: Lemma lt_ref (a b : t) : lt a b <-> T1.lt (refine a) (refine b).
proof: Proof. unfold lt, T1.lt; rewrite compare_ref; now split. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )