Once individuation of proofs has been settled, we can distinguish between replaceable thinking and superfluous thinking, where these attributions are understood as relative to a given argument or proof. In the process of thinking through a proof, a given part of the thinking is replaceable if thinking of some other kind could stand in place of the given part in a process that would count as thinking through the same proof. A given part of the thinking is superfluous if its excision without replacement would be a process of thinking through the same proof. Superfluous thinking may be extremely valuable in facilitating grasp of the proof text and in enabling one to understand the idea underlying the proof steps; but it is not necessary for thinking through the proof. 