proposition: Lemma backward_add: sigma • fst (addEQ x y z) ≡ sigma • snd (addEQ x y z) -> m + n = p.
proof: Proof. Proof using EQz EQy EQx. intros EQ; unfold addEQ, fst, snd in EQ; asimpl in EQ. rewrite EQx, EQy, EQz, <-enc_add in EQ. eauto using enc_equiv_injective. 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