proposition: Lemma split_refineEquiv_proj1_sig A P Q : refineEquiv { x : { x : A | P x } | Q (proj1_sig x) } (x <- { x | P x /\ Q x }; p <- { _ : P x | True }; ret (exist P x p)).
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