#f #K #T #H elim H -f -K -T
[ /2 width=1 by frees_sort/
| #f * /3 width=1 by frees_atom, frees_unit, frees_lref/
#f #K #T #H elim H -f -K -T
[ /2 width=1 by frees_sort/
| #f * /3 width=1 by frees_atom, frees_unit, frees_lref/
-fact frees_inv_append_void_aux: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≘ f →
- ∀K. L = ⓧ.K → K ⊢ 𝐅*⦃T⦄ ≘ f.
+fact frees_inv_append_void_aux:
+ ∀f,L,T. L ⊢ 𝐅+⦃T⦄ ≘ f →
+ ∀K. L = ⓧ.K → K ⊢ 𝐅+⦃T⦄ ≘ f.