let produces an or instead of two imps

using a disjunction here keeps things in a form that is easier to
eliminate duplicate logical info with (i.e. the type system has an
easier time detecting unneeded disjunctions than implications, so using
disjunctions keeps some programs from creating propositions that grow
exponentially)