fact: Definition refineEquiv_split_ex A B (P : A -> Prop) (P' : A -> B -> Prop) : @refineEquiv _ { b | exists a, P a /\ P' a b }%comp (a <- { a | P a /\ exists b, P' a b }; { b | P' a b })%comp.
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