proposition: Lemma refine_under_bind_both_trans {A B} : forall c c' c'' (x y : A -> Comp B), refine c c' -> (forall a, c ↝ a -> refine (x a) (y a)) -> refine (a <- c'; y a) c'' -> refine (a <- c; x a) c''.
proof: Proof. intros; etransitivity; eauto using refine_under_bind_both. 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