Why3: Как проверить список

Question

У меня есть следующий тест, но я не уверен, как работает синтаксис why3 для списков goals, может кто поможет?

      goal Testexecute :
(* execute (list int) (list instruction (SPush)) *)
    execute [(Econst 42),(Econst 21)] [SPush 2] = [(Econst 2),(Econst 42),(Econst 21)]
end

Спасибо!