[FOM] An intuitionistic query

[Arnold Neumaier]

Alice tells Bob that she has a set A={a,b,c} of cardinality 2, but she
is silent about any further detail. Intuition tells Bob that a, b, c
are names for two distinct elements, so that a=b or a=c or b=c.
Can intuitionistic logic prove this argument correct?

In other words, is
    A={a,b,c}, |A|=2    ==>   a=b v a=c v b=c          (*)
intuitionistically provable with generic interpretations of
the symbols on the left hand side of (*)?


Arnold Neumaier