simp only [←QPF.map_comp, Function.comp]
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x