The Coq mailing list

["Peter Hawkins" <hawkinsp AT cs.stanford.edu>]

Hi...

I'm wondering whether there's a quick way to discount goals with
hypotheses of this form:
EqH: s = a::s
s: list A
a: A
A: Set

I can prove this lemma:
Lemma list_not_rec: forall (A:Set) (s:list A) i, s = i::s -> False.
Proof.
 intros; induction s.
 discriminate.
 inversion H. auto.
Qed.

and solve my goal using:
elim (list_not_rec _ _ _ EqH).

but given that self-referential equalities like EqH cannot hold for
any (necessarily finite) instance of an inductive type, I was hoping
that there might be a more general tactic to handle these sorts of
hypotheses without doing one proof by induction for each type.

Cheers,
Peter