proposition: Lemma in_concat : forall l y, In y (concat l) <-> exists x, In x l /\ In y x.
proof: Proof. intro l; induction l as [|a l IHl]; simpl; intro y; split; intros H. - contradiction. - destruct H as (x,(H,_)); contradiction. - destruct (in_app_or _ _ _ H) as [H0|H0]. + exists a; auto. + destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). exists x; auto. - apply in_or_app. destruct H as (x,(H0,H1)); destruct H0. + subst; auto. + right; destruct (IHl y) as (_,H2); apply H2. exists x; auto. Qed.
imports: PeanoNat