The hideL weakening proof rule discards an available assumption P
.
You should hide irrelevant assumptions whenever possible, because that can save a lot of computation time during the proof.
Use hideL by clicking the closed-eye symbol next to a formula you hover over.
See also