(defun memb (e x)
  (if (endp x)
      nil
      (if (equal e (car x))
          t
          (memb e (cdr x)))))

(defun ap (x y)
  (if (endp x)
      y
      (cons (car x)
            (ap (cdr x) y))))

(defun rm! (e x)
  (if (endp x)
      nil
      (if (equal e (car x))
          (rm! e (cdr x))
          (cons (car x)
                (rm! e (cdr x))))))

(defun set-equal (x y)
  (if (endp x)
      (endp y)
      (and (memb (car x) y)
           (set-equal (rm! (car x) (cdr x))
                      (rm! (car x) y)))))

(defthm memb-rm!
  (equal (memb e (rm! d x))
         (if (equal e d)
             nil
             (memb e x))))

#|
(defthm memb-rm!-fact1
  (implies (equal e d)
           (not (memb e (rm! d x)))))

(defthm memb-rm!-fact2
  (implies (not (equal e d))
           (equal (memb e (rm! d x))
                  (memb e x))))
|#

(defthm set-equal-prop1
  (implies (set-equal x y)
           (iff (memb e x)
                (memb e y))))

; -----------------------------------------------------------------
; This is easily proved:
(thm (equal (ap (ap a b) c) (ap a (ap b c))))

; This is is "impossible" to prove by induction:
(thm (equal (ap (ap a a) a) (ap a (ap a a))))

; This can be easily proved:
(thm (equal (ap (ap a b) b) (ap a (ap b b))))
; -----------------------------------------------------------------


(defun subset (x y)
  (if (endp x)
      t
      (and (memb (car x) y)
           (subset (cdr x) y))))

(defthm rm!-ap
  (equal (rm! e (ap a b))
         (ap (rm! e a)
             (rm! e b))))

(defthm subset-rm!
  (implies (subset x y)
           (subset (rm! e x)
                   (rm! e y))))

;-----------------------------------------------------------------

(i-am-here)

*** Key checkpoint under a top-level induction: ***

Subgoal *1/3.1'
(IMPLIES (AND (CONSP A)
              (NOT (MEMB (CAR A) B))
              (SUBSET B A))
         (SET-EQUAL (AP (RM! (CAR A) (CDR A))
                        (RM! (CAR A) B))
                    (RM! (CAR A) (CDR A))))

;-----------------------------------------------------------------


(defthm car-ap
  (equal (car (ap a b))
         (if (endp a)
             (car b)
             (car a))))

(defthm cdr-ap
  (equal (cdr (ap a b))
         (if (endp a)
             (cdr b)
             (ap (cdr a) b))))

(defthm set-equal-prop2-lemma
  (implies (subset b a)
           (set-equal (ap a b) a))
  :hints
  (("Goal" :induct (set-equal a b))
   ("Subgoal *1/2''"
    :use (:instance subset-rm!
                    (x b)
                    (y a)
                    (e (car a))))
   ("Subgoal *1/3'" :expand ((SET-EQUAL (AP A B) A)))))
   
(defthm set-equal-prop2
  (set-equal (ap a a) a))