most notably, adding the missing proof that L-wave and L-bar are Elgot
to that end, unifying the constructing of L-bar and L-wave, along the way
fixing various level issues