proposition: Lemma lambda_corecursion_natural: forall (X Y : Set) (f : X -> Y) (sbx : T_ (B_ X)), lambda_corecursion Y (lift_T_ (B_ X) (B_ Y) (lift_B_ X Y f) sbx) = lift_B_ (T_ X) (T_ Y) (lift_T_ X Y f) (lambda_corecursion X sbx).
proof: Proof. intros X Y f [bx | w0]; simpl. unfold identity_as_Set_Functor.lift_F_; do 2 rewrite lift_B_compose; apply lift_B_extensionality; trivial. rewrite lift_B_compose; unfold Weak_fin_coalg_as_Set_Functor.lift_F_; apply lift_B_extensionality; trivial. Qed.
imports: WeaklyFinalCoalgebra