coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] equality/injection

From: Nadeem Abdul Hamid <nadeem AT acm.org>
To: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] equality/injection
Date: Mon, 04 Feb 2002 11:27:35 -0500
Organization: Yale University

Can the following lemma be proven in Coq?:

Inductive Def1 : Set
  := c1 : Def1.

Inductive DefProp : Def1 -> Prop
  := c2 : (d:Def1)(DefProp d).

Inductive Comb : Set
  := c3 : (d:Def1)(DefProp d) -> Comb.

Lemma eq_comb
  : (d1,d1':Def1; d2:(DefProp d1); d2':(DefProp d1'))
    d1=d1' ->
    (c3 d1 d2)=(c3 d1' d2').

Thanks in advance,
--- nadeem

[Coq-Club] equality/injection, Nadeem Abdul Hamid
- Re: [Coq-Club] equality/injection, Christine Paulin
  - [Coq-Club] Re: equality/injection, Nadeem Abdul Hamid
    - Re: [Coq-Club] Re: equality/injection, Christine Paulin