-lemma lreq_inv_next1: ∀g,J,K1,Y. K1.ⓘ{J} ≡[⫯g] Y →
- ∃∃K2. K1 ≡[g] K2 & Y = K2.ⓘ{J}.
-#g #J #K1 #Y #H elim (lexs_inv_next1 … H) -H /2 width=3 by ex2_intro/
+lemma lreq_inv_next1: ∀g,J,K1,Y. K1.ⓘ{J} ≐[⫯g] Y →
+ ∃∃K2. K1 ≐[g] K2 & Y = K2.ⓘ{J}.
+#g #J #K1 #Y #H
+elim (lexs_inv_next1 … H) -H #Z #K2 #HK12 #H1 #H2 destruct
+<(ceq_ext_inv_eq … H1) -Z /2 width=3 by ex2_intro/