proposition: Lemma mult_ref : forall alpha beta: t, refine (alpha * beta) = T1.T1mul (refine alpha) (refine beta).
proof: Proof. induction alpha. - cbn; destruct beta. + now cbn. + cbn; destruct p; now cbn. - induction beta. + destruct a; cbn. destruct n; now cbn. + destruct a, a0; cbn. destruct n; cbn. destruct n1; cbn; trivial. * f_equal; rewrite IHbeta; f_equal. * cbn. destruct n1. cbn. reflexivity. cbn. f_equal. f_equal. lia. rewrite IHbeta; f_equal. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )