no goals
ι : Type ?u.78062
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
x✝ : a ≠ b
h : a ≠ b := x✝
⊢ indexOf a (b :: l) = succ (indexOf a l)
simp only [indexOf, findIdx_cons, Bool.cond_eq_ite, beq_iff_eq, h, ite_false]