Let locations have distinct inner monads #39
Description
See the HasChor issue.
I think this will be harder for us than for them; the structure of the inner monads would have to be such that we could manipultate proof objects saying "p is in ps and has ms as part of its inner moanadic api".