$($definec in $($a :all x :tl$)$ :bool

$($and $($consp x$)$

$($or $(==$ a $($car x$))$

$($in a $($cdr x$)))))$

$($definec ap $($x y :tl$)$ :tl

$($if $($endp x$)$ y

$($cons $($car x$)$

$($ap $($cdr x$)$ y$))))$

$($definec rv $($x :tl$)$ :tl

$($if $($endp x$)$ x

$($ap $($rv $($cdr x$))$

$($list $($car x$)))))$

$($definec rem$-$dups $($x :tl$)$ :tl

$($cond $(($endp x$)$ x$)$

$(($in $($car x$)($cdr x$))($rem$-$dups $($cdr x$)))$

$($t $($cons $($car x$)$

$($rem$-$dups $($cdr x$))))))$

; You get this property for free, since we did it in class. See

; l$26.$proof for the proof checker proof. You will have to do similar

; proofs for this homework.

$($property ap$-$assoc $($x y z :tl$)$

$(==($ap $($ap x y$)$ z$)$

$($ap x $($ap y z$))))$

; The first two lemmas are proof checker proofs of in$-$ap using

; different induction schemes.

Lemma in$-$ap$1$:

$(=>(^($tlp x$)($tlp y$))$

$(==($in a $($ap x y$))$

$($v $($in a x$)($in a y$))))$

Proof by: Induction on $($in a x$)$

XXX