Coq to Why3: с обозначениями

Question

В Coq у меня есть следующий код:

      Fixpoint executeBool (state:M.t Z) (stack:list Z) (program:list insStBool) {struct program} : list Z :=
  match program with 
    ...
    | (SBSkip (S n))::l => executeBool_skip n state stack l
  end
  with executeBool_skip (n:nat) (state:M.t Z) (stack:list Z) (program:list insStBool) : list Z :=
    match program with
    ...
    end.

Как я могу использовать эту нотацию для написания этого кода в Why3? Я знаю, что мне тоже нужно переписать код, но я ничего не могу найти на with обозначение (и я не могу определить executeBool_skip отдельно, потому что он использует executeBool и наоборот).

Спасибо!