Как делать дела с индуктивным типом в Coq

Я хочу использовать тактику destruct , чтобы доказать утверждение по делам. Я прочитал пару примеров в Интернете и запутался. Могу ли я кто-нибудь объяснит это лучше?

Вот небольшой пример (есть и другие способы решения, но попробуйте использовать destruct ):

 Inductive three := zero 
                  | one 
                  | two.
 Lemma has2b2: forall a:three, a<>zero /\ a<>one -> a=two.

Теперь в некоторых примерах в Интернете предлагается сделать следующее:

intros. destruct a.

В котором случай, который я получаю:

3 subgoals H : zero <> zero /\ zero <> one
______________________________________(1/3) 
zero = two

______________________________________(2/3) 
one = two

______________________________________(3/3) 
two = two

Итак, я хочу доказать, что первые два случая невозможны. Но машина перечисляет их как подцели и хочет, чтобы я ДОКАЗЫВАЛ их ... что невозможно.

Резюме: Как точно отбросить невозможные случаи?

Я видел несколько примеров, использующих инверсию , но я не понимаю процедуру.

Наконец, что произойдет, если моя лемма зависит от нескольких индуктивных типов и я все еще хотите охватить ВСЕ случаи?