rw [h₂]
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : x = y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
no goals