proposition: Lemma mul_ren s t delta: ren delta (mul s t) = mul (ren delta s) (ren delta t).
proof: Proof. unfold mul; asimpl; reflexivity. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)