/3 width=6 by lex_liftable_dedropable_sn, cpxs_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: was: lpxs_drop_conf *)
/3 width=6 by lex_liftable_dedropable_sn, cpxs_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: was: lpxs_drop_conf *)