The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

No, that looks unsolvable to me, unless isFree has an extremely
specific definition, such that ((exists a . isFree a) -> (forall a .
isFree a)).

If you got there starting from a solvable goal, you may have used an
intermediate step erasing valuable information. (Eg. destruct does
that sometimes if you don't retain an equality between the scrutinee
and its destructed components.)

On Wed, Jul 22, 2015 at 8:24 AM, Bahman Sistany 
<bsistany AT yahoo.ca>
 wrote:
> 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
>
>
>
>
>
>