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