| Who Cites is assoc sep? |
|
is_assoc_sep | Def is_assoc_sep(A; f) == is_assoc(A; x,y.(f(x,y))) |
|
| Thm* f:(A A A). is_assoc_sep(A; f) Prop |
|
is_assoc | Def is_assoc(A; x,z.f(x;z)) == x,y,z:A. f(x;f(y;z)) = f(f(x;y);z) A |
|
| Thm* A:Type, f:(A A A). is_assoc(A; x,z.f(x,z)) Prop |