A question we face is whether, in order to come to know the truth of a conclusion by following an argument involving generalisation on an arbitrary instance (a.k.a. universal generalisation, or universal quantifier introduction), the thinking must include a conscious, explicit check that the proviso is met. It is clearly not enough that the proviso is in fact met. For in that case it might just be the thinker’s good luck that the proviso is met; hence the thinker would not know that the generalisation is valid and so would not have genuinely thought through the proof at that step.