The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

If the inductive proof of n + 1 = S n is Qeded, then you cannot reduce it in proof terms using it, I think that's what Ilmārs is saying. There's currently no getting around reproving it transparently.
-- Matthieu

Le ven. 22 avr. 2016 à 13:55, Pierre Courtieu <pierre.courtieu AT gmail.com> a écrit :

2016-04-22 0:32 GMT+02:00 Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>:
> Probably I can't. They're opaque and that's all.

I am afraid so.

> I need them, for example, to prove that types list A (n + 1) and list A (S
> n) are equal and then use this equality in computations.

I don't understand, an equality cannot help "computation" as far as I
can tell. You mean that this equality allows to rewrite *and then* you
can compute right? But then the transparency is not the problem.

> For now I just prove necessary equality again, this time transparently.

Can you give some code here please? I don't see what transparency can help here.

Best
Pierre Courtieu