Georges Gonthier

Add [in A] notation.

8

Add `[in A]` notation for `fun x => x \in A`, the natural applicative equivalent of a collective predicate `A`. Replace `(mem A)` and `[mem A]`, which had a similar...

Revise use of numerical occurrence selectors

11

Numerical occurrence selectors such as `{1 3}`, `{-2}` or `{7}`, which convenient during proof development, can be fragile. Context patterns (possibly in combination with the `set` and `rewrite /` tactics)...

See review of #277 : with `E` of the form `forall R (P : seq T -> R), ... -> forall s, P s -> P t`, both `elim/E: (t)`...

### Description of the problem While `rewrite` tactic of Ssreflect can rewrite under binders, as long as no bound variable occurs in the redex, and it can use generalized rewriting...