Comment by c-cube

I agree that the treatment of alpha equivalence might not be the best. Isabelle/HOL has pattern unification which makes it easier.

For the type variables: it's a matter of taste! I prefer it this way, and it's quite useful if you expect terms and theorems to have free variables (quite common in automatic provers). Having free variables is a good way to specify things like rewrite rules, backward chaining clauses, etc. so it doesn't come out of the blue.