1; A trivial test 2 3(in-package "ACL2") 4 5(defun foo (x) 6 (cons x x)) 7 8(defthm foo-prop 9 (equal (car (foo x)) 10 x)) 11 12(progn 13 (defun bar (x) 14 (foo x)) 15 (defun h (x) 16 (bar x))) 17