proposition: Lemma bisim_Str_spelled: forall (S0 S1: F_coalgebra) (R :S0.(states) -> S1.(states) -> Prop) (xs:S0.(states)) (ys:S1.(states)), R xs ys -> is_F_bisimulation S0 S1 R -> fst (S0.(transition) xs) = fst (S1.(transition) ys) /\ R (snd (S0.(transition) xs)) (snd (S1.(transition) ys)).
proof: Proof. intros S0 S1 R xs ys hypR [gamma hyp_gamma]. destruct (hyp_gamma (exist (fun xy=> R (fst xy) (snd xy)) (xs,ys) hypR)) as [hyp1 hyp2]. unfold lift_F_ in *. destruct (gamma (exist (fun xy : states S0 * states S1 => R (fst xy) (snd xy)) (xs, ys) hypR)) as [b [[s1 s2] hyp]]. simpl in *. destruct (S0.(transition) xs) as [x0 xs']. destruct (S1.(transition) ys) as [y0 ys']. simpl in *. inversion hyp1; inversion hyp2. subst x0 y0 xs' ys'; split; trivial. Qed.
imports: WeaklyFinalCoalgebra