[lemmas] Reify proof information for recursive theorems.

Information about interactive mutually recursive proofs was stored as
a closure on an ad-hoc hook, then later made available to the hook
closing actions.

Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.

TODO: Should investigate what's going on with implicits, maybe submit
a separate PR.

0 files changed, 0 insertions, 0 deletions