Howe's proof in Abella

• The submitted paper
• The code:
  • The forallp version. First download forallp-Abella:
    git clone git://github.com/chaudhuri/abella.git
    cd abella
    git checkout forallp
    omake
  • The standard version (Abella 1.3.5)