Commit 2021-08-26 11:17 0861cc75

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.