(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: uses: drop_lpxs_trans *)
lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G).
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: uses: drop_lpxs_trans *)
lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G).
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: uses: lpxs_drop_conf *)
lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G).
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: uses: lpxs_drop_conf *)
lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G).
(* Basic_2A1: uses: lpxs_drop_trans_O1 *)
lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G).
(* Basic_2A1: uses: lpxs_drop_trans_O1 *)
lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G).