no goals
α : Type u_1
p : α → Option α
l : List α
h : ∀ (a : α), a ∈ l → p a = none
⊢ replaceF p l = l
induction l with
| nil => rfl
| cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]
no goals
case nil
α : Type u_1
p : α → Option α
h : ∀ (a : α), a ∈ [] → p a = none
⊢ replaceF p [] = []
rfl
no goals
case cons
α : Type u_1
p : α → Option α
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → p a = none) → replaceF p tail✝ = tail✝
h : ∀ (a : α), a ∈ head✝ :: tail✝ → p a = none
⊢ replaceF p (head✝ :: tail✝) = head✝ :: tail✝
simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]