rw [←imap_spec, ←imap_spec]
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
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).fst) z) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).snd) z)
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
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) z =
    IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) z