take CatStr(# {0},{{0}},({0} :-> 0),({0} :-> 0),(({0},{0}) :-> {0}) #) ; :: thesis: ( not CatStr(# {0},{{0}},({0} :-> 0),({0} :-> 0),(({0},{0}) :-> {0}) #) is void & not CatStr(# {0},{{0}},({0} :-> 0),({0} :-> 0),(({0},{0}) :-> {0}) #) is empty )
thus ( not CatStr(# {0},{{0}},({0} :-> 0),({0} :-> 0),(({0},{0}) :-> {0}) #) is void & not CatStr(# {0},{{0}},({0} :-> 0),({0} :-> 0),(({0},{0}) :-> {0}) #) is empty ) ; :: thesis: verum