如何证明两个变量的归纳类型是不相等的，如果他们的领域不相等？

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.