proposition: Lemma refineEquiv_if_ret {A} : forall (cond : bool) (ta ea : A), refineEquiv (ret (If cond Then ta Else ea)) (If cond Then ret ta Else ret ea).
proof: Proof. split; destruct cond; reflexivity. 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