proposition: Lemma comp_split_snd {A B} (x : A * B) : refineEquiv (ret (snd x)) (ab <- ret x; ret (snd ab)).
proof: Proof. autorewrite with refine_monad; reflexivity. 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