Tactical.VALID

When list-tactic ltac is applied to a goal list gl it produces a new goal list gl' and a justification. When the justification is applied to a list thl' of theorems which are the new goals gl', proved, it should produce a list thl of theorems which are the goals gl, proved.

Precisely, for each goal (asl, g) in gl, the corresponding theorem in thl should be A |- g, with A a subset of asl. If this is not the case, then the list-tactic is invalid, and VALID_LT ltac gl fails (raises an exception). Otherwise, VALID_LT ltac gl behaves the same as ltac gl.