proposition: Lemma lambda_star_naturality: forall (Lambda : T_over_B_distributive) (X Y : Set) (f : X -> Y) (tsbx : T_star_ (B_ X)), lift_B_ (T_star_ X) (T_star_ Y) (lift_T_star_ X Y f) (lambda_star Lambda X tsbx) = lambda_star Lambda Y (lift_T_star_ (B_ X) (B_ Y) (lift_B_ X Y f) tsbx).
proof: Proof. intros Lambda X Y f [j tjbx]. unfold lambda_star at 1. fold B_. simpl. set (tmp:=lambda_iter_ Lambda j X tjbx). stepl (lift_B_ _ _ (T_star_coproject_ Y j) (lift_B_ _ _ (lift_T_iter _ _ f j) tmp)); [|do 2 rewrite lift_B_compose; apply lift_B_extensionality; trivial]. subst tmp. f_equal. fold T_iter. apply lambda_iter_naturality. Qed.
imports: LambdaCoiteration