For anyone confused here, the “simple” here comes from the simply-typed lambda calculus, that it models. This post addresses several issues with a tutorial paper on a dependently-typed lambda calculus, which is what all the build-up is for.

I would have found this blog post helpful when I was implementing the original tutorial paper, because I got stuck with the higher-order abstract syntax for lambdas. The original uses lambda literals from Haskell, which I couldn't figure it out how to express in Coq or Rust, because of the type recursion and some other issues. Whereas, I would easily be able to implement the first-order alternative presented here in either language.