Let g be a map defined as the Nisan–Wigderson generator but based on an NP ∩ coNP -function f. Any string b outside the range of g determines a propositional tautology τb expressing this fact. Razborov [27] has conjectured that if f is hard on average for P/poly then these tautologies have no polynomial size proofs in the Extended Frege system EF. We consider a more general Statement that the tautologies have no polynomial size proofs in any propositional proof system. (...) This is equivalent to the statement that the complement of the range of g contains no infinite NP set. We prove that Statement is consistent with Cook' s theory PV and, in fact, with the true universal theory T PV in the language of PV. If PV in this consistency statement could be extended to "a bit" stronger theory then Razborov's conjecture would follow, and if TPV could be added too then Statement would follow. We discuss this problem in some detail, pointing out a certain form of reflection principle for propositional logic, and we introduce a related feasible disjunction property of proof systems. (shrink)