fact: Fixpoint lift_F_iter (X Y:Set) (f:X->Y) j {struct j} : F_iter j X -> F_iter j Y := match j as n return (F_iter n X -> F_iter n Y) with | O => f | S j' => lift_F_iter (F_ X) (F_ Y) (lift_F_ _ _ f) j' end.