Проблема в том, что @List.filter nat ожидает функцию типа nat -> bool, но вы предоставили функцию типа nat -> Prop. Здесь @List.filter nat - это List.filter, примененное к аргументу типа nat. Одно из различий между bool и Prop состоит в том, что bool разрешимо, а Prop нет: существуют предложения P, такие, что ни P, ни ~P не известны; всегда можно определить, является ли что-то true или false.
Чтобы разрешить эту ситуацию, вам нужно написать функцию типа nat -> bool, которая возвращает true при применении к аргументу чем 7 и false в противном случае. Вы можете воспользоваться тем, что стандартная библиотека определяет логические функции сравнения над натуральными числами. Я бы также предложил прочитать первый том Software Foundations , чтобы ознакомиться с Coq. Он более доступен и легок в обращении, чем некоторые другие выдающиеся введения (он использовался в курсе проверки программ в моем университете, который предполагал небольшой опыт функционального программирования).
Вот минимальный пример, использующий только встроенный тип списка и обозначения:
Require Import Coq.Lists.List.
Import ListNotations.
Fixpoint filterb {A : Type} (f : A -> bool) (xs : list A) : list A :=
match xs with
| [] => []
| x :: xs => if f x then x :: filterb f xs else filterb f xs
end.
Fixpoint ltb (n m : nat) : bool :=
match n, m with
| n , 0 => false
| 0 , S m => true
| S n, S m => ltb n m
end.
Eval compute in (filterb (fun n => ltb 7 n) [5;6;7;8;9]).
(* = [8;9] *)