Definitions: Mathlib.Data, part 4 of 6

the land of x and x1 (from the name)

Let $x$ and $x_{1}$ be numerators. Then the land of $x$ and $x_{1}$ is a numerator.

Let $x$ and $x_{1}$ be numerators. Then $\operatorname{ldiff}$ applied to $x$ and $x_{1}$ is a numerator.

Let $x$ and $x_{1}$ be numerators. Then $\operatorname{lor}$ applied to $x$ and $x_{1}$ is a numerator.

Let $x$ and $x_{1}$ be numerators. Then $\operatorname{lxor}$ applied to $x$ and $x_{1}$ is a numerator.

the one bit of x (from the name)

Let $x$ be a numerator. Then the one bit of $x$ is a list of natural numbers.

Let $x$ be a numerator. Let $x_{1}$ be a natural number. Then $\operatorname{shiftl}$ applied to $x$ and $x_{1}$ is a numerator.

Let $x$ be a numerator. Let $x_{1}$ be a natural number. Then $\operatorname{shiftr}$ applied to $x$ and $x_{1}$ is a numerator.

the test bit of x and x1 (from the name)

Let $x$ be a numerator. Let $x_{1}$ be a natural number. Then the test bit of $x$ and $x_{1}$ is an element of $\mathrm{Bool}$.

The elements of $\mathrm{NzsNum}$ are a basic type.

the bit of x and x1 (from the name)

Let $x$ be an element of $\mathrm{Bool}$. Let $x_{1}$ be an element of $\mathrm{NzsNum}$. Then the bit of $x$ and $x_{1}$ is an element of $\mathrm{NzsNum}$.

the bit of x (from the name)

Let $x$ be an element of $\mathrm{NzsNum}$. Then the bit of $x$ is an element of $\mathrm{NzsNum}$ defined as the bit of $\operatorname{false}$ and $x$.

the bit of x (from the name)

Let $x$ be an element of $\mathrm{NzsNum}$. Then the bit of $x$ is an element of $\mathrm{NzsNum}$ defined as the bit of $\operatorname{true}$ and $x$.

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 the set of functions from elements $x$ of $\mathrm{Bool}$ to elements of $\mathrm{motive}$ applied to $\operatorname{msb}$ applied to $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\mathrm{Bool}$ and elements $x_{2}$ of $\mathrm{NzsNum}$ to elements of $\mathrm{motive}$ applied to the bit of $x_{1}$ and $x_{2}$.

Let $z$ be a function from elements $b_{1}$ of $\mathrm{Bool}$ to elements of $C$ applied to the zero of $b_{1}$. Let $s$ be a function from elements $b$ of $\mathrm{Bool}$ and numerators $p_{1}$ and elements of $C$ applied to $p_{1}$ to elements of $C$ applied to the bit of $b$ and $p_{1}$. Let $p$ be an element of $\mathrm{NzsNum}$. Then $\operatorname{drec'}$ applied to $b_{1}$, $z$, $b$, $p_{1}$, $s$ and $p$ is an element of $C$ applied to $\operatorname{nz}$ applied to $p$ defined as the function that maps $p_{1}$, $s$ and $p$ to $\operatorname{brecOn}$ applied to $b$, $\mathrm{NzsNum\_\_drec'\_\_\_f}$ applied to $b_{1}$ and $z$, $p_{1}$, $s$ and $p$.

the head of x (from the name)

Let $x$ be an element of $\mathrm{NzsNum}$. Then the head of $x$ is an element of $\mathrm{Bool}$.

Let $x$ be an element of $\mathrm{Bool}$. Then $\operatorname{msb}$ applied to $x$ is an element of $\mathrm{NzsNum}$.

Let $x$ be an element of $\mathrm{NzsNum}$. Then $\operatorname{not}$ applied to $x$ is an element of $\mathrm{NzsNum}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{NzsNum\_\_not\_\_\_f}$.

the sign of x (from the name)

Let $x$ be an element of $\mathrm{NzsNum}$. Then the sign of $x$ is an element of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x$ and $\mathrm{NzsNum\_\_sign\_\_\_f}$.

the tail of x (from the name)

Let $x$ be an element of $\mathrm{NzsNum}$. Then the tail of $x$ is a numerator.

the land of x and x1 (from the name)

Let $x$ and $x_{1}$ be positive part numerators. Then the land of $x$ and $x_{1}$ is a numerator defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_land\_\_\_f}$ and $x_{1}$.

Let $x$ and $x_{1}$ be positive part numerators. Then $\operatorname{ldiff}$ applied to $x$ and $x_{1}$ is a numerator defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_ldiff\_\_\_f}$ and $x_{1}$.

Let $x$ and $x_{1}$ be positive part numerators. Then $\operatorname{lor}$ applied to $x$ and $x_{1}$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_lor\_\_\_f}$ and $x_{1}$.

Let $x$ and $x_{1}$ be positive part numerators. Then $\operatorname{lxor}$ applied to $x$ and $x_{1}$ is a numerator defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_lxor\_\_\_f}$ and $x_{1}$.

the one bit of x and x1 (from the name)

Let $x$ be a positive part numerator. Let $x_{1}$ be a natural number. Then the one bit of $x$ and $x_{1}$ is a list of natural numbers defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_oneBits\_\_\_f}$ and $x_{1}$.

Let $x$ be a positive part numerator. Let $x_{1}$ be a natural number. Then $\operatorname{shiftl}$ applied to $x$ and $x_{1}$ is a positive part numerator defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{PosNum\_\_shiftl\_\_\_f}$ and $x$.

Let $x$ be a positive part numerator. Let $x_{1}$ be a natural number. Then $\operatorname{shiftr}$ applied to $x$ and $x_{1}$ is a numerator defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_shiftr\_\_\_f}$ and $x_{1}$.

the test bit of x and x1 (from the name)

Let $x$ be a positive part numerator. Let $x_{1}$ be a natural number. Then the test bit of $x$ and $x_{1}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{PosNum\_\_testBit\_\_\_f}$ and $x_{1}$.

numerator (from the name)

The numerators are a basic type.

the sum of a and b (from the name)

Let $a$ and $b$ be numerators. Then the sum of $a$ and $b$ is a numerator defined as the sum of $b$ and $\operatorname{false}$.

the bit of x and x1 (from the name)

Let $x$ be an element of $\mathrm{Bool}$. Let $x_{1}$ be a numerator. Then the bit of $x$ and $x_{1}$ is a numerator.

the bit of x (from the name)

Let $x$ be a numerator. Then the bit of $x$ is a numerator defined as the bit of $\operatorname{false}$ and $x$.

the bit of x (from the name)

Let $x$ be a numerator. Then the bit of $x$ is a numerator defined as the bit of $\operatorname{true}$ and $x$.

the bit of x and n (from the name)

Let $x$ be a numerator. Let $n$ be a natural number. Then the bit of $x$ and $n$ is a vector of $\mathrm{Bool}$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{SNum\_\_bits\_\_\_f}$ and $x$.

the sum of x1 and x2 (from the name)

Let $x$ and $x_{1}$ be numerators. Let $x_{2}$ be an element of $\mathrm{Bool}$. Then the sum of $x_{1}$ and $x_{2}$ is a numerator defined as $\operatorname{rec'}$ applied to the function that maps $a$, $p$ and $c$ to $\operatorname{czAdd}$ applied to $c$, $a$ and $p$, the function that maps $a_{1}$, $p_{1}$ and $\mathrm{IH}$ to $\operatorname{rec'}$ applied to the function that maps $b$ and $c_{1}$ to $\operatorname{czAdd}$ applied to $c_{1}$, $b$ and the bit of $a_{1}$ and $p_{1}$ and the function that maps $b_{1}$, $q$, $x$ and $c_{2}$ to the bit of $\operatorname{xor3}$ applied to $a_{1}$, $b_{1}$ and $c_{2}$ and $\mathrm{IH}$ applied to $q$ and $\operatorname{carry}$ applied to $a_{1}$, $b_{1}$ and $c_{2}$, $x$, $x_{1}$ and $x_{2}$.

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 the set of functions from elements $x$ of $\mathrm{Bool}$ to elements of $\mathrm{motive}$ applied to the zero of $x$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $\mathrm{NzsNum}$ to elements of $\mathrm{motive}$ applied to $\operatorname{nz}$ applied to $x_{1}$.

Let $x$ and $x_{1}$ be elements of $\mathrm{Bool}$. Let $x_{2}$ be a numerator. Then $\operatorname{czAdd}$ applied to $x$, $x_{1}$ and $x_{2}$ is a numerator.

Let $z$ be a function from elements $b_{1}$ of $\mathrm{Bool}$ to elements of $C$ applied to the zero of $b_{1}$. Let $s$ be a function from elements $b$ of $\mathrm{Bool}$ and numerators $p_{1}$ and elements of $C$ applied to $p_{1}$ to elements of $C$ applied to the bit of $b$ and $p_{1}$. Let $p$ be a numerator. Then $\operatorname{drec'}$ applied to $b_{1}$, $z$, $b$, $p_{1}$, $s$ and $p$ is an element of $C$ applied to $p$.

the head of x (from the name)

Let $x$ be a numerator. Then the head of $x$ is an element of $\mathrm{Bool}$.

the product of a and x (from the name)

Let $a$ and $x$ be numerators. Then the product of $a$ and $x$ is a numerator defined as $\operatorname{rec'}$ applied to the function that maps $b$ to $\mathrm{cond}$ applied to $b$, $\operatorname{neg}$ applied to $a$ and $0$, the function that maps $b_{1}$, $x$ and $\mathrm{IH}$ to $\mathrm{cond}$ applied to $b_{1}$, the sum of the bit of $\mathrm{IH}$ and $a$ and the bit of $\mathrm{IH}$ and $x$.

the negation of n (from the name)

Let $n$ be a numerator. Then the negation of $n$ is a numerator defined as the successor of $\operatorname{not}$ applied to $n$.

Let $x$ be a numerator. Then $\operatorname{not}$ applied to $x$ is a numerator.

Let $x$ be an element of $\mathrm{NzsNum}$. Then $\operatorname{nz}$ applied to $x$ is a numerator.

the predecessor of x (from the docstring)

Let $x$ be a numerator. Then the predecessor of $x$ is a numerator defined as $\operatorname{rec'}$ applied to the function that maps $b$ to $\mathrm{cond}$ applied to $b$, $\operatorname{not}$ applied to $1$ and $\operatorname{not}$ applied to $0$, the function that maps $b_{1}$, $p$ and $\mathrm{predp}$ to $\mathrm{cond}$ applied to $b_{1}$, the bit of $\operatorname{false}$ and $p$ and the bit of $\operatorname{true}$ and $\mathrm{predp}$ and $x$.

Let $z$ and $s$ be functions from elements of $\mathrm{Bool}$ to elements of $x$. Let $x_{1}$ be a numerator. Then $\operatorname{rec'}$ applied to $z$, $s$ and $x_{1}$ is an element of $x$ defined as $\operatorname{drec'}$ applied to $z$, $s$ and $x_{1}$.

the sign of x (from the name)

Let $x$ be a numerator. Then the sign of $x$ is an element of $\mathrm{Bool}$.

the difference of a and b (from the name)

Let $a$ and $b$ be numerators. Then the difference of $a$ and $b$ is a numerator defined as $a + \operatorname{neg} (b)$.

the successor of x (from the docstring)

Let $x$ be a numerator. Then the successor of $x$ is a numerator defined as $\operatorname{rec'}$ applied to the function that maps $b$ to $\mathrm{cond}$ applied to $b$, $0$ and $1$, the function that maps $b_{1}$, $p$ and $\mathrm{succp}$ to $\mathrm{cond}$ applied to $b_{1}$, the bit of $\operatorname{false}$ and $\mathrm{succp}$ and the bit of $\operatorname{true}$ and $p$ and $x$.

the tail of x (from the name)

Let $x$ be a numerator. Then the tail of $x$ is a numerator.

the test bit of x and x1 (from the name)

Let $x$ be a natural number. Let $x_{1}$ be a numerator. Then the test bit of $x$ and $x_{1}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x$, $\mathrm{SNum\_\_testBit\_\_\_f}$ and $x_{1}$.

the zero of x (from the name)

Let $x$ be an element of $\mathrm{Bool}$. Then the zero of $x$ is a numerator.

the integer of x (from the name)

Let $x$ be a numerator. Then the integer of $x$ is an integer defined as $\operatorname{rec'}$ applied to the function that maps $a$ to $\mathrm{cond}$ applied to $a$, $\operatorname{neg}$ applied to $1$ and $0$, the function that maps $a_{1}$, $\mathrm{\_p}$ and $\mathrm{IH}$ to $\mathrm{cond}$ applied to $a_{1}$, $2 \times \mathrm{IH} + 1$ and $2 \times \mathrm{IH}$ and $x$.

the transfer (from the name)

the transfer (from the name)

n is prime (from the name)

Let $n$ be a numerator. Then $n$ is prime, if the cast numerator of $n$ is prime.

the smallest prime factor of x (from the docstring)

Let $x$ be a numerator. Then the smallest prime factor of $x$ is a positive part numerator.

n is prime (from the name)

Let $n$ be a positive part numerator. Then $n$ is prime, if the cast positive part numerator of $n$ is prime.

the smallest prime factor of x (from the docstring)

Let $x$ be a positive part numerator. Then the smallest prime factor of $x$ is a positive part numerator.

the transfer (from the name)

Let $x_{2}$ be an element of $\mathrm{Option}$ applied to $x$. Let $x_{3}$ be an element of $x_{1}$. Let $x_{4}$ be a function from elements of $x$ to elements of $x_{1}$. Then $\operatorname{casesOn'}$ applied to $x_{2}$, $x_{3}$ and $x_{4}$ is an element of $x_{1}$.

the eliminator of f and x2 (from the name)

Let $b$ be an element of $x_{1}$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{Option}$ applied to $x$. Then the eliminator of $f$ and $x_{2}$ is an element of $x_{1}$.

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 an element of $\mathrm{Option}$ applied to $x_{1}$. Then the traverse of $f$ and $x_{3}$ is an element of $F$ applied to $\mathrm{Option}$ applied to $x_{2}$ defined as $\operatorname{mapA}$ applied to $f$ and $x_{3}$.

the map of a and b (from the name)

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $a$ be an element of $\mathrm{Option}$ applied to $x$. Let $b$ be an element of $\mathrm{Option}$ applied to $x_{1}$. Then the map of $a$ and $b$ is an element of $\mathrm{Option}$ applied to $x_{2}$ defined as $\operatorname{bind}$ applied to $a$ and the function that maps $a_{1}$ to $\operatorname{map}$ applied to $f$ applied to $a_{1}$ and $b$.

Let $x_{2}$ be an element of $\mathrm{Ordering}$. Let $x_{3}$ and $x_{4}$ be elements of $x$. Then we can say that $\operatorname{Compares}$ holds for $x_{2}$, $x_{3}$ and $x_{4}$.

Let $o$ be an element of $\mathrm{Ordering}$. Let $x$ be a function from elements of $\mathrm{Proof}$ applied to $\EqtMACRoH {o}{\operatorname{eq}}$ to elements of $\mathrm{Ordering}$. Then $\operatorname{dthen}$ applied to $o$ and $x$ is an element of $\mathrm{Ordering}$.

the comparison of a and b (from the name)

Let $a$ and $b$ be elements of $x$. Then the comparison of $a$ and $b$ is an element of $\mathrm{Ordering}$ defined as $\mathrm{cmpUsing}$ applied to the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Lt} (x_{3} , x_{4})$, $a$ and $b$.

Let $\mathrm{lt}$ be a function from elements of $x$ and elements of $x$ to propositions. Let $a$ and $b$ be elements of $x$. Then $\mathrm{cmpUsing}$ applied to $\mathrm{lt}$, $a$ and $b$ is an element of $\mathrm{Ordering}$ defined as $\iteMACRoG {\mathrm{lt} (a , b)}{\operatorname{lt}}{(\iteMACRoG {\mathrm{lt} (b , a)}{\operatorname{gt}}{\operatorname{eq}})}$.

x1 is balanced (from the name)

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $x_{1}$ is balanced, if $\operatorname{brecOn}$ holds for $x_{1}$ and $\mathrm{Ordnode\_\_Balanced\_\_\_f}$.

Let $l$ and $r$ be natural numbers. Then $\operatorname{BalancedSz}$ holds for $l$ and $r$, if $l + r \leq 1$ or $l$ is less than or equal to the product of the delta and $r$ and $r$ is less than or equal to the product of the delta and $l$.

Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{3}$ be an element of $\mathrm{WithBot}$ applied to $x$. Let $x_{4}$ be an element of $\mathrm{WithTop}$ applied to $x$. Then $\operatorname{Bounded}$ holds for $x_{2}$, $x_{3}$ and $x_{4}$, if $\operatorname{brecOn}$ holds for $x_{2}$, $\mathrm{Ordnode\_\_Bounded\_\_\_f}$, $x_{3}$ and $x_{4}$.

Let $n$ and $m$ be natural numbers. Then $\operatorname{Raised}$ holds for $n$ and $m$, if $m = n$ or $m = n + 1$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{Sized}$ holds for $x_{1}$, if $\operatorname{brecOn}$ holds for $x_{1}$ and $\mathrm{Ordnode\_\_Sized\_\_\_f}$.

the balance of x1 and r (from the name)

Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the balance of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\iteMACRoG {\mathrm{Leq} (\operatorname{size} (l)+ \operatorname{size} (r), 1)}{\operatorname{node'} (x_{1} , r)}{(\iteMACRoG {\mathrm{Gt} (\operatorname{size} (r), \operatorname{delta} \times \operatorname{size} (l))}{\operatorname{rotateL} (l , x_{1} , r)}{(\iteMACRoG {\mathrm{Gt} (\operatorname{size} (l), \operatorname{delta} \times \operatorname{size} (r))}{\operatorname{rotateR} (l , x_{1} , r)}{\operatorname{node'} (x_{1} , r)})})}$.

the balance of x1 and r (from the name)

Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the balance of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\iteMACRoG {\mathrm{Leq} (\operatorname{size} (l)+ \operatorname{size} (r), 1)}{\operatorname{node'} (x_{1} , r)}{(\iteMACRoG {\mathrm{Gt} (\operatorname{size} (l), \operatorname{delta} \times \operatorname{size} (r))}{\operatorname{rotateR} (l , x_{1} , r)}{\operatorname{node'} (x_{1} , r)})}$.

the balance of x1 and r (from the name)

Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the balance of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\iteMACRoG {\mathrm{Leq} (\operatorname{size} (l)+ \operatorname{size} (r), 1)}{\operatorname{node'} (x_{1} , r)}{(\iteMACRoG {\mathrm{Gt} (\operatorname{size} (r), \operatorname{delta} \times \operatorname{size} (l))}{\operatorname{rotateL} (l , x_{1} , r)}{\operatorname{node'} (x_{1} , r)})}$.

the node of y and r (from the name)

Let $l$, $m$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ and $y$ be elements of $x$. Then the node of $y$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as the node of $y$ and $r$.

the node of y and r (from the name)

Let $l$, $m$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ and $y$ be elements of $x$. Then the node of $y$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as the node of $x_{1}$ and the node of $y$ and $r$.

the node of x4 and x5 (from the name)

Let $x_{1}$, $x_{3}$ and $x_{5}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ and $x_{4}$ be elements of $x$. Then the node of $x_{4}$ and $x_{5}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the node of x4 and x5 (from the name)

Let $x_{1}$, $x_{3}$ and $x_{5}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ and $x_{4}$ be elements of $x$. Then the node of $x_{4}$ and $x_{5}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{realSize}$ applied to $x_{1}$ is a natural number defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Ordnode\_\_realSize\_\_\_f}$.

Let $x_{1}$ and $x_{3}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{rotateL}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

Let $x_{1}$ and $x_{3}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{rotateR}$ applied to $x_{1}$, $x_{2}$ and $x_{3}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the order node of x1 (from the name)

Let $x_{1}$ be a binary tree of $x$. Then the order node of $x_{1}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{BinaryTree\_\_toOrdNode\_\_\_f}$.

Let $x$ be a set. Then the elements of $\mathrm{Ordnode}$ applied to $x$ are a basic type.

Let $P$ be a function from elements of $x$ to propositions. Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{All}$ holds for $P$ and $x_{1}$, if $\operatorname{brecOn}$ holds for $x_{1}$ and $\mathrm{Ordnode\_\_All\_\_\_f}$ applied to $P$.

Let $x_{2}$ be an element of $x$. Let $x_{3}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{Amem}$ holds for $x_{2}$ and $x_{3}$, if $\operatorname{Any}$ holds for the function that maps $y$ to the proposition that $x_{2} \leq y \leq x_{2}$ and $x_{3}$.

Let $P$ be a function from elements of $x$ to propositions. Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{Any}$ holds for $P$ and $x_{1}$, if $\operatorname{brecOn}$ holds for $x_{1}$ and $\mathrm{Ordnode\_\_Any\_\_\_f}$ applied to $P$.

Let $x_{1}$ be an element of $x$. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{Emem}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{Any}$ holds for $\mathrm{Eq} (x_{1})$ and $x_{2}$.

Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{Equiv}$ holds for $x_{1}$ and $x_{2}$, if $\operatorname{size} (x_{1})= \operatorname{size} (x_{2})$ and the list of $x_{1}$ is equal to the list of $x_{2}$.

Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{adjustWith}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_adjustWith\_\_\_f}$ applied to $f$ and $x_{3}$.

Let $f$ be a function from elements of $\mathrm{Option}$ applied to $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{alter}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_alter\_\_\_f}$ applied to $f$ and $x_{3}$.

Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$ such that $\operatorname{All}$ holds for $P$ and $t$. Then $\operatorname{attach'}$ applied to $t$ and $h$ is an element of $\mathrm{Ordnode}$ applied to $\SubtypeSet {a}{P (a)}$ defined as $\operatorname{pmap}$ applied to $\operatorname{mk}$, $t$ and $h$.

the balance of x1 and r (from the name)

Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the balance of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the balance of x1 and r (from the name)

Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the balance of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the balance of x1 and r (from the name)

Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the balance of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$.

Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{3}$ be an element of $\mathrm{Ordnode}$ applied to $x_{1}$. Then $\operatorname{copair}$ applied to $x_{2}$ and $x_{3}$ is an element of $\mathrm{Ordnode}$ applied to $\mathrm{Sum}$ applied to $x$ and $x_{1}$ defined as $\operatorname{merge}$ applied to the map of $\operatorname{inl}$ and $x_{2}$ and the map of $\operatorname{inr}$ and $x_{3}$.

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 natural numbers $\mathrm{size}$ and elements $l$ of $\mathrm{Ordnode}$ applied to $x$ and elements $x_{1}$ of $x$ and elements $r$ of $\mathrm{Ordnode}$ applied to $x$ to elements of $\mathrm{motive}$ applied to the node of $x_{1}$ and $r$.

the delta (from the name)

The delta is a natural number defined as $3$.

the difference of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then the difference of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$, $\mathrm{Ordnode\_\_diff\_\_\_f}$ and $x_{3}$.

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{disjoint}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{Ordnode\_\_disjoint\_\_\_f}$ and $x_{4}$.

Let $i$ be a natural number. Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{drop}$ applied to $i$ and $t$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\iteMACRoG {\mathrm{Leq} (\operatorname{size} (t), i)}{\operatorname{nil}}{\operatorname{dropAux} (t , i)}$.

Let $p$ be a function from elements of $x$ to propositions. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{dropWhile}$ applied to $p$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_dropWhile\_\_\_f}$ applied to $p$.

the dual of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the dual of $x_{1}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Ordnode\_\_dual\_\_\_f}$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{empty}$ applied to $x_{1}$ is an element of $\mathrm{Bool}$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{erase}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_erase\_\_\_f}$ applied to $x_{3}$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{eraseMax}$ applied to $x_{1}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Ordnode\_\_eraseMax\_\_\_f}$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{eraseMin}$ applied to $x_{1}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Ordnode\_\_eraseMin\_\_\_f}$.

the filter of p and x2 (from the name)

Let $p$ be a function from elements of $x$ to propositions. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the filter of $p$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_filter\_\_\_f}$ applied to $p$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{find}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_find\_\_\_f}$ applied to $x_{3}$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findGe}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_findGe\_\_\_f}$ applied to $x_{3}$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findGt}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_findGt\_\_\_f}$ applied to $x_{3}$.

Let $x_{3}$ be an element of $x$. Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findIndex}$ applied to $x_{3}$ and $t$ is an element of $\mathrm{Option}$ applied to $\Natural$ defined as $\operatorname{findIndexAux}$ applied to $x_{3}$, $t$ and $0$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findLe}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_findLe\_\_\_f}$ applied to $x_{3}$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findLt}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_findLt\_\_\_f}$ applied to $x_{3}$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findMax}$ applied to $x_{1}$ is an element of $\mathrm{Option}$ applied to $x$.

Let $x_{1}$ be an element of $x$. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findMax'}$ applied to $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{Ordnode\_\_findMax'\_\_\_f}$ and $x_{1}$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{findMin}$ applied to $x_{1}$ is an element of $\mathrm{Option}$ applied to $x$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{findMin'}$ applied to $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Ordnode\_\_findMin'\_\_\_f}$ and $x_{2}$.

the fold of f and x2 (from the name)

Let $z$ be an element of $x_{1}$. Let $f$ be a function from elements of $x_{1}$ and elements of $x$ and elements of $x_{1}$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the fold of $f$ and $x_{2}$ is an element of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_fold\_\_\_f}$ applied to $z$ and $f$.

Let $f$ be a function from elements of $x_{1}$ and elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Let $x_{3}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{foldl}$ applied to $f$, $x_{2}$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{Ordnode\_\_foldl\_\_\_f}$ applied to $f$ and $x_{2}$.

Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{1}$. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{3}$ be an element of $x_{1}$. Then $\operatorname{foldr}$ applied to $f$, $x_{2}$ and $x_{3}$ is an element of $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{Ordnode\_\_foldr\_\_\_f}$ applied to $f$ and $x_{3}$.

the glue of x1 and x2 (from the name)

Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then the glue of $x_{1}$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the image of f and t (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the image of $f$ and $t$ is an element of $\mathrm{Ordnode}$ applied to $x_{1}$ defined as $\operatorname{ofList}$ applied to $\operatorname{map}$ applied to $f$ and the list of $t$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{insert}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_insert\_\_\_f}$ applied to $x_{3}$.

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{insert'}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_insert'\_\_\_f}$ applied to $x_{3}$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be an element of $x$. Then $\operatorname{insertMax}$ applied to $x_{1}$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Ordnode\_\_insertMax\_\_\_f}$ and $x_{2}$.

Let $x_{1}$ be an element of $x$. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{insertMin}$ applied to $x_{1}$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_insertMin\_\_\_f}$ applied to $x_{1}$.

Let $f$ be a function from elements of $x$ to elements of $x$. Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{insertWith}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_insertWith\_\_\_f}$ applied to $f$ and $x_{3}$.

the intersection of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then the intersection of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{Ordnode\_\_inter\_\_\_f}$ and $x_{4}$.

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{isSubset}$ applied to $x_{3}$ and $x_{4}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{and}$ applied to $\operatorname{decide}$ applied to $\mathrm{Leq} (\operatorname{size} (x_{3}), \operatorname{size} (x_{4}))$ and $\operatorname{isSubsetAux}$ applied to $x_{3}$ and $x_{4}$.

the link of x1 and x2 (from the name)

Let $l$ and $x_{2}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the link of $x_{1}$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $l$, $\mathrm{Ordnode\_\_link\_\_\_f}$ applied to $x_{1}$ and $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 an element of $\mathrm{Ordnode}$ applied to $x$. Then the map of $f$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x_{1}$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_map\_\_\_f}$ applied to $f$.

the membership of x3 and x4 (from the name)

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the membership of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Bool}$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_mem\_\_\_f}$ applied to $x_{3}$.

Let $l$ and $x_{1}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{merge}$ applied to $l$ and $x_{1}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{recOn}$ applied to $l$, the function that maps $r$ to $r$, the function that maps $\mathrm{ls}$, $\mathrm{ll}$, $\mathrm{lx}$, $\mathrm{lr}$, $x_{1}$, $\mathrm{IHlr}$ and $r_{1}$ to $\operatorname{recOn}$ applied to $r_{1}$, the node of $\mathrm{lx}$ and $\mathrm{lr}$ and the function that maps $\mathrm{rs}$, $\mathrm{rl}$, $\mathrm{rx}$, $\mathrm{rr}$, $\mathrm{IHrl}$ and $x_{2}$ to $\iteMACRoG {\mathrm{Lt} (\operatorname{delta} \times \mathrm{ls} , \mathrm{rs})}{\operatorname{balanceL} (\mathrm{rx} , \mathrm{rr})}{(\iteMACRoG {\mathrm{Lt} (\operatorname{delta} \times \mathrm{rs} , \mathrm{ls})}{\operatorname{balanceR} (\mathrm{lx} , \mathrm{IHlr} (\operatorname{node} (\mathrm{rx} , \mathrm{rr})))}{\operatorname{glue} (\operatorname{node} (\mathrm{lx} , \mathrm{lr}), \operatorname{node} (\mathrm{rx} , \mathrm{rr}))})}$ and $x_{1}$.

$\operatorname{nil}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the node of x1 and r (from the name)

Let $\mathrm{size}$ be a natural number. Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the node of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the node of x1 and r (from the name)

Let $l$ and $r$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{1}$ be an element of $x$. Then the node of $x_{1}$ and $r$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as the node of $x_{1}$ and $r$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be a natural number. Then $\operatorname{nth}$ 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{Ordnode\_\_nth\_\_\_f}$ and $x_{2}$.

Let $x_{1}$ be a list of elements of $x$. Then $\operatorname{ofAscList}$ applied to $x_{1}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

Let $l$ be a list of elements of $x$. Then $\operatorname{ofList}$ applied to $l$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{foldr}$ applied to $\operatorname{insert}$, $\operatorname{nil}$ and $l$.

Let $x_{3}$ be a list of elements of $x$. Then $\operatorname{ofList'}$ applied to $x_{3}$ is an element of $\mathrm{Ordnode}$ applied to $x$.

the partition of p and x2 (from the name)

Let $p$ be a function from elements of $x$ to propositions. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the partition of $p$ and $x_{2}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Ordnode}$ applied to $x$ and $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_partition\_\_\_f}$ applied to $p$.

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 $t$ be an element of $\mathrm{Ordnode}$ applied to $x$ such that $\operatorname{All}$ holds for $P$ and $t$. Then $\operatorname{pmap}$ applied to $a$, $f$, $t$ and $h$ is an element of $\mathrm{Ordnode}$ applied to $x_{1}$ defined as the function that maps $h$ to $\operatorname{brecOn}$ applied to $f$, $\mathrm{Ordnode\_\_pmap\_\_\_f}$ applied to $a$, $t$ and $h$.

the powerset of t (from the name)

Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the powerset of $t$ is an element of $\mathrm{Ordnode}$ applied to $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{insertMin}$ applied to $\operatorname{nil}$ and $\operatorname{foldr}$ applied to the function that maps $x_{1}$ and $\mathrm{ts}$ to the glue of $\operatorname{insertMin}$ applied to the singleton of $x_{1}$ and the map of $\operatorname{insertMin}$ applied to $x_{1}$ and $\mathrm{ts}$ and $\mathrm{ts}$, $t$ and $\operatorname{nil}$.

the product of x2 and x3 (from the name)

Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{3}$ be an element of $\mathrm{Ordnode}$ applied to $x_{1}$. Then the product of $x_{2}$ and $x_{3}$ is an element of $\mathrm{Ordnode}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ defined as the fold of the function that maps $x_{4}$, $a$ and $x_{5}$ to $\operatorname{merge}$ applied to $x_{4}$ and $\operatorname{merge}$ applied to the map of $\ProdmkMACRoU {a}$ and $x_{3}$ and $x_{5}$ and $x_{2}$.

the ratio (from the name)

The ratio is a natural number defined as $2$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be a natural number. Then $\operatorname{removeNth}$ applied to $x_{1}$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Ordnode\_\_removeNth\_\_\_f}$ and $x_{2}$.

the representation of o and n (from the name)

Let $o$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $n$ be a natural number. Then the representation of $o$ and $n$ is an element of $\operatorname{Format}$ defined as $\operatorname{brecOn}$ applied to $o$ and $\mathrm{Ordnode\_\_repr\_\_\_f}$ applied to $n$.

the singleton of a (from the name)

Let $a$ be an element of $x$. Then the singleton of $a$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as the node of $a$ and $\operatorname{nil}$.

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{size}$ applied to $x_{1}$ is a natural number.

the span of p and x2 (from the name)

Let $p$ be a function from elements of $x$ to propositions. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the span of $p$ and $x_{2}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Ordnode}$ applied to $x$ and $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_span\_\_\_f}$ applied to $p$.

the split of x3 and x4 (from the name)

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the split of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Ordnode}$ applied to $x$ and $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_split\_\_\_f}$ applied to $x_{3}$.

the split of x3 and x4 (from the name)

Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the split of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Ordnode}$ applied to $x$ and $\mathrm{Prod}$ applied to $\mathrm{Option}$ applied to $x$ and $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_split3\_\_\_f}$ applied to $x_{3}$.

Let $i$ be a natural number. Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{splitAt}$ applied to $i$ and $t$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Ordnode}$ applied to $x$ and $\mathrm{Ordnode}$ applied to $x$ defined as $\iteMACRoG {\mathrm{Leq} (\operatorname{size} (t), i)}{(\ProdmkMACRoU {t}{\operatorname{nil}})}{\operatorname{splitAtAux} (t , i)}$.

the split maximum of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the split maximum of $x_{1}$ is an element of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $\mathrm{Ordnode}$ applied to $x$ and $x$.

the split maximum of x2 and x3 (from the name)

Let $x_{1}$ and $x_{3}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be an element of $x$. Then the split maximum of $x_{2}$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to $\mathrm{Ordnode}$ applied to $x$ and $x$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{Ordnode\_\_splitMax'\_\_\_f}$, $x_{1}$ and $x_{2}$.

the split minimum of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the split minimum of $x_{1}$ is an element of $\mathrm{Option}$ applied to $\mathrm{Prod}$ applied to $x$ and $\mathrm{Ordnode}$ applied to $x$.

the split minimum of x2 and x3 (from the name)

Let $x_{1}$ and $x_{3}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Let $x_{2}$ be an element of $x$. Then the split minimum of $x_{2}$ and $x_{3}$ is an element of $\mathrm{Prod}$ applied to $x$ and $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$, $\mathrm{Ordnode\_\_splitMin'\_\_\_f}$, $x_{2}$ and $x_{3}$.

Let $i$ be a natural number. Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{take}$ applied to $i$ and $t$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\iteMACRoG {\mathrm{Leq} (\operatorname{size} (t), i)}{t}{\operatorname{takeAux} (t , i)}$.

Let $p$ be a function from elements of $x$ to propositions. Let $x_{2}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{takeWhile}$ applied to $p$ and $x_{2}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{2}$ and $\mathrm{Ordnode\_\_takeWhile\_\_\_f}$ applied to $p$.

the binary tree of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the binary tree of $x_{1}$ is a binary tree of $x$ defined as $\operatorname{brecOn}$ applied to $x_{1}$ and $\mathrm{Ordnode\_\_toBinaryTree\_\_\_f}$.

the list of t (from the name)

Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then the list of $t$ is a list of elements of $x$ defined as $\operatorname{foldr}$ applied to $\operatorname{cons}$, $t$ and $\operatorname{nil}$.

Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{toRevList}$ applied to $t$ is a list of elements of $x$ defined as $\operatorname{foldl}$ applied to $\mathrm{flip}$ applied to $\operatorname{cons}$, $\operatorname{nil}$ and $t$.

the union of x3 and x4 (from the name)

Let $x_{3}$ and $x_{4}$ be elements of $\mathrm{Ordnode}$ applied to $x$. Then the union of $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{3}$, $\mathrm{Ordnode\_\_union\_\_\_f}$ and $x_{4}$.

Let $f$ be a function from elements of $x$ to elements of $\mathrm{Option}$ applied to $x$. Let $x_{3}$ be an element of $x$. Let $x_{4}$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $\operatorname{updateWith}$ applied to $f$, $x_{3}$ and $x_{4}$ is an element of $\mathrm{Ordnode}$ applied to $x$ defined as $\operatorname{brecOn}$ applied to $x_{4}$ and $\mathrm{Ordnode\_\_updateWith\_\_\_f}$ applied to $f$ and $x_{3}$.

t is valid (from the name)

Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Then $t$ is valid, if the top is valid with respect to $t$.

hi is valid with respect to t (from the name)

Let $\mathrm{lo}$ be an element of $\mathrm{WithBot}$ applied to $x$. Let $t$ be an element of $\mathrm{Ordnode}$ applied to $x$. Let $\mathrm{hi}$ be an element of $\mathrm{WithTop}$ applied to $x$. Then we can say that $\mathrm{hi}$ is valid with respect to $t$.

Let $x$ be a set. Then an element of $\mathrm{Ordset}$ applied to $x$ is an element of the function that maps $x$ to $\SubtypeSet {t}{\operatorname{Valid} (t)}$.

s is empty (from the name)

Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then $s$ is empty, if $\EqtMACRoH {s}{\operatorname{emptyCollection}}$.

Let $x_{3}$ be an element of $x$. Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then $\operatorname{erase}$ applied to $x_{3}$ and $s$ is an element of $\mathrm{Ordset}$ applied to $x$ defined as $\operatorname{erase}$ applied to $x_{3}$ and $s$.

Let $x_{3}$ be an element of $x$. Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then $\operatorname{find}$ applied to $x_{3}$ and $s$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\operatorname{find}$ applied to $x_{3}$ and $s$.

Let $x_{3}$ be an element of $x$. Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then $\operatorname{insert}$ applied to $x_{3}$ and $s$ is an element of $\mathrm{Ordset}$ applied to $x$ defined as $\operatorname{insert}$ applied to $x_{3}$ and $s$.

Let $x_{3}$ be an element of $x$. Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then $\operatorname{insert'}$ applied to $x_{3}$ and $s$ is an element of $\mathrm{Ordset}$ applied to $x$ defined as $\operatorname{insert'}$ applied to $x_{3}$ and $s$.

the map of f and s (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{2}$ such that $\mathrm{StrictMono}$ holds for $f$. Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then the map of $f$ and $s$ is an element of $\mathrm{Ordset}$ applied to $x_{2}$ defined as the map of $f$ and $s$.

the membership of x3 and s (from the name)

Let $x_{3}$ be an element of $x$. Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then the membership of $x_{3}$ and $s$ is an element of $\mathrm{Bool}$ defined as $\operatorname{decide}$ applied to $\MembershipmemMACRoT {s}{x_{3}}$.

$\operatorname{nil}$ is an element of $\mathrm{Ordset}$ applied to $x$ defined as $\operatorname{nil}$.

the singleton of a (from the name)

Let $a$ be an element of $x$. Then the singleton of $a$ is an element of $\mathrm{Ordset}$ applied to $x$ defined as $\operatorname{singleton}$ applied to $a$.

Let $s$ be an element of $\mathrm{Ordset}$ applied to $x$. Then $\operatorname{size}$ applied to $s$ is a natural number defined as $\operatorname{size}$ applied to $s$.

function of x and x1 (from the name)

Let $x$ and $x_{1}$ be sets. Then a function of $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of functions from elements of $x$ to parts of $x_{1}$.

the domain of f (from the docstring)

Let $f$ be a function of $x$ and $x_{1}$. Then the domain of $f$ is an element of $\wp x$ defined as $\operatorname{ofPred}$ applied to the function that maps $a$ to the proposition that $f$ applied to $a$ is a domain.

Let $f$ be a function of $x$ and $x_{1}$. Let $s$ be an element of the domain of $f$. Then $\operatorname{asSubtype}$ applied to $f$ and $s$ is an element of $x_{1}$.

Let $f$ be a function of $x$ and $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to functions of $x$ and $x_{2}$. Then there is a function of $x$ and $x_{2}$. Proof. Let $f$ be arbitrary. Let $g$ be arbitrary. Let $a$ be arbitrary. By a. By f. Let $b$ be arbitrary. By b. By a. By g. By Part__bind.

the composition of f and g (from the name)

Let $f$ be a function of $x_{1}$ and $x_{2}$. Let $g$ be a function of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a function of $x$ and $x_{2}$ defined as the function that maps $a$ to $\operatorname{bind}$ applied to $g$ applied to $a$ and $f$.

Let $f$ be a function of $x$ and $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Then $\operatorname{core}$ applied to $f$ and $s$ is an element of $\wp x$ defined as $\operatorname{core}$ applied to the graph of $f$ and $s$.

the equivalence subtype (from the name)

The equivalence subtype is an equivalence from the set of functions of $x$ and $x_{1}$ to $\Sigma$ applied to the function that maps $p$ to the set of functions from elements of $\SubtypeSet {x_{3}}{p (x_{3})}$ to elements of $x_{1}$.

Let $f$ be a function of $x$ and $x_{1}$. Let $x_{2}$ be an element of $x$. Then $\operatorname{evalOpt}$ applied to $f$ and $x_{2}$ is an element of $\mathrm{Option}$ applied to $x_{1}$ defined as the option of $f$ applied to $x_{2}$.

Let $f$ be a function of $x$ and $\mathrm{Sum}$ applied to $x_{1}$ and $x$. Then there is a function of $x$ and $x_{1}$.

Assume that $\MembershipmemMACRoT {\operatorname{fix} (f , a)}{b}$. Let $H$ be a function from elements $\mathrm{a'}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{fix} (f , \mathrm{a'})}{b}$ and functions from elements $\mathrm{a''}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {f (\mathrm{a'})}{\operatorname{inr} (\mathrm{a''})}$ to elements of $C$ applied to $\mathrm{a''}$ to elements of $C$ applied to $\mathrm{a'}$. Then $\operatorname{fixInduction}$ applied to $h$, $\mathrm{a'}$ and $H$ is an element of $C$ applied to $a$.

Assume that $\MembershipmemMACRoT {\operatorname{fix} (f , a)}{b}$. Let $\mathrm{hbase}$ be a function from elements $\mathrm{a\_final}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {f (\mathrm{a\_final})}{\operatorname{inl} (b)}$ to elements of $C$ applied to $\mathrm{a\_final}$. Let $\mathrm{hind}$ be a function from elements $x_{2}$ of $x$ and elements $x_{3}$ of $x$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{fix} (f , x_{3})}{b}$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {f (x_{2})}{\operatorname{inr} (x_{3})}$ and elements of $C$ applied to $x_{3}$ to elements of $C$ applied to $x_{2}$. Then $\operatorname{fixInduction'}$ applied to $h$, $\mathrm{a\_final}$, $\mathrm{hbase}$, $x_{2}$, $x_{3}$ and $\mathrm{hind}$ is an element of $C$ applied to $a$.

the function of f and a (from the name)

Let $f$ be a function of $x$ and $x_{1}$. Let $a$ be an element of $x$ such that $a$ is an element of the domain of $f$. Then the function of $f$ and $a$ is an element of $x_{1}$ defined as $\operatorname{get}$ applied to $f$ applied to $a$ and $h$.

the graph of f (from the name)

Let $f$ be a function of $x$ and $x_{1}$. Then the graph of $f$ is an element of $\wp \mathrm{Prod} (x , x_{1})$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to $\MembershipmemMACRoT {f (\ProdfstMACRoZ {p})}{\ProdsndMACRoAA {p}}$.

the graph of f (from the name)

Let $f$ be a function of $x$ and $x_{1}$. Then the graph of $f$ is a set relation of $x$ and $x_{1}$.

the identity of x (from the docstring)

Let $x$ be a set. Then the identity of $x$ is a function of $x$ and $x$ defined as $\operatorname{some}$.

the image of f and s (from the name)

Let $f$ be a function of $x$ and $x_{1}$. Let $s$ be an element of $\wp x$. Then the image of $f$ and $s$ is an element of $\wp x_{1}$ defined as the image of the graph of $f$ and $s$.

the lift of f (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the lift of $f$ is a function of $x$ and $x_{1}$ defined as the function that maps $a$ to $\operatorname{some}$ applied to $f$ applied to $a$.

the map of f and g (from the name)

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

the preimage of f and s (from the name)

Let $f$ be a function of $x$ and $x_{1}$. Let $s$ be an element of $\wp x_{1}$. Then the preimage of $f$ and $s$ is an element of $\wp x$ defined as the preimage of the graph of $f$ and $s$.

the product lift of f and g (from the name)

Let $f$ be a function of $x$ and $x_{1}$. Let $g$ be a function of $x$ and $x_{2}$. Then the product lift of $f$ and $g$ is a function of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

the product map of f and g (from the name)

Let $f$ be a function of $x$ and $x_{2}$. Let $g$ be a function of $x_{1}$ and $x_{3}$. Then the product map of $f$ and $g$ is a function of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.

Let $x_{2}$ be an element of $x_{1}$. Then there is a function of $x$ and $x_{1}$. Proof. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. By x2. By Part__some.

the range of f (from the docstring)

Let $f$ be a function of $x$ and $x_{1}$. Then the range of $f$ is an element of $\wp x_{1}$ defined as $\operatorname{ofPred}$ applied to the function that maps $b$ to the proposition that there exists an element $a$ of $x$, such that $\MembershipmemMACRoT {f (a)}{b}$.

the restriction of f and s (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $s$ be an element of $\wp x$. Then the restriction of $f$ and $s$ is a function of $x$ and $x_{1}$ defined as $\operatorname{restrict}$ applied to the lift of $f$ and $\mathrm{Set\_\_subset\_univ}$ applied to $s$.

Let $f$ be a function of $x$ and $x_{1}$ such that $p$ is less than or equal to the domain of $f$. Then there is a function of $x$ and $x_{1}$. Proof. Let $f$ be arbitrary. Let $H$ be arbitrary. Let $x_{2}$ be arbitrary. By p. By x2. By Membership__mem. By x2. By f. By x2. By H. By Part__restrict.

the subtype of p and f (from the name)

Let $p$ be a function from elements of $x_{1}$ to propositions. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the subtype of $p$ and $f$ is a function of $x$ and $\SubtypeSet {x_{2}}{p (x_{2})}$ defined as the function that maps $a$ to $\operatorname{mk}$ applied to $p$ applied to $f$ applied to $a$ and $\operatorname{mk}$ applied to $f$ applied to $a$.

multivariate functor of n (from the name)

Let $n$ be a natural number. Then the multivariate functors of $n$ are a basic type.

Let $\mathrm{self}$ be a multivariate functor of $n$. Then an element of $\operatorname{A}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a multivariate functor of $n$. Let $x$ be an element of $\operatorname{A}$ applied to $\mathrm{self}$. Then there is a type vector of $n$. Proof. Let $\mathrm{self}$ be arbitrary. Let $x$ be arbitrary. By self. By x. By MvPFunctor__proj1.

object of P and x (from the name)

Let $P$ be a multivariate functor of $n$. Let $x$ be a type vector of $n$. Then an object of $P$ and $x$ is an element of the function that maps $P$ and $x$ to $\Sigma$ applied to the function that maps $a$ to the set of arrows of $\operatorname{B}$ applied to $P$ and $a$ and $x$.

Let $P$ be a multivariate functor of $n + 1$. Let $\mathrm{f'}$ be an arrow of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $x_{1}$. Then there is an arrow of $\operatorname{B}$ applied to $P$ and $a$ and $\operatorname{append1}$ applied to $x$ and $x_{1}$. Proof. Let $P$ be arbitrary. Let $\mathrm{f'}$ be arbitrary. Let $f$ be arbitrary. By f'. By f. By TypeVec__splitFun.

the composition of P and Q (from the name)

Let $P$ be a multivariate functor of $n$. Let $Q$ be a function from elements of $\mathrm{Fin2}$ applied to $n$ to multivariate functors of $m$. Then the composition of $P$ and $Q$ is a multivariate functor of $m$ defined as $\operatorname{mk}$ applied to $\Sigma$ applied to the function that maps $x$ to the set of functions from elements $i$ of $\mathrm{Fin2}$ applied to $n$ and elements of $\operatorname{B}$ applied to $P$, $x$ and $i$ to elements of $\operatorname{A}$ applied to $Q$ applied to $i$ and the function that maps $a$ and $i_{1}$ to $\Sigma$ applied to the function that maps $j$ to $\Sigma$ applied to the function that maps $b$ to $\operatorname{B}$ applied to $Q$ applied to $j$, $\operatorname{snd}$ applied to $a$, $j$ and $b$ and $i_{1}$.

Let $x_{1}$ be an object of the composition of $P$ and $Q$ and $x$. Then $\operatorname{get}$ applied to $x_{1}$ is an object of $P$ and the function that maps $i$ to the set of objects of $Q$ applied to $i$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{fst}$ applied to $\operatorname{fst}$ applied to $x_{1}$ and the function that maps $i$ and $a$ to $\operatorname{mk}$ applied to $\operatorname{snd}$ applied to $\operatorname{fst}$ applied to $x_{1}$, $i$ and $a$ and the function that maps $j$ and $b$ to $\operatorname{snd}$ applied to $x_{1}$, $j$ and $\operatorname{mk}$ applied to $i$ and $\operatorname{mk}$ applied to $a$ and $b$.

Let $x_{1}$ be an object of $P$ and the function that maps $i$ to the set of objects of $Q$ applied to $i$ and $x$. Then $\operatorname{mk}$ applied to $x_{1}$ is an object of the composition of $P$ and $Q$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{fst}$ applied to $x_{1}$ and the function that maps $x_{2}$ and $a$ to $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $x_{1}$, $x_{2}$ and $a$ and the function that maps $i$ and $a_{1}$ to $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $x_{1}$, $\operatorname{fst}$ applied to $a_{1}$ and $\operatorname{fst}$ applied to $\operatorname{snd}$ applied to $a_{1}$, $i$ and $\operatorname{snd}$ applied to $\operatorname{snd}$ applied to $a_{1}$.

the constant of n and A (from the name)

Let $n$ be a natural number. Let $A$ be a set. Then the constant of $n$ and $A$ is a multivariate functor of $n$ defined as $\operatorname{mk}$ applied to $A$ and the function that maps $x$ and $x_{1}$ to $\mathrm{PEmpty}$.

Let $x_{1}$ be an object of the constant of $n$ and $A$ and $x$. Then $\operatorname{get}$ applied to $x_{1}$ is an element of $A$ defined as $\operatorname{fst}$ applied to $x_{1}$.

Let $n$ be a natural number. Let $x$ be an element of $A$. Then $\operatorname{mk}$ applied to $n$ and $x$ is an object of the constant of $n$ and $A$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $x$ and the function that maps $x_{2}$ and $a$ to $\operatorname{elim}$ applied to $a$.

Let $P$ be a multivariate functor of $n + 1$. Then $\operatorname{drop}$ applied to $P$ is a multivariate functor of $n$ defined as $\operatorname{mk}$ applied to $\operatorname{A}$ applied to $P$ and the function that maps $a$ to $\operatorname{drop}$ applied to $\operatorname{B}$ applied to $P$ and $a$.

Let $P$ be a multivariate functor of $n + 1$. Then $\operatorname{last}$ applied to $P$ is a functor defined as $\operatorname{mk}$ applied to $\operatorname{A}$ applied to $P$ and the function that maps $a$ to $\operatorname{last}$ applied to $\operatorname{B}$ applied to $P$ and $a$.

the map of f and x2 (from the name)

Let $P$ be a multivariate functor of $n$. Let $f$ be an arrow of $x$ and $x_{1}$. Let $x_{2}$ be an object of $P$ and $x$. Then the map of $f$ and $x_{2}$ is an object of $P$ and $x_{1}$.

Let $P$ be a multivariate functor of $n + 1$. Let $x$ be a type vector of $n$. Then an element of $\operatorname{M}$ applied to $P$ and $x$ is an element of the function that maps $P$ and $x$ to the set of objects of $\operatorname{mp}$ applied to $P$ and $x$.

path of x and x1 (from the name)

Let $P$ be a multivariate functor of $n + 1$. Let $x$ be an element of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$. Let $x_{1}$ be an element of $\mathrm{Fin2}$ applied to $n$. Then the paths of $x$ and $x_{1}$ are a basic type.

the child of i and c (from the name)

Let $x$ be an element of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$. Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ such that $\EqtMACRoH {\operatorname{dest} (x)}{\operatorname{mk} (a , f)}$. Let $j$ be an element of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$. Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $c$ be a path of $f$ applied to $j$ and $i$. Then the child of $i$ and $c$ is a path of $x$ and $i$.

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 the set of functions from elements $x$ of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ and elements $a$ of $\operatorname{A}$ applied to $P$ and functions $f$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ and elements $h$ of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{dest} (x)}{\operatorname{mk} (a , f)}$ and elements $i$ of $\mathrm{Fin2}$ applied to $n$ and elements $c$ of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$, $a$ and $i$ to elements of $\mathrm{motive}$ applied to $x$, $i$ and the root of $i$ and $c$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ and elements $a_{1}$ of $\operatorname{A}$ applied to $P$ and functions $f_{1}$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a_{1}$ to elements of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ and elements $h_{1}$ of $\mathrm{Proof}$ applied to $\EqtMACRoH {\operatorname{dest} (x_{2})}{\operatorname{mk} (a_{1} , f_{1})}$ and elements $j$ of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a_{1}$ and elements $i_{1}$ of $\mathrm{Fin2}$ applied to $n$ and paths $c_{1}$ of $f_{1}$ applied to $j$ and $i_{1}$ to elements of $\mathrm{motive}$ applied to $x_{2}$, $i_{1}$ and the child of $i_{1}$ and $c_{1}$.

the root of i and c (from the name)

Let $x$ be an element of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$. Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ such that $\EqtMACRoH {\operatorname{dest} (x)}{\operatorname{mk} (a , f)}$. Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $c$ be an element of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$, $a$ and $i$. Then the root of $i$ and $c$ is a path of $x$ and $i$.

Let $P$ be a multivariate functor of $n + 1$. Let $g$ be a function from elements of $x_{1}$ to objects of $P$ and $\operatorname{append1}$ applied to $x$ and $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{corec}$ applied to $P$, $g$ and $x_{2}$ is an element of $\operatorname{M}$ applied to $P$ and $x$ defined as $\operatorname{corec'}$ applied to $P$, the function that maps $b$ to $\operatorname{fst}$ applied to $g$ applied to $b$, the function that maps $b_{1}$ to $\operatorname{dropFun}$ applied to $\operatorname{snd}$ applied to $g$ applied to $b_{1}$, the function that maps $b_{2}$ to $\operatorname{lastFun}$ applied to $\operatorname{snd}$ applied to $g$ applied to $b_{2}$ and $x_{2}$.

Let $P$ be a multivariate functor of $n + 1$. Let $x_{2}$ be a function from elements of $x_{1}$ to elements of $\operatorname{A}$ applied to $P$. Let $x_{3}$ be a function from elements $b_{1}$ of $x_{1}$ to arrows of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $x_{2}$ applied to $b_{1}$ and $x$. Let $x_{4}$ be a function from elements $b$ of $x_{1}$ and elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $x_{2}$ applied to $b$ to elements of $x_{1}$. Let $x_{5}$ be an element of $x_{1}$. Then $\operatorname{corec'}$ applied to $P$, $x_{2}$, $b_{1}$, $x_{3}$, $b$, $x_{4}$ and $x_{5}$ is an element of $\operatorname{M}$ applied to $P$ and $x$.

Let $P$ be a multivariate functor of $n + 1$. Let $x_{2}$ be a function from elements of $x_{1}$ to elements of $\operatorname{A}$ applied to $P$. Let $x_{3}$ be a function from elements $b_{2}$ of $x_{1}$ to arrows of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $x_{2}$ applied to $b_{2}$ and $x$. Let $x_{4}$ be a function from elements $b_{1}$ of $x_{1}$ and elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $x_{2}$ applied to $b_{1}$ to elements of $x_{1}$. Let $x_{5}$ be an element of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$. Let $b$ be an element of $x_{1}$ such that $\EqtMACRoH {x_{5}}{\operatorname{corecShape} (P , x_{2} , x_{4} , b)}$. Then there is an arrow of the set of elements of $\operatorname{Path}$ applied to $x_{5}$ and $x$. Proof. Let $P$ be arbitrary. Let $x_{2}$ be arbitrary. Let $x_{3}$ be arbitrary. Let $x_{4}$ be arbitrary. Let $x_{5}$ be arbitrary. Let $b$ be arbitrary. Let $h$ be arbitrary. Let $x_{6}$ be arbitrary. Let $x_{7}$ be arbitrary. By h. By P. By x2. By b2. By x3. By MvPFunctor__M__corecContents___f. By x4. By x5. By MvPFunctor__M__Path__brecOn.

Let $P$ be a multivariate functor of $n + 1$. Let $x_{1}$ be a function from elements of $x$ to elements of $\operatorname{A}$ applied to $P$. Let $x_{2}$ be a function from elements $b$ of $x$ and elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $x_{1}$ applied to $b$ to elements of $x$. Let $x_{3}$ be an element of $x$. Then $\operatorname{corecShape}$ applied to $P$, $x_{1}$, $b$, $x_{2}$ and $x_{3}$ is an element of $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ defined as the function that maps $x_{3}$ to $\operatorname{corec}$ applied to the function that maps $b$ to $\operatorname{mk}$ applied to $x_{1}$ applied to $b$ and $b$ applied to $b$, $x_{2}$ and $x_{3}$.

Let $P$ be a multivariate functor of $n + 1$. Let $x_{1}$ be an element of $\operatorname{M}$ applied to $P$ and $x$. Then $\operatorname{dest}$ applied to $P$ and $x_{1}$ is an object of $P$ and $\operatorname{append1}$ applied to $x$ and $\operatorname{M}$ applied to $P$ and $x$.

Let $P$ be a multivariate functor of $n + 1$. Assume that $\EqtMACRoH {\operatorname{dest} (x_{1})}{\operatorname{mk} (a , f)}$. Let $\mathrm{f'}$ be an arrow of the set of elements of $\operatorname{Path}$ applied to $x_{1}$ and $x$. Then $\operatorname{dest'}$ applied to $P$, $h$ and $\mathrm{f'}$ is an object of $P$ and $\operatorname{append1}$ applied to $x$ and $\operatorname{M}$ applied to $P$ and $x$ defined as $\operatorname{mk}$ applied to $a$ and the split function of $\operatorname{pathDestLeft}$ applied to $P$, $h$ and $\mathrm{f'}$ and the function that maps $x_{2}$ to $\operatorname{mk}$ applied to $f$ applied to $x_{2}$ and $\operatorname{pathDestRight}$ applied to $P$, $h$, $\mathrm{f'}$ and $x_{2}$.

Let $P$ be a multivariate functor of $n + 1$. Let $x_{1}$ be an object of $P$ and $\operatorname{append1}$ applied to $x$ and $\operatorname{M}$ applied to $P$ and $x$. Then $\operatorname{mk}$ applied to $P$ and $x_{1}$ is an element of $\operatorname{M}$ applied to $P$ and $x$ defined as $\operatorname{corec}$ applied to $P$, the function that maps $i$ to $\operatorname{map}$ applied to $\operatorname{appendFun}$ applied to the identity and $\operatorname{dest}$ applied to $P$ and $i$ and $x_{1}$.

Let $P$ be a multivariate functor of $n + 1$. Assume that $\EqtMACRoH {a}{\mathrm{a'}}$. Then there is an arrow of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $\mathrm{a'}$. Proof. Let $P$ be arbitrary. Let $h$ be arbitrary. Let $\mathrm{\_i}$ be arbitrary. Let $b$ be arbitrary. By h. By b. By Eq__recOn.

Let $P$ be a multivariate functor of $n + 1$. Assume that $\EqtMACRoH {a}{\mathrm{a'}}$. Let $x$ be an element of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$. Then $\operatorname{castLastB}$ applied to $P$, $h$ and $x$ is an element of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $\mathrm{a'}$ defined as $\operatorname{recOn}$ applied to $h$ and $x$.

Let $P$ be a multivariate functor of $n + 1$. Then $\operatorname{mp}$ applied to $P$ is a multivariate functor of $n$ defined as $\operatorname{mk}$ applied to $\operatorname{M}$ applied to $\operatorname{last}$ applied to $P$ and the set of elements of $\operatorname{Path}$.

Let $P$ be a multivariate functor of $n + 1$. Let $x$ be a type vector of $n$. Then an element of $\operatorname{W}$ applied to $P$ and $x$ is an element of the function that maps $P$ and $x$ to the set of objects of $\operatorname{wp}$ applied to $P$ and $x$.

path of x and x1 (from the name)

Let $P$ be a multivariate functor of $n + 1$. Let $x$ be an element of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$. Let $x_{1}$ be an element of $\mathrm{Fin2}$ applied to $n$. Then the paths of $x$ and $x_{1}$ are a basic type.

the child of j and c (from the name)

Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$. Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $j$ be an element of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$. Let $c$ be a path of $f$ applied to $j$ and $i$. Then the child of $j$ and $c$ is a path of $\operatorname{mk}$ applied to $a$ and $f$ and $i$.

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 the set of functions from elements $a$ of $\operatorname{A}$ applied to $P$ and functions $f$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$ and elements $i$ of $\mathrm{Fin2}$ applied to $n$ and elements $c$ of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$, $a$ and $i$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $a$ and $f$, $i$ and the root of $i$ and $c$ and $\mathrm{PULift}$ applied to the set of functions from elements $a_{1}$ of $\operatorname{A}$ applied to $P$ and functions $f_{1}$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a_{1}$ to elements of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$ and elements $i_{1}$ of $\mathrm{Fin2}$ applied to $n$ and elements $j$ of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a_{1}$ and paths $c_{1}$ of $f_{1}$ applied to $j$ and $i_{1}$ to elements of $\mathrm{motive}$ applied to $\operatorname{mk}$ applied to $a_{1}$ and $f_{1}$, $i_{1}$ and the child of $j$ and $c_{1}$.

the root of i and c (from the name)

Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$. Let $i$ be an element of $\mathrm{Fin2}$ applied to $n$. Let $c$ be an element of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$, $a$ and $i$. Then the root of $i$ and $c$ is a path of $\operatorname{mk}$ applied to $a$ and $f$ and $i$.

Let $P$ be a multivariate functor of $n + 1$. Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $\mathrm{f'}$ be an arrow of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $x_{1}$. Then $\operatorname{objAppend1}$ applied to $P$, $a$, $\mathrm{f'}$ and $f$ is an object of $P$ and $\operatorname{append1}$ applied to $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $a$ and the split function of $\mathrm{f'}$ and $f$.

the case of ih and a (from the name)

Let $P$ be a multivariate functor of $n + 1$. Let $\mathrm{ih}$ be a function from elements $a$ of $\operatorname{A}$ applied to $P$ and arrows $\mathrm{f'}$ of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$ and functions $f$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $P$ and $x$ to elements of $C$ applied to $\operatorname{wMk}$ applied to $P$, $a$, $\mathrm{f'}$ and $f$. Let $x_{1}$ be an element of $\operatorname{W}$ applied to $P$ and $x$. Then the case of $a$ and $\mathrm{f'}$ is an element of $C$ applied to $x_{1}$ defined as the function that maps $f$, $\mathrm{ih}$ and $x_{1}$ to the ind of the function that maps $a$, $\mathrm{f'}$, $f$ and $\mathrm{\_ih'}$ to $a$ applied to $a$, $\mathrm{f'}$ and $f$ and $\mathrm{f'}$.

Let $P$ be a multivariate functor of $n + 1$. Let $x_{1}$ be an element of $\operatorname{W}$ applied to $P$ and $x$. Then $\operatorname{wDest'}$ applied to $P$ and $x_{1}$ is an object of $P$ and $\operatorname{append1}$ applied to $x$ and $\operatorname{W}$ applied to $P$ and $x$ defined as $\operatorname{wRec}$ applied to $P$, the function that maps $a$, $\mathrm{f'}$, $f$ and $x_{1}$ to $\operatorname{mk}$ applied to $a$ and the split function of $\mathrm{f'}$ and $f$ and $x_{1}$.

the ind of ih and a (from the name)

Let $P$ be a multivariate functor of $n + 1$. Let $\mathrm{ih}$ be a function from elements $a$ of $\operatorname{A}$ applied to $P$ and arrows $\mathrm{f'}$ of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$ and functions $f$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $P$ and $x$ and functions from elements $i$ of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $C$ applied to $f$ applied to $i$ to elements of $C$ applied to $\operatorname{wMk}$ applied to $P$, $a$, $\mathrm{f'}$ and $f$. Let $x_{1}$ be an element of $\operatorname{W}$ applied to $P$ and $x$. Then the ind of $a$ and $\mathrm{f'}$ is an element of $C$ applied to $x_{1}$.

the map of g and x2 (from the name)

Let $P$ be a multivariate functor of $n + 1$. Let $g$ be an arrow of $x$ and $x_{1}$. Let $x_{2}$ be an element of $\operatorname{W}$ applied to $P$ and $x$. Then the map of $g$ and $x_{2}$ is an element of $\operatorname{W}$ applied to $P$ and $x_{1}$ defined as $\operatorname{map}$ applied to $g$ and $x_{2}$.

Let $P$ be a multivariate functor of $n + 1$. Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $\mathrm{f'}$ be an arrow of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $P$ and $x$. Then $\operatorname{wMk}$ applied to $P$, $a$, $\mathrm{f'}$ and $f$ is an element of $\operatorname{W}$ applied to $P$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $a$ and the function that maps $i$ to $\operatorname{fst}$ applied to $f$ applied to $i$ and $\operatorname{wPathCasesOn}$ applied to $P$, $\mathrm{f'}$ and the function that maps $i_{1}$ to $\operatorname{snd}$ applied to $f$ applied to $i_{1}$.

Let $P$ be a multivariate functor of $n + 1$. Let $x_{1}$ be an object of $P$ and $\operatorname{append1}$ applied to $x$ and $\operatorname{W}$ applied to $P$ and $x$. Then $\operatorname{wMk'}$ applied to $P$ and $x_{1}$ is an element of $\operatorname{W}$ applied to $P$ and $x$.

Let $P$ be a multivariate functor of $n + 1$. Let $\mathrm{g'}$ be an arrow of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$. Let $g$ be a function from elements $j$ of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to arrows of the set of elements of $\operatorname{WPath}$ applied to $f$ applied to $j$ and $x$. Then there is an arrow of the set of elements of $\operatorname{WPath}$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $x$.

Let $P$ be a multivariate functor of $n + 1$. Let $h$ be an arrow of the set of elements of $\operatorname{WPath}$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $x$. Then there is an arrow of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$. Proof. Let $P$ be arbitrary. Let $h$ be arbitrary. Let $i$ be arbitrary. Let $c$ be arbitrary. By i. By i. By c. By MvPFunctor__WPath__root. By h.

Let $P$ be a multivariate functor of $n + 1$. Let $h$ be an arrow of the set of elements of $\operatorname{WPath}$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $x$. Let $j$ be an element of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$. Then there is an arrow of the set of elements of $\operatorname{WPath}$ applied to $f$ applied to $j$ and $x$. Proof. Let $P$ be arbitrary. Let $h$ be arbitrary. Let $j$ be arbitrary. Let $i$ be arbitrary. Let $c$ be arbitrary. By i. By j. By c. By MvPFunctor__WPath__child. By h.

Let $P$ be a multivariate functor of $n + 1$. Let $g$ be a function from elements $a$ of $\operatorname{A}$ applied to $P$ and arrows of $\operatorname{B}$ applied to $\operatorname{drop}$ applied to $P$ and $a$ and $x$ and functions from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $P$ and $x$ and functions from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $C$ to elements of $C$. Let $x_{1}$ be an element of $\operatorname{W}$ applied to $P$ and $x$. Then $\operatorname{wRec}$ applied to $P$, $a$, $g$ and $x_{1}$ is an element of $C$.

Let $P$ be a multivariate functor of $n + 1$. Then $\operatorname{wp}$ applied to $P$ is a multivariate functor of $n$ defined as $\operatorname{mk}$ applied to $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$ and the set of elements of $\operatorname{WPath}$.

Let $P$ be a multivariate functor of $n + 1$. Let $\mathrm{ih}$ be a function from elements $a$ of $\operatorname{A}$ applied to $P$ and functions $f$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$ and arrows $\mathrm{f'1}$ of the set of elements of $\operatorname{WPath}$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $x$ and functions from elements $i$ of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $C$ applied to $f$ applied to $i$ and $\operatorname{wPathDestRight}$ applied to $P$, $\mathrm{f'1}$ and $i$ to elements of $C$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $\mathrm{f'1}$. Let $x_{1}$ be an element of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$. Let $\mathrm{f'}$ be an arrow of the set of elements of $\operatorname{WPath}$ applied to $x_{1}$ and $x$. Then $\operatorname{wpInd}$ applied to $P$, $a$, $f$, $\mathrm{f'1}$, $\mathrm{ih}$, $x_{1}$ and $\mathrm{f'}$ is an element of $C$ applied to $x_{1}$ and $\mathrm{f'}$ defined as the function that maps $\mathrm{ih}$, $x_{1}$ and $\mathrm{f'}$ to $\operatorname{brecOn}$ applied to $f$, $\mathrm{MvPFunctor\_\_wpInd\_\_\_f}$ applied to $P$ and $a$, $\mathrm{f'1}$, $\mathrm{ih}$, $x_{1}$ and $\mathrm{f'}$.

Let $P$ be a multivariate functor of $n + 1$. Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$. Let $\mathrm{f'}$ be an arrow of the set of elements of $\operatorname{WPath}$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $x$. Then $\operatorname{wpMk}$ applied to $P$, $a$, $f$ and $\mathrm{f'}$ is an element of $\operatorname{W}$ applied to $P$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $\mathrm{f'}$.

Let $P$ be a multivariate functor of $n + 1$. Let $g$ be a function from elements $a$ of $\operatorname{A}$ applied to $P$ and functions $f$ from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$ and arrows of the set of elements of $\operatorname{WPath}$ applied to $\operatorname{mk}$ applied to $a$ and $f$ and $x$ and functions from elements of $\operatorname{B}$ applied to $\operatorname{last}$ applied to $P$ and $a$ to elements of $C$ to elements of $C$. Let $x_{1}$ be an element of $\operatorname{W}$ applied to $\operatorname{last}$ applied to $P$. Let $x_{2}$ be an arrow of the set of elements of $\operatorname{WPath}$ applied to $x_{1}$ and $x$. Then $\operatorname{wpRec}$ applied to $P$, $a$, $f$, $g$, $x_{1}$ and $x_{2}$ is an element of $C$ defined as the function that maps $x_{1}$ and $x_{2}$ to $\operatorname{brecOn}$ applied to $f$, $\mathrm{MvPFunctor\_\_wpRec\_\_\_f}$ applied to $P$ and $a$, $g$, $x_{1}$ and $x_{2}$.

functor (from the name)

The functors are a basic type.

Let $\mathrm{self}$ be a functor. Then an element of $\operatorname{A}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be a functor. Let $x$ be an element of $\operatorname{A}$ applied to $\mathrm{self}$. Then an element of $\operatorname{B}$ applied to $\mathrm{self}$ and $x$ is an element of the function that maps $\mathrm{self}$ and $x$ to $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x$.

index of P (from the name)

Let $P$ be a functor. Then an index of $P$ is an element of the function that maps $P$ to $\Sigma$ applied to the function that maps $x$ to $\operatorname{B}$ applied to $P$ and $x$.

object of P and x (from the name)

Let $P$ be a functor. Let $x$ be a set. Then an object of $P$ and $x$ is an element of the function that maps $P$ and $x$ to $\Sigma$ applied to the function that maps $x_{1}$ to the set of functions from elements of $\operatorname{B}$ applied to $P$ and $x_{1}$ to elements of $x$.

the first component of x1 (from the name)

Let $x_{1}$ be an object of $P$ and $x$. Then the first component of $x_{1}$ is an element of $\operatorname{A}$ applied to $P$ defined as $\operatorname{fst}$ applied to $x_{1}$.

Let $x_{3}$ be an object of $P$ and $x_{1}$. Let $i$ be an index of $P$. Then $\operatorname{iget}$ applied to $x_{3}$ and $i$ is an element of $x_{1}$.

Let $a$ be an element of $\operatorname{A}$ applied to $P$. Let $f$ be a function from elements of $\operatorname{B}$ applied to $P$ and $a$ to elements of $x$. Then $\operatorname{mk}$ applied to $a$ and $f$ is an object of $P$ and $x$ defined as $\operatorname{mk}$ applied to $a$ and $f$.

the second component of x1 and x2 (from the name)

Let $x_{1}$ be an object of $P$ and $x$. Let $x_{2}$ be an element of $\operatorname{B}$ applied to $P$ and the first component of $x_{1}$. Then the second component of $x_{1}$ and $x_{2}$ is an element of $x$ defined as $\operatorname{snd}$ applied to $x_{1}$ and $x_{2}$.

Let $P$ be a functor. Then an element of $\operatorname{W}$ applied to $P$ is an element of the function that maps $P$ to the set of types of $\operatorname{B}$ applied to $P$.

Let $x$ be an element of $\operatorname{W}$ applied to $P$. Let $x_{1}$ be an element of $\operatorname{B}$ applied to $P$ and the head of $x$. Then $\operatorname{children}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{W}$ applied to $P$.

Let $x$ be an element of $\operatorname{W}$ applied to $P$. Then $\operatorname{dest}$ applied to $x$ is an object of $P$ and $\operatorname{W}$ applied to $P$.

the head of x (from the name)

Let $x$ be an element of $\operatorname{W}$ applied to $P$. Then the head of $x$ is an element of $\operatorname{A}$ applied to $P$.

Let $x$ be an object of $P$ and $\operatorname{W}$ applied to $P$. Then $\operatorname{mk}$ applied to $x$ is an element of $\operatorname{W}$ applied to $P$.

the composition of x and x1 (from the name)

Let $x$ and $x_{1}$ be functors. Then the composition of $x$ and $x_{1}$ is a functor defined as $\operatorname{mk}$ applied to $\Sigma$ applied to the function that maps $x_{2}$ to the set of functions from elements of $\operatorname{B}$ applied to $x$ and $x_{2}$ to elements of $\operatorname{A}$ applied to $x_{1}$ and the function that maps $x_{4}$ to $\Sigma$ applied to the function that maps $u$ to $\operatorname{B}$ applied to $x_{1}$ and $\operatorname{snd}$ applied to $x_{4}$ and $u$.

Let $x$ and $x_{1}$ be functors. Let $x_{3}$ be an object of the composition of $x$ and $x_{1}$ and $x_{2}$. Then $\operatorname{get}$ applied to $x$, $x_{1}$ and $x_{3}$ is an object of $x$ and the set of objects of $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{fst}$ applied to the first component of $x_{3}$ and the function that maps $x_{4}$ to $\operatorname{mk}$ applied to $\operatorname{snd}$ applied to the first component of $x_{3}$ and $x_{4}$ and the function that maps $x_{5}$ to the second component of $x_{3}$ and $\operatorname{mk}$ applied to $x_{4}$ and $x_{5}$.

Let $x$ and $x_{1}$ be functors. Let $x_{3}$ be an object of $x$ and the set of objects of $x_{1}$ and $x_{2}$. Then $\operatorname{mk}$ applied to $x$, $x_{1}$ and $x_{3}$ is an object of the composition of $x$ and $x_{1}$ and $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the first component of $x_{3}$ and $\operatorname{comp}$ applied to $\operatorname{fst}$ and $\operatorname{snd}$ applied to $x_{3}$ and the function that maps $x_{4}$ to the second component of the second component of $x_{3}$ and $\operatorname{fst}$ applied to $x_{4}$ and $\operatorname{snd}$ applied to $x_{4}$.

the map of f and x2 (from the name)

Let $P$ be a functor. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $x_{2}$ be an object of $P$ and $x$. Then the map of $f$ and $x_{2}$ is an object of $P$ and $x_{1}$ defined as $\operatorname{mk}$ applied to the first component of $x_{2}$ and $\operatorname{comp}$ applied to $f$ and $\operatorname{snd}$ applied to $x_{2}$.

Let $x$ be an element of $\operatorname{CofixA}$ applied to $F$ and $n$. Let $x_{1}$ be an element of $\operatorname{CofixA}$ applied to $F$ and $n + 1$. Then we can say that $\operatorname{Agree}$ holds for $x$ and $x_{1}$.

Assume that $\operatorname{Agree}$ holds for $x$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $x$ be a function from natural numbers $n$ to elements of $\operatorname{CofixA}$ applied to $F$ and $n$. Then $\operatorname{AllAgree}$ holds for $n$ and $x$, if for all natural numbers $n$, $\operatorname{Agree}$ holds for $n$ applied to $n$ and $n$ applied to the successor of $n$.

Let $F$ be a functor. Let $x$ be a natural number. Then the elements of $\operatorname{CofixA}$ applied to $F$ and $x$ are a basic type.

$\operatorname{continue}$ is an element of $\operatorname{CofixA}$ applied to $F$ and $0$.

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 $0$ and $\operatorname{continue}$ and $\mathrm{PULift}$ applied to the set of functions from natural numbers $n$ and elements $a$ of $\operatorname{A}$ applied to $F$ and functions $x$ from elements of $\operatorname{B}$ applied to $F$ and $a$ to elements of $\operatorname{CofixA}$ applied to $F$ and $n$ to elements of $\mathrm{motive}$ applied to the successor of $n$ and the intro of $a$ and $x$.

the default of F and n (from the name)

Let $F$ be a functor. Let $n$ be a natural number. Then the default of $F$ and $n$ is an element of $\operatorname{CofixA}$ applied to $F$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$ and $\mathrm{PFunctor\_\_Approx\_\_CofixA\_\_default\_\_\_f}$ applied to $F$.

the intro of a and x (from the name)

Let $a$ be an element of $\operatorname{A}$ applied to $F$. Let $x$ be a function from elements of $\operatorname{B}$ applied to $F$ and $a$ to elements of $\operatorname{CofixA}$ applied to $F$ and $n$. Then the intro of $a$ and $x$ is an element of $\operatorname{CofixA}$ applied to $F$ and the successor of $n$.

path of F (from the name)

Let $F$ be a functor. Then a path of $F$ is an element of the function that maps $F$ to the set of lists of indexes of $F$.

Let $x$ be an element of $\operatorname{CofixA}$ applied to $F$ and the successor of $n$. Let $x_{1}$ be an element of $\operatorname{B}$ applied to $F$ and the head of $x$. Then $\operatorname{children'}$ applied to $x$ and $x_{1}$ is an element of $\operatorname{CofixA}$ applied to $F$ and $n$.

the head of x (from the name)

Let $x$ be an element of $\operatorname{CofixA}$ applied to $F$ and the successor of $n$. Then the head of $x$ is an element of $\operatorname{A}$ applied to $F$.

Let $f$ be a function from elements of $X$ to objects of $F$ and $X$. Let $x$ be an element of $X$. Let $n$ be a natural number. Then $\operatorname{sCorec}$ applied to $f$, $x$ and $n$ is an element of $\operatorname{CofixA}$ applied to $F$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{PFunctor\_\_Approx\_\_sCorec\_\_\_f}$ applied to $f$ and $x$.

Let $x$ be an element of $\operatorname{CofixA}$ applied to $F$ and $n + 1$. Then $\operatorname{truncate}$ applied to $x$ is an element of $\operatorname{CofixA}$ applied to $F$ and $n$ defined as $\operatorname{brecOn}$ applied to $n$, $\mathrm{PFunctor\_\_Approx\_\_truncate\_\_\_f}$ and $x$.

Let $F$ be a functor. Then an element of $\operatorname{M}$ applied to $F$ is an element of the function that maps $F$ to $\operatorname{MIntl}$ applied to $F$.

Let $x$ be a natural number. Let $x_{1}$ and $x_{2}$ be elements of $\operatorname{M}$ applied to $F$. Then we can say that $\operatorname{Agree'}$ holds for $x$, $x_{1}$ and $x_{2}$.

Assume that $\operatorname{Agree'}$ holds for $x$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.

Let $x$ be an object of $F$ and $\operatorname{M}$ applied to $F$. Let $n$ be a natural number. Then $\operatorname{sMk}$ applied to $x$ and $n$ is an element of $\operatorname{CofixA}$ applied to $F$ and $n$.

Let $R$ be a function from elements of $\operatorname{M}$ applied to $F$ and elements of $\operatorname{M}$ applied to $F$ to propositions. Then we can say that $\operatorname{IsBisimulation}$ holds for $R$.

Let $x$ be a path of $F$. Let $x_{1}$ be an element of $\operatorname{M}$ applied to $F$. Then we can say that $\operatorname{IsPath}$ holds for $x$ and $x_{1}$.

Assume that $\operatorname{IsPath}$ holds for $x$ and $x_{1}$. Then we can say that $\operatorname{below}$ holds for $t$.

the case of f and x1 (from the name)

Let $f$ be a function from objects $x_{1}$ of $F$ and $\operatorname{M}$ applied to $F$ to elements of $r$ applied to $\operatorname{mk}$ applied to $x_{1}$. Let $x$ be an element of $\operatorname{M}$ applied to $F$. Then the case of $x_{1}$ and $f$ is an element of $r$ applied to $x$.

Let $x$ be an element of $\operatorname{M}$ applied to $F$. Let $f$ be a function from objects $x_{1}$ of $F$ and $\operatorname{M}$ applied to $F$ to elements of $r$ applied to $\operatorname{mk}$ applied to $x_{1}$. Then $\operatorname{casesOn}$ applied to $x$, $x_{1}$ and $f$ is an element of $r$ applied to $x$ defined as the function that maps $f$ to the case of $x_{1}$ and $x$.

Let $x$ be an element of $\operatorname{M}$ applied to $F$. Let $f$ be a function from elements $a$ of $\operatorname{A}$ applied to $F$ and functions $f_{1}$ from elements of $\operatorname{B}$ applied to $F$ and $a$ to elements of $\operatorname{M}$ applied to $F$ to elements of $r$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $a$ and $f_{1}$. Then $\operatorname{casesOn'}$ applied to $x$, $a$, $f_{1}$ and $f$ is an element of $r$ applied to $x$.

Let $x$ be an element of $\operatorname{M}$ applied to $F$. Let $i$ be an element of $\operatorname{B}$ applied to $F$ and the head of $x$. Then $\operatorname{children}$ applied to $x$ and $i$ is an element of $\operatorname{M}$ applied to $F$.

Let $f$ be a function from elements of $X$ to objects of $F$ and $X$. Let $i$ be an element of $X$. Then $\operatorname{corec}$ applied to $f$ and $i$ is an element of $\operatorname{M}$ applied to $F$ defined as $\operatorname{mk}$ applied to $\operatorname{sCorec}$ applied to $f$ and $i$ and $\mathrm{PFunctor\_\_Approx\_\_P\_corec}$ applied to $f$ and $i$.

Let $F$ be a function from sets $X$ and functions from elements of $x$ to elements of $X$ and elements of $x$ to elements of $\mathrm{Sum}$ applied to $\operatorname{M}$ applied to $P$ and the set of objects of $P$ and $X$. Let $x_{1}$ be an element of $x$. Then $\operatorname{corec'}$ applied to $X$, $F$ and $x_{1}$ is an element of $\operatorname{M}$ applied to $P$.

Let $x$ be an element of $X$. Let $f$ be a function from elements of $X$ to objects of $F$ and $X$. Then $\operatorname{corecOn}$ applied to $x$ and $f$ is an element of $\operatorname{M}$ applied to $F$ defined as $\operatorname{corec}$ applied to $f$ and $x$.

Let $F$ be a function from sets $X$ and functions from elements of $x$ to elements of $X$ and elements of $x$ to objects of $P$ and $X$. Let $x_{1}$ be an element of $x$. Then $\mathrm{PFunctor\_\_M\_\_corec\_u2081\_}$ applied to $X$, $F$ and $x_{1}$ is an element of $\operatorname{M}$ applied to $P$ defined as the function that maps $x_{1}$ to $\operatorname{corec}$ applied to $X$ applied to $x$ and $\mathrm{id}$, $F$ and $x_{1}$.

Let $x$ be an element of $\operatorname{M}$ applied to $F$. Then $\operatorname{dest}$ applied to $x$ is an object of $F$ and $\operatorname{M}$ applied to $F$ defined as $\operatorname{mk}$ applied to the head of $x$ and the function that maps $i$ to $\operatorname{children}$ applied to $x$ and $i$.

the head of x (from the name)

Let $x$ be an element of $\operatorname{M}$ applied to $F$. Then the head of $x$ is an element of $\operatorname{A}$ applied to $F$ defined as the head of $\operatorname{approx}$ applied to $x$ and $1$.

Let $i$ be an index of $F$. Let $x_{2}$ be an element of $\operatorname{M}$ applied to $F$. Then $\operatorname{ichildren}$ applied to $i$ and $x_{2}$ is an element of $\operatorname{M}$ applied to $F$.

Let $\mathrm{ps}$ be a path of $F$. Let $x_{2}$ be an element of $\operatorname{M}$ applied to $F$. Then $\operatorname{iselect}$ applied to $\mathrm{ps}$ and $x_{2}$ is an element of $\operatorname{A}$ applied to $F$ defined as the head of $\operatorname{isubtree}$ applied to $\mathrm{ps}$ and $x_{2}$.

Let $x_{2}$ be a path of $F$. Let $x_{3}$ be an element of $\operatorname{M}$ applied to $F$. Then $\operatorname{isubtree}$ applied to $x_{2}$ and $x_{3}$ is an element of $\operatorname{M}$ applied to $F$ defined as $\operatorname{brecOn}$ applied to $x_{2}$, $\mathrm{PFunctor\_\_M\_\_isubtree\_\_\_f}$ and $x_{3}$.

Let $x$ be an object of $F$ and $\operatorname{M}$ applied to $F$. Then $\operatorname{mk}$ applied to $x$ is an element of $\operatorname{M}$ applied to $F$ defined as $\operatorname{mk}$ applied to $\operatorname{sMk}$ applied to $x$ and $\mathrm{PFunctor\_\_M\_\_Approx\_\_P\_mk}$ applied to $x$.

Let $F$ be a functor. Then the elements of $\operatorname{MIntl}$ applied to $F$ are a basic type.

Let $\mathrm{self}$ be an element of $\operatorname{MIntl}$ applied to $F$. Let $n$ be a natural number. Then $\operatorname{approx}$ applied to $\mathrm{self}$ and $n$ is an element of $\operatorname{CofixA}$ applied to $F$ and $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $n$.

$\operatorname{pnatIsoNat}$ is an order isomorphism of $\PNatMACRoAD$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{pnatEquivNat}$ and the function that maps $x$ and $x_{1}$ to $\mathrm{PNat\_\_natPred\_le\_natPred}$.

Let $a$ be a positive natural number. Let $\mathrm{hz}$ be an element of $p$ applied to $1$. Let $\mathrm{hi}$ be a function from positive natural numbers $n$ and functions from positive natural numbers $m$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (m , n)$ to elements of $p$ applied to $m$ to elements of $p$ applied to $n + 1$. Then $\operatorname{caseStrongInductionOn}$ applied to $a$, $\mathrm{hz}$, $n$ and $\mathrm{hi}$ is an element of $p$ applied to $a$.

the coercion additive homomorphism (from the name)

The coercion additive homomorphism is an additive homomorphism of $\PNatMACRoAD$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{val}$ and $\mathrm{PNat\_\_add\_coe}$.

the coercion monoid homomorphism (from the name)

The coercion monoid homomorphism is a monoid homomorphism of $\PNatMACRoAD$ and $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{PNat\_\_one\_coe}$ and $\mathrm{PNat\_\_mul\_coe}$.

Let $n$ be a positive natural number. Let $\mathrm{one}$ be an element of $p$ applied to $1$. Let $\mathrm{succ}$ be a function from positive natural numbers $n_{1}$ and elements of $p$ applied to $n_{1}$ to elements of $p$ applied to $n_{1} + 1$. Then $\operatorname{recOn}$ applied to $n$, $\mathrm{one}$, $n_{1}$ and $\mathrm{succ}$ is an element of $p$ applied to $n$.

the successor natural number of n (from the name)

Let $n$ be a natural number. Then the successor natural number of $n$ is a positive natural number defined as the successor of $n$.

the natural number of n and h (from the name)

Let $n$ be a natural number such that $\mathrm{autoParam}$ holds for $\mathrm{Lt} (0 , n)$ and $\mathrm{Nat\_\_toPNat\_\_\_auto\_1}$. Then the natural number of $n$ and $h$ is a positive natural number defined as $n$.

the natural number of n (from the name)

Let $n$ be a natural number. Then the natural number of $n$ is a positive natural number defined as the successor natural number of the predecessor of $n$.

the quotient of m and k (from the name)

Let $m$ and $k$ be positive natural numbers. Then the quotient of $m$ and $k$ is a natural number defined as $\ProdsndMACRoAA {\operatorname{modDiv} (m , k)}$.

Let $m$ and $k$ be positive natural numbers. Then $\operatorname{divExact}$ applied to $m$ and $k$ is a positive natural number defined as the successor of the quotient of $m$ and $k$.

Let $m$ and $k$ be positive natural numbers. Then $\operatorname{mod}$ applied to $m$ and $k$ is a positive natural number defined as $\ProdfstMACRoZ {\operatorname{modDiv} (m , k)}$.

Let $m$ and $k$ be positive natural numbers. Then $\operatorname{modDiv}$ applied to $m$ and $k$ is an element of $\mathrm{Prod}$ applied to $\PNatMACRoAD$ and $\Natural$ defined as $\operatorname{modDivAux}$ applied to $k$, the remainder of the value of $m$ modulo the value of $k$ and the quotient of the value of $m$ and the value of $k$.

the natural predecessor of i (from the name)

Let $i$ be a positive natural number. Then the natural predecessor of $i$ is a natural number defined as the difference between the value of $i$ and $1$.

Let $\mathrm{mk}$ be a function from natural numbers $n$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (0 , n)$ to elements of $C$ applied to the natural number of $n$. Let $t$ be a positive natural number. Then $\operatorname{recToPNat}$ applied to $n$, $\mathrm{mk}$ and $t$ is an element of $C$ applied to $t$.

Let $n$ be a positive natural number. Let $x$ be a function from positive natural numbers $k$ and functions from positive natural numbers $m$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Lt} (m , k)$ to elements of $p$ applied to $m$ to elements of $p$ applied to $k$. Then $\operatorname{strongInductionOn}$ applied to $n$, $k$ and $x$ is an element of $p$ applied to $n$ defined as the function that maps $x$ to $\mathrm{PNat\_\_strongInductionOn\_\_\_unary}$ applied to $k$, $n$ and $x$.

$\operatorname{pnatEquivNat}$ is an equivalence from $\PNatMACRoAD$ to $\Natural$ defined as $\operatorname{mk}$ applied to $\operatorname{natPred}$, $\operatorname{succPNat}$, $\mathrm{PNat\_\_succPNat\_natPred}$ and $\mathrm{Nat\_\_natPred\_succPNat}$.

the factor multiset of n (from the name)

Let $n$ be a positive natural number. Then the factor multiset of $n$ is a prime multiset.

the factor multiset equivalence (from the name)

The factor multiset equivalence is an equivalence from $\PNatMACRoAD$ to the set of prime multisets defined as $\operatorname{mk}$ applied to $\operatorname{factorMultiset}$, $\operatorname{prod}$, $\mathrm{PNat\_\_prod\_factorMultiset}$ and $\mathrm{PrimeMultiset\_\_factorMultiset\_prod}$.

prime multiset (from the name)

A prime multiset is a multiset of $\NatPrimesMACRoA$.

the coercion natural monoid homomorphism (from the name)

The coercion natural monoid homomorphism is an additive monoid homomorphism of the set of prime multisets and the set of multisets of $\Natural$ defined as the map additive monoid homomorphism of the function that maps $p$ to the proposition that $p$ is prime.

the coercion natural monoid homomorphism (from the name)

The coercion natural monoid homomorphism is an additive monoid homomorphism of the set of prime multisets and the set of multisets of $\PNatMACRoAD$ defined as the map additive monoid homomorphism of $\operatorname{toPNat}$.

the prime multiset of l and h (from the name)

Let $l$ be a list of natural numbers such that for all natural numbers $p$, if $p$ is an element of $l$, then $p$ is prime. Then the prime multiset of $l$ and $h$ is a prime multiset defined as the prime multiset of the multiset of $l$ and $h$.

the prime multiset of v and h (from the name)

Let $v$ be a multiset of $\Natural$ such that for all natural numbers $p$, if $p$ is an element of $v$, then $p$ is prime. Then the prime multiset of $v$ and $h$ is a prime multiset defined as $\operatorname{pmap}$ applied to the function that maps $p$ and $\mathrm{hp}$ to $p$, $v$ and $h$.

the prime multiset of l and h (from the name)

Let $l$ be a list of positive natural numbers such that for all positive natural numbers $p$, if $p$ is an element of $l$, then $p$ is prime. Then the prime multiset of $l$ and $h$ is a prime multiset defined as the prime multiset of the multiset of $l$ and $h$.

the prime multiset of v and h (from the name)

Let $v$ be a multiset of $\PNatMACRoAD$ such that for all positive natural numbers $p$, if $p$ is an element of $v$, then $p$ is prime. Then the prime multiset of $v$ and $h$ is a prime multiset defined as $\operatorname{pmap}$ applied to the function that maps $p$ and $\mathrm{hp}$ to the value of $p$, $v$ and $h$.

the multiset consisting of p (from the docstring)

Let $p$ be a prime number. Then the multiset consisting of $p$ is a prime multiset defined as $\operatorname{singleton}$ applied to $p$.

the product of v (from the docstring)

Let $v$ be a prime multiset. Then the product of $v$ is a positive natural number defined as the product of the natural multiset of $v$.

the natural multiset of x (from the name)

Let $x$ be a prime multiset. Then the natural multiset of $x$ is a multiset of $\Natural$ defined as the map of the function that maps $p$ to the proposition that $p$ is prime and $x$.

the natural multiset of x (from the name)

Let $x$ be a prime multiset. Then the natural multiset of $x$ is a multiset of $\PNatMACRoAD$ defined as the map of $\operatorname{toPNat}$ and $x$.

Assume that there exists a positive natural number $n$, such that $p$ holds for $n$. Then $\operatorname{find}$ applied to $h$ is a positive natural number defined as $\operatorname{findX}$ applied to $h$.

Assume that there exists a positive natural number $n_{1}$, such that $p$ holds for $n_{1}$. Then $\operatorname{findX}$ applied to $h$ is an element of $\SubtypeSet {n}{\mathrm{and} (p (n), \mathrm{forall} (\PNatMACRoAD , \lambda m . \mathrm{if} (\mathrm{Lt} (m , n), \mathrm{not} (p (m)))))}$.

positive natural number (by hand)

$\PNatMACRoAD$ is a set defined as $\SubtypeSet {n}{\mathrm{Lt} (0 , n)}$.

the value of x (from the name)

Let $x$ be a positive natural number. Then the value of $x$ is a natural number defined as $\mathrm{Lt} (0 , x)$.

the natural number of x (from the name)

Let $x$ be a prime number. Then the natural number of $x$ is a positive natural number defined as $x$.

m is coprime to n (from the name)

Let $m$ and $n$ be positive natural numbers. Then $m$ is coprime to $n$, if the greatest common divisor of $m$ and $n$ is equal to $1$.

p is prime (from the name)

Let $p$ be a positive natural number. Then $p$ is prime, if the value of $p$ is prime.

the greatest common divisor of n and m (from the name)

Let $n$ and $m$ be positive natural numbers. Then the greatest common divisor of $n$ and $m$ is a positive natural number defined as the greatest common divisor of the value of $n$ and the value of $m$.

the least common multiple of n and m (from the name)

Let $n$ and $m$ be positive natural numbers. Then the least common multiple of $n$ and $m$ is a positive natural number defined as the least common multiple of the value of $n$ and the value of $m$.

The elements of $\operatorname{XgcdType}$ are a basic type.

u is reduced (from the name)

Let $u$ be an element of $\operatorname{XgcdType}$. Then $u$ is reduced, if $\operatorname{ap} (u)= \operatorname{bp} (u)$.

u is reduced (from the name)

Let $u$ be an element of $\operatorname{XgcdType}$. Then $u$ is reduced, if $\EqtMACRoH {\operatorname{a} (u)}{\operatorname{b} (u)}$.

u is special (from the name)

Let $u$ be an element of $\operatorname{XgcdType}$. Then $u$ is special, if $\operatorname{wp} (u)+ \operatorname{zp} (u)+ \operatorname{wp} (u)\times \operatorname{zp} (u)= \operatorname{x} (u)\times \operatorname{y} (u)$.

u is special (from the name)

Let $u$ be an element of $\operatorname{XgcdType}$. Then $u$ is special, if $\operatorname{w} (u)\times \operatorname{z} (u)$ is equal to the successor natural number of $\operatorname{x} (u)\times \operatorname{y} (u)$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{a}$ applied to $u$ is a positive natural number defined as the successor natural number of $\operatorname{ap}$ applied to $u$.

Let $\mathrm{self}$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{ap}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{b}$ applied to $u$ is a positive natural number defined as the successor natural number of $\operatorname{bp}$ applied to $u$.

Let $\mathrm{self}$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{bp}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj5}$ applied to $\mathrm{self}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{finish}$ applied to $u$ is an element of $\operatorname{XgcdType}$ defined as $\operatorname{mk}$ applied to $\operatorname{wp}$ applied to $u$, $(\operatorname{wp} (u)+ 1)\times \operatorname{qp} (u)+ \operatorname{x} (u)$, $\operatorname{y}$ applied to $u$, $\operatorname{y} (u)\times \operatorname{qp} (u)+ \operatorname{zp} (u)$, $\operatorname{bp}$ applied to $u$ and $\operatorname{bp}$ applied to $u$.

the flip of u (from the name)

Let $u$ be an element of $\operatorname{XgcdType}$. Then the flip of $u$ is an element of $\operatorname{XgcdType}$ defined as $\operatorname{mk}$ applied to $\operatorname{zp}$ applied to $u$, $\operatorname{y}$ applied to $u$, $\operatorname{x}$ applied to $u$, $\operatorname{wp}$ applied to $u$, $\operatorname{bp}$ applied to $u$ and $\operatorname{ap}$ applied to $u$.

Let $w$, $z$, $a$ and $b$ be positive natural numbers. Let $x$ and $y$ be natural numbers. Then $\operatorname{mk'}$ applied to $w$, $x$, $y$, $z$, $a$ and $b$ is an element of $\operatorname{XgcdType}$ defined as $\operatorname{mk}$ applied to the predecessor of the value of $w$, $x$, $y$, the predecessor of the value of $z$, the predecessor of the value of $a$ and the predecessor of the value of $b$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{q}$ applied to $u$ is a natural number defined as $\frac{ \operatorname{ap} (u)+ 1}{\operatorname{bp} (u)+ 1}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{qp}$ applied to $u$ is a natural number defined as $\operatorname{q} (u)- 1$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{r}$ applied to $u$ is a natural number defined as $\HModhModMACRoF {(\operatorname{ap} (u)+ 1)}{(\operatorname{bp} (u)+ 1)}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{reduce}$ applied to $u$ is an element of $\operatorname{XgcdType}$.

the start of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the start of $a$ and $b$ is an element of $\operatorname{XgcdType}$ defined as $\operatorname{mk}$ applied to $0$, $0$, $0$, $0$, the difference between the value of $a$ and $1$ and the difference between the value of $b$ and $1$.

the step of u (from the name)

Let $u$ be an element of $\operatorname{XgcdType}$. Then the step of $u$ is an element of $\operatorname{XgcdType}$ defined as $\operatorname{mk}$ applied to $\operatorname{y} (u)\times \operatorname{q} (u)+ \operatorname{zp} (u)$, $\operatorname{y}$ applied to $u$, $(\operatorname{wp} (u)+ 1)\times \operatorname{q} (u)+ \operatorname{x} (u)$, $\operatorname{wp}$ applied to $u$, $\operatorname{bp}$ applied to $u$ and $\operatorname{r} (u)- 1$.

the successor of t (from the name)

Let $t$ be an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$. Then the successor of $t$ is an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\ProdmkMACRoU {\mathrm{succ} (\ProdfstMACRoZ {t})}{\mathrm{succ} (\ProdsndMACRoAA {t})}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{v}$ applied to $u$ is an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\ProdmkMACRoU {(\operatorname{val} (\operatorname{w} (u))\times \operatorname{val} (\operatorname{a} (u))+ \operatorname{x} (u)\times \operatorname{val} (\operatorname{b} (u)))}{(\operatorname{y} (u)\times \operatorname{val} (\operatorname{a} (u))+ \operatorname{val} (\operatorname{z} (u))\times \operatorname{val} (\operatorname{b} (u)))}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{vp}$ applied to $u$ is an element of $\mathrm{Prod}$ applied to $\Natural$ and $\Natural$ defined as $\ProdmkMACRoU {(\operatorname{wp} (u)+ \operatorname{x} (u)+ \operatorname{ap} (u)+ \operatorname{wp} (u)\times \operatorname{ap} (u)+ \operatorname{x} (u)\times \operatorname{bp} (u))}{(\operatorname{y} (u)+ \operatorname{zp} (u)+ \operatorname{bp} (u)+ \operatorname{y} (u)\times \operatorname{ap} (u)+ \operatorname{zp} (u)\times \operatorname{bp} (u))}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{w}$ applied to $u$ is a positive natural number defined as the successor natural number of $\operatorname{wp}$ applied to $u$.

Let $\mathrm{self}$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{wp}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{x}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Let $\mathrm{self}$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{y}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Let $u$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{z}$ applied to $u$ is a positive natural number defined as the successor natural number of $\operatorname{zp}$ applied to $u$.

Let $\mathrm{self}$ be an element of $\operatorname{XgcdType}$. Then $\operatorname{zp}$ applied to $\mathrm{self}$ is a natural number defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the greatest common divisor of $a$ and $b$ is a positive natural number defined as the successor natural number of $\operatorname{wp} (\operatorname{xgcd} (a , b))+ \operatorname{x} (\operatorname{xgcd} (a , b))$.

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the greatest common divisor of $a$ and $b$ is a positive natural number defined as the successor natural number of $\operatorname{y} (\operatorname{xgcd} (a , b))+ \operatorname{zp} (\operatorname{xgcd} (a , b))$.

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the greatest common divisor of $a$ and $b$ is a positive natural number defined as $\operatorname{a}$ applied to $\operatorname{xgcd}$ applied to $a$ and $b$.

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the greatest common divisor of $a$ and $b$ is a positive natural number defined as $\operatorname{w}$ applied to $\operatorname{xgcd}$ applied to $a$ and $b$.

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the greatest common divisor of $a$ and $b$ is a natural number defined as $\operatorname{x}$ applied to $\operatorname{xgcd}$ applied to $a$ and $b$.

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the greatest common divisor of $a$ and $b$ is a natural number defined as $\operatorname{y}$ applied to $\operatorname{xgcd}$ applied to $a$ and $b$.

the greatest common divisor of a and b (from the name)

Let $a$ and $b$ be positive natural numbers. Then the greatest common divisor of $a$ and $b$ is a positive natural number defined as $\operatorname{z}$ applied to $\operatorname{xgcd}$ applied to $a$ and $b$.

the default (from the name)

The default is an element of $\operatorname{XgcdType}$ defined as $\operatorname{mk}$ applied to $\operatorname{default}$, $\operatorname{default}$, $\operatorname{default}$, $\operatorname{default}$, $\operatorname{default}$ and $\operatorname{default}$.

Let $a$ and $b$ be positive natural numbers. Then $\operatorname{xgcd}$ applied to $a$ and $b$ is an element of $\operatorname{XgcdType}$ defined as $\operatorname{reduce}$ applied to the start of $a$ and $b$.

part of x (from the name)

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

self is a domain (from the name)

Let $\mathrm{self}$ be a part of $x$. Then $\mathrm{self}$ is a domain, if $\operatorname{proj0}$ holds for $\mathrm{self}$.

Let $o$ be a part of $x$. Let $a$ be an element of $x$. Then $\operatorname{Mem}$ holds for $o$ and $a$, if there exists an element $h$ of $\operatorname{Dom}$ applied to $o$, such that $\EqtMACRoH {\operatorname{get} (o , h)}{a}$.

Let $p$ be a proposition. Let $f$ be a function from elements of $\mathrm{Proof}$ applied to $p$ to parts of $x$. Then $\operatorname{assert}$ applied to $p$ and $f$ is a part of $x$.

Let $f$ be a part of $x$. Let $g$ be a function from elements of $x$ to parts of $x_{1}$. Then $\operatorname{bind}$ applied to $f$ and $g$ is a part of $x_{1}$ defined as $\operatorname{assert}$ applied to the proposition that $f$ is a domain and the function that maps $b$ to $g$ applied to $\operatorname{get}$ applied to $f$ and $b$.

the equivalence option (from the name)

The equivalence option is an equivalence from the set of parts of $x$ to $\mathrm{Option}$ applied to $x$.

Let $\mathrm{self}$ be a part of $x$ such that $\mathrm{self}$ is a domain. Then $\operatorname{get}$ applied to $\mathrm{self}$ and $h$ is an element of $x$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $h$.

Let $a$ be a part of $x$. Let $d$ be an element of $x$. Then $\operatorname{getOrElse}$ applied to $a$ and $d$ is an element of $x$ defined as $\mathrm{dite}$ applied to the proposition that $a$ is a domain, the function that maps $\mathrm{ha}$ to $\operatorname{get}$ applied to $a$ and $\mathrm{ha}$ and the function that maps $\mathrm{ha1}$ to $d$.

the map of f and o (from the name)

Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Let $o$ be a part of $x$. Then the map of $f$ and $o$ is a part of $x_{1}$ defined as $\operatorname{mk}$ applied to the proposition that $o$ is a domain and $\operatorname{comp}$ applied to $f$ and $\operatorname{get}$ applied to $o$.

the none (from the name)

The none is a part of $x$.

the part of x1 (from the name)

Let $x_{1}$ be an element of $\mathrm{Option}$ applied to $x$. Then the part of $x_{1}$ is a part of $x$.

Let $p$ be a proposition. Let $o$ be a part of $x$ such that if $p$, then $o$ is a domain. Then $\operatorname{restrict}$ applied to $p$, $o$ and $H$ is a part of $x$ defined as $\operatorname{mk}$ applied to $p$ and the function that maps $h$ to $\operatorname{get}$ applied to $o$ and $H$ applied to $h$.

Let $a$ be an element of $x$. Then $\operatorname{some}$ applied to $a$ is a part of $x$ defined as $\operatorname{mk}$ applied to $\mathrm{True}$ and the function that maps $h$ to $a$.

the option of o (from the name)

Let $o$ be a part of $x$. Then the option of $o$ is an element of $\mathrm{Option}$ applied to $x$ defined as $\mathrm{dite}$ applied to the proposition that $o$ is a domain, the function that maps $h$ to $\operatorname{some}$ applied to $\operatorname{get}$ applied to $o$ and $h$ and the function that maps $h_{1}$ to $\operatorname{none}$.

Let $o$ be a part of $x$. Then $\operatorname{unwrap}$ applied to $o$ is an element of $x$.