j
k
j a
j l
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
Retour au fil de discussion
Retour à la liste