proposition: Lemma Lam_bisimulation_4_1_5_lambda_star_iterate : forall (Lambda:T_over_B_distributive) (j:nat) (Xtb:F_algebra) (tjbx : T_iter j (B_ Xtb.(carrier))), iterate_algebra j (Build_F_algebra _ (fun tbx=> lift_B_ _ _ Xtb.(operation) (Lambda.(lambda_) _ tbx))) tjbx = lift_B_ _ _ (fun x => iterate_algebra j Xtb x) (lambda_iter_ Lambda j _ tjbx).
proof: Proof. intros [lam_ lam_nat_] j; induction j; intros [X beta_X] tjbx; unfold carrier, operation. apply lift_B_id. simpl. fold T_. set (tmp:=lift_T_iter (T_ (B_ X)) (B_ X) (fun tbx => lift_B_ (T_ X) X beta_X (lam_ X tbx)) j tjbx). assert (hyp_rewrite_tmp:=IHj (Build_F_algebra X beta_X) tmp). fold T_ in hyp_rewrite_tmp. simpl in hyp_rewrite_tmp. rewrite hyp_rewrite_tmp; clear hyp_rewrite_tmp. rewrite <- (lift_B_compose (T_iter j (T_ X)) (T_iter j X) X _ (iterate_algebra j (Build_F_algebra X beta_X))). assert (left_commut:lambda_iter_ (Build_T_over_B_distributive lam_ lam_nat_) j X tmp= lift_B_ (T_iter j (T_ X)) (T_iter j X) (lift_T_iter (T_ X) X beta_X j) (lambda_iter_ (Build_T_over_B_distributive lam_ lam_nat_) j (T_ X) (lift_T_iter (T_ (B_ X)) (B_ (T_ X)) (lam_ X) j tjbx))); [|rewrite left_commut; apply lift_B_extensionality; trivial]. subst tmp. rewrite <- (lift_T_iter_compose (T_ (B_ X)) (B_ (T_ X)) _ (lam_ X)). fold lift_T_iter. set (tmp2:=lift_T_iter (T_ (B_ X)) (B_ (T_ X)) (lam_ X) j tjbx). symmetry. apply lambda_iter_naturality. Qed.
imports: LambdaCoiteration