Theorem: LambdaCalculi.LambdaTerm.replace'_case (LambdaCalculi/LambdaCalculus.lean)

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
f : ℕ → LambdaTerm p U C → Option (LambdaTerm p U C)
n : ℕ
h : p.coprod = true
l r t : LambdaTerm p U C
⊢ replace' f n (case h l r t) =
    match f n (case h l r t) with
    | some u => u
    | none => case h (replace' f (n + 1) l) (replace' f (n + 1) r) (replace' f n t)
Tactic:
simp only [replace']
State after:
no goals