-[ /3 width=1 by or_introl, conj/
-| #f #I #L #V #s #_ #j #H destruct
-| #f #I #L #V #_ #j #H destruct
-| #f #I #L #V #i #Hf #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #f #I #L #V #l #_ #j #H destruct
-| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #j #H destruct
-| #f1 #f2 #f #I #L #V #T #_ #_ #_ #j #H destruct
+[ #f #L #s #_ #Z #Y #_ #H destruct
+| #f #i #_ #Z #Y #H destruct
+| #f #I #L #V #_ #Z #Y #H destruct
+| #f #I #L #Hf #Z #Y #H destruct /2 width=3 by ex2_intro/
+| #f #I #L #i #_ #Z #Y #_ #H destruct
+| #f #L #l #_ #Z #Y #_ #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #_ #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #_ #H destruct
+]
+qed-.
+
+lemma frees_inv_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
+/2 width=7 by frees_inv_unit_aux/ qed-.
+
+fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K,j. L = K.ⓘ{I} → X = #(⫯j) →
+ ∃∃g. K ⊢ 𝐅*⦃#j⦄ ≡ g & f = ↑g.
+#f #L #X * -f -L -X
+[ #f #L #s #_ #Z #Y #j #_ #H destruct
+| #f #i #_ #Z #Y #j #H destruct
+| #f #I #L #V #_ #Z #Y #j #_ #H destruct
+| #f #I #L #_ #Z #Y #j #_ #H destruct
+| #f #I #L #i #Hf #Z #Y #j #H1 #H2 destruct /2 width=3 by ex2_intro/
+| #f #L #l #_ #Z #Y #j #_ #H destruct
+| #f1 #f2 #f #p #I #L #V #T #_ #_ #_ #Z #Y #j #_ #H destruct
+| #f1 #f2 #f #I #L #V #T #_ #_ #_ #Z #Y #j #_ #H destruct
+]
+qed-.
+
+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