[mizar] Possible language extension?

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

Hello!

For some time I've been thinking about the following.
Consider the following theorem:

  theorem Example: P & Q & R implies S & T
  proof
   assume
A1: P;
   assume
A2: Q;
   assume
A3: R;
   ...
  end;

It seems strange to have to write P, Q and R _again_ when you
just wrote those assumptions in the statement of the theorem.

Now wouldn't it be nice to be able to say:

  theorem
   assume
A1: P;
   assume
A2: Q;
   assume
A3: R;
Example: S & T
  proof
   ...
  end;

It would match the assumptions in definitions.  Also I think
I've seen this idiom with "assume" in the statement of a
theorem in actual mathematical texts.

Would it be hard to implement this?  I guess the machinery
for diffuse reasoning should help here?

Or is this a silly idea?

Freek