. intro i 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 [←imap_spec, ←imap_spec]
    conv =>
      congr <;> rw [←abs_repr z]
    rw [←abs_imap]
    rw [←abs_imap]
    cases repr z with | mk nz kz =>
    simp only [IContainer.Map, Function.comp]
    apply congrArg abs
    rw [Sigma.mk.inj_iff]
    simp only [true_and, heq_eq_eq]
    funext a
    apply Quot.sound
    right
    apply (kz a).2
case h₁
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ ∀ (i : I) (x y : M F i),
    x = y ∨ r i x y →
      IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
        IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ x = y ∨ r i x y
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ x = y ∨ r i x y