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