[Bug] Kernel error when blaster tactic is used and some other subgoals are conculded with sorry/proofs

Error `(kernel)` application type mismatch ...` is raised when `blaster` tactic is used to prove some of the sub-goals of a theorem, while some remaining sub-goals are concluded with either `sorry` or a manual proof is provided.

E.g. Here blaster tactic is only used to optimize the goal to be proved.

```
theorem sto8 :
∀ (x : ProcessSCInput) (s : ComputeReserve),
isSellSCOrder x →
validOrderInput x →
resultToComputeReserve (fromHaltState $ compiledProcessSCOrder x) = some s →
validSellSC x s := by
intro x s;
blaster (only-optimize: 1)
by_cases x.state.crN_SC = 0 <;>
by_cases x.state.crN_RC = 0
. sorry
. sorry
. sorry
. sorry
```