proposition: Lemma eq_ret_compute : forall (A: Type) (x y: A), x = y -> ret x ↝ y.
proof: Proof. intros; subst; apply ReturnComputes; trivial. 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