instantiate parameter
   heap
< 
   separation
with 
   heapmap
   
by mapping
      : Heap[A] → Map[Ref[A], A]; 
      ∅ : Heap[A] → ∅ : Map[Ref[A] × A]; 
      # .  : (Heap[A] → Nat) → # .  : (Map[Ref[A] × A] → Nat); 
       . ∈ .  : (Ref[A] × Heap[A] → Bool) →  . ∈ .  : (Ref[A] × Map[Ref[A] × A] → Bool); 
      alloc# → alloc#; 
       . (. := .)  →  . [ . := . ]h : (Map[Ref[A] × A] × Ref[A] × A → Map[Ref[A] × A]); 
       . ( . )  →  . [ . ]h : (Map[Ref[A] × A] × Ref[A] → A); 
       . ++ .  : (Heap[A] × Ref[A] → Heap[A]) →  . +h .  : (Map[Ref[A] × A] × Ref[A] → Map[Ref[A] × A]); 
       . -- .  : (Heap[A] × Ref[A] → Heap[A]) →  . --h .  : (Map[Ref[A] × A] × Ref[A] → Map[Ref[A] × A]); 
   rename 
       . ∪ .  : (Heap[A] × Heap[A] → Heap[A]) →  . ∪ .  : (Map[Ref[A] × A] × Map[Ref[A] × A] → Map[Ref[A] × A]); 
       . \ .  : (Heap[A] × Set[Ref[A]] → Heap[A]) →  . \ .  : (Map[Ref[A] × A] × Set[Ref[A]] → Map[Ref[A] × A]); 
       . \ .  : (Heap[A] × Heap[A] → Heap[A]) →  . \ .  : (Map[Ref[A] × A] × Map[Ref[A] × A] → Map[Ref[A] × A]); 
      dom .  → dom .  : (Map[Ref[A] × A] → Set[Ref[A]]); 
       . * .  →  . * .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
       . ⊗ .  →  . ⊗ .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
       . -* .  →  . -* .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
       . -⊗ .  →  . -⊗ .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
      not .  : ((Heap[A] → Bool) → Heap[A] -> Bool) → not .  : ((Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
       . and .  : ((Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] -> Bool)
      →  . and .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
       . or .  : ((Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] -> Bool)
      →  . or .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
       . -> .  : ((Heap[A] → Bool) × (Heap[A] → Bool) → Heap[A] -> Bool)
      →  . -> .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
      ⌜ . ⌝ → ⌜ . ⌝ : (Bool → Map[Ref[A] × A] -> Bool); 
      { . } : (Heap[A] → Heap[A] -> Bool) → { . } : (Map[Ref[A] × A] → Map[Ref[A] × A] -> Bool); 
      ite → ite : (Bool × (Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Map[Ref[A] × A] -> Bool); 
       . => .  →  . => .  : (Ref[A] × A → Map[Ref[A] × A] -> Bool); 
      _∃ .  : ((B → Heap[A] -> Bool) → Heap[A] -> Bool) → _∃ .  : ((B → Map[Ref[A] × A] -> Bool) → Map[Ref[A] × A] -> Bool); 
      _∃ .  : ((B × C → Heap[A] -> Bool) → Heap[A] -> Bool) → _∃ .  : ((B × C → Map[Ref[A] × A] -> Bool) → Map[Ref[A] × A] -> Bool); 
      _∃ .  : ((B × C × D → Heap[A] -> Bool) → Heap[A] -> Bool)
      → _∃ .  : ((B × C × D → Map[Ref[A] × A] -> Bool) → Map[Ref[A] × A] -> Bool); 
       . =>_ →  . =>_ : (Ref[A] → Map[Ref[A] × A] -> Bool); 
       . =>? →  . =>? : (Ref[A] → Map[Ref[A] × A] -> Bool); 
       . ⊆ .  : (Heap[A] × Heap[A] → Bool) →  . ⊆ .  : (Map[Ref[A] × A] × Map[Ref[A] × A] → Bool); 
       . ⊥ .  →  . ⊥ .  : (Map[Ref[A] × A] × Map[Ref[A] × A] → Bool); 
      emp → emp : (Map[Ref[A] × A] → Bool); 
      true : (Heap[A] → Bool) → true : (Map[Ref[A] × A] → Bool); 
      false : (Heap[A] → Bool) → false : (Map[Ref[A] × A] → Bool); 
      precise → precise : ((Map[Ref[A] × A] → Bool) → Bool); 
       . ⊆ .  : ((Heap[A] → Bool) × (Heap[A] → Bool) → Bool) →  . ⊆ .  : ((Map[Ref[A] × A] → Bool) × (Map[Ref[A] × A] → Bool) → Bool); 
       . ≡ .  →  . ≡ .  : (Map[Ref[A] × A] × Map[Ref[A] × A] → Bool); 
end instantiate