proposition: Lemma mapii_dep_spec : (forall a1 a2 : A, {a1 = a2}+{a1 <> a2}) -> forall l f l', (forall a a_in_l a_in_l', f a a_in_l = f a a_in_l') -> (In l' (mapii_dep (Dep_fun l f)) <-> exists l1, exists a, exists a_in_l, exists b, exists l2, In b (f a a_in_l) /\ l = l1 ++ a :: l2 /\ l' = l1 ++ b :: l2).
proof: Proof. intros eqA l; induction l as [ | a l]; intros f l' proof_ir; split; intro H. contradiction. destruct H as [[ | a1 l1] [a [a_in_l [b [l2 [_ [H _]]]]]]]; discriminate. rewrite mapii_dep_unfold in H; 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 (or_introl ((fix In (a : A) (l : list A) {struct l} : Prop := match l with | nil => False | b :: m => b = a \/ In a m end) a l) (eq_refl a)); exists b; exists l; subst; repeat split; trivial. rewrite in_map_iff in H; destruct H as [l'' [H1 H2]]. unfold dep_fun_tail in H2. rewrite IHl in H2. destruct H2 as [l1 [a' [a'_in_l [b [l2 [K [K' K'']]]]]]]. exists (a :: l1); exists a'; exists (or_intror (a = a') a'_in_l); exists b; exists l2; subst; repeat split; trivial. intros; apply proof_ir; right; trivial. destruct H as [l1 [a' [a'_in_l [b [l2 [K [K' K'']]]]]]]; subst. destruct l1 as [ | a1 l1]; simpl in K'; injection K'; clear K'; intros. subst l2 a'. simpl; rewrite mapii_dep_unfold; simpl. apply in_or_app; left; rewrite in_map_iff; exists b; split; trivial. simpl; rewrite <- (proof_ir a a'_in_l); trivial. rewrite mapii_dep_unfold; simpl. apply in_or_app; right; simpl; rewrite in_map_iff. exists (l1 ++ b :: l2); split; subst a1; trivial. unfold dep_fun_tail. rewrite IHl. destruct (eqA a a') as [a_eq_a' | a_diff_a']. subst a'. assert (a_in_l : In a l). clear K; subst l; apply in_or_app; right; left; trivial. exists l1; exists a; exists a_in_l; exists b; exists l2; repeat split; trivial. rewrite <- (proof_ir a a'_in_l); trivial. assert (a'_in_l' : In a' l). clear K; destruct a'_in_l as [a'_eq_a | a'_in_l]; trivial. absurd (a = a'); trivial. exists l1; exists a'; exists a'_in_l'; exists b; exists l2; repeat split; trivial. rewrite <- (proof_ir a' a'_in_l); trivial. intros a'' a''_in_l1 a''_in_l2; refine (proof_ir a'' _ _). Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)