proposition: Lemma typing_mulEQ x y z: x *ₑ y =ₑ z ∈ E -> Gamma__dwk ⊢₂(3) mulEQ x y z : alpha → (alpha → alpha) → alpha.
proof: Proof. intros; unfold mulEQ. split; cbn [fst snd]; [| econstructor]. repeat match goal with [|- _ ⊢(_) _ : _] => econstructor end; try reflexivity. all: try eapply Gamma__dwk_nth; eauto. all: eapply 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)