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_CoPeano_bisimilar_spelled. generalize (lift_F_extensionality_bisim_CoPeano _ f0 f1 bx hyp_eq). destruct bx as [u|bx']; fold w. intros [hyp1 hyp2]; rewrite hyp1; rewrite hyp2; trivial. intros (s1' & s2' & hyp1 & hyp2 & hyp3). rewrite hyp1; rewrite hyp2. constructor 2 with s1' s2'; simpl; trivial. Defined.
imports: WeaklyFinalCoalgebra