The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Thu, Nov 08, 2007 at 08:45:46PM +0100, anabelcesar anabelcesar wrote:
> Dear Instructors,
> I' ve only used Coq for a few months so please forgive my ignorance.
> 
> I have written the following code in order to relate the equality
> with an arrow type, but I have obtained an easy proof
> for the lemma trans1 but when I tried a similar proof for
> the lemma trans2 a "Cannot solve a second-order unification problem"
> error is obtained. Is it possible to proof that lemma?

If you delay the introduction of b, your proof goes through:

Lemma trans2: forall b:B,  (a_b (b_a b))=b.
Proof.
unfold b_a.
unfold a_b.
case p.
trivial.
Qed.

As to the why, I'll have to leave that to those more knowledgeable than
me :)

Edsko