proposition: Lemma refine_skip {A B C} (c : Comp A) (f : A -> Comp B) (dummy : A -> Comp C) : refine (Bind c f) (a <- c; dummy a>> f a).
proof: Proof. repeat first [ intro | computes_to_inv | computes_to_econstructor; eassumption | computes_to_econstructor; try eassumption; [] ]. computes_to_econstructor; eauto. 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