Feature request: permitting more than one proof per theorem

I often want to collect several different proofs of the same theorem. In fact, sometimes theorems are trivial and one is looking for a range of proofs for that theorem. Consider, for example, the theorem (p -> p) -> p -> p: this is trivial but it's different proofs look like Church numerals.

A possible way to accommodate the collection of several proofs in Abella might be to introduce a keyword such as reprove as a Proof state manipulation tactics. Its meaning would be:

Check that the last Top-level command was, in fact, Theorem. The reprove keyword should not be allowed immediately following a Definition, for example.
Check that the previous theorem has a completed proof.
Reinstate the previous theorem and start reading the following text as a new proof of that theorem.

An example of what I have in mind is the following.

Theorem church-numerals : (p -> p) -> p -> p.
% the numeral for one
  intros succ zero. one: apply succ to zero. clear zero. search.
reprove. % the numeral for two
  intros succ zero. one: apply succ to zero. clear zero. 
                    two: apply succ to one.  clear one. search.
reprove. % the numeral for three
  intros succ zero. one: apply succ to zero. clear zero. 
                    two: apply succ to one.  clear one.
                    three: apply succ to two.  clear two. search.

abella-prover / abella-prover.org

Feature request: permitting more than one proof per theorem #12