all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code

(binary:application/pdf)