lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2.
#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H
elim (cpcs_inv_cprs … H) -H #T #H1 #H2
elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct
lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2.
#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H
elim (cpcs_inv_cprs … H) -H #T #H1 #H2
elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct