A model M is a pair (F,V) where V is an interpretation (valuation) sending atomic types to subsets of W.  For complex types, the valuation respects the clauses below.  We write x ∈ V(A) as M,x ⊩ A or, if no confusion will arise, x ⊩ A.