The elementary calculus of binary relations as developed by Tarski in [5] may be thought of as a certain part of the first-order predicate calculus. Though less expressive, its theory (i.e. the set of its valid sentences) was shown to be undecidable by Tarski in [6]. Translated into algebraic logic this means that the equational theory of the class of relation algebras is undecidable. Similarly it can be proved that the same holds for the (sub-) class of proper relation algebras. The idea in Tarski's proof is to describe a pairing function by which any quantifier prefix may be contracted. In this note we apply a different method to treat the case of finite structures. We prove the Theorem. The equational theory of the class of finite proper relation algebras is undecidable. This result was announced in [4]. The main tool is representing the graph of primitive recursive functions via the cardinalities in finite simple models of equations.