proposition: Lemma rel_image_lift_F_Str_bisimilar_spelled: forall (b_x b_y: F_ Str.(states)), rel_image_lift_F_ _ _ bisimilar b_x b_y <-> fst b_x = fst b_y /\ snd b_x (=) snd b_y.
proof: Proof. intros [b_x [x xs]] [b_y [y ys]]. simpl; unfold rel_image_lift_F_. split; simpl. intros [x0 [y0 [[eq_1 eq_2] [eq_3 eq_4]]]]. split. simpl in eq_1, eq_2. transitivity (hd x0);[|transitivity (hd y0); trivial; symmetry]; match goal with | [ id1 : (?X1, ?X3) = _ |- ?X1 =?X2 ] => match goal with | [ id2: _ = (?X2, ?X4) |- ?X1 =?X2 ] => change (fst(X1,X3)= fst(X2,X4));apply f_equal; trivial end end. apply trans_bisimilar with (tl x0);[|apply trans_bisimilar with (tl y0); trivial; apply sym_bisimilar]; match goal with | [ id1 : (?X3, ?X1) = _ |- ?X1 (=)?X2 ] => match goal with | [ id2: _ = (?X4, ?X2) |- ?X1 (=)?X2 ] => change (snd(X3,X1)(=) snd(X4,X2)); rewrite <- id2 end end; apply refl_bisimilar. intros [hyp1 hyp2]. simpl. exists (Cons b_x (Cons x xs)). exists (Cons b_y (Cons y ys)). split. constructor; assumption. split; simpl; trivial. Qed.
imports: WeaklyFinalCoalgebra