apply congrArg abs
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ abs { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst } =
    abs { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd }
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst } =
    { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd }