proposition: Lemma backward_vars x: sigma • fst (varEQ x) ≡ sigma • snd (varEQ x) -> exists n, sigma x = enc n.
proof: Proof. Proof using N. intros ?. eapply enc_characteristic; trivial. cbn in H. asimpl. asimpl in H. unfold shift in *. unfold funcomp at 5 in H. asimpl in H. rewrite <-H. unfold funcomp at 4. asimpl. reflexivity. 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