proposition: Lemma refine_If_Then_Else_ret {A} : forall i (t e : A), refine (@If_Then_Else (Comp A) i (ret t) (ret e)) (ret (@If_Then_Else A i t e)).
proof: Proof. destruct i; 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