In ‘Quantifiers and Propositional Attitudes’ (1956), Quine demonstrated that the naïve model-theoretic formalization of belief ascriptions de re, applied to cases of recognition failure, produces two unwelcome effects: 1) the seeming inconsistency of belief systems ascribed to rational agents, and 2) the contradictoriness of some (apparently well justified) belief reports. In the paper under discussion, Domanov claims that proof-theoretical formalization of belief ascriptions, based on the constructive type theory, precludes those effects. I challenge this claim by showing that the formalism (...) used by him reproduces at least the first of them. I suggest that this is so because of the identifying of variables from different contexts in Domanov’s definition of context extension functions. (shrink)