Bug: Investigate if using `option` instead of `option'` is OK in `zepto` branch

# Why?

I swapped `option'` with `option` and it typechecks.

Not sure it's correct though!

# What?

- [ ] Check `Megaparsec.lean`'s logic, compare `option` with `option'`.
- [ ] If the semantics are consistent, do nothing. Otherwise, fix the bug.

Read the parser logic in Megaparsec.lean on the zepto branch, then compare the semantics of option and option'. Determine whether the typechecking substitution preserves the intended behavior; if it does, no code change is needed, otherwise fix the discrepancy and verify the relevant parser behavior.

Written by the indexing model from the issue text.