The so-called "untyped λ-calculus": how many types does it really have?

[λ the β-Redex Reducer]

You're supposed to ignore lots of true facts when they don't help in what you're doing.

Ignore, not deny.