proposition: Lemma lift_F_extensionality: forall (X Y:Set) (f0 f1:X->Y) fx, (forall x, f0 x = f1 x) -> lift_F_ _ _ f0 fx = lift_F_ _ _ f1 fx.
proof: Proof. intros X Y g f fx hyp; unfold lift_F_; apply F_theory.lift_F_iter_extensionality; assumption. Qed.