proposition: Lemma BindComputes {A B: Type} : forall (ca : Comp A) (f : A -> Comp B) (a : A) (b : B), ca ↝ a -> f a ↝ b -> ca >>= f ↝ b.
proof: Proof. econstructor; eauto. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Notations