(RENAME subtypes <:)
(REWRITE (object_to_int $x) $x)
(REWRITE (int_to_object $x) $x)
(REWRITE (object_to_array $x) $x)
(REWRITE (array_to_object $x) $x)

  (forall (?h Heap) (?o Object) (?f Object) (?e Object)
     (= (select2 (store2 ?h ?o ?f ?e) ?o ?f) ?e))

  (forall (?h Heap) (?o Object) (?f Object) (?p Object) (?g Object) (?e Object) 
     (implies
     	 (not (= ?o ?p))
         (= (select2 (store2 ?h ?o ?f ?e) ?p ?g)
            (select2 ?h ?p ?g))))

  (forall (?h Heap) (?o Object) (?f Object) (?p Object) (?g Object) (?e Object) 
     (implies
     	 (not (= ?f ?g))
         (= (select2 (store2 ?h ?o ?f ?e) ?p ?g)
            (select2 ?h ?p ?g))))