. intro x y h₁
  induction h₁
  rw [corec, QPF.M.destruct_corec]
  conv =>
    congr
    . skip
    . skip
    . rhs
      simp only [bind.automaton]
  exists (λ x => ⟨⟨x, corec (bind.automaton k) (.inr x)⟩, by rfl⟩) <$> destruct x
  rw [destruct]
  constructor
  . simp only [←QPF.map_comp, Function.comp]
    apply Eq.trans _ (QPF.map_id _)
    rfl
  . simp only [←QPF.map_comp, Function.comp]
    rfl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : QPF.M (FreeF F S)),
    corec (bind.automaton k) (Sum.inr x) = y →
      QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
        (QPF.M.destruct y)
no goals