consider p being FinSeqLen of 1;
consider f being Function of (1 -tuples_on BOOLEAN ),BOOLEAN ;
take 1GateCircStr p,f ; :: thesis: ( 1GateCircStr p,f is unsplit & 1GateCircStr p,f is gate`1=arity & 1GateCircStr p,f is gate`2=den & 1GateCircStr p,f is gate`2isBoolean & not 1GateCircStr p,f is void & 1GateCircStr p,f is strict )
thus ( 1GateCircStr p,f is unsplit & 1GateCircStr p,f is gate`1=arity & 1GateCircStr p,f is gate`2=den & 1GateCircStr p,f is gate`2isBoolean & not 1GateCircStr p,f is void & 1GateCircStr p,f is strict ) ; :: thesis: verum