Estoy tratando de escribir el colador de Eratóstenes en Coq. Tengo una funcióncrossout : forall {n:nat}, vector bool n -> nat -> vector bool n. Cuando el tamiz encuentra un número que es primo, usacrossout para marcar todos los números que no son primos y luego se repiten en el vector resultante. Obviamente, el tamiz no puede ser estructuralmente recursivo en el propio vector, pero es estructuralmente recursivo en la longitud del vector. Lo que quiero es hacer algo como esto:

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.

Pero si lo escribo así, Coq se queja de que la longitud dev' no es un subtermico den. Sé que lo es, pero no importa cómo estructure la función, parece que no puedo convencer a Coq de que lo es. ¿Alguien sabe como puedo?