have : P x₂ → P x₁ := P_subst (symm ‹x₁ ≃ x₂›)
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this : P x₁ → P x₂
⊢ P x₁ ↔ P x₂
α : Sort u
inst✝ : EqvOp α
P : α → Prop
P_subst : ∀ {y₁ y₂ : α}, y₁ ≃ y₂ → P y₁ → P y₂
x₁ x₂ : α
x✝ : x₁ ≃ x₂
this✝ : P x₁ → P x₂
this : P x₂ → P x₁
⊢ P x₁ ↔ P x₂