-
Jacques-Henri Jourdan authored
The types of propositions for monPred lemma need to be [monPred I PROP] and not [bi_car (monPredI I PROP)], otherwise iIntoValid fails in a very weird way. Seems to be related to a Coq bug.
e181f737
The types of propositions for monPred lemma need to be [monPred I PROP] and not [bi_car (monPredI I PROP)], otherwise iIntoValid fails in a very weird way. Seems to be related to a Coq bug.