Mechanically proving element non-membership

Question

I'm facing a (possibly simple) problem while proving a theorem.

I need to show that under several (true) assumptions, some element is not in a set. Such assumptions are all met and there is are lemmata that can be employed to reach the conclusion. The problem comes from the fact that the lemma for doing so must be applied an arbitrary number of times.

Lemma 1: $\forall x:\big(x\in X \iff P(x) \big)$

Lemma 2: $\forall x,y : (P(x) \land Q(y) \land x\neq y) \Rightarrow qq \neq x $

Lemma 3: $\forall x : P(x) \Rightarrow Q(x)$

Assumption: $\vert X\vert=k \land k\ge 2 %\big(\forall x\in X.P(x)\big)$

Desired result: $qq\not\in X$

What i tried so far:

Proof: Intuitively, it is easy to see that $qq\not\in X$ because I can choose two elements $a$ and $b$ of $X$ (they are distinct by definition), plug them in lemma 2, and get that $qq\neq a$. If we apply this idea $k$ times we get that $qq$ is not an element of $X$, hence it is not in $X$. $\Box$

When $k=2$ or bounded, this reasoning works.

The problem: $k$ is not known in advance and I can not mechanically apply Lemma 2 arbitrarily many times.

How can I prove this intuitive fact in a mechanical fashion? I've been (vaguely) suggested to employ a bijection but i still don't see how to do so.

Answer 1

I eventually proved the theorem in a mechanical fashion and I want to thank j_random_hacker for pointing out a proof sketch based on induction and correcting my wrong initial formal statement.

The actual (mechanical) solution did require the employment of an inductive predicate that allows the human prover to instantiate the inductive hypothesis to a set $X'$.

The employment of natural induction in a mechanized fashion seems to be insufficient for carrying out the proof. This specific problem is discussed further here: Induction examples in PVS, slide 23/61. A different solution suggested there is subtyping.