proposition: Lemma refine_flip A (a : Comp A) B (b : Comp B) C (z : A -> B -> Comp C) : refineEquiv (x <- a; y <- b; z x y) (y <- b; x <- a; z x y).
proof: Proof. intros. Local Transparent Bind. unfold Bind. unfold refineEquiv. unfold refine. Local Transparent computes_to. unfold computes_to. unfold Ensembles.In. split; intros x H; do 2 destruct H; do 2 destruct H0; exists x1; split; trivial; exists x0; split; trivial. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common.StringBound Fiat.Common.Ensembles.IndexedEnsembles Fiat.Computation.FoldComp Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure