proposition: Lemma delta_is_F_bisimulation (S1:F_coalgebra) :is_F_bisimulation _ _ (@eq S1.(states)).
proof: Proof. unfold is_F_bisimulation. exists (fun s1s2_h=>lift_F_ _ _ (fun (s:S1.(states))=>exist (fun z => (fst z = snd z)) (s,s) (refl_equal s)) (S1.(transition) (fst (proj1_sig s1s2_h)))). intros [[s1 s2] hyp]; split; simpl; simpl in hyp; rewrite lift_F_compose; rewrite lift_F_id; [| rewrite hyp]; trivial. Defined.
imports: ExtensionalFunctor Setoid