..And prove some additional lemmas.
Following a discussion w/ @robbertkrebbers
Since it is not necessary for is_closed_expr to simplify well, it might be better to formulate it in terms of sets, not lists.
This is convenient when you have e.g. a description of a type system where contexts are maps, and you want to prove that all well-typed expressions are appropriately closed.