Pour transformer une proposition en une "mere proposition", et que tu ne veux/peux pas utiliser `conv_erase`, au lieu de

|P| = Erased P

tu peux utiliser la double négation

|P| = (P → ?A) → ?A

maintenant qu'on a la "functional extensionality".

Stefan