(in-package "ACL2")

(include-book "standard-52-card-deck")