proposition: Lemma refine_If_Opt_Then_Else_ret {A B} : forall i (t : A -> B) (e : B), refine (@If_Opt_Then_Else A (Comp B) i (fun a => ret (t a)) (ret e)) (ret (@If_Opt_Then_Else A B 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