proposition: Lemma lift_F_iter_id (X:Set) j (fx:F_iter j X): fx = lift_F_iter X X (fun x0 : X => x0) j fx.
proof: Proof. revert X fx. induction j; intros X fx. simpl; trivial. simpl in *. transitivity (lift_F_iter (F_ X) (F_ X) (fun x0 : F_ X => x0) j fx). apply IHj. apply lift_F_iter_extensionality. apply lift_F_id. Qed.