I think, loosely, an existential quantifier is "trivial" if you can immediately discharge it. I don't know that there's a very formal approach to this, but ther

I think, loosely, an existential quantifier is "trivial" if you can immediately discharge it. I don't know that there's a very formal approach to this, but there's definitely a way to dream up completely trivial existential quantifiers. The only obvious one that comes to mind is an existential quantifying over a singular domain. If Unit is the type containing the single value (), then `exists (x: Unit) . P x` is trivially P (). Even a tiny extension of this (e.g. exists (x: Boolean) . P x) is enough to make this no longer trivial as it at least indicates a search process and can be used to encode arbitrary expansion as long as you can nest existentials. So that's the other way I could imagine it being trivial: if existentials aren't allowed to index very powerful statements, if the Ps above cannot themselves include quantified statements.