TRS:
 {       or(true(), y) -> true(),
         or(x, true()) -> true(),
  or(false(), false()) -> false(),
         mem(x, nil()) -> false(),
        mem(x, set(y)) -> =(x, y),
   mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))}
 MPO:
  Prec:
   mem > or, 
   mem > false, 
   mem > =
   empty
  Strict:
   {}
   Weak:
    {}
  Qed