proposition: Lemma typing_equations q e: e ∈ E -> q ∈ eqs e -> Gamma__deq ⊢₂(2) q : alpha → alpha → alpha.
proof: Proof. intros H H1; destruct e; cbn in H1; intuition; subst; auto using typing_const, typing_add, typing_mul. all: eapply typing_var_eq; autotype. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)