Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(75519 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(245 entries)

Binder Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(61331 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(144 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(89 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(236 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6913 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1141 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(34 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(269 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(443 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(296 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(604 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(248 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3386 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(140 entries)

---

Q

qapp [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qapp [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qapp [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qapp [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qcase [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qcase [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qcase [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qcase [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qcofix [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qcofix [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qcofix [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qcofix [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qcofixs [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qcofixs [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qcofixs [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qcofixs [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qcofix_subst [lemma, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qconst [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qconst [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qconst [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qconst [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qfix [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qfix [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qfix [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qfix [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qfixs [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qfixs [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qfixs [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qfixs [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qfix_subst [lemma, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qi:3 [binder, in MetaCoq.Examples.constructor_tac]
qpres [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qpres [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qpres [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qpreserves [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qpreserves_wellformed [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
Qpreserves_True [instance, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qpreserves_closedn [instance, in MetaCoq.Erasure.ERemoveParams]
qpres_qcofix [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres_qfix [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres_qsubst [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres_qproj [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres_qcase [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres_qapp [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres_qcons [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qpres_qpres [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qpres:132 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qproj [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qproj [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qproj [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qproj [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qsubst [projection, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qsubst [record, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qsubst [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qsubst [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qsubst_Qcofixs [instance, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qsubst_Qfixs [instance, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qs:187 [binder, in MetaCoq.Template.EnvironmentTyping]
qt:243 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:246 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:251 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:254 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:44 [binder, in MetaCoq.Examples.demo]
qt:8 [binder, in MetaCoq.Examples.metacoq_tour]
qualid [definition, in MetaCoq.Template.Kernames]
q'':1191 [binder, in MetaCoq.Translations.MiniHoTT]
q'':1199 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q'':1245 [binder, in MetaCoq.Translations.MiniHoTT]
q'':1253 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q'':24 [binder, in MetaCoq.Template.utils.MCCompare]
q':1044 [binder, in MetaCoq.Translations.MiniHoTT]
q':1052 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1169 [binder, in MetaCoq.Translations.MiniHoTT]
q':1177 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1180 [binder, in MetaCoq.Translations.MiniHoTT]
q':1188 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1190 [binder, in MetaCoq.Translations.MiniHoTT]
q':1198 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1210 [binder, in MetaCoq.Translations.MiniHoTT]
q':1218 [binder, in MetaCoq.Translations.MiniHoTT]
q':1218 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1226 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1244 [binder, in MetaCoq.Translations.MiniHoTT]
q':1252 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1257 [binder, in MetaCoq.Translations.MiniHoTT]
q':1265 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':1307 [binder, in MetaCoq.Translations.MiniHoTT]
q':1315 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q':211 [binder, in MetaCoq.Template.utils.All_Forall]
q':23 [binder, in MetaCoq.Template.utils.MCCompare]
Q':2527 [binder, in MetaCoq.Template.utils.All_Forall]
Q':262 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Q':873 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q1:128 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
q1:146 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
q1:160 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
q1:2793 [binder, in MetaCoq.Translations.MiniHoTT]
q1:2801 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q1:2805 [binder, in MetaCoq.Translations.MiniHoTT]
q1:2813 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q1:328 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q2:129 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
q2:147 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
q2:161 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
q2:2795 [binder, in MetaCoq.Translations.MiniHoTT]
q2:2803 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q2:2807 [binder, in MetaCoq.Translations.MiniHoTT]
q2:2815 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q2:329 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:100 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:100 [binder, in MetaCoq.Translations.param_generous_packed]
q:1002 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:1009 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:101 [binder, in MetaCoq.PCUIC.PCUICElimination]
Q:1023 [binder, in MetaCoq.PCUIC.PCUICTyping]
q:1027 [binder, in MetaCoq.Translations.MiniHoTT]
Q:103 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:1030 [binder, in MetaCoq.PCUIC.PCUICTyping]
q:1035 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:104 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:1043 [binder, in MetaCoq.Translations.MiniHoTT]
q:1051 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:106 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:1060 [binder, in MetaCoq.Template.utils.All_Forall]
q:1062 [binder, in MetaCoq.Translations.MiniHoTT]
q:1070 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:108 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:108 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:108 [binder, in MetaCoq.PCUIC.PCUICConfluence]
q:1080 [binder, in MetaCoq.Translations.MiniHoTT]
q:1086 [binder, in MetaCoq.Translations.MiniHoTT]
q:1088 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1090 [binder, in MetaCoq.Template.utils.All_Forall]
q:1093 [binder, in MetaCoq.Translations.MiniHoTT]
q:1094 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:11 [binder, in MetaCoq.Template.utils.MCPred]
Q:110 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:110 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
q:1101 [binder, in MetaCoq.Translations.MiniHoTT]
q:1101 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1109 [binder, in MetaCoq.Translations.MiniHoTT]
q:1109 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1117 [binder, in MetaCoq.Translations.MiniHoTT]
q:1117 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1118 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:112 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
q:1124 [binder, in MetaCoq.Translations.MiniHoTT]
q:1125 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1131 [binder, in MetaCoq.Translations.MiniHoTT]
q:1132 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1137 [binder, in MetaCoq.Translations.MiniHoTT]
q:1139 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:114 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:1142 [binder, in MetaCoq.Translations.MiniHoTT]
q:1145 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1150 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1154 [binder, in MetaCoq.Translations.MiniHoTT]
Q:116 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:1160 [binder, in MetaCoq.Translations.MiniHoTT]
q:1162 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1165 [binder, in MetaCoq.PCUIC.PCUICReduction]
q:1168 [binder, in MetaCoq.Translations.MiniHoTT]
q:1168 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:117 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:1176 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1179 [binder, in MetaCoq.Translations.MiniHoTT]
q:1187 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1189 [binder, in MetaCoq.Translations.MiniHoTT]
q:119 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
q:1197 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:12 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
Q:120 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
q:1201 [binder, in MetaCoq.Translations.MiniHoTT]
Q:1209 [binder, in MetaCoq.Template.utils.All_Forall]
q:1209 [binder, in MetaCoq.Translations.MiniHoTT]
q:1209 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1217 [binder, in MetaCoq.Translations.MiniHoTT]
q:1217 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:122 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
q:1225 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1227 [binder, in MetaCoq.Translations.MiniHoTT]
q:1235 [binder, in MetaCoq.Translations.MiniHoTT]
q:1235 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:124 [binder, in MetaCoq.Template.EnvironmentTyping]
q:1243 [binder, in MetaCoq.Translations.MiniHoTT]
q:1243 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1251 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1256 [binder, in MetaCoq.Translations.MiniHoTT]
Q:126 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
q:1264 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1267 [binder, in MetaCoq.Translations.MiniHoTT]
q:1275 [binder, in MetaCoq.Translations.MiniHoTT]
q:1275 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1279 [binder, in MetaCoq.Translations.MiniHoTT]
q:1283 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1286 [binder, in MetaCoq.Translations.MiniHoTT]
q:1287 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:129 [binder, in MetaCoq.PCUIC.PCUICConfluence]
q:1294 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:13 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:130 [binder, in MetaCoq.Template.EnvironmentTyping]
q:1306 [binder, in MetaCoq.Translations.MiniHoTT]
Q:131 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:1314 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1315 [binder, in MetaCoq.Translations.MiniHoTT]
q:1323 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1325 [binder, in MetaCoq.Translations.MiniHoTT]
q:1333 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1336 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
q:1341 [binder, in MetaCoq.Translations.MiniHoTT]
q:1349 [binder, in MetaCoq.Template.utils.All_Forall]
q:1349 [binder, in MetaCoq.Translations.MiniHoTT]
q:1349 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1355 [binder, in MetaCoq.Translations.MiniHoTT]
q:1357 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1363 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1365 [binder, in MetaCoq.Translations.MiniHoTT]
q:1373 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1382 [binder, in MetaCoq.Template.utils.All_Forall]
q:1396 [binder, in MetaCoq.Translations.MiniHoTT]
q:1403 [binder, in MetaCoq.Translations.MiniHoTT]
q:1404 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1411 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:142 [binder, in MetaCoq.Template.utils.MCProd]
q:143 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:1453 [binder, in MetaCoq.Template.utils.All_Forall]
q:146 [binder, in MetaCoq.Template.utils.All_Forall]
Q:15 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
Q:150 [binder, in MetaCoq.Template.utils.All_Forall]
Q:1526 [binder, in MetaCoq.Template.utils.All_Forall]
Q:1533 [binder, in MetaCoq.Template.utils.All_Forall]
Q:1541 [binder, in MetaCoq.Template.utils.All_Forall]
Q:155 [binder, in MetaCoq.PCUIC.PCUICAlpha]
q:155 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Q:1563 [binder, in MetaCoq.Template.utils.All_Forall]
Q:1578 [binder, in MetaCoq.Template.utils.All_Forall]
Q:16 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
Q:16 [binder, in MetaCoq.Template.TypingWf]
Q:165 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Q:165 [binder, in MetaCoq.Template.monad_utils]
q:1681 [binder, in MetaCoq.Translations.MiniHoTT]
q:1682 [binder, in MetaCoq.Translations.MiniHoTT]
q:1689 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1690 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1705 [binder, in MetaCoq.Template.utils.All_Forall]
Q:171 [binder, in MetaCoq.Template.utils.All_Forall]
q:1712 [binder, in MetaCoq.Translations.MiniHoTT]
q:1719 [binder, in MetaCoq.Translations.MiniHoTT]
q:1720 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1725 [binder, in MetaCoq.Translations.MiniHoTT]
q:1727 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1733 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1734 [binder, in MetaCoq.Translations.MiniHoTT]
q:1742 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1743 [binder, in MetaCoq.Translations.MiniHoTT]
q:175 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:1751 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1752 [binder, in MetaCoq.Translations.MiniHoTT]
Q:1753 [binder, in MetaCoq.Template.utils.All_Forall]
q:176 [binder, in MetaCoq.Translations.times_bool_fun]
q:1760 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1762 [binder, in MetaCoq.Translations.MiniHoTT]
q:1770 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1771 [binder, in MetaCoq.Translations.MiniHoTT]
q:1779 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1780 [binder, in MetaCoq.Translations.MiniHoTT]
q:1786 [binder, in MetaCoq.Translations.MiniHoTT]
q:1788 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1789 [binder, in MetaCoq.Translations.MiniHoTT]
Q:1790 [binder, in MetaCoq.Template.utils.All_Forall]
q:1791 [binder, in MetaCoq.Translations.MiniHoTT]
q:1794 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1797 [binder, in MetaCoq.Template.utils.All_Forall]
q:1797 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1799 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:18 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:180 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:1822 [binder, in MetaCoq.Template.utils.All_Forall]
Q:1827 [binder, in MetaCoq.Template.utils.All_Forall]
q:1830 [binder, in MetaCoq.Translations.MiniHoTT]
q:1831 [binder, in MetaCoq.Translations.MiniHoTT]
q:1832 [binder, in MetaCoq.Translations.MiniHoTT]
q:1833 [binder, in MetaCoq.Translations.MiniHoTT]
q:1834 [binder, in MetaCoq.Translations.MiniHoTT]
q:1835 [binder, in MetaCoq.Translations.MiniHoTT]
q:1836 [binder, in MetaCoq.Translations.MiniHoTT]
q:1837 [binder, in MetaCoq.Translations.MiniHoTT]
q:1838 [binder, in MetaCoq.Translations.MiniHoTT]
q:1838 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1839 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:184 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:1840 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1841 [binder, in MetaCoq.Template.utils.All_Forall]
q:1841 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1842 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1843 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1844 [binder, in MetaCoq.Translations.MiniHoTT]
q:1844 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1845 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1846 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1851 [binder, in MetaCoq.Translations.MiniHoTT]
q:1852 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1859 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:186 [binder, in MetaCoq.Template.EnvironmentTyping]
Q:1860 [binder, in MetaCoq.Template.utils.All_Forall]
q:1861 [binder, in MetaCoq.Translations.MiniHoTT]
Q:1867 [binder, in MetaCoq.Template.utils.All_Forall]
q:1868 [binder, in MetaCoq.Translations.MiniHoTT]
q:1869 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1875 [binder, in MetaCoq.Translations.MiniHoTT]
q:1876 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:188 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:1882 [binder, in MetaCoq.Translations.MiniHoTT]
q:1883 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1889 [binder, in MetaCoq.Template.utils.All_Forall]
q:1889 [binder, in MetaCoq.Translations.MiniHoTT]
q:1890 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1896 [binder, in MetaCoq.Translations.MiniHoTT]
q:1897 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1904 [binder, in MetaCoq.Translations.MiniHoTT]
q:1904 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1906 [binder, in MetaCoq.Template.utils.All_Forall]
q:1911 [binder, in MetaCoq.Template.utils.All_Forall]
q:1912 [binder, in MetaCoq.Translations.MiniHoTT]
q:1912 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1919 [binder, in MetaCoq.Translations.MiniHoTT]
q:1920 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1921 [binder, in MetaCoq.Template.utils.All_Forall]
Q:1926 [binder, in MetaCoq.Template.utils.All_Forall]
q:1926 [binder, in MetaCoq.Translations.MiniHoTT]
q:1927 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:1931 [binder, in MetaCoq.Template.utils.All_Forall]
q:1933 [binder, in MetaCoq.Translations.MiniHoTT]
q:1934 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1940 [binder, in MetaCoq.Translations.MiniHoTT]
q:1941 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1947 [binder, in MetaCoq.Translations.MiniHoTT]
q:1948 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1954 [binder, in MetaCoq.Translations.MiniHoTT]
q:1955 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:196 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
q:196 [binder, in MetaCoq.Examples.tauto]
q:1961 [binder, in MetaCoq.Translations.MiniHoTT]
q:1962 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1968 [binder, in MetaCoq.Translations.MiniHoTT]
q:1969 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:197 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:197 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
q:1975 [binder, in MetaCoq.Translations.MiniHoTT]
q:1976 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1982 [binder, in MetaCoq.Translations.MiniHoTT]
q:1983 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1989 [binder, in MetaCoq.Translations.MiniHoTT]
q:199 [binder, in MetaCoq.Translations.MiniHoTT]
q:1990 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:1996 [binder, in MetaCoq.Translations.MiniHoTT]
q:1997 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2 [binder, in MetaCoq.Template.utils.MCRelations]
Q:2 [binder, in MetaCoq.Template.utils.ByteCompareSpec]
Q:2 [binder, in MetaCoq.Template.utils.MCArith]
q:2003 [binder, in MetaCoq.Translations.MiniHoTT]
q:2004 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:201 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Q:201 [binder, in MetaCoq.Template.monad_utils]
q:2010 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2011 [binder, in MetaCoq.Template.utils.All_Forall]
q:2011 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2017 [binder, in MetaCoq.Translations.MiniHoTT]
q:2018 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2024 [binder, in MetaCoq.Translations.MiniHoTT]
q:2025 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2031 [binder, in MetaCoq.Translations.MiniHoTT]
q:2032 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2037 [binder, in MetaCoq.Translations.MiniHoTT]
q:2039 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:204 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:204 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
q:2042 [binder, in MetaCoq.Translations.MiniHoTT]
q:2045 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2047 [binder, in MetaCoq.Translations.MiniHoTT]
q:2050 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2052 [binder, in MetaCoq.Translations.MiniHoTT]
q:2055 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2057 [binder, in MetaCoq.Translations.MiniHoTT]
q:2060 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2062 [binder, in MetaCoq.Translations.MiniHoTT]
q:2065 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2067 [binder, in MetaCoq.Translations.MiniHoTT]
q:207 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:207 [binder, in MetaCoq.Translations.MiniHoTT]
q:207 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2070 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2072 [binder, in MetaCoq.Translations.MiniHoTT]
q:2075 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:208 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:208 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:2080 [binder, in MetaCoq.Translations.MiniHoTT]
q:2080 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2088 [binder, in MetaCoq.Translations.MiniHoTT]
q:2088 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2096 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:21 [binder, in MetaCoq.Template.utils.MCUtils]
Q:21 [binder, in MetaCoq.PCUIC.PCUICConfluence]
q:210 [binder, in MetaCoq.Template.utils.All_Forall]
q:2110 [binder, in MetaCoq.Translations.MiniHoTT]
q:2118 [binder, in MetaCoq.Translations.MiniHoTT]
q:2118 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2126 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:213 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:215 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:215 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2167 [binder, in MetaCoq.Translations.MiniHoTT]
q:2168 [binder, in MetaCoq.Translations.MiniHoTT]
q:2175 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2176 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:218 [binder, in MetaCoq.Template.EnvironmentTyping]
q:2181 [binder, in MetaCoq.Translations.MiniHoTT]
q:2182 [binder, in MetaCoq.Translations.MiniHoTT]
q:2189 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:219 [binder, in MetaCoq.Template.TypingWf]
q:2190 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2195 [binder, in MetaCoq.Translations.MiniHoTT]
q:2196 [binder, in MetaCoq.Translations.MiniHoTT]
q:22 [binder, in MetaCoq.Template.utils.MCCompare]
Q:220 [binder, in MetaCoq.Template.EnvironmentTyping]
q:220 [binder, in MetaCoq.Template.utils.wGraph]
q:2203 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2204 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2209 [binder, in MetaCoq.Translations.MiniHoTT]
q:221 [binder, in MetaCoq.Template.utils.wGraph]
q:2210 [binder, in MetaCoq.Translations.MiniHoTT]
q:2217 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2218 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:222 [binder, in MetaCoq.Translations.MiniHoTT]
q:2222 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2227 [binder, in MetaCoq.Template.utils.All_Forall]
q:2230 [binder, in MetaCoq.Translations.MiniHoTT]
q:2230 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2237 [binder, in MetaCoq.Translations.MiniHoTT]
q:2238 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2241 [binder, in MetaCoq.Template.utils.All_Forall]
q:2245 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2247 [binder, in MetaCoq.Translations.MiniHoTT]
q:2255 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2257 [binder, in MetaCoq.Translations.MiniHoTT]
q:2265 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2267 [binder, in MetaCoq.Translations.MiniHoTT]
q:227 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
q:2275 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2277 [binder, in MetaCoq.Translations.MiniHoTT]
q:228 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2284 [binder, in MetaCoq.Template.utils.All_Forall]
q:2285 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2287 [binder, in MetaCoq.Translations.MiniHoTT]
q:2294 [binder, in MetaCoq.Translations.MiniHoTT]
q:2295 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2298 [binder, in MetaCoq.Template.utils.All_Forall]
q:230 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2302 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2307 [binder, in MetaCoq.Template.utils.All_Forall]
Q:231 [binder, in MetaCoq.Template.EnvironmentTyping]
Q:2316 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2337 [binder, in MetaCoq.Template.utils.All_Forall]
q:234 [binder, in MetaCoq.Translations.MiniHoTT]
q:2351 [binder, in MetaCoq.Translations.MiniHoTT]
q:2359 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:236 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2362 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2397 [binder, in MetaCoq.Template.utils.All_Forall]
q:240 [binder, in MetaCoq.Translations.MiniHoTT]
q:2400 [binder, in MetaCoq.Translations.MiniHoTT]
q:2408 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:242 [binder, in MetaCoq.Template.EnvironmentTyping]
q:242 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2421 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2428 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2437 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2446 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2455 [binder, in MetaCoq.Template.utils.All_Forall]
q:246 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2464 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2468 [binder, in MetaCoq.Translations.MiniHoTT]
q:247 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:2476 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2479 [binder, in MetaCoq.Translations.MiniHoTT]
Q:248 [binder, in MetaCoq.Template.utils.All_Forall]
q:248 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:248 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2487 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2491 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2495 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2499 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2507 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2507 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2515 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:252 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2520 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2525 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2528 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2532 [binder, in MetaCoq.Translations.MiniHoTT]
q:254 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2540 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2540 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2541 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2548 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2552 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2554 [binder, in MetaCoq.Translations.MiniHoTT]
Q:256 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2561 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2562 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2568 [binder, in MetaCoq.Template.utils.All_Forall]
Q:2569 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:258 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2582 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2590 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2594 [binder, in MetaCoq.Template.utils.All_Forall]
Q:26 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:260 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:261 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
q:261 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:263 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:263 [binder, in MetaCoq.Template.TypingWf]
Q:2636 [binder, in MetaCoq.Translations.MiniHoTT]
Q:264 [binder, in MetaCoq.Template.utils.All_Forall]
q:264 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:264 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2644 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:265 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:266 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2669 [binder, in MetaCoq.Translations.MiniHoTT]
q:2677 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2678 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2686 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2697 [binder, in MetaCoq.Translations.MiniHoTT]
q:2705 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:272 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:272 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2733 [binder, in MetaCoq.Translations.MiniHoTT]
Q:274 [binder, in MetaCoq.Template.utils.All_Forall]
q:274 [binder, in MetaCoq.Translations.MiniHoTT]
q:2740 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2741 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2746 [binder, in MetaCoq.Translations.MiniHoTT]
q:2748 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2752 [binder, in MetaCoq.Translations.MiniHoTT]
q:2754 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2760 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2764 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2765 [binder, in MetaCoq.Translations.MiniHoTT]
q:2772 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2773 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:279 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:280 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:281 [binder, in MetaCoq.Translations.MiniHoTT]
q:2815 [binder, in MetaCoq.Translations.MiniHoTT]
q:282 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2823 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2825 [binder, in MetaCoq.Translations.MiniHoTT]
q:2833 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2836 [binder, in MetaCoq.Translations.MiniHoTT]
Q:284 [binder, in MetaCoq.Template.utils.All_Forall]
q:2844 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2863 [binder, in MetaCoq.Translations.MiniHoTT]
q:2871 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2872 [binder, in MetaCoq.Translations.MiniHoTT]
q:288 [binder, in MetaCoq.Translations.MiniHoTT]
q:2880 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:289 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:29 [binder, in MetaCoq.PCUIC.PCUICConfluence]
q:291 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:2915 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2923 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2923 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2930 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2931 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2935 [binder, in MetaCoq.Translations.MiniHoTT]
q:2938 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:294 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:294 [binder, in MetaCoq.Template.utils.wGraph]
Q:2943 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:295 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:295 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2950 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2958 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:296 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:296 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2960 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2966 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2968 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:2974 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2987 [binder, in MetaCoq.Translations.MiniHoTT]
q:2988 [binder, in MetaCoq.Translations.MiniHoTT]
Q:2992 [binder, in MetaCoq.Translations.MiniHoTT]
q:2995 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:2996 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:3 [binder, in MetaCoq.Template.utils.MCPred]
q:30 [binder, in MetaCoq.Template.TemplateMonad.Core]
Q:30 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
Q:3000 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:302 [binder, in MetaCoq.Translations.MiniHoTT]
q:303 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:305 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:309 [binder, in MetaCoq.Translations.MiniHoTT]
q:310 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:311 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:312 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:313 [binder, in MetaCoq.PCUIC.PCUICSR]
Q:316 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:316 [binder, in MetaCoq.Translations.MiniHoTT]
q:317 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:319 [binder, in MetaCoq.Template.EnvironmentTyping]
q:321 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:323 [binder, in MetaCoq.Translations.MiniHoTT]
q:324 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:326 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:327 [binder, in MetaCoq.Template.utils.All_Forall]
q:329 [binder, in MetaCoq.Translations.MiniHoTT]
q:33 [binder, in MetaCoq.Examples.demo]
q:331 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:332 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:333 [binder, in MetaCoq.Template.utils.All_Forall]
q:334 [binder, in MetaCoq.Translations.MiniHoTT]
q:335 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:337 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:339 [binder, in MetaCoq.Translations.MiniHoTT]
Q:34 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:34 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:340 [binder, in MetaCoq.Template.Environment]
Q:341 [binder, in MetaCoq.Template.utils.All_Forall]
Q:341 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
q:342 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:343 [binder, in MetaCoq.Template.utils.wGraph]
q:344 [binder, in MetaCoq.Translations.MiniHoTT]
q:345 [binder, in MetaCoq.Template.utils.wGraph]
Q:346 [binder, in MetaCoq.Template.Environment]
q:346 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Q:347 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
q:347 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:349 [binder, in MetaCoq.Translations.MiniHoTT]
q:352 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:353 [binder, in MetaCoq.Template.utils.wGraph]
q:354 [binder, in MetaCoq.Translations.MiniHoTT]
Q:356 [binder, in MetaCoq.Template.utils.All_Forall]
q:357 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:359 [binder, in MetaCoq.Translations.MiniHoTT]
Q:36 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:361 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
q:362 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:364 [binder, in MetaCoq.Translations.MiniHoTT]
q:367 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:372 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:38 [binder, in MetaCoq.Examples.demo]
Q:383 [binder, in MetaCoq.Template.BasicAst]
Q:4 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
Q:40 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:400 [binder, in MetaCoq.Translations.MiniHoTT]
q:403 [binder, in MetaCoq.Template.utils.wGraph]
q:408 [binder, in MetaCoq.Translations.MiniHoTT]
q:408 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:41 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:413 [binder, in MetaCoq.Template.utils.All_Forall]
Q:416 [binder, in MetaCoq.PCUIC.PCUICNormal]
q:416 [binder, in MetaCoq.Translations.MiniHoTT]
q:416 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:421 [binder, in MetaCoq.Template.utils.wGraph]
Q:423 [binder, in MetaCoq.Template.utils.All_Forall]
q:424 [binder, in MetaCoq.Translations.MiniHoTT]
q:424 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:432 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:441 [binder, in MetaCoq.Translations.MiniHoTT]
Q:448 [binder, in MetaCoq.Template.utils.All_Forall]
q:449 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:45 [binder, in MetaCoq.Template.TypingWf]
q:451 [binder, in MetaCoq.Translations.MiniHoTT]
Q:453 [binder, in MetaCoq.Template.utils.All_Forall]
q:459 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:46 [binder, in MetaCoq.Translations.translation_utils]
q:460 [binder, in MetaCoq.Translations.MiniHoTT]
q:468 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:47 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:47 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
Q:47 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Q:481 [binder, in MetaCoq.Template.utils.All_Forall]
Q:484 [binder, in MetaCoq.Examples.tauto]
Q:486 [binder, in MetaCoq.Examples.tauto]
Q:488 [binder, in MetaCoq.Template.utils.All_Forall]
Q:488 [binder, in MetaCoq.Examples.tauto]
q:5 [binder, in MetaCoq.Template.utils.MCCompare]
q:508 [binder, in MetaCoq.PCUIC.PCUICAst]
q:509 [binder, in MetaCoq.Translations.MiniHoTT]
q:516 [binder, in MetaCoq.Translations.MiniHoTT]
q:517 [binder, in MetaCoq.PCUIC.PCUICAst]
q:517 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:523 [binder, in MetaCoq.Translations.MiniHoTT]
q:524 [binder, in MetaCoq.PCUIC.PCUICAst]
q:524 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:53 [binder, in MetaCoq.Template.utils.All_Forall]
q:531 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:532 [binder, in MetaCoq.Translations.MiniHoTT]
q:540 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:545 [binder, in MetaCoq.Translations.MiniHoTT]
Q:553 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:553 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:556 [binder, in MetaCoq.Translations.MiniHoTT]
Q:56 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:562 [binder, in MetaCoq.Template.utils.All_Forall]
q:564 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:565 [binder, in MetaCoq.Translations.MiniHoTT]
Q:568 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:572 [binder, in MetaCoq.PCUIC.PCUICAst]
q:573 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:576 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:576 [binder, in MetaCoq.Translations.MiniHoTT]
Q:579 [binder, in MetaCoq.Template.utils.All_Forall]
q:584 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:587 [binder, in MetaCoq.Translations.MiniHoTT]
q:590 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:595 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:596 [binder, in MetaCoq.Translations.MiniHoTT]
Q:6 [binder, in MetaCoq.Template.TypingWf]
q:60 [binder, in MetaCoq.Template.utils.All_Forall]
q:604 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:605 [binder, in MetaCoq.Translations.MiniHoTT]
q:61 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:61 [binder, in MetaCoq.Template.utils.wGraph]
Q:61 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
q:613 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:614 [binder, in MetaCoq.Translations.MiniHoTT]
Q:618 [binder, in MetaCoq.Template.utils.All_Forall]
q:619 [binder, in MetaCoq.Template.utils.wGraph]
q:620 [binder, in MetaCoq.Translations.MiniHoTT]
q:622 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:625 [binder, in MetaCoq.Template.utils.wGraph]
q:625 [binder, in MetaCoq.Translations.MiniHoTT]
q:628 [binder, in MetaCoq.Template.utils.wGraph]
q:628 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:63 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:63 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
Q:63 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
q:632 [binder, in MetaCoq.Template.utils.wGraph]
q:633 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:636 [binder, in MetaCoq.Template.utils.wGraph]
q:65 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:65 [binder, in MetaCoq.Template.TypingWf]
Q:660 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:665 [binder, in MetaCoq.Template.utils.wGraph]
q:671 [binder, in MetaCoq.Template.utils.wGraph]
q:674 [binder, in MetaCoq.Template.utils.wGraph]
Q:676 [binder, in MetaCoq.Template.EnvironmentTyping]
Q:678 [binder, in MetaCoq.Template.utils.All_Forall]
Q:68 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
q:680 [binder, in MetaCoq.Template.utils.wGraph]
q:684 [binder, in MetaCoq.Template.utils.wGraph]
Q:685 [binder, in MetaCoq.Template.EnvironmentTyping]
q:69 [binder, in MetaCoq.Examples.demo]
Q:696 [binder, in MetaCoq.Template.EnvironmentTyping]
Q:699 [binder, in MetaCoq.Template.utils.All_Forall]
q:7 [binder, in MetaCoq.Template.utils.MCCompare]
Q:7 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:71 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:719 [binder, in MetaCoq.Translations.MiniHoTT]
Q:72 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Q:72 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
q:727 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:734 [binder, in MetaCoq.Template.EnvironmentTyping]
Q:739 [binder, in MetaCoq.Template.utils.All_Forall]
q:742 [binder, in MetaCoq.Translations.MiniHoTT]
Q:749 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Q:75 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:750 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:78 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:789 [binder, in MetaCoq.Template.utils.All_Forall]
Q:80 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
q:80 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Q:800 [binder, in MetaCoq.PCUIC.PCUICReduction]
Q:805 [binder, in MetaCoq.PCUIC.PCUICReduction]
q:809 [binder, in MetaCoq.Translations.MiniHoTT]
q:817 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:820 [binder, in MetaCoq.Translations.MiniHoTT]
q:824 [binder, in MetaCoq.Template.utils.wGraph]
q:828 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:83 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:831 [binder, in MetaCoq.Template.utils.wGraph]
q:831 [binder, in MetaCoq.Translations.MiniHoTT]
q:839 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:84 [binder, in MetaCoq.Template.utils.All_Forall]
Q:84 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
q:843 [binder, in MetaCoq.Translations.MiniHoTT]
Q:846 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:849 [binder, in MetaCoq.Translations.MiniHoTT]
q:851 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:854 [binder, in MetaCoq.Translations.MiniHoTT]
Q:857 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:857 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:858 [binder, in MetaCoq.Translations.MiniHoTT]
q:86 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:861 [binder, in MetaCoq.Template.utils.All_Forall]
Q:862 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:863 [binder, in MetaCoq.Template.utils.wGraph]
q:866 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:87 [binder, in MetaCoq.Translations.MiniHoTT]
Q:872 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
Q:872 [binder, in MetaCoq.Translations.MiniHoTT]
q:876 [binder, in MetaCoq.Translations.MiniHoTT]
Q:880 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:882 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Q:884 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:884 [binder, in MetaCoq.Translations.MiniHoTT]
q:884 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:89 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Q:891 [binder, in MetaCoq.Translations.MiniHoTT]
q:892 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:896 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
Q:899 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:9 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
q:9 [binder, in MetaCoq.Template.utils.MCPred]
Q:90 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
Q:90 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:902 [binder, in MetaCoq.Template.utils.All_Forall]
Q:912 [binder, in MetaCoq.Template.utils.All_Forall]
Q:915 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
Q:92 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
Q:927 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:934 [binder, in MetaCoq.Translations.MiniHoTT]
Q:941 [binder, in MetaCoq.PCUIC.PCUICConversion]
q:942 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:948 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
Q:95 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
q:95 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:950 [binder, in MetaCoq.Translations.MiniHoTT]
q:958 [binder, in MetaCoq.Translations.MiniHoTT_paths]
q:96 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:96 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:962 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:970 [binder, in MetaCoq.Translations.MiniHoTT]
Q:973 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
q:978 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Q:98 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Q:980 [binder, in MetaCoq.Template.utils.All_Forall]
Q:99 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:99 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
q:99 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]

---

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(75519 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(245 entries)

Binder Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(61331 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(144 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(89 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(236 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6913 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1141 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(34 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(269 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(443 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(296 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(604 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(248 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3386 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(140 entries)

Generated by coqdoc and improved with CoqdocJS