rfl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x✝ y x : QPF.M (FreeF F S)
⊢ (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (x, corec (bind.automaton k) (Sum.inr x)).fst
    (x, corec (bind.automaton k) (Sum.inr x)).snd
no goals