proposition: Lemma typing_enc Gamma n: Gamma ⊢(3) enc n : alpha → (alpha → alpha) → alpha.
proof: Proof. unfold enc. econstructor. econstructor. eapply AppL_ordertyping_repeated; [|eauto]. eapply repeated_ordertyping; simplify; trivial. intros ? <- % repeated_in; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)