(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with
+rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with
[ nil2 ⇒ ◊
| cons2 l m cs ⇒ {l + i, m} @ pluss cs i
].
(* Basic properties *********************************************************)
-lemma pluss_SO2: â\88\80l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1.
+lemma pluss_SO2: â\88\80l,m,cs. ({l, m} @ cs) + 1 = {â\86\91l, m} @ cs + 1.
normalize // qed.
(* Basic inversion lemmas ***************************************************)