• GT Coq du 10 octobre 2008
• Ssreflect
• Syntaxe du destruct avec clause _eq
• Conclusion personnelle