3 (function n -> (function f -> (function m ->
5 Matita_nat_nat.O -> (f m)
6 | Matita_nat_nat.S(p) -> (Matita_nat_plus.plus (f (Matita_nat_plus.plus (Matita_nat_nat.S(p)) m)) (sigma p f m)))
12 (function n -> (function f -> (function m ->
14 Matita_nat_nat.O -> (f m)
15 | Matita_nat_nat.S(p) -> (Matita_nat_times.times (f (Matita_nat_plus.plus (Matita_nat_nat.S(p)) m)) (pi p f m)))