-lemma cpm_theta: ∀n,h,p,G,L,V1,V,V2,W1,W2,T1,T2.
- ❪G,L❫ ⊢ V1 ➡[h] V → ⇧[1] V ≘ V2 → ❪G,L❫ ⊢ W1 ➡[h] W2 →
- ❪G,L.ⓓW1❫ ⊢ T1 ➡[n,h] T2 →
- ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ➡[n,h] ⓓ[p]W2.ⓐV2.T2.
-#n #h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV1 #HV2 * #riW #rhW #HW12 *
+lemma cpm_theta: ∀h,n,p,G,L,V1,V,V2,W1,W2,T1,T2.
+ ❪G,L❫ ⊢ V1 ➡[h,0] V → ⇧[1] V ≘ V2 → ❪G,L❫ ⊢ W1 ➡[h,0] W2 →
+ ❪G,L.ⓓW1❫ ⊢ T1 ➡[h,n] T2 →
+ ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ➡[h,n] ⓓ[p]W2.ⓐV2.T2.
+#h #n #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV1 #HV2 * #riW #rhW #HW12 *