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:
    1. L:List (N:Nat (N in nil = false))
    2. 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,