Add :makelemma command in interactive editing

Given a metavariable and a line number, add a new top level function to
solve that metavariable, and fill in the metavariable with an
application of that function.

e.g. given

  plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
  plus_commutes Z m = ?pcrhs_Z
  plus_commutes (S k) m = rewrite plus_commutes k m in ?pcrhs_S

:makelemma on pcrhs_S will update the file to

  pcrhs_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)

  plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
  plus_commutes Z m = ?pcrhs_Z
  plus_commutes (S k) m = rewrite plus_commutes k m in (pcrhs_S k m)

where pcrhs_S can be built interactively in the normal way.