Let φ, ψ, χ stand for well formed formulas, and let m, n, o stand for available line numbers in a derivation.