-
Robbert Krebbers authored
put it into a type class `BiPureForall`. This property does not hold for embeddings of classical logic into Coq.
6e334252
put it into a type class `BiPureForall`. This property does not hold for embeddings of classical logic into Coq.