proposition: Lemma lift_F_extensionality: forall (X Y:Set) (f0 f1:X->Y) bx, (forall x, f0 x = f1 x) -> lift_F_ _ _ f0 bx = lift_F_ _ _ f1 bx.
proof: Proof. intros X Y f0 f1 bx hyp_ext; unfold lift_F_; destruct bx as [b x]; repeat rewrite hyp_ext; trivial. Qed.
imports: WeaklyFinalCoalgebra