apply eqv_defn.mpr
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ (y, x₁) ≃ (y, x₂)
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
x₁ x₂ : β
y : α
x✝ : x₁ ≃ x₂
⊢ y ≃ y ∧ x₁ ≃ x₂