proposition: Theorem getSupport_In_Seq : forall (A B : Set)(c : Comp A)(f : A -> Comp B) b a, In a (getSupport c) -> In b (getSupport (f a)) -> In b (getSupport (Bind c f)).
proof: Proof. intuition. simpl. eapply in_getUnique. eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eauto. eauto. trivial. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec