4 lines
78 B
Text
4 lines
78 B
Text
|
unfold_rec2.lean:8:2: proof state
|
|||
|
|
a n : ℕ
|
|||
|
|
⊢ a = 2 → f (a * 2) n = f 4 n
|