proposition: Lemma refine_pick_forall_Prop A B C (a : A) (Q : C -> A -> Prop) (P : A -> C -> B -> Prop) b : (forall c : C, Q c a -> refine {x : B | P a c x} b) -> refine {b' : B | forall c : C, Q c a -> P a c b'} b.
proof: Proof. unfold refine; intros; computes_to_econstructor; intros. generalize (H _ H1 _ H0); intros. computes_to_inv; assumption. 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