proposition: Lemma split_refineEquiv_snd_proj1_sig A B P Q : refineEquiv { x : { x : A * B | P x } | Q (snd (proj1_sig x)) } (x <- { x : B | Q x }; y <- { y : A | P (y, x) }; pf <- { pf : P (y, x) | 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