package coq-kruskal-veldman

  1. Overview
  2. Homepage
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.

Rocq

Interactive Theorem Prover