proposition: Lemma refineEquiv_pick_forall_eq A B (a : A) (P : A -> B -> Prop) : @refineEquiv _ (Pick (fun b => forall a', a = a' -> P a' b)) (Pick (P a)).
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