1 2 3 4 5 6 7
Variables P Q : Prop. Axiom pqrw : P <-> Q. Require Setoid. Goal P -> Q. unshelve (rewrite pqrw).