Right.  We don't expect the proof to be used, nor to have a speed effect, so we should use the default, which is `Defined`.  (The idea being that anything that's not an hProp is potentially relevant (and even hProps are sometimes judgmentally relevant), so the default is `Defined`, even for things that used to be in `Prop`.)