funext _
case h
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ Functor.map
      ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) =
    Functor.map id
case h.h
F : Type u₁ → Type u₁
inst : QPF F
x✝¹ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
x✝ : F (M F)
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      x✝ =
    id <$> x✝