Creat a minimal tactic system for the kernel

[SimonGuilloud]

We should be able to define "deduced steps" helpers for the kernel in a unified way. This should first include versions of basis proofsteps with most arguments automatically infered, and then steps such as InstantiateForall and others, who should be encapsulated in subproofs.