-lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-/3 width=3/ qed.
-
-lemma cpcs_tpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T →
- ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ⬌* T2.
-#L #T1 #T #HT1 #T2 #d #e #HT2
-@(cpcs_cpr_strap1 … HT1) -T1 /2 width=3/
-qed-.
-
-lemma cpcs_tpss_conf: ∀L,T,T1,d,e. L ⊢ T ▶* [d, e] T1 →
- ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-#L #T #T1 #d #e #HT1 #T2 #HT2
-@(cpcs_cpr_conf … HT2) -T2 /2 width=3/
-qed-.
+lemma cpcs_cpr_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+/3 width=3 by cpcs_strap2, or_intror/ qed-.