proposition: Lemma mapii_spec : forall (A : Type) (f : A -> list A) l l', (In l' (mapii f l) <-> exists l1, exists a, exists b, exists l2, In b (f a) /\ l = l1 ++ a :: l2 /\ l' = l1 ++ b :: l2).
proof: Proof. intros A f l; induction l as [ | a l]; intros l'; split; intro H. contradiction. destruct H as [[ | a1 l1] [a [b [l2 [_ [H _]]]]]]; discriminate. simpl in H; destruct (in_app_or _ _ _ H) as [H' | H']; clear H; rename H' into H. rewrite in_map_iff in H; destruct H as [b [H1 H2]]. exists (@nil A); exists a; exists b; exists l; subst; repeat split; trivial. rewrite in_map_iff in H; destruct H as [l'' [H1 H2]]. rewrite (IHl l'') in H2. destruct H2 as [l1 [a' [b [l2 [K [K' K'']]]]]]. exists (a :: l1); exists a'; exists b; exists l2; subst; repeat split; trivial. destruct H as [l1 [a' [b [l2 [K [K' K'']]]]]]; subst. destruct l1 as [ | a1 l1]; simpl in K'; injection K'; clear K'; intros; subst. simpl; apply in_or_app; left; rewrite in_map_iff; exists b; split; trivial. simpl; apply in_or_app; right; simpl; rewrite in_map_iff. exists (l1 ++ b :: l2); split; trivial. rewrite IHl. exists l1; exists a'; exists b; exists l2; repeat split; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)