proposition: Lemma lift_F_iter_compose (X Y Z:Set) (g:X->Y) (f:Y->Z) j s_ix: lift_F_iter Y Z f j (lift_F_iter X Y g j s_ix) = lift_F_iter X Z (fun x => f (g x)) j s_ix.
proof: Proof. revert X Y Z g f s_ix. induction j; intros X Y Z g f s_ix. simpl; trivial. simpl. rewrite IHj. apply lift_F_iter_extensionality. apply (lift_F_compose X Y Z g f). Qed.