proposition: Lemma not_In_getSupport_bind_cp : forall (A B : Set)(eqda : eq_dec A)(eqdb : eq_dec B)(c1 : Comp B)(c2 : B -> Comp A) b a, ~ In (b, a) (getSupport_bind_cp c1 c2) -> ~ In b (getSupport c1) \/ ~ In a (getSupport (c2 b)).
proof: Proof. intuition. destruct (in_dec eqdb b (getSupport c1)); intuition. destruct (in_dec eqda a (getSupport (c2 b))); intuition. exfalso. eapply H. eapply In_getSupport_bind_cp; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat