在引理的結論中搜尋模式

當你知道它的結論應該是什麼時，搜尋一個引理：

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

你還可以搜尋部分結論（結論和一個或幾個最後的假設）。

Coq < Require Import Arith.
Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _).
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p

警告：如果你混淆了假設的順序，你將找不到任何東西：

Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).