proposition: Theorem in_flattenPair : forall (A B : Type)(ls : list (A * (list B))) a b entryList, In (a, entryList) ls -> In b entryList -> In (a, b) (flattenPair ls).
proof: Proof. induction ls; intuition; simpl in *. intuition. inversion H1; clear H1; subst. eapply in_or_app. left. eapply in_map_iff. econstructor. intuition. eapply in_or_app. right. eapply IHls; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat