proposition: Lemma typing_a Gamma: Gamma ⊢(2) a : alpha.
proof: Proof. econstructor; cbn; auto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)