proposition: Lemma eq_corecM0 m0 : corecM0 M0 m0 = m0.
proof: Proof. induction finalM0 as [[G H1] H2]. cbn. specialize (H2 (coalgebra_homo_id F M0)). change (pr1 (G,, H1) m0 = pr1 (coalgebra_homo_id F M0) m0). apply (maponpaths (fun X => pr1 X m0)). apply pathsinv0. assumption. 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