Add formula parameters, new proof

[tirix]

Adds the possibility to pass formulas as parameter to tactics. A forth theorem ~ajfval can now be proven using the updated tactics.