(* Basic_2A1: uses: drop_lpxs_trans *)
lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G).
-/3 width=5 by drops_lfpx_trans, dedropable_sn_LTC/ qed-.
+/3 width=5 by drops_lfpx_trans, dedropable_sn_CTC/ qed-.
(* 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).
-/3 width=5 by lfpx_drops_conf, dropable_sn_LTC/ qed-.
+/3 width=5 by lfpx_drops_conf, dropable_sn_CTC/ qed-.
(* Basic_2A1: uses: lpxs_drop_trans_O1 *)
lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G).
-/3 width=5 by lfpx_drops_trans, dropable_dx_LTC/ qed-.
+/3 width=5 by lfpx_drops_trans, dropable_dx_CTC/ qed-.