+set "baseuri" "cic:/matita/tests/letrec/".
+
alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
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) ].