Estou tentando escrever a peneira de Eratóstenes na Coq. Eu tenho uma funçãocrossout : forall {n:nat}, vector bool n -> nat -> vector bool n. Quando a peneira encontra um número que é primo, ele usacrossout para marcar todos os números que não são primos e depois recorre ao vetor resultante. A peneira obviamente não pode ser estruturalmente recursiva no próprio vetor, mas é estruturalmente recursiva no comprimento do vetor. O que eu quero é fazer algo assim:

Fixpoint sieve {n:nat} (v:vector bool n) (acc:nat) {struct n} : list nat :=
  match v with
    | [] => Datatypes.nil
    | false :: v' => sieve v' (S acc)
    | true :: v' => Datatypes.cons acc (sieve (crossout v' acc) (S acc))
  end.

Mas se eu escrevo assim, Coq reclama que o comprimento dev' não é um subterfúgion. Eu sei que é, mas não importa como eu estruturo a função, não consigo convencer Coq de que é. Alguém sabe como eu posso?