We use this new feature to implement array access notation `a[i]`.
indentifier.lean
fun x, e
fun x => e
=>
:=