for MCFunc being Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
for output being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds MCFunc . ((MCFunc ") . output) = output