proposition: Lemma map_simpl : forall A B f l, @map A B f l = match l with | nil => nil | a :: l=> (f a) :: (@map A B f l) end.
proof: Proof. intros A B f l; destruct l ; reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid