proposition: Lemma mul_subst s t sigma: sigma • (mul s t) = mul (sigma • s) (sigma • t).
proof: Proof. unfold mul; asimpl; cbn. do 4 f_equal. now asimpl. now asimpl. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)