simp only [eval_succ]
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ eval f (i :: c) = eval g (i :: c)
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ (f i.fst == i.snd || eval f c) = (g i.fst == i.snd || eval g c)