This seems like a really strange place to prove that String is an OrderedType. None of the rest of the file depends on this definition.
Also, concerning the same file, but a different part. What are the extra lemmas at the end of the file for? I would have expected this file to end by proving that [Map [K,V]] is a SeparationAlgebra. Are these extra properties useful for proving things in other files? If so, does that mean that SepAlg is not a complete definition?
This seems like a really strange place to prove that String is an OrderedType. None of the rest of the file depends on this definition.
Also, concerning the same file, but a different part. What are the extra lemmas at the end of the file for? I would have expected this file to end by proving that [Map [K,V]] is a SeparationAlgebra. Are these extra properties useful for proving things in other files? If so, does that mean that SepAlg is not a complete definition?