rw [←QPF.M.map_comp]
case h₀.right
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
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
case h₀.right
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
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y