proposition: Lemma Lam_coiterator_uniqueness: forall (Lambda:T_over_B_distributive) (Xbt: BT_coalgebroid) (f g:Xbt.(bs_states) -> w.(states)), (forall x, w.(transition) (f x) = lift_B_ _ _ (Beta Lambda) (lift_B_ _ _ (lift_T_ _ _ f) (Xbt.(bs_transition) x))) -> (forall x, w.(transition) (g x) = lift_B_ _ _ (Beta Lambda) (lift_B_ _ _ (lift_T_ _ _ g) (Xbt.(bs_transition) x))) -> forall x, f x (=) g x.
proof: Proof. intros Lambda Xbt f g hyp_f hyp_g. apply (lambda_coinduction_lambda_bialgebras_like Lambda Xbt (Build_TB_bialgebra w (Beta Lambda)) (Build_TB_bialgebra w (Beta Lambda)) f g). apply weakly_final_lambda_bialgebra. apply weakly_final_lambda_bialgebra. unfold is_like_lambda_bismulation; intros rtb; symmetry; simpl in *; rewrite (hyp_f rtb); rewrite lift_B_compose; trivial. unfold is_like_lambda_bismulation; intros rtb; symmetry; simpl in *; rewrite (hyp_g rtb); rewrite lift_B_compose; trivial. Qed.
imports: LambdaCoiteration