 Substitution-failure is supported for contingently coextensive expressions. For instance, (19) does not entail want(^(a(pringle(sweater))))(jack) even if there are worlds where all and only woollen sweaters are Pringle sweaters, so long as there are other worlds where this is not so. Let u be a world of the latter sort. Then a(pringle(sweater)) at u and a(woollen(sweater)) at u are different functions of type (ib)b, making ^(a(pringle(sweater))) and ^(a(woollen(sweater))) different at every world. Therefore want(^(a(pringle(sweater)))) may map Jack to FALSE at worlds where want(^(a(woollen(sweater)))) maps Jack to TRUE: since want is applied to different inputs here, the outputs may also be different.