How do I put proof obs onto operator args?

[Forwarded by horning@src.dec.com for kirk@zipcode.Jpl.Nasa.Gov]

Say I have something like
T tuple of a:A, b:B;
op(t) == t_set(...);

But I want all uses of op() to incur a proof obligation that
some predicates on T hold (e.g. b has certain properties, or

Am I going about this all wrong, or is there a way to state this,
or is there a better paradigm, or what?

Thanks to all who read this!