More work on MoreLogic.v