Proving the security of a one-way function with partially known input Let's say we have a construction like in this question: We have a OWF $h(.)$, a secret salt TXT, and a counter starting at 1, and we compute

H1 = h(TXT || 1)
H2 = h(TXT || 2)
...
Hn = h(TXT || n)


According to the linked question, this scheme is secure. However, I was wondering how to formally proove this.

My first attempt was to try to formalize the scheme a little: Given the OWF $h(x)$, we construct $h'(x) = h(TXT\ ||\ x)$. Now, we can do the usual dance of "Assuming $h'(x)$ is no OWF, a PPT algorithm A exists that inverts it with non-negligible probability." We now have to use $A$ to construct a PPT attacker $B$ that inverts $h(.)$.

However, $h'(x)$ clearly does not even properly represent what the scheme above is doing (we know that TXT is fixed, but have no guarantee that $x$ is increasing monotonically). Since the function does not match the problem, it's not interesting if it is an OWF.

In fact, since the scheme does not even have any parameters, any attempt to put it into the form of an OWF is doomed. It's more of a PRNG, with TXT being the seed. So, one way to phrase the security requirement of this scheme would be "no algorithm $A$ exists that can determine TXT in PPT with a non-negligible probability, given any number of consecutive outputs of the PRNG".

This is where my ideas end. I am not sure how one would go about prooving this, or if there is a more elegant way to perform this proof. I'd be interested in how you would solve this problem (and if it is even possible).

(Note that this is no homework assignment, just me being curious about how one would proove this. It's also related to another question of mine, where the security of the scheme could be prooven in the same way)
You are right, it does not seem as if a reduction from OWF works here. Indeed it rather seems like a separation is possible. This is what @RickyDemer describes in his comment, i.e. showing that there exists at least one OWF $h$ for which the above use case is insecure. This would show that a reduction from OWF is impossible. 

You definitely can get a proof if you assume $h$ is a pseudorandom function family. In that case $TXT$ would have to be treated as key and the counter as message. Finding the (secret) key used for a PRF would allow to distinguish it from a truly random function with high probability and hence learning $TXT$ from the above inputs means breaking the PRF property of $h$... In practice you can for example use any HMAC as PRF.