coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Rui Baptista <rpgcbaptista AT gmail.com>
To: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
Cc: Cedric Auger <sedrikov AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Posting my first bigger stuff (for experience/training)
Date: Tue, 26 Nov 2013 09:45:42 +0000

Have you looked at example 7 in chapter 26 "User defined equalities and relations" of the manual?

It doesn't mention f_equiv though.

Re: [Coq-Club] Posting my first bigger stuff (for experience/training), (continued)