proposition: Lemma backward_consts: sigma • fst (constEQ x) ≡ sigma • snd (constEQ x) -> n = 1.
proof: Proof. Proof using EQx. intros EQ; unfold constEQ, fst, snd in EQ. asimpl in EQ. rewrite EQx in EQ. eapply enc_equiv_injective; eauto. 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