/2 width=4 by lsuba_inv_atom2_aux/ qed-.
fact lsuba_inv_bind2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2. L2 = K2.ⓘ[I] →
(∃∃K1. G ⊢ K1 ⫃⁝ K2 & L1 = K1.ⓘ[I]) ∨
/2 width=4 by lsuba_inv_atom2_aux/ qed-.
fact lsuba_inv_bind2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2. L2 = K2.ⓘ[I] →
(∃∃K1. G ⊢ K1 ⫃⁝ K2 & L1 = K1.ⓘ[I]) ∨