| tps_atom : ∀L,I,d,e. tps d e L (⓪{I}) (⓪{I})
| tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
⇩[0, i] L ≡ K. ⓓV → ⇧[0, i + 1] V ≡ W → tps d e L (#i) W
| tps_atom : ∀L,I,d,e. tps d e L (⓪{I}) (⓪{I})
| tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
⇩[0, i] L ≡ K. ⓓV → ⇧[0, i + 1] V ≡ W → tps d e L (#i) W