proposition: Lemma refine_eqA_into_ret : forall {A: Type} {eqA: list A -> list A -> Prop}, Reflexive eqA -> forall (comp : Comp (list A)) (impl result: list A), comp = ret impl -> ( comp ↝ result -> eqA result impl ).
proof: Proof. intros; subst; computes_to_inv; subst; 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