put it into a type class `BiPureForall`.

This property does not hold for embeddings of classical logic into Coq.