Maude stuff

@andreistefanescu @traiansf please review.
However, I don't really understand why matching on mi is allowed since mi is a function.  maybe it should be called something else?