The allL proof rule makes use of a universal assumption ∀x p(x) by plugging in any arbitrary term e and assuming p(e), which follows from ∀x p(x).

Learning resources