some progress, but I still don't think I have the locally nameless thing right
trying forall L instead of exists L; not sure if better