Common checkpoints - acl2/acl2 GitHub Wiki
#Some common checkpoints and what they mean
(implies (not (consp x)) (not x))
Add (true-listp x) to your hypotheses.
#Some common checkpoints and what they mean
(implies (not (consp x)) (not x))Add (true-listp x) to your hypotheses.