I need to prove a theorem involving 2 variables a and b, a hypothesis H specifying the possible values of a (a = v1 \/ a = v2 \/ ... \/ a = vn), and a hypothesis H0 specifying values of b (b = v1' \/ b = v2' \/ ... \/ b = vn'), and a hypothesis that a and b are not equal. I can't use repeat (destruct H0; xxx) because it would destruct the hypothesis H0: b = vn', and make the proof impossible to continue. Is there a way to do "repeat" only finite number of times? Or what are some other ways to solve the problem that I currently have?
My proof currently looks like this (xxx is a tactic I defined myself):
intros. subst.
destruct H.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
xxx.
destruct H.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
destruct H0. xxx.
xxx.
...(just repeat the above)
It is best to include a minimal working example with your question. I tried to reconstruct your question as best I could, but without a full example, I had to guess in some places.
The following seems to work:
From Coq Require Import Utf8.
Parameter A : Type.
Parameter v1 v2 v3 v4 v5 v6 v7 v8 v1' v2' v3' v4' v5' v6' v7' v8' : A.
Goal ∀ a b : A, (a = v1 ∨ a = v2 ∨ a = v3 ∨ a = v4 ∨
a = v5 ∨ a = v6 ∨ a = v7 ∨ a = v8) →
(b = v1' ∨ b = v2' ∨ b = v3' ∨ b = v4' ∨
b = v5' ∨ b = v6' ∨ b = v7' ∨ b = v8') → False.
Proof.
intros a b H H0.
(repeat destruct H as [ | ]); (repeat destruct H0 as [ | ]).