If tac applied to the goal (asl,g) produces a justification that
does not create a theorem A |- g, with A a subset of asl, then
VALID tac (asl,g) fails (raises an exception). If tac produces a
valid proof on the goal, then the behaviour of VALID tac (asl,g) is
the same as tac (asl,g)