coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nadeem Abdul Hamid <nadeem AT acm.org>
- To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] Injection
- Date: Wed, 02 Jan 2002 10:08:43 -0600
- Organization: Yale University
Is is possible to prove the following lemma for this
inductive definition?
Inductive jdef : Set
:= jconst : (k:Set)k -> jdef.
Lemma eq_jdef : (x,y:nat)
(jconst ? x)=(jconst ? y)
-> x=y.
Normally, the Injection tactic could be used, but apparently
jdef is impredicative so it doesn't work.
--- nadeem
- [Coq-Club] Injection, Nadeem Abdul Hamid
- Re: [Coq-Club] Injection, Christine Paulin
Archive powered by MhonArc 2.6.16.