#T elim T -T *
/2 width=1 by lifts_sort, lifts_lref, lifts_gref, lifts_bind, lifts_flat/
qed.
(* Main inversion properties ************************************************)
#T elim T -T *
/2 width=1 by lifts_sort, lifts_lref, lifts_gref, lifts_bind, lifts_flat/
qed.
(* Main inversion properties ************************************************)