(defun removeequiv(x) (if (atom x) x (if (= (length x) 3) (if (eq (second x) 'equivalent) (list (list (removeequiv (first x)) 'implies (removeequiv (third x))) 'and (list (removeequiv (third x)) 'implies (removeequiv (first x))) ) (list (removeequiv (first x)) (second x) (removeequiv (third x)) ) ) (if (= (length x) 2) (list (first x) (removeequiv (second x))) (list (removeequiv (first x))) ) ) ) )