[lemma] Remove special case for first constant in mutual definition save path.

This could still use some more work due to the way proofs are
structured, in particular:

- the handling of the primary type w.r.t. Econstr
- refining Info.t so open/close invariants hold by typing

Very interestingly, better typing means that the tension between
tension between `start_dependent_lemma` and the handling of mutual
definitions starts to surface.

In particular, the information contained in `Info.thms` is not to be
used by all non-standard terminators.

However, it seems that such refactoring would better fit once we have
finished cleaning up the regular save path.

0 files changed, 0 insertions, 0 deletions