(atj-type-to-pred-gen-mono-thms-2 subs sups) → *
Function:
(defun atj-type-to-pred-gen-mono-thms-2 (subs sups) (declare (xargs :guard (and (atj-type-listp subs) (atj-type-listp sups)))) (let ((__function__ 'atj-type-to-pred-gen-mono-thms-2)) (declare (ignorable __function__)) (cond ((endp subs) nil) (t (append (atj-type-to-pred-gen-mono-thms-1 (car subs) sups) (atj-type-to-pred-gen-mono-thms-2 (cdr subs) sups))))))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-of-atj-type-list-fix-subs (equal (atj-type-to-pred-gen-mono-thms-2 (atj-type-list-fix subs) sups) (atj-type-to-pred-gen-mono-thms-2 subs sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-atj-type-list-equiv-congruence-on-subs (implies (atj-type-list-equiv subs subs-equiv) (equal (atj-type-to-pred-gen-mono-thms-2 subs sups) (atj-type-to-pred-gen-mono-thms-2 subs-equiv sups))) :rule-classes :congruence)
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-of-atj-type-list-fix-sups (equal (atj-type-to-pred-gen-mono-thms-2 subs (atj-type-list-fix sups)) (atj-type-to-pred-gen-mono-thms-2 subs sups)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thms-2-atj-type-list-equiv-congruence-on-sups (implies (atj-type-list-equiv sups sups-equiv) (equal (atj-type-to-pred-gen-mono-thms-2 subs sups) (atj-type-to-pred-gen-mono-thms-2 subs sups-equiv))) :rule-classes :congruence)