Theorem: LambdaCalculi.LambdaTerm.replace'_some (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 : ℕ
t u : LambdaTerm p U C
h : f n t = some u
⊢ replace' f n t = u
Tactic:
cases t <;> simp only [h, replace']
State after:
no goals