proposition: Lemma refine_If_Then_Else_trans {A} : forall (c : bool) (x y z : Comp A), refine x y -> forall x0 y0 : Comp A, refine x0 y0 -> refine (If c Then y Else y0) z -> refine (If c Then x Else x0) z.
proof: Proof. intros; etransitivity; eauto using refine_If_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