Only unary/binary functions in the core

[wwitzel]

I'm not sure how well this would work or if it would be desirable, but what if n-ary functions were implemented as definitions outside of the core? This would simplify proof-checking, but proofs would be longer. This may (or may not) be a desirable trade. Alternatively, we could keep the core as is but translate proofs from into something that can be checked by a simpler proof-checker. It's worth exploring the possibilities before deciding.