proposition: Lemma forward_mult : m * n = p -> sigma • fst (mulEQ x y z) ≡ sigma • snd (mulEQ x y z).
proof: Proof. Proof using EQz EQy EQx. intros; unfold mulEQ, fst, snd; asimpl. now rewrite EQx, EQy, EQz, <-enc_mul, H. Qed.
imports: List Arith Lia Undecidability.HOU(std.std calculus.calculus) Undecidability.HOU.second_order(diophantine_equations dowek.encoding) Undecidability.HOU.unification.nth_order_unification