feat(untyped): the Leftmost Reduction Theorem

[m-ow]

Introduces leftmost reduction ⭢ℓ, a beta-step contracting the redex at position 0, together with normal forms, and proves the Leftmost Reduction Theorem: if a term beta-reduces to a normal form, the leftmost strategy reaches it too.
The result falls out of standardization, following Copes (2018).

Builds on top of #679

[lengyijun]

Can you add 2 theorems :

1. NormalForm M <-> Normal FullBeta M
2. Decidable Normal FullBeta

[m-ow]

@lengyijun Sounds good, I'll get both into a separate PR soon :)

[lengyijun]

Should we rename Normal to NormalBeta ?
Or put it in namespace "FullBeta"

Normal may also refer to Normal FullBetaEta or Normal FullEta