| lreq_zero: ∀I1,I2,L1,L2,V1,V2.
lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 →
| lreq_zero: ∀I1,I2,L1,L2,V1,V2.
lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 →