consider f being Function of (0 -tuples_on BOOLEAN ),BOOLEAN ;
consider p being FinSeqLen of ;
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