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