如何让Coq化简不可证伪的模式匹配？

我正在学习《逻辑基础》（Logic Foundations），在完成lower_grade_lowers练习时，遇到Coq行为不符合预期的情况。当前我的证明目标如下：

grade_comparison match l with
                 | A | _ => Grade l Natural
                 end (Grade l Plus) = Lt

我认为这个目标应该可以化简：| A | _ => ...的分支不存在证伪的可能，预期Coq会将其化简为：

grade_comparison (Grade l Natural) (Grade l Plus) = Lt

但实际并未实现，我不清楚其中原因。

内容的提问来源于stack exchange，提问作者Nicolas Rinaudo