blob: e597cd29516ea76daf34d72cc6d78069da08ed45 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(*
Example proof script for ACL2 Proof General.
$Id$
*)
(defthm assoc->assoc-equal
(equal (assoc x a)
(assoc-equal x a)))
(defthm assoc->assoc-equal
(equal (assoc x a)
(assoc-equal x a)))
|