set p = the FinSeqLen of 0 ;
set f = the Function of (0 -tuples_on BOOLEAN),BOOLEAN;
take
1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN)
; ( 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is gate`2isBoolean & not 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is empty )
thus
( 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is gate`2isBoolean & not 1GateCircStr ( the FinSeqLen of 0 , the Function of (0 -tuples_on BOOLEAN),BOOLEAN) is empty )
; verum