instantiate parameter
   olist-act
< 
   olist-min-max
with 
   oarray
   
by mapping
      : List → Array; 
      [] → []; 
       . + .  : (Elem × List → List) →  . + .  : (Elem × Array → Array); 
      # .  → # . ; 
       . ' →  . '; 
       . + .  : (List × List → List) →  . + .  : (Array × Array → Array); 
       . + .  : (List × Elem → List) →  . + .  : (Array × Elem → Array); 
       . +2 .  →  . +2 . ; 
       . ++ .  →  . ++ . ; 
      rmdup → rmdup; 
      rev → rev; 
      mklist → mklist; 
      fillfirst → fillfirst; 
       . -l .  →  . -l . ; 
       . -1l .  →  . -1l . ; 
       . -p .  →  . -p . ; 
      pos → pos; 
      frome → frome; 
       . ∪ .  →  . ∪ . ; 
       . \ .  →  . \ . ; 
      filter : (List × List → List) → filter : (Array × Array → Array); 
      #oc → #oc; 
       . < .  : (List × List → Bool) →  . < .  : (Array × Array → Bool); 
       . ∈ .  →  . ∈ . ; 
      dups → dups; 
      disj → disj; 
       . ⊑ .  →  . ⊑ . ; 
       . ⊒ .  →  . ⊒ . ; 
       . ⊆ .  →  . ⊆ . ; 
      perm → perm; 
       . ⊆m .  →  . ⊆m . ; 
       . head →  . first; 
       . tail →  . rest; 
       . ( . )  →  . ( . ) ; 
       . (. := .)  →  . (. := .) ; 
       . last →  . last; 
       . butlast →  . butlast; 
      butlastn → butlastn; 
      firstn → firstn; 
      restn → restn; 
      lastn → lastn; 
      sublist → sublist; 
   rename 
      ins≤ → ins≤; 
      merge → merge; 
      sort → sort; 
      count : (List × (Elem → Bool) → Nat) → count : (Array × (Elem → Bool) → Nat); 
      filter : (List × (Elem → Bool) → List) → filter : (Array × (Elem → Bool) → Array); 
      ordered≤ → ordered≤; 
      ordered< → ordered<; 
      all< : (List × Elem → Bool) → all< : (Array × Elem → Bool); 
      all< : (List × Nat × Nat × Elem → Bool) → all< : (Array × Nat × Nat × Elem → Bool); 
      all≤ : (List × Elem → Bool) → all≤ : (Array × Elem → Bool); 
      all≤ : (List × Nat × Nat × Elem → Bool) → all≤ : (Array × Nat × Nat × Elem → Bool); 
      all> : (List × Elem → Bool) → all> : (Array × Elem → Bool); 
      all> : (List × Nat × Nat × Elem → Bool) → all> : (Array × Nat × Nat × Elem → Bool); 
      all≥ : (List × Elem → Bool) → all≥ : (Array × Elem → Bool); 
      all≥ : (List × Nat × Nat × Elem → Bool) → all≥ : (Array × Nat × Nat × Elem → Bool); 
      count : (List × Nat × Nat × (Elem → Bool) → Nat) → count : (Array × Nat × Nat × (Elem → Bool) → Nat); 
      min : (List → Elem) → min : (Array → Elem); 
      max : (List → Elem) → max : (Array → Elem); 
end instantiate