proposition: Lemma getSupport_Bind_In : forall (A B : Set) (c : Comp B)(f : B -> Comp A) a, In a (getSupport (Bind c f)) -> exists b, In b (getSupport c) /\ In a (getSupport (f b)).
proof: Proof. intuition. simpl in *. apply in_getUnique_if in H. eapply in_flatten in H. destruct H. intuition. apply in_map_iff in H0. destruct H0. intuition. subst. econstructor. intuition; eauto. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec