Make proof tactics always return correct proofs given correct components

Created by: cache-nez

Current limitation of the tactics is taking ProofSteps as arguments. The tactic has no way of knowing the preceding steps or the imports, required for the proof. Hence if the supplied arguments are not the very first steps of the proof and/or the proof needs imports, the result of the tactic application is not a valid proof since it misses these parts. This PR changes the tactics signature to take Subproofs as arguments, thus collecting all necessary details.

This PR depends on #30, because without it the tactic application might remove a wrong formula from the sequent, and should be merged after it.