case inr h₂ =>
  have ⟨z, h₃⟩ := h₀ _ _ h₂
  clear h₂
  rw [←h₃.1, ←h₃.2]
  clear h₃
  rw [←map_comp, ←map_comp]
  conv =>
    congr <;> rw [←abs_repr z]
  rw [←abs_map]
  rw [←abs_map]
  cases repr z with | mk nz kz =>
  simp only [Container.Map, Function.comp]
  apply congrArg abs
  rw [Container.Obj.snd_equals_iff]
  funext a
  apply Quot.sound
  right
  apply (kz a).2
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₂ : r 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