Add :addmissing REPL command

:am [line] [name] gives the missing clauses for the [name] defined on line
[line]. Correspondingly, :am! updates the source file.
Leave metavariables for unfinished proofs

If the maximum search depth is reached, the proof so far may still
be useful.
Add Bifunctor typeclass. Provide instance for Either.
Add WriterT.
Add ReaderT.