Recherche:

au fait y a-t-il une version pdf de ce cours en ligne ?

au fait minhkhue, où en es-tu ?

parce qu'on parle (j'ai un peu fait digressé le sujet), mais on ne sait pas si de ton côté ça avance ?

as-tu au moins compris où allait servir...

j'ai réservé ma place à l'asile, mais il y a une longue liste d'attente :roll:




l'argument serait plutôt... quand j'ai besoin de quelque chose, y a sûrement le système logique ad-hoc déjà...

mathématiquement oui... pour la preuve, je ne vois pas trop comment m'en sortir pour démontrer en Coq qu'une chose est vraie pour tout élément d'un ensemble vide





justement c'est cela que...

pour infos, j'ai essayé de la faire en entier... et je suis tombé sur un point non constructible :'(

mais peut-être y a-t-il une autre manière de procéder... je ne suis pas expert en Coq :aie:

tu connais forcément replace

connais-tu la commande unfold ?
http://coq.inria.fr/V8.1/tutorial.html

selon moi, il te faudra aussi inversion...