refactor(*): move code about `ulift`/`plift` (#8863)
* move old file about `ulift`/`plift` from `data.ulift` to `control.ulift`;
* redefine `ulift.map` etc without pattern matching;
* create new `data.ulift`, move `ulift.subsingleton` etc from `data.equiv.basic` to this file;
* add `ulift.is_empty` and `plift.is_empty`;
* add `ulift.exists`, `plift.exists`, `ulift.forall`, and `plift.forall`;
* rename `equiv.nonempty_iff_nonempty` to `equiv.nonempty_congr` to match `equiv.subsingleton_congr` etc;
* rename `plift.fintype` to `plift.fintype_Prop`, add a new `plift.fintype`.
