The types of propositions for monPred lemma need to be [monPred I PROP] and...

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.
2 jobs for gen_proofmode in 3 minutes and 27 seconds (queued for 2 seconds)
Status Name Job ID Coverage
  Build
passed build-coq.8.7.1 #7389
fp-timing

00:03:13

 
  Deploy
passed opam #7390

00:00:14