rw [Sigma.mk.inj_iff]
case mk
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
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst } =
    { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd }
case mk
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
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ nz = nz ∧
    HEq (fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst) fun y =>
      Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd