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