clear 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
z : F { p // r p.fst p.snd }
h₃ : (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).fst) <$> z =
    (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).snd) <$> z
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
z : F { p // r p.fst p.snd }
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).fst) <$> z =
    (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).snd) <$> z