Function:
(defun atj-type-to-pred-gen-mono-thm (sub sup) (declare (xargs :guard (and (atj-typep sub) (atj-typep sup)))) (let ((__function__ 'atj-type-to-pred-gen-mono-thm)) (declare (ignorable __function__)) (if (atj-type-<= sub sup) (cons (cons 'defthm (cons (packn (list 'atj-type-to-pred-thm- (atj-type-to-keyword sub) '- (atj-type-to-keyword sup))) (cons (cons 'implies (cons (cons (atj-type-to-pred sub) '(val)) (cons (cons (atj-type-to-pred sup) '(val)) 'nil))) '(:rule-classes nil)))) 'nil) nil)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-of-atj-type-fix-sub (equal (atj-type-to-pred-gen-mono-thm (atj-type-fix sub) sup) (atj-type-to-pred-gen-mono-thm sub sup)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-atj-type-equiv-congruence-on-sub (implies (atj-type-equiv sub sub-equiv) (equal (atj-type-to-pred-gen-mono-thm sub sup) (atj-type-to-pred-gen-mono-thm sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-of-atj-type-fix-sup (equal (atj-type-to-pred-gen-mono-thm sub (atj-type-fix sup)) (atj-type-to-pred-gen-mono-thm sub sup)))
Theorem:
(defthm atj-type-to-pred-gen-mono-thm-atj-type-equiv-congruence-on-sup (implies (atj-type-equiv sup sup-equiv) (equal (atj-type-to-pred-gen-mono-thm sub sup) (atj-type-to-pred-gen-mono-thm sub sup-equiv))) :rule-classes :congruence)