for SBT being Permutation of (8 -tuples_on BOOLEAN)
for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds (InvSubBytes SBT) . ((SubBytes SBT) . input) = input