proposition: Lemma lift_F_extensionality_bisim: forall (X:Set) (f0 f1:X->w.(states)) bx, (forall x, f0 x (=) f1 x) -> rel_image_lift_F_ _ _ bisimilar (lift_F_ _ _ f0 bx) (lift_F_ _ _ f1 bx).
proof: Proof. intros X f0 f1 bx hyp_eq. apply <- rel_image_lift_F_Str_bisimilar_spelled. apply lift_F_extensionality_bisim_Str; assumption. Defined.
imports: WeaklyFinalCoalgebra