\v0 -> v0 1 ?1 1 ?3 1 f 1 2 \v0 -> v0 ?1 f f 1 2 2 g 0 \v0 -> g v0 g ?1 5 3 g2 f 32 g2 23 3.14 succ zero ?1 zeroF dec (succF zeroF) dec zeroF \v0 -> dec v0 dec ?1 g3 ?3 0 g (g2 ?1 0) succ (succ zero) zero dec2 0 err succ err \v0 -> dec (dec v0)