A machine-checked solution to the Jacobians challenge

27.1. Keystones🔗

  • tail duality injectivity/surjectivity

  • Miranda Lemma 3.6 order downgrade