proposition: Theorem FunctExt_iff_UniqInverse : FunctionalExtensionality <-> UniqueInverse.
proof: Proof. split. - apply FunctExt_UniqInverse. - intro; apply FunctExt_iff_EqDeltaProjs, UniqInverse_EqDeltaProjs; trivial. Qed.