-lemma rdeq_cpxs_trans: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈*[h] T1 →
- ∀L2. L2 ≛[h, o, T0] L0 →
- ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈*[h] T & T ≛[h, o] T1.
-#h #o #G #L0 #T0 #T1 #H @(cpxs_ind_dx … H) -T0 /2 width=3 by ex2_intro/
+lemma rdeq_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/