proposition: Theorem flat_map_empty: forall A B (ll:list A) (f: A -> list B) , flat_map f ll =[] <=> forall a, LIn a ll -> f a =[].
proof: Proof. sp_iff Case. Case "->". intros Hmap a Hin; remember (f a) as fa; destruct fa. auto. assert ({a: A $ LIn a ll # LIn b (f a)}) as Hass; try (apply lin_flat_map in Hass; rewrite Hmap in Hass; inversion Hass). exists a. (split; auto). rewrite <- Heqfa. constructor; auto. Case "<-". intros Hin. remember (flat_map f ll) as flat; destruct flat ;auto. assert ( LIn b (flat_map f ll)) as Hinbf by (rewrite <- Heqflat; constructor; auto). apply lin_flat_map in Hinbf. exrepnd. apply Hin in Hinbf1. rewrite Hinbf1 in Hinbf0. inversion Hinbf0. Qed.
imports: UsefulTypes bin_rels Omega