(* Properties with generic slicing for local environments *******************)
lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G).
(* Properties with generic slicing for local environments *******************)
lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G).