-let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
-[O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S
-l) \Rightarrow (minus k l)])]).
+rec definition minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match
+n with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S
+k) | (S l) \Rightarrow (minus k l)])]).