(aver (eq check :simple))
;; If the proven type is a subtype of the possibly
;; weakened type check then it's always true and is
(aver (eq check :simple))
;; If the proven type is a subtype of the possibly
;; weakened type check then it's always true and is