proposition: Lemma refineEquiv_pick_prim_prod: forall (A B : Type) (PA : A -> Prop) (PB : B -> Prop), refineEquiv {x : prim_prod A B | PA (prim_fst x) /\ PB (prim_snd x)} (a <- {a : A | PA a}; b <- {b : B | PB b}; ret {| prim_fst := a; prim_snd := b |}).
proof: Proof. split; intros; intros v Comp_v; computes_to_inv; subst; repeat computes_to_econstructor; simpl; intuition eauto. destruct v; simpl; computes_to_econstructor. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory