proposition: Lemma forward_vars x n: sigma x = enc n -> sigma • fst (varEQ x) ≡ sigma • snd (varEQ x).
proof: Proof. intros; unfold varEQ, fst, snd. cbn. unfold shift, var_zero, funcomp; rewrite H; asimpl. rewrite !enc_app. change (var 0 (var 1)) with (@AppL X (repeat (var 0) 1) (var 1)). now rewrite <-AppL_app, <-repeated_plus, Nat.add_comm. 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