i. At the instance level one has the primitive "c1 inheres_in c2 at t" relation, satisfying the principle of non-migration (a inheres_in b at t & a exists_at t' -> a inheres_in b at t') and possibly other axioms ("There are no bare particulars" etc.)
ii. At the universal level we have the two definitions:
C1 inheres_in C2 =df. (c1)(t) [c1 instance_of C1 at t -> (Ec2) (c2 instance_of C2 at t & c1 inheres_in c2 at t)]
C2 is_bearer_of C1 =df. (c2)(t) [c2 instance_of C2 at t -> (Ec1) (c1 instance_of C1 at t & c1 inheres_in c2 at t)]
No other clauses/qualifications necessary: non-migration takes care of everything.
inheres_in is a relation between dependent continuants and their bearers. Examples:
the particular redness that inheres in a particular fly eye.
Can anything inhere in >1 bearer? Generically dependent continuants? Or is this a different relation?