English
Dest of a corec' equals a certain lifted map: the destination of corec' g x equals appendFun id (Sum.elim id (Cofix.corec' g)) applied to g x.
Русский
Dest(corec' g x) = appendFun id (Sum.elim id (Cofix.corec' g)) <$$> g x.
LaTeX
$$$\\mathrm{dest}\\big(\\mathrm{Cofix.corec'}\\ g\\ x\\big) = \\mathrm{appendFun}\\ id (\\mathrm{Sum.elim}\\ id (\\mathrm{Cofix.corec'}\\ g)) <$$> g\\ x$$$
Lean4
theorem corec_roll {α : TypeVec n} {X Y} {x₀ : X} (f : X → Y) (g : Y → F (α ::: X)) :
Cofix.corec (g ∘ f) x₀ = Cofix.corec (MvFunctor.map (id ::: f) ∘ g) (f x₀) :=
by
mv_bisim x₀ with R a b x Ha Hb
rw [Ha, Hb, Cofix.dest_corec, Cofix.dest_corec, Function.comp_apply, Function.comp_apply]
rw [MvFunctor.map_map, ← appendFun_comp_id]
refine liftR_map_last _ _ _ _ ?_
intro a; refine ⟨a, rfl, rfl⟩
