#line 123 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  // note: eq is not necessarily required for a membership test
  // for example: string member of regexp doesn't require
  // string equality
  // Set need not be finite (example regexp again)
  // A list is a set, despite the duplications
  class Set[c,t] {
    fun mem (elt:t, container:c):bool => elt \(\in\) container;
    virtual fun \(\in\) : t * c-> bool;
    fun \(\owns\) (container:c, elt:t) => elt \(\in\) container;
    fun \(\ni\) (container:c, elt:t) => elt \(\in\) container;
    fun \(\notin\) (elt:t, container:c) => not (elt \(\in\) container);
  
    fun \(\cup\)[c2 with Set[c2,t]]
      (x:c, y:c2) =>
      { e : t | e \(\in\) x or e \(\in\) y }
    ;
  
    fun \(\cap\)[c2 with Set[c2,t]]
      (x:c, y:c2) =>
      { e : t | e \(\in\) x and e \(\in\) y }
    ;
  
    fun \(\setminus\)[c2 with Set[c2,t]]
      (x:c, y:c2) =>
      { e : t | e \(\in\) x and e \(\notin\) y }
    ;
  }
  
  #line 176 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  interface set_form[T] { has_elt: T -> bool; }
  
  instance[T] Set[set_form[T], T] {
    fun \(\in\) (elt:T, s:set_form[T]) => s.has_elt elt;
  }
  open[T] Set[set_form[T],T];
  
  // INVERSE image of a set under a function
  // For a function f: t -> t2, an element e
  // is in a restriction of the domain t if its
  // image in t2 is in the specified set.
  fun invimg[t,c2,t2 with Set[c2,t2]]
    (f:t->t2, x:c2) : set_form[t] =>
    { e : t | (f e) \(\in\) x }
  ;
  
  #line 199 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  
  fun \(\times\)[U,V] (x:set_form[U],y:set_form[V]) =>
    { u,v : U * V | u \(\in\) x and v \(\in\) y }
  ;
  
  fun \(\otimes\)[U,V] (x:set_form[U],y:set_form[V]) =>
    { u,v : U * V | u \(\in\) x and v \(\in\) y }
  ;
  
  fun \(\otimes\)[U,V,W] (head:set_form[U], tail:set_form[V*W]) =>
    { u,v,w : U * V * W | u \(\in\) head and (v,w) \(\in\) tail }
  ;
  
  fun \(\otimes\)[NH,OH,OT] (head:set_form[NH], tail:set_form[OH**OT]) =>
    { h,,(oh,,ot) : NH ** (OH ** OT) | h \(\in\) head and (oh,,ot) \(\in\) tail }
  ;