consider p being natural-valued FinSeqLen of 0 ;
consider f being Function of (0 -tuples_on X),X;
take 1GateCircStr (p,f) ; :: thesis: 1GateCircStr (p,f) is with_nonpair_inputs
thus 1GateCircStr (p,f) is with_nonpair_inputs ; :: thesis: verum