Quelle  arrays_examples.prf

(arrays_examples
 (foo1 0 (foo1-1 nil 3569928030 ("" (postpone) nil nil) nil shostak))
 (foo2 0
  (foo2-1 nil 3569928025 ("" (grind) nil nil)
   ((length def-decl "nat" list_props nil)
    (list2finseq const-decl "finseq[T]" list2finseq nil)
    (NS0 const-decl "ArrayOf[10][[nat, string]]" arrays_examples nil)
    (NS1 const-decl "ArrayOf[10][[nat, string]]" arrays_examples nil))
   shostak)))