# Re: [isabelle] Uniqueness quantification

```I indeed want "p q" to hold for exactly one of the 5 expressions, i.e.
only one of the 5 predicates returns true for all arguments.

Applying clarify/clarsimp seems to work indeed. However, if I change
the type of the predicates from "nat =>  bool" to "(nat*nat) =>  bool",
the proof breaks. Do you know why the input type of the predicates
affects the proof?
```
```
```
No particularly good ideas here, except that things are becoming more complicated.
```
```
```Right, but how come the reverse doesn't hold? If there's exactly one
of the predicates returning true, then isn't the length of the
filtered list one?
```
```
```
No. To phrase what I said before in different language again, the cardinality of the set you've been talking about "{p1, p2, p3, p4, p5}" isn't necessarily 5. If "p1 = p2" then there are less than 5 unique elements of the set "{p1, p2, p3, p4, p5}".
```
```
To rephrase this once more: if you add a p6 to your axiomatization with the axiom ax6: "p6 = p5", then the equivalent lemma is still provable:
```
lemma lem: "EX! p:{p1,p2,p3,p4,p5, p6}. p q"
```
apply (simp add: conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib)
```  apply clarsimp
apply (metis axs)
done

```
The reason this is provable is because "{p1, p2, p3, p4, p5, p6} = {p1, p2, p3, p4, p5}", so it's really just the same as the 5 example.
```
Yours,
Thomas.

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.