+let rec fact =
+ \lambda x:nat.
+ [\lambda x:nat. nat]
+ match x:nat with
+ [ O \Rightarrow 1
+ | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
+in
+(fact 4)
+### (* METASENV after disambiguation *)
+ |- ?2: Type
+ |- ?3: ?2[]
+### (* TERM after disambiguation *)
+[fact:=
+Fix fact {
+fact / 0 : (nat->nat) :=
+[x:nat]
+<[x:nat]nat>Cases x of
+ O => (S O)
+ S => [x:nat](mult (S x) (fact x))
+end}
+](fact (S (S (S (S O)))))
+### (* TYPE_OF the disambiguated term *)
+nat
+### (* REDUCED disambiguated term *)
+(S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) :=
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) O))))))))