``` val a : type. val p : a -> prop. val y : a. goal ((fun (x : a) . x asserting p x) y) = y. ``` throws ``` Error: monomorphization: invalid problem: could not find `p` in new graph ```