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) ; :: thesis: ( 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 ) ; :: thesis: verum