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
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
h₂ : 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)
no goals