alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-let rec plus n m : nat \def
+let rec plus n m \def
match n with
[ O \Rightarrow m
| (S x) \Rightarrow S (plus x m) ].