coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem to remove the type option...

From: Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>
To: frederic.gava AT wanadoo.fr
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Problem to remove the type option...
Date: Fri, 21 Mar 2003 18:29:38 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Frederic GAVA
<frederic.gava AT wanadoo.fr>
wrote:
> mais pas ceci
>
>  Lemma egal_some: (T:Set)(a,b:T) ((Some ? a)=(Some ? b)) -> (a=b).
>  ???
>

This one is easy:

Intros T a b hyp.
Inversion hyp.
Trivial.

Pierre Courtieu

[Coq-Club] Problem to remove the type option..., Frederic GAVA
- Re: [Coq-Club] Problem to remove the type option..., Pierre Courtieu