Index

#	Type.Family.Tuple
&&	Type.Family.Bool
*	Type.Family.Nat
*:	Data.Type.Vector
+	Type.Family.Nat
++	Type.Family.List
+:	Data.Type.Vector
.&&	Data.Type.Boolean
.&.	Data.Type.Conjunction
.*	Data.Type.Nat
.+	Data.Type.Nat
.++	Data.Type.Vector
.==	Data.Type.Boolean
.?	Data.Type.Boolean
.\\	Data.Type.Product.Env
.^	Data.Type.Nat
.^^	Data.Type.Boolean
.\|\|	Data.Type.Boolean
//	Type.Class.Witness
//?	Type.Class.Witness
//?+	Type.Class.Witness
:&&:
1 (Type/Class)	Data.Type.Conjunction
2 (Data Constructor)	Data.Type.Conjunction
:&:
1 (Type/Class)	Data.Type.Conjunction
2 (Data Constructor)	Data.Type.Conjunction
:*	Data.Type.Vector
:*:
1 (Type/Class)	Data.Type.Conjunction
2 (Data Constructor)	Data.Type.Conjunction
:+	Data.Type.Vector
:+:	Data.Type.Disjunction
:-
1 (Type/Class)	Type.Class.Witness
2 (Data Constructor)	Data.Type.Difference
:.:	Data.Type.Combinator
::<	Data.Type.Product
:<
1 (Type/Class)	Type.Family.List
2 (Data Constructor)	Data.Type.Product, Data.Type.Subset
:<<	Data.Type.Product.Lifted
:>	Data.Type.Product
:>>	Data.Type.Product.Lifted
:\|:	Data.Type.Disjunction
:~:	Type.Class.Witness, Data.Type.Index.Trans
<	Type.Family.Nat
<#	Type.Class.Higher
<##	Type.Class.Higher
<###	Type.Class.Higher
<$>
1 (Type/Class)	Type.Family.Tuple
2 (Type/Class)	Type.Family.List
3 (Type/Class)	Type.Family.Either
4 (Type/Class)	Type.Family.Maybe
<&>
1 (Type/Class)	Type.Family.Tuple
2 (Type/Class)	Type.Family.List
3 (Type/Class)	Type.Family.Either
4 (Type/Class)	Type.Family.Maybe
<*>
1 (Type/Class)	Type.Family.Tuple
2 (Type/Class)	Type.Family.List
3 (Type/Class)	Type.Family.Either
4 (Type/Class)	Type.Family.Maybe
<=	Type.Family.Nat
<=#	Type.Class.Higher
<=##	Type.Class.Higher
<=###	Type.Class.Higher
<==>
1 (Type/Class)	Type.Family.Bool
2 (Function)	Data.Type.Boolean
<>	Type.Family.Monoid
<\|>
1 (Type/Class)	Type.Family.Either
2 (Type/Class)	Type.Family.Maybe
=###=	Type.Class.Higher
=##=	Type.Class.Higher
=#=	Type.Class.Higher
==	Type.Class.Witness, Type.Family.Bool
==>
1 (Type/Class)	Type.Family.Bool
2 (Function)	Data.Type.Boolean
=?=	Type.Class.Witness
=??=	Type.Class.Witness
>	Type.Family.Nat
>#	Type.Class.Higher
>##	Type.Class.Higher
>###	Type.Class.Higher
>+<	Data.Type.Disjunction
>--->	Type.Class.Higher
>-->	Type.Class.Higher
>->	Type.Class.Higher
>:
1 (Type/Class)	Type.Family.List
2 (Function)	Data.Type.Product
>::	Data.Type.Product
>=	Type.Family.Nat
>=#	Type.Class.Higher
>=##	Type.Class.Higher
>=###	Type.Class.Higher
>>-	Type.Class.Higher
>>--	Type.Class.Higher
>>---	Type.Class.Higher
>>:	Data.Type.Product.Lifted
>>=-	Type.Class.Higher
>>=--	Type.Class.Higher
>>=---	Type.Class.Higher
>>=~	Type.Class.Higher
>>~	Type.Class.Higher
>\|<	Data.Type.Disjunction
absurd	Type.Class.Witness
absurdC	Type.Class.Witness
addCong	Type.Family.Nat
addS	Data.Type.Nat
AddW
1 (Type/Class)	Type.Family.Nat
2 (Data Constructor)	Type.Family.Nat
addZ	Data.Type.Nat
append'	Data.Type.Product
appendCong	Type.Family.List
appendF	Data.Type.Product.Lifted
apply	Type.Class.Witness
Bifunctor1	Type.Class.Higher
bimap1	Type.Class.Higher
BoolC	Type.Family.Bool
Boolean	Data.Type.Boolean
BoolEquality	Data.Type.Boolean
boolEquality	Data.Type.Boolean
bottom	Type.Class.Witness
C
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
castWith	Type.Class.Witness
commute	Type.Class.Witness
Comp
1 (Type/Class)	Type.Family.Constraint
2 (Data Constructor)	Data.Type.Combinator
Comp1
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
compare1	Type.Class.Higher
compare2	Type.Class.Higher
compare3	Type.Class.Higher
compC	Type.Class.Witness
compose	Data.Type.Vector
Concat	Type.Family.List
concatCong	Type.Family.List
Conj
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
conjC	Type.Class.Witness
Const	Type.Class.Witness
constC	Type.Class.Witness
Constraint	Type.Family.Constraint
contraC	Type.Class.Witness
Cur
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
Cur3
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
curry'	Data.Type.Product
curryF	Data.Type.Product.Lifted
curryFan	Data.Type.Conjunction
curryPar	Data.Type.Conjunction
Dec	Type.Class.Witness
decCase	Type.Class.Witness
DecEquality	Type.Class.Witness
decideEquality	Type.Class.Witness
decomp	Data.Type.Sum
Delete	Data.Type.Product.Env
delete'	Data.Type.Product.Env
diagonal	Data.Type.Vector
Difference
1 (Type/Class)	Data.Type.Difference
2 (Type/Class)	Data.Type.Product.Env
difference'	Data.Type.Product.Env
diffLen	Data.Type.Difference
diffProd	Data.Type.Difference
diffSum	Data.Type.Difference
disjC	Type.Class.Witness
eitherAltCong	Type.Family.Either
eitherApCong	Type.Family.Either
EitherC	Type.Family.Either
eitherC	Type.Class.Witness
eitherFmapCong	Type.Family.Either
eitherPamfCong	Type.Family.Either
Elem	Data.Type.Index
elemIndex	Data.Type.Index
elimDifference	Data.Type.Difference
elimFin	Data.Type.Fin
elimIndex	Data.Type.Index
elimLength	Data.Type.Length
elimNat	Data.Type.Nat
elimProd	Data.Type.Product
elimRemove	Data.Type.Remove
elimSum	Data.Type.Sum
elimV	Data.Type.Vector
elimVecT	Data.Type.Vector
entailed	Type.Class.Witness
Env
1 (Type/Class)	Data.Type.Product.Env
2 (Data Constructor)	Data.Type.Product.Env
Eq1	Type.Class.Higher
eq1	Type.Class.Higher
Eq2	Type.Class.Higher
eq2	Type.Class.Higher
Eq3	Type.Class.Higher
eq3	Type.Class.Higher
EQS	Data.Type.Nat.Inequality
EQZ	Data.Type.Nat.Inequality
Every	Data.Type.Index
every	Data.Type.Index
Every2	Data.Type.Index
every2	Data.Type.Index
EveryC	Data.Type.Index
exConjEq	Data.Type.Conjunction
exFalso	Type.Class.Witness
expCong	Type.Family.Nat
Fail	Type.Family.Constraint
failC	Type.Class.Witness
Fails	Type.Class.Witness
False_	Data.Type.Boolean
falso	Type.Class.Witness
fanFirst	Data.Type.Conjunction
fanFst	Data.Type.Conjunction
fanSnd	Data.Type.Conjunction
fdecomp	Data.Type.Sum.Lifted
Fin	Data.Type.Fin
fin	Data.Type.Fin
findex	Data.Type.Sum.Lifted
findV	Data.Type.Vector
findVecT	Data.Type.Vector
finj	Data.Type.Sum.Lifted
FInL	Data.Type.Sum.Lifted
finNat	Data.Type.Fin
FInR	Data.Type.Sum.Lifted
fins	Data.Type.Fin
finZ	Data.Type.Fin
Flip
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
flipTestEquality1	Data.Type.Combinator
Foldable1	Type.Class.Higher
foldMap1	Type.Class.Higher
Forall	Type.Class.Witness
forall	Type.Class.Witness
fprj	Data.Type.Sum.Lifted
FProd	Data.Type.Product.Lifted
fromInt	Type.Family.Nat
FromJust	Type.Family.Maybe
fromJustCong	Type.Family.Maybe
FromLeft	Type.Family.Either
fromLeftCong	Type.Family.Either
FromRight	Type.Family.Either
fromRightCong	Type.Family.Either
FS	Data.Type.Fin
Fst	Type.Family.Tuple
Fst3	Type.Family.Tuple
fst3Cong	Type.Family.Tuple
fstCong	Type.Family.Tuple
Fsts	Type.Family.List
Fsts3	Type.Family.List
FSum	Data.Type.Sum.Lifted
Functor1	Type.Class.Higher
FZ	Data.Type.Fin
gcastWith	Type.Class.Witness
getC	Data.Type.Combinator
getComp	Data.Type.Combinator
getComp1	Data.Type.Combinator
getCur	Data.Type.Combinator
getCur3	Data.Type.Combinator
getEnv	Data.Type.Product.Env
getFlip	Data.Type.Combinator
getI	Data.Type.Combinator
getJoin	Data.Type.Combinator
getLL	Data.Type.Combinator
getMatrix	Data.Type.Vector
getRR	Data.Type.Combinator
getSub	Type.Class.Witness
getUncur	Data.Type.Combinator
getUncur3	Data.Type.Combinator
GTS	Data.Type.Nat.Inequality
GTZ	Data.Type.Nat.Inequality
Head	Type.Family.List
head'
1 (Function)	Data.Type.Product
2 (Function)	Data.Type.Vector
headF	Data.Type.Product.Lifted
HeadM	Type.Family.List
Holds	Type.Class.Witness
I
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
ibimap1	Type.Class.Higher
If	Type.Family.Bool
if'	Data.Type.Boolean
Iff	Type.Family.Constraint
IffC	Type.Family.Constraint
IFin	Data.Type.Fin.Indexed
ifinNat	Data.Type.Fin.Indexed
ifinVal	Data.Type.Fin.Indexed
ifinZ	Data.Type.Fin.Indexed
ifoldMap	Data.Type.Vector
ifoldMap1	Type.Class.Higher
ifoldMapF	Data.Type.Product.Lifted
ifoldMapFSum	Data.Type.Sum.Lifted
IFS	Data.Type.Fin.Indexed
IFZ	Data.Type.Fin.Indexed
imap	Data.Type.Vector
imap1	Type.Class.Higher
imapF	Data.Type.Product.Lifted
imapFSum	Data.Type.Sum.Lifted
impossible	Type.Class.Witness
Index	Data.Type.Index
index
1 (Function)	Data.Type.Sum
2 (Function)	Data.Type.Product
3 (Function)	Data.Type.Vector
index'	Data.Type.Vector
indexF	Data.Type.Product.Lifted
indices	Data.Type.Product
indices'	Data.Type.Product
Init	Type.Family.List
Init'	Type.Family.List
init'	Data.Type.Product
initCong	Type.Family.List
initF	Data.Type.Product.Lifted
InitM	Type.Family.List
inj	Data.Type.Sum
injectFSum	Data.Type.Sum.Lifted
injectSum	Data.Type.Sum
InL	Data.Type.Sum
inner	Type.Class.Witness
InR	Data.Type.Sum
Insert	Data.Type.Product.Env
insert'	Data.Type.Product.Env
Intersection	Data.Type.Product.Env
intersection'	Data.Type.Product.Env
Iota	Type.Family.Nat
iotaCong	Type.Family.Nat
IS	Data.Type.Index
IsLeft	Type.Family.Either
IsNothing	Type.Family.Maybe
IsRight	Type.Family.Either
IsZero	Type.Family.Nat
itraverse	Data.Type.Vector
itraverse1	Type.Class.Higher
itraverseF	Data.Type.Product.Lifted
itraverseFSum	Data.Type.Sum.Lifted
Ix	Type.Family.Nat
IxBifunctor1	Type.Class.Higher
IxComp
1 (Type/Class)	Data.Type.Index.Trans
2 (Data Constructor)	Data.Type.Index.Trans
ixCong	Type.Family.Nat
IxEnv	Data.Type.Index.Trans
IxFirst
1 (Type/Class)	Data.Type.Index.Trans
2 (Data Constructor)	Data.Type.Index.Trans
IxFoldable1	Type.Class.Higher
IxFunctor1	Type.Class.Higher
IxHead	Data.Type.Index.Trans
IxJust
1 (Type/Class)	Data.Type.Index.Trans
2 (Data Constructor)	Data.Type.Index.Trans
IxLift	Data.Type.Index.Trans
ixLift	Data.Type.Index.Trans
IxList	Data.Type.Index.Trans
ixList	Data.Type.Product.Env
IxList'	Data.Type.Index.Trans
ixNil	Data.Type.Index
IxOr	Data.Type.Index.Trans
IxOrL	Data.Type.Index.Trans
IxOrR	Data.Type.Index.Trans
ixRem	Data.Type.Remove
IxSecond
1 (Type/Class)	Data.Type.Index.Trans
2 (Data Constructor)	Data.Type.Index.Trans
IxTail	Data.Type.Index.Trans
IxTraversable1	Type.Class.Higher
IZ	Data.Type.Index
Join
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
Just_	Data.Type.Option
Known	Type.Class.Known
known	Type.Class.Known
KnownC	Type.Class.Known
L	Data.Type.Disjunction
L'	Data.Type.Disjunction
Last	Type.Family.List
Last'	Type.Family.List
last'	Data.Type.Product
lastCong	Type.Family.List
lastF	Data.Type.Product.Lifted
LastM	Type.Family.List
leftCong	Type.Family.Either
leftNotRight	Type.Family.Either
Len	Type.Family.Nat
lenCong	Type.Family.Nat
Length	Data.Type.Length
LessEq	Data.Type.Fin.Indexed
lEven	Data.Type.Length
LiftI	Data.Type.Index.Trans
liftIFin	Data.Type.Fin.Indexed
ListC	Type.Family.List
listMapCong	Type.Family.List
LL
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
lOdd	Data.Type.Length
Lookup	Data.Type.Product.Env
lookup'	Data.Type.Product.Env
lookupPar	Data.Type.Product
LS	Data.Type.Length
LTC	Data.Type.Fin.Indexed
LTS	Data.Type.Nat.Inequality
LTZ	Data.Type.Nat.Inequality
LZ	Data.Type.Length
M
1 (Type/Class)	Data.Type.Vector
2 (Data Constructor)	Data.Type.Vector
m0	Data.Type.Vector
m1	Data.Type.Vector
m2	Data.Type.Vector
m3	Data.Type.Vector
m4	Data.Type.Vector
map1	Type.Class.Higher
mapC	Data.Type.Combinator
mapCur	Data.Type.Combinator
mapCur3	Data.Type.Combinator
mapFlip	Data.Type.Combinator
mapJoin	Data.Type.Combinator
mapUncur	Data.Type.Combinator
mapUncur3	Data.Type.Combinator
Matrix	Data.Type.Vector
maybeAltCong	Type.Family.Maybe
maybeApCong	Type.Family.Maybe
MaybeC	Type.Family.Maybe
maybeFmapCong	Type.Family.Maybe
maybePamfCong	Type.Family.Maybe
Member	Data.Type.Product.Env
member'	Data.Type.Product.Env
Mempty	Type.Family.Monoid
mgen	Data.Type.Vector
mgen_	Data.Type.Vector
msome	Type.Class.Higher
msome2	Type.Class.Higher
msome3	Type.Class.Higher
msomeC	Type.Class.Higher
mulCong	Type.Family.Nat
MulW
1 (Type/Class)	Type.Family.Nat
2 (Data Constructor)	Type.Family.Nat
mzipWith	Data.Type.Vector
N	Type.Family.Nat
N0	Type.Family.Nat
N1	Type.Family.Nat
N10	Type.Family.Nat
N2	Type.Family.Nat
N3	Type.Family.Nat
N4	Type.Family.Nat
N5	Type.Family.Nat
N6	Type.Family.Nat
N7	Type.Family.Nat
N8	Type.Family.Nat
N9	Type.Family.Nat
Nat	Data.Type.Nat
natCompare	Data.Type.Nat.Inequality
NatEQ	Data.Type.Nat.Inequality
NatEq	Type.Family.Nat
NatGT	Data.Type.Nat.Inequality
NatLT	Data.Type.Nat.Inequality
natVal	Data.Type.Nat
neq1	Type.Class.Higher
neq2	Type.Class.Higher
neq3	Type.Class.Higher
nilFSum	Data.Type.Sum.Lifted
nilNotCons	Type.Family.List
nilSum	Data.Type.Sum
Not	Type.Family.Bool
not'	Data.Type.Boolean
nothingCong	Type.Family.Maybe
nothingNotJust	Type.Family.Maybe
Nothing_	Data.Type.Option
Null	Type.Family.List
nullCong	Type.Family.List
onHead'	Data.Type.Product
onHeadF	Data.Type.Product.Lifted
onIFinPred	Data.Type.Fin.Indexed
onIxPred	Data.Type.Index
Only	Type.Family.List
only	Data.Type.Product
onlyF	Data.Type.Product.Lifted
only_	Data.Type.Product
onMatrix	Data.Type.Vector
onNatPred	Data.Type.Nat
onSome	Type.Class.Higher
onSome2	Type.Class.Higher
onSome3	Type.Class.Higher
onTail	Data.Type.Vector
onTail'	Data.Type.Product
onTailF	Data.Type.Product.Lifted
Option	Data.Type.Option
option	Data.Type.Option
Ord1	Type.Class.Higher
Ord2	Type.Class.Higher
Ord3	Type.Class.Higher
outer	Type.Class.Witness
pairMapCong	Type.Family.Tuple
parFst	Data.Type.Conjunction
parSnd	Data.Type.Conjunction
permute	Data.Type.Product
permute'	Data.Type.Product
Pos	Type.Family.Nat
ppMatrix	Data.Type.Vector
ppMatrix'	Data.Type.Vector
ppVec	Data.Type.Vector
Pred	Type.Family.Nat
pred'	Data.Type.Nat
predCong	Type.Family.Nat
prj	Data.Type.Sum
Prod	Data.Type.Product, Data.Type.Subset
Proven	Type.Class.Witness
pureC	Type.Class.Witness
qed	Type.Class.Witness
R	Data.Type.Disjunction
R'	Data.Type.Disjunction
Read1	Type.Class.Higher
Read2	Type.Class.Higher
Read3	Type.Class.Higher
readMaybe1	Type.Class.Higher
readMaybe2	Type.Class.Higher
readMaybe3	Type.Class.Higher
reads1	Type.Class.Higher
reads2	Type.Class.Higher
reads3	Type.Class.Higher
readsPrec1	Type.Class.Higher
readsPrec2	Type.Class.Higher
readsPrec3	Type.Class.Higher
Refl	Type.Class.Witness, Data.Type.Index.Trans
Refuted	Type.Class.Witness
remIx	Data.Type.Remove
remLen	Data.Type.Remove
Remove	Data.Type.Remove
remProd	Data.Type.Remove
remSub	Data.Type.Remove
remSum	Data.Type.Remove
Reverse	Type.Family.List
reverse'	Data.Type.Product
reverseCong	Type.Family.List
reverseF	Data.Type.Product.Lifted
rightCong	Type.Family.Either
RR
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
RS	Data.Type.Remove
RZ	Data.Type.Remove
S	Type.Family.Nat
select	Data.Type.Product
Show1	Type.Class.Higher
show1	Type.Class.Higher
Show2	Type.Class.Higher
show2	Type.Class.Higher
Show3	Type.Class.Higher
show3	Type.Class.Higher
shows1	Type.Class.Higher
shows2	Type.Class.Higher
shows3	Type.Class.Higher
showsPrec1	Type.Class.Higher
showsPrec2	Type.Class.Higher
showsPrec3	Type.Class.Higher
Snd	Type.Family.Tuple
Snd3	Type.Family.Tuple
snd3Cong	Type.Family.Tuple
sndCong	Type.Family.Tuple
Snds	Type.Family.List
Snds3	Type.Family.List
snocCong	Type.Family.List
Some
1 (Type/Class)	Type.Class.Higher
2 (Data Constructor)	Type.Class.Higher
some	Type.Class.Higher
Some2
1 (Type/Class)	Type.Class.Higher
2 (Data Constructor)	Type.Class.Higher
some2	Type.Class.Higher
Some3
1 (Type/Class)	Type.Class.Higher
2 (Data Constructor)	Type.Class.Higher
some3	Type.Class.Higher
SomeC
1 (Type/Class)	Type.Class.Higher
2 (Data Constructor)	Type.Class.Higher
someC	Type.Class.Higher
Sub	Type.Class.Witness
subExt	Data.Type.Subset
subExtBy	Data.Type.Subset
subIx	Data.Type.Subset
subNil	Data.Type.Subset
subProd	Data.Type.Subset
subRefl	Data.Type.Subset
Subset	Data.Type.Subset
subSum	Data.Type.Subset
subTrans	Data.Type.Subset
Sum	Data.Type.Sum
sym	Type.Class.Witness
S_	Data.Type.Nat
Tail	Type.Family.List
tail'
1 (Function)	Data.Type.Product
2 (Function)	Data.Type.Vector
tailF	Data.Type.Product.Lifted
TailM	Type.Family.List
TestEquality	Type.Class.Witness
testEquality	Type.Class.Witness
TestEquality1	Type.Class.Witness
testEquality1	Type.Class.Witness
Thd3	Type.Family.Tuple
thd3Cong	Type.Family.Tuple
Thds3	Type.Family.List
toBool	Data.Type.Boolean
toEquality	Type.Class.Witness
toList	Data.Type.Product
top	Type.Class.Witness
trans	Type.Class.Witness
transC	Type.Class.Witness
transpose	Data.Type.Vector
Traversable1	Type.Class.Higher
traverse1	Type.Class.Higher
True_	Data.Type.Boolean
Tuple	Data.Type.Product
Uncur
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
Uncur3
1 (Type/Class)	Data.Type.Combinator
2 (Data Constructor)	Data.Type.Combinator
uncurry'	Data.Type.Product
uncurryF	Data.Type.Product.Lifted
uncurryFan	Data.Type.Conjunction
uncurryPar	Data.Type.Conjunction
Union	Data.Type.Product.Env
union'	Data.Type.Product.Env
vacuous	Type.Class.Witness
vap	Data.Type.Vector
vDel	Data.Type.Vector
Vec	Data.Type.Vector
VecT	Data.Type.Vector
vfoldMap	Data.Type.Vector
vfoldMap'	Data.Type.Vector
vfoldr	Data.Type.Vector
vgen	Data.Type.Vector
vgen_	Data.Type.Vector
vmap	Data.Type.Vector
Void	Type.Class.Witness
vrep	Data.Type.Vector
vtranspose	Data.Type.Vector
weaken
1 (Function)	Data.Type.Fin
2 (Function)	Data.Type.Fin.Indexed
Wit
1 (Type/Class)	Type.Class.Witness
2 (Data Constructor)	Type.Class.Witness
Wit1
1 (Type/Class)	Type.Class.Witness
2 (Data Constructor)	Type.Class.Witness
Without	Data.Type.Remove
without
1 (Function)	Data.Type.Fin
2 (Function)	Data.Type.Remove
WithoutAll	Data.Type.Difference
withoutAll	Data.Type.Difference
withSome	Type.Class.Higher
withSome2	Type.Class.Higher
withSome3	Type.Class.Higher
withV	Data.Type.Vector
withVecT	Data.Type.Vector
witMaybe	Type.Class.Witness
Witness	Type.Class.Witness
WitnessC	Type.Class.Witness
witnessed	Type.Class.Witness
Witnesses	Data.Type.Product
Z	Type.Family.Nat
zeroCong	Type.Family.Nat
Zip	Type.Family.List
zipLines	Data.Type.Vector
zNotS	Type.Family.Nat
Z_	Data.Type.Nat
\\	Type.Class.Witness
^	Type.Family.Nat
^^	Type.Family.Bool
_fst	Data.Type.Conjunction
_S	Data.Type.Nat
_s	Data.Type.Nat
_snd	Data.Type.Conjunction
_Z	Data.Type.Nat
_ZneS	Data.Type.Nat
\|\|	Type.Family.Bool
~~	Type.Class.Witness
Ø
1 (Type/Class)	Type.Family.List
2 (Data Constructor)	Data.Type.Product, Data.Type.Subset
ØC	Type.Family.Constraint
ØD	Data.Type.Difference
ØF	Data.Type.Product.Lifted
ØV	Data.Type.Vector
∈	Data.Type.Index
∘	Type.Class.Witness
∧	Type.Class.Witness
∨	Type.Class.Witness
⊆	Data.Type.Subset