proposition: Lemma refine_bind_dedup {A B} (c1 : Comp A) (f : A -> A -> Comp B) : refine (a <- c1; b <- c1; f a b) (a <- c1; f a a).
proof: Proof. 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