 Quantifier elimination for the random graph

Every small partial embedding of a monster random graph extends by back-and-forth to an automorphism, using saturation and the extension axioms. It is therefore elementary, and the theory of the random graph eliminates quantifiers.