Everything nicely defined and proved

Only thing left is mtype_r_dec. To prove this we need to turn that relation into a function.
And for that we need a good measure for the find function.