-let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B :=
- match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)].
+definition foldr ≝
+ λA,B:Type.λf:A→B→B.λb:B.
+ let rec foldr (l : list A) on l : B :=
+ match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr l)]
+ in foldr.