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)

---

D

d [definition, in MetaCoq.Examples.demo]
dapp_r [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dapp_l [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
da:46 [binder, in MetaCoq.Erasure.EInduction]
da:48 [binder, in MetaCoq.Erasure.EInduction]
dbody [projection, in MetaCoq.Template.BasicAst]
dbody [projection, in MetaCoq.Erasure.EAst]
dbody':1060 [binder, in MetaCoq.Erasure.ErasureFunction]
dbody':1061 [binder, in MetaCoq.Erasure.ErasureFunction]
dbody':1075 [binder, in MetaCoq.Erasure.ErasureFunction]
dbody':447 [binder, in MetaCoq.Erasure.ErasureFunction]
dbody':448 [binder, in MetaCoq.Erasure.ErasureFunction]
dbody':457 [binder, in MetaCoq.Erasure.ErasureFunction]
dbody:339 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dcase_c [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dcase_preturn [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
debug_term [definition, in MetaCoq.Translations.param_binary]
debug_term [definition, in MetaCoq.Translations.standard_model]
debug_term [definition, in MetaCoq.Translations.param_original]
debug:13 [binder, in MetaCoq.Translations.param_original]
debug:27 [binder, in MetaCoq.Translations.param_binary]
decision [abbreviation, in MetaCoq.PCUIC.PCUICNormal]
DeclarationTyping [module, in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.Forall_decls_typing [definition, in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.isType [definition, in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.on_wf_global_env_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.refine_type [lemma, in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.type_local_decl [definition, in MetaCoq.Template.EnvironmentTyping]
DeclarationTyping.wf_local_rel [definition, in MetaCoq.Template.EnvironmentTyping]
declared [definition, in MetaCoq.Template.common.uGraph]
DeclaredInv [section, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_constructor_ind_decl [lemma, in MetaCoq.PCUIC.PCUICProgress]
declared_cstr_levels [definition, in MetaCoq.Template.Universes]
declared_projection_projs_nonempty [lemma, in MetaCoq.PCUIC.PCUICElimination]
declared_cstr_levels_sub [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
declared_constructor_typing_spine_not_arity [lemma, in MetaCoq.Erasure.EArities]
declared_constructor_type_not_arity [lemma, in MetaCoq.Erasure.EArities]
declared_projection_closed_type [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_indices [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_args [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_type [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_gen_type [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed_arities [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_constructors [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_params_inst [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_params [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_type [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_constant_closed_body [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_constant_closed_type [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_decl_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_pars_indices [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_projection_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed_ind [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_decl_closed_ind [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_projection_closed_ind [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_lookup [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
declared_inductive_inj [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
declared_projection_unique [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
declared_constructor_unique [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
declared_constructor_arity [lemma, in MetaCoq.Erasure.ErasureCorrectness]
declared_projection_type_and_eq [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_projection_type [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_projections_subslet [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_projections [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_projections_subslet_ind [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_constructor_wf_pars_args [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_inductive_valid_type [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_inductive_type [lemma, in MetaCoq.PCUIC.PCUICInductives]
declared_inductive_unique_sig [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
declared_inductive_unique [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
declared_constructor_valid_ty [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
declared_inductive_closed_indices [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
declared_kn [definition, in MetaCoq.Erasure.ErasureFunction]
declared_minductive_ind_npars [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_projection_constructor [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_constructor_inductive [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_inductive_minductive [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_projection_inj [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_constructor_inj [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_inductive_inj [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_constant_inj [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
declared_projection_lookup [lemma, in MetaCoq.Erasure.EGlobalEnv]
declared_constructor_lookup [lemma, in MetaCoq.Erasure.EGlobalEnv]
declared_inductive_lookup [lemma, in MetaCoq.Erasure.EGlobalEnv]
declared_minductive_lookup [lemma, in MetaCoq.Erasure.EGlobalEnv]
declared_constant_lookup [lemma, in MetaCoq.Erasure.EGlobalEnv]
declared_projection [definition, in MetaCoq.Erasure.EGlobalEnv]
declared_constructor [definition, in MetaCoq.Erasure.EGlobalEnv]
declared_inductive [definition, in MetaCoq.Erasure.EGlobalEnv]
declared_minductive [definition, in MetaCoq.Erasure.EGlobalEnv]
declared_constant [definition, in MetaCoq.Erasure.EGlobalEnv]
declared_projection_indices [lemma, in MetaCoq.PCUIC.PCUICSR]
declared_projection_declared_constructor [lemma, in MetaCoq.PCUIC.PCUICSR]
declared_constructor_expanded [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
declared_minductive_expanded [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
declared_inductive_wf_global_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
declared_inductive_wf_ext_wk [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
declared_minductive_closed_inds [lemma, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
declared_constructor_wf_case_branch_context [lemma, in MetaCoq.Template.TypingWf]
declared_inductive_wf_case_predicate_context [lemma, in MetaCoq.Template.TypingWf]
declared_minductive_wf [lemma, in MetaCoq.Template.TypingWf]
declared_constant_wf [lemma, in MetaCoq.Template.TypingWf]
declared_projection_wf [lemma, in MetaCoq.Template.TypingWf]
declared_constructor_wf [lemma, in MetaCoq.Template.TypingWf]
declared_inductive_wf_params [lemma, in MetaCoq.Template.TypingWf]
declared_inductive_wf_ctors [lemma, in MetaCoq.Template.TypingWf]
declared_inductive_wf_indices [lemma, in MetaCoq.Template.TypingWf]
declared_inductive_wf [lemma, in MetaCoq.Template.TypingWf]
declared_projection_inv [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constructor_inv_decls [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_inductive_inv_decls [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_minductive_inv_decls [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constructor_inv [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_inductive_inv [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_minductive_inv [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constant_inv [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constructor_assumption_context [lemma, in MetaCoq.Erasure.Prelim]
declared_global_uctx_global_ext_uctx [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
declc:59 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
declc:68 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
decli:17 [binder, in MetaCoq.Erasure.ErasureFunction]
decli:30 [binder, in MetaCoq.PCUIC.PCUICInductives]
decli:42 [binder, in MetaCoq.PCUIC.PCUICInductives]
declm:408 [binder, in MetaCoq.PCUIC.PCUICInductives]
declm:422 [binder, in MetaCoq.PCUIC.PCUICInductives]
declm:54 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
declm:732 [binder, in MetaCoq.PCUIC.PCUICSR]
decls_prefix_wf [lemma, in MetaCoq.Erasure.ErasureFunction]
decls_prefix [definition, in MetaCoq.Erasure.ErasureFunction]
decls':1419 [binder, in MetaCoq.Erasure.ErasureFunction]
decls':145 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
decls:1020 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1025 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
decls:1033 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1040 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1138 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1154 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1177 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:120 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
decls:1208 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1220 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1233 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1248 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1259 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1269 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1277 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1283 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1290 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1304 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1324 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1341 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:137 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
decls:1381 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1403 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1411 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1418 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1420 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1423 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1430 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:144 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
decls:1491 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1499 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1505 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1513 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1519 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1532 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:1537 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:180 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
decls:265 [binder, in MetaCoq.Erasure.EEtaExpanded]
decls:432 [binder, in MetaCoq.Template.Checker]
decls:506 [binder, in MetaCoq.Template.EtaExpand]
decls:512 [binder, in MetaCoq.Template.EtaExpand]
decls:518 [binder, in MetaCoq.Template.EtaExpand]
decls:67 [binder, in MetaCoq.Template.AstUtils]
decls:781 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:821 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:934 [binder, in MetaCoq.Erasure.ErasureFunction]
decls:952 [binder, in MetaCoq.Erasure.ErasureFunction]
decl_type [projection, in MetaCoq.Template.BasicAst]
decl_body [projection, in MetaCoq.Template.BasicAst]
decl_name [projection, in MetaCoq.Template.BasicAst]
decl_ws_cumul_pb [abbreviation, in MetaCoq.PCUIC.PCUICInductiveInversion]
decl_hole_body [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl_hole_type [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl_body [projection, in MetaCoq.Erasure.EAst]
decl_name [projection, in MetaCoq.Erasure.EAst]
decl_size [definition, in MetaCoq.Examples.tauto]
decl_type_eq_context_upto_names [lemma, in MetaCoq.PCUIC.PCUICConfluence]
decl_body_eq_context_upto_names [lemma, in MetaCoq.PCUIC.PCUICConfluence]
decl_size [definition, in MetaCoq.PCUIC.utils.PCUICSize]
decl_size_map_decl_hom [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
decl_depth_gen [definition, in MetaCoq.PCUIC.Syntax.PCUICDepth]
decl':10 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
decl':132 [binder, in MetaCoq.Erasure.EDeps]
decl':1486 [binder, in MetaCoq.Erasure.ErasureFunction]
decl':170 [binder, in MetaCoq.Erasure.EDeps]
decl':172 [binder, in MetaCoq.Erasure.EDeps]
decl':19 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl':205 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
decl':43 [binder, in MetaCoq.SafeChecker.PCUICErrors]
decl':47 [binder, in MetaCoq.SafeChecker.PCUICErrors]
decl':51 [binder, in MetaCoq.SafeChecker.PCUICErrors]
decl':60 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
decl':760 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl':783 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
decl':8 [binder, in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
decl':829 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl':932 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl':940 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl1:206 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
decl1:3 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
decl2:207 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
decl2:4 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
decl:10 [binder, in MetaCoq.Template.EnvironmentTyping]
decl:10 [binder, in MetaCoq.Erasure.EGlobalEnv]
decl:100 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:101 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:1017 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:102 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:1029 [binder, in MetaCoq.Template.Typing]
decl:104 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:104 [binder, in MetaCoq.Erasure.EWcbvEval]
decl:106 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:107 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:1089 [binder, in MetaCoq.Template.Typing]
decl:109 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:1097 [binder, in MetaCoq.Template.Typing]
decl:111 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:111 [binder, in MetaCoq.Erasure.ErasureProperties]
decl:113 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
decl:113 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:113 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
decl:114 [binder, in MetaCoq.Translations.translation_utils]
decl:114 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
decl:114 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
decl:115 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:115 [binder, in MetaCoq.Translations.times_bool_fun]
decl:116 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
decl:117 [binder, in MetaCoq.Translations.times_bool_fun]
decl:117 [binder, in MetaCoq.Erasure.EWellformed]
decl:120 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
decl:122 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:122 [binder, in MetaCoq.Erasure.EGlobalEnv]
decl:125 [binder, in MetaCoq.Template.Typing]
decl:1264 [binder, in MetaCoq.Template.Typing]
decl:127 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
decl:127 [binder, in MetaCoq.Template.Checker]
decl:1275 [binder, in MetaCoq.Template.Typing]
decl:1278 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1281 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1284 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1287 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1290 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1293 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:13 [binder, in MetaCoq.Erasure.EPretty]
decl:13 [binder, in MetaCoq.Erasure.EExtends]
decl:1305 [binder, in MetaCoq.Template.Typing]
decl:131 [binder, in MetaCoq.Erasure.EDeps]
decl:132 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
decl:1328 [binder, in MetaCoq.Template.Typing]
decl:133 [binder, in MetaCoq.Translations.times_bool_fun]
decl:134 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:134 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:135 [binder, in MetaCoq.Translations.times_bool_fun]
decl:135 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:137 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:139 [binder, in MetaCoq.Translations.translation_utils]
decl:14 [binder, in MetaCoq.Erasure.EEnvMap]
decl:14 [binder, in MetaCoq.Erasure.EGlobalEnv]
decl:140 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
decl:1426 [binder, in MetaCoq.Erasure.ErasureFunction]
decl:144 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:145 [binder, in MetaCoq.PCUIC.PCUICInductives]
decl:146 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:147 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:147 [binder, in MetaCoq.Erasure.EWellformed]
decl:148 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:1485 [binder, in MetaCoq.Erasure.ErasureFunction]
decl:15 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:150 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:151 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:153 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:153 [binder, in MetaCoq.Template.Environment]
decl:154 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:155 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:155 [binder, in MetaCoq.Template.Environment]
decl:156 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:157 [binder, in MetaCoq.Template.Environment]
decl:158 [binder, in MetaCoq.Template.WcbvEval]
decl:158 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:159 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:16 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl:160 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:162 [binder, in MetaCoq.PCUIC.PCUICInversion]
decl:164 [binder, in MetaCoq.Template.Environment]
decl:165 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:167 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
decl:167 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
decl:169 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:17 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
decl:170 [binder, in MetaCoq.PCUIC.PCUICInversion]
decl:171 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:179 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
decl:183 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decl:185 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decl:19 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:19 [binder, in MetaCoq.Erasure.EExtends]
decl:194 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:200 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
decl:202 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:203 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
decl:205 [binder, in MetaCoq.PCUIC.PCUICReduction]
decl:210 [binder, in MetaCoq.SafeChecker.PCUICErrors]
decl:212 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
decl:229 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:231 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:233 [binder, in MetaCoq.Template.BasicAst]
decl:235 [binder, in MetaCoq.Template.BasicAst]
decl:235 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
decl:235 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
decl:237 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
decl:24 [binder, in MetaCoq.PCUIC.PCUICValidity]
decl:24 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl:242 [binder, in MetaCoq.Erasure.Extract]
decl:243 [binder, in MetaCoq.Template.BasicAst]
decl:247 [binder, in MetaCoq.Template.TypingWf]
decl:26 [binder, in MetaCoq.PCUIC.PCUICInversion]
decl:261 [binder, in MetaCoq.Erasure.EEtaExpanded]
decl:267 [binder, in MetaCoq.Template.EtaExpand]
decl:267 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
decl:276 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
decl:284 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:296 [binder, in MetaCoq.Template.Typing]
decl:3 [binder, in MetaCoq.Template.EnvironmentTyping]
decl:30 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:30 [binder, in MetaCoq.PCUIC.PCUICValidity]
decl:302 [binder, in MetaCoq.PCUIC.PCUICInductives]
decl:308 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
decl:31 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl:316 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
decl:316 [binder, in MetaCoq.Template.WcbvEval]
decl:32 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:32 [binder, in MetaCoq.Template.Normal]
decl:32 [binder, in MetaCoq.Erasure.EGlobalEnv]
decl:32 [binder, in MetaCoq.Examples.add_constructor]
decl:320 [binder, in MetaCoq.PCUIC.PCUICInductives]
decl:323 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
decl:34 [binder, in MetaCoq.Template.EnvMap]
decl:342 [binder, in MetaCoq.Erasure.EWcbvEval]
decl:344 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:347 [binder, in MetaCoq.Erasure.EArities]
decl:349 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:349 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:349 [binder, in MetaCoq.Erasure.ERemoveParams]
decl:35 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:35 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decl:35 [binder, in MetaCoq.Erasure.EGlobalEnv]
decl:35 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
decl:351 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:352 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:352 [binder, in MetaCoq.PCUIC.PCUICInductives]
decl:355 [binder, in MetaCoq.Erasure.ERemoveParams]
decl:36 [binder, in MetaCoq.Template.EnvMap]
decl:364 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:368 [binder, in MetaCoq.PCUIC.PCUICNormal]
decl:37 [binder, in MetaCoq.Template.Pretty]
decl:380 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:385 [binder, in MetaCoq.PCUIC.PCUICSR]
decl:398 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
decl:4 [binder, in MetaCoq.Erasure.EExtends]
decl:40 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:404 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
decl:41 [binder, in MetaCoq.SafeChecker.PCUICErrors]
decl:41 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:415 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:417 [binder, in MetaCoq.PCUIC.PCUICSpine]
decl:42 [binder, in MetaCoq.Template.Pretty]
decl:42 [binder, in MetaCoq.PCUIC.PCUICReduction]
decl:420 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:421 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:421 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
decl:428 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:428 [binder, in MetaCoq.Template.EtaExpand]
decl:438 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:440 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:45 [binder, in MetaCoq.SafeChecker.PCUICErrors]
decl:454 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
decl:46 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
decl:464 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
decl:47 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:471 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:48 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:48 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:484 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:486 [binder, in MetaCoq.Template.EtaExpand]
decl:49 [binder, in MetaCoq.PCUIC.PCUICInductives]
decl:49 [binder, in MetaCoq.SafeChecker.PCUICErrors]
decl:495 [binder, in MetaCoq.Template.EtaExpand]
decl:496 [binder, in MetaCoq.Examples.tauto]
decl:5 [binder, in MetaCoq.Erasure.EInlineProjections]
decl:509 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:51 [binder, in MetaCoq.Template.EtaExpand]
decl:513 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:514 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
decl:526 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:53 [binder, in MetaCoq.PCUIC.PCUICNormal]
decl:539 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:54 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:543 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:548 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
decl:55 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
decl:57 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
decl:575 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
decl:58 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:58 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:58 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
decl:582 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
decl:583 [binder, in MetaCoq.Template.EnvironmentTyping]
decl:584 [binder, in MetaCoq.PCUIC.PCUICSpine]
decl:586 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:59 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
decl:594 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:6 [binder, in MetaCoq.Template.EnvironmentTyping]
decl:60 [binder, in MetaCoq.Template.Environment]
decl:60 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:606 [binder, in MetaCoq.Template.Typing]
decl:61 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
decl:614 [binder, in MetaCoq.PCUIC.PCUICConfluence]
decl:618 [binder, in MetaCoq.PCUIC.PCUICConfluence]
decl:62 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
decl:622 [binder, in MetaCoq.PCUIC.PCUICConfluence]
decl:626 [binder, in MetaCoq.PCUIC.PCUICConfluence]
decl:63 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:630 [binder, in MetaCoq.PCUIC.PCUICConfluence]
decl:634 [binder, in MetaCoq.Template.Typing]
decl:65 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:65 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
decl:65 [binder, in MetaCoq.Template.WcbvEval]
decl:65 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:658 [binder, in MetaCoq.Template.EnvironmentTyping]
decl:66 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decl:66 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:674 [binder, in MetaCoq.Template.Typing]
decl:68 [binder, in MetaCoq.Erasure.EPretty]
decl:680 [binder, in MetaCoq.Template.Typing]
decl:7 [binder, in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
decl:7 [binder, in MetaCoq.Erasure.EGlobalEnv]
decl:70 [binder, in MetaCoq.Template.AstUtils]
decl:70 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:71 [binder, in MetaCoq.Template.Normal]
decl:710 [binder, in MetaCoq.PCUIC.PCUICEquality]
decl:74 [binder, in MetaCoq.Template.EtaExpand]
decl:74 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
decl:75 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:759 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:766 [binder, in MetaCoq.Template.Universes]
decl:77 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
decl:77 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:78 [binder, in MetaCoq.PCUIC.PCUICProgress]
decl:782 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
decl:79 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:799 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:8 [binder, in MetaCoq.Erasure.EExtends]
decl:80 [binder, in MetaCoq.Erasure.EPretty]
decl:81 [binder, in MetaCoq.Translations.translation_utils]
decl:81 [binder, in MetaCoq.Translations.times_bool_fun]
decl:828 [binder, in MetaCoq.PCUIC.PCUICSR]
decl:828 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:83 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
decl:849 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:85 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:85 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:851 [binder, in MetaCoq.Erasure.ErasureFunction]
decl:854 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
decl:86 [binder, in MetaCoq.Translations.times_bool_fun]
decl:87 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:9 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
decl:909 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:91 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:917 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:92 [binder, in MetaCoq.PCUIC.PCUICInversion]
decl:92 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:93 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
decl:931 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:935 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:939 [binder, in MetaCoq.Erasure.ErasureFunction]
decl:939 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:94 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:956 [binder, in MetaCoq.PCUIC.PCUICTyping]
decl:97 [binder, in MetaCoq.Translations.translation_utils]
decl:970 [binder, in MetaCoq.Template.Typing]
decl:996 [binder, in MetaCoq.PCUIC.PCUICTyping]
decompose_type_of_constructor [lemma, in MetaCoq.Template.EtaExpand]
decompose_prod12 [lemma, in MetaCoq.Template.EtaExpand]
decompose_prod_lift [lemma, in MetaCoq.Template.EtaExpand]
decompose_app_app [lemma, in MetaCoq.Erasure.EInduction]
decompose_app_notApp [lemma, in MetaCoq.Erasure.EInduction]
decompose_app_rec_notApp [lemma, in MetaCoq.Erasure.EInduction]
decompose_app_inv [lemma, in MetaCoq.Erasure.EInduction]
decompose_app_rec_inv [lemma, in MetaCoq.Erasure.EInduction]
decompose_app_size [lemma, in MetaCoq.Erasure.EInduction]
decompose_app_rec_size [lemma, in MetaCoq.Erasure.EInduction]
decompose_app_rec_inv' [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_eq [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_eq_right [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_tFix [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_tFix [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_head [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_eq_mkApps [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_nonnil [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_inv [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_inv [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_notApp [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_notApp [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum_it_mkProd [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod_n_assum_it_mkProd [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod_n_assum [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum_ctx [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_prod [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_mkApps [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_mkApps [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
decompose_app_tApp_split [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
decompose_stack_stack_cat [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
decompose_stack_noStackApp [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
decompose_stack_closed [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
decompose_lam [definition, in MetaCoq.Erasure.EPretty]
decompose_prod_assum_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decompose_prod_assum_mkApps_nonnil [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decompose_prod_assum_spec [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
decompose_arity [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph [inductive, in MetaCoq.PCUIC.PCUICSubstitution]
decompose_prod_assum_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
decompose_prod_n_assum0 [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
decompose_app_subst [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
decompose_app_rec_subst [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
decompose_prod_assum_it_mkProd_or_LetIn' [lemma, in MetaCoq.PCUIC.PCUICInductives]
decompose_stack_twice [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at_length [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at_eq [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack_appstack [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack_not_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack_eq [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_stack [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
decompose_prod_assum_upto_names' [lemma, in MetaCoq.PCUIC.PCUICAlpha]
decompose_app_upto [lemma, in MetaCoq.PCUIC.PCUICAlpha]
decompose_stack_at_appstack_None [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
decompose_app_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
decompose_prod_assum_mkApps [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
decompose_app_wf [lemma, in MetaCoq.Examples.tauto]
decompose_app_eq [lemma, in MetaCoq.Examples.tauto]
decompose_app_size_tApp2 [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
decompose_app_size_tApp1 [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
decompose_app_rec_length [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
decompose_app_rec_length_mono [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
decompose_app_tApp_split [lemma, in MetaCoq.Erasure.ERemoveParams]
decompose_app_rec_inv' [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_rec_eq [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_eq_right [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_notApp [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_rec_notApp [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_inv [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_rec_inv [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_mkApps [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app_rec_mkApps [lemma, in MetaCoq.Erasure.EAstUtils]
decompose_app [definition, in MetaCoq.Erasure.EAstUtils]
decompose_app_rec [definition, in MetaCoq.Erasure.EAstUtils]
decompose_prod_n_assum_extend_ctx [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
decompose_app_rename [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
decompose_app_rec_rename [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
decompose_app_inst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decompose_app_rec_inst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decompose_prod_n_assum_inv [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
decompose_cstr_concl [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
decompose_lam [definition, in MetaCoq.Template.Pretty]
decompose_app_inv [lemma, in MetaCoq.Template.TypingWf]
decompose_app_mkApp [lemma, in MetaCoq.Template.TypingWf]
decompose_prod_assum_it_mkProd [lemma, in MetaCoq.Template.AstUtils]
decompose_prod_n_assum_it_mkProd [lemma, in MetaCoq.Template.AstUtils]
decompose_lam_n_assum [definition, in MetaCoq.Template.AstUtils]
decompose_prod_n_assum [definition, in MetaCoq.Template.AstUtils]
decompose_prod_assum [definition, in MetaCoq.Template.AstUtils]
decompose_prod [definition, in MetaCoq.Template.AstUtils]
decompose_app_mkApps [lemma, in MetaCoq.Template.AstUtils]
decompose_app [definition, in MetaCoq.Template.AstUtils]
decompose_app_rec_inv2 [lemma, in MetaCoq.Erasure.Prelim]
decompose_lam [definition, in MetaCoq.PCUIC.utils.PCUICPretty]
decomp_step_size [lemma, in MetaCoq.Examples.tauto]
decomp_step [definition, in MetaCoq.Examples.tauto]
decomp_branch' [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
decomp_branch [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
dec_All [lemma, in MetaCoq.PCUIC.PCUICNormal]
def [record, in MetaCoq.Template.BasicAst]
def [record, in MetaCoq.Erasure.EAst]
default_term [definition, in MetaCoq.Translations.param_binary]
default_checker_flags [instance, in MetaCoq.Template.config]
default_normalizing [instance, in MetaCoq.PCUIC.PCUICSN]
default_fuel [definition, in MetaCoq.Template.Checker]
default_term [definition, in MetaCoq.Translations.standard_model]
default_wcbv_flags [definition, in MetaCoq.Erasure.EWcbvEval]
default_term [definition, in MetaCoq.Translations.param_original]
default_relevance [definition, in MetaCoq.Template.AstUtils]
default_sort_family [definition, in MetaCoq.Template.AstUtils]
default:2 [binder, in MetaCoq.Template.utils.MCOption]
default:386 [binder, in MetaCoq.Template.utils.MCList]
default:74 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
default:8 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
DefinitionEntry [constructor, in MetaCoq.Template.Ast]
DefinitionEntry [constructor, in MetaCoq.PCUIC.PCUICAst]
DefinitionEntry [constructor, in MetaCoq.Erasure.EAst]
definition_entry_opaque [projection, in MetaCoq.Template.Ast]
definition_entry_universes [projection, in MetaCoq.Template.Ast]
definition_entry_body [projection, in MetaCoq.Template.Ast]
definition_entry_type [projection, in MetaCoq.Template.Ast]
definition_entry [record, in MetaCoq.Template.Ast]
definition_entry_opaque [projection, in MetaCoq.PCUIC.PCUICAst]
definition_entry_universes [projection, in MetaCoq.PCUIC.PCUICAst]
definition_entry_body [projection, in MetaCoq.PCUIC.PCUICAst]
definition_entry_type [projection, in MetaCoq.PCUIC.PCUICAst]
definition_entry [record, in MetaCoq.PCUIC.PCUICAst]
definition_entry_opaque [projection, in MetaCoq.Erasure.EAst]
definition_entry_body [projection, in MetaCoq.Erasure.EAst]
definition_entry [record, in MetaCoq.Erasure.EAst]
defs:117 [binder, in MetaCoq.Erasure.EDeps]
defs:12 [binder, in MetaCoq.Template.WcbvEval]
defs:12 [binder, in MetaCoq.Erasure.ECSubst]
defs:122 [binder, in MetaCoq.Erasure.EDeps]
defs:135 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:137 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:147 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:149 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:229 [binder, in MetaCoq.Erasure.Extract]
defs:23 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
defs:232 [binder, in MetaCoq.Erasure.Extract]
defs:274 [binder, in MetaCoq.PCUIC.PCUICNormal]
defs:280 [binder, in MetaCoq.PCUIC.PCUICNormal]
defs:36 [binder, in MetaCoq.Erasure.EPretty]
defs:36 [binder, in MetaCoq.Erasure.EDeps]
defs:39 [binder, in MetaCoq.Erasure.EDeps]
defs:42 [binder, in MetaCoq.Erasure.EDeps]
defs:49 [binder, in MetaCoq.Erasure.EDeps]
defs:50 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
defs:60 [binder, in MetaCoq.Template.Pretty]
defs:64 [binder, in MetaCoq.PCUIC.PCUICNormal]
def_ty:179 [binder, in MetaCoq.Template.EtaExpand]
def_ty:109 [binder, in MetaCoq.Template.EtaExpand]
def_eq_dec [instance, in MetaCoq.Template.BasicAst]
def_ty:91 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
def_ty:27 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
def_ty:195 [binder, in MetaCoq.Template.Ast]
def_sig [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
def_hole_body [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
def_hole_type [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
def_hole [inductive, in MetaCoq.PCUIC.Syntax.PCUICPosition]
def_size [definition, in MetaCoq.Examples.tauto]
def_size [definition, in MetaCoq.PCUIC.utils.PCUICSize]
def_depth_gen [definition, in MetaCoq.PCUIC.Syntax.PCUICDepth]
def':38 [binder, in MetaCoq.Template.EtaExpand]
def':46 [binder, in MetaCoq.Template.EtaExpand]
def:10 [binder, in MetaCoq.Template.AstUtils]
def:100 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:1008 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:107 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:108 [binder, in MetaCoq.Template.EtaExpand]
def:114 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:118 [binder, in MetaCoq.Erasure.EAstUtils]
def:121 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:1222 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1223 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1234 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1235 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1237 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1238 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1239 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1240 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1241 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1242 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1250 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1251 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1260 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1261 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1276 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1279 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1282 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1285 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1288 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1291 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:148 [binder, in MetaCoq.PCUIC.PCUICAst]
def:178 [binder, in MetaCoq.Template.EtaExpand]
def:19 [binder, in MetaCoq.Template.EtaExpand]
def:192 [binder, in MetaCoq.Erasure.EEtaExpanded]
def:194 [binder, in MetaCoq.Template.Ast]
def:21 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
def:225 [binder, in MetaCoq.Erasure.EEtaExpanded]
def:259 [binder, in MetaCoq.Template.Universes]
def:26 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
def:285 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:286 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:287 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:288 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:289 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:290 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:291 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:292 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:309 [binder, in MetaCoq.Template.Ast]
def:32 [binder, in MetaCoq.Erasure.EAst]
def:33 [binder, in MetaCoq.Erasure.EPretty]
def:374 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
def:376 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:381 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:413 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
def:426 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
def:45 [binder, in MetaCoq.Template.WfAst]
def:46 [binder, in MetaCoq.Template.BasicAst]
def:479 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
def:48 [binder, in MetaCoq.Template.WfAst]
def:48 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
def:50 [binder, in MetaCoq.Template.BasicAst]
def:506 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
def:56 [binder, in MetaCoq.Template.WfAst]
def:57 [binder, in MetaCoq.Template.WfAst]
def:57 [binder, in MetaCoq.Template.Pretty]
def:589 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:590 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:601 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:602 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:616 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:620 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:624 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:624 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:628 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:632 [binder, in MetaCoq.PCUIC.PCUICConfluence]
def:635 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:65 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
def:650 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:656 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:832 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
def:86 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:89 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:90 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
demo [library]
deps':1276 [binder, in MetaCoq.Erasure.ErasureFunction]
deps':1282 [binder, in MetaCoq.Erasure.ErasureFunction]
deps':839 [binder, in MetaCoq.Erasure.ErasureFunction]
deps':936 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1019 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1032 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1038 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1146 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1161 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1176 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1228 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1241 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1247 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1258 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1268 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1275 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1281 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1299 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1301 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1323 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1340 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1376 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1398 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1427 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1437 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1487 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1496 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1503 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1510 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1528 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:1531 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:779 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:789 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:819 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:834 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:838 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:844 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:933 [binder, in MetaCoq.Erasure.ErasureFunction]
deps:951 [binder, in MetaCoq.Erasure.ErasureFunction]
depth [definition, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depthA:92 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depthB:93 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth_subst_instance_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth_subst_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth_subst_decl [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth_subst_instance [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth_mkApps [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth':866 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
depth:1 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:10 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:12 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:14 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:39 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:4 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:77 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:8 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:85 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:858 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
depth:864 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Deq:1665 [binder, in MetaCoq.Translations.MiniHoTT]
Deq:1671 [binder, in MetaCoq.Translations.MiniHoTT]
Deq:1673 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Deq:1679 [binder, in MetaCoq.Translations.MiniHoTT_paths]
destArity [definition, in MetaCoq.Template.Ast]
destArity [definition, in MetaCoq.PCUIC.PCUICAst]
destArity_mkApps_Ind [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_mkApps_None [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_tInd [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_tApp [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_tFix [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_app_Some [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_app [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_app_aux [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
destArity_mkApps [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
destArity_alpha [lemma, in MetaCoq.PCUIC.PCUICAlpha]
destArity_spec_Some [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
destArity_spec [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
destArity_it_mkProd_or_LetIn [lemma, in MetaCoq.Template.TypingWf]
destArity_spec [lemma, in MetaCoq.Template.TypingWf]
destInd [definition, in MetaCoq.Template.Typing]
destInd [definition, in MetaCoq.PCUIC.PCUICTyping]
destInd [definition, in MetaCoq.Template.AstUtils]
destInd_Some_eq [lemma, in MetaCoq.PCUIC.PCUICInductives]
destInd_head_lift_inv [lemma, in MetaCoq.PCUIC.PCUICInductives]
destInd_head_lift [lemma, in MetaCoq.PCUIC.PCUICInductives]
destInd_head_subst [lemma, in MetaCoq.PCUIC.PCUICInductives]
destInd_spec [lemma, in MetaCoq.PCUIC.PCUICAlpha]
destInd_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
df:1698 [binder, in MetaCoq.Translations.MiniHoTT]
df:1706 [binder, in MetaCoq.Translations.MiniHoTT_paths]
diamond [definition, in MetaCoq.PCUIC.PCUICConfluence]
diamond_pred1_rel_alpha [lemma, in MetaCoq.PCUIC.PCUICConfluence]
diamond_pred1_rel [lemma, in MetaCoq.PCUIC.PCUICConfluence]
diamond_confluent [lemma, in MetaCoq.PCUIC.PCUICConfluence]
diamond_t_t_confluent [lemma, in MetaCoq.PCUIC.PCUICConfluence]
diamond_t1n_t1n_confluent [lemma, in MetaCoq.PCUIC.PCUICConfluence]
diamond_t1n_t_confluent [lemma, in MetaCoq.PCUIC.PCUICConfluence]
diamond_proper [instance, in MetaCoq.PCUIC.PCUICConfluence]
dirpath [definition, in MetaCoq.Template.Kernames]
DirPathOT [module, in MetaCoq.Template.Kernames]
dirpath_eqdec [instance, in MetaCoq.Template.Kernames]
disable_projections_env_flag [definition, in MetaCoq.Erasure.EInlineProjections]
disable_projections_term_flags [definition, in MetaCoq.Erasure.EInlineProjections]
disable_prop_cases [definition, in MetaCoq.Erasure.EInlineProjections]
disable_prop_cases [definition, in MetaCoq.Erasure.EWcbvEval]
Discharge [constructor, in MetaCoq.Template.TemplateMonad.Common]
discr_expanded_head [definition, in MetaCoq.Erasure.EEtaExpandedFix]
discr_construct0_cofix [definition, in MetaCoq.PCUIC.Syntax.PCUICViews]
discr_construct_cofix [definition, in MetaCoq.PCUIC.Syntax.PCUICViews]
discr_construct0_cofix [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
discr_construct_cofix [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
discr_construct [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
discr_construct [definition, in MetaCoq.Erasure.EEtaExpanded]
discr_prod_letin [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
discr':121 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
discr':208 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr':221 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr':281 [binder, in MetaCoq.Erasure.EArities]
discr':383 [binder, in MetaCoq.PCUIC.PCUICNormal]
discr:101 [binder, in MetaCoq.Erasure.EDeps]
discr:101 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:105 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
discr:110 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:110 [binder, in MetaCoq.Erasure.EWcbvEval]
discr:112 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr:114 [binder, in MetaCoq.Template.WcbvEval]
discr:116 [binder, in MetaCoq.Erasure.EWcbvEval]
discr:117 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
discr:119 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:121 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr:121 [binder, in MetaCoq.Erasure.EWcbvEval]
discr:123 [binder, in MetaCoq.Template.WcbvEval]
discr:125 [binder, in MetaCoq.Template.EtaExpand]
discr:131 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:142 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:156 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:165 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:166 [binder, in MetaCoq.Template.WcbvEval]
discr:178 [binder, in MetaCoq.Template.WcbvEval]
discr:199 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:199 [binder, in MetaCoq.Erasure.EEtaExpanded]
discr:200 [binder, in MetaCoq.Template.EtaExpand]
discr:207 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr:208 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:208 [binder, in MetaCoq.Template.Ast]
discr:208 [binder, in MetaCoq.Template.WcbvEval]
discr:216 [binder, in MetaCoq.Erasure.Extract]
discr:217 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:217 [binder, in MetaCoq.Template.WcbvEval]
discr:22 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:220 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr:222 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:232 [binder, in MetaCoq.Erasure.EEtaExpanded]
discr:28 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
discr:280 [binder, in MetaCoq.Erasure.EArities]
discr:29 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:324 [binder, in MetaCoq.Erasure.EArities]
discr:37 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
discr:37 [binder, in MetaCoq.Erasure.EWcbvEval]
discr:382 [binder, in MetaCoq.PCUIC.PCUICNormal]
discr:393 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
discr:45 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:46 [binder, in MetaCoq.Erasure.EWcbvEval]
discr:5 [binder, in MetaCoq.PCUIC.PCUICProgress]
discr:51 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:54 [binder, in MetaCoq.Erasure.EWcbvEval]
discr:60 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:60 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
discr:71 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr:74 [binder, in MetaCoq.Template.WcbvEval]
discr:75 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
discr:814 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
discr:83 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
discr:84 [binder, in MetaCoq.Template.WcbvEval]
discr:90 [binder, in MetaCoq.Erasure.EWcbvEval]
discr:99 [binder, in MetaCoq.Erasure.EWcbvEval]
DistinctCoFix [constructor, in MetaCoq.SafeChecker.PCUICErrors]
DistinctStuckProj [constructor, in MetaCoq.SafeChecker.PCUICErrors]
distr_subst [lemma, in MetaCoq.Erasure.ELiftSubst]
distr_subst_rec [lemma, in MetaCoq.Erasure.ELiftSubst]
distr_lift_subst10 [lemma, in MetaCoq.Erasure.ELiftSubst]
distr_lift_subst [lemma, in MetaCoq.Erasure.ELiftSubst]
distr_lift_subst_rec [lemma, in MetaCoq.Erasure.ELiftSubst]
distr_lift_subst_context_rec [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
distr_lift_subst_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
distr_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
distr_subst_rec [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst10 [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst_rec [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
distr_subst [lemma, in MetaCoq.Template.LiftSubst]
distr_subst_rec [lemma, in MetaCoq.Template.LiftSubst]
distr_lift_subst10 [lemma, in MetaCoq.Template.LiftSubst]
distr_lift_subst [lemma, in MetaCoq.Template.LiftSubst]
distr_lift_subst_rec [lemma, in MetaCoq.Template.LiftSubst]
dlam_tm [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlam_ty [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlet_in [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlet_ty [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlet_bd [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dlexmod [inductive, in MetaCoq.PCUIC.utils.PCUICUtils]
dlexmod_Acc [lemma, in MetaCoq.PCUIC.utils.PCUICUtils]
dlexprod [inductive, in MetaCoq.PCUIC.utils.PCUICUtils]
dlexprod_trans [instance, in MetaCoq.PCUIC.utils.PCUICUtils]
dlexprod_Acc [lemma, in MetaCoq.PCUIC.utils.PCUICUtils]
dlexprod_Acc_gen [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
dname [projection, in MetaCoq.Template.BasicAst]
dname [projection, in MetaCoq.Erasure.EAst]
dname:338 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dname:341 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
domsort:225 [binder, in MetaCoq.Template.Universes]
domsort:293 [binder, in MetaCoq.Template.Universes]
dom':196 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom':205 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom':214 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom':221 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:115 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:115 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
dom:121 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:127 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
dom:193 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:201 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:210 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:210 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
dom:220 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:346 [binder, in MetaCoq.PCUIC.PCUICSpine]
dom:352 [binder, in MetaCoq.PCUIC.PCUICSpine]
dom:365 [binder, in MetaCoq.PCUIC.PCUICSpine]
dom:366 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
dom:465 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:472 [binder, in MetaCoq.PCUIC.PCUICConversion]
dom:495 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
dom:73 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
do_check_ind_sorts [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
dpath_forall' [definition, in MetaCoq.Translations.MiniHoTT]
dpath_forall_constant [definition, in MetaCoq.Translations.MiniHoTT]
dpath_forall [definition, in MetaCoq.Translations.MiniHoTT]
dpath_paths2 [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_lFFr [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_FFlr [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_FlFr [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_Fr [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_Fl [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_lr [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_r [definition, in MetaCoq.Translations.MiniHoTT]
dpath_path_l [definition, in MetaCoq.Translations.MiniHoTT]
dpath_forall' [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_forall_constant [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_forall [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_paths2 [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_lFFr [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_FFlr [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_FlFr [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_Fr [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_Fl [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_lr [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_r [definition, in MetaCoq.Translations.MiniHoTT_paths]
dpath_path_l [definition, in MetaCoq.Translations.MiniHoTT_paths]
dprod_r [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dprod_l [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dproj_c [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dp':17 [binder, in MetaCoq.Template.Kernames]
dp:1 [binder, in MetaCoq.Template.Kernames]
dp:14 [binder, in MetaCoq.Template.Kernames]
dp:4 [binder, in MetaCoq.Template.Kernames]
dp:5 [binder, in MetaCoq.Template.Kernames]
ds:117 [binder, in MetaCoq.Template.Checker]
ds:439 [binder, in MetaCoq.Template.utils.wGraph]
ds:448 [binder, in MetaCoq.Template.utils.wGraph]
dtype [projection, in MetaCoq.Template.BasicAst]
dtype:342 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
dummy_branch [definition, in MetaCoq.Template.Typing]
dummy_branch [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
dummy_decl [definition, in MetaCoq.PCUIC.TemplateToPCUIC]
d':115 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d':118 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':121 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d':124 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':133 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d':134 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
d':1340 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d':135 [binder, in MetaCoq.Erasure.Extract]
d':137 [binder, in MetaCoq.Erasure.Extract]
d':1376 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d':1380 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d':14 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
d':144 [binder, in MetaCoq.Erasure.Extract]
d':146 [binder, in MetaCoq.Erasure.Extract]
d':146 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
d':15 [binder, in MetaCoq.PCUIC.PCUICSpine]
d':154 [binder, in MetaCoq.Translations.translation_utils]
d':1657 [binder, in MetaCoq.Template.utils.All_Forall]
d':168 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':172 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d':1721 [binder, in MetaCoq.Template.utils.All_Forall]
d':173 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':1761 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d':178 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':183 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':186 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d':188 [binder, in MetaCoq.PCUIC.PCUICConversion]
d':189 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d':1928 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d':1930 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d':1933 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d':1937 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d':202 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d':207 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':210 [binder, in MetaCoq.PCUIC.PCUICEquality]
d':213 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':2132 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d':2144 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d':221 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':221 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':226 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':2262 [binder, in MetaCoq.Template.utils.All_Forall]
d':227 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d':228 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':2290 [binder, in MetaCoq.Template.utils.All_Forall]
d':2304 [binder, in MetaCoq.Template.utils.All_Forall]
d':231 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':2313 [binder, in MetaCoq.Template.utils.All_Forall]
d':2322 [binder, in MetaCoq.Template.utils.All_Forall]
d':236 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':236 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':2396 [binder, in MetaCoq.Template.utils.All_Forall]
d':241 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':2411 [binder, in MetaCoq.Template.utils.All_Forall]
d':2417 [binder, in MetaCoq.Template.utils.All_Forall]
d':244 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':252 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':257 [binder, in MetaCoq.Template.utils.MCList]
d':26 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
d':26 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d':265 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':27 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
d':273 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d':279 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d':286 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':292 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':300 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':301 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':302 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':303 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':304 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':305 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':306 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':307 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':308 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':309 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':310 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':310 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':311 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':312 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':313 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':314 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':318 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
d':335 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
d':34 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
d':342 [binder, in MetaCoq.Template.Environment]
d':348 [binder, in MetaCoq.Template.Environment]
d':353 [binder, in MetaCoq.Template.Environment]
d':360 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d':369 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
d':374 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d':376 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
d':377 [binder, in MetaCoq.PCUIC.PCUICNormal]
d':380 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d':384 [binder, in MetaCoq.Template.EtaExpand]
d':387 [binder, in MetaCoq.Template.BasicAst]
d':390 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d':396 [binder, in MetaCoq.Template.BasicAst]
d':399 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d':405 [binder, in MetaCoq.Template.BasicAst]
d':411 [binder, in MetaCoq.PCUIC.PCUICNormal]
d':412 [binder, in MetaCoq.Template.BasicAst]
d':422 [binder, in MetaCoq.PCUIC.PCUICEquality]
d':449 [binder, in MetaCoq.Erasure.ErasureFunction]
d':450 [binder, in MetaCoq.PCUIC.PCUICInductives]
d':458 [binder, in MetaCoq.Erasure.ErasureFunction]
d':493 [binder, in MetaCoq.Template.Typing]
d':501 [binder, in MetaCoq.Template.utils.MCList]
d':51 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d':513 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d':522 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d':525 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d':58 [binder, in MetaCoq.Translations.translation_utils]
d':584 [binder, in MetaCoq.PCUIC.PCUICEquality]
d':6 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
d':616 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d':62 [binder, in MetaCoq.Erasure.Extract]
d':624 [binder, in MetaCoq.Erasure.ErasureFunction]
d':626 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d':630 [binder, in MetaCoq.Erasure.ErasureFunction]
d':637 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d':651 [binder, in MetaCoq.Erasure.ErasureFunction]
d':657 [binder, in MetaCoq.Erasure.ErasureFunction]
d':663 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d':67 [binder, in MetaCoq.Translations.translation_utils]
d':67 [binder, in MetaCoq.Erasure.Extract]
d':72 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
d':73 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
d':78 [binder, in MetaCoq.PCUIC.PCUICEquality]
d':78 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d':838 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d':88 [binder, in MetaCoq.PCUIC.PCUICEquality]
d':888 [binder, in MetaCoq.Erasure.ErasureFunction]
d':89 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d':900 [binder, in MetaCoq.Erasure.ErasureFunction]
d':938 [binder, in MetaCoq.PCUIC.PCUICConversion]
d':943 [binder, in MetaCoq.PCUIC.PCUICConversion]
d':952 [binder, in MetaCoq.PCUIC.PCUICConversion]
d':953 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d':96 [binder, in MetaCoq.PCUIC.PCUICEquality]
d0:1048 [binder, in MetaCoq.PCUIC.PCUICReduction]
d0:1119 [binder, in MetaCoq.PCUIC.PCUICReduction]
d0:120 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d0:123 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d0:183 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d0:185 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d0:186 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d0:193 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d0:194 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d0:239 [binder, in MetaCoq.PCUIC.PCUICConversion]
d0:258 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d0:296 [binder, in MetaCoq.Template.EtaExpand]
d0:304 [binder, in MetaCoq.Template.EtaExpand]
d0:353 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d0:372 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d0:377 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d0:380 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d0:444 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d0:449 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d0:451 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d0:476 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d0:87 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d0:870 [binder, in MetaCoq.PCUIC.PCUICReduction]
d0:90 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d1:1049 [binder, in MetaCoq.PCUIC.PCUICReduction]
d1:1120 [binder, in MetaCoq.PCUIC.PCUICReduction]
d1:121 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d1:124 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d1:184 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d1:23 [binder, in MetaCoq.Template.Reflect]
d1:240 [binder, in MetaCoq.PCUIC.PCUICConversion]
d1:259 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d1:297 [binder, in MetaCoq.Template.EtaExpand]
d1:305 [binder, in MetaCoq.Template.EtaExpand]
d1:354 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d1:373 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d1:378 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d1:381 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d1:39 [binder, in MetaCoq.Erasure.ErasureCorrectness]
d1:40 [binder, in MetaCoq.Erasure.ErasureCorrectness]
d1:41 [binder, in MetaCoq.Erasure.ErasureCorrectness]
d1:42 [binder, in MetaCoq.Erasure.ErasureCorrectness]
d1:445 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d1:450 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d1:452 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d1:871 [binder, in MetaCoq.PCUIC.PCUICReduction]
D1:915 [binder, in MetaCoq.Translations.MiniHoTT]
D1:923 [binder, in MetaCoq.Translations.MiniHoTT_paths]
d2:24 [binder, in MetaCoq.Template.Reflect]
D2:916 [binder, in MetaCoq.Translations.MiniHoTT]
D2:924 [binder, in MetaCoq.Translations.MiniHoTT_paths]
d:10 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:100 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:1000 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d:1001 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:1008 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:101 [binder, in MetaCoq.PCUIC.PCUICArities]
d:101 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
d:101 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:101 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:1019 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:102 [binder, in MetaCoq.Template.Checker]
d:1022 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:1023 [binder, in MetaCoq.Erasure.ErasureFunction]
d:1029 [binder, in MetaCoq.Template.utils.wGraph]
d:1037 [binder, in MetaCoq.Template.utils.wGraph]
d:104 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:104 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:104 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
d:1041 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:1042 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:1043 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:1044 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:105 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:1056 [binder, in MetaCoq.Erasure.ErasureFunction]
d:106 [binder, in MetaCoq.Template.Environment]
d:106 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:107 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:1071 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:1073 [binder, in MetaCoq.Erasure.ErasureFunction]
d:1078 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:109 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:109 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:11 [binder, in MetaCoq.Template.EtaExpand]
d:11 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:11 [binder, in MetaCoq.Template.TemplateCheckWf]
d:11 [binder, in MetaCoq.Erasure.EAst]
d:11 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:11 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:110 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:111 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:111 [binder, in MetaCoq.Erasure.EGlobalEnv]
d:111 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:1112 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:1113 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:1114 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:1115 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:113 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:114 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d:114 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:115 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:115 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:116 [binder, in MetaCoq.Template.WfAst]
d:116 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:1167 [binder, in MetaCoq.Template.utils.wGraph]
d:117 [binder, in MetaCoq.Translations.translation_utils]
d:117 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:1176 [binder, in MetaCoq.PCUIC.PCUICConfluence]
D:118 [binder, in MetaCoq.Template.utils.All_Forall]
d:1180 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:1184 [binder, in MetaCoq.Erasure.ErasureFunction]
d:119 [binder, in MetaCoq.Erasure.EDeps]
d:119 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:119 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:119 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:1195 [binder, in MetaCoq.Template.Typing]
d:12 [binder, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
d:12 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
d:120 [binder, in MetaCoq.Erasure.EDeps]
d:120 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d:1204 [binder, in MetaCoq.Template.Typing]
d:121 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:122 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:1227 [binder, in MetaCoq.Template.Typing]
d:123 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:1236 [binder, in MetaCoq.Template.Typing]
d:124 [binder, in MetaCoq.Erasure.EDeps]
d:1249 [binder, in MetaCoq.Translations.MiniHoTT]
d:125 [binder, in MetaCoq.Translations.translation_utils]
d:125 [binder, in MetaCoq.Erasure.EDeps]
d:1257 [binder, in MetaCoq.Translations.MiniHoTT_paths]
d:127 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:127 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:128 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:129 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:13 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:13 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d:13 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:13 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
D:13 [binder, in MetaCoq.Template.utils.MCProd]
d:13 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:130 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:1318 [binder, in MetaCoq.Template.Typing]
d:132 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d:133 [binder, in MetaCoq.Template.EtaExpand]
d:133 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
d:133 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:1334 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:1339 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:134 [binder, in MetaCoq.Template.EtaExpand]
d:134 [binder, in MetaCoq.Erasure.Extract]
d:1343 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:136 [binder, in MetaCoq.Template.EtaExpand]
d:136 [binder, in MetaCoq.Erasure.Extract]
d:1375 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:1378 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:139 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:14 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
d:14 [binder, in MetaCoq.PCUIC.PCUICSpine]
d:140 [binder, in MetaCoq.Template.EtaExpand]
d:140 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
d:1400 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:141 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:141 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:141 [binder, in MetaCoq.Erasure.ERemoveParams]
d:143 [binder, in MetaCoq.Template.BasicAst]
d:143 [binder, in MetaCoq.PCUIC.PCUICArities]
d:143 [binder, in MetaCoq.Erasure.Extract]
d:143 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:1443 [binder, in MetaCoq.Erasure.ErasureFunction]
d:1449 [binder, in MetaCoq.Erasure.ErasureFunction]
d:145 [binder, in MetaCoq.Erasure.Extract]
d:145 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
d:145 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:145 [binder, in MetaCoq.Template.TypingWf]
D:147 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:147 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:147 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:148 [binder, in MetaCoq.Erasure.ERemoveParams]
d:149 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:149 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:149 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:149 [binder, in MetaCoq.Template.TypingWf]
d:15 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:15 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:15 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
D:1507 [binder, in MetaCoq.Translations.MiniHoTT]
d:151 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:151 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:151 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
D:1515 [binder, in MetaCoq.Translations.MiniHoTT_paths]
D:1519 [binder, in MetaCoq.Translations.MiniHoTT]
d:152 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
D:1527 [binder, in MetaCoq.Translations.MiniHoTT_paths]
d:153 [binder, in MetaCoq.Template.BasicAst]
d:153 [binder, in MetaCoq.Erasure.ERemoveParams]
d:153 [binder, in MetaCoq.Template.LiftSubst]
d:155 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:155 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:155 [binder, in MetaCoq.Template.LiftSubst]
d:156 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:157 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:157 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:157 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:157 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
d:157 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:157 [binder, in MetaCoq.Template.LiftSubst]
d:159 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
d:16 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:16 [binder, in MetaCoq.Erasure.Extract]
d:16 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:160 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
d:160 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:160 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:161 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:161 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:162 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:163 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:164 [binder, in MetaCoq.Erasure.EInlineProjections]
d:164 [binder, in MetaCoq.PCUIC.PCUICInversion]
d:164 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:165 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:165 [binder, in MetaCoq.PCUIC.PCUICInversion]
d:1656 [binder, in MetaCoq.Template.utils.All_Forall]
d:166 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
D:1663 [binder, in MetaCoq.Translations.MiniHoTT]
D:1669 [binder, in MetaCoq.Translations.MiniHoTT]
d:167 [binder, in MetaCoq.Erasure.EInlineProjections]
d:167 [binder, in MetaCoq.PCUIC.PCUICConfluence]
D:1671 [binder, in MetaCoq.Translations.MiniHoTT_paths]
D:1677 [binder, in MetaCoq.Translations.MiniHoTT_paths]
d:168 [binder, in MetaCoq.PCUIC.PCUICArities]
d:169 [binder, in MetaCoq.Template.EnvironmentTyping]
d:169 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:169 [binder, in MetaCoq.Template.LiftSubst]
d:17 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:17 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d:17 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:170 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
d:171 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
d:171 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:171 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:172 [binder, in MetaCoq.Template.EnvironmentTyping]
d:172 [binder, in MetaCoq.PCUIC.PCUICInversion]
d:172 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:1720 [binder, in MetaCoq.Template.utils.All_Forall]
d:173 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:173 [binder, in MetaCoq.PCUIC.PCUICInversion]
d:173 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:176 [binder, in MetaCoq.Template.EnvironmentTyping]
d:1760 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d:177 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:177 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
d:178 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:179 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:18 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:18 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
d:18 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
d:180 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:180 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
d:181 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:182 [binder, in MetaCoq.Template.BasicAst]
d:182 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
d:182 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
d:182 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:183 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:183 [binder, in MetaCoq.Template.Environment]
d:185 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:185 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:185 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:186 [binder, in MetaCoq.Template.BasicAst]
d:186 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:187 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
D:187 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:188 [binder, in MetaCoq.Template.Environment]
d:188 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d:189 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:189 [binder, in MetaCoq.Template.BasicAst]
d:189 [binder, in MetaCoq.Template.Environment]
d:1896 [binder, in MetaCoq.Template.utils.All_Forall]
d:19 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:1902 [binder, in MetaCoq.Template.utils.All_Forall]
d:1927 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d:1929 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d:193 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:1932 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d:1936 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
D:1937 [binder, in MetaCoq.Template.utils.All_Forall]
d:194 [binder, in MetaCoq.Template.Environment]
d:194 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
D:1957 [binder, in MetaCoq.Template.utils.All_Forall]
d:196 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:2 [binder, in MetaCoq.Template.utils.MCCompare]
d:2 [binder, in MetaCoq.Template.TemplateCheckWf]
d:2 [binder, in MetaCoq.Erasure.EEnvMap]
d:20 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
d:20 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
d:20 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
D:20 [binder, in MetaCoq.Template.utils.MCProd]
d:201 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d:202 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:204 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:204 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:206 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:206 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:208 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:209 [binder, in MetaCoq.PCUIC.PCUICEquality]
d:209 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:21 [binder, in MetaCoq.Template.EtaExpand]
d:21 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
d:21 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:21 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
d:21 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
d:210 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:210 [binder, in MetaCoq.Template.EtaExpand]
D:210 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:212 [binder, in MetaCoq.Template.EtaExpand]
d:212 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:2131 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
D:2134 [binder, in MetaCoq.Template.utils.All_Forall]
d:214 [binder, in MetaCoq.Template.EtaExpand]
d:214 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:2143 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
D:2146 [binder, in MetaCoq.Template.utils.All_Forall]
D:215 [binder, in MetaCoq.Template.utils.All_Forall]
d:216 [binder, in MetaCoq.Template.EtaExpand]
d:218 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:218 [binder, in MetaCoq.Template.EtaExpand]
d:219 [binder, in MetaCoq.Erasure.EWcbvEval]
d:22 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d:22 [binder, in MetaCoq.PCUIC.PCUICInversion]
d:22 [binder, in MetaCoq.Template.Environment]
d:220 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:220 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:220 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:221 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:223 [binder, in MetaCoq.Template.EtaExpand]
d:224 [binder, in MetaCoq.Template.EtaExpand]
d:224 [binder, in MetaCoq.Erasure.EWcbvEval]
d:225 [binder, in MetaCoq.Template.BasicAst]
d:225 [binder, in MetaCoq.Erasure.ErasureFunction]
d:225 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:2255 [binder, in MetaCoq.Template.utils.All_Forall]
d:226 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
D:226 [binder, in MetaCoq.Template.utils.All_Forall]
d:226 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:226 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d:2261 [binder, in MetaCoq.Template.utils.All_Forall]
d:227 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:228 [binder, in MetaCoq.Template.BasicAst]
d:2289 [binder, in MetaCoq.Template.utils.All_Forall]
d:23 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:23 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:23 [binder, in MetaCoq.Template.utils.MCProd]
d:230 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:230 [binder, in MetaCoq.Erasure.ErasureFunction]
d:230 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:230 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:2303 [binder, in MetaCoq.Template.utils.All_Forall]
d:231 [binder, in MetaCoq.Erasure.Extract]
d:231 [binder, in MetaCoq.Template.Environment]
d:2312 [binder, in MetaCoq.Template.utils.All_Forall]
d:232 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:232 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:2321 [binder, in MetaCoq.Template.utils.All_Forall]
d:2328 [binder, in MetaCoq.Template.utils.All_Forall]
d:2334 [binder, in MetaCoq.Template.utils.All_Forall]
d:234 [binder, in MetaCoq.Erasure.Extract]
d:2349 [binder, in MetaCoq.Template.utils.All_Forall]
d:235 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:235 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:2354 [binder, in MetaCoq.Template.utils.All_Forall]
d:2359 [binder, in MetaCoq.Template.utils.All_Forall]
D:237 [binder, in MetaCoq.Template.utils.All_Forall]
D:237 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:2395 [binder, in MetaCoq.Template.utils.All_Forall]
d:24 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
d:24 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
d:240 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:240 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:241 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:2410 [binder, in MetaCoq.Template.utils.All_Forall]
d:2418 [binder, in MetaCoq.Template.utils.All_Forall]
d:243 [binder, in MetaCoq.Template.EtaExpand]
d:243 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:244 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:245 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:245 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
d:245 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:246 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:2467 [binder, in MetaCoq.Template.utils.All_Forall]
d:247 [binder, in MetaCoq.Template.BasicAst]
d:247 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:2472 [binder, in MetaCoq.Template.utils.All_Forall]
d:249 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:25 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:25 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
d:25 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d:250 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
d:251 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:252 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:253 [binder, in MetaCoq.Template.BasicAst]
d:256 [binder, in MetaCoq.Template.utils.MCList]
d:256 [binder, in MetaCoq.Erasure.EEtaExpanded]
d:256 [binder, in MetaCoq.Template.TypingWf]
D:2562 [binder, in MetaCoq.Template.utils.All_Forall]
D:2566 [binder, in MetaCoq.Template.utils.All_Forall]
d:257 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:258 [binder, in MetaCoq.Template.BasicAst]
d:259 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:26 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
d:26 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
d:26 [binder, in MetaCoq.Erasure.EExtends]
d:261 [binder, in MetaCoq.Template.EtaExpand]
d:263 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:264 [binder, in MetaCoq.PCUIC.PCUICConfluence]
D:266 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:268 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:268 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:269 [binder, in MetaCoq.PCUIC.PCUICInductives]
d:27 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
d:27 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:27 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:27 [binder, in MetaCoq.Erasure.EGlobalEnv]
d:27 [binder, in MetaCoq.Erasure.EExtends]
d:27 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:27 [binder, in MetaCoq.Erasure.EGenericMapEnv]
d:270 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:272 [binder, in MetaCoq.PCUIC.PCUICInductives]
d:272 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:272 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:274 [binder, in MetaCoq.PCUIC.PCUICInductives]
d:275 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
D:276 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:278 [binder, in MetaCoq.PCUIC.PCUICConfluence]
d:279 [binder, in MetaCoq.Template.EtaExpand]
d:28 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
d:28 [binder, in MetaCoq.Template.EnvMap]
d:28 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:28 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
d:28 [binder, in MetaCoq.PCUIC.PCUICContexts]
d:284 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:285 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:285 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:285 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:286 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:289 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
d:29 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:29 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
D:2902 [binder, in MetaCoq.Translations.MiniHoTT]
d:291 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:291 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
D:2910 [binder, in MetaCoq.Translations.MiniHoTT_paths]
d:294 [binder, in MetaCoq.Template.EtaExpand]
d:296 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:298 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:3 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:30 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
d:30 [binder, in MetaCoq.Template.EnvMap]
d:30 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:300 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:301 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:301 [binder, in MetaCoq.PCUIC.PCUICAst]
d:301 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:304 [binder, in MetaCoq.Erasure.ERemoveParams]
d:306 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:306 [binder, in MetaCoq.PCUIC.PCUICAst]
D:306 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:307 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:308 [binder, in MetaCoq.PCUIC.PCUICInductives]
d:309 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:31 [binder, in MetaCoq.Template.Typing]
d:31 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:31 [binder, in MetaCoq.Template.Environment]
d:31 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:31 [binder, in MetaCoq.Erasure.EExtends]
d:313 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:317 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
d:32 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
d:32 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:32 [binder, in MetaCoq.Erasure.EExtends]
d:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:326 [binder, in MetaCoq.PCUIC.PCUICSR]
d:329 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
d:33 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
d:33 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:33 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
D:33 [binder, in MetaCoq.Template.utils.MCProd]
d:33 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:331 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
d:331 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:332 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
d:338 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:339 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:34 [binder, in MetaCoq.Template.EtaExpand]
d:34 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
D:340 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:341 [binder, in MetaCoq.Template.Environment]
d:342 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:344 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:347 [binder, in MetaCoq.Template.Environment]
d:35 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
d:35 [binder, in MetaCoq.Template.Pretty]
D:350 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:352 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:352 [binder, in MetaCoq.Template.Environment]
d:357 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
d:359 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d:359 [binder, in MetaCoq.PCUIC.PCUICSpine]
d:36 [binder, in MetaCoq.Template.EtaExpand]
d:36 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:36 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
d:361 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:362 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:364 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:368 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
d:368 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:37 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:37 [binder, in MetaCoq.Erasure.EPretty]
d:373 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
D:375 [binder, in MetaCoq.Template.utils.All_Forall]
d:375 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
d:376 [binder, in MetaCoq.PCUIC.PCUICNormal]
d:377 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
d:379 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:38 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:38 [binder, in MetaCoq.PCUIC.PCUICValidity]
d:38 [binder, in MetaCoq.Template.utils.MCOption]
d:38 [binder, in MetaCoq.Erasure.EExtends]
d:383 [binder, in MetaCoq.Template.EtaExpand]
d:383 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:386 [binder, in MetaCoq.Template.BasicAst]
D:387 [binder, in MetaCoq.Template.utils.All_Forall]
d:389 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:39 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
d:39 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
d:392 [binder, in MetaCoq.PCUIC.PCUICAst]
d:395 [binder, in MetaCoq.Template.BasicAst]
d:397 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
D:397 [binder, in MetaCoq.Template.utils.All_Forall]
d:398 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
D:398 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
d:398 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:399 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:4 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:400 [binder, in MetaCoq.Erasure.ERemoveParams]
d:403 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:404 [binder, in MetaCoq.Template.BasicAst]
d:404 [binder, in MetaCoq.Erasure.ERemoveParams]
d:405 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
D:405 [binder, in MetaCoq.Template.utils.All_Forall]
D:408 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
d:41 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:41 [binder, in MetaCoq.Template.EnvMap]
d:41 [binder, in MetaCoq.Template.Environment]
d:41 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
d:410 [binder, in MetaCoq.PCUIC.PCUICNormal]
d:411 [binder, in MetaCoq.Template.BasicAst]
d:412 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d:417 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:418 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:42 [binder, in MetaCoq.Template.EtaExpand]
d:42 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:42 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:421 [binder, in MetaCoq.PCUIC.PCUICEquality]
d:422 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:424 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:427 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:429 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:430 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:431 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:432 [binder, in MetaCoq.Erasure.ERemoveParams]
d:44 [binder, in MetaCoq.Template.EtaExpand]
d:44 [binder, in MetaCoq.Translations.translation_utils]
d:444 [binder, in MetaCoq.PCUIC.PCUICTyping]
d:447 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:447 [binder, in MetaCoq.PCUIC.PCUICInductives]
d:45 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
d:46 [binder, in MetaCoq.Erasure.EDeps]
d:47 [binder, in MetaCoq.Erasure.EInlineProjections]
d:47 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
d:47 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
d:471 [binder, in MetaCoq.PCUIC.PCUICAst]
d:475 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:475 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:476 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:479 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:48 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:48 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
d:480 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:49 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:49 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
d:492 [binder, in MetaCoq.Template.Typing]
d:497 [binder, in MetaCoq.Template.utils.MCList]
d:5 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
d:5 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
d:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
d:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:5 [binder, in MetaCoq.Erasure.EGenericMapEnv]
d:50 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:50 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d:50 [binder, in MetaCoq.Erasure.EWellformed]
d:500 [binder, in MetaCoq.Template.utils.MCList]
d:505 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d:506 [binder, in MetaCoq.PCUIC.PCUICInductives]
d:51 [binder, in MetaCoq.Template.Environment]
d:512 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
D:515 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:518 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:518 [binder, in MetaCoq.PCUIC.PCUICInductives]
d:519 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:52 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
d:521 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:524 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:526 [binder, in MetaCoq.Template.EtaExpand]
d:529 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
d:53 [binder, in MetaCoq.Erasure.EDeps]
d:53 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
d:532 [binder, in MetaCoq.PCUIC.PCUICAst]
d:54 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:543 [binder, in MetaCoq.Template.EtaExpand]
d:543 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:55 [binder, in MetaCoq.Template.BasicAst]
d:55 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
d:55 [binder, in MetaCoq.Template.Environment]
d:55 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:555 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:56 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:56 [binder, in MetaCoq.Erasure.EAst]
d:56 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
d:57 [binder, in MetaCoq.Translations.translation_utils]
d:57 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
d:57 [binder, in MetaCoq.Erasure.EWellformed]
d:57 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:58 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:58 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:583 [binder, in MetaCoq.PCUIC.PCUICEquality]
d:584 [binder, in MetaCoq.Template.Typing]
d:59 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:591 [binder, in MetaCoq.Template.Typing]
d:60 [binder, in MetaCoq.Template.BasicAst]
d:61 [binder, in MetaCoq.Erasure.Extract]
d:61 [binder, in MetaCoq.Erasure.EAst]
d:612 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:612 [binder, in MetaCoq.PCUIC.PCUICSR]
d:62 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:623 [binder, in MetaCoq.Erasure.ErasureFunction]
d:625 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d:629 [binder, in MetaCoq.Erasure.ErasureFunction]
d:636 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d:64 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
d:64 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
D:641 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:65 [binder, in MetaCoq.Template.BasicAst]
d:65 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d:650 [binder, in MetaCoq.Erasure.ErasureFunction]
d:655 [binder, in MetaCoq.Template.EnvironmentTyping]
d:656 [binder, in MetaCoq.Erasure.ErasureFunction]
d:658 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:66 [binder, in MetaCoq.Translations.translation_utils]
d:66 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
d:66 [binder, in MetaCoq.Erasure.Extract]
d:66 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
d:66 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:661 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:662 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d:668 [binder, in MetaCoq.Template.EnvironmentTyping]
d:67 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d:675 [binder, in MetaCoq.Template.utils.MCList]
d:675 [binder, in MetaCoq.Template.Typing]
d:677 [binder, in MetaCoq.Template.Typing]
d:679 [binder, in MetaCoq.Template.utils.MCList]
d:68 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:68 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:681 [binder, in MetaCoq.Template.Typing]
d:683 [binder, in MetaCoq.Template.Typing]
d:69 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d:69 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:694 [binder, in MetaCoq.Erasure.ErasureFunction]
d:7 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:70 [binder, in MetaCoq.Template.BasicAst]
d:70 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:70 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
d:701 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:71 [binder, in MetaCoq.Erasure.EInlineProjections]
d:71 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
d:72 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
d:72 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
d:72 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
d:721 [binder, in MetaCoq.Template.EnvironmentTyping]
D:723 [binder, in MetaCoq.Template.utils.MCList]
d:729 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
d:73 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
d:741 [binder, in MetaCoq.Template.Typing]
d:741 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:748 [binder, in MetaCoq.PCUIC.PCUICReduction]
d:76 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:76 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
d:768 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:769 [binder, in MetaCoq.Template.Typing]
d:77 [binder, in MetaCoq.Template.EnvironmentTyping]
d:77 [binder, in MetaCoq.PCUIC.PCUICEquality]
d:77 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d:771 [binder, in MetaCoq.Template.Universes]
d:775 [binder, in MetaCoq.Template.Universes]
d:78 [binder, in MetaCoq.Erasure.EGenericMapEnv]
D:793 [binder, in MetaCoq.Translations.MiniHoTT]
d:795 [binder, in MetaCoq.Erasure.ErasureFunction]
d:797 [binder, in MetaCoq.Erasure.ErasureFunction]
d:799 [binder, in MetaCoq.Erasure.ErasureFunction]
d:8 [binder, in MetaCoq.Erasure.EAst]
d:8 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
d:8 [binder, in MetaCoq.Template.TypingWf]
d:80 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:80 [binder, in MetaCoq.Template.TypingWf]
d:80 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
d:801 [binder, in MetaCoq.Erasure.ErasureFunction]
D:801 [binder, in MetaCoq.Translations.MiniHoTT_paths]
d:803 [binder, in MetaCoq.Erasure.ErasureFunction]
d:805 [binder, in MetaCoq.Erasure.ErasureFunction]
d:807 [binder, in MetaCoq.Erasure.ErasureFunction]
d:809 [binder, in MetaCoq.Erasure.ErasureFunction]
d:811 [binder, in MetaCoq.Erasure.ErasureFunction]
d:812 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
d:813 [binder, in MetaCoq.Erasure.ErasureFunction]
d:815 [binder, in MetaCoq.Erasure.ErasureFunction]
d:817 [binder, in MetaCoq.Erasure.ErasureFunction]
d:82 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:82 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:82 [binder, in MetaCoq.Erasure.EPretty]
d:82 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
d:82 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
d:82 [binder, in MetaCoq.Erasure.EGenericMapEnv]
d:83 [binder, in MetaCoq.Template.BasicAst]
d:83 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d:83 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:83 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:834 [binder, in MetaCoq.Template.Typing]
d:837 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
D:84 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:84 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d:85 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d:85 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:85 [binder, in MetaCoq.Erasure.EGenericMapEnv]
d:86 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:86 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:86 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:87 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
d:87 [binder, in MetaCoq.PCUIC.PCUICEquality]
d:87 [binder, in MetaCoq.Erasure.ErasureProperties]
d:87 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
D:873 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:878 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:88 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:88 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:88 [binder, in MetaCoq.PCUIC.PCUICAlpha]
d:88 [binder, in MetaCoq.Erasure.ErasureProperties]
d:88 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:88 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:880 [binder, in MetaCoq.Erasure.ErasureFunction]
d:887 [binder, in MetaCoq.Erasure.ErasureFunction]
d:89 [binder, in MetaCoq.Erasure.ErasureProperties]
d:89 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
d:892 [binder, in MetaCoq.Erasure.ErasureFunction]
d:896 [binder, in MetaCoq.Erasure.ErasureFunction]
d:899 [binder, in MetaCoq.Erasure.ErasureFunction]
d:9 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:9 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
d:9 [binder, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
d:90 [binder, in MetaCoq.Erasure.ErasureProperties]
d:90 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
d:901 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:905 [binder, in MetaCoq.Erasure.ErasureFunction]
d:91 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:919 [binder, in MetaCoq.Template.Typing]
d:937 [binder, in MetaCoq.Erasure.ErasureFunction]
d:937 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:942 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:946 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d:95 [binder, in MetaCoq.PCUIC.PCUICEquality]
d:951 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:952 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d:96 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:96 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
d:96 [binder, in MetaCoq.Erasure.ERemoveParams]
d:96 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:961 [binder, in MetaCoq.PCUIC.PCUICConversion]
d:964 [binder, in MetaCoq.Erasure.ErasureFunction]
d:97 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
d:97 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:974 [binder, in MetaCoq.Erasure.ErasureFunction]
d:98 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
d:987 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d:99 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:99 [binder, in MetaCoq.Erasure.ERemoveParams]
d:990 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
d:991 [binder, in MetaCoq.PCUIC.PCUICTyping]
dΣ:490 [binder, in MetaCoq.Template.EtaExpand]

---

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