Implicit Binder Predicate

Stream: lean4

[Kenny Lau]

Currently, in Mathlib, the predicate of "subset" is defined as:

∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂

Note that we currently have "binder predicates", i.e.:

∀ a ∈ s₁, a ∈ s₂

But these two versions differ in the explicitness of a. I wonder if we should support either of the following syntaxes:

• ∀ ⦃a⦄ ∈ s₁, a ∈ s₂
• ∀ ⦃a ∈ s₁⦄, a ∈ s₂

[Yaël Dillies]

This is a very common use case and it has been suggested before that ∀ a ∈ s, p a could actually just mean ∀ ⦃a⦄, a ∈ s → p a. Indeed, the other (=current) interpretation ∀ a, a ∈ s → p a seems to be heuristically never useful