proposition: Lemma map_ext' : forall (A B : Type) (f g : A -> B) (l:list A), (forall a : A, a el l -> f a = g a) -> map f l = map g l.
proof: Proof. intros. induction l. - reflexivity. - simpl. rewrite H;auto using in_eq, in_cons. f_equal. apply IHl. intros. apply H. auto using in_eq, in_cons. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd