proposition: Lemma refineEquiv_pick_pair_snd_dep A B (PA : A -> Prop) (PB : A * B -> Prop) : @refineEquiv _ { x | PA (fst x) /\ PB x }%comp (a <- { a | PA a }; b <- { b | PB (a, b) }; ret (a, b))%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