We need to make a name correspond to many different (but similar) theorems.

For example, unordered sets {a, b}, Obviously a∈{a, b} and b∈{a, b}

Similar **trivial theorems** should have the same name.

Otherwise the context will be full of garbage lemmas …

By definition in coq a theorem *is* a name (associated to a proof). Hence you cannot have two theorems with the same name. So yes the environment is filled with thousands of (necessarily distinct) names.

```
Require Import Ensembles.
Search In.
Full_intro: forall (U : Type) (x : U), In U (Full_set U) x
In_singleton: forall (U : Type) (x : U), In U (Singleton U x) x
Couple_r: forall (U : Type) (x y : U), In U (Couple U x y) y
Couple_l: forall (U : Type) (x y : U), In U (Couple U x y) x
Triple_m: forall (U : Type) (x y z : U), In U (Triple U x y z) y
Triple_l: forall (U : Type) (x y z : U), In U (Triple U x y z) x
Triple_r: forall (U : Type) (x y z : U), In U (Triple U x y z) z
...
```

Usually that is not a problem:

`Search`

is quite a powerful tool to narrow your search.- Modules help for structuring the name space.
- Trivial lemmas are put in hint database and you never need to name them again.

```
Require Import Ensembles.
Search In Couple. (* list lemmas about both In and Couple. *)
Hint Resolve Couple_l Couple_r: mySetDb.
Goal In _ (Couple _ 2 3) 2.
Proof.
auto with mySetDb.
Qed.
Goal In _ (Couple _ 2 3) 3.
Proof.
auto with mySetDb.
Qed.
```

(edited: removed useless calls to `unfold`

)