package coq-kruskal-veldman

  1. Overview
  2. No Docs
Wim Veldman's proof of Higman's and Kruskal tree theorems

Install

Dune Dependency

Authors

Maintainers

Sources

Kruskal-Veldman-1.3.tar.gz
sha256=0a2e33bb394709bd5eb723d5bd47a25770fb8129d0fff5fb83ca44916f3da210

Description

This library formalizes additional tools for AF relations, eg AF lexicographic induction and relational quasi morphisms applied to Wim Veldman's constructive proof of the tree theorem.