my first theorem prover see elaboration-zoo for the original implementation and look here for a good tutorial on normalization by evaluation.