/3 width=5 by lfxs_liftable_dedropable_sn, tdeq_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
/3 width=5 by lfxs_liftable_dedropable_sn, tdeq_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)