The quantifier-free type of a tuple records all atomic and negated atomic formulas it satisfies, equivalently all quantifier-free formulas. Equal such types identify the generated substructures by sending each term value at one tuple to the value of the same term at the other tuple. Equality formulas make this correspondence well defined, and the relational formulas make it an isomorphism.
New to topics? Read the docs here!