-lemma cpcs_ind_dx: ∀L,T2. ∀R:predicate term. R T2 →
- (∀T1,T. L ⊢ T1 ⬌ T → L ⊢ T ⬌* T2 → R T → R T1) →
- ∀T1. L ⊢ T1 ⬌* T2 → R T1.
-#L #T2 #R #HT2 #IHT2 #T1 #HT12
-@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+lemma cpcs_ind_dx: ∀G,L,T2. ∀R:predicate term. R T2 →
+ (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → R T → R T1) →
+ ∀T1. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T1.
+normalize /3 width=6 by TC_star_ind_dx/