-lemma lreq_inv_next: ∀I1,I2,L1,L2,V1,V2,f.
- L1.ⓑ{I1}V1 ≡[⫯f] (L2.ⓑ{I2}V2) →
- ∧∧ L1 ≡[f] L2 & V1 = V2 & I1 = I2.
-/2 width=1 by lexs_inv_next/ qed-.
+lemma lreq_inv_next: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≡[↑f] L2.ⓘ{I2} →
+ L1 ≡[f] L2 ∧ I1 = I2.
+#f #I1 #I2 #L1 #L2 #H elim (lexs_inv_next … H) -H
+/3 width=3 by ceq_ext_inv_eq, conj/
+qed-.