-lemma lprs_pair (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡*[h] L2 →
- ∀V1,V2. ❪G,L1❫ ⊢ V1 ➡*[h] V2 →
- ∀I. ❪G,L1.ⓑ[I]V1❫ ⊢ ➡*[h] L2.ⓑ[I]V2.
+lemma lprs_pair (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡*[h,0] L2 →
+ ∀V1,V2. ❪G,L1❫ ⊢ V1 ➡*[h,0] V2 →
+ ∀I. ❪G,L1.ⓑ[I]V1❫ ⊢ ➡*[h,0] L2.ⓑ[I]V2.