Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
| ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
/2 width=1 by rex_inv_zero_length/ qed-.
Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
| ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
/2 width=1 by rex_inv_zero_length/ qed-.