The andL proof rule expresses that if we have a conjunction P∧Q among our assumptions, then we can separately assume both conjuncts P as well as Q, instead.
See also
prop uses all propositional logic rules for operators ¬,∧,∨,→,↔
unfold does all easy steps until loop or ODE without excessive branching