Previously expected propositions were erased frequently
(at lets and ifs) and checking for logical entailment
was unidirectional instead of bidirectional. In other words,
instead of checking if propositions held at the leaves
of the AST, we would typecheck the AST and blindly propagate
up ALL logical info we learned at each step. This meant that
we would get exponential blow up of propositions even when
we didn't care about their content.
With this commit, instead now we send down expected types
*and* propositions so we can verify expected types and
propisitions are satisfied at leaves, thereby relieving the
need to constantly report up huge amounts of logical info
while typechecking.
