Logic Induction — Proof Atlas

Well-founded induction, formalized twice: on paper and in Lean 4

92 theorems sorry-free

127 of 127 declarations