proposition: Lemma in_getSupport_bind_cp_fst : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) a0, In a0 (getSupport_bind_cp c1 c2) -> In (fst a0) (getSupport c1).
proof: Proof. intuition. unfold getSupport_bind_cp, getSupport_bind in *. destruct a0. eapply in_flattenPair_inv in H. destruct H. intuition. simpl. eapply in_map_iff in H1. destruct H1. intuition. inversion H1; clear H1; subst. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat