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
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