-lemma lfxs_fwd_bind_sn: ∀R,I,L1,L2,V,T,p. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2.
-#R #I #L1 #L2 #V #T #p * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf
+lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2.
+#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf