This PR adds `num?` parameter to `mkPatternFromTheorem` to control how
many leading quantifiers are stripped when creating a pattern. This
enables matching theorems where only some quantifiers should be
converted to pattern variables.
For example, to match `mk_forall_and : (∀ x, P x) → (∀ x, Q x) → (∀ x, P
x ∧ Q x)` against a goal `∀ x, q x 0 ∧ q (f (f x)) y`, we use
`mkPatternFromTheorem ``mk_forall_and (some 5)` to create the pattern `∀
x, ?P x ∧ ?Q x`, keeping the outermost `∀` in the pattern rather than
converting it to a pattern variable.
4e1a2487b7