(* 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 ***************************************************)