如何證明兩個變量的歸納類型是不相等的，如果他們的領域不相等？

Question

假設我有一個感應式：

Inductive addr : Type := mk_addr : Z -> Z -> addr. 

是否可以證明下面的目標是什麼？

Goal 
    forall (x y z : Z), 
    y <> z -> mk_addr x y <> mk_addr x z. 

Answer 1

congruence可以照顧它：

Goal 
    forall (x y z : Z), 
    y <> z -> mk_addr x y <> mk_addr x z. 

congruence. 
Qed. 

或者，你可以證明這種說法的對換句：

Goal 
forall (x y z : Z), 
y <> z -> mk_addr x y <> mk_addr x z. 
intros x y z H1 H2. 
apply H1. 
injection H2. 
trivial. 
Qed.