proposition: Lemma getSupport_In_Bind : forall (A B : Set) b (c : Comp B)(f : B -> Comp A) a, In b (getSupport c) -> In a (getSupport (f b)) -> In a (getSupport (Bind c f)).
proof: Proof. intuition. simpl. eapply in_getUnique. eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eapply eq_refl. eauto. trivial. Qed.
imports: Crypto FCF RndNat