The call type(a, verification) checks to see if a is a valid verification expression. By definition, a verification expression is any expression a for which the commands verify(expr1, expr2, boolean(a)) and (with appropriate arguments) verify(expr1, expr2, a) could succeed.

$\mathrm{type}\left(\mathrm{set}\,\mathrm{verification}\right)$

$\mathrm{true}$

$\mathrm{verify}\left(\left\{a\,b\right\}\,\left\{a\,b\,c\right\}\,\mathrm{set}\right)$

$\mathrm{false}$

$\mathrm{verify}\left(\left\{a\,b\,c\right\}\,\left\{a\,b\,c\right\}\,\mathrm{set}\right)$

$\mathrm{true}$

$\mathrm{type}\left(\mathrm{list}\left(\mathrm{expand}\right)\,\mathrm{verification}\right)$

$\mathrm{true}$

$\mathrm{verify}\left(\left[a\,b\,x\left(x-1\right)\right]\,\left[a\,b\,x^2-x\right]\,\mathrm{list}\left(\mathrm{expand}\right)\right)$

$\mathrm{true}$

$\mathrm{myver}≔\neg \mathrm{set}\wedge \mathrm{`subset`}$

$\mathrm{myver}≔\neg \mathrm{set}\wedge \mathrm{subset}$

$\mathrm{type}\left(\mathrm{myver}\,\mathrm{verification}\right)$

$\mathrm{true}$

$\mathrm{verify}\left(\left\{a\,b\right\}\,\left\{a\,b\,c\right\}\,\mathrm{myver}\right)$

$\mathrm{true}$

$\mathrm{verify}\left(\left\{a\,b\,c\right\}\,\left\{a\,b\,c\right\}\,\mathrm{myver}\right)$

$\mathrm{false}$