I am fairly familiar with LPL and natural deduction. As I recall, elimination is regarded as one of the rules of inference. Aren't those regarded as axioms or axiom schemas? If so, those are assumptions. You're probably not going to be able to prove they are true within first order logic. However, it may have been proven that elimination is consistent with the other axioms/axiom schemas. I don't know all that's involved with that other than metalogic theorems. To me, elimination seems intuitively obvious: if something is true for all objects, then it's true for a particular object.