These two exports bring in two axioms.
Function extensionality:
\begin{equation*} \forall x, f x = g x \to f = g \end{equation*}
Propositional extensionality:
\begin{equation*} \forall \phi \psi, (\phi \iff \psi) \iff \phi = \psi \end{equation*}
These axioms are known to be consistent with Coq's theory. They are not fundamental to Tealeaves in the sense that propositional equality could be replaced everywhere with setoids, but these axioms make the formalization much more convenient.
From Coq.Logic Require Export
FunctionalExtensionality
PropExtensionality.