proposition: Lemma lift_F_extensionality_bisim_CoPeano: forall (X:Set) (f0 f1:X->CoPeano.(states)) bx, (forall x, f0 x (=) f1 x) -> match bx with | inl starX => lift_F_ _ _ f0 bx = inl _ tt /\ lift_F_ _ _ f1 bx=inl _ tt | inr b_x' => exists s1', exists s2', lift_F_ _ _ f0 bx = inr unit s1' /\ lift_F_ _ _ f1 bx = inr _ s2' /\ s1' (=) s2' end.
proof: Proof. intros X f0 f1 bx hyp_ext. unfold lift_F_. destruct bx as [u|x']. split; destruct u; trivial. exists (f0 x'); exists (f1 x'); repeat split; trivial. Qed.
imports: WeaklyFinalCoalgebra