\subsection{Structural Induction}
In this subsection, we present structural induction over lists.
The same concept also applies similarly to trees and more.
Weak Structural Induction on treees is presented in the subsequent subsection.

For both, we only provide the natural deduction rules, as the proofs proceed analogously to the ones for mathematical induction.

\subsubsection{Weak Structural Induction}
\[
    \begin{prooftree}
        \hypo{\Gamma \vdash P(\texttt{[]})}
        \hypo{\Gamma, P(\texttt{xs}) \vdash P(\texttt{x : xs})}
        \infer2[where \texttt{x}, \texttt{xs} not free in $\Gamma$]{\Gamma \vdash \forall \texttt{xs} . P(\texttt{xs})}
    \end{prooftree}
\]

\subsubsection{Strong Structural Induction}
\inlinedefinition[Subterm relation] denoted $\sqsubset$ is defined as follows:
\[
    \forall xs, ys . xs \sqsubset ys \Leftrightarrow (\exists x. ys = x:xs) \lor (\exists zs . xs \sqsubset zs \land zs \sqsubset ys)
\]
\begin{align*}
    \begin{prooftree}
        \hypo{\Gamma, \forall ys \sqsubset xs . P(ys) \vdash P(xs)}
        \infer1[$xs$ not free in $\Gamma$, $ys$ not free in $P(xs)$]{\Gamma \vdash \forall xs . P(xs)}
    \end{prooftree}
\end{align*}
