proposition: Lemma normal_enc n: normal (enc n).
proof: Proof. do 2 eapply normal_lam_intro. induction n; cbn; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)