-lemma cpms_theta_dx (n) (h) (G) (L):
- ∀V1,V. ⦃G,L⦄ ⊢ V1 ➡[h] V →
- ∀V2. ⬆*[1] V ≘ V2 →
- ∀W1,W2. ⦃G,L⦄ ⊢ W1 ➡[h] W2 →
- ∀T1,T2. ⦃G,L.ⓓW1⦄ ⊢ T1 ➡*[n,h] T2 →
- ∀p. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n,h] ⓓ{p}W2.ⓐV2.T2.
-#n #h #G #L #V1 #V #HV1 #V2 #HV2 #W1 #W2 #HW12 #T1 #T2 #H @(cpms_ind_dx … H) -T2
+lemma cpms_theta_dx (h) (n) (G) (L):
+ ∀V1,V. ❪G,L❫ ⊢ V1 ➡[h,0] V →
+ ∀V2. ⇧[1] V ≘ V2 →
+ ∀W1,W2. ❪G,L❫ ⊢ W1 ➡[h,0] W2 →
+ ∀T1,T2. ❪G,L.ⓓW1❫ ⊢ T1 ➡*[h,n] T2 →
+ ∀p. ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ➡*[h,n] ⓓ[p]W2.ⓐV2.T2.
+#h #n #G #L #V1 #V #HV1 #V2 #HV2 #W1 #W2 #HW12 #T1 #T2 #H @(cpms_ind_dx … H) -T2