A new calculus for intuitionistic Strong Löb logic: strong termination and cut elimination, formalised

Table of Contents

Source code

Coq version: 8.16.1