#192:
(true-listp y) -> (true-listp (cons x y))
<-> {Re: def true-listp}
(true-listp y) -> (if (consp (cons x y))
			(true-listp (cdr (cons x y)))
			(equal (cons x y) nil)))
<-> {Comp.}
(true-listp y) -> (if t
			(true-listp (cdr (cons x y)))
			(equal (cons x y) nil)))
<-> {Re: if-ax1}
(true-listp y) -> (true-listp (cdr (cons x y)))
<-> {Re: cdr-cons axiom}
(true-listp y) -> (true-listp y)
<-> {Hyp}
(true-listp y) -> t
<-> {Re: short-circuit}
t

#196:
((P -> Q) ^ (P -> R)) -> (P -> (Q ^ R))
<-> {Promotion}
((P -> Q) ^ (P -> R) ^ P) -> (Q ^ R)
<-> {Forward Chaining}
(Q ^ R ^ P) -> (Q ^ R)
<-> {Hyp twice}
(Q ^ R ^ P) -> (t ^ t)
<-> {Comp}
(Q ^ R ^ P) -> t
<-> {Short Circuit}
t

#198:
((A -> D) ^ (B -> E) ^ (D -> (E -> C))) -> ((A ^ B) -> C)
<-> {Promotion}
((A -> D) ^ (B -> E) ^ (D -> (E -> C)) ^ (A ^ B)) -> (C)
<-> {Associativity}
((A -> D) ^ (B -> E) ^ (D -> (E -> C)) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ (B -> E) ^ (D -> (E -> C)) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ (B -> E) ^ (E -> C) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ E ^ (E -> C) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ E ^ C ^ A ^ B) -> (C)
<-> {Hyp}
(D ^ E ^ C ^ A ^ B) -> t
<-> {Short Circuit}
t

#205:
(not (consp a)) -> (app (app a b) c) = (app a (app b c))
<-> {Re: def consp}
(not (not (endp a))) -> (app (app a b) c) = (app a (app b c))
<-> {Comp}
(endp a) -> (app (app a b) c) = (app a (app b c))
<-> {Re: def app}
(endp a) -> (if (endp (app a b))
		c
		(cons (car (app a b)) (app (cdr (app a b)) c)))
	    = (app a (app b c))
<-> {Re: def app}
(endp a) -> (if (endp (if (endp a)
				 b
				(cons (car a) (app (cdr a) b)))
		c
		(cons (car (app a b)) (app (cdr (app a b)) c)))
	    = (app a (app b c))
<-> {Hyp}
(endp a) -> (if (endp (if t
				 b
				(cons (car a) (app (cdr a) b)))
		c
		(cons (car (app a b)) (app (cdr (app a b)) c)))
	    = (app a (app b c))
<-> {Re: if-ax1}
(endp a) -> (if (endp b)
		c
		(cons (car (app a b)) (app (cdr (app a b)) c)))
	    = (app a (app b c))
<-> {Re: def app}
(endp a) -> (if (endp b)
		c
		(cons (car (app a b)) (app (cdr (app a b)) c)))
	  = (if (endp a) 
		(app b c)
		(cons (car a) (app (cdr a) (app b c)))
<-> {Hyp}
(endp a) -> (if (endp b)
		c
		(cons (car (app a b)) (app (cdr (app a b)) c)))
	  = (if t 
		(app b c)
		(cons (car a) (app (cdr a) (app b c)))
<-> {Re: if-ax1}
(endp a) -> (if (endp b)
		c
		(cons (car (app a b)) (app (cdr (app a b)) c)))
	  = (app b c)
<-> {Re: def app}
(endp a) -> (if (endp b)
		c
		(cons (car (if (endp a)
				 b
				(cons (car a) (app (cdr a) b))))) (app (cdr (app a b)) c)))
	  = (app b c)
		
<-> {Hyp}
(endp a) -> (if (endp b)
		c
		(cons (car (if t
				 b
				(cons (car a) (app (cdr a) b))))) (app (cdr (app a b)) c)))
	  = (app b c)
<-> {Re: if-ax1} 
(endp a) -> (if (endp b)
		c
		(cons (car b) (app (cdr (app a b)) c)))
	  = (app b c)
<-> {Re: def app}
(endp a) -> (if (endp b)
		c
		(cons (car b) (app (cdr (if (endp a)
						 b
						(cons (car a) (app (cdr a) b)))) c)))
	  = (app b c)
<-> {Hyp}
(endp a) -> (if (endp b)
		c
		(cons (car b) (app (cdr (if t
						 b
						(cons (car a) (app (cdr a) b)))) c)))
	  = (app b c)
<-> {Re: if-ax1}
(endp a) -> (if (endp b)
		c
		(cons (car b) (app (cdr b) c)))
	  = (app b c)
<-> {Re: def app}
(endp a) -> (if (endp b)
		c
		(cons (car b) (app (cdr b) c)))
	  = (if (endp b)
		c
		(cons (car b) (app (cdr b) c)))
<-> {Equal-reflexive}
(endp a) -> t
<-> {Short circuit}
t

#206:
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(app (app a b) c) = (app a (app b c))

<-> {Re: def app}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(app (if (not (consp a))
	  b
	  (cons (car a) (app (cdr a) b))) c) 
= 
(app a (app b c))

<-> {Hyp}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(app (if nil
	  b
	  (cons (car a) (app (cdr a) b))) c) 
= 
(app a (app b c))

<-> {Re: if-ax2}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(app (cons (car a) (app (cdr a) b)) c) 
= 
(app a (app b c))

<-> {Re: def app}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(app (cons (car a) (app (cdr a) b)) c) 
= 
(if (not (consp a))
    (app b c)
    (cons (car a) (app (cdr a) (app b c))))

<-> {Hyp}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(app (cons (car a) (app (cdr a) b)) c) 
= 
(if nil
    (app b c)
    (cons (car a) (app (cdr a) (app b c))))

<-> {Re: if-ax2}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(app (cons (car a) (app (cdr a) b)) c) 
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: def app}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(if (not (consp (cons (car a) (app (cdr a) b)))) 
     c 
     (cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c)))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: consp-cons}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(if nil 
     c 
     (cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c)))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: if-ax2}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c)))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: car-cons}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(cons (car a) (app (cdr (cons (car a) (app (cdr a) b))) c))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: cdr-cons}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(cons (car a) (app (app (cdr a) b) c))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Hyp}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
(cons (car a) (app (cdr a) (app b c)))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Equal-reflexive}

((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
-> 
t

<-> {Short Circuit}
t


#214: (app-associative)
(app (app a b) c) = (app a (app b c))
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case: 
(not (consp a)) -> (app (app a b) c) = (app a (app b c))

<-> {Re: Def app}

(not (consp a)) 
-> 
(app (if (not (consp a))
	  b
	  (cons (car a) (app (cdr a) b))) 
      c) 
= 
(app a (app b c))

<-> {Hyp & Re: if-ax1}

(not (consp a)) 
-> 
(app b c) 
= 
(app a (app b c))

<-> {Re: def app}

(not (consp a)) 
-> 
(app b c) 
= 
(if (not (consp a))
    (app b c)
    (cons (car a) (app (cdr a) (app b c))))

<-> {Hyp & Re: if-ax1}

(not (consp a)) 
-> 
(app b c) 
= 
(app b c)

<-> {Equal-reflexive}

(not (consp a)) 
-> 
t

<-> {Short Circuit}
t

4. Induction Step
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (app a b) c) = (app a (app b c))

<-> {Re: def app twice}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (if (not (consp a))
	b
	(cons (car a) (app (cdr a) b))) 
      c) 
= 
(if (not (consp a))
    (app b c)
    (cons (car a) (app (cdr a) (app b c))))

<-> {Hyp & Re: if-ax2 Twice}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (cons (car a) (app (cdr a) b)) c) 
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: def app}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(if (not (consp (cons (car a) (app (cdr a) b))))
     c
    (cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: consp-cons & if-ax2}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: car-cons}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (cdr (cons (car a) (app (cdr a) b))) c))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Re: cdr-cons}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (app (cdr a) b) c))
= 
(cons (car a) (app (cdr a) (app b c)))

<-> {Hyp}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (app (cdr a) b) c))
= 
(cons (car a) (app (app (cdr a) b) c))

<-> {Equal-reflexive}

(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
t

<-> {Short Circuit}
t

Q.E.D.

#216: (mapnil-app)
(mapnil (app a b)) = (app (mapnil a) (mapnil b))
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case: 
(not (consp a)) -> (mapnil (app a b)) = (app (mapnil a) (mapnil b))

<-> {Re: def app}

(not (consp a)) 
-> 
(mapnil (if (not (consp a))
	     b 
	    (cons (car a) (app (cdr a) b))))
= 
(app (mapnil a) (mapnil b))

<-> {Hyp & Re: if-ax1}

(not (consp a)) 
-> 
(mapnil b)
= 
(app (mapnil a) (mapnil b))

<-> {Re: def mapnil}

(not (consp a)) 
-> 
(mapnil b)
= 
(app (if (endp a)
	 nil
	 (cons nil (mapnil (cdr x))))
     (mapnil b))

<-> {Re: def endp & if-ax1}

(not (consp a)) 
-> 
(mapnil b)
= 
(app nil (mapnil b))

<-> {Re: def app}

(not (consp a)) 
-> 
(mapnil b)
= 
(if (not (consp nil))
    (mapnil b)
    (cons (car nil) (app (cdr nil) (mapnil b))))

<-> {Comp}

(not (consp a)) 
-> 
(mapnil b)
= 
(if t
    (mapnil b)
    (cons (car nil) (app (cdr nil) (mapnil b))))

<-> {Re: if-ax1}

(not (consp a)) 
-> 
(mapnil b)
= 
(mapnil b)

<-> {Equal-reflexive}

(not (consp a)) 
-> 
t

<-> {Short circuit}
t

4. Induction Step
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(mapnil (app a b)) = (app (mapnil a) (mapnil b))

<-> {Re: def app}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(mapnil (if (not (consp a))
	     b
	    (cons (car a) (app (cdr a) b)))
=
(app (mapnil a) (mapnil b))

<-> {Hyp & Re: if-ax2}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(mapnil (cons (car a) (app (cdr a) b)))
=
(app (mapnil a) (mapnil b))

<-> {Re: def mapnil}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(if (endp (cons (car a) (app (cdr a) b)))
    nil
    (cons nil (mapnil (cdr (cons (car a) (app (cdr a) b))))))
=
(app (mapnil a) (mapnil b))

<-> {Re: def endp}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(if (not (consp (cons (car a) (app (cdr a) b))))
    nil
    (cons nil (mapnil (cdr (cons (car a) (app (cdr a) b))))))
=
(app (mapnil a) (mapnil b))

<-> {Re: consp-cons & if-ax2}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (cdr (cons (car a) (app (cdr a) b)))))
=
(app (mapnil a) (mapnil b))

<-> {Re: cdr-cons}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(app (mapnil a) (mapnil b))

<-> {Re: def mapnil & def endp}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(app (if (not (consp a))
	  nil
	  (cons nil (mapnil (cdr a))))
     (mapnil b))

<-> {Hyp & Re: if-ax2}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(app (cons nil (mapnil (cdr a))) (mapnil b))

<-> {Re: def app}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(if (not (consp (cons nil (mapnil (cdr a)))))
    (mapnil b)
    (cons (car (cons nil (mapnil (cdr a)))) (mapnil b)))

<-> {Re: consp-cons & if-ax2}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(cons (car (cons nil (mapnil (cdr a)))) (mapnil b)))

<-> {Re: car-cons}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(cons nil (mapnil b))

<-> {Hyp}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (app (mapnil (cdr a)) (mapnil b)))
=
(cons nil (mapnil b))

<-> {Re: def app}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (if (not (consp (mapnil (cdr a))))
		    (mapnil b)
		    (cons (car (mapnil (cdr a))) (app (cdr (mapnil (cdr a))) (mapnil b)))))
=
(cons nil (mapnil b))

<-> {Hyp & Re: if-ax1}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil b))
=
(cons nil (mapnil b))

<-> {Equal-reflexive}

(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
t

<-> {Short circuit}
t

#217: (mapnil-rev)
(rev (mapnil a)) = (mapnil (rev a))
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case: 
(not (consp a)) -> (rev (mapnil a)) = (mapnil (rev a))

<-> {Re: def mapnil & def endp}

(not (consp a))
->
(rev (if (not (consp a))
	 nil
	 (cons nil (mapnil (cdr a)))))
=
(mapnil (rev a))

<-> {Hyp & Re: if-ax1}

(not (consp a))
->
(rev nil)
=
(mapnil (rev a))

<-> {Re: def rev & def endp}

(not (consp a))
->
(rev nil)
=
(mapnil (if (not (consp a))
	    nil
	    (app (rev (cdr x)) (cons (car x) nil))))

<-> {Hyp & Re: if-ax1}

(not (consp a))
->
(rev nil)
=
(mapnil nil)

<-> {Re: def mapnil}

(not (consp a))
->
(rev nil)
=
(if (endp nil)
    nil
    (cons nil (mapnil (cdr nil))))

<-> {Comp & if-ax1}

(not (consp a))
->
(rev nil)
=
nil

<-> {Re: def rev}

(not (consp a))
->
(if (endp nil)
    nil
    (app (rev (cdr nil)) (cons (car nil) nil)))
=
nil

<-> {Comp & Re: if-ax1}

(not (consp a))
->
nil
=
nil

<-> {Equal-reflexive}

(not (consp a))
->
t

<-> {Short Circuit}
t

4. Induction Step
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(rev (mapnil a)) = (mapnil (rev a))

<-> {Re: def mapnil & def endp}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(rev (if (not (consp a))
	  nil
	  (cons nil (mapnil (cdr a))))
=
(mapnil (rev a))

<-> {Hyp & Re: if-ax2}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(rev (cons nil (mapnil (cdr a))))
=
(mapnil (rev a))

<-> {Re: def rev & def endp}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(rev (cons nil (mapnil (cdr a))))
=
(mapnil (if (not (consp a))
	    nil
	    (app (rev (cdr a)) (cons (car a) nil))))

<-> {Hyp & Re: if-ax2}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(rev (cons nil (mapnil (cdr a))))
=
(mapnil (app (rev (cdr a)) (cons (car a) nil)))

<-> {Re: def rev}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(if (not (consp (cons nil (mapnil (cdr a)))))
    nil
    (app (rev (cdr (cons nil (mapnil (cdr a))))) (cons (car (cons nil (mapnil (cdr a)))) nil)))
=
(mapnil (app (rev (cdr a)) (cons (car a) nil)))

<-> {Re: consp-cons & if-ax2}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (rev (cdr (cons nil (mapnil (cdr a))))) (cons (car (cons nil (mapnil (cdr a)))) nil))
=
(mapnil (app (rev (cdr a)) (cons (car a) nil)))

<-> {Re: q216 mapnil-app}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (rev (cdr (cons nil (mapnil (cdr a))))) (cons (car (cons nil (mapnil (cdr a)))) nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))

<-> {Re: cdr-cons}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (rev (mapnil (cdr a))) (cons (car (cons nil (mapnil (cdr a)))) nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))

<-> {Re: car-cons}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (rev (mapnil (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))

<-> {Hyp}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))

<-> {Re: def mapnil & def endp}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (if (not (consp (cons (car a) nil)))
				nil
				(cons nil (mapnil (cdr x)))))

<-> {Re: consp-cons & if-ax2}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (cons nil (mapnil (cdr x))))

<-> {Comp}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (cons nil nil))

<-> {Equal-reflexive}

(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
-> 
t

<-> {Short Circuit}
t

Q.E.D.

#218: (rev-rev)
(true-listp a) -> (rev (rev a)) = a
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case: 
(not (consp a)) -> ((true-listp a) -> (rev (rev a)) = a)

<-> {Re: def rev & def endp}

(not (consp a)) -> ((true-listp a)
-> 
(rev (if (not (consp a))
	  nil
	  (app (rev (cdr x)) (cons (car x) nil))))
= 
a

<-> {Hyp & Re: if-ax1}

(not (consp a)) -> ((true-listp a)
-> 
(rev nil)
= 
a

<-> {Re: def rev & def endp}

(not (consp a)) -> ((true-listp a)
-> 
(if (not (consp nil))
    nil
    (app (rev (cdr x)) (cons (car x) nil)))
= 
a

<-> {Comp & Re: if-ax1}

(not (consp a)) -> ((true-listp a)
-> 
nil
= 
a

<-> {Re: def true-listp}

(not (consp a)) -> (if (consp a)
			(true-listp (cdr a))
			(equal a nil))
-> 
nil
= 
a

<-> {Hyp & Re: if-ax2}

(not (consp a)) -> (equal a nil)
-> 
nil
= 
a

<-> {Hyp}

(not (consp a)) -> (equal a nil)
-> 
t

<-> {Short-circuit}
t

4. Induction Step
(consp a) ^ ((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
((true-listp a) -> (rev (rev a)) = a)

<-> {Re: def rev & def endp}

(consp a) ^ ((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
((true-listp a) 
-> 
(rev (if (not (consp a))
	 nil
	 (app (rev (cdr a)) (cons (car a) nil))))
=
a

<-> {Promotion}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(rev (if (not (consp a))
	 nil
	 (app (rev (cdr a)) (cons (car a) nil))))
=
a

<-> {Hyp & Re: if-ax2}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(rev (app (rev (cdr a)) (cons (car a) nil)))
=
a

<-> {Re: Q219 rev-app}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (rev (cons (car a) nil)) (rev (rev (cdr a))))
=
a

<-> {Hyp}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (rev (cons (car a) nil)) (cdr a))
=
a

<-> {Re: def rev & def endp}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app ((if (not (consp (cons (car a) nil))))
	  nil
	  (app (rev (cdr (cons (car a) nil))) (cons (car (cons (car a) nil)) nil)))
     (cdr a))
=
a

<-> {Re: consp-cons & if-ax2}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (app (rev (cdr (cons (car a) nil))) (cons (car (cons (car a) nil)) nil))
     (cdr a))
=
a

<-> {Re: cdr-cons}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (app (rev nil) (cons (car (cons (car a) nil)) nil))
     (cdr a))
=
a

<-> {Re: car-cons}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (app (rev nil) (cons (car a) nil))
     (cdr a))
=
a

<-> {Re: def rev & def endp}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (app (if (not (consp nil))
	      nil	
	      (app (rev (cdr nil)) (cons (car nil) nil)))
	  (cons (car a) nil))
     (cdr a))
=
a

<-> {Comp & Re: if-ax1}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (app nil (cons (car a) nil))
     (cdr a))
=
a

<-> {Re: def app & def endp}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (if (not (consp nil))
	 (cons (car a) nil)
	 (cons (car nil) (app (cdr nil) (cons (car a) nil))))
(cdr a))
=
a

<-> {Comp & Re: if-ax1}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(app (cons (car a) nil) (cdr a))
=
a

<-> {Re: def app & def endp}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(if (not (consp (cons (car a) nil)))
    (cdr a)
    (cons (car (cons (car a) nil)) (app (cdr (cons (car a) nil)) (cdr a))))
=
a

<-> {Re: consp-cons & if-ax2}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(cons (car (cons (car a) nil)) (app (cdr (cons (car a) nil)) (cdr a)))
=
a

<-> {Re: car-cons}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(cons (car a) (app (cdr (cons (car a) nil)) (cdr a)))
=
a

<-> {Re: cdr-cons}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(cons (car a) (app nil (cdr a)))
=
a

<-> {Re: def app & def endp}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(cons (car a) (if (not (consp nil))
		  (cdr a)
		  (cons (car nil) (app (cdr nil) (cdr a)))))
=
a

<-> {Comp & Re: if-ax1}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
(cons (car a) (cdr a))
=
a

<-> {Re: cons-car-cdr axiom}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
a
=
a

<-> {Equal-reflexive}

(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
-> 
t

<-> {Short Circuit}
t

Q.E.D.

#220: (mem-app)
(mem e (app a b)) <-> ((mem e a) | (mem e b))
lemma: (x <-> x) ; due to equal-reflexive, anything is iff equivalent to itself.
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case: 
(not (consp a)) -> 
((mem e (app a b)) 
<-> 
((mem e a) | (mem e b)))

<-> {Re: def app & def endp}

(not (consp a)) -> 
((mem e (if (not (consp a)
	     b
	     (cons (car a) (app (cdr a) b))))
<-> 
((mem e a) | (mem e b)))

<-> {Hyp & Re: if-ax1}

(not (consp a)) -> 
(mem e b)
<-> 
((mem e a) | (mem e b)))

<-> {Re: def mem & def endp}

(not (consp a)) -> 
(mem e b)
<-> 
((if (not (consp a))
      nil
      (if (equal x (car y))
	   t
	   (mem x (cdr y)))) | (mem e b))

<-> {Hyp & Re: if-ax1}

(not (consp a)) -> 
(mem e b)
<-> 
(nil | (mem e b))

<-> {Short Circuit}

(not (consp a)) -> 
(mem e b)
<-> 
(mem e b)

<-> {Re: def lemma}
(not (consp a)) -> t

<-> {Short Circuit}
t

4. Induction Step
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
((mem e (app a b)) 
<-> 
((mem e a) | (mem e b))

<-> {Re: def app & def endp}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
((mem e (if (not (consp a))
	     b
	     (cons (car a) (app (cdr a) b)))
<-> 
((mem e a) | (mem e b))

<-> {Hyp & Re: if-ax2}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(mem e (cons (car a) (app (cdr a) b)))
<-> 
((mem e a) | (mem e b))

<-> {Re: def mem & def endp}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(if (not (consp (cons (car a) (app (cdr a) b))))
    nil
    (if (equal e (car (cons (car a) (app (cdr a) b))))
	 t
	 (mem e (cdr (cons (car a) (app (cdr a) b))))))
<-> 
((mem e a) | (mem e b))

<-> {Re: consp-cons & if-ax2}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(if (equal e (car (cons (car a) (app (cdr a) b))))
    t
    (mem e (cdr (cons (car a) (app (cdr a) b)))))
<-> 
((mem e a) | (mem e b))

<-> {Re: cdr-cons}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(if (equal e (car (cons (car a) (app (cdr a) b))))
    t
    (mem e (app (cdr a) b)))
<-> 
((mem e a) | (mem e b))

<-> {Re: car-cons}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(if (equal e (car a))
    t
    (mem e (app (cdr a) b)))
<-> 
((mem e a) | (mem e b))

<-> {Re: def mem & def endp}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(if (equal e (car a))
    t
    (mem e (app (cdr a) b)))
<-> 
(if (not (consp a))
    nil
    (if (equal e (car a))
	t
	(mem e (cdr a)))) | (mem e b)

<-> {Hyp & Re: if-ax2}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(if (equal e (car a))
    t
    (mem e (app (cdr a) b)))
<-> 
(if (equal e (car a))
	t
	(mem e (cdr a))) | (mem e b)

<-> {Hyp}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
(if (equal e (car a))
    t
    (mem e (app (cdr a) b)))
<-> 
(if (equal e (car a))
    t
    (mem e (app (cdr a) b)))

<-> {Re: def lemma}

(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
-> 
t

<-> {Short Circuit}
t

Q.E.D.