| Who Cites is assoc sep? |
|
is_assoc_sep | Def is_assoc_sep(A; f) == is_assoc(A; x,y.(f(x,y))) |
| | Thm* f:(AAA). 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:(AAA). is_assoc(A; x,z.f(x,z)) Prop |