proposition: Lemma compare_ref (a b : t) : compare a b = compare (refine a) (refine b).
proof: Proof. revert b; induction a. - destruct b. + easy. + cbn. now destruct p. - destruct a, b. + now cbn. + destruct p; cbn. destruct (n ?= n1) eqn: cn_n1; destruct (n0 ?= n2) eqn: c_n0_n2; rewrite compare_fin_rw; now rewrite cn_n1. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )