simp only [eval_succ]
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
⊢ eval f (c :: x) = eval g (c :: x)
α : Type
f g : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (i : α), mem i x → f i = g i) → eval f x = eval g x
w : ∀ (i : α), mem i (c :: x) → f i = g i
⊢ (Clause.eval f c && eval f x) = (Clause.eval g c && eval g x)