<p>i just finished implementing X-propagation semantics in the SMT-based transformation verifier (i.e. it now uses refinement and not equivalence) and as a result i am suddenly at war with the law of excluded middle</p><p>the pass that lowers `match` cells thinks that (or x (not x)) is always true. which it isn't! and so the transformation is invalid under our refinement rules</p><p>no idea what to do about it :D</p>
