The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Le 21/11/2011 15:53, Victor Porton a écrit :
> Parameter A : Set.
> Parameter B : A ->  Prop.
>
> Structure Foo := mkFoo { a : A; b : B a }.
>
> (* How to prove this lemma? Is it possible at all? *)
> Lemma my (u : Foo) : B (@a u).

Is it possible and *******trivial*********


Lemma my (u : Foo) : B (@a u).
destruct u;trivial.
Qed.


Do you mean you didn't try such an elementary solution ?

P.