+lemma cpms_inv_abst_sn_cprs (h) (n) (p) (G) (L) (W):
+ ∀T,X. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡*[n,h] X →
+ ∃∃U. ⦃G,L.ⓛW⦄⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓛ{p}W.U ➡*[h] X.
+#h #n #p #G #L #W #T #X #H
+elim (cpms_inv_abst_sn … H) -H #W0 #U #HW0 #HTU #H destruct
+@(ex2_intro … HTU) /2 width=1 by cpms_bind/
+qed-.
+