proposition: Lemma corec_computation C c : destrM (corecM C c) = # F (corecM C) (pr2 C c).
proof: Proof. apply idpath. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorCoalgebras_legacy UniMath.CategoryTheory.Categories.Type.Core UniMath.Induction.PolynomialFunctors UniMath.Induction.M.Core UniMath.Induction.M.Uniqueness