The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Jieung Kim wrote:
> I have one more question about a proof.

Is this a proof that you've already worked out informally?  That's an 
appropriate first step before asking for Coq-specific advice, in which 
case you should be asking how to encode particular steps of your 
informal proof, rather than the theorem overall.

> For example, In this case, I think I cannot prove
>
>     *Lemma sub_ty_same_or_not: forall t1 t2, (sub_ty t1 t2) \/
>     ~(sub_ty t1 t2).*

This theorem looks provable to me.