搜索模式

在假设或结论中搜索涉及模式的所有事实：

Coq < Search (_ + O).
plus_n_O: forall n : nat, n = n + 0

_ 字符用作通配符，可以多次使用：

Coq < Search (S _ <= _).
le_S_n: forall n m : nat, S n <= S m -> n <= m
le_n_S: forall n m : nat, n <= m -> S n <= S m

你还可以搜索非线性模式：

Coq < Search (?x <= ?x).
le_n: forall n : nat, n <= n