lemma finite_injections
minor formatting
lemma wd_outcome: allocation is well-defined