Dear all, I have a reflection goal, `reflect (X : Prop ) (b : bool))`

for some expression `X`

and `b`

. I would like to perform some manipulation (`rewrite or_assoc`

) to X to some equivalent `X'`

expression as I have a lemma which solve for `reflect (X' : Prop )(b : bool )`

easily.

The `reflect`

predicate does not allow rewriting directly, so `apply: (iffP idP)`

is used to unfold `reflect`

, so that the required manipulation can be performed. After which I would like to reverse the `apply: (iffP idP)`

tactic to restore the `reflect`

expression. Is there anyway to do this?

Many thanks!!

```
From mathcomp Require Import all_ssreflect.
Context (P Q : Prop) (b : bool).
Hypothesis (PQ : P <-> Q) (Pb : reflect P b).
Goal reflect Q b.
Proof. by apply/(equivP Pb PQ). Qed.
```

Thanks @Pierre-Yves Strub ! `equivP`

is exactly what I'm looking for :)

Last updated: Jul 23 2024 at 20:01 UTC