proposition: Lemma In_getSupport_bind_cp : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) b a, In b (getSupport c1) -> In a (getSupport (c2 b)) -> In (b, a) (getSupport_bind_cp c1 c2).
proof: Proof. intuition. unfold getSupport_bind_cp, getSupport_bind. eapply in_flattenPair. eapply in_map_iff. econstructor; intuition. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat