Inductive case: if head prefix doesn't collide with tail prefixes and tail is prefix-free, then head *: tail is prefix-free.
Inductive case: if head prefix doesn't collide with tail prefixes and tail is prefix-free, then head *: tail is prefix-free.
This implementation requires UniqueNames evidence, which ensures that table names are distinct. With length-prefix encoding, distinct names guarantee prefix-free prefixes.