proposition: Lemma eq_ref (a b : t) : a = b <-> refine a = refine b.
proof: Proof. destruct (compare_correct a b). - split. + intro; now subst. + trivial. - split. + intro; now subst. + rewrite lt_ref in H. intros H0; rewrite H0 in H. destruct (T1.lt_irrefl H). - split. + intro; now subst. + rewrite lt_ref in H. intros H0; rewrite H0 in H. destruct (T1.lt_irrefl H). Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )