When an argument is declared to be single-threaded the guard of the function is augmented by conjoining to it the condition that the argument satisfy the recognizer for the single-threaded object.
The syntactic checks done to enforce the legal use of single-threaded objects are also sufficient to allow these guard conjuncts to be automatically proved.