proposition: Lemma plus_ref : forall alpha beta: t, refine (alpha + beta) = T1.T1add (refine alpha) (refine beta).
proof: Proof. induction alpha, beta. - now cbn. - now cbn. - cbn; destruct a. now cbn. - destruct a, p; cbn; destruct (n ?= n1) eqn:cn_n1. 1,2: rewrite T1.compare_fin_rw in *; rewrite cn_n1; now cbn. rewrite T1.compare_fin_rw in *; cbn;rewrite cn_n1, IHalpha; now cbn. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )