Manuscript III@2 · III.tex · section · 82dad3e5
Constructions that do not discharge the sourced successor
Constructions that do not discharge the sourced successor · lines 2541–2547
A later construction does not change the domain or equivalence relation of an earlier theorem. The four opening rows remain different questions.