Fix some problems with Lemma 7.5.12

The converse direction of Lemma 7.5.12 is false unless Q is fiberwise merely inhabited.  Also, there was a typo in the proof.  (I discovered both of these things while Coqing it.)