L1.ⓑ{I1}V1 ≡[⫯f] (L2.ⓑ{I2}V2) →
∧∧ L1 ≡[f] L2 & V1 = V2 & I1 = I2.
/2 width=1 by lexs_inv_next/ qed-.
(* Basic_2A1: includes: lreq_inv_succ *)
L1.ⓑ{I1}V1 ≡[⫯f] (L2.ⓑ{I2}V2) →
∧∧ L1 ≡[f] L2 & V1 = V2 & I1 = I2.
/2 width=1 by lexs_inv_next/ qed-.
(* Basic_2A1: includes: lreq_inv_succ *)