SearchAbout and.
(* Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)