-definition cbk:
- C \to nat
-\def
- let rec cbk (c: C) on c: nat \def (match c with [(CSort m) \Rightarrow m |
-(CHead c0 _ _) \Rightarrow (cbk c0)]) in cbk.
+rec definition cbk (c: C) on c: nat \def match c with [(CSort m) \Rightarrow
+m | (CHead c0 _ _) \Rightarrow (cbk c0)].