fact: Definition enc n : exp X := lambda lambda AppL (repeat (var 0) n) (var 1).
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)