-lemma frees_inv_zero: ∀L,f. L ⊢ 𝐅*⦃#0⦄ ≡ f →
- (L = ⋆ ∧ 𝐈⦃f⦄) ∨
- ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
-/2 width=3 by frees_inv_zero_aux/ qed-.
-
-fact frees_inv_lref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j) →
- (L = ⋆ ∧ 𝐈⦃f⦄) ∨
- ∃∃I,K,V,g. K ⊢ 𝐅*⦃#j⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
-#L #X #f * -L -X -f
-[ /3 width=1 by or_introl, conj/
-| #I #L #V #s #f #_ #j #H destruct
-| #I #L #V #f #_ #j #H destruct
-| #I #L #V #i #f #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #I #L #V #l #f #_ #j #H destruct
-| #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #j #H destruct
-| #I #L #V #T #f1 #f2 #f #_ #_ #_ #j #H destruct
+lemma frees_inv_lref: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
+ ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g.
+/2 width=6 by frees_inv_lref_aux/ qed-.
+
+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