-lemma reqx_cpxs_trans: ∀h,G,L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈*[h] T1 →
- ∀L2. L2 ≛[T0] L0 →
- ∃∃T. ❪G,L2❫ ⊢ T0 ⬈*[h] T & T ≛ T1.
-#h #G #L0 #T0 #T1 #H @(cpxs_ind_dx … H) -T0 /2 width=3 by ex2_intro/
+lemma reqx_cpxs_trans (G):
+ ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈* T1 → ∀L2. L2 ≛[T0] L0 →
+ ∃∃T. ❪G,L2❫ ⊢ T0 ⬈* T & T ≛ T1.
+#G #L0 #T0 #T1 #H @(cpxs_ind_dx … H) -T0 /2 width=3 by ex2_intro/