chk-length-and-keys

other

(in-package "ACL2")

keyword-value-listp-when-not-mv-nth-0-of-chk-length-and-keystheorem

(defthm keyword-value-listp-when-not-mv-nth-0-of-chk-length-and-keys
  (implies (and (not (mv-nth 0 (chk-length-and-keys actuals form wrld)))
      (true-listp actuals))
    (keyword-value-listp actuals))
  :hints (("Goal" :in-theory (enable chk-length-and-keys keyword-value-listp))))