Use new API (Trace and Lift are images).
Renaming: V -> A (set on which the trace is taken).

Renaming: Lift' -> Lift_full.
Rm Trace' (clearly equivalent to the new Trace).

Rename BA var of type subset A.

V -> A.

WIP: add Lift_Trace_equiv and Trace_Lift.

Now, we have (Subset V : set_system U -> set_system U),
(Lift V : set (subset V) -> set_system U), and
(Trace V : set_system U -> set (subset V)).

Add lift_rev and trace_equiv.

Add new form for trace_full{set,}_r.

Some renaming.
Proof of is_Basisp_Union_any_closure completed.