proposition: Lemma lift_F_id :forall X (fx: F_ X), fx = lift_F_ X X (fun x0 : X => x0) fx.
proof: Proof. intros X fx; trivial. unfold lift_F_. transitivity (FA.lift_F_ (FB_ X) (FB_ X) (fun x0 : FB_ X => x0) fx); [apply FA.lift_F_id|]. apply FA.lift_F_extensionality. apply FB.lift_F_id. Qed.