fact: Fixpoint iterate_algebra (j:nat) (X:F_algebra) {struct j} : T_iter j X.(carrier) -> X.(carrier):= match j with | O => fun tx => tx | S j' => fun tx => iterate_algebra j' X (lift_T_iter _ _ X.(operation) j' tx) end.
imports: LambdaCoiteration