proposition: Theorem lambda_iter_naturality: forall (Lambda : T_over_B_distributive) (j:nat) (X Y : Set) (f : X -> Y) (tjbx : T_iter j (B_ X)), lift_B_ _ _ (lift_T_iter X Y f j) (lambda_iter_ Lambda j X tjbx) = lambda_iter_ Lambda j Y (lift_T_iter (B_ X) (B_ Y) (lift_B_ X Y f) j tjbx).
proof: Proof. intros [lam_ nat_lam_] j; induction j; intros X Y f tjbx; trivial. fold T_iter in IHj. change ( lift_B_ _ _ (lift_T_iter _ _ (lift_F_ X Y f) j) (lambda_iter_ (Build_T_over_B_distributive lam_ nat_lam_) j (T_ X) (lift_T_iter _ _ (lam_ X) j tjbx)) = lambda_iter_ (Build_T_over_B_distributive lam_ nat_lam_) j (T_ Y) (lift_T_iter _ _ (lam_ Y) j (lift_T_iter _ _ (lift_B_ X Y f) (S j) tjbx) )); trivial. rewrite (IHj (T_ X) (T_ Y) (lift_T_ _ _ f)). f_equal. simpl. do 2 rewrite lift_T_iter_compose. fold lift_T_iter T_ B_. apply lift_T_iter_extensionality. symmetry; apply nat_lam_. Qed.
imports: LambdaCoiteration