proposition: Lemma enc_eta n: enc n ≡ lambda lambda (enc n) (var 1) (var 0).
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)