proposition: Lemma mapii_dep_eq : forall l f g, (forall t (t_in_l : In t l), f t t_in_l = g t t_in_l) -> mapii_dep (Dep_fun l f) = mapii_dep (Dep_fun l g).
proof: Proof. intro l; induction l as [ | a l]; intros f g H; do 2 rewrite mapii_dep_unfold; simpl; trivial. rewrite (H a). apply (f_equal (fun ll => map (fun b : A => b :: l) (g a (or_introl ((fix In (a0 : A) (l0 : list A) {struct l0} : Prop := match l0 with | nil => False | b :: m => b = a0 \/ In a0 m end) a l) (eq_refl a))) ++ map (fun k : list A => a :: k) ll)). unfold dep_fun_tail. apply IHl. intros; apply H; right; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)