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