Re: [mizar] consider

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

Hi Josef,

[...]
>So in more than a half of the relevant cases, the linking
>would be "immediately" useful.

Thanks very much for investigating this!  Maybe this will
help me eventually get my wish that I can use "then" after
a consider...

Two questions:

- Do these counts include "assume that" and "let ... such
  that" and so on?

- If you only look at considers that have just one statement
  inside (so you can't be confused about what the "then"
  refers to), then how many are there then?  Is this easy
  to find out?

So the considers that do not get a reference to the statement
in the consider immediately after, they are generally
followed by a "take" or a "set" or something like that?

Freek