proposition: Lemma gf_typing Gamma n: Gamma ⊢(2) gf n : alpha → alpha.
proof: Proof. econstructor. eapply enc_typing. eauto. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)