-lemma cpm_tdeq_inv_bind_sn_void (a) (h) (o) (n) (p) (I) (G) (L):
- ∀V,T1. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] →
- ∀X. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛[h,o] X →
- ∃∃T2. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G, L.ⓧ⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T2.
-#a #h #o #n #p #I #G #L #V #T1 #H0 #X #H1 #H2
+lemma cpm_tdeq_inv_bind_sn_void (a) (h) (n) (p) (I) (G) (L):
+ ∀V,T1. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] →
+ ∀X. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛ X →
+ ∃∃T2. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G,L.ⓧ⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓑ{p,I}V.T2.
+#a #h #n #p #I #G #L #V #T1 #H0 #X #H1 #H2