Definitions: Mathlib.Data, part 6 of 6

Let $x_{2}$ and $i$ be elements of $x$. Let $f$ be a function from elements $j$ of $\SubtypeSet {i_{1}}{\mathrm{Neq} (i_{1} , x_{2})}$ to elements of $M$ applied to $j$. Let $x_{3}$ be an element of $M$ applied to $x_{2}$. Then $\operatorname{subtypeNeLift}$ applied to $x_{2}$, $j$, $f$, $x_{3}$ and $i$ is an element of $M$ applied to $i$.

Let $a$ be an element of $x$. Then $\mathrm{Sum3\_\_in\_u2080\_}$ applied to $a$ is an element of $\mathrm{Sum}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$ defined as $\operatorname{inl}$ applied to $a$.

Let $b$ be an element of $x_{1}$. Then $\mathrm{Sum3\_\_in\_u2081\_}$ applied to $b$ is an element of $\mathrm{Sum}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$ defined as $\operatorname{inr}$ applied to $\operatorname{inl}$ applied to $b$.

Let $c$ be an element of $x_{2}$. Then $\mathrm{Sum3\_\_in\_u2082\_}$ applied to $c$ is an element of $\mathrm{Sum}$ applied to $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x_{2}$ defined as $\operatorname{inr}$ applied to $\operatorname{inr}$ applied to $c$.

the sum lexicographic lift of x10 and x11 (from the name)

Let $x_{6}$ be a function from elements of $x$ and elements of $x_{2}$ to finite sets of $x_{4}$. Let $x_{7}$ be a function from elements of $x_{1}$ and elements of $x_{3}$ to finite sets of $x_{5}$. Let $x_{8}$ be a function from elements of $x$ and elements of $x_{3}$ to finite sets of $x_{4}$. Let $x_{9}$ be a function from elements of $x$ and elements of $x_{3}$ to finite sets of $x_{5}$. Let $x_{10}$ be an element of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Let $x_{11}$ be an element of $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$. Then the sum lexicographic lift of $x_{10}$ and $x_{11}$ is a finite set of $\mathrm{Sum}$ applied to $x_{4}$ and $x_{5}$.

the sum lift of x6 and x7 (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{2}$ to finite sets of $x_{4}$. Let $g$ be a function from elements of $x_{1}$ and elements of $x_{3}$ to finite sets of $x_{5}$. Let $x_{6}$ be an element of $\mathrm{Sum}$ applied to $x$ and $x_{1}$. Let $x_{7}$ be an element of $\mathrm{Sum}$ applied to $x_{2}$ and $x_{3}$. Then the sum lift of $x_{6}$ and $x_{7}$ is a finite set of $\mathrm{Sum}$ applied to $x_{4}$ and $x_{5}$.

symmetric power of x and n (from the name)

Let $x$ be a set. Let $n$ be an element of $\Natural$. Then a symmetric power of $x$ and $n$ is an element of the function that maps $x$ and $n$ to $\SubtypeSet {s}{\mathrm{Eq} (\operatorname{card} (s), n)}$.

symmetric power of x and n (from the name)

Let $x$ be a set. Let $n$ be a natural number. Then a symmetric power of $x$ and $n$ is an element of the function that maps $x$ and $n$ to $\mathrm{Quotient}$ applied to $\operatorname{isSetoid}$ applied to $x$ and $n$.

Let $s$ be a symmetric power of $x$ and $n$. Let $\mathrm{s'}$ be a symmetric power of $x$ and $\mathrm{n'}$. Then $\operatorname{append}$ applied to $s$ and $\mathrm{s'}$ is a symmetric power of $x$ and $n + \mathrm{n'}$ defined as $s + \mathrm{s'}$.

Let $s$ be a symmetric power of $x$ and $n$. Then $\operatorname{attach}$ applied to $s$ is a symmetric power of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {s}{x_{1}})}$ and $n$ defined as $\operatorname{attach}$ applied to $s$.

the cast of h (from the name)

Assume that $n = m$. Then the cast of $h$ is an equivalence from the set of symmetric powers of $x$ and $n$ to the set of symmetric powers of $x$ and $m$.

Let $a$ be an element of $x$. Let $s$ be a symmetric power of $x$ and $n$. Then $\operatorname{cons}$ applied to $a$ and $s$ is a symmetric power of $x$ and the successor of $n$ defined as $\operatorname{cons}$ applied to $a$ and $s$.

Let $x_{1}$ be an element of $x$. Let $x_{2}$ be a symmetric power of $x$ and $n$. Then $\operatorname{cons'}$ applied to $x_{1}$ and $x_{2}$ is a symmetric power of $x$ and the successor of $n$.

the equivalence congruence of e (from the name)

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the equivalence congruence of $e$ is an equivalence from the set of symmetric powers of $x$ and $n$ to the set of symmetric powers of $x_{1}$ and $n$.

Let $s$ be a symmetric power of $x$ and $n + 1$. Let $a$ be an element of $x$ such that $a$ is an element of $s$. Then $\operatorname{erase}$ applied to $s$, $a$ and $h$ is a symmetric power of $x$ and $n$ defined as $\operatorname{erase}$ applied to $s$ and $a$.

Let $a$ be an element of $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $m$ be a symmetric power of $x$ and $n - \operatorname{val} (i)$. Then $\operatorname{fill}$ applied to $a$, $i$ and $m$ is a symmetric power of $x$ and $n$.

Let $a$ be an element of $x$. Let $m$ be a symmetric power of $x$ and $n$. Then $\operatorname{filterNe}$ applied to $a$ and $m$ is an element of $\Sigma$ applied to the function that maps $i$ to the set of symmetric powers of $x$ and $n - \operatorname{val} (i)$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a symmetric power of $x$ and $n$. Then the map of $f$ and $x_{2}$ is a symmetric power of $x_{1}$ and $n$ defined as the map of $f$ and $x_{2}$.

Let $m$ be a multiset of $x$ such that the cardinality of $m$ is equal to $n$. Then $\operatorname{mk}$ applied to $m$ and $h$ is a symmetric power of $x$ and $n$ defined as $m$.

$\operatorname{nil}$ is a symmetric power of $x$ and $0$ defined as $0$.

the symmetric power of x1 (from the name)

Let $x_{1}$ be a vector of $x$ and $n$. Then the symmetric power of $x_{1}$ is a symmetric power of $x$ and $n$ defined as the multiset of $x_{1}$.

the one equivalence (from the name)

The one equivalence is an equivalence from $x$ to the set of symmetric powers of $x$ and $1$.

Let $n$ be a natural number. Let $a$ be an element of $x$. Then $\operatorname{replicate}$ applied to $n$ and $a$ is a symmetric power of $x$ and $n$ defined as $\operatorname{replicate}$ applied to $n$ and $a$.

the symmetric power equivalence symmetric power (from the name)

The symmetric power equivalence symmetric power is an equivalence from the set of symmetric powers of $x$ and $n$ to the set of symmetric powers of $x$ and $n$.

the multiset of s (from the name)

Let $s$ be a symmetric power of $x$ and $n$. Then the multiset of $s$ is a multiset of $x$ defined as $s$.

the decode of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{Sum}$ applied to the set of symmetric powers of $\mathrm{Option}$ applied to $x$ and $n$ and the set of symmetric powers of $x$ and the successor of $n$. Then the decode of $x_{1}$ is a symmetric power of $\mathrm{Option}$ applied to $x$ and the successor of $n$.

Let $s$ be a symmetric power of $\mathrm{Option}$ applied to $x$ and the successor of $n$. Then $\operatorname{encode}$ applied to $s$ is an element of $\mathrm{Sum}$ applied to the set of symmetric powers of $\mathrm{Option}$ applied to $x$ and $n$ and the set of symmetric powers of $x$ and the successor of $n$.

the symmetric power option successor equivalence (from the name)

The symmetric power option successor equivalence is an equivalence from the set of symmetric powers of $\mathrm{Option}$ applied to $x$ and the successor of $n$ to $\mathrm{Sum}$ applied to the set of symmetric powers of $\mathrm{Option}$ applied to $x$ and $n$ and the set of symmetric powers of $x$ and the successor of $n$ defined as $\operatorname{mk}$ applied to $\operatorname{encode}$, $\operatorname{decode}$, $\mathrm{SymOptionSuccEquiv\_\_decode\_encode}$ and $\mathrm{SymOptionSuccEquiv\_\_encode\_decode}$.

$\operatorname{e1}$ is an equivalence from $\SubtypeSet {s}{(\MembershipmemMACRoT {s}{0})}$ to the set of symmetric powers of $\mathrm{Fin}$ applied to the successor of $n$ and $k$.

$\operatorname{e2}$ is an equivalence from $\SubtypeSet {s}{\mathrm{not} (\MembershipmemMACRoT {s}{0})}$ to the set of symmetric powers of $\mathrm{Fin}$ applied to the successor of $n$ and $k$.

the sigma fiber from relation of sym and hf (from the name)

Assume that $r$ is symmetric. Assume that $r \leq \operatorname{r}$. Then the sigma fiber from relation of $\mathrm{sym}$ and $\mathrm{hf}$ is an equivalence from the set of elements of $\operatorname{fromRel}$ applied to $\mathrm{sym}$ to $\Sigma$ applied to the function that maps $b$ to the set of elements of $\operatorname{fromRel}$ applied to $\operatorname{comap}$ applied to the function that maps $a$ to $\EqtMACRoH {f (a)}{b}$.

the sigma quotient from relation of sym and f (from the name)

Assume that $r$ is symmetric. Let $f$ be a relation homomorphism of $r$ and $\mathrm{r'}$. Then the sigma quotient from relation of $\mathrm{sym}$ and $f$ is an equivalence from the set of elements of $\operatorname{fromRel}$ applied to $\mathrm{sym}$ to $\Sigma$ applied to the function that maps $q$ to the set of elements of $\operatorname{fromRel}$ applied to $\operatorname{comap}$ applied to the function that maps $x_{2}$ to $\EqtMACRoH {\operatorname{mk} (\mathrm{r'} , f (x_{2}))}{q}$.

the sigma quotient from relation of sym and f (from the name)

Assume that $r$ is symmetric. Let $f$ be a relation homomorphism of $r$ and $\operatorname{r}$. Then the sigma quotient from relation of $\mathrm{sym}$ and $f$ is an equivalence from the set of elements of $\operatorname{fromRel}$ applied to $\mathrm{sym}$ to $\Sigma$ applied to the function that maps $q$ to the set of elements of $\operatorname{fromRel}$ applied to $\operatorname{comap}$ applied to the function that maps $x_{2}$ to $\EqtMACRoH {\operatorname{mk} (\mathrm{r'} , f (x_{2}))}{q}$.

the symmetric power map of f (from the name)

Let $f$ be an embedding of $x$ and $x_{1}$. Then the symmetric power map of $f$ is an embedding of the set of symmetric squares of $x$ and the set of symmetric squares of $x_{1}$.

the symmetric power of s (from the name)

Let $s$ be an element of $\wp x$. Then the symmetric power of $s$ is an element of the power set of the set of symmetric squares of $x$.

symmetric square of x (from the docstring)

Let $x$ be a set. Then a symmetric square of $x$ is an element of the function that maps $x$ to $\mathrm{Quot}$ applied to $\operatorname{Rel}$ applied to $x$.

x1 is a diagonal (from the name)

Let $x_{1}$ be a symmetric square of $x$. Then $x_{1}$ is a diagonal, if $\operatorname{lift}$ holds for $\mathrm{Eq}$ and $x_{1}$.

Let $x_{1}$ be an element of $x$. Let $z$ be a symmetric square of $x$. Then $\operatorname{Mem}$ holds for $x_{1}$ and $z$, if there exists an element $y$ of $x$, such that $\EqtMACRoH {z}{\operatorname{mk} (x_{1} , y)}$.

the other of h (from the name)

Assume that $a$ is an element of $z$. Then the other of $h$ is an element of $x$ defined as $\operatorname{choose}$ applied to $h$.

the other of h (from the name)

Assume that $a$ is an element of $z$. Then the other of $h$ is an element of $x$.

Let $x$ be a set. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Prod}$ applied to $x$ and $x$. Then we can say that $\operatorname{Rel}$ holds for $x$, $x_{1}$ and $x_{2}$.

Let $s$ be an element of the power set of the set of symmetric squares of $x$. Let $x_{1}$ and $y$ be elements of $x$. Then $\operatorname{ToRel}$ holds for $s$, $x_{1}$ and $y$, if $\MembershipmemMACRoT {s}{\operatorname{mk} (x_{1} , y)}$.

the sum of x1 (from the name)

Let $x_{1}$ be a symmetric square of $M$. Then the sum of $x_{1}$ is an element of $M$ defined as $\operatorname{lift}$ applied to the function that maps $x_{4}$ and $x_{5}$ to $x_{4} + x_{5}$ and $x_{1}$.

Let $s$ be a symmetric square of $x$ such that for all elements $a_{1}$ of $x$, if $a_{1}$ is an element of $s$, then $P$ holds for $a_{1}$. Then $\operatorname{attachWith}$ applied to $s$ and $h$ is a symmetric square of $\SubtypeSet {a}{P (a)}$ defined as $\operatorname{pmap}$ applied to $\operatorname{mk}$, $s$ and $h$.

the diagonal of x1 (from the name)

Let $x_{1}$ be an element of $x$. Then the diagonal of $x_{1}$ is a symmetric square of $x$ defined as $\operatorname{mk}$ applied to $x_{1}$ and $x_{1}$.

the diagonal element of z and h (from the name)

Let $z$ be a symmetric square of $x$ such that $z$ is a diagonal. Then the diagonal element of $z$ and $h$ is an element of $x$.

the diagonal element equivalence (from the name)

The diagonal element equivalence is an element of $\EquivMACRoAE {(\SubtypeSet {a}{\operatorname{IsDiag} (a)})}{x}$.

the diagonal set (from the name)

The diagonal set is an element of the power set of the set of symmetric squares of $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $z$ to the proposition that $z$ is a diagonal.

the equivalence multiset of x (from the name)

Let $x$ be a set. Then the equivalence multiset of $x$ is an element of $\EquivMACRoAE {\mathrm{Sym2} (x)}{(\SubtypeSet {s}{\mathrm{Eq} (\operatorname{card} (s), 2)})}$ defined as the symmetric square of $x$.

the symmetric square of x (from the docstring)

Let $x$ be a set. Then the symmetric square of $x$ is an equivalence from the set of symmetric squares of $x$ to the set of symmetric powers of $x$ and $2$ defined as the composition of the symmetric square and the inverse of the symmetric power equivalence symmetric power.

Assume that $r$ is symmetric. Then $\operatorname{fromRel}$ applied to $\mathrm{sym}$ is an element of the power set of the set of symmetric squares of $x$ defined as $\operatorname{ofPred}$ applied to $\operatorname{lift}$ applied to $r$.

Let $z$ be a symmetric square of $x$ such that $\MembershipmemMACRoT {\operatorname{fromRel} (\mathrm{sym})}{z}$. Let $f$ be a function from elements $a_{1}$ of $x$ and elements $b_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $r$ applied to $a_{1}$ and $b_{1}$ to elements of $\mathrm{motive}$ such that for all elements $a$ and $b$ of $x$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $r$ applied to $a$ and $b$, $\EqtMACRoH {f (a , b , h_{1})}{f (b , a , \mathrm{symm} (h_{1}))}$. Then $\operatorname{fromRelNdrec}$ applied to $z$, $\mathrm{hz}$, $a_{1}$, $b_{1}$, $f$ and $h$ is an element of $\mathrm{motive}$.

Let $x$ be a set. Then $\operatorname{fromRelOrderIso}$ applied to $x$ is an order isomorphism of $\SubtypeSet {r}{\operatorname{Symm} (r)}$ and $\wp \mathrm{Sym2} (x)$.

Let $f$ be a function from elements $a_{1}$ of $x$ and elements $b_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $a_{1}$ and $b_{1}$ such that for all elements $a$ and $b$ of $x$, $\mathrm{HEq}$ holds for $f$ applied to $a$ and $b$ and $f$ applied to $b$ and $a$. Let $z$ be a symmetric square of $x$. Then $\operatorname{hrec}$ applied to $a_{1}$, $b_{1}$, $f$, $h$ and $z$ is an element of $\mathrm{motive}$ applied to $z$.

the lift (from the name)

The lift is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (x , \lambda x_{2} . \mathrm{forall} (x , \lambda x_{3} . \EqtMACRoH {f (x_{2} , x_{3})}{f (x_{3} , x_{2})}))}$ to the set of functions from symmetric squares of $x$ to elements of $x_{1}$.

the lift (from the name)

The lift is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (x , \lambda x_{3} . \mathrm{forall} (x , \lambda x_{4} . \mathrm{forall} (x_{1} , \lambda x_{5} . \mathrm{forall} (x_{1} , \lambda x_{6} . \mathrm{and} (\EqtMACRoH {f (x_{3} , x_{4} , x_{5} , x_{6})}{f (x_{4} , x_{3} , x_{5} , x_{6})}, \EqtMACRoH {f (x_{3} , x_{4} , x_{5} , x_{6})}{f (x_{3} , x_{4} , x_{6} , x_{5})})))))}$ to the set of functions from symmetric squares of $x$ and symmetric squares of $x_{1}$ to elements of $x_{2}$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a symmetric square of $x$. Then the map of $f$ and $x_{2}$ is a symmetric square of $x_{1}$.

Let $a$ and $b$ be elements of $x$. Then $\operatorname{mk}$ applied to $a$ and $b$ is a symmetric square of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{Rel}$ applied to $x$ and $\ProdmkMACRoU {a}{b}$.

the embedding of a (from the name)

Let $a$ be an element of $x$. Then the embedding of $a$ is an embedding of $x$ and the set of symmetric squares of $x$.

the product of x1 (from the name)

Let $x_{1}$ be a symmetric square of $M$. Then the product of $x_{1}$ is an element of $M$ defined as $\operatorname{lift}$ applied to the function that maps $x_{4}$ and $x_{5}$ to $x_{4} \times x_{5}$ and $x_{1}$.

Let $f$ be a function from elements $a_{1}$ of $x$ and elements of $\mathrm{Proof}$ applied to $P$ applied to $a_{1}$ to elements of $x_{1}$. Let $s$ be a symmetric square of $x$ such that for all elements $a$ of $x$, if $a$ is an element of $s$, then $P$ holds for $a$. Then $\operatorname{pmap}$ applied to $a_{1}$, $f$, $s$ and $h$ is a symmetric square of $x_{1}$.

Let $z$ be a symmetric square of $x$. Let $f$ be a function from elements $a_{1}$ of $x$ and elements $b_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $a_{1}$ and $b_{1}$ such that for all elements $a$, $b$, $c$ and $d$ of $x$, for all elements $h_{1}$ of $\mathrm{Proof}$ applied to $\operatorname{Rel}$ applied to $x$, $\ProdmkMACRoU {a}{b}$ and $\ProdmkMACRoU {c}{d}$, $\EqtMACRoH {\operatorname{ndrec} (f (a , b), \operatorname{sound} (h_{1}))}{f (c , d)}$. Then $\operatorname{recOn}$ applied to $z$, $a_{1}$, $b_{1}$, $f$ and $h$ is an element of $\mathrm{motive}$ applied to $z$.

Let $z$ be a symmetric square of $x$. Let $f$ be a function from elements $a$ of $x$ and elements $b$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $a$ and $b$. Then $\operatorname{recOnSubsingleton}$ applied to $z$, $a$, $b$ and $f$ is an element of $\mathrm{motive}$ applied to $z$.

the symmetric square (from the docstring)

The symmetric square is an equivalence from the set of symmetric squares of $x$ to the set of symmetric powers of $x$ and $2$.

the finite set of z (from the name)

Let $z$ be a symmetric square of $x$. Then the finite set of $z$ is a finite set of $x$ defined as the finite set of the multiset of $z$.

the multiset of z (from the name)

Let $z$ be a symmetric square of $x$. Then the multiset of $z$ is a multiset of $x$ defined as $\operatorname{lift}$ applied to the function that maps $x_{3}$ and $x_{4}$ to the multiset of $\operatorname{cons}$ applied to $x_{3}$ and $\operatorname{cons}$ applied to $x_{4}$ and $\operatorname{nil}$ and $z$.

the relative order embedding of x (from the name)

Let $x$ be a set. Then the relative order embedding of $x$ is an order embedding of the power set of the set of symmetric squares of $x$ and the set of functions from elements of $x$ and elements of $x$ to propositions defined as the order embedding of $\operatorname{ToRel}$ and $\mathrm{Sym2\_\_toRel\_mono\_iff}$.

the symmetric power product of f (from the name)

Let $f$ be an element of $\FinsuppMACRoQ {x}{x_{1}}$. Then the symmetric power product of $f$ is a finitely supported function from the set of symmetric squares of $x$ to $x_{1}$ defined as $\operatorname{onFinset}$ applied to the symmetric power of the support of $f$, the function that maps $p$ to the product of the map of $\operatorname{coe}$ applied to $f$ and $p$ and $\mathrm{Finsupp\_\_mem\_sym2\_support\_of\_mul\_ne\_zero}$.

binary tree of x (from the name)

Let $x$ be a set. Then the binary trees of $x$ are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\operatorname{nil}$ and $\mathrm{PULift}$ applied to the set of functions from elements $\mathrm{value}$ of $x$ and binary trees $\mathrm{left}$ of $x$ and binary trees $\mathrm{right}$ of $x$ to elements of $\mathrm{motive}$ applied to the node of $\mathrm{left}$ and $\mathrm{right}$.

the height of x1 (from the name)

Let $x_{1}$ be a binary tree of $x$. Then the height of $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{BinaryTree\_\_height\_\_\_f}$.

the left of x1 (from the name)

Let $x_{1}$ be a binary tree of $x$. Then the left of $x_{1}$ is a binary tree of $x$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a binary tree of $x$. Then the map of $f$ and $x_{2}$ is a binary tree of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{BinaryTree\_\_map\_\_\_f}$ applied to $f$.

$\operatorname{nil}$ is a binary tree of $x$.

the node of left and right (from the name)

Let $\mathrm{value}$ be an element of $x$. Let $\mathrm{left}$ and $\mathrm{right}$ be binary trees of $x$. Then the node of $\mathrm{left}$ and $\mathrm{right}$ is a binary tree of $x$.

the numerator leave of x1 (from the name)

Let $x_{1}$ be a binary tree of $x$. Then the numerator leave of $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{BinaryTree\_\_numLeaves\_\_\_f}$.

the numerator node of x1 (from the name)

Let $x_{1}$ be a binary tree of $x$. Then the numerator node of $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{BinaryTree\_\_numNodes\_\_\_f}$.

the right of x1 (from the name)

Let $x_{1}$ be a binary tree of $x$. Then the right of $x_{1}$ is a binary tree of $x$.

the traverse of f and x3 (from the name)

Let $f$ be a function from elements of $x_{1}$ to elements of $m$ applied to $x_{2}$. Let $x_{3}$ be a binary tree of $x_{1}$. Then the traverse of $f$ and $x_{3}$ is an element of $m$ applied to the set of binary trees of $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{BinaryTree\_\_traverse\_\_\_f}$ applied to $f$.

Let $t$ be a binary tree of $\mathrm{Unit}$. Let $\mathrm{base}$ be an element of $\mathrm{motive}$ applied to $\operatorname{nil}$. Let $\mathrm{ind}$ be a function from binary trees $x$ of $\mathrm{Unit}$ and binary trees $y$ of $\mathrm{Unit}$ and elements of $\mathrm{motive}$ applied to $x$ and elements of $\mathrm{motive}$ applied to $y$ to elements of $\mathrm{motive}$ applied to the node of $x$ and $y$. Then $\operatorname{unitRecOn}$ applied to $t$, $\mathrm{base}$, $x$, $y$ and $\mathrm{ind}$ is an element of $\mathrm{motive}$ applied to $t$ defined as the function that maps $y$ and $\mathrm{ind}$ to $\operatorname{recOn}$ applied to $t$, $\mathrm{base}$, the function that maps $\mathrm{\_u}$ to $x$, $y$ and $\mathrm{ind}$.

the representation of x2 and x3 (from the name)

Let $x_{2}$ be a binary tree of $x$. Let $x_{3}$ be a natural number. Then the representation of $x_{2}$ and $x_{3}$ is an element of $\operatorname{Format}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{instReprBinaryTree\_\_repr\_\_\_f}$ and $x_{3}$.

Let $x_{1}$ be a positive part numerator. Let $x_{2}$ be a binary tree of $x$. Then $\operatorname{get}$ applied to $x_{1}$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{BinaryTree\_\_get\_\_\_f}$ and $x_{2}$.

Let $n$ be a positive part numerator. Let $t$ be a binary tree of $x$. Let $v$ be an element of $x$. Then $\operatorname{getOrElse}$ applied to $n$, $t$ and $v$ is an element of $x$ defined as $\operatorname{getD}$ applied to $\operatorname{get}$ applied to $n$ and $t$ and $v$.

the index of x2 and x3 (from the name)

Let $\mathrm{lt}$ be a function from elements of $x$ and elements of $x$ to propositions. Let $x_{2}$ be an element of $x$. Let $x_{3}$ be a binary tree of $x$. Then the index of $x_{2}$ and $x_{3}$ is an element of $\mathrm{Option}$ applied to the set of positive part numerators defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{BinaryTree\_\_indexOf\_\_\_f}$ applied to $\mathrm{lt}$ and $x_{2}$.

type vector of n (from the name)

Let $n$ be a natural number. Then a type vector of $n$ is an element of the function that maps $n$ to the set of functions from elements of $\mathrm{Fin2}$ applied to $n$ to sets.

arrow of x and x1 (from the name)

Let $x$ and $x_{1}$ be type vectors of $n$. Then an arrow of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of functions from elements $i$ of $\mathrm{Fin2}$ applied to $n$ and elements of $x$ applied to $i$ to elements of $x_{1}$ applied to $i$.

Assume that $\EqtMACRoH {x}{x_{1}}$. Then there is an arrow of $x$ and $x_{1}$.

Assume that $\EqtMACRoH {x}{x_{1}}$. Then there is an arrow of $x_{1}$ and $x$.

curry of x and x1 (from the name)

Let $F$ be a function from type vectors of $n + 1$ to sets. Let $x$ be a set. Let $x_{1}$ be a type vector of $n$. Then a curry of $x$ and $x_{1}$ is an element of the function that maps $F$, $x$ and $x_{1}$ to $F$ applied to $\operatorname{append1}$ applied to $x_{1}$ and $x$.

Let $x$ be a type vector of $n$. Let $p$ be a function from elements of $x_{1}$ to propositions. Let $x_{2}$ be an element of $\operatorname{append1}$ applied to $x$, $x_{1}$ and $i$. Then we can say that $\operatorname{PredLast}$ holds for $x$, $p$ and $x_{2}$.

Let $x$ be a type vector of $n$. Let $p$ be a function from elements of $x_{1}$ to propositions. Then there is an arrow of $\operatorname{append1}$ applied to $x$ and $x_{1}$ and $\operatorname{repeat}$ applied to $n + 1$ and the set of propositions. Proof. Let $x$ be arbitrary. Let $p$ be arbitrary. By True. By x. By TypeVec__const. By p. By TypeVec__splitFun.

Let $x$ be a type vector of $n$. Let $r$ be a function from elements of $x_{1}$ and elements of $x_{2}$ to propositions. Let $x_{3}$ be an element of $\operatorname{append1}$ applied to $x$, $x_{1}$ and $i$. Let $x_{4}$ be an element of $\operatorname{append1}$ applied to $x$, $x_{2}$ and $i$. Then we can say that $\operatorname{RelLast}$ holds for $x$, $r$, $x_{3}$ and $x_{4}$.

Let $x$ be a type vector of $n$. Let $p$ be a function from elements of $x_{1}$ and elements of $x_{1}$ to propositions. Then there is an arrow of the product of $\operatorname{append1}$ applied to $x$ and $x_{1}$ and $\operatorname{append1}$ applied to $x$ and $x_{1}$ and $\operatorname{repeat}$ applied to $n + 1$ and the set of propositions. Proof. Let $x$ be arbitrary. Let $p$ be arbitrary. By x. By TypeVec__repeatEq. By p. By Function__uncurry. By TypeVec__splitFun.

the subtype of x1 (from the name)

Let $x_{1}$ be an arrow of $x$ and $\operatorname{repeat}$ applied to $n$ and the set of propositions. Then the subtype of $x_{1}$ is a type vector of $n$ defined as the function that maps $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{TypeVec\_\_Subtype\_\_\_\_f}$, $x$ and $x_{1}$.

Let $x$ be a type vector of $n$. Let $x_{1}$ be a set. Then there is a type vector of $n + 1$.

Let $H$ be a function from type vectors $x_{1}$ of $n$ and sets $x_{2}$ to elements of $C$ applied to $\operatorname{append1}$ applied to $x_{1}$ and $x_{2}$. Let $x$ be a type vector of $n + 1$. Then $\operatorname{append1Cases}$ applied to $x_{1}$, $x_{2}$, $H$ and $x$ is an element of $C$ applied to $x$.

Let $f$ be an arrow of $x$ and $x_{1}$. Let $g$ be a function from elements of $x_{2}$ to elements of $x_{3}$. Then there is an arrow of $\operatorname{append1}$ applied to $x$ and $x_{2}$ and $\operatorname{append1}$ applied to $x_{1}$ and $x_{3}$. Proof. Let $f$ be arbitrary. Let $g$ be arbitrary. By f. By g. By TypeVec__splitFun.

Let $n$ be a natural number. Let $f$ be a function from sets $t$ and type vectors $v_{1}$ of $n$ to elements of $x$ applied to $\operatorname{append1}$ applied to $v_{1}$ and $t$. Let $v$ be a type vector of $n + 1$. Then $\operatorname{casesCons}$ applied to $n$, $t$, $v_{1}$, $f$ and $v$ is an element of $x$ applied to $v$.

Let $f$ be an element of $x$ applied to $\operatorname{elim0}$. Let $v$ be a type vector of $0$. Then $\operatorname{casesNil}$ applied to $f$ and $v$ is an element of $x$ applied to $v$.

the composition of g and f (from the name)

Let $g$ be an arrow of $x_{1}$ and $x_{2}$. Let $f$ be an arrow of $x$ and $x_{1}$. Then the composition of $g$ and $f$ is an arrow of $x$ and $x_{2}$ defined as the function that maps $i$ and $x_{3}$ to $g$ applied to $i$ and $f$ applied to $i$ and $x_{3}$.

the constant of x1 and x2 (from the name)

Let $x_{1}$ be an element of $x$. Let $x_{2}$ be a type vector of $n$. Then the constant of $x_{1}$ and $x_{2}$ is an arrow of $x_{2}$ and $\operatorname{repeat}$ applied to $n$ and $x$ defined as the function that maps $x_{3}$ to $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{TypeVec\_\_const\_\_\_f}$ applied to $x_{1}$ and $x_{2}$.

the diagonal difference (from the name)

The diagonal difference is an arrow of $x$ and the subtype of $\operatorname{repeatEq}$ applied to $x$ defined as the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{TypeVec\_\_diagSub\_\_\_f}$, $x$ and $x_{2}$.

Let $x$ be a type vector of $n + 1$. Then there is a type vector of $n$. Proof. Let $x$ be arbitrary. Let $i$ be arbitrary. By i. By Fin2__fs. By x.

Let $f$ be an arrow of $x$ and $x_{1}$. Then there is an arrow of $\operatorname{drop}$ applied to $x$ and $\operatorname{drop}$ applied to $x_{1}$. Proof. Let $f$ be arbitrary. Let $i$ be arbitrary. By i. By Fin2__fs. By f.

Let $x$ be a set. Then there is an arrow of $\operatorname{drop}$ applied to $\operatorname{repeat}$ applied to the successor of $n$ and $x$ and $\operatorname{repeat}$ applied to $n$ and $x$. Proof. Let $x$ be arbitrary. Let $x_{1}$ be arbitrary. By x1. By x. By TypeVec__dropRepeat___f. By Fin2__brecOn.

There is an arrow of $\operatorname{append1}$ applied to $\operatorname{drop}$ applied to $x$ and $\operatorname{last}$ applied to $x$ and $x$. Proof. By x. By TypeVec__append1_drop_last. By TypeVec__Arrow__mp.

the identity (from the name)

The identity is an arrow of $x$ and $x$ defined as the function that maps $x_{1}$ and $x_{2}$ to $x_{2}$.

Let $x$ be a type vector of $n + 1$. Then an element of $\operatorname{last}$ applied to $x$ is an element of the function that maps $x$ to $x$ applied to $\operatorname{fz}$.

the last function of f and x2 (from the name)

Let $f$ be an arrow of $x$ and $x_{1}$. Let $x_{2}$ be an element of $\operatorname{last}$ applied to $x$. Then the last function of $f$ and $x_{2}$ is an element of $\operatorname{last}$ applied to $x_{1}$ defined as $f$ applied to $\operatorname{fz}$ and $x_{2}$.

There is an arrow of $x$ and $x_{1}$. Proof. Let $i$ be arbitrary. By i. By Fin2__elim0.

the type vector of x1 (from the name)

Let $x_{1}$ be an element of $\operatorname{repeat}$ applied to $n$, $x$ and $i$. Then the type vector of $x_{1}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $i$, $\mathrm{TypeVec\_\_ofRepeat\_\_\_f}$ and $x_{1}$.

the type vector of p (from the name)

Let $p$ be an arrow of $x$ and $\operatorname{repeat}$ applied to $n$ and the set of propositions. Then the type vector of $p$ is an arrow of the subtype of $p$ and the function that maps $i$ to $\SubtypeSet {x_{1}}{\operatorname{ofRepeat} (p (i , x_{1}))}$ defined as the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{TypeVec\_\_ofSubtype\_\_\_f}$, $x$, $p$ and $x_{2}$.

the type vector of p (from the name)

Let $p$ be an arrow of the product of $x$ and $x$ and $\operatorname{repeat}$ applied to $n$ and the set of propositions. Then the type vector of $p$ is an arrow of the subtype of $p$ and the function that maps $i$ to $\SubtypeSet {x_{1}}{\operatorname{ofRepeat} (p (i , \operatorname{mk} (i , \ProdfstMACRoZ {x_{1}}, \ProdsndMACRoAA {x_{1}})))}$ defined as the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{TypeVec\_\_ofSubtype'\_\_\_f}$, $x$, $p$ and $x_{2}$.

the product of x and x1 (from the name)

Let $x$ and $x_{1}$ be type vectors of $n$. Then the product of $x$ and $x_{1}$ is a type vector of $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{TypeVec\_\_prod\_\_\_f}$, $x$ and $x_{1}$.

the diagonal (from the name)

The diagonal is an arrow of $x$ and the product of $x$ and $x$ defined as the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{TypeVec\_\_prod\_\_diag\_\_\_f}$, $x$ and $x_{2}$.

the first component (from the name)

The first component is an arrow of the product of $x$ and $x_{1}$ and $x$ defined as the function that maps $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{TypeVec\_\_prod\_\_fst\_\_\_f}$, $x$ and $x_{1}$.

the map of x4 and x5 (from the name)

Let $x_{4}$ be an arrow of $x$ and $x_{2}$. Let $x_{5}$ be an arrow of $x_{1}$ and $x_{3}$. Then the map of $x_{4}$ and $x_{5}$ is an arrow of the product of $x$ and $x_{1}$ and the product of $x_{2}$ and $x_{3}$ defined as the function that maps $x_{6}$ and $x_{7}$ to $\operatorname{brecOn}$ applied to $x_{6}$, $\mathrm{TypeVec\_\_prod\_\_map\_\_\_f}$, $x$, $x_{1}$, $x_{2}$, $x_{3}$, $x_{4}$, $x_{5}$ and $x_{7}$.

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $x_{2}$ be an element of $x$ applied to $i$. Let $x_{3}$ be an element of $x_{1}$ applied to $i$. Then $\operatorname{mk}$ applied to $i$, $x_{2}$ and $x_{3}$ is an element of the product of $x$ and $x_{1}$ defined as $\operatorname{brecOn}$ applied to $i$, $\mathrm{TypeVec\_\_prod\_\_mk\_\_\_f}$, $x$, $x_{1}$, $x_{2}$ and $x_{3}$.

the second component (from the name)

The second component is an arrow of the product of $x$ and $x_{1}$ and $x_{1}$ defined as the function that maps $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{TypeVec\_\_prod\_\_snd\_\_\_f}$, $x$ and $x_{1}$.

Let $n$ be a natural number. Let $x$ be a set. Then there is a type vector of $n$. Proof. Let $n$ be arbitrary. Let $x$ be arbitrary. By n. By TypeVec__repeat___f. By x. By Nat__brecOn.

Let $x$ be a type vector of $n$. Then there is an arrow of the product of $x$ and $x$ and $\operatorname{repeat}$ applied to $n$ and the set of propositions. Proof. Let $x$ be arbitrary. By n. By TypeVec__repeatEq___f. By x. By Nat__brecOn.

the split function of f and g (from the name)

Let $f$ be an arrow of $\operatorname{drop}$ applied to $x$ and $\operatorname{drop}$ applied to $x_{1}$. Let $g$ be a function from elements of $\operatorname{last}$ applied to $x$ to elements of $\operatorname{last}$ applied to $x_{1}$. Then the split function of $f$ and $g$ is an arrow of $x$ and $x_{1}$.

the subtype value of p (from the name)

Let $p$ be an arrow of $x$ and $\operatorname{repeat}$ applied to $n$ and the set of propositions. Then the subtype value of $p$ is an arrow of the subtype of $p$ and $x$ defined as the function that maps $x_{1}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{TypeVec\_\_subtypeVal\_\_\_f}$, $x$ and $p$.

There is an arrow of $x$ and $\operatorname{append1}$ applied to $\operatorname{drop}$ applied to $x$ and $\operatorname{last}$ applied to $x$. Proof. By x. By TypeVec__append1_drop_last. By TypeVec__Arrow__mpr.

the subtype of p (from the name)

Let $p$ be an arrow of $x$ and $\operatorname{repeat}$ applied to $n$ and the set of propositions. Then the subtype of $p$ is an arrow of the function that maps $i$ to $\SubtypeSet {x_{1}}{\operatorname{ofRepeat} (p (i , x_{1}))}$ and the subtype of $p$ defined as the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{TypeVec\_\_toSubtype\_\_\_f}$, $x$, $p$ and $x_{2}$.

the subtype of p (from the name)

Let $p$ be an arrow of the product of $x$ and $x$ and $\operatorname{repeat}$ applied to $n$ and the set of propositions. Then the subtype of $p$ is an arrow of the function that maps $i$ to $\SubtypeSet {x_{1}}{\operatorname{ofRepeat} (p (i , \operatorname{mk} (i , \ProdfstMACRoZ {x_{1}}, \ProdsndMACRoAA {x_{1}})))}$ and the subtype of $p$ defined as the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{TypeVec\_\_toSubtype'\_\_\_f}$, $x$, $p$ and $x_{2}$.

Let $n$ be a natural number. Let $t$ and $\mathrm{t'}$ be sets. Let $v$ and $\mathrm{v'}$ be type vectors of $n$. Let $F$ be a function from functions $f$ from elements of $t$ to elements of $\mathrm{t'}$ and arrows $\mathrm{fs1}$ of $v$ and $\mathrm{v'}$ to elements of $x$ applied to $\operatorname{appendFun}$ applied to $\mathrm{fs1}$ and $f$. Let $\mathrm{fs}$ be an arrow of $\operatorname{append1}$ applied to $v$ and $t$ and $\operatorname{append1}$ applied to $\mathrm{v'}$ and $\mathrm{t'}$. Then $\mathrm{TypeVec\_\_typevecCasesCons\_u2082\_}$ applied to $n$, $t$, $\mathrm{t'}$, $v$, $\mathrm{v'}$, $f$, $\mathrm{fs1}$, $F$ and $\mathrm{fs}$ is an element of $x$ applied to $\mathrm{fs}$.

Let $n$ be a natural number. Let $F$ be a function from sets $t$ and sets $\mathrm{t'}$ and functions $f$ from elements of $t$ to elements of $\mathrm{t'}$ and type vectors $v_{1}$ of $n$ and type vectors $\mathrm{v'1}$ of $n$ and arrows $\mathrm{fs1}$ of $v_{1}$ and $\mathrm{v'1}$ to elements of $x$ applied to $\operatorname{append1}$ applied to $v_{1}$ and $t$, $\operatorname{append1}$ applied to $\mathrm{v'1}$ and $\mathrm{t'}$ and $\operatorname{appendFun}$ applied to $\mathrm{fs1}$ and $f$. Let $v$ and $\mathrm{v'}$ be type vectors of $n + 1$. Let $\mathrm{fs}$ be an arrow of $v$ and $\mathrm{v'}$. Then $\mathrm{TypeVec\_\_typevecCasesCons\_u2083\_}$ applied to $n$, $t$, $\mathrm{t'}$, $f$, $v_{1}$, $\mathrm{v'1}$, $\mathrm{fs1}$, $F$, $v$, $\mathrm{v'}$ and $\mathrm{fs}$ is an element of $x$ applied to $v$, $\mathrm{v'}$ and $\mathrm{fs}$.

Let $f$ be an element of $x$ applied to $\operatorname{nilFun}$. Let $f_{1}$ be an arrow of $\operatorname{elim0}$ and $\operatorname{elim0}$. Then $\mathrm{TypeVec\_\_typevecCasesNil\_u2082\_}$ applied to $f$ and $f_{1}$ is an element of $x$ applied to $f_{1}$.

Let $f$ be an element of $x$ applied to $\operatorname{elim0}$, $\operatorname{elim0}$ and $\operatorname{nilFun}$. Let $v$ and $\mathrm{v'}$ be type vectors of $0$. Let $\mathrm{fs}$ be an arrow of $v$ and $\mathrm{v'}$. Then $\mathrm{TypeVec\_\_typevecCasesNil\_u2083\_}$ applied to $f$, $v$, $\mathrm{v'}$ and $\mathrm{fs}$ is an element of $x$ applied to $v$, $\mathrm{v'}$ and $\mathrm{fs}$.

Let $c$ be an element of $\mathrm{UInt8}$. Then $\operatorname{isASCIIAlpha}$ applied to $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{or}$ applied to $\operatorname{isASCIIUpper}$ applied to $c$ and $\operatorname{isASCIILower}$ applied to $c$.

Let $c$ be an element of $\mathrm{UInt8}$. Then $\operatorname{isASCIIAlphanum}$ applied to $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{or}$ applied to $\operatorname{isASCIIAlpha}$ applied to $c$ and $\operatorname{isASCIIDigit}$ applied to $c$.

Let $c$ be an element of $\mathrm{UInt8}$. Then $\operatorname{isASCIIDigit}$ applied to $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{and}$ applied to $\operatorname{decide}$ applied to $\mathrm{Geq} (c , 48)$ and $\operatorname{decide}$ applied to $\mathrm{Leq} (c , 57)$.

Let $c$ be an element of $\mathrm{UInt8}$. Then $\operatorname{isASCIILower}$ applied to $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{and}$ applied to $\operatorname{decide}$ applied to $\mathrm{Geq} (c , 97)$ and $\operatorname{decide}$ applied to $\mathrm{Leq} (c , 122)$.

Let $c$ be an element of $\mathrm{UInt8}$. Then $\operatorname{isASCIIUpper}$ applied to $c$ is an element of $\mathrm{Bool}$ defined as $\operatorname{and}$ applied to $\operatorname{decide}$ applied to $\mathrm{Geq} (c , 65)$ and $\operatorname{decide}$ applied to $\mathrm{Leq} (c , 90)$.

the characteristic of n (from the name)

Let $n$ be an element of $\mathrm{UInt8}$. Then the characteristic of $n$ is an element of $\mathrm{Char}$.

Let $x$ be a set. Let $n$ be a natural number. Then $\operatorname{vectorEquivFin}$ applied to $x$ and $n$ is an equivalence from the set of vectors of $x$ and $n$ to the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$.

Let $v$ be a vector of $x$ and $m$. Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $0$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from natural numbers $n$ and elements $\mathrm{hd}$ of $x$ and vectors $\mathrm{tl}$ of $x$ and $n$ to elements of $\mathrm{motive}$ applied to the successor of $n$ and $\operatorname{cons}$ applied to $\mathrm{hd}$ and $\mathrm{tl}$. Then $\operatorname{casesOn}$ applied to $v$, $\mathrm{nil}$, $n$, $\mathrm{hd}$, $\mathrm{tl}$ and $\mathrm{cons}$ is an element of $\mathrm{motive}$ applied to $m$ and $v$ defined as the function that maps $\mathrm{hd}$, $\mathrm{tl}$ and $\mathrm{cons}$ to $\operatorname{inductionOn}$ applied to $v$, $\mathrm{nil}$, the function that maps $x_{1}$, $\mathrm{hd}$, $\mathrm{tl}$ and $x_{2}$ to $n$ applied to $x_{1}$, $\mathrm{hd}$ and $\mathrm{tl}$, $\mathrm{hd}$, $\mathrm{tl}$ and $\mathrm{cons}$.

Let $x_{2}$ be a vector of $x$ and $m$. Let $x_{3}$ be a vector of $x_{1}$ and $m$. Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $0$, $\operatorname{nil}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from natural numbers $n$ and elements $x_{4}$ of $x$ and elements $y$ of $x_{1}$ and vectors $\mathrm{xs}$ of $x$ and $n$ and vectors $\mathrm{ys}$ of $x_{1}$ and $n$ to elements of $\mathrm{motive}$ applied to the successor of $n$, $\operatorname{cons}$ applied to $x_{4}$ and $\mathrm{xs}$ and $\operatorname{cons}$ applied to $y$ and $\mathrm{ys}$. Then $\mathrm{List\_\_Vector\_\_casesOn\_u2082\_}$ applied to $x_{2}$, $x_{3}$, $\mathrm{nil}$, $n$, $x_{4}$, $y$, $\mathrm{xs}$, $\mathrm{ys}$ and $\mathrm{cons}$ is an element of $\mathrm{motive}$ applied to $m$, $x_{2}$ and $x_{3}$ defined as the function that maps $x_{4}$, $y$, $\mathrm{xs}$, $\mathrm{ys}$ and $\mathrm{cons}$ to $\mathrm{List\_\_Vector\_\_inductionOn\_u2082\_}$ applied to $x_{2}$, $x_{3}$, $\mathrm{nil}$, the function that maps $x_{4}$, $x_{5}$, $y$, $\mathrm{xs}$, $\mathrm{ys}$ and $x_{6}$ to $n$ applied to $x_{4}$, $x_{5}$, $y$, $\mathrm{xs}$ and $\mathrm{ys}$, $x_{4}$, $y$, $\mathrm{xs}$, $\mathrm{ys}$ and $\mathrm{cons}$.

Let $x_{3}$ be a vector of $x$ and $m$. Let $x_{4}$ be a vector of $x_{1}$ and $m$. Let $x_{5}$ be a vector of $x_{2}$ and $m$. Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $0$, $\operatorname{nil}$, $\operatorname{nil}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from natural numbers $n$ and elements $x_{6}$ of $x$ and elements $y$ of $x_{1}$ and elements $z$ of $x_{2}$ and vectors $\mathrm{xs}$ of $x$ and $n$ and vectors $\mathrm{ys}$ of $x_{1}$ and $n$ and vectors $\mathrm{zs}$ of $x_{2}$ and $n$ to elements of $\mathrm{motive}$ applied to the successor of $n$, $\operatorname{cons}$ applied to $x_{6}$ and $\mathrm{xs}$, $\operatorname{cons}$ applied to $y$ and $\mathrm{ys}$ and $\operatorname{cons}$ applied to $z$ and $\mathrm{zs}$. Then $\mathrm{List\_\_Vector\_\_casesOn\_u2083\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$, $\mathrm{nil}$, $n$, $x_{6}$, $y$, $z$, $\mathrm{xs}$, $\mathrm{ys}$, $\mathrm{zs}$ and $\mathrm{cons}$ is an element of $\mathrm{motive}$ applied to $m$, $x_{3}$, $x_{4}$ and $x_{5}$ defined as the function that maps $x_{6}$, $y$, $z$, $\mathrm{xs}$, $\mathrm{ys}$, $\mathrm{zs}$ and $\mathrm{cons}$ to $\mathrm{List\_\_Vector\_\_inductionOn\_u2083\_}$ applied to $x_{3}$, $x_{4}$, $x_{5}$, $\mathrm{nil}$, the function that maps $x_{6}$, $x_{7}$, $y$, $z$, $\mathrm{xs}$, $\mathrm{ys}$, $\mathrm{zs}$ and $x_{8}$ to $n$ applied to $x_{6}$, $x_{7}$, $y$, $z$, $\mathrm{xs}$, $\mathrm{ys}$ and $\mathrm{zs}$, $x_{6}$, $y$, $z$, $\mathrm{xs}$, $\mathrm{ys}$, $\mathrm{zs}$ and $\mathrm{cons}$.

Let $v$ be a vector of $x$ and $n$. Let $\mathrm{nil}$ be an element of $C$ applied to $0$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from natural numbers $n_{1}$ and elements $x_{1}$ of $x$ and vectors $w$ of $x$ and $n_{1}$ and elements of $C$ applied to $n_{1}$ and $w$ to elements of $C$ applied to the successor of $n_{1}$ and $\operatorname{cons}$ applied to $x_{1}$ and $w$. Then $\operatorname{inductionOn}$ applied to $v$, $\mathrm{nil}$, $n_{1}$, $x_{1}$, $w$ and $\mathrm{cons}$ is an element of $C$ applied to $n$ and $v$.

Let $v$ be a vector of $x$ and $n$. Let $w$ be a vector of $x_{1}$ and $n$. Let $\mathrm{nil}$ be an element of $C$ applied to $0$, $\operatorname{nil}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from natural numbers $n_{1}$ and elements $a$ of $x$ and elements $b$ of $x_{1}$ and vectors $x_{2}$ of $x$ and $n_{1}$ and vectors $y$ of $x_{1}$ and $n_{1}$ and elements of $C$ applied to $n_{1}$, $x_{2}$ and $y$ to elements of $C$ applied to the successor of $n_{1}$, $\operatorname{cons}$ applied to $a$ and $x_{2}$ and $\operatorname{cons}$ applied to $b$ and $y$. Then $\mathrm{List\_\_Vector\_\_inductionOn\_u2082\_}$ applied to $v$, $w$, $\mathrm{nil}$, $n_{1}$, $a$, $b$, $x_{2}$, $y$ and $\mathrm{cons}$ is an element of $C$ applied to $n$, $v$ and $w$.

Let $u$ be a vector of $x$ and $n$. Let $v$ be a vector of $x_{1}$ and $n$. Let $w$ be a vector of $x_{2}$ and $n$. Let $\mathrm{nil}$ be an element of $C$ applied to $0$, $\operatorname{nil}$, $\operatorname{nil}$ and $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from natural numbers $n_{1}$ and elements $a$ of $x$ and elements $b$ of $x_{1}$ and elements $c$ of $x_{2}$ and vectors $x_{3}$ of $x$ and $n_{1}$ and vectors $y$ of $x_{1}$ and $n_{1}$ and vectors $z$ of $x_{2}$ and $n_{1}$ and elements of $C$ applied to $n_{1}$, $x_{3}$, $y$ and $z$ to elements of $C$ applied to the successor of $n_{1}$, $\operatorname{cons}$ applied to $a$ and $x_{3}$, $\operatorname{cons}$ applied to $b$ and $y$ and $\operatorname{cons}$ applied to $c$ and $z$. Then $\mathrm{List\_\_Vector\_\_inductionOn\_u2083\_}$ applied to $u$, $v$, $w$, $\mathrm{nil}$, $n_{1}$, $a$, $b$, $c$, $x_{3}$, $y$, $z$ and $\mathrm{cons}$ is an element of $C$ applied to $n$, $u$, $v$ and $w$.

Let $a$ be an element of $x$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $v$ be a vector of $x$ and $n$. Then $\operatorname{insertIdx}$ applied to $a$, $i$ and $v$ is a vector of $x$ and $n + 1$ defined as $\operatorname{insertIdx}$ applied to $v$, $\operatorname{val}$ applied to $i$ and $a$.

the last element of v (from the docstring)

Let $v$ be a vector of $x$ and $n + 1$. Then the last element of $v$ is an element of $x$ defined as $\operatorname{get}$ applied to $v$ and $\operatorname{last}$ applied to $n$.

Let $x_{2}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $m$ applied to $x_{1}$. Then $\operatorname{mOfFn}$ applied to $x_{2}$ is an element of $m$ applied to the set of vectors of $x_{1}$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{List\_\_Vector\_\_mOfFn\_\_\_f}$ and $x_{2}$.

Let $f$ be a function from elements of $x_{1}$ to elements of $m$ applied to $x_{2}$. Let $x_{3}$ be a vector of $x_{1}$ and $n$. Then $\operatorname{mmap}$ applied to $f$ and $x_{3}$ is an element of $m$ applied to the set of vectors of $x_{2}$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{List\_\_Vector\_\_mmap\_\_\_f}$ applied to $f$ and $x_{3}$.

the reverse of v (from the name)

Let $v$ be a vector of $x$ and $n$. Then the reverse of $v$ is a vector of $x$ and $n$ defined as $\operatorname{reverse}$ applied to the list of $v$.

Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $x_{1}$. Let $b$ be an element of $x_{1}$. Let $v$ be a vector of $x$ and $n$. Then $\operatorname{scanl}$ applied to $f$, $b$ and $v$ is a vector of $x_{1}$ and $n + 1$ defined as $\operatorname{scanl}$ applied to $f$, $b$ and the list of $v$.

the set of i and a (from the name)

Let $v$ be a vector of $x$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Let $a$ be an element of $x$. Then the set of $i$ and $a$ is a vector of $x$ and $n$ defined as $\operatorname{set}$ applied to $v$, $\operatorname{val}$ applied to $i$ and $a$.

the array of x1 (from the name)

Let $x_{1}$ be a vector of $x$ and $n$. Then the array of $x_{1}$ is an element of $\mathrm{Array}$ applied to $x$.

the traverse of f and x3 (from the name)

Let $f$ be a function from elements of $x_{1}$ to elements of $F$ applied to $x_{2}$. Let $x_{3}$ be a vector of $x_{1}$ and $n$. Then the traverse of $f$ and $x_{3}$ is an element of $F$ applied to the set of vectors of $x_{2}$ and $n$.

vector of x and n (from the name)

Let $x$ be a set. Let $n$ be a natural number. Then a vector of $x$ and $n$ is an element of the function that maps $x$ and $n$ to $\SubtypeSet {l}{\mathrm{Eq} (\operatorname{length} (l), n)}$.

the congruence of h and x1 (from the name)

Assume that $n = m$. Let $x_{1}$ be a vector of $x$ and $n$. Then the congruence of $h$ and $x_{1}$ is a vector of $x$ and $m$.

Let $x_{1}$ be an element of $x$. Let $x_{2}$ be a vector of $x$ and $n$. Then $\operatorname{cons}$ applied to $x_{1}$ and $x_{2}$ is a vector of $x$ and the successor of $n$.

Let $i$ be a natural number. Let $x_{1}$ be a vector of $x$ and $n$. Then $\operatorname{drop}$ applied to $i$ and $x_{1}$ is a vector of $x$ and $n - i$.

the eliminator of H and l (from the name)

Let $H$ be a function from lists $l$ of elements of $x$ to elements of $C$ applied to $\operatorname{length}$ applied to $l$ and $l$. Let $v$ be a vector of $x$ and $n$. Then the eliminator of $l$ and $H$ is an element of $C$ applied to $n$ and $v$.

Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Let $x_{1}$ be a vector of $x$ and $n$. Then $\operatorname{eraseIdx}$ applied to $i$ and $x_{1}$ is a vector of $x$ and $n - 1$.

Let $l$ be a vector of $x$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{get}$ applied to $l$ and $i$ is an element of $x$.

the head of x1 (from the name)

Let $x_{1}$ be a vector of $x$ and the successor of $n$. Then the head of $x_{1}$ is an element of $x$.

the length of x1 (from the docstring)

Let $x_{1}$ be a vector of $x$ and $n$. Then the length of $x_{1}$ is a natural number defined as $n$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a vector of $x$ and $n$. Then the map of $f$ and $x_{2}$ is a vector of $x_{1}$ and $n$.

Let $f$ be a function from elements of $x$ and elements of $x_{2}$ to elements of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{1}$. Let $x_{3}$ be a vector of $x$ and $n$. Let $x_{4}$ be an element of $x_{2}$. Then $\operatorname{mapAccumr}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\mathrm{Prod}$ applied to $x_{2}$ and the set of vectors of $x_{1}$ and $n$.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ and elements of $x_{2}$ to elements of $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$. Let $x_{4}$ be a vector of $x$ and $n$. Let $x_{5}$ be a vector of $x_{1}$ and $n$. Let $x_{6}$ be an element of $x_{2}$. Then $\mathrm{List\_\_Vector\_\_mapAccumr\_u2082\_}$ applied to $f$, $x_{4}$, $x_{5}$ and $x_{6}$ is an element of $\mathrm{Prod}$ applied to $x_{2}$ and the set of vectors of $x_{3}$ and $n$.

the map of x3 and x4 (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be a vector of $x$ and $n$. Let $x_{4}$ be a vector of $x_{1}$ and $n$. Then the map of $x_{3}$ and $x_{4}$ is a vector of $x_{2}$ and $n$.

$\operatorname{nil}$ is a vector of $x$ and $0$ defined as $\operatorname{nil}$.

the vector of x1 (from the name)

Let $x_{1}$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then the vector of $x_{1}$ is a vector of $x$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{List\_\_Vector\_\_ofFn\_\_\_f}$ and $x_{1}$.

Let $f$ be a function from elements $a$ of $x$ and elements of $\mathrm{Proof}$ applied to $p$ applied to $a$ to elements of $x_{1}$. Let $v$ be a vector of $x$ and $n$ such that for all elements $x_{2}$ of $x$, if $x_{2}$ is an element of the list of $v$, then $p$ holds for $x_{2}$. Then $\operatorname{pmap}$ applied to $a$, $f$, $v$ and $h$ is a vector of $x_{1}$ and $n$.

Let $n$ be a natural number. Let $a$ be an element of $x$. Then $\operatorname{replicate}$ applied to $n$ and $a$ is a vector of $x$ and $n$ defined as $\operatorname{replicate}$ applied to $n$ and $a$.

Let $v$ be a vector of $x$ and $n$. Let $i$ be a natural number. Let $\mathrm{fill}$ be an element of $x$. Then $\operatorname{shiftLeftFill}$ applied to $v$, $i$ and $\mathrm{fill}$ is a vector of $x$ and $n$.

Let $v$ be a vector of $x$ and $n$. Let $i$ be a natural number. Let $\mathrm{fill}$ be an element of $x$. Then $\operatorname{shiftRightFill}$ applied to $v$, $i$ and $\mathrm{fill}$ is a vector of $x$ and $n$.

the tail of x1 (from the docstring)

Let $x_{1}$ be a vector of $x$ and $n$. Then the tail of $x_{1}$ is a vector of $x$ and $n - 1$.

Let $i$ be a natural number. Let $x_{1}$ be a vector of $x$ and $n$. Then $\operatorname{take}$ applied to $i$ and $x_{1}$ is a vector of $x$ and $\MinminMACRoAG {i}{n}$.

the list of v (from the name)

Let $v$ be a vector of $x$ and $n$. Then the list of $v$ is a list of elements of $x$ defined as $v$.

Let $v$ be a vector of $x$ and $n$. Let $\mathrm{nil}$ be an element of $C$ applied to $0$ and $\operatorname{nil}$. Let $\mathrm{snoc}$ be a function from natural numbers $n_{1}$ and vectors $\mathrm{xs}$ of $x$ and $n_{1}$ and elements $x_{1}$ of $x$ to elements of $C$ applied to $n_{1} + 1$ and $\operatorname{snoc}$ applied to $\mathrm{xs}$ and $x_{1}$. Then $\operatorname{revCasesOn}$ applied to $v$, $\mathrm{nil}$, $n_{1}$, $\mathrm{xs}$, $x_{1}$ and $\mathrm{snoc}$ is an element of $C$ applied to $n$ and $v$ defined as the function that maps $\mathrm{xs}$, $x_{1}$ and $\mathrm{snoc}$ to $\operatorname{revInductionOn}$ applied to $v$, $\mathrm{nil}$, the function that maps $x_{1}$, $\mathrm{xs}$, $x_{2}$ and $x_{3}$ to $n_{1}$ applied to $x_{1}$, $\mathrm{xs}$ and $x_{2}$, $\mathrm{xs}$, $x_{1}$ and $\mathrm{snoc}$.

Let $v$ be a vector of $x$ and $n$. Let $\mathrm{nil}$ be an element of $C$ applied to $0$ and $\operatorname{nil}$. Let $\mathrm{snoc}$ be a function from natural numbers $n_{1}$ and vectors $\mathrm{xs}$ of $x$ and $n_{1}$ and elements $x_{1}$ of $x$ and elements of $C$ applied to $n_{1}$ and $\mathrm{xs}$ to elements of $C$ applied to $n_{1} + 1$ and $\operatorname{snoc}$ applied to $\mathrm{xs}$ and $x_{1}$. Then $\operatorname{revInductionOn}$ applied to $v$, $\mathrm{nil}$, $n_{1}$, $\mathrm{xs}$, $x_{1}$ and $\mathrm{snoc}$ is an element of $C$ applied to $n$ and $v$.

Let $v$ be a vector of $x$ and $n$. Let $w$ be a vector of $x_{1}$ and $n$. Let $\mathrm{nil}$ be an element of $C$ applied to $0$, $\operatorname{nil}$ and $\operatorname{nil}$. Let $\mathrm{snoc}$ be a function from natural numbers $n_{1}$ and vectors $\mathrm{xs}$ of $x$ and $n_{1}$ and vectors $\mathrm{ys}$ of $x_{1}$ and $n_{1}$ and elements $x_{2}$ of $x$ and elements $y$ of $x_{1}$ and elements of $C$ applied to $n_{1}$, $\mathrm{xs}$ and $\mathrm{ys}$ to elements of $C$ applied to $n_{1} + 1$, $\operatorname{snoc}$ applied to $\mathrm{xs}$ and $x_{2}$ and $\operatorname{snoc}$ applied to $\mathrm{ys}$ and $y$. Then $\mathrm{List\_\_Vector\_\_revInductionOn\_u2082\_}$ applied to $v$, $w$, $\mathrm{nil}$, $n_{1}$, $\mathrm{xs}$, $\mathrm{ys}$, $x_{2}$, $y$ and $\mathrm{snoc}$ is an element of $C$ applied to $n$, $v$ and $w$.

Let $x_{1}$ be a vector of $x$ and $n$. Let $x_{2}$ be an element of $x$. Then $\operatorname{snoc}$ applied to $x_{1}$ and $x_{2}$ is a vector of $x$ and $n + 1$ defined as $\operatorname{hAppend}$ applied to $x_{1}$ and $\operatorname{cons}$ applied to $x_{2}$ and $\operatorname{nil}$.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $x_{3}$ be a vector of $x$ and $n$. Let $x_{4}$ be a vector of $x_{1}$ and $n$. Then $\operatorname{zipWith}$ applied to $f$, $x_{3}$ and $x_{4}$ is a vector of $x_{2}$ and $n$ defined as $\operatorname{zipWith}$ applied to $f$, $x_{3}$ and $x_{4}$.

vector of x and n (from the name)

Let $x$ be a set. Let $n$ be a natural number. Then a vector of $x$ and $n$ is an element of the function that maps $x$ and $n$ to the set of functions from elements of $\mathrm{Fin2}$ applied to $n$ to elements of $x$.

Let $v$ be a vector of $x$ and $m$. Let $w$ be a vector of $x$ and $n$. Then there is a vector of $x$ and $n + m$. Proof. Let $v$ be arbitrary. Let $w$ be arbitrary. By v. By w. Let $x_{1}$ be arbitrary. Let $a$ be arbitrary. Let $x_{2}$ be arbitrary. Let $\mathrm{IH}$ be arbitrary. By a. By IH. By Vector3__cons. By Vector3__recOn.

Let $a$ be an element of $x$. Let $v$ be a vector of $x$ and $n$. Then there is a vector of $x$ and $n + 1$. Proof. Let $a$ be arbitrary. Let $v$ be arbitrary. Let $i$ be arbitrary. By v. By i. By Fin2__cases'.

Let $H$ be a function from elements $a$ of $x$ and vectors $t$ of $x$ and $n$ to elements of $C$ applied to $\operatorname{cons}$ applied to $a$ and $t$. Let $v$ be a vector of $x$ and $n + 1$. Then $\operatorname{consElim}$ applied to $a$, $t$, $H$ and $v$ is an element of $C$ applied to $v$.

the head of v (from the name)

Let $v$ be a vector of $x$ and $n + 1$. Then the head of $v$ is an element of $x$ defined as $v$ applied to $\operatorname{fz}$.

Let $a$ be an element of $x$. Let $v$ be a vector of $x$ and $n$. Let $i$ be an element of $\mathrm{Fin2}$ applied to $n + 1$. Then there is a vector of $x$ and $n + 1$. Proof. Let $a$ be arbitrary. Let $v$ be arbitrary. Let $i$ be arbitrary. Let $j$ be arbitrary. By a. By v. By i. By j. By Fin2__insertPerm. By Vector3__cons.

There is a vector of $x$ and $0$.

Let $H$ be an element of $C$ applied to $\operatorname{nil}$. Let $v$ be a vector of $x$ and $0$. Then $\operatorname{nilElim}$ applied to $H$ and $v$ is an element of $C$ applied to $v$.

Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $v$ be a vector of $x$ and $n$. Then $\operatorname{nth}$ applied to $i$ and $v$ is an element of $x$ defined as $v$ applied to $i$.

the vector of f (from the name)

Let $f$ be a function from elements of $\mathrm{Fin2}$ applied to $n$ to elements of $x$. Then the vector of $f$ is a vector of $x$ and $n$ defined as $f$.

Let $v$ be a vector of $x$ and $n$. Let $H_{0}$ be an element of $C$ applied to $0$ and $\operatorname{nil}$. Let $\mathrm{Hs}$ be a function from natural numbers $n_{1}$ and elements $a$ of $x$ and vectors $w$ of $x$ and $n_{1}$ and elements of $C$ applied to $n_{1}$ and $w$ to elements of $C$ applied to $n_{1} + 1$ and $\operatorname{cons}$ applied to $a$ and $w$. Then $\operatorname{recOn}$ applied to $v$, $H_{0}$, $n_{1}$, $a$, $w$ and $\mathrm{Hs}$ is an element of $C$ applied to $n$ and $v$ defined as the function that maps $a$, $w$ and $\mathrm{Hs}$ to $\operatorname{brecOn}$ applied to $n$, $\mathrm{Vector3\_\_recOn\_\_\_f}$ applied to $H_{0}$ and $n_{1}$, $v$, $a$, $w$ and $\mathrm{Hs}$.

the tail of v (from the name)

Let $v$ be a vector of $x$ and $n + 1$. Then the tail of $v$ is a vector of $x$ and $n$ defined as the function that maps $i$ to $v$ applied to $\operatorname{fs}$ applied to $i$.

Let $k$ be a natural number. Let $x_{1}$ be a function from vectors of $x$ and $k$ to propositions. Then $\mathrm{VectorAll}$ holds for $k$ and $x_{1}$, if $\operatorname{brecOn}$ holds for $k$, $\mathrm{VectorAll\_\_\_f}$ and $x_{1}$.

Let $p$ be a function from elements of $x$ to propositions. Let $v$ be a vector of $x$ and $n$. Then $\mathrm{VectorAllP}$ holds for $p$ and $v$, if $\operatorname{recOn}$ holds for $v$, $\mathrm{True}$ and the function that maps $x_{1}$, $a$, $v_{1}$ and $\mathrm{IH}$ to $\operatorname{recOn}$ applied to $v_{1}$, $p$ applied to $a$ and the function that maps $x_{2}$, $x_{3}$, $x_{4}$ and $x_{5}$ to the proposition that $p$ holds for $a$ and $\mathrm{IH}$.

Let $k$ be a natural number. Let $x_{1}$ be a function from vectors of $x$ and $k$ to propositions. Then $\mathrm{VectorEx}$ holds for $k$ and $x_{1}$, if $\operatorname{brecOn}$ holds for $k$, $\mathrm{VectorEx\_\_\_f}$ and $x_{1}$.

type of x1 (from the name)

Let $x_{1}$ be a function from elements of $x$ to sets. Then the types of $x_{1}$ are a basic type.

the depth of x3 (from the docstring)

Let $x_{3}$ be a type of $x_{1}$. Then the depth of $x_{3}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{3}$ and $\mathrm{WType\_\_depth\_\_\_f}$.

the eliminator of x3 and x4 (from the name)

Let $x_{2}$ be a set. Let $x_{3}$ be a function from elements of $\Sigma$ applied to the function that maps $a$ to the set of functions from elements of $x_{1}$ applied to $a$ to elements of $x_{2}$ to elements of $x_{2}$. Let $x_{4}$ be a type of $x_{1}$. Then the eliminator of $x_{3}$ and $x_{4}$ is an element of $x_{2}$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{WType\_\_elim\_\_\_f}$ applied to $x_{2}$ and $x_{3}$.

the equivalence sigma of x1 (from the name)

Let $x_{1}$ be a function from elements of $x$ to sets. Then the equivalence sigma of $x_{1}$ is an equivalence from the set of types of $x_{1}$ to $\Sigma$ applied to the function that maps $a$ to the set of functions from elements of $x_{1}$ applied to $a$ to types of $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toSigma}$, $\operatorname{ofSigma}$, $\mathrm{WType\_\_ofSigma\_toSigma}$ and $\mathrm{WType\_\_toSigma\_ofSigma}$.

the type of x2 (from the name)

Let $x_{2}$ be an element of $\Sigma$ applied to the function that maps $a$ to the set of functions from elements of $x_{1}$ applied to $a$ to types of $x_{1}$. Then the type of $x_{2}$ is a type of $x_{1}$.

the sigma of x2 (from the name)

Let $x_{2}$ be a type of $x_{1}$. Then the sigma of $x_{2}$ is an element of $\Sigma$ applied to the function that maps $a$ to the set of functions from elements of $x_{1}$ applied to $a$ to types of $x_{1}$.

list of x (from the name)

Let $x$ be a set. Then the lists of $x$ are a basic type.

Let $x_{1}$ be an element of $x$. Then $\mathrm{WType\_\_List\_u3b1\_\_\_cons}$ applied to $x_{1}$ is a list of $x$.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{WType\_\_List\_u3b1\_\_\_ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to $\mathrm{WType\_\_List\_u3b1\_\_\_nil}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\mathrm{WType\_\_List\_u3b1\_\_\_cons}$ applied to $x_{1}$.

$\mathrm{WType\_\_List\_u3b1\_\_\_nil}$ is a list of $x$.

the list equivalence unit sum of x (from the name)

Let $x$ be a set. Then the list equivalence unit sum of $x$ is an equivalence from the set of lists of $x$ to $\mathrm{Sum}$ applied to $\mathrm{PUnit}$ and $x$.

list of x and x1 (from the name)

Let $x$ be a set. Let $x_{1}$ be a list of $x$. Then the lists of $x$ and $x_{1}$ are a basic type.

natural number (from the name)

The natural numbers are a basic type.

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\mathrm{WType\_\_Nat\_u3b1\_\_\_ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the zero and $\mathrm{PULift}$ applied to $\mathrm{motive}$ applied to the successor.

the successor (from the name)

The successor is a natural number.

the zero (from the name)

The zero is a natural number.

the natural equivalence unit sum unit (from the name)

The natural equivalence unit sum unit is an equivalence from the set of natural numbers to $\mathrm{Sum}$ applied to $\mathrm{PUnit}$ and $\mathrm{PUnit}$.

natural number of x (from the name)

Let $x$ be a natural number. Then the natural numbers of $x$ are a basic type.

the equivalence list of x (from the name)

Let $x$ be a set. Then the equivalence list of $x$ is an equivalence from the set of types of the set of elements of $\mathrm{WType\_\_List\_u3b2\_}$ applied to $x$ to the set of lists of elements of $x$ defined as $\operatorname{mk}$ applied to $\operatorname{toList}$ applied to $x$, $\operatorname{ofList}$ applied to $x$, $\mathrm{WType\_\_leftInverse\_list}$ applied to $x$ and $\mathrm{WType\_\_rightInverse\_list}$ applied to $x$.

the equivalence natural number (from the name)

The equivalence natural number is an equivalence from the set of types of the set of elements of $\mathrm{WType\_\_Nat\_u3b2\_}$ to $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{toNat}$, $\operatorname{ofNat}$, $\mathrm{WType\_\_leftInverse\_nat}$ and $\mathrm{WType\_\_rightInverse\_nat}$.

the type of x and x1 (from the name)

Let $x$ be a set. Let $x_{1}$ be a list of elements of $x$. Then the type of $x$ and $x_{1}$ is a type of the set of elements of $\mathrm{WType\_\_List\_u3b2\_}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{WType\_\_ofList\_\_\_f}$ applied to $x$.

the type of x (from the name)

Let $x$ be a natural number. Then the type of $x$ is a type of the set of elements of $\mathrm{WType\_\_Nat\_u3b2\_}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{WType\_\_ofNat\_\_\_f}$.

the list of x and x1 (from the name)

Let $x$ be a set. Let $x_{1}$ be a type of the set of elements of $\mathrm{WType\_\_List\_u3b2\_}$ applied to $x$. Then the list of $x$ and $x_{1}$ is a list of elements of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{WType\_\_toList\_\_\_f}$ applied to $x$.

the natural number of x (from the name)

Let $x$ be a type of the set of elements of $\mathrm{WType\_\_Nat\_u3b2\_}$. Then the natural number of $x$ is a natural number defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{WType\_\_toNat\_\_\_f}$.

sequence of x (from the name)

Let $x$ be a set. Then a sequence of $x$ is an element of the function that maps $x$ to the set of sequences of $\mathrm{Option}$ applied to $x$.

Let $s$ be a sequence of $x$. Let $a$ be an element of $x$. Then $\operatorname{Mem}$ holds for $s$ and $a$, if $\operatorname{Mem}$ holds for $s$ and $\operatorname{some}$ applied to $a$.

Let $x_{1}$ and $x_{2}$ be sequences of $x$. Then $\operatorname{append}$ applied to $x_{1}$ and $x_{2}$ is a sequence of $x$ defined as $\operatorname{append}$ applied to $x_{1}$ and $x_{2}$.

Let $s$ be a sequence of $x$. Let $f$ be a function from elements of $x$ to sequences of $x_{1}$. Then $\operatorname{bind}$ applied to $s$ and $f$ is a sequence of $x_{1}$ defined as the join of the map of $f$ and $s$.

Let $a$ be an element of $x$. Let $x_{1}$ be a sequence of $x$. Then $\operatorname{cons}$ applied to $a$ and $x_{1}$ is a sequence of $x$ defined as $\operatorname{cons}$ applied to $\operatorname{some}$ applied to $a$ and $x_{1}$.

Let $x_{1}$ be a sequence of $x$. Then $\operatorname{destruct}$ applied to $x_{1}$ is a computation of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and the set of sequences of $x$.

Let $s$ be a sequence of $x$. Let $x_{1}$ be a natural number. Then $\operatorname{drop}$ applied to $s$ and $x_{1}$ is a sequence of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Stream'\_\_WSeq\_\_drop\_\_\_f}$ applied to $s$.

Let $x_{1}$ be a computation of the set of sequences of $x$. Then $\operatorname{flatten}$ applied to $x_{1}$ is a sequence of $x$.

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Then $\mathrm{Stream'\_\_WSeq\_\_get?}$ applied to $s$ and $n$ is a computation of $\mathrm{Option}$ applied to $x$ defined as the head of $\operatorname{drop}$ applied to $s$ and $n$.

the head of s (from the name)

Let $s$ be a sequence of $x$. Then the head of $s$ is a computation of $\mathrm{Option}$ applied to $x$ defined as the map of the function that maps $x_{1}$ to $\operatorname{map}$ applied to $\ProdfstMACRoZ$ and $x_{1}$ and $\operatorname{destruct}$ applied to $s$.

the join of S (from the name)

Let $S$ be a sequence of the set of sequences of $x$. Then the join of $S$ is a sequence of $x$.

the map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be a sequence of $x$. Then the map of $f$ and $x_{2}$ is a sequence of $x_{1}$ defined as the map of $\operatorname{map}$ applied to $f$ and $x_{2}$.

$\operatorname{nil}$ is a sequence of $x$ defined as $\operatorname{nil}$.

the sequence of l (from the name)

Let $l$ be a list of elements of $x$. Then the sequence of $l$ is a sequence of $x$ defined as the sequence of the sequence of $l$.

the sequence of x1 (from the name)

Let $x_{1}$ be a sequence of $x$. Then the sequence of $x_{1}$ is a sequence of $x$ defined as the function that maps $x_{2}$ to $\operatorname{map}$ applied to $\operatorname{some}$ and $x_{2}$ applied to $x_{1}$.

the sequence of l (from the name)

Let $l$ be an element of $\mathrm{Stream'}$ applied to $x$. Then the sequence of $l$ is a sequence of $x$ defined as the sequence of the sequence of $l$.

Let $s$ be a sequence of $x$. Let $\mathrm{nil}$ be an element of $\mathrm{motive}$ applied to $\operatorname{nil}$. Let $\mathrm{cons}$ be a function from elements $x_{1}$ of $x$ and sequences $s_{2}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{cons}$ applied to $x_{1}$ and $s_{2}$. Let $\mathrm{think}$ be a function from sequences $s_{1}$ of $x$ to elements of $\mathrm{motive}$ applied to $\operatorname{think}$ applied to $s_{1}$. Then $\operatorname{recOn}$ applied to $s$, $\mathrm{nil}$, $x_{1}$, $s_{2}$, $\mathrm{cons}$, $s_{1}$ and $\mathrm{think}$ is an element of $\mathrm{motive}$ applied to $s$ defined as the function that maps $\mathrm{cons}$, $s_{1}$ and $\mathrm{think}$ to $\operatorname{recOn}$ applied to $s$, $\mathrm{nil}$, the function that maps $o$ to $\operatorname{recOn}$ applied to $o$, $s_{2}$ and $x_{1}$, $\mathrm{cons}$, $s_{1}$ and $\mathrm{think}$.

Let $a$ be an element of $x$. Then $\operatorname{ret}$ applied to $a$ is a sequence of $x$ defined as the sequence of $\operatorname{cons}$ applied to $a$ and $\operatorname{nil}$.

the tail of s (from the name)

Let $s$ be a sequence of $x$. Then the tail of $s$ is a sequence of $x$ defined as $\operatorname{flatten}$ applied to $\operatorname{map}$ applied to the function that maps $o$ to $\operatorname{recOn}$ applied to $o$, $\operatorname{nil}$ and $\ProdsndMACRoAA$ and $\operatorname{destruct}$ applied to $s$.

Let $x_{1}$ be a sequence of $x$. Then $\operatorname{think}$ applied to $x_{1}$ is a sequence of $x$ defined as $\operatorname{cons}$ applied to $\operatorname{none}$ and $x_{1}$.

the list of s (from the name)

Let $s$ be a sequence of $x$. Then the list of $s$ is a computation of the set of lists of elements of $x$.

s is finite (from the docstring)

Let $s$ be a sequence of $x$. Then we can say that $s$ is finite.

Let $s$ be a sequence of $x$. Let $p$ be a function from elements of $x$ to elements of $\mathrm{Bool}$. Then $\operatorname{all}$ applied to $s$ and $p$ is a computation of $\mathrm{Bool}$.

Let $s$ be a sequence of $x$. Let $p$ be a function from elements of $x$ to elements of $\mathrm{Bool}$. Then $\operatorname{any}$ applied to $s$ and $p$ is a computation of $\mathrm{Bool}$.

the collect of s and n (from the name)

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Then the collect of $s$ and $n$ is a list of elements of $x$ defined as $\operatorname{filterMap}$ applied to $\mathrm{id}$ and $\operatorname{take}$ applied to $n$ and $s$.

the compute of s (from the name)

Let $s$ be a sequence of $x$. Then the compute of $s$ is a sequence of $x$.

the filter of p and x2 (from the name)

Let $p$ be a function from elements of $x$ to propositions. Let $x_{2}$ be a sequence of $x$. Then the filter of $p$ and $x_{2}$ is a sequence of $x$ defined as the filter map of the function that maps $a$ to $\iteMACRoG {p (a)}{\operatorname{some} (a)}{\operatorname{none}}$ and $x_{2}$.

the filter map of f and x2 (from the name)

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x_{1}$. Let $x_{2}$ be a sequence of $x$. Then the filter map of $f$ and $x_{2}$ is a sequence of $x_{1}$.

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a sequence of $x$. Then $\operatorname{find}$ applied to $p$ and $s$ is a computation of $\mathrm{Option}$ applied to $x$ defined as the head of the filter of $p$ and $s$.

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a sequence of $x$. Then $\operatorname{findIndex}$ applied to $p$ and $s$ is a computation of $\Natural$ defined as $\operatorname{map}$ applied to the function that maps $o$ to $\operatorname{getD}$ applied to $o$ and $0$ and the head of $\operatorname{findIndexes}$ applied to $p$ and $s$.

Let $p$ be a function from elements of $x$ to propositions. Let $s$ be a sequence of $x$. Then $\operatorname{findIndexes}$ applied to $p$ and $s$ is a sequence of $\Natural$.

Let $s$ be a sequence of $x$. Then $\operatorname{get}$ applied to $s$ is a list of elements of $x$ defined as $\operatorname{get}$ applied to the list of $s$.

the index of a and x2 (from the name)

Let $a$ be an element of $x$. Let $x_{2}$ be a sequence of $x$. Then the index of $a$ and $x_{2}$ is a computation of $\Natural$ defined as $\operatorname{findIndex}$ applied to $\mathrm{Eq} (a)$ and $x_{2}$.

Let $a$ be an element of $x$. Let $x_{2}$ be a sequence of $x$. Then $\operatorname{indexesOf}$ applied to $a$ and $x_{2}$ is a sequence of $\Natural$ defined as $\operatorname{findIndexes}$ applied to $\mathrm{Eq} (a)$ and $x_{2}$.

Let $s$ be a sequence of $x$. Then $\operatorname{inits}$ applied to $s$ is a sequence of the set of lists of elements of $x$.

Let $s$ be a sequence of $x$. Then $\operatorname{isEmpty}$ applied to $s$ is a computation of $\mathrm{Bool}$ defined as the map of $\operatorname{isNone}$ and the head of $s$.

the length of s (from the name)

Let $s$ be a sequence of $x$. Then the length of $s$ is a computation of $\Natural$.

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Then $\operatorname{removeNth}$ applied to $s$ and $n$ is a sequence of $x$.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x$. Let $a$ be an element of $x$. Let $s$ be a sequence of $x_{1}$. Then $\operatorname{scanl}$ applied to $f$, $a$ and $s$ is a sequence of $x$.

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Then $\operatorname{splitAt}$ applied to $s$ and $n$ is a computation of $\mathrm{Prod}$ applied to the set of lists of elements of $x$ and the set of sequences of $x$.

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Then $\operatorname{take}$ applied to $s$ and $n$ is a sequence of $x$.

the union of s1 and s2 (from the name)

Let $s_{1}$ and $s_{2}$ be sequences of $x$. Then the union of $s_{1}$ and $s_{2}$ is a sequence of $x$.

Let $s$ be a sequence of $x$. Let $n$ be a natural number. Let $a$ be an element of $x$. Then $\operatorname{updateNth}$ applied to $s$, $n$ and $a$ is a sequence of $x$.

Let $x_{2}$ be a sequence of $x$. Let $x_{3}$ be a sequence of $x_{1}$. Then $\operatorname{zip}$ applied to $x_{2}$ and $x_{3}$ is a sequence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as $\operatorname{zipWith}$ applied to $\ProdmkMACRoU$, $x_{2}$ and $x_{3}$.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $s_{1}$ be a sequence of $x$. Let $s_{2}$ be a sequence of $x_{1}$. Then $\operatorname{zipWith}$ applied to $f$, $s_{1}$ and $s_{2}$ is a sequence of $x_{2}$.

s is productive (from the docstring)

Let $s$ be a sequence of $x$. Then we can say that $s$ is productive.

the sequence of s (from the name)

Let $s$ be a sequence of $x$. Then the sequence of $s$ is a sequence of $x$ defined as the function that maps $n$ to $\operatorname{get}$ applied to $\mathrm{Stream'\_\_WSeq\_\_get?}$ applied to $s$ and $n$.

Let $R$ be a function from sequences of $x$ and sequences of $x$ to propositions. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and the set of sequences of $x$. Then $\operatorname{BisimO}$ holds for $R$, $x_{1}$ and $x_{2}$, if $\operatorname{LiftRelO}$ holds for the function that maps $x_{1}$ and $x_{2}$ to $\EqtMACRoH {x_{1}}{x_{2}}$, $R$, $x_{1}$ and $x_{2}$.

Let $x_{1}$ and $x_{2}$ be sequences of $x$. Then $\operatorname{Equiv}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{LiftRel}$ holds for $\mathrm{Eq}$, $x_{1}$ and $x_{2}$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $s$ be a sequence of $x$. Let $t$ be a sequence of $x_{1}$. Then $\operatorname{LiftRel}$ holds for $R$, $s$ and $t$, if there exists a function $C$ from sequences of $x$ and sequences of $x_{1}$ to propositions, such that $C$ holds for $s$ and $t$ and for all sequences $s_{1}$ of $x$, for all sequences $t_{1}$ of $x_{1}$, if $C$ holds for $s_{1}$ and $t_{1}$, then $\operatorname{LiftRel}$ holds for $\operatorname{LiftRelO}$ applied to $R$ and $C$, $\operatorname{destruct}$ applied to $s_{1}$ and $\operatorname{destruct}$ applied to $t_{1}$.

Let $R$ be a function from elements of $x$ and elements of $x_{1}$ to propositions. Let $C$ be a function from sequences of $x$ and sequences of $x_{1}$ to propositions. Let $x_{2}$ be an element of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and the set of sequences of $x$. Let $x_{3}$ be an element of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x_{1}$ and the set of sequences of $x_{1}$. Then we can say that $\operatorname{LiftRelO}$ holds for $R$, $C$, $x_{2}$ and $x_{3}$.

the automorphism group of n (from the docstring)

Let $n$ be a natural number. Then the automorphism group of $n$ is an additive equivalence of the set of additive automorphisms of $\mathrm{ZMod}$ applied to $n$ and $\mathrm{Additive}$ applied to $\UnitsMACRoAO {\mathrm{ZMod} (n)}$.

the residue class equivalence of N (from the name)

Let $N$ be a natural number. Then the residue class equivalence of $N$ is an element of $\EquivMACRoAE {\Natural}{\mathrm{Prod} (\mathrm{ZMod} (N), \Natural)}$.

the cast of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{ZMod}$ applied to $n$. Then the cast of $x_{1}$ is an element of $R$.

the cast homomorphism of h and R (from the name)

Assume that $m$ divides $n$. Let $R$ be a set. Then the cast homomorphism of $h$ and $R$ is a ring homomorphism of $\mathrm{ZMod}$ applied to $n$ and $R$.

Assume that $m$ and $n$ are coprime. Then $\operatorname{chineseRemainder}$ applied to $h$ is a ring isomorphism of $\mathrm{ZMod}$ applied to $m \times n$ and $\mathrm{Prod}$ applied to $\mathrm{ZMod}$ applied to $m$ and $\mathrm{ZMod}$ applied to $n$.

the finite equivalence of n (from the name)

Let $n$ be a natural number. Then the finite equivalence of $n$ is a ring isomorphism of $\mathrm{Fin}$ applied to $n$ and $\mathrm{ZMod}$ applied to $n$.

the inverse of n and x (from the name)

Let $n$ be a natural number. Let $x$ be an element of $\mathrm{ZMod}$ applied to $n$. Then the inverse of $n$ and $x$ is an element of $\mathrm{ZMod}$ applied to $n$.

the lift of n (from the name)

Let $n$ be a natural number. Then the lift of $n$ is an equivalence from $\SubtypeSet {f}{(\EqtMACRoH {f (n)}{0})}$ to the set of additive monoid homomorphisms of $\mathrm{ZMod}$ applied to $n$ and $A$.

the ring isomorphism of R and h1 (from the name)

Let $R$ be a set such that the cardinality of $R$ is equal to $n$. Then the ring isomorphism of $R$ and $h_{1}$ is a ring isomorphism of $\mathrm{ZMod}$ applied to $n$ and $R$ defined as the ring isomorphism of the cast homomorphism of $\mathrm{dvd\_refl}$ applied to $n$ and $R$ and $\mathrm{ZMod\_\_castHom\_bijective}$ applied to $R$ and $h_{1}$.

the ring isomorphism congruence of h (from the name)

Assume that $m = n$. Then the ring isomorphism congruence of $h$ is a ring isomorphism of $\mathrm{ZMod}$ applied to $m$ and $\mathrm{ZMod}$ applied to $n$.

the ring isomorphism of hp and hR (from the name)

Let $R$ be a set. Assume that $p$ is prime. Assume that the cardinality of $R$ is equal to $p$. Then the ring isomorphism of $\mathrm{hp}$ and $\mathrm{hR}$ is a ring isomorphism of $\mathrm{ZMod}$ applied to $p$ and $R$ defined as the ring isomorphism of $R$ and $\mathrm{hR}$.

the unit of x and h (from the name)

Let $x$ be a natural number such that $x$ and $n$ are coprime. Then the unit of $x$ and $h$ is a unit of $\mathrm{ZMod}$ applied to $n$.

the unit equivalence coprime (from the name)

The unit equivalence coprime is an element of $\EquivMACRoAE {\UnitsMACRoAO {\mathrm{ZMod} (n)}}{(\SubtypeSet {x}{(\NatCoprimeMACRoC {\operatorname{val} (x)}{n})})}$.

the value of x (from the name)

Let $x$ be an element of $\mathrm{ZMod}$ applied to $n$. Then the value of $x$ is a natural number.

Let $x$ be a natural number. Then the elements of $\mathrm{ZMod}$ applied to $x$ are a basic type.

the orbit of a and b (from the docstring)

Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then the orbit of $a$ and $b$ is an equivalence from the set of elements of the orbit of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (a)}{x_{4}})}$ and $b$ to $\mathrm{ZMod}$ applied to the minimal period of the function that maps $x_{5}$ to the sum of $a$ and $x_{5}$ and $b$ defined as the composition of the orbit equivalence quotient stabilizer of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (a)}{x_{4}})}$ and $b$ and $\operatorname{toEquiv}$ applied to the quotient of $a$ and $b$.

the quotient of a and b (from the docstring)

Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then the quotient of $a$ and $b$ is an additive equivalence of the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (a)}{x_{4}})}$ and the stabilizer of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{zmultiples} (a)}{x_{5}})}$ and $b$ and $\mathrm{ZMod}$ applied to the minimal period of the function that maps $x_{6}$ to the sum of $a$ and $x_{6}$ and $b$.

Let $a$ be an integer. Then $\operatorname{quotientZMultiplesEquivZMod}$ applied to $a$ is an additive equivalence of the set of quotients of $\Integer$ and $\operatorname{zmultiples}$ applied to $a$ and $\mathrm{ZMod}$ applied to $\IntnatAbsMACRoY {a}$ defined as the composition of the inverse of the quotient additive equivalence of $\mathrm{Int\_\_zmultiples\_natAbs}$ applied to $a$ and $\operatorname{quotientZMultiplesNatEquivZMod}$ applied to $\IntnatAbsMACRoY {a}$.

Let $n$ be a natural number. Then $\operatorname{quotientZMultiplesNatEquivZMod}$ applied to $n$ is an additive equivalence of the set of quotients of $\Integer$ and $\operatorname{zmultiples}$ applied to $n$ and $\mathrm{ZMod}$ applied to $n$ defined as the composition of the inverse of the quotient additive equivalence of $\mathrm{ZMod\_\_ker\_intCastAddHom}$ applied to $n$ and the quotient kernel equivalence of the cast additive homomorphism of $\mathrm{ZMod}$ applied to $n$ and $\operatorname{cast}$.

the orbit of a and b (from the docstring)

Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then the orbit of $a$ and $b$ is an equivalence from the set of elements of the orbit of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{zpowers} (a)}{x_{4}})}$ and $b$ to $\mathrm{ZMod}$ applied to the minimal period of the function that maps $x_{5}$ to $\HSMulhSMulMACRoAL {a}{x_{5}}$ and $b$ defined as the composition of the orbit equivalence quotient stabilizer of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{zpowers} (a)}{x_{4}})}$ and $b$ and $\operatorname{toEquiv}$ applied to the quotient of $a$ and $b$.

the quotient of a and b (from the docstring)

Let $a$ be an element of $x$. Let $b$ be an element of $x_{1}$. Then the quotient of $a$ and $b$ is a multiplicative equivalence of the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{zpowers} (a)}{x_{4}})}$ and the stabilizer of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{zpowers} (a)}{x_{5}})}$ and $b$ and the set of multiplicatives of $\mathrm{ZMod}$ applied to the minimal period of the function that maps $x_{6}$ to $\HSMulhSMulMACRoAL {a}{x_{6}}$ and $b$ defined as $\operatorname{toMultiplicative}$ applied to the quotient of $\operatorname{ofMul}$ applied to $a$ and $b$.

Let $H$ be a subgroup of $G$. Let $g$ be an element of $G$. Then $\operatorname{quotientEquivSigmaZMod}$ applied to $H$ and $g$ is an equivalence from the set of quotients of $G$ and $H$ to $\Sigma$ applied to the function that maps $q$ to $\mathrm{ZMod}$ applied to the minimal period of the function that maps $x_{1}$ to $\HSMulhSMulMACRoAL {g}{x_{1}}$ and $\operatorname{out}$ applied to $q$ defined as the composition of the self equivalence sigma orbit of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{zpowers} (g)}{x_{1}})}$ and the set of quotients of $G$ and $H$ and the right sigma congruence of the function that maps $q$ to the orbit of $g$ and $\operatorname{out}$ applied to $q$.

Let $a$ be an integer. Then $\operatorname{quotientSpanEquivZMod}$ applied to $a$ is a ring isomorphism of the set of quotients of $\Integer$ and the span of $\operatorname{singleton}$ applied to $a$ and $\mathrm{ZMod}$ applied to $\IntnatAbsMACRoY {a}$ defined as the composition of the inverse of the quotient equivalence of $\mathrm{Int\_\_span\_natAbs}$ applied to $a$ and $\operatorname{quotientSpanNatEquivZMod}$ applied to $\IntnatAbsMACRoY {a}$.

Let $n$ be a natural number. Then $\operatorname{quotientSpanNatEquivZMod}$ applied to $n$ is a ring isomorphism of the set of quotients of $\Integer$ and the span of $\operatorname{singleton}$ applied to $n$ and $\mathrm{ZMod}$ applied to $n$.

the equivalence product of n and hn (from the name)

Let $n$ be an element of $\Natural$ such that $n \neq 0$. Then the equivalence product of $n$ and $\mathrm{hn}$ is a ring isomorphism of $\mathrm{ZMod}$ applied to $n$ and the set of functions from elements $p$ of $\SubtypeSet {x}{(\MembershipmemMACRoT {\operatorname{primeFactors} (n)}{x})}$ to elements of $\mathrm{ZMod}$ applied to $p ^ {\NatfactorizationappMACRoI {n}{p}}$ defined as the composition of the ring isomorphism congruence of $\mathrm{Nat\_\_prod\_primeFactors\_coe\_pow\_factorization}$ applied to $\mathrm{hn}$ and the product equivalence product of the function that maps $p$ to $p ^ {\NatfactorizationappMACRoI {n}{p}}$ and $\mathrm{Nat\_\_pairwise\_coprime\_pow\_primeFactors\_factorization}$.

the product equivalence product of a and coprime (from the name)

Let $a$ be a function from elements of $x$ to natural numbers such that $\operatorname{onFun}$ applied to $\NatCoprimeMACRoC$ and $a$ is pairwise. Then the product equivalence product of $a$ and $\mathrm{coprime}$ is a ring isomorphism of $\mathrm{ZMod}$ applied to $\FinsetProd {\FinsetunivMACRoAC}{i}{a (i)}$ and the set of functions from elements $i_{1}$ of $x$ to elements of $\mathrm{ZMod}$ applied to $a$ applied to $i_{1}$.

the unit of n and h (from the name)

Let $n$ be an integer such that $n$ is coprime to $m$. Then the unit of $n$ and $h$ is a unit of $\mathrm{ZMod}$ applied to $m$ defined as $\operatorname{mk}$ applied to $n$, $\operatorname{inv}$ applied to $n$, $\mathrm{ZMod\_\_coe\_int\_mul\_inv\_eq\_one}$ applied to $h$ and $\mathrm{ZMod\_\_coe\_int\_inv\_mul\_eq\_one}$ applied to $h$.

the unit map of hm (from the name)

Assume that $n$ divides $m$. Then the unit map of $\mathrm{hm}$ is a monoid homomorphism of $\UnitsMACRoAO {\mathrm{ZMod} (m)}$ and $\UnitsMACRoAO {\mathrm{ZMod} (n)}$ defined as the map of the monoid homomorphism of the cast homomorphism of $\mathrm{hm}$ and $\mathrm{ZMod}$ applied to $n$.

the value minimum absolute value of x (from the name)

Let $x$ be an element of $\mathrm{ZMod}$ applied to $n$. Then the value minimum absolute value of $x$ is an integer.