Completed L/N/M proofs. Included agda versions because why not.
ignore agdai