. intro x y h₂
  cases h₂
  case inl h₂ =>
    rw [h₂]
  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
case 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),
    x = y ∨ 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

case a
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 ∨ r x y
case a
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 ∨ r x y