proposition: Lemma split_refineEquiv_fst_proj1_sig A B P Q : refineEquiv { x : { x : A * B | P x } | Q (fst (proj1_sig x)) } (x <- { x : A | Q x }; y <- { y : B | P (x, y) }; pf <- { pf : P (x, y) | True }; ret (exist P _ pf)).
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