proposition: Theorem in_flatten : forall (A : Set)(ls : list (list A)) a, In a (flatten ls) <-> exists x : _, In x ls /\ In a x.
proof: Proof. induction ls; simpl in *; intuition. destruct H; intuition. apply in_app_or in H. intuition. exists a; intuition. apply IHls in H0. destruct H0. intuition. exists x; intuition. apply in_or_app. destruct H; intuition. subst. intuition. right. eapply IHls. econstructor. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation