aboutsummaryrefslogtreecommitdiffstats
path: root/theories (follow)
Commit message (Expand)AuthorAgeFilesLines
* lexicographic order proven well founded, checker extracted and verifying admi...Marcos Magueta2026-07-125-1/+121
* admission runs the containment checker extracted from rocqMarcos Magueta2026-07-112-3/+128
* rocq proof: structural decrease is well foundedMarcos Magueta2026-07-115-0/+74