proposition: Lemma GT_typing Gamma m n: Gamma ⊢(2) T n m : alpha → alpha → alpha → alpha.
proof: Proof. do 3 econstructor. eapply lin_typing; [|eauto]. rewrite repeated_tab. simplify. eapply tab_typing. intros; econstructor; cbn. econstructor. all: eauto using enc_typing. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)