-theorem cnv_cpmuwe_mono (a) (h) (G) (L):
- ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] → ∀T1,n1. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n1] T1 →
- ∀T2,n2. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n2] T2 →
+theorem cnv_cpmuwe_mono (h) (a) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![h,a] →
+ ∀n1,T1. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n1] T1 →
+ ∀n2,T2. ⦃G,L⦄ ⊢ T0 ➡*𝐍𝐖*[h,n2] T2 →