fact: Definition Beta_iter (j:nat) (X:TB_bialgebra) : T_iter j (states X.(coalgebra_part)) ->states X.(coalgebra_part):= iterate_algebra j (Build_F_algebra (states X.(coalgebra_part)) X.(algebra_part)).
imports: LambdaCoiteration