When a mlw file contained "while not foo do", one of the VCs contained
"not not foo" as a hypothesis, due to a poor interaction between bool and
prop. This commit ensures that such hypotheses get simplified to "foo".