The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

I'm mechanizing some meta-theory, and need to prove around a dozen lemmas 
that state that various pieces of syntax cannot appear inside themselves.  
The basic cases are easy, but the more complicated cases are giving me 
trouble, so I'd like to appeal to this list for help.  Here is an example:

Inductive ty : Set :=
 | one : ty
 | prop : ty
 | prod : ty -> ty -> ty
 | pow : ty -> ty
 | dom : ty
 | zero : ty
 | sum : ty -> ty -> ty.

(* easy *)
Lemma contra_sum : forall t t', t = sum t t' -> False.
Proof.
 intros. induction t; intros; try discriminate.
 apply IHt1. injection H. intros. subst t2.
 auto.
Qed.

(* hard *)
Lemma contra_sum_prod : forall t1 t0 t2,
                   (t0 = sum (prod t1 t0) t2) -> False.
Proof.
(* help *)