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.
New to topics? Read the docs here!