proposition: Lemma Bind_refine_If_Then_Else {A B} : forall i (t e : A -> Comp B) (ca : Comp A), refine (a <- ca; If i Then t a Else e a) (If i Then (a <- ca; t a) Else (a <- ca; e a)).
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