proposition: Lemma commutativity_Lam_coiterator_rel_image_lifting (Lambda:T_over_B_distributive) (BS: BT_coalgebroid) (x:BS.(bs_states)) : rel_image_lift_B_ w w bisimilar (w.(transition) (Lam_coiterator Lambda BS x)) ( lift_B_ _ _ (Beta Lambda) (lift_B_ _ _ (lift_T_ _ _ (Lam_coiterator Lambda BS)) (bs_transition BS x))).
proof: Proof. destruct BS as [X X_tr]. unfold Lam_coiterator. rewrite (commutativity_F_unfold (Build_F_coalgebra (T_star_ X) (fun x0 : T_star_ X => lift_B_ (T_star_ (T_ X)) (T_star_ X) (Chi X) (lambda_star Lambda (T_ X) (lift_T_star_ X (B_ (T_ X)) X_tr x0)))) (T_star_coproject_ X 0 x)). set (i0:=T_star_coproject_ X 0). set (i1:=T_star_coproject_ X 1). set (T_star_phi:=lift_T_star_ _ _ X_tr). set (lambda_star_SX := lambda_star Lambda (T_ X)). set (B_Chi_X := lift_B_ _ _ (Chi X)). set (h := F_unfold (Build_F_coalgebra (T_star_ X) (fun x=> B_Chi_X (lambda_star_SX (T_star_phi x))))). unfold transition, bs_transition, bs_states. assert (rwt_tmp:=lift_B_compose _ _ _ (lift_T_ _ _ (fun x0 : X => h (i0 x0))) (Beta Lambda) (X_tr x)). fold T_ lift_B_; fold T_ lift_B_ in rwt_tmp; rewrite rwt_tmp. assert (square1:(T_star_coproject_ (B_ (T_ X)) 0 ) (X_tr x) = T_star_phi (i0 x)); trivial. rewrite <- square1. assert (triangle2:(lift_B_ _ _ (T_star_coproject_ (T_ X) 0 )) (X_tr x) = (lambda_star_SX (T_star_coproject_ (B_ (T_ X)) 0 (X_tr x)))); [destruct Lambda; trivial|]. rewrite <- triangle2. assert (triangle3:(lift_B_ _ _ (T_star_coproject_ X 1) (X_tr x))=B_Chi_X (lift_B_ _ _ (T_star_coproject_ (T_ X) 0) (X_tr x))); [unfold B_Chi_X; rewrite lift_B_compose; apply lift_B_extensionality; trivial|]. rewrite <- triangle3. unfold T_iter. clear rwt_tmp. assert (rwt_tmp:=(lift_B_compose _ _ _ (T_star_coproject_ X 1) h (X_tr x))). unfold states at 1. simpl; simpl in rwt_tmp; fold lift_B_ in rwt_tmp; rewrite rwt_tmp. apply (lift_B_extensionality_bisim (T_ X) (fun x0=> h (i1 x0)) (fun x0:T_ X=> Beta Lambda (lift_T_ X w.(states) (fun x1 : X => h (i0 x1)) x0))). apply (Lam_coiterator_4_11_bisim Lambda (Build_BT_coalgebroid X X_tr)). Qed.
imports: WeaklyFinalCoalgebra