proposition: Lemma refine_If_Opt_Then_Else_trans {A B} : forall (c : option B) (e e' z: Comp A) (t t' : B -> Comp A), (forall b, refine (t b) (t' b)) -> (refine e e') -> refine (Ifopt c as b' Then t' b' Else e') z -> refine (Ifopt c as b' Then t b' Else e) z.
proof: Proof. intros; etransitivity; eauto using refine_If_Opt_Then_Else. 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