25 Avr
2024
25 Avr
'24
10:38
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