coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Bahman Sistany <bsistany AT yahoo.ca>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] How to refer to a un-destructed inductive types in Theorems
Date: Wed, 22 Jul 2015 06:24:50 +0000 (UTC)

Hi,

I have a simple inductive type called 'constraint. Let's say in my context at some point I have:

a : constraint

b : constraint

The goal is some proposition isFree involving b. so:

a : constraint

b : constraint

H: isFree (a).

------------------------------------

isFree(b)

What am I missing from proving this simple goal given H? I know if I had 'a=b' in the context, it would be simple but I don't.

And proof-irrelevance applies to Props only otherwise it would have given me a=b.

In this case should I expect that isFree (a) implies isFree(b)?

--Bahman

[Coq-Club] How to refer to a un-destructed inductive types in Theorems, Bahman Sistany, 07/22/2015
- Re: [Coq-Club] How to refer to a un-destructed inductive types in Theorems, Gabriel Scherer, 07/22/2015
- Re: [Coq-Club] How to refer to a un-destructed inductive types in Theorems, Cedric Auger, 07/22/2015