-lemma lprs_cprs_conf_sn (h) (G): ∀L0. ∀T0,T1:term. ❪G,L0❫ ⊢ T0 ➡*[h] T1 →
- ∀L1. ❪G,L0❫ ⊢ ➡*[h] L1 →
- ∃∃T. ❪G,L0❫ ⊢ T1 ➡*[h] T & ❪G,L1❫ ⊢ T0 ➡*[h] T.
+lemma lprs_cprs_conf_sn (h) (G): ∀L0. ∀T0,T1:term. ❪G,L0❫ ⊢ T0 ➡*[h,0] T1 →
+ ∀L1. ❪G,L0❫ ⊢ ➡*[h,0] L1 →
+ ∃∃T. ❪G,L0❫ ⊢ T1 ➡*[h,0] T & ❪G,L1❫ ⊢ T0 ➡*[h,0] T.