Imagine two safe APIs, one to build terms (validating type-of) and one building theorems (validating is-true).
I'd like to assume that a number n is positive and build a proof of it being not zero. I could write it like this
pi n\ type-of n nat => (mk-app positive n H, is-true H => ( ... use H to show not-zero n ...))
The link between pi n and type-of n nat is striking, and one can imagine a single operation pi-type-of nat n. But I don't see how this would extend to the implication that assumes is-true (app positive n).