In the Little Typer chapter 2 frame 100 gives the following definition: (claim pearwise+ (→ Pear Pear Pear)) (define pearwise+ (λ (anjou bosc) (elim-Pear anjou (λ (a1 d1) (elim-Pear bosc (...