-fact frees_inv_bind_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
- ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀x. X = §x → 𝐈⦃f⦄.
+#f #L #X #H elim H -f -L -X //
+[ #f #i #_ #x #H destruct
+| #f #_ #L #V #_ #_ #x #H destruct
+| #f #_ #L #_ #x #H destruct
+| #f #_ #L #i #_ #_ #x #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #_ #_ #x #H destruct
+]
+qed-.
+
+lemma frees_inv_gref: ∀f,L,l. L ⊢ 𝐅*⦃§l⦄ ≘ f → 𝐈⦃f⦄.
+/2 width=5 by frees_inv_gref_aux/ qed-.
+
+fact frees_inv_bind_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≘ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≘ f2 & f1 ⋓ ⫱f2 ≘ f.