-lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ¡⫃[h, g] K2.ⓑ{I}W →
- (∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
- ∃∃K1,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
- scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
- ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ¡⫃[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, g] K2.ⓑ{I}W →
+ (∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
+ ∃∃K1,V,l1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g, l1] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+ ⦃G, K1⦄ ⊢ V ▪[h, g] l1+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l1 &
+ G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1.ⓓⓝW.V.