This is really helpful. Minor nit under Curry-Howard correspondence: "True propositions have exactly one term" should be "have at least one term".