proposition: Lemma lift_F_iter_extensionality: forall (X Y:Set) (f0 f1:X->Y) j s_ix, (forall x, f0 x = f1 x) -> lift_F_iter _ _ f0 j s_ix = lift_F_iter _ _ f1 j s_ix.
proof: Proof. intros X Y f0 f1 j; revert X Y f0 f1; induction j; intros X Y f0 f1 s_ix hyp_ext. simpl; apply hyp_ext. simpl. rewrite (IHj (F_ X) (F_ Y) (lift_F_ X Y f0) (lift_F_ X Y f1) s_ix). trivial. intros sx. apply (lift_F_extensionality X Y f0 f1 sx hyp_ext). Qed.