-lemma cpms_inv_abst_bi (n) (h) (G) (L):
- ∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 →
- ∧∧ ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2.
-#n #h #G #L #p #W1 #W2 #T1 #T2 #H
+lemma cpms_inv_abst_bi (n) (h) (p1) (p2) (G) (L):
+ ∀W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p1}W1.T1 ➡*[n, h] ⓛ{p2}W2.T2 →
+ ∧∧ p1 = p2 & ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2.
+#n #h #p1 #p2 #G #L #W1 #W2 #T1 #T2 #H