/3 width=3 by cpms_trans, cpms_cast_sn/
]
qed.
+
+theorem cpms_trans_swap (h) (G) (L) (T1):
+ ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡*[n1,h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡*[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T2.
+#h #G #L #T1 #n1 #T #HT1 #n2 #T2 #HT2
+lapply (cpms_trans … HT1 … HT2) -T <commutative_plus #HT12
+/2 width=1 by cpms_inv_plus/
+qed-.