proposition: Lemma refine_If_Opt_Then_Else_Bind {A B C} : forall (i : option A) (t : A -> Comp B) (e : Comp B) (c : B -> Comp C), refine (b <- If_Opt_Then_Else i t e; c b) (If_Opt_Then_Else i (fun a' => b <- t a'; c b) (b <- e; c b)).
proof: Proof. intros; destruct i; simpl; 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