chore(frontends/lean/placeholder_elaborator): indent code
fix(library/unifier): missing justification when updating choice constraints

The bug was not producing incorrect results, but really bad error
messages.
See: empty.lean.expected.out