proposition: Lemma Lam_bisimulation_4_1_5_iterate_pres_algebra_morphism :forall (j:nat) (Xa Ya:F_algebra) (f: Xa.(carrier) -> Ya.(carrier)), (forall tx, Ya.(operation) (lift_T_ _ _ f tx) = f (Xa.(operation) tx)) -> forall tjx, iterate_algebra j Ya (lift_T_iter _ _ f j tjx) = f (iterate_algebra j Xa tjx).
proof: Proof. induction j; intros [X beta_X] [Y beta_Y] f hyp_alg_map tjx; simpl in *; trivial. rewrite <- (IHj (Build_F_algebra X beta_X) (Build_F_algebra Y beta_Y) f hyp_alg_map). rewrite lift_T_iter_compose; fold lift_T_iter; simpl. f_equal. rewrite lift_T_iter_compose; fold lift_T_iter; simpl. apply lift_T_iter_extensionality. assumption. Qed.
imports: LambdaCoiteration