Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms.

Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.