Move some per-lemma variables to section contexts

I'm not sure which is the preferred style, but Bas told me that there
was some kind of problem in ObjectClassifier with not assuming
Univalence or Funext as an axiom.  I tried to track it down, but
everything seems to work fine.