Case-insensitively test for the existence of a substring.
(isubstrp x y) determines if x ever occurs as a case-insensitive substring of y.
See also substrp for a case-sensitive version.
See also istrpos for an alternative that reports the position of the matched substring.
(defthm iprefixp-when-isubstrp (implies (isubstrp x y) (iprefixp (explode x) (nthcdr (istrpos x y) (explode y)))))
(defthm completeness-of-isubstrp (implies (and (iprefixp (explode x) (nthcdr m (explode y))) (force (natp m))) (isubstrp x y)))
(defthm istreqv-implies-equal-isubstrp-1 (implies (istreqv x x-equiv) (equal (isubstrp x y) (isubstrp x-equiv y))) :rule-classes (:congruence))