proposition: Lemma Bind_inv {A B: Type} : forall (ca : Comp A) (f : A -> Comp B) (v : B), ca >>= f ↝ v -> exists a', ca ↝ a' /\ f a' ↝ v.
proof: Proof. destruct 1; eauto. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Fiat.Common Fiat.Computation.Notations