2.4. Reducibility
A term is reducible when its L0 meaning can take a beta step. The contextual
form ReducibleIn is used when reasoning under named binders.
def ReducibleIn (ρ : List String) (e : L1) : Prop :=
∃ e', L1.toL0With ρ e →β₀ e'def Reducible (e : L1) : Prop :=
ReducibleIn [] e