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