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