4462.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/closed/4462.v

blob: c680518c6a14e8f259846d8f360f4e71f76e80d4 (plain)

Variables P Q : Prop.
Axiom pqrw : P <-> Q.

Require Setoid.

Goal P -> Q.
unshelve (rewrite pqrw).