Use lemma function like « by » operator
In addition to #547, it would be very useful to call a lemma function for writing a formula (aka, its ensures) along with its proof (aka, its requires).
Hence, the semantics of f a…
where f
is a lemma function would be similar to (E a…) by (R a…)
, where E
and R
are the ensures & requires of f
, although there is no need for side condition (R a… -> E a…)
since the lemma has been already established.
The manual description would be (Cf. § 7.3.4):
« An occurrence of f a...
where f
is a lemma function generates no side condition, since the lemma has already been established. When f a...
occurs as a premise, it is reduced to the conjunction of E a...
for all ensures E
of f
(the conclusion of the lemma are exhibited). When f a...
occurs as a goal, it is reduced to the conjunction of R a...
(the premisses of the lemma are verified). »