How do I put proof obs onto operator args?

   From: kirk@zipcode.Jpl.Nasa.Gov (Kirk Reinholtz)
   Date: Tue, 08 Mar 94 11:55:50 -0800
   Sender: horning@src.dec.com
   X-Mts: smtp

   [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?

	I was hoping someone else would answer this, but I don't think
I understand the question.  This is at the LSL level (it looks like to me),

Why doesn't it suffice to do something like...

Foo: trait
  T tuple of a:A, b:B
  assumes theProofObligationTrait
    op: T -> T
  asserts for all t:T
   op(t) == t_set(...)

... where the trait "theProofObligationTrait" would have to hold in each
case where this trait (Foo) is used?

Is there something more interesting going on?  (probably)