int empty(list* lst) { return !lst || lst->tag == NIL; }
  
  element head(list* l) {  
  head  
  require( ! empty(l) );
  return l->e;
  }
  
  
  list* tail(list* l) { 
  tail  
  require( ! empty(l) );
  return l->next;
  }
  
  
  bool equal(list* l, list* m) { 
  equal  
  switch( l->tag) {
    case NIL: return empty(m);
    case CONS: return !empty(m) && 
  		head(l) == head(m) &&
  		tail(l) == tail(m);
    }
  }