qed-.
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.
qed-.
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.