[mizar] Assumption in redefinition?

[Freek Wiedijk <freek@cs.kun.nl>]

Hi, it's me again, with yet another question...

I have a definition that looks like

  define
   let k,d being Nat;
   assume k <= d;
   func foo(k,d) ...
   ...
  end;

Later on, I want to redefine this function, but for that I
need the assumption k <= d again.  So I try:

  define
   let k,d being Nat;
   assume
  A1: k <= d;
   redefine func foo(k,d) ...
   ...
  end;

Then Mizar tells me I may not use this assumption A1.  But
"foo" only is meaningful when k <= d!  So what can I do?
Isn't it possible to do a redefinition like this?

So I want to refer to the assumption from the original
definition.

Freek