-| cpysa_atom : ∀I,G,L,d,e. cpysa d e G L (⓪{I}) (⓪{I})
-| cpysa_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d+e →
- ⬇[i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 →
- ⬆[0, i+1] V2 ≡ W2 → cpysa d e G L (#i) W2
-| cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
- cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V1) T1 T2 →
- cpysa d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
-| cpysa_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
- cpysa d e G L V1 V2 → cpysa d e G L T1 T2 →
- cpysa d e G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+| cpysa_atom : ∀I,G,L,l,m. cpysa l m G L (⓪{I}) (⓪{I})
+| cpysa_subst: ∀I,G,L,K,V1,V2,W2,i,l,m. l ≤ yinj i → i < l+m →
+ ⬇[i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(l+m-i)) G K V1 V2 →
+ ⬆[0, i+1] V2 ≡ W2 → cpysa l m G L (#i) W2
+| cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,l,m.
+ cpysa l m G L V1 V2 → cpysa (⫯l) m G (L.ⓑ{I}V1) T1 T2 →
+ cpysa l m G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| cpysa_flat : ∀I,G,L,V1,V2,T1,T2,l,m.
+ cpysa l m G L V1 V2 → cpysa l m G L T1 T2 →
+ cpysa l m G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)