| cons | : | [nat → nat × funlist] ⟶ funlist |
| false | : | bool |
| head | : | [funlist] ⟶ nat → nat |
| if | : | [bool × nat → string × nat → string] ⟶ nat → string |
| nil | : | funlist |
| s | : | [nat] ⟶ nat |
| tail | : | [funlist] ⟶ funlist |
| test | : | [nat → nat] ⟶ bool |
| true | : | bool |
| F | : | nat → string |
| Z | : | nat → string |
| G | : | nat → nat |
| V | : | funlist |
| if(true, F, Z) | ⇒ | F |
| if(false, F, Z) | ⇒ | Z |
| test(λ%X:nat.s(%X)) | ⇒ | true |
| head(cons(G, V)) | ⇒ | G |
| tail(cons(G, V)) | ⇒ | V |