Quickly simplifying the expression 'ite ("a"="b") x y'

Question

When being left with an expression of the form ite ("a"="b") x y which involves a decidable equality between two distinct string literals, it appear that simp on its own does not allow me to reduce this expressions to y. This is in contrast to the case of ite ("a"="a") x y which is reduced to x with simp. So I find myself doing a case analysis cases decidable.em ("a"="b") with H H and then handling one case using exfalso and dec_trivial and the other by using simp [H]. So I am able to move forward, but I was wondering if there was a more idiomatic and shorter way to achieve the same result.

Answer 1

Either rw [if_neg (show "a" ≠ "b", from dec_trivial)] or simp [if_neg (show "a" ≠ "b", from dec_trivial)] is the easiest way I know.