Proving non-existence of an infinite inductive value in Coq

Suppose I have a very simple inductive type:

Inductive ind : Set :=
    | ind0 : ind
    | ind1 : ind -> ind.

and I'd like to prove that certain values can't exist. Specifically, that there can't be non-well-founded values: ~exists i, i = ind1 i.

I've looked around a bit on the internet and came up with nothing. I was able to write:

Fixpoint depth (i : ind) : nat :=
    match i with
    | ind0 => 0
    | ind1 i2 => 1 + depth i2
    end.

Goal ~exists i, i = ind1 i.
Proof.
    intro. inversion_clear H.
    remember (depth x) as d.
    induction d.
        rewrite H0 in Heqd; simpl in Heqd. discriminate.
        rewrite H0 in Heqd; simpl in Heqd. injection Heqd. assumption.
Qed.

which works, but seems really ugly and non-general.

Solution

I don't think there is a general method for proving such goals. From my experience, this has not seemed to be such a problem, however. In your case, there is a simpler proof, using the congruence tactic:

Inductive ind : Type :=
| ind0 : ind
| ind1 : ind -> ind.

Goal ~exists i, i = ind1 i.
Proof.
  intros [x Hx]. induction x; congruence.
Qed.