proposition: Lemma typing_varEQ x: x ∈ Vars__de E -> Gamma__dwk ⊢₂(3) varEQ x : alpha → (alpha → alpha) → alpha.
proof: Proof. intros; unfold varEQ. split; cbn [fst snd]. all: repeat match goal with [|- _ ⊢(_) _ : _] => econstructor end; try reflexivity. all: cbn; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)