proposition: Lemma typing_F x: x ∈ Vars__de E -> Gamma__deq ⊢(2) @var ag (F x) : alpha → alpha.
proof: Proof. intros H. econstructor. cbn; auto. now eapply Gamma__deq_nth_F, Fs_in. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)