proposition: Lemma forward_consts: n = 1 -> sigma • fst (constEQ x) ≡ sigma • snd (constEQ x).
proof: Proof. Proof using EQx. intros; unfold constEQ, fst, snd. subst. asimpl; now rewrite EQx. 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