proposition: Lemma typing_equations d e: e ∈ E -> d ∈ eqs e -> Gamma__dwk ⊢₂(3) d : alpha → (alpha → alpha) → alpha.
proof: Proof. intros H H1; destruct e; cbn in H1; intuition idtac; subst. all: eauto using typing_constEQ, typing_addEQ, typing_mulEQ. all: eapply typing_varEQ, Vars__de_in; eauto; cbn; intuition. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)