proposition: Lemma lift_F_extensionality_bisim_Str: forall (X:Set) (f0 f1:X->Str.(states)) bx, (forall x, f0 x (=) f1 x) -> fst (lift_F_ _ _ f0 bx) = fst (lift_F_ _ _ f1 bx) /\ snd (lift_F_ _ _ f0 bx) (=) snd (lift_F_ _ _ f1 bx).
proof: Proof. intros X f0 f1 bx hyp_ext. unfold lift_F_. destruct bx as [b x]; split; simpl; trivial. Qed.
imports: WeaklyFinalCoalgebra