A local derivation made under additional temporary assumptions. Its conclusions can be used within their scopes, but exporting a result requires a rule that accounts for those assumptions. Indentation, boxes or explicit assumption labels record that dependency information.
New to topics? Read the docs here!