simp [h]
case a
α : 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
i : α
h : mem i x
⊢ mem i (c :: x)
no goals