Temporary assumption
= Temporary assumption
A <temporary assumption> is introduced for a hypothetical subproof and retained only within that scope. A suitable <inference rule> can discharge it while forming a conclusion valid under the surrounding assumptions. Its scope must be recorded even when the assumption is unused inside the subproof.