proposition: Lemma refineEquiv_pick_pick A (P1 P2 : A -> Prop) (H : forall x, P1 x <-> P2 x) : @refineEquiv _ { x : A | P1 x }%comp { x : A | P2 x }%comp.
proof: Proof. t_refine. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.Tactics