proposition: Lemma typing_mul x y z: x *ₑ y =ₑ z ∈ E -> Gamma__deq ⊢₂(2) mulEQ x y z : alpha → alpha → alpha.
proof: Proof. intros; unfold mulEQ; split; cbn [fst snd]; autotype; auto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)