+fact frees_inv_atom_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀J. L = ⋆ → X = ⓪{J} → 𝐈⦃f⦄.
+#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
+[5,6: #I #L #V #T [ #p ] #f1 #f2 #f #_ #_ #_ #_ #_ #J #_ #H destruct
+|*: #I #L #V [1,3,4: #x ] #f #_ #_ #J #H destruct
+]
+qed-.
+
+lemma frees_inv_atom: ∀I,f. ⋆ ⊢ 𝐅*⦃⓪{I}⦄ ≡ f → 𝐈⦃f⦄.
+/2 width=6 by frees_inv_atom_aux/ qed-.
+