head { cons p q } | |

= lambda c {$c {lambda {x y} {$x}} } { cons p q } |
by variable substitution and list reduction of the first element |

-> cons p q {lambda {x y} {$x}} |
by currying and lambda reduction and list reduction of the first element |

= lambda {a b f} {$f $a $b} p q {lambda {x y} {$x}} |
by variable substitution and list reduction of the first element |

-> lambda {b f } { $f p $b } q {lambda {x y} {$x}} |
by currying |

-> lambda f {$f p q} {lambda {x y} {$x}} |
by currying |

-> lambda {x y} {$x} p q |
by currying and lambda reduction and list reduction of the first element |

-> lambda {y} {p} q |
by currying |

-> p |
by currying and lambda reduction and list reduction of the first element |