proposition: Lemma enc_succ n s f: enc (S n) s f ≡ f (enc n s f).
proof: Proof. now rewrite !enc_app. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)