proposition: Lemma maximal_bisimulation_conat_pred_property2: forall (S1 S2:F_coalgebra) s1 s2 (hyp: maximal_bisimulation _ _ s1 s2) s1' s2' (hyp': maximal_bisimulation _ _ s1' s2'), S1.(transition) s1 = inr unit s1' -> S2.(transition) s2 = inr unit s2' -> { hyp'' | maximal_bisimulation_conat_pred S1 S2 (exist (fun s1s2 => maximal_bisimulation S1 S2 (fst s1s2) (snd s1s2)) (s1, s2) hyp) = inr unit (exist (fun s1s2 => maximal_bisimulation S1 S2 (fst s1s2) (snd s1s2)) (s1', s2') hyp'')}.
proof: Proof. intros S1 S2 x y hyp s1' s2' hyp' hyp1 hyp2. unfold maximal_bisimulation_conat_pred. destruct (conat_transition_dec_inf S1 x) as [[starX hyp_trX]|[x' hyp_trX]]. apply False_ind; rewrite hyp1 in hyp_trX; discriminate hyp_trX. destruct (conat_transition_dec_inf S2 y) as [[starY hyp_trY]|[y' hyp_trY]]. apply False_ind; rewrite hyp2 in hyp_trY; discriminate hyp_trY. assert (hyp_s1':x'=s1'); [rewrite hyp1 in hyp_trX; rewrite <- (inr_injection _ _ _ _ hyp_trX); trivial|]. assert (hyp_s2':y'=s2'); [rewrite hyp2 in hyp_trY; rewrite <- (inr_injection _ _ _ _ hyp_trY); trivial|]. rewrite <- hyp_s1' in hyp'; rewrite <- hyp_s2' in hyp'; rewrite <- hyp_s1'; rewrite <- hyp_s2'. exists (match hyp with | max_bisim_conat_O hyp_bis1 _ => False_ind (maximal_bisimulation S1 S2 x' y') (eq_ind (inl (states S1) tt) (fun e : F_ (states S1) => match e with | inl _ => True | inr _ => False end) I (inr unit x') (eq_ind (transition S1 x) (fun f : F_ (states S1) => f = inr unit x') hyp_trX (inl (states S1) tt) hyp_bis1)) | max_bisim_conat_S s1'0 s2'0 hyp_bis1 hyp_bis2 hyp0 => eq_ind s1'0 (fun x'0 : states S1 => maximal_bisimulation S1 S2 x'0 y') (eq_ind s2'0 (fun y'0 : states S2 => maximal_bisimulation S1 S2 s1'0 y'0) hyp0 y' (inr_injection (states S2) unit s2'0 y' (eq_ind (transition S2 y) (fun f : F_ (states S2) => f = inr unit y') hyp_trY (inr unit s2'0) hyp_bis2))) x' (inr_injection (states S1) unit s1'0 x' (eq_ind (transition S1 x) (fun f : F_ (states S1) => f = inr unit x') hyp_trX (inr unit s1'0) hyp_bis1)) end). reflexivity. Defined.
imports: WeaklyFinalCoalgebra