Added a few new dependencies, some coq tactics and functions for moving lines up
and down.