case cons
α✝ : Type u_1
f : α✝ → Option α✝
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : length (replaceF f tail✝) = length tail✝
⊢ length
      (match f head✝ with
      | none => head✝ :: replaceF f tail✝
      | some a => a :: tail✝) =
    succ (length tail✝)
α✝ : Type u_1
f : α✝ → Option α✝
l : List α✝
⊢ length (replaceF f l) = length l
induction l <;> simp [replaceF]
no goals
case cons
α✝ : Type u_1
f : α✝ → Option α✝
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : length (replaceF f tail✝) = length tail✝
⊢ length
      (match f head✝ with
      | none => head✝ :: replaceF f tail✝
      | some a => a :: tail✝) =
    succ (length tail✝)
split <;> simp [*]