Feature request: allow repetitions of definitions and theorems

[chaudhuri]

Currently we do not allow repetitions of Definitions and Theorems. This is causing various issues with the IPFS branch that are not worth getting into here.

Personally, I see no issue with allowing repetitions of definitions and theorems as long as they are identical.

(Issue arose in discussion with @innofarah.)

---

If we go this way, then one issue to consider is whether we use "identical" to mean "up to lambda-equivalence". For example, are the following two defintions identical?

Definition is_abs : tm -> prop by
  is_abs (abs R).

Definition is_abs : tm -> prop by
  is_abs (abs (x\ R x)).

[chaudhuri]

This feature could also obviate #133, perhaps.

[chaudhuri]

This is now implemented in the ipfs branch which may eventually be merged with master.