  Sets and relations are very useful concepts for defining denotational
semantics. In the Coq proof assistant, curried functions to Prop are used to
represent sets and relations, e.g. A -> Prop, A -> B -> Prop, A -> B -> C ->
Prop, etc. Further, the membership relation can be encoded by function
applications, e.g. X a represents a in X if X: A -> Prop. This is very
convenient for developing formal definitions and proofs for professional users,
but it makes propositions more difficult to read for non-professional users,
e.g. students of a program semantics course. We develop a small Coq library of
sets and relations so that standard math notations can be used when teaching
denotational semantics of simple imperative languages. This library is
developed using Coq's type class system. It brings about zero proof-term
overhead comparing with the existing formalization of sets.
