-lemma lfxs_inv_bind: ∀R,I,L1,L2,V1,V2,T,p. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 →
+lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2
+[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
+| lapply (frees_inv_gref … H1) -H1 #Hf
+ elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
+ elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct
+ /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 →