Proof rules in discrete math When you write that a element is arbitrary, for example,
 "Let z be an arbitrary animal", does that automatically implies that you are using generalization rule as a proof?
 A: In mathematical practice, in order to prove that a formula $\phi$ is true for every element $x$, a standard move is to write :

"let $t$ be an element"

and then prove $\phi[t/x]$ without using any information about $t$. Then $\phi[t/x]$ must be true regardless of what element $t$ is, and so $∀x \phi$ is proved.
Thus, when starting an argument with "let $t$", we introduce a new term (constant or variable) considering it "generic"; if we prove $\phi$, then we can apply the $\forall$-introduction rule (also called : Generalization) and conclude with $\forall x \phi$.
The $\forall$-introduction rule is :

if $\Gamma \vdash \phi$, then $\Gamma \vdash \forall x \phi$, provided that $x$ is not free in any formula of $\Gamma$.

We have to take care about the "let $t$ arbitrary". Consider this (wrong) derivation :
1) $x=0$ --- assumed [$x$ is not "arbitrary" !]
2) $\forall x (x=0)$ --- Generalization (wrong : $x$ is not free in 1)
3) $x=0 \to \forall x (x=0)$
4) $\forall x[x=0 \to \forall x (x=0)]$ --- Generalization (now is "legal")

5) $0=0 \to \forall x (x=0)$ --- from 4) by Instantiation.

The last formula is clearly false in $\mathbb N$; thus, the derivation must be wrong !

An argument starting with "let $t$ arbitrary" can also invlove $\exists$-elimination:

if $\Gamma,ϕ[t/x] \vdash ψ$, then $Γ,∃xϕ(x) \vdash ψ$, provided that $t$ is not free in $ψ$ or any formula of $Γ$.

In this case, we "know" that $\exists x \phi$ and we we start by writing :

"let $t$ be a $\phi$s";

if from this assumption we can derive a conclusion $\psi$ that does not mention $t$, we are licensed to conclude $\psi$ from the premise : "there exists some $\phi$s".
