-fact lsubc_inv_bind2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2. L2 = K2.ⓘ{I} →
- (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓘ{I}) ∨
- â\88\83â\88\83K1,V,W,A. â¦\83G,K1,Vâ¦\84 ϵ[RP] ã\80\9aAã\80\9b & â¦\83G,K1,Wâ¦\84 ϵ[RP] ã\80\9aAã\80\9b & â¦\83G,K2â¦\84 ⊢ W ⁝ A &
+fact lsubc_inv_bind2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2. L2 = K2.ⓘ[I] →
+ (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓘ[I]) ∨
+ â\88\83â\88\83K1,V,W,A. â\9d¨G,K1,Vâ\9d© ϵ â\9f¦Aâ\9f§[RP] & â\9d¨G,K1,Wâ\9d© ϵ â\9f¦Aâ\9f§[RP] & â\9d¨G,K2â\9d© ⊢ W ⁝ A &