| Search_pat of search_kind * string (* searches with string pattern *)
| Search_term of search_kind * 'term (* searches with term pattern *)
| Proof
| Search_pat of search_kind * string (* searches with string pattern *)
| Search_term of search_kind * 'term (* searches with term pattern *)
| Proof