data nat = zero | succ nat
data int where
pos : nat -> int
neg : nat -> int
neg_zero_eq_zero : pos zero = neg zero
получается тип, где pos zero доказуемо равно neg zero, хоть конструкторы разные
и доказательство это как раз наш конструктор neg_zero_eq_zero