lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G).
/3 width=6 by lfxs_liftable_dedropable_sn, cpx_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G).
/3 width=6 by lfxs_liftable_dedropable_sn, cpx_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)