+
+fact frees_inv_bind_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T,a. X = ⓑ{a,I}V.T →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+#L #X #f * -L -X -f
+[ #I #f #_ #J #W #U #b #H destruct
+| #I #L #V #s #f #_ #J #W #U #b #H destruct
+| #I #L #V #f #_ #J #W #U #b #H destruct
+| #I #L #V #i #f #_ #J #W #U #b #H destruct
+| #I #L #V #p #f #_ #J #W #U #b #H destruct
+| #I #L #V #T #a #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #J #W #U #b #H destruct
+]
+qed-.
+
+lemma frees_inv_bind: ∀I,L,V,T,a,f. L ⊢ 𝐅*⦃ⓑ{a,I}V.T⦄ ≡ f →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+/2 width=4 by frees_inv_bind_aux/ qed-.
+
+fact frees_inv_flat_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
+#L #X #f * -L -X -f
+[ #I #f #_ #J #W #U #H destruct
+| #I #L #V #s #f #_ #J #W #U #H destruct
+| #I #L #V #f #_ #J #W #U #H destruct
+| #I #L #V #i #f #_ #J #W #U #H destruct
+| #I #L #V #p #f #_ #J #W #U #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct
+| #I #L #V #T #f1 #f2 #f #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma frees_inv_flat: ∀I,L,V,T,f. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
+/2 width=4 by frees_inv_flat_aux/ qed-.
+
+(* Basic properties ********************************************************)
+
+lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
+#L #T #f1 #H elim H -L -T -f1
+[ /3 width=3 by frees_atom, isid_eq_repl_back/
+| #I #L #V #s #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_sort/
+| #I #L #V #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/
+| #I #L #V #i #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/
+| #I #L #V #p #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/
+| /3 width=7 by frees_bind, sor_eq_repl_back3/
+| /3 width=7 by frees_flat, sor_eq_repl_back3/
+]
+qed-.
+
+lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
+#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
+qed-.
+
+lemma frees_sort_gen: ∀L,s,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃⋆s⦄ ≡ f.
+#L elim L -L
+/4 width=3 by frees_eq_repl_back, frees_sort, frees_atom, eq_push_inv_isid/
+qed.
+
+lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
+#L elim L -L
+/4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
+qed.