proposition: Lemma refineEquiv_swap_bind {A B C} (c1 : Comp A) (c2 : Comp B) (f : A -> B -> Comp C) : refineEquiv (a <- c1; b <- c2; f a b) (b <- c2; a <- c1; f a b).
proof: Proof. split; repeat intro; computes_to_inv; repeat (econstructor; try eassumption). 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