proposition: Lemma map_id : forall (A : Type) l, map (fun t : A => t) l = l.
proof: Proof. intros A l; induction l as [ | t l]; simpl; trivial. rewrite IHl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)