theorem Validator.Certificate.valid.soundness {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.valid) (h : C.IsUnsolvable) : pt.Unsolvable