(* Properties with generic slicing for local environments *******************)
lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G).
(* Properties with generic slicing for local environments *******************)
lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G).