快速简化表达式'ite ("a"="b") x‘

Question

当留给表单ite ("a"="b") x y的表达式(涉及两个不同字符串文本之间可判定的相等)时，simp本身似乎不允许我将这个表达式简化为y。这与ite ("a"="a") x y的情况形成了对比，后者通过simp简化为x。因此，我发现自己正在做一个案例分析，cases decidable.em ("a"="b") with H H，然后使用exfalso和dec_trivial处理一个案例，而另一个使用simp [H]。因此，我能够向前迈进，但我想知道是否有一个更惯用和更短的方式来实现同样的结果。

Answer 1

rw [if_neg (show "a" ≠ "b", from dec_trivial)]或simp [if_neg (show "a" ≠ "b", from dec_trivial)]都是我所知道的最简单的方法。