proposition: Lemma enc_typing Gamma s n: (Gamma ⊢(2) s : alpha) -> Gamma ⊢(2) enc n s : alpha.
proof: Proof. intros; unfold enc. eapply lin_typing; auto. eapply repeated_ordertyping; [|auto]. intros ? <- % repeated_in. econstructor; auto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)