  To resolve the difficulty, we note that in deriving Excluded Middle from ACL1 essential use was made of the principles of Predicative Comprehension and Extensionality of  Functions[18].   It follows that, in systems of constructive mathematics affirming AC (but not Excluded Middle) either the principle of Predicative Comprehension or the principle of Extensionality of Functions must fail. While the principle of Predicative Comprehension can be given a constructive justification, no such justification can be provided for the principle of Extensionality of Functions. Functions on predicates are given intensionally, and satisfy just the corresponding principle of Intensionality \(\forall X \forall Y \forall F[X = Y \rightarrow  FX = FY]\). The principle of Extensionality can easily be made to fail by considering, for example, the predicates \(P\): rational featherless biped and \(Q\): human being and the function \(K\) on predicates which assigns to each predicate the number of words in its description. Then we can agree that \(P \approx Q\) but \(KP = 3\) and \(KQ = 2\).