consider f being Function of 0 -tuples_on BOOLEAN , BOOLEAN ;
consider p being FinSeqLen of 0 ;
take 1GateCircStr p,f ; :: thesis: ( 1GateCircStr p,f is gate`2isBoolean & not 1GateCircStr p,f is empty )
thus ( 1GateCircStr p,f is gate`2isBoolean & not 1GateCircStr p,f is empty ) ; :: thesis: verum