fix(library_search): find id (#2414)
Previously `library_search` could not find theorems that did not have a head symbol (e.g. were function types with source and target both "variables all the way down"). Now it can, so it solves:
```lean
example (α : Prop) : α → α :=
by library_search -- says: `exact id`
example (p : Prop) [decidable p] : (¬¬p) → p :=
by library_search -- says: `exact not_not.mp`
example (a b : Prop) (h : a ∧ b) : a :=
by library_search -- says: `exact h.left`
example (P Q : Prop) [decidable P] [decidable Q]: (¬ Q → ¬ P) → (P → Q) :=
by library_search -- says: `exact not_imp_not.mp`
```
