Handling ite

Stream: new members

[Guilherme Espada]

I have a goal of the form:

some_cons (ite (t = x) s (t_var t))

What is the best way to turn this into two goals?
I tried

by_cases t=x,
{
      rw h,
      simp,
}

Which works in the positive case. However, I don't know how to simplify the negative case.

Thanks

[Anne Baanen]

tactic#split_ifs? Or you can rw if_neg (h : ¬ t = x)

[Anne Baanen]

(docs#if_pos and docs#if_neg)

[Guilherme Espada]

Split_ifs is exactly what I was looking for, thanks!