+inductive mr2: Type[0] :=
+ | nil2 : mr2
+ | cons2: nat → nat → mr2 → mr2.
+
+interpretation "nil (multiple relocation with pairs)"
+ 'Diamond = (nil2).
+
+interpretation "cons (multiple relocation with pairs)"
+ 'Semicolon hd1 hd2 tl = (cons2 hd1 hd2 tl).