Implementing Sets with Lists
LIST is a refinement of SET.
We want to prove
L:List (N:Nat (N in nil = false)) and
L:List (M,N:Nat ( $ N in cons(M, L) = N == M or N in L $ ))
.
Conjunction elimination introduces subgoals as follows:

L:List (N:Nat (N in nil = false))

L:List (M,N:Nat ( $ N in cons(M, L) = N == M or N in L $ ))
This page was generated
by Kumo on
Mon Jun 15 13:44:45 PDT 1998
from code written by Grigore Rosu,