proposition: Theorem map_id : forall f : A -> A, (forall x : A, f (f x) = x) -> forall L : list A, map f (map f L) = L.
proof: Proof. intros f H' L; elim L; simpl in |- *; auto. intros a l H'0. rewrite H'; rewrite H'0; auto. Qed.
imports: Coq(Arith) Coq(List)