MoreLogic.v done, except pigeonhole