proposition: Lemma maximal_bisimulation_conat_pred_property1: forall (S1 S2:F_coalgebra) (u:unit) s1 s2 (hyp: maximal_bisimulation _ _ s1 s2), S1.(transition) s1 = inl S1.(states) u -> maximal_bisimulation_conat_pred S1 S2 (exist (fun s1s2 => maximal_bisimulation S1 S2 (fst s1s2) (snd s1s2)) (s1, s2) hyp) = inl _ u.
proof: Proof. intros S1 S2 u x y hyp hyp1. unfold maximal_bisimulation_conat_pred. destruct (conat_transition_dec_inf S1 x) as [[starX hyp_trX]|[x' hyp_trX]]. f_equal; induction starX; destruct u; reflexivity. apply False_ind; rewrite hyp1 in hyp_trX; discriminate hyp_trX. Qed.
imports: WeaklyFinalCoalgebra