{{!

   Assumption predicates (and possibly operators), and ASSUME directive.
   
   For example:

   \* True iff 'field' in records in 'set'  have correct 'domain'
   Assume_DomainOfAField( set, field, domain ) == { p[field] : p \in  set }  = domain

   \* Verify that domain of named field is correct
   Assume_Pet_Domains == Assume_DomainOfAField( t_Pet, "id", d_pet_id )

   \* Domain verification phase 1
   ASSUME Assume_Pet_Domains


}}

{{!>assumption_generic.tla}}
{{!>assumption_pet.tla}}