proposition: Lemma rel_image_lift_F_CoPeano_bisimilar_spelled: forall (b_x b_y: F_ CoPeano.(states)), rel_image_lift_F_ _ _ bisimilar b_x b_y <-> match b_x, b_y with | inl starX, inl starY => starX = starY | inr b_x', inr b_y' => co_S b_x' (=) co_S b_y' | _, _ => False end.
proof: Proof. intros [ux|x] [uy|y]; simpl; unfold rel_image_lift_F_; split; simpl; intros hyp. destruct ux; destruct uy; reflexivity... exists co_O; exists co_O; repeat split; simpl. constructor 1; simpl; trivial. destruct ux; destruct uy; reflexivity. destruct ux; destruct uy; reflexivity... destruct hyp as [x [y' [hyp [hyp1 hyp2]]]]. inversion hyp as [hyp3 hyp4|s1' s2' hyp3 hyp4 hyp5]; simpl in *. rewrite <- hyp2 in hyp4; discriminate hyp4. rewrite <- hyp1 in hyp3; discriminate hyp3... contradiction... destruct hyp as [x' [y [hyp [hyp1 hyp2]]]]. inversion hyp as [hyp3 hyp4|s1' s2' hyp3 hyp4 hyp5]; simpl in *. rewrite <- hyp1 in hyp3; discriminate hyp3. rewrite <- hyp2 in hyp4; discriminate hyp4... contradiction... destruct hyp as [x' [y' [hyp [hyp1 hyp2]]]]; replace (co_S x) with x'; [replace (co_S y) with y'; trivial|]; apply pred_inr_co_S; assumption... exists (co_S x); exists (co_S y); repeat split; simpl; assumption. Qed.
imports: WeaklyFinalCoalgebra