funext a
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)
⊢ (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
case mk.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
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)
a : IContainer.B (C F) i nz
⊢ Quot.mk (fun x y => x = y ∨ r (IContainer.N (C F) i nz a) x y) (↑(kz a)).fst =
    Quot.mk (fun x y => x = y ∨ r (IContainer.N (C F) i nz a) x y) (↑(kz a)).snd