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

(945 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

(18 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

(6 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

(43 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

(30 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

(133 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

(335 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

(6 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

(12 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

(95 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

(8 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

(11 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

(2 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

(241 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

(5 entries)

---

Global Index

A

AccProof [definition, in MetaCoq.Induction.standardNested]
Acc_introᵗ [constructor, in MetaCoq.Induction.standardNested]
Accᵗ [inductive, in MetaCoq.Induction.standardNested]
addContainer [library]
addContainer [library]
addContainer_test2 [library]
addContrapos [definition, in MetaCoq.Induction.implication]
addContraposType [definition, in MetaCoq.Induction.implication]
addHelper [definition, in typing]
addInductiveHypothesis [definition, in typing]
addition [inductive, in MetaCoq.Induction.test]
addS [constructor, in MetaCoq.Induction.test]
addType [definition, in MetaCoq.Induction.addContainer]
addType [definition, in MetaCoq.Induction.addContainer]
addType [definition, in MetaCoq.Induction.addContainer_test2]
add0 [constructor, in MetaCoq.Induction.test]
All [constructor, in MetaCoq.Induction.nested_datatypes]
AllI [inductive, in MetaCoq.Induction.parametricity_test]
AllSpecial [lemma, in typing]
allVass [definition, in typing]
All_over_All [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
All_forall [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
All_cons [constructor, in MetaCoq.Induction.parametricity_test]
All_nil [constructor, in MetaCoq.Induction.parametricity_test]
All2 [inductive, in MetaCoq.Induction.addContainer_test2]
All2_cons [constructor, in MetaCoq.Induction.addContainer_test2]
All2_nil [constructor, in MetaCoq.Induction.addContainer_test2]
appCons [lemma, in typing]
appConsNilFront [lemma, in typing]
appInjLen [lemma, in typing]
appLen [lemma, in typing]
appOneNeqNil [lemma, in typing]
ascii_to_string [definition, in typing]
ascii_to_string [definition, in MetaCoq.Induction.de_bruijn_print]
assumption [projection, in MetaCoq.Induction.helperGen]
assumption [projection, in MetaCoq.Induction.helperGen_test]
assumptionType [projection, in MetaCoq.Induction.helperGen]
assumptionType [projection, in MetaCoq.Induction.helperGen_test]
augmentType [definition, in MetaCoq.Induction.addContainer]
augmentType [definition, in MetaCoq.Induction.addContainer]
augmentType [definition, in MetaCoq.Induction.addContainer_test2]
AuxLemma [section, in typing]

B

Basic [section, in typing]
betterInd [record, in MetaCoq.Induction.destruct_lemma]
bodyIndApp [lemma, in typing]
boolᵗ [inductive, in MetaCoq.Induction.standardNested]
boolᵗ [inductive, in MetaCoq.Induction.removeNonAug_test]
branchesHaveFittingTypes [lemma, in typing]
branchesHaveTypes [lemma, in typing]
branchTypes [definition, in typing]
branchTypesFit [lemma, in typing]
branchTypeTypes [lemma, in typing]
brtree [inductive, in MetaCoq.Induction.elpi_test]
bruijn_print [definition, in typing]
bruijn_print_aux [definition, in typing]
bruijn_print [definition, in MetaCoq.Induction.de_bruijn_print]
bruijn_print_aux [definition, in MetaCoq.Induction.de_bruijn_print]

C

canElim [definition, in MetaCoq.Induction.destruct_lemma]
canElim [definition, in typing]
caseEnvHasType [lemma, in typing]
changeMode [definition, in MetaCoq.Induction.Modes]
changeMode [definition, in MetaCoq.Induction.mode_test]
cleanInd [definition, in MetaCoq.Induction.removeNonAug_test]
cleanInd [definition, in MetaCoq.Induction.removeNonAug]
cleanIndTop [definition, in MetaCoq.Induction.removeNonAug_test]
cleanIndTop [definition, in MetaCoq.Induction.removeNonAug]
cleanOInd [definition, in MetaCoq.Induction.removeNonAug_test]
cleanOInd [definition, in MetaCoq.Induction.removeNonAug]
Cng [constructor, in MetaCoq.Induction.elpi_test]
Cog [constructor, in MetaCoq.Induction.elpi_test]
collectLambdaMapIsNotLambda [lemma, in typing]
collectLambdaMaxElim [lemma, in typing]
collectLambdaMkLambda [lemma, in typing]
collectLambdaProdDisjoint [lemma, in typing]
collectLift [lemma, in typing]
collectNoLambda [lemma, in typing]
collectNoProd [lemma, in typing]
collectProdLambdaDisjoint [lemma, in typing]
collectProdMaxElim [lemma, in typing]
collectProdMkProd [lemma, in typing]
collectProdMkProdGen [lemma, in typing]
collectProdVass [lemma, in typing]
collectReplace [lemma, in typing]
collect_prods [definition, in MetaCoq.Induction.non_uniform_test]
collect_prods [definition, in MetaCoq.Induction.non_uniform]
collect_lambdas [definition, in MetaCoq.Induction.destruct_lemma]
collect_prods [definition, in MetaCoq.Induction.destruct_lemma]
collect_prods2 [lemma, in typing]
collect_lambdas [definition, in typing]
collect_prods [definition, in typing]
computeContrapos [definition, in MetaCoq.Induction.implication]
concatString [definition, in typing]
concatString [definition, in MetaCoq.Induction.de_bruijn_print]
Cong [constructor, in MetaCoq.Induction.elpi_test]
Conj [constructor, in MetaCoq.Induction.nested_datatypes]
consistentInstanceExt [lemma, in typing]
consMin [lemma, in typing]
constrMapping [definition, in typing]
constructorList [library]
const2 [constructor, in MetaCoq.Induction.addContainer_test2]
consᵗ [constructor, in MetaCoq.Induction.standardNested]
consᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]
containerInd [inductive, in MetaCoq.Induction.nested_datatypes]
containerInd2 [inductive, in MetaCoq.Induction.nested_datatypes]
containerInd3 [inductive, in MetaCoq.Induction.nested_datatypes]
containerInd4 [inductive, in MetaCoq.Induction.nested_datatypes]
containerInd4Inst [instance, in MetaCoq.Induction.standardNested]
containerInd4Proof [definition, in MetaCoq.Induction.standardNested]
containerInd4ᵗ [inductive, in MetaCoq.Induction.standardNested]
countLeb [lemma, in typing]
countMax [lemma, in typing]
countOfCtor [definition, in MetaCoq.Induction.non_uniform_test]
countOfCtor [definition, in MetaCoq.Induction.non_uniform]
countOfCtor [definition, in typing]
count_prods [definition, in MetaCoq.Induction.non_uniform_test]
count_prods [definition, in MetaCoq.Induction.non_uniform]
count_prods [definition, in MetaCoq.Induction.destruct_lemma]
count_prods [definition, in typing]
create [definition, in MetaCoq.Induction.destruct_lemma]
create [definition, in typing]
createAppChain [definition, in MetaCoq.Induction.destruct_lemma]
createAppChain [definition, in typing]
createAppChainOff [definition, in MetaCoq.Induction.destruct_lemma]
createAppChainOff [definition, in typing]
createElim [definition, in MetaCoq.Induction.destruct_lemma]
createElim [definition, in typing]
createElimType [definition, in typing]
createFunction [definition, in MetaCoq.Induction.helperGen]
createFunction [definition, in MetaCoq.Induction.helperGen_test]
createFunction [definition, in MetaCoq.Induction.show]
createReturnNone [lemma, in typing]
createShow [definition, in MetaCoq.Induction.show]
createShowFunc [definition, in MetaCoq.Induction.show]
createSome [lemma, in typing]
cshapeArgsVass [lemma, in typing]
cshapeTypingList [lemma, in typing]
Ct0 [constructor, in MetaCoq.Induction.test]
cumul_eta_r [lemma, in typing]
CustomFunction [section, in typing]
C_I [constructor, in MetaCoq.Induction.elpi_test]
c10 [constructor, in MetaCoq.Induction.nested_datatypes]
c12 [constructor, in MetaCoq.Induction.nested_datatypes]
c20 [constructor, in MetaCoq.Induction.nested_datatypes]
c3 [constructor, in MetaCoq.Induction.nested_datatypes]
c4 [constructor, in MetaCoq.Induction.nested_datatypes]
c4ᵗ [constructor, in MetaCoq.Induction.standardNested]

D

deep [inductive, in MetaCoq.Induction.elpi_test]
defAssumption [definition, in MetaCoq.Induction.standardNested]
defInst [instance, in MetaCoq.Induction.standardNested]
defProof [definition, in MetaCoq.Induction.standardNested]
deLift01 [definition, in MetaCoq.Induction.removeNonAug_test]
deLift01 [definition, in MetaCoq.Induction.removeNonAug]
dep [inductive, in MetaCoq.Induction.non_uniform_test]
dep [inductive, in MetaCoq.Induction.test]
dep0 [constructor, in MetaCoq.Induction.non_uniform_test]
dep0 [constructor, in MetaCoq.Induction.test]
deriveShowType [definition, in MetaCoq.Induction.show]
destAritySimpl [lemma, in typing]
destruct_lemma [library]
de_bruijn_print [library]
diffIndBody [lemma, in typing]
Disj [constructor, in MetaCoq.Induction.nested_datatypes]
double [inductive, in MetaCoq.Induction.test]
dS [constructor, in MetaCoq.Induction.test]
d0 [constructor, in MetaCoq.Induction.test]

E

elpi_test [library]
Enat [definition, in MetaCoq.Induction.test]
eqIsEq [lemma, in MetaCoq.Induction.test]
eqT [inductive, in MetaCoq.Induction.test]
eq_term_upto_univ_refl [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
errorMessage [definition, in MetaCoq.Induction.helperGen]
errorMessage [definition, in MetaCoq.Induction.helperGen_test]
etaConvRetType3 [lemma, in typing]
etaConvType [lemma, in typing]
etaConvTypeGen [lemma, in typing]
etaConvTypeInv [lemma, in typing]
Ex [constructor, in MetaCoq.Induction.nested_datatypes]
extendList [definition, in MetaCoq.Induction.show]
extendName [definition, in MetaCoq.Induction.destruct_lemma]
extendOnConstructors [lemma, in typing]
extractFunction [definition, in MetaCoq.Induction.helperGen]
extractFunction [definition, in MetaCoq.Induction.helperGen_test]
extractOption [lemma, in typing]

F

F [definition, in MetaCoq.Induction.standardNested]
Fal [constructor, in MetaCoq.Induction.nested_datatypes]
falseᵗ [constructor, in MetaCoq.Induction.standardNested]
falseᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]
filteri [definition, in typing]
findRec [definition, in MetaCoq.Induction.helperGen]
findRec [definition, in MetaCoq.Induction.helperGen_test]
findRecInd [definition, in MetaCoq.Induction.helperGen]
findRecInd [definition, in MetaCoq.Induction.helperGen_test]
findRel [definition, in MetaCoq.Induction.destruct_lemma]
findRel [definition, in typing]
fixEnvWf [lemma, in typing]
fixGuardAxiom [lemma, in typing]
fixTypeTypes [lemma, in typing]
foldLiftSubstIndices [lemma, in typing]
foldLiftSubstIndices3 [lemma, in typing]
foldMkLambda [lemma, in typing]
foldMkLambdaUnfold [lemma, in typing]
foldMkProd [lemma, in typing]
foldMkProdLetIn [lemma, in typing]
foldMkProdUnfold [lemma, in typing]
fold_right_sum_leq [lemma, in MetaCoq.Induction.destruct_lemma]
fold_right_map [lemma, in MetaCoq.Induction.destruct_lemma]
fold_right_min [lemma, in typing]
form [inductive, in MetaCoq.Induction.nested_datatypes]
foterm [inductive, in MetaCoq.Induction.nested_datatypes]
foterm_induct [definition, in MetaCoq.Induction.rose_ind_test]
Func [constructor, in MetaCoq.Induction.nested_datatypes]
Funcs [axiom, in MetaCoq.Induction.nested_datatypes]
Functions [section, in typing]
fun_ar [axiom, in MetaCoq.Induction.nested_datatypes]

G

G [inductive, in MetaCoq.Induction.non_uniform_test]
G [inductive, in MetaCoq.Induction.test]
G [inductive, in MetaCoq.Induction.parametricity_test]
generateInductiveAssumptions [definition, in MetaCoq.Induction.destruct_lemma]
generatePCall2 [definition, in MetaCoq.Induction.destruct_lemma]
getConstructName [definition, in typing]
getConstructName [definition, in MetaCoq.Induction.de_bruijn_print]
getCtors [definition, in MetaCoq.Induction.constructorList]
getCtorsSimpl [definition, in MetaCoq.Induction.constructorList]
getInd [definition, in MetaCoq.Induction.helperGen]
getInd [definition, in MetaCoq.Induction.helperGen_test]
getIndProp [definition, in MetaCoq.Induction.addContainer]
getIndProp [definition, in MetaCoq.Induction.addContainer]
getIndProp [definition, in MetaCoq.Induction.addContainer_test2]
getInds [definition, in MetaCoq.Induction.helperGen]
getInds [definition, in MetaCoq.Induction.helperGen_test]
getInductiveCalls [definition, in typing]
getInductiveName [definition, in typing]
getInductiveName [definition, in MetaCoq.Induction.de_bruijn_print]
getInner [definition, in MetaCoq.Induction.destruct_lemma]
getKelim [lemma, in typing]
getMaxElim [definition, in MetaCoq.Induction.destruct_lemma]
getMaxElim [definition, in typing]
getMaxElimSort [lemma, in typing]
getMinChain [definition, in MetaCoq.Induction.non_uniform_test]
getMinChain [definition, in MetaCoq.Induction.non_uniform]
getMinChain [definition, in typing]
getMode [definition, in MetaCoq.Induction.Modes]
getMode [definition, in MetaCoq.Induction.mode_test]
getName [definition, in MetaCoq.Induction.Modes]
getName [definition, in MetaCoq.Induction.MetaCoqInductionPrinciples]
getName [definition, in typing]
getName [definition, in MetaCoq.Induction.mode_test]
getOndIndBody [lemma, in typing]
getP [definition, in MetaCoq.Induction.non_uniform_test]
getP [definition, in MetaCoq.Induction.non_uniform]
getP [definition, in typing]
getParamCount [definition, in MetaCoq.Induction.non_uniform_test]
getParamCount [definition, in MetaCoq.Induction.non_uniform]
getParamCount [definition, in typing]
getParamCountBound [lemma, in typing]
getPCount [definition, in MetaCoq.Induction.non_uniform_test]
getPCount [definition, in MetaCoq.Induction.non_uniform]
getPCount [definition, in typing]
GI [constructor, in MetaCoq.Induction.non_uniform_test]
GI [constructor, in MetaCoq.Induction.test]
GI [constructor, in MetaCoq.Induction.parametricity_test]
G2 [inductive, in MetaCoq.Induction.non_uniform_test]
G2 [inductive, in MetaCoq.Induction.test]
G2I1 [constructor, in MetaCoq.Induction.non_uniform_test]
G2I1 [constructor, in MetaCoq.Induction.test]
G2I2 [constructor, in MetaCoq.Induction.non_uniform_test]
G2I2 [constructor, in MetaCoq.Induction.test]
G3 [inductive, in MetaCoq.Induction.non_uniform_test]
G3 [inductive, in MetaCoq.Induction.test]
G3I [constructor, in MetaCoq.Induction.non_uniform_test]
G3I [constructor, in MetaCoq.Induction.test]
G4 [inductive, in MetaCoq.Induction.test]
G4I [constructor, in MetaCoq.Induction.test]
G5 [inductive, in MetaCoq.Induction.test]
G5I [constructor, in MetaCoq.Induction.test]

H

H [definition, in MetaCoq.Induction.implication]
H [constructor, in MetaCoq.Induction.elpi_test]
hasSat [definition, in MetaCoq.Induction.destruct_lemma]
hasSat [definition, in typing]
helperGen [library]
helperGen_test [library]
H2 [axiom, in MetaCoq.Induction.implication]
H3 [definition, in MetaCoq.Induction.implication]

I

id [definition, in MetaCoq.Induction.destruct_lemma]
id [definition, in typing]
Idx [inductive, in MetaCoq.Induction.elpi_test]
Impl [constructor, in MetaCoq.Induction.nested_datatypes]
implication [library]
indAppType [lemma, in typing]
indC0 [constructor, in MetaCoq.Induction.test]
indexIndTest [inductive, in MetaCoq.Induction.test]
indicesType [lemma, in typing]
indicesVass [lemma, in typing]
indParamVass [lemma, in typing]
indTest [inductive, in MetaCoq.Induction.test]
inj_sur [lemma, in MetaCoq.Induction.trans_inj_sur]
instantiateParams [lemma, in typing]
instantiateParams3 [lemma, in typing]
instParamsSubstSimpl [lemma, in typing]
interactive [library]
invert_type_App [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
inv_opt_monad [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
in_mapi [lemma, in typing]
in_app_or [lemma, in typing]
isAugmentable [definition, in MetaCoq.Induction.helperGen]
isAugmentable [definition, in MetaCoq.Induction.helperGen_test]
isAugmentable [definition, in MetaCoq.Induction.removeNonAug_test]
isAugmentable [definition, in MetaCoq.Induction.removeNonAug]
isLambdaInv [lemma, in typing]
isLetIn [definition, in typing]
isProd [definition, in MetaCoq.Induction.destruct_lemma]
isProd [definition, in typing]
isProdInv [lemma, in typing]
is_Node [constructor, in MetaCoq.Induction.standardNested]
is_Leaf [constructor, in MetaCoq.Induction.standardNested]
is_rtree [inductive, in MetaCoq.Induction.standardNested]
is_consV [constructor, in MetaCoq.Induction.standardNested]
is_nilV [constructor, in MetaCoq.Induction.standardNested]
is_vec [inductive, in MetaCoq.Induction.standardNested]
is_pair [constructor, in MetaCoq.Induction.standardNested]
is_prod [inductive, in MetaCoq.Induction.standardNested]
is_list_in [lemma, in MetaCoq.Induction.standardNested]
is_cons [constructor, in MetaCoq.Induction.standardNested]
is_nil [constructor, in MetaCoq.Induction.standardNested]
is_list [inductive, in MetaCoq.Induction.standardNested]
itMkProdInj [lemma, in typing]
itMkProdNeq [lemma, in typing]
it_mkProd_inv [lemma, in typing]

J

join [definition, in typing]
join [definition, in MetaCoq.Induction.de_bruijn_print]

L

Leaf [constructor, in MetaCoq.Induction.nested_datatypes]
Leaf [constructor, in MetaCoq.Induction.elpi_test]
LeafProp [constructor, in MetaCoq.Induction.parametricity_test]
leElimTyping [lemma, in typing]
LeLemma [section, in typing]
LeLemma.Hind [variable, in typing]
LeLemma.Hmind [variable, in typing]
LeLemma.Hwf [variable, in typing]
LeLemma.Γ [variable, in typing]
LeLemma.Σ [variable, in typing]
lengthAppend [lemma, in typing]
leq_term_refl [lemma, in typing]
leq_term_refl [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
le_elim [lemma, in typing]
liftAdd [lemma, in typing]
liftCollectProd [lemma, in typing]
liftContextSucc [lemma, in typing]
liftContextSum [lemma, in typing]
liftIndicesVass [lemma, in typing]
liftIndIndices [lemma, in typing]
liftIndParams [lemma, in typing]
liftIndType [lemma, in typing]
liftingInVass [lemma, in typing]
liftInstIndices [lemma, in typing]
LiftIsProd [lemma, in typing]
liftMaxElim [lemma, in typing]
liftMkRel [lemma, in typing]
liftReplaceLastProd [lemma, in typing]
liftSubstInstanceConstr [lemma, in typing]
liftSubstInstanceConstrGen [lemma, in typing]
liftSubstInstanceConstr2 [lemma, in typing]
lifttInd [lemma, in typing]
liftUnderReplaceLambda [lemma, in typing]
lift_wf_local_rel [lemma, in typing]
lift_it_mkProd_or_LetIn [lemma, in typing]
lift_it_mkLambda_or_LetIn [lemma, in typing]
lift_context_len [lemma, in typing]
lift01 [definition, in MetaCoq.Induction.show]
linebreak [definition, in typing]
linebreak [definition, in MetaCoq.Induction.de_bruijn_print]
listAssumption [definition, in MetaCoq.Induction.standardNested]
listAssumption2 [definition, in MetaCoq.Induction.standardNested]
listCtors [definition, in MetaCoq.Induction.constructorList]
listInst [instance, in MetaCoq.Induction.standardNested]
listProof [definition, in MetaCoq.Induction.standardNested]
listProof2 [definition, in MetaCoq.Induction.standardNested]
listᵗ [inductive, in MetaCoq.Induction.standardNested]
listᵗ [inductive, in MetaCoq.Induction.removeNonAug_test]
lt_plus_S_r [lemma, in MetaCoq.Induction.destruct_lemma]
lt_plus_S_l [lemma, in MetaCoq.Induction.destruct_lemma]

M

MainSec [section, in typing]
MainSec.caseBodySec [section, in typing]
MainSec.caseBodySec.caseBody [variable, in typing]
MainSec.caseBodySec.HeqcaseBody [variable, in typing]
MainSec.declI [variable, in typing]
MainSec.declM [variable, in typing]
MainSec.findBody [variable, in typing]
MainSec.Hwf [variable, in typing]
MainSec.ind [variable, in typing]
MainSec.ind_sorts [variable, in typing]
MainSec.ind_ctors_sort [variable, in typing]
MainSec.ind_arity_eq [variable, in typing]
MainSec.ind_sort [variable, in typing]
MainSec.ind_indices [variable, in typing]
MainSec.ind_body [variable, in typing]
MainSec.matchSec [section, in typing]
MainSec.matchSec.Env [variable, in typing]
MainSec.matchSec.HeqEnv [variable, in typing]
MainSec.matchSec.HeqmatchObj [variable, in typing]
MainSec.matchSec.HeqmatchType [variable, in typing]
MainSec.matchSec.HeqretType [variable, in typing]
MainSec.matchSec.matchObj [variable, in typing]
MainSec.matchSec.matchType [variable, in typing]
MainSec.matchSec.retType [variable, in typing]
MainSec.mind_body [variable, in typing]
MainSec.nameF [variable, in typing]
MainSec.nparCount [variable, in typing]
MainSec.onArity [variable, in typing]
MainSec.onConstructors [variable, in typing]
MainSec.onGuard [variable, in typing]
MainSec.onInd [variable, in typing]
MainSec.onIndB [variable, in typing]
MainSec.onInductives [variable, in typing]
MainSec.onNpars [variable, in typing]
MainSec.onParams [variable, in typing]
MainSec.onProjections [variable, in typing]
MainSec.uniP [variable, in typing]
MainSec.univ [variable, in typing]
MainSec.Γ [variable, in typing]
MainSec.Σ [variable, in typing]
Main2 [lemma, in typing]
mapAgreement [lemma, in typing]
mapDeclNested [lemma, in typing]
mapDeclVass [lemma, in typing]
mapExt [lemma, in typing]
mapId [lemma, in typing]
mapiExt [lemma, in typing]
mapiLiftContext [lemma, in typing]
mapiNatRec [lemma, in typing]
mapiNatRecGen [lemma, in typing]
mapiNested [lemma, in typing]
mapiRecNested [lemma, in typing]
mapIsProdLam [lemma, in typing]
mapiSub [lemma, in typing]
mapi_rec_len [lemma, in typing]
mapLen [lemma, in typing]
mapMk [lemma, in typing]
mapOne [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
mapOptionOutApp [lemma, in typing]
mapParamIndRelEq [lemma, in typing]
mapParamIndRelEq3 [lemma, in typing]
mapProdNoProd [lemma, in typing]
mapProdToLambda [definition, in MetaCoq.Induction.destruct_lemma]
mapProdToLambda [definition, in typing]
mapProdToLambdaItMkProd [lemma, in typing]
mapProdToLambda2 [definition, in typing]
mapSndAdd0 [lemma, in typing]
mapTypeErase [lemma, in typing]
mapTypeEraseAux [lemma, in typing]
map_context_lifting [definition, in MetaCoq.Induction.show]
matchElimLower [lemma, in typing]
matchObjTyping [lemma, in typing]
matchOnMkApps [lemma, in typing]
matchTypeHasType [lemma, in typing]
matchTypeHasType' [lemma, in typing]
matchTypeSimpl [lemma, in typing]
matchTypeType [definition, in typing]
matchTypeTypeFit [lemma, in typing]
maxElimSort [variable, in typing]
maxElimType [lemma, in typing]
MetaCoqInductionPrinciples [library]
MetaCoqTheorem [section, in typing]
mfixpointAssumption [definition, in MetaCoq.Induction.standardNested]
mfixpointInst [instance, in MetaCoq.Induction.standardNested]
mfixpointProof [definition, in MetaCoq.Induction.standardNested]
minChainMax [lemma, in typing]
minChainMin [lemma, in typing]
mkAppMkApps [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
mkAppNoLambda [lemma, in typing]
mkAppsExt [lemma, in typing]
mkAppsTApp [lemma, in typing]
mkLambdaCollect [lemma, in typing]
mkRel [definition, in typing]
mkRelApp [lemma, in typing]
mkRelNum [definition, in MetaCoq.Induction.destruct_lemma]
mode [record, in MetaCoq.Induction.Modes]
mode [record, in MetaCoq.Induction.mode_test]
Modes [library]
mode_test [library]
mP [constructor, in MetaCoq.Induction.test]
mutParam [inductive, in MetaCoq.Induction.test]

N

nameAppend [definition, in MetaCoq.Induction.addContainer]
nameAppend [definition, in MetaCoq.Induction.addContainer]
nameAppend [definition, in MetaCoq.Induction.addContainer_test2]
nameEq [lemma, in typing]
nameToString [definition, in typing]
nameToString [definition, in MetaCoq.Induction.de_bruijn_print]
name_of [abbreviation, in MetaCoq.Induction.MetaCoqInductionPrinciples]
name_of [abbreviation, in typing]
namingEq2 [axiom, in typing]
natCtors [definition, in MetaCoq.Induction.constructorList]
natRecAppGen [lemma, in typing]
natRecExt [lemma, in typing]
natToChar [definition, in typing]
natToChar [definition, in MetaCoq.Induction.de_bruijn_print]
natToString [definition, in typing]
natToString [definition, in MetaCoq.Induction.de_bruijn_print]
natᵗ [inductive, in MetaCoq.Induction.standardNested]
natᵗ [inductive, in MetaCoq.Induction.removeNonAug_test]
nested [library]
nestedMode [definition, in MetaCoq.Induction.helperGen]
nestedMode [definition, in MetaCoq.Induction.helperGen_test]
nested_datatypes [library]
nestGuard [inductive, in MetaCoq.Induction.elpi_test]
nilt2 [constructor, in MetaCoq.Induction.addContainer_test2]
nilᵗ [constructor, in MetaCoq.Induction.standardNested]
nilᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]
Node [constructor, in MetaCoq.Induction.nested_datatypes]
Node [constructor, in MetaCoq.Induction.elpi_test]
NodeProp [constructor, in MetaCoq.Induction.parametricity_test]
node3 [constructor, in MetaCoq.Induction.nested_datatypes]
noLambdaMaxElim [lemma, in typing]
nonAugInd [definition, in MetaCoq.Induction.removeNonAug_test]
nonAugInd [definition, in MetaCoq.Induction.removeNonAug]
nonUniCount [lemma, in typing]
non_uniform [library]
non_uniform_test [library]
noProdMaxElim [lemma, in typing]
nthInds [lemma, in typing]

O

onConstructorIndBodyNotMatter [lemma, in typing]
onContextInv [lemma, in typing]
onIndDeclInd [lemma, in typing]
onIndMutInd [lemma, in typing]
onIndNth [lemma, in typing]
onSndId [lemma, in typing]
on_fst [definition, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
optionMapNested [lemma, in typing]
optMonadEq [lemma, in typing]
optMonadEq2 [lemma, in typing]
outerGuard [inductive, in MetaCoq.Induction.elpi_test]
outNestGuard [inductive, in MetaCoq.Induction.elpi_test]
Oᵗ [constructor, in MetaCoq.Induction.standardNested]
Oᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]

P

P [module, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
pAppliedIndType [lemma, in typing]
pAppliedIndType' [lemma, in typing]
parametricity_test_2 [library]
parametricity_test [library]
PCUICToTemplate [library]
PCUICToTemplateCorrectness [library]
pfree [inductive, in MetaCoq.Induction.test]
PICUICTheory [section, in typing]
PL [module, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
pointLessIf [lemma, in typing]
Pred [constructor, in MetaCoq.Induction.nested_datatypes]
Preds [axiom, in MetaCoq.Induction.nested_datatypes]
pred_ar [axiom, in MetaCoq.Induction.nested_datatypes]
pretty [definition, in MetaCoq.Induction.show]
principle [projection, in MetaCoq.Induction.destruct_lemma]
principleType [projection, in MetaCoq.Induction.destruct_lemma]
printer [definition, in MetaCoq.Induction.interactive]
prodAssumption [definition, in MetaCoq.Induction.standardNested]
prodInst [instance, in MetaCoq.Induction.standardNested]
prodProof [definition, in MetaCoq.Induction.standardNested]
prodProof2 [definition, in MetaCoq.Induction.standardNested]
proof [projection, in MetaCoq.Induction.helperGen]
proof [projection, in MetaCoq.Induction.helperGen_test]
proofType [projection, in MetaCoq.Induction.helperGen]
proofType [projection, in MetaCoq.Induction.helperGen_test]
PT [module, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
pType [lemma, in typing]
p0 [constructor, in MetaCoq.Induction.test]
p1 [constructor, in MetaCoq.Induction.test]
p2 [constructor, in MetaCoq.Induction.test]
p3 [constructor, in MetaCoq.Induction.test]
p4 [constructor, in MetaCoq.Induction.test]

Q

Qcon [constructor, in MetaCoq.Induction.test]
quantifyCases [definition, in MetaCoq.Induction.destruct_lemma]
quantifyCases [definition, in typing]
quantifyCasesLen [lemma, in typing]
quantifyCasesType [lemma, in typing]

R

registered [record, in MetaCoq.Induction.helperGen]
registered [record, in MetaCoq.Induction.helperGen_test]
relnMkRel [lemma, in typing]
removeArgList [definition, in MetaCoq.Induction.removeNonAug_test]
removeArgList [definition, in MetaCoq.Induction.removeNonAug]
removeArityCount [lemma, in typing]
removeArityProdCount [lemma, in typing]
removeArityProds [lemma, in typing]
removeArityProds2 [lemma, in typing]
removeElements [definition, in MetaCoq.Induction.removeNonAug_test]
removeElements [definition, in MetaCoq.Induction.removeNonAug]
removeMkProd [lemma, in typing]
removeNonAug [library]
removeNonAugList [definition, in MetaCoq.Induction.removeNonAug_test]
removeNonAugList [definition, in MetaCoq.Induction.removeNonAug]
removeNonAugmentable [definition, in MetaCoq.Induction.removeNonAug_test]
removeNonAugmentable [definition, in MetaCoq.Induction.removeNonAug]
removeNonAug_test [library]
removeProdMaxElim [lemma, in typing]
removeReplaceProd [lemma, in typing]
remove_prods [definition, in typing]
remove_lambdas [definition, in typing]
replaceLambdaMaxElim [lemma, in typing]
replaceLastLambda [definition, in MetaCoq.Induction.destruct_lemma]
replaceLastLambda [definition, in typing]
replaceLastLambdaNoLambda [lemma, in typing]
replaceLastLambdaSelf [lemma, in typing]
replaceLastLambda' [definition, in MetaCoq.Induction.destruct_lemma]
replaceLastLambda' [definition, in typing]
replaceLastOffset [definition, in typing]
replaceLastOffsetAll [lemma, in typing]
replaceLastProd [definition, in MetaCoq.Induction.destruct_lemma]
replaceLastProd [definition, in typing]
replaceLastProdNotProd [lemma, in typing]
replaceLastProdReplaceLastProd [lemma, in typing]
replaceLastProdSelf [lemma, in typing]
replaceLastProd' [definition, in MetaCoq.Induction.destruct_lemma]
replaceLastProd' [definition, in typing]
replaceLastTypeLambda [lemma, in typing]
replaceLastTypeLambdaItLam [lemma, in typing]
replaceLastTypeProd [lemma, in typing]
replaceMap [lemma, in typing]
replaceOffsetUnderItProd [lemma, in typing]
replaceOneProd [lemma, in typing]
replaceProdMaxElim [lemma, in typing]
replaceUnderItMkLambda [lemma, in typing]
replaceUnderItMkProd [lemma, in typing]
replaceUnderLambda [lemma, in typing]
replaceUnderOneLambda [lemma, in typing]
retTypeLifting [lemma, in typing]
revCollect [lemma, in typing]
revInj [lemma, in typing]
revLen [lemma, in typing]
revRev [lemma, in typing]
rev_elim [lemma, in typing]
rewriteCaseEnv [lemma, in typing]
rewriteCaseEnvType [lemma, in typing]
RLLambdaIsLambdaInner [lemma, in typing]
RLLambdaIsLambdaOuter [lemma, in typing]
RLProdIsProd [lemma, in typing]
roseTree [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeDN1 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeDN2 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeDN3 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeDN4 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeDN5 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeDN6 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeDN7 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeNN1 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeNN2 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeNN3 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeNN4 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeNN5 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeNN6 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeNN7 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO1 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO10 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO11 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO13 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO2 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO3 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO3P [inductive, in MetaCoq.Induction.parametricity_test]
roseTreeO3_ind_MC [definition, in MetaCoq.Induction.standardNested]
roseTreeO3ᵗ [inductive, in MetaCoq.Induction.standardNested]
roseTreeO4 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO5 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO6 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO7 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO8 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreeO9 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI1 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI2 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI3 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI4 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI5 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI6 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI7 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI8 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTreePI8 [inductive, in MetaCoq.Induction.non_uniform_test]
roseTree2 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTree3 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTree4 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTree5 [inductive, in MetaCoq.Induction.nested_datatypes]
roseTree6 [inductive, in MetaCoq.Induction.nested_datatypes]
rose_ind_test [library]
rtree [inductive, in MetaCoq.Induction.nested_datatypes]
rtreeInst [instance, in MetaCoq.Induction.standardNested]
rtreeO3Proof [definition, in MetaCoq.Induction.standardNested]
rtreeProof [definition, in MetaCoq.Induction.standardNested]
rtreeProof2 [definition, in MetaCoq.Induction.standardNested]
rtreeProp [inductive, in MetaCoq.Induction.parametricity_test]
rtree_ind_MC_Test [definition, in MetaCoq.Induction.standardNested]
runElim [definition, in MetaCoq.Induction.destruct_lemma]
runElim [definition, in typing]
runShow [definition, in MetaCoq.Induction.show]

S

show [library]
showFunction [definition, in MetaCoq.Induction.show]
simplLiftContext [lemma, in typing]
size_induction [lemma, in MetaCoq.Induction.destruct_lemma]
skipnApp [lemma, in typing]
standardNested [library]
state [projection, in MetaCoq.Induction.Modes]
state [projection, in MetaCoq.Induction.mode_test]
stringQ [definition, in MetaCoq.Induction.show]
substAdd [definition, in typing]
substApp [definition, in typing]
substContextSubstInstParamVass [lemma, in typing]
substInstanceConstrIndices [lemma, in typing]
substInstanceConstrMkProd [lemma, in typing]
substInstanceConstrParam [lemma, in typing]
substInstanceContextLen [lemma, in typing]
substInstParamVass [lemma, in typing]
substNoApp [lemma, in typing]
subst_it_mkLambda_or_LetIn [lemma, in typing]
subst_it_mkProd_or_LetIn [lemma, in typing]
subst_context_len [lemma, in typing]
succLen [lemma, in typing]
Sᵗ [constructor, in MetaCoq.Induction.standardNested]
Sᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]

T

T [module, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
template_to_pcuic [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
termNegType [definition, in MetaCoq.Induction.implication]
termsize [definition, in MetaCoq.Induction.destruct_lemma]
termSizeLifting [lemma, in MetaCoq.Induction.destruct_lemma]
term_size_ind [definition, in MetaCoq.Induction.destruct_lemma]
test [library]
testInd [definition, in MetaCoq.Induction.helperGen_test]
TL [module, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
Tmp [section, in typing]
toExtendedListLen [lemma, in typing]
toExtendedListLenNoBody [lemma, in typing]
Top [constructor, in MetaCoq.Induction.nested_datatypes]
trans [definition, in MetaCoq.Induction.destruct_lemma]
trans [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans [definition, in MetaCoq.Induction.show]
trans_mfix_All2 [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mfix_All [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_branches [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_wf_local_env [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_wf_local' [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_fix_context [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_build_case_predicate_type [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_it_mkProd_or_LetIn [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mkProd_or_LetIn [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_destr_arity [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_instantiate_params' [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_instantiate_params [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_declared_projection [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_dbody [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_dtype [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_type_of_constructor [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_ind_type [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_cst_type [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_subst_instance_constr [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_subst10 [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_subst [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_decl_type [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mkApps [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_declared_inductive [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_consistent_instance_ext [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_constraintSet_in [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_declared_constant [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_lookup [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_in_level_set [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mem_level_set [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_global_ext_levels [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_def [definition, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_lift [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_global [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_global_decls [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_global_decl [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_minductive_body [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_constant_body [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_one_ind_body [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_ctor [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_local [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_decl [definition, in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_inj_sur [library]
tree [constructor, in MetaCoq.Induction.nested_datatypes]
treeDN1 [constructor, in MetaCoq.Induction.nested_datatypes]
treeDN2 [constructor, in MetaCoq.Induction.nested_datatypes]
treeDN3 [constructor, in MetaCoq.Induction.nested_datatypes]
treeDN4 [constructor, in MetaCoq.Induction.nested_datatypes]
treeDN5 [constructor, in MetaCoq.Induction.nested_datatypes]
treeDN6 [constructor, in MetaCoq.Induction.nested_datatypes]
treeDN7 [constructor, in MetaCoq.Induction.nested_datatypes]
treeNN1 [constructor, in MetaCoq.Induction.nested_datatypes]
treeNN2 [constructor, in MetaCoq.Induction.nested_datatypes]
treeNN3 [constructor, in MetaCoq.Induction.nested_datatypes]
treeNN4 [constructor, in MetaCoq.Induction.nested_datatypes]
treeNN5 [constructor, in MetaCoq.Induction.nested_datatypes]
treeNN6 [constructor, in MetaCoq.Induction.nested_datatypes]
treeNN7 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO1 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO10 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO11 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO13 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO2 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO3 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO3P [constructor, in MetaCoq.Induction.parametricity_test]
treeO3ᵗ [constructor, in MetaCoq.Induction.standardNested]
treeO4 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO5 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO6 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO7 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO8 [constructor, in MetaCoq.Induction.nested_datatypes]
treeO9 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI1 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI2 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI3 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI4 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI5 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI6 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI7 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI8 [constructor, in MetaCoq.Induction.nested_datatypes]
treePI8 [constructor, in MetaCoq.Induction.non_uniform_test]
tree2 [constructor, in MetaCoq.Induction.nested_datatypes]
tree3 [constructor, in MetaCoq.Induction.nested_datatypes]
tree4 [constructor, in MetaCoq.Induction.nested_datatypes]
tree5 [constructor, in MetaCoq.Induction.nested_datatypes]
tree6 [constructor, in MetaCoq.Induction.nested_datatypes]
trivialPred [definition, in MetaCoq.Induction.destruct_lemma]
trivialProof [definition, in MetaCoq.Induction.destruct_lemma]
trueᵗ [constructor, in MetaCoq.Induction.standardNested]
trueᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]
tr1 [definition, in MetaCoq.Induction.destruct_lemma]
tr2 [definition, in MetaCoq.Induction.destruct_lemma]
TT [module, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
typeBranch [lemma, in typing]
typeCons [constructor, in typing]
typeF [lemma, in typing]
typeIndAppIndices [lemma, in typing]
typeLiftLiftApplication [lemma, in typing]
typeNat [lemma, in typing]
typeNil [constructor, in typing]
typeParamsP [lemma, in typing]
typeSnoc [lemma, in typing]
typeSnocInv [lemma, in typing]
typetInd [lemma, in typing]
type_LambdaR [lemma, in typing]
type_LambdaL [lemma, in typing]
type_Rel2 [lemma, in typing]
type_it_mkProd_or_LetIn [lemma, in typing]
type_Lambda2 [lemma, in typing]
type_it_mkLambda_or_LetIn [lemma, in typing]
type_mkApp [lemma, in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
typing [library]
typingApp [lemma, in typing]
typingF [lemma, in typing]
typingLiftAppChain [lemma, in typing]
typingList [inductive, in typing]
typingListIndices [lemma, in typing]
typingListIndices2 [lemma, in typing]
typingListOffset [lemma, in typing]
typingParamInd [lemma, in typing]
typingSpineIndices [lemma, in typing]
typingSpineIndices' [lemma, in typing]
typingSpineIndices2 [lemma, in typing]
typingSpineInstInstf [lemma, in typing]
typingSpineInstInstf' [lemma, in typing]
typingSpineLifting [lemma, in typing]
typingSpineParamIndexRel [lemma, in typing]
typingSpineParamIndexRelLiftet [lemma, in typing]
typingSpineProdApp [lemma, in typing]
typingSpineReflexive [instance, in typing]
t1 [definition, in MetaCoq.Induction.non_uniform_test]
t2 [definition, in MetaCoq.Induction.non_uniform_test]
t2 [inductive, in MetaCoq.Induction.addContainer_test2]

U

Unnamed_thm1 [definition, in MetaCoq.Induction.rose_ind_test]
Unnamed_thm0 [definition, in MetaCoq.Induction.rose_ind_test]
Unnamed_thm [definition, in MetaCoq.Induction.rose_ind_test]

V

var_foterm [constructor, in MetaCoq.Induction.nested_datatypes]
vassCons [lemma, in typing]
vassSubstContext [lemma, in typing]
vec [definition, in MetaCoq.Induction.standardNested]
vec [inductive, in MetaCoq.Induction.parametricity_test]
vec [definition, in MetaCoq.Induction.removeNonAug_test]
veccons [constructor, in MetaCoq.Induction.parametricity_test]
vecconsᵗ [constructor, in MetaCoq.Induction.standardNested]
vecconsᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]
vecconsᵗ' [constructor, in MetaCoq.Induction.standardNested]
vecInst [instance, in MetaCoq.Induction.standardNested]
vecnil [constructor, in MetaCoq.Induction.parametricity_test]
vecnilᵗ [constructor, in MetaCoq.Induction.standardNested]
vecnilᵗ [constructor, in MetaCoq.Induction.removeNonAug_test]
vecnilᵗ' [constructor, in MetaCoq.Induction.standardNested]
vecProof [definition, in MetaCoq.Induction.standardNested]
vecProof2 [definition, in MetaCoq.Induction.standardNested]
vecProof2' [definition, in MetaCoq.Induction.standardNested]
vecᵗ [inductive, in MetaCoq.Induction.standardNested]
vecᵗ [inductive, in MetaCoq.Induction.removeNonAug_test]
vecᵗ' [inductive, in MetaCoq.Induction.standardNested]
vt1 [definition, in MetaCoq.Induction.non_uniform_test]
vt2 [definition, in MetaCoq.Induction.non_uniform_test]

W

weakeningWfLocalRel [lemma, in typing]
wfLocalBaseCase [lemma, in typing]
wfLocalBaseCaseSndArgs [lemma, in typing]
wfLocalCaseEnvEnv [lemma, in typing]
wfLocalCases [lemma, in typing]
wfLocalEnv [lemma, in typing]
wfLocalF [lemma, in typing]
wfLocalFixContext [lemma, in typing]
wfLocalFixEnv [lemma, in typing]
wfLocalFmInst [lemma, in typing]
wfLocalFmInstmInst [lemma, in typing]
wfLocalFmInstmInstmInst [lemma, in typing]
wfLocalIndicesMin [lemma, in typing]
wfLocalindInst [lemma, in typing]
wfLocalIndInst [lemma, in typing]
wfLocalLeParams [lemma, in typing]
wfLocalMatchObjEnv [lemma, in typing]
wfLocalMatchTypeEnv [lemma, in typing]
wfLocalP [lemma, in typing]
wfLocalParams [lemma, in typing]
wfLocalParamsMin [lemma, in typing]
wfLocalParamsMinMin [lemma, in typing]
wfLocalParamsP [lemma, in typing]
wfLocalQuantifyCases [lemma, in typing]
wfLocalRelCases [lemma, in typing]
wfLocalRelCasesAux [lemma, in typing]
wfLocalRelCasesF [lemma, in typing]
wfLocalRelCshapeArgs [lemma, in typing]
wfLocalRelIndices [lemma, in typing]
wfLocalRelIndicesMin [lemma, in typing]
wfLocalRelIndices2 [lemma, in typing]
wfLocalRelTypingList [lemma, in typing]
wfLocalToRel [lemma, in typing]
wfParams [lemma, in typing]
wfParamsAux [lemma, in typing]
wfSigma [lemma, in typing]
wf_local_rel_app_inv [lemma, in typing]
wf_local_app_inv [lemma, in typing]

X

xs1 [definition, in MetaCoq.Induction.show]
xs2 [definition, in MetaCoq.Induction.show]
xs3 [definition, in MetaCoq.Induction.show]
xs4 [definition, in MetaCoq.Induction.show]

other

_ +s _ [notation, in typing]
_ :s _ [notation, in typing]
_ +s _ [notation, in MetaCoq.Induction.de_bruijn_print]
_ :s _ [notation, in MetaCoq.Induction.de_bruijn_print]
Derive Container for _ [notation, in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme _ := Induction for _ [notation, in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme Induction for _ [notation, in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme Elimination for _ [notation, in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme _ := Elimination for _ Sort Type [notation, in typing]
Scheme _ := Elimination for _ Sort Type [notation, in typing]
Scheme Elimination for _ Sort Type [notation, in typing]
Scheme Elimination for _ [notation, in typing]
Set _ [notation, in MetaCoq.Induction.Modes]
Set Nested Inductives [notation, in MetaCoq.Induction.MetaCoqInductionPrinciples]
Set _ [notation, in MetaCoq.Induction.mode_test]
Unset _ [notation, in MetaCoq.Induction.Modes]
Unset Nested Inductives [notation, in MetaCoq.Induction.MetaCoqInductionPrinciples]
Unset _ [notation, in MetaCoq.Induction.mode_test]

---

Notation Index

other

_ +s _ [in typing]
_ :s _ [in typing]
_ +s _ [in MetaCoq.Induction.de_bruijn_print]
_ :s _ [in MetaCoq.Induction.de_bruijn_print]
Derive Container for _ [in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme _ := Induction for _ [in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme Induction for _ [in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme Elimination for _ [in MetaCoq.Induction.MetaCoqInductionPrinciples]
Scheme _ := Elimination for _ Sort Type [in typing]
Scheme _ := Elimination for _ Sort Type [in typing]
Scheme Elimination for _ Sort Type [in typing]
Scheme Elimination for _ [in typing]
Set _ [in MetaCoq.Induction.Modes]
Set Nested Inductives [in MetaCoq.Induction.MetaCoqInductionPrinciples]
Set _ [in MetaCoq.Induction.mode_test]
Unset _ [in MetaCoq.Induction.Modes]
Unset Nested Inductives [in MetaCoq.Induction.MetaCoqInductionPrinciples]
Unset _ [in MetaCoq.Induction.mode_test]

---

Module Index

P

P [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
PL [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
PT [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]

T

T [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
TL [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
TT [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]

---

Variable Index

L

LeLemma.Hind [in typing]
LeLemma.Hmind [in typing]
LeLemma.Hwf [in typing]
LeLemma.Γ [in typing]
LeLemma.Σ [in typing]

M

MainSec.caseBodySec.caseBody [in typing]
MainSec.caseBodySec.HeqcaseBody [in typing]
MainSec.declI [in typing]
MainSec.declM [in typing]
MainSec.findBody [in typing]
MainSec.Hwf [in typing]
MainSec.ind [in typing]
MainSec.ind_sorts [in typing]
MainSec.ind_ctors_sort [in typing]
MainSec.ind_arity_eq [in typing]
MainSec.ind_sort [in typing]
MainSec.ind_indices [in typing]
MainSec.ind_body [in typing]
MainSec.matchSec.Env [in typing]
MainSec.matchSec.HeqEnv [in typing]
MainSec.matchSec.HeqmatchObj [in typing]
MainSec.matchSec.HeqmatchType [in typing]
MainSec.matchSec.HeqretType [in typing]
MainSec.matchSec.matchObj [in typing]
MainSec.matchSec.matchType [in typing]
MainSec.matchSec.retType [in typing]
MainSec.mind_body [in typing]
MainSec.nameF [in typing]
MainSec.nparCount [in typing]
MainSec.onArity [in typing]
MainSec.onConstructors [in typing]
MainSec.onGuard [in typing]
MainSec.onInd [in typing]
MainSec.onIndB [in typing]
MainSec.onInductives [in typing]
MainSec.onNpars [in typing]
MainSec.onParams [in typing]
MainSec.onProjections [in typing]
MainSec.uniP [in typing]
MainSec.univ [in typing]
MainSec.Γ [in typing]
MainSec.Σ [in typing]
maxElimSort [in typing]

---

Library Index

A

addContainer
addContainer
addContainer_test2

C

constructorList

D

destruct_lemma
de_bruijn_print

E

elpi_test

H

helperGen
helperGen_test

I

implication
interactive

M

MetaCoqInductionPrinciples
Modes
mode_test

N

nested
nested_datatypes
non_uniform
non_uniform_test

P

parametricity_test_2
parametricity_test
PCUICToTemplate
PCUICToTemplateCorrectness

R

removeNonAug
removeNonAug_test
rose_ind_test

S

show
standardNested

T

test
trans_inj_sur
typing

---

Constructor Index

A

Acc_introᵗ [in MetaCoq.Induction.standardNested]
addS [in MetaCoq.Induction.test]
add0 [in MetaCoq.Induction.test]
All [in MetaCoq.Induction.nested_datatypes]
All_cons [in MetaCoq.Induction.parametricity_test]
All_nil [in MetaCoq.Induction.parametricity_test]
All2_cons [in MetaCoq.Induction.addContainer_test2]
All2_nil [in MetaCoq.Induction.addContainer_test2]

C

Cng [in MetaCoq.Induction.elpi_test]
Cog [in MetaCoq.Induction.elpi_test]
Cong [in MetaCoq.Induction.elpi_test]
Conj [in MetaCoq.Induction.nested_datatypes]
const2 [in MetaCoq.Induction.addContainer_test2]
consᵗ [in MetaCoq.Induction.standardNested]
consᵗ [in MetaCoq.Induction.removeNonAug_test]
Ct0 [in MetaCoq.Induction.test]
C_I [in MetaCoq.Induction.elpi_test]
c10 [in MetaCoq.Induction.nested_datatypes]
c12 [in MetaCoq.Induction.nested_datatypes]
c20 [in MetaCoq.Induction.nested_datatypes]
c3 [in MetaCoq.Induction.nested_datatypes]
c4 [in MetaCoq.Induction.nested_datatypes]
c4ᵗ [in MetaCoq.Induction.standardNested]

D

dep0 [in MetaCoq.Induction.non_uniform_test]
dep0 [in MetaCoq.Induction.test]
Disj [in MetaCoq.Induction.nested_datatypes]
dS [in MetaCoq.Induction.test]
d0 [in MetaCoq.Induction.test]

E

Ex [in MetaCoq.Induction.nested_datatypes]

F

Fal [in MetaCoq.Induction.nested_datatypes]
falseᵗ [in MetaCoq.Induction.standardNested]
falseᵗ [in MetaCoq.Induction.removeNonAug_test]
Func [in MetaCoq.Induction.nested_datatypes]

G

GI [in MetaCoq.Induction.non_uniform_test]
GI [in MetaCoq.Induction.test]
GI [in MetaCoq.Induction.parametricity_test]
G2I1 [in MetaCoq.Induction.non_uniform_test]
G2I1 [in MetaCoq.Induction.test]
G2I2 [in MetaCoq.Induction.non_uniform_test]
G2I2 [in MetaCoq.Induction.test]
G3I [in MetaCoq.Induction.non_uniform_test]
G3I [in MetaCoq.Induction.test]
G4I [in MetaCoq.Induction.test]
G5I [in MetaCoq.Induction.test]

H

H [in MetaCoq.Induction.elpi_test]

I

Impl [in MetaCoq.Induction.nested_datatypes]
indC0 [in MetaCoq.Induction.test]
is_Node [in MetaCoq.Induction.standardNested]
is_Leaf [in MetaCoq.Induction.standardNested]
is_consV [in MetaCoq.Induction.standardNested]
is_nilV [in MetaCoq.Induction.standardNested]
is_pair [in MetaCoq.Induction.standardNested]
is_cons [in MetaCoq.Induction.standardNested]
is_nil [in MetaCoq.Induction.standardNested]

L

Leaf [in MetaCoq.Induction.nested_datatypes]
Leaf [in MetaCoq.Induction.elpi_test]
LeafProp [in MetaCoq.Induction.parametricity_test]

M

mP [in MetaCoq.Induction.test]

N

nilt2 [in MetaCoq.Induction.addContainer_test2]
nilᵗ [in MetaCoq.Induction.standardNested]
nilᵗ [in MetaCoq.Induction.removeNonAug_test]
Node [in MetaCoq.Induction.nested_datatypes]
Node [in MetaCoq.Induction.elpi_test]
NodeProp [in MetaCoq.Induction.parametricity_test]
node3 [in MetaCoq.Induction.nested_datatypes]

O

Oᵗ [in MetaCoq.Induction.standardNested]
Oᵗ [in MetaCoq.Induction.removeNonAug_test]

P

Pred [in MetaCoq.Induction.nested_datatypes]
p0 [in MetaCoq.Induction.test]
p1 [in MetaCoq.Induction.test]
p2 [in MetaCoq.Induction.test]
p3 [in MetaCoq.Induction.test]
p4 [in MetaCoq.Induction.test]

Q

Qcon [in MetaCoq.Induction.test]

S

Sᵗ [in MetaCoq.Induction.standardNested]
Sᵗ [in MetaCoq.Induction.removeNonAug_test]

T

Top [in MetaCoq.Induction.nested_datatypes]
tree [in MetaCoq.Induction.nested_datatypes]
treeDN1 [in MetaCoq.Induction.nested_datatypes]
treeDN2 [in MetaCoq.Induction.nested_datatypes]
treeDN3 [in MetaCoq.Induction.nested_datatypes]
treeDN4 [in MetaCoq.Induction.nested_datatypes]
treeDN5 [in MetaCoq.Induction.nested_datatypes]
treeDN6 [in MetaCoq.Induction.nested_datatypes]
treeDN7 [in MetaCoq.Induction.nested_datatypes]
treeNN1 [in MetaCoq.Induction.nested_datatypes]
treeNN2 [in MetaCoq.Induction.nested_datatypes]
treeNN3 [in MetaCoq.Induction.nested_datatypes]
treeNN4 [in MetaCoq.Induction.nested_datatypes]
treeNN5 [in MetaCoq.Induction.nested_datatypes]
treeNN6 [in MetaCoq.Induction.nested_datatypes]
treeNN7 [in MetaCoq.Induction.nested_datatypes]
treeO1 [in MetaCoq.Induction.nested_datatypes]
treeO10 [in MetaCoq.Induction.nested_datatypes]
treeO11 [in MetaCoq.Induction.nested_datatypes]
treeO13 [in MetaCoq.Induction.nested_datatypes]
treeO2 [in MetaCoq.Induction.nested_datatypes]
treeO3 [in MetaCoq.Induction.nested_datatypes]
treeO3P [in MetaCoq.Induction.parametricity_test]
treeO3ᵗ [in MetaCoq.Induction.standardNested]
treeO4 [in MetaCoq.Induction.nested_datatypes]
treeO5 [in MetaCoq.Induction.nested_datatypes]
treeO6 [in MetaCoq.Induction.nested_datatypes]
treeO7 [in MetaCoq.Induction.nested_datatypes]
treeO8 [in MetaCoq.Induction.nested_datatypes]
treeO9 [in MetaCoq.Induction.nested_datatypes]
treePI1 [in MetaCoq.Induction.nested_datatypes]
treePI2 [in MetaCoq.Induction.nested_datatypes]
treePI3 [in MetaCoq.Induction.nested_datatypes]
treePI4 [in MetaCoq.Induction.nested_datatypes]
treePI5 [in MetaCoq.Induction.nested_datatypes]
treePI6 [in MetaCoq.Induction.nested_datatypes]
treePI7 [in MetaCoq.Induction.nested_datatypes]
treePI8 [in MetaCoq.Induction.nested_datatypes]
treePI8 [in MetaCoq.Induction.non_uniform_test]
tree2 [in MetaCoq.Induction.nested_datatypes]
tree3 [in MetaCoq.Induction.nested_datatypes]
tree4 [in MetaCoq.Induction.nested_datatypes]
tree5 [in MetaCoq.Induction.nested_datatypes]
tree6 [in MetaCoq.Induction.nested_datatypes]
trueᵗ [in MetaCoq.Induction.standardNested]
trueᵗ [in MetaCoq.Induction.removeNonAug_test]
typeCons [in typing]
typeNil [in typing]

V

var_foterm [in MetaCoq.Induction.nested_datatypes]
veccons [in MetaCoq.Induction.parametricity_test]
vecconsᵗ [in MetaCoq.Induction.standardNested]
vecconsᵗ [in MetaCoq.Induction.removeNonAug_test]
vecconsᵗ' [in MetaCoq.Induction.standardNested]
vecnil [in MetaCoq.Induction.parametricity_test]
vecnilᵗ [in MetaCoq.Induction.standardNested]
vecnilᵗ [in MetaCoq.Induction.removeNonAug_test]
vecnilᵗ' [in MetaCoq.Induction.standardNested]

---

Lemma Index

A

AllSpecial [in typing]
All_over_All [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
All_forall [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
appCons [in typing]
appConsNilFront [in typing]
appInjLen [in typing]
appLen [in typing]
appOneNeqNil [in typing]

B

bodyIndApp [in typing]
branchesHaveFittingTypes [in typing]
branchesHaveTypes [in typing]
branchTypesFit [in typing]
branchTypeTypes [in typing]

C

caseEnvHasType [in typing]
collectLambdaMapIsNotLambda [in typing]
collectLambdaMaxElim [in typing]
collectLambdaMkLambda [in typing]
collectLambdaProdDisjoint [in typing]
collectLift [in typing]
collectNoLambda [in typing]
collectNoProd [in typing]
collectProdLambdaDisjoint [in typing]
collectProdMaxElim [in typing]
collectProdMkProd [in typing]
collectProdMkProdGen [in typing]
collectProdVass [in typing]
collectReplace [in typing]
collect_prods2 [in typing]
consistentInstanceExt [in typing]
consMin [in typing]
countLeb [in typing]
countMax [in typing]
createReturnNone [in typing]
createSome [in typing]
cshapeArgsVass [in typing]
cshapeTypingList [in typing]
cumul_eta_r [in typing]

D

destAritySimpl [in typing]
diffIndBody [in typing]

E

eqIsEq [in MetaCoq.Induction.test]
eq_term_upto_univ_refl [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
etaConvRetType3 [in typing]
etaConvType [in typing]
etaConvTypeGen [in typing]
etaConvTypeInv [in typing]
extendOnConstructors [in typing]
extractOption [in typing]

F

fixEnvWf [in typing]
fixGuardAxiom [in typing]
fixTypeTypes [in typing]
foldLiftSubstIndices [in typing]
foldLiftSubstIndices3 [in typing]
foldMkLambda [in typing]
foldMkLambdaUnfold [in typing]
foldMkProd [in typing]
foldMkProdLetIn [in typing]
foldMkProdUnfold [in typing]
fold_right_sum_leq [in MetaCoq.Induction.destruct_lemma]
fold_right_map [in MetaCoq.Induction.destruct_lemma]
fold_right_min [in typing]

G

getKelim [in typing]
getMaxElimSort [in typing]
getOndIndBody [in typing]
getParamCountBound [in typing]

I

indAppType [in typing]
indicesType [in typing]
indicesVass [in typing]
indParamVass [in typing]
inj_sur [in MetaCoq.Induction.trans_inj_sur]
instantiateParams [in typing]
instantiateParams3 [in typing]
instParamsSubstSimpl [in typing]
invert_type_App [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
inv_opt_monad [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
in_mapi [in typing]
in_app_or [in typing]
isLambdaInv [in typing]
isProdInv [in typing]
is_list_in [in MetaCoq.Induction.standardNested]
itMkProdInj [in typing]
itMkProdNeq [in typing]
it_mkProd_inv [in typing]

L

leElimTyping [in typing]
lengthAppend [in typing]
leq_term_refl [in typing]
leq_term_refl [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
le_elim [in typing]
liftAdd [in typing]
liftCollectProd [in typing]
liftContextSucc [in typing]
liftContextSum [in typing]
liftIndicesVass [in typing]
liftIndIndices [in typing]
liftIndParams [in typing]
liftIndType [in typing]
liftingInVass [in typing]
liftInstIndices [in typing]
LiftIsProd [in typing]
liftMaxElim [in typing]
liftMkRel [in typing]
liftReplaceLastProd [in typing]
liftSubstInstanceConstr [in typing]
liftSubstInstanceConstrGen [in typing]
liftSubstInstanceConstr2 [in typing]
lifttInd [in typing]
liftUnderReplaceLambda [in typing]
lift_wf_local_rel [in typing]
lift_it_mkProd_or_LetIn [in typing]
lift_it_mkLambda_or_LetIn [in typing]
lift_context_len [in typing]
lt_plus_S_r [in MetaCoq.Induction.destruct_lemma]
lt_plus_S_l [in MetaCoq.Induction.destruct_lemma]

M

Main2 [in typing]
mapAgreement [in typing]
mapDeclNested [in typing]
mapDeclVass [in typing]
mapExt [in typing]
mapId [in typing]
mapiExt [in typing]
mapiLiftContext [in typing]
mapiNatRec [in typing]
mapiNatRecGen [in typing]
mapiNested [in typing]
mapiRecNested [in typing]
mapIsProdLam [in typing]
mapiSub [in typing]
mapi_rec_len [in typing]
mapLen [in typing]
mapMk [in typing]
mapOne [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
mapOptionOutApp [in typing]
mapParamIndRelEq [in typing]
mapParamIndRelEq3 [in typing]
mapProdNoProd [in typing]
mapProdToLambdaItMkProd [in typing]
mapSndAdd0 [in typing]
mapTypeErase [in typing]
mapTypeEraseAux [in typing]
matchElimLower [in typing]
matchObjTyping [in typing]
matchOnMkApps [in typing]
matchTypeHasType [in typing]
matchTypeHasType' [in typing]
matchTypeSimpl [in typing]
matchTypeTypeFit [in typing]
maxElimType [in typing]
minChainMax [in typing]
minChainMin [in typing]
mkAppMkApps [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
mkAppNoLambda [in typing]
mkAppsExt [in typing]
mkAppsTApp [in typing]
mkLambdaCollect [in typing]
mkRelApp [in typing]

N

nameEq [in typing]
natRecAppGen [in typing]
natRecExt [in typing]
noLambdaMaxElim [in typing]
nonUniCount [in typing]
noProdMaxElim [in typing]
nthInds [in typing]

O

onConstructorIndBodyNotMatter [in typing]
onContextInv [in typing]
onIndDeclInd [in typing]
onIndMutInd [in typing]
onIndNth [in typing]
onSndId [in typing]
optionMapNested [in typing]
optMonadEq [in typing]
optMonadEq2 [in typing]

P

pAppliedIndType [in typing]
pAppliedIndType' [in typing]
pointLessIf [in typing]
pType [in typing]

Q

quantifyCasesLen [in typing]
quantifyCasesType [in typing]

R

relnMkRel [in typing]
removeArityCount [in typing]
removeArityProdCount [in typing]
removeArityProds [in typing]
removeArityProds2 [in typing]
removeMkProd [in typing]
removeProdMaxElim [in typing]
removeReplaceProd [in typing]
replaceLambdaMaxElim [in typing]
replaceLastLambdaNoLambda [in typing]
replaceLastLambdaSelf [in typing]
replaceLastOffsetAll [in typing]
replaceLastProdNotProd [in typing]
replaceLastProdReplaceLastProd [in typing]
replaceLastProdSelf [in typing]
replaceLastTypeLambda [in typing]
replaceLastTypeLambdaItLam [in typing]
replaceLastTypeProd [in typing]
replaceMap [in typing]
replaceOffsetUnderItProd [in typing]
replaceOneProd [in typing]
replaceProdMaxElim [in typing]
replaceUnderItMkLambda [in typing]
replaceUnderItMkProd [in typing]
replaceUnderLambda [in typing]
replaceUnderOneLambda [in typing]
retTypeLifting [in typing]
revCollect [in typing]
revInj [in typing]
revLen [in typing]
revRev [in typing]
rev_elim [in typing]
rewriteCaseEnv [in typing]
rewriteCaseEnvType [in typing]
RLLambdaIsLambdaInner [in typing]
RLLambdaIsLambdaOuter [in typing]
RLProdIsProd [in typing]

S

simplLiftContext [in typing]
size_induction [in MetaCoq.Induction.destruct_lemma]
skipnApp [in typing]
substContextSubstInstParamVass [in typing]
substInstanceConstrIndices [in typing]
substInstanceConstrMkProd [in typing]
substInstanceConstrParam [in typing]
substInstanceContextLen [in typing]
substInstParamVass [in typing]
substNoApp [in typing]
subst_it_mkLambda_or_LetIn [in typing]
subst_it_mkProd_or_LetIn [in typing]
subst_context_len [in typing]
succLen [in typing]

T

template_to_pcuic [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
termSizeLifting [in MetaCoq.Induction.destruct_lemma]
toExtendedListLen [in typing]
toExtendedListLenNoBody [in typing]
trans_mfix_All2 [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mfix_All [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_branches [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_wf_local_env [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_wf_local' [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_fix_context [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_build_case_predicate_type [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_it_mkProd_or_LetIn [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mkProd_or_LetIn [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_destr_arity [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_instantiate_params' [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_instantiate_params [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_declared_projection [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_dbody [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_dtype [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_type_of_constructor [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_ind_type [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_cst_type [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_subst_instance_constr [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_subst10 [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_subst [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_decl_type [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mkApps [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_declared_inductive [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_consistent_instance_ext [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_constraintSet_in [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_declared_constant [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_lookup [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_in_level_set [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_mem_level_set [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_global_ext_levels [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_lift [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
typeBranch [in typing]
typeF [in typing]
typeIndAppIndices [in typing]
typeLiftLiftApplication [in typing]
typeNat [in typing]
typeParamsP [in typing]
typeSnoc [in typing]
typeSnocInv [in typing]
typetInd [in typing]
type_LambdaR [in typing]
type_LambdaL [in typing]
type_Rel2 [in typing]
type_it_mkProd_or_LetIn [in typing]
type_Lambda2 [in typing]
type_it_mkLambda_or_LetIn [in typing]
type_mkApp [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
typingApp [in typing]
typingF [in typing]
typingLiftAppChain [in typing]
typingListIndices [in typing]
typingListIndices2 [in typing]
typingListOffset [in typing]
typingParamInd [in typing]
typingSpineIndices [in typing]
typingSpineIndices' [in typing]
typingSpineIndices2 [in typing]
typingSpineInstInstf [in typing]
typingSpineInstInstf' [in typing]
typingSpineLifting [in typing]
typingSpineParamIndexRel [in typing]
typingSpineParamIndexRelLiftet [in typing]
typingSpineProdApp [in typing]

V

vassCons [in typing]
vassSubstContext [in typing]

W

weakeningWfLocalRel [in typing]
wfLocalBaseCase [in typing]
wfLocalBaseCaseSndArgs [in typing]
wfLocalCaseEnvEnv [in typing]
wfLocalCases [in typing]
wfLocalEnv [in typing]
wfLocalF [in typing]
wfLocalFixContext [in typing]
wfLocalFixEnv [in typing]
wfLocalFmInst [in typing]
wfLocalFmInstmInst [in typing]
wfLocalFmInstmInstmInst [in typing]
wfLocalIndicesMin [in typing]
wfLocalindInst [in typing]
wfLocalIndInst [in typing]
wfLocalLeParams [in typing]
wfLocalMatchObjEnv [in typing]
wfLocalMatchTypeEnv [in typing]
wfLocalP [in typing]
wfLocalParams [in typing]
wfLocalParamsMin [in typing]
wfLocalParamsMinMin [in typing]
wfLocalParamsP [in typing]
wfLocalQuantifyCases [in typing]
wfLocalRelCases [in typing]
wfLocalRelCasesAux [in typing]
wfLocalRelCasesF [in typing]
wfLocalRelCshapeArgs [in typing]
wfLocalRelIndices [in typing]
wfLocalRelIndicesMin [in typing]
wfLocalRelIndices2 [in typing]
wfLocalRelTypingList [in typing]
wfLocalToRel [in typing]
wfParams [in typing]
wfParamsAux [in typing]
wfSigma [in typing]
wf_local_rel_app_inv [in typing]
wf_local_app_inv [in typing]

---

Axiom Index

F

Funcs [in MetaCoq.Induction.nested_datatypes]
fun_ar [in MetaCoq.Induction.nested_datatypes]

H

H2 [in MetaCoq.Induction.implication]

N

namingEq2 [in typing]

P

Preds [in MetaCoq.Induction.nested_datatypes]
pred_ar [in MetaCoq.Induction.nested_datatypes]

---

Projection Index

A

assumption [in MetaCoq.Induction.helperGen]
assumption [in MetaCoq.Induction.helperGen_test]
assumptionType [in MetaCoq.Induction.helperGen]
assumptionType [in MetaCoq.Induction.helperGen_test]

P

principle [in MetaCoq.Induction.destruct_lemma]
principleType [in MetaCoq.Induction.destruct_lemma]
proof [in MetaCoq.Induction.helperGen]
proof [in MetaCoq.Induction.helperGen_test]
proofType [in MetaCoq.Induction.helperGen]
proofType [in MetaCoq.Induction.helperGen_test]

S

state [in MetaCoq.Induction.Modes]
state [in MetaCoq.Induction.mode_test]

---

Inductive Index

A

Accᵗ [in MetaCoq.Induction.standardNested]
addition [in MetaCoq.Induction.test]
AllI [in MetaCoq.Induction.parametricity_test]
All2 [in MetaCoq.Induction.addContainer_test2]

B

boolᵗ [in MetaCoq.Induction.standardNested]
boolᵗ [in MetaCoq.Induction.removeNonAug_test]
brtree [in MetaCoq.Induction.elpi_test]

C

containerInd [in MetaCoq.Induction.nested_datatypes]
containerInd2 [in MetaCoq.Induction.nested_datatypes]
containerInd3 [in MetaCoq.Induction.nested_datatypes]
containerInd4 [in MetaCoq.Induction.nested_datatypes]
containerInd4ᵗ [in MetaCoq.Induction.standardNested]

D

deep [in MetaCoq.Induction.elpi_test]
dep [in MetaCoq.Induction.non_uniform_test]
dep [in MetaCoq.Induction.test]
double [in MetaCoq.Induction.test]

E

eqT [in MetaCoq.Induction.test]

F

form [in MetaCoq.Induction.nested_datatypes]
foterm [in MetaCoq.Induction.nested_datatypes]

G

G [in MetaCoq.Induction.non_uniform_test]
G [in MetaCoq.Induction.test]
G [in MetaCoq.Induction.parametricity_test]
G2 [in MetaCoq.Induction.non_uniform_test]
G2 [in MetaCoq.Induction.test]
G3 [in MetaCoq.Induction.non_uniform_test]
G3 [in MetaCoq.Induction.test]
G4 [in MetaCoq.Induction.test]
G5 [in MetaCoq.Induction.test]

I

Idx [in MetaCoq.Induction.elpi_test]
indexIndTest [in MetaCoq.Induction.test]
indTest [in MetaCoq.Induction.test]
is_rtree [in MetaCoq.Induction.standardNested]
is_vec [in MetaCoq.Induction.standardNested]
is_prod [in MetaCoq.Induction.standardNested]
is_list [in MetaCoq.Induction.standardNested]

L

listᵗ [in MetaCoq.Induction.standardNested]
listᵗ [in MetaCoq.Induction.removeNonAug_test]

M

mutParam [in MetaCoq.Induction.test]

N

natᵗ [in MetaCoq.Induction.standardNested]
natᵗ [in MetaCoq.Induction.removeNonAug_test]
nestGuard [in MetaCoq.Induction.elpi_test]

O

outerGuard [in MetaCoq.Induction.elpi_test]
outNestGuard [in MetaCoq.Induction.elpi_test]

P

pfree [in MetaCoq.Induction.test]

R

roseTree [in MetaCoq.Induction.nested_datatypes]
roseTreeDN1 [in MetaCoq.Induction.nested_datatypes]
roseTreeDN2 [in MetaCoq.Induction.nested_datatypes]
roseTreeDN3 [in MetaCoq.Induction.nested_datatypes]
roseTreeDN4 [in MetaCoq.Induction.nested_datatypes]
roseTreeDN5 [in MetaCoq.Induction.nested_datatypes]
roseTreeDN6 [in MetaCoq.Induction.nested_datatypes]
roseTreeDN7 [in MetaCoq.Induction.nested_datatypes]
roseTreeNN1 [in MetaCoq.Induction.nested_datatypes]
roseTreeNN2 [in MetaCoq.Induction.nested_datatypes]
roseTreeNN3 [in MetaCoq.Induction.nested_datatypes]
roseTreeNN4 [in MetaCoq.Induction.nested_datatypes]
roseTreeNN5 [in MetaCoq.Induction.nested_datatypes]
roseTreeNN6 [in MetaCoq.Induction.nested_datatypes]
roseTreeNN7 [in MetaCoq.Induction.nested_datatypes]
roseTreeO1 [in MetaCoq.Induction.nested_datatypes]
roseTreeO10 [in MetaCoq.Induction.nested_datatypes]
roseTreeO11 [in MetaCoq.Induction.nested_datatypes]
roseTreeO13 [in MetaCoq.Induction.nested_datatypes]
roseTreeO2 [in MetaCoq.Induction.nested_datatypes]
roseTreeO3 [in MetaCoq.Induction.nested_datatypes]
roseTreeO3P [in MetaCoq.Induction.parametricity_test]
roseTreeO3ᵗ [in MetaCoq.Induction.standardNested]
roseTreeO4 [in MetaCoq.Induction.nested_datatypes]
roseTreeO5 [in MetaCoq.Induction.nested_datatypes]
roseTreeO6 [in MetaCoq.Induction.nested_datatypes]
roseTreeO7 [in MetaCoq.Induction.nested_datatypes]
roseTreeO8 [in MetaCoq.Induction.nested_datatypes]
roseTreeO9 [in MetaCoq.Induction.nested_datatypes]
roseTreePI1 [in MetaCoq.Induction.nested_datatypes]
roseTreePI2 [in MetaCoq.Induction.nested_datatypes]
roseTreePI3 [in MetaCoq.Induction.nested_datatypes]
roseTreePI4 [in MetaCoq.Induction.nested_datatypes]
roseTreePI5 [in MetaCoq.Induction.nested_datatypes]
roseTreePI6 [in MetaCoq.Induction.nested_datatypes]
roseTreePI7 [in MetaCoq.Induction.nested_datatypes]
roseTreePI8 [in MetaCoq.Induction.nested_datatypes]
roseTreePI8 [in MetaCoq.Induction.non_uniform_test]
roseTree2 [in MetaCoq.Induction.nested_datatypes]
roseTree3 [in MetaCoq.Induction.nested_datatypes]
roseTree4 [in MetaCoq.Induction.nested_datatypes]
roseTree5 [in MetaCoq.Induction.nested_datatypes]
roseTree6 [in MetaCoq.Induction.nested_datatypes]
rtree [in MetaCoq.Induction.nested_datatypes]
rtreeProp [in MetaCoq.Induction.parametricity_test]

T

typingList [in typing]
t2 [in MetaCoq.Induction.addContainer_test2]

V

vec [in MetaCoq.Induction.parametricity_test]
vecᵗ [in MetaCoq.Induction.standardNested]
vecᵗ [in MetaCoq.Induction.removeNonAug_test]
vecᵗ' [in MetaCoq.Induction.standardNested]

---

Instance Index

C

containerInd4Inst [in MetaCoq.Induction.standardNested]

D

defInst [in MetaCoq.Induction.standardNested]

L

listInst [in MetaCoq.Induction.standardNested]

M

mfixpointInst [in MetaCoq.Induction.standardNested]

P

prodInst [in MetaCoq.Induction.standardNested]

R

rtreeInst [in MetaCoq.Induction.standardNested]

T

typingSpineReflexive [in typing]

V

vecInst [in MetaCoq.Induction.standardNested]

---

Section Index

A

AuxLemma [in typing]

B

Basic [in typing]

C

CustomFunction [in typing]

F

Functions [in typing]

L

LeLemma [in typing]

M

MainSec [in typing]
MainSec.caseBodySec [in typing]
MainSec.matchSec [in typing]
MetaCoqTheorem [in typing]

P

PICUICTheory [in typing]

T

Tmp [in typing]

---

Abbreviation Index

N

name_of [in MetaCoq.Induction.MetaCoqInductionPrinciples]
name_of [in typing]

---

Definition Index

A

AccProof [in MetaCoq.Induction.standardNested]
addContrapos [in MetaCoq.Induction.implication]
addContraposType [in MetaCoq.Induction.implication]
addHelper [in typing]
addInductiveHypothesis [in typing]
addType [in MetaCoq.Induction.addContainer]
addType [in MetaCoq.Induction.addContainer]
addType [in MetaCoq.Induction.addContainer_test2]
allVass [in typing]
ascii_to_string [in typing]
ascii_to_string [in MetaCoq.Induction.de_bruijn_print]
augmentType [in MetaCoq.Induction.addContainer]
augmentType [in MetaCoq.Induction.addContainer]
augmentType [in MetaCoq.Induction.addContainer_test2]

B

branchTypes [in typing]
bruijn_print [in typing]
bruijn_print_aux [in typing]
bruijn_print [in MetaCoq.Induction.de_bruijn_print]
bruijn_print_aux [in MetaCoq.Induction.de_bruijn_print]

C

canElim [in MetaCoq.Induction.destruct_lemma]
canElim [in typing]
changeMode [in MetaCoq.Induction.Modes]
changeMode [in MetaCoq.Induction.mode_test]
cleanInd [in MetaCoq.Induction.removeNonAug_test]
cleanInd [in MetaCoq.Induction.removeNonAug]
cleanIndTop [in MetaCoq.Induction.removeNonAug_test]
cleanIndTop [in MetaCoq.Induction.removeNonAug]
cleanOInd [in MetaCoq.Induction.removeNonAug_test]
cleanOInd [in MetaCoq.Induction.removeNonAug]
collect_prods [in MetaCoq.Induction.non_uniform_test]
collect_prods [in MetaCoq.Induction.non_uniform]
collect_lambdas [in MetaCoq.Induction.destruct_lemma]
collect_prods [in MetaCoq.Induction.destruct_lemma]
collect_lambdas [in typing]
collect_prods [in typing]
computeContrapos [in MetaCoq.Induction.implication]
concatString [in typing]
concatString [in MetaCoq.Induction.de_bruijn_print]
constrMapping [in typing]
containerInd4Proof [in MetaCoq.Induction.standardNested]
countOfCtor [in MetaCoq.Induction.non_uniform_test]
countOfCtor [in MetaCoq.Induction.non_uniform]
countOfCtor [in typing]
count_prods [in MetaCoq.Induction.non_uniform_test]
count_prods [in MetaCoq.Induction.non_uniform]
count_prods [in MetaCoq.Induction.destruct_lemma]
count_prods [in typing]
create [in MetaCoq.Induction.destruct_lemma]
create [in typing]
createAppChain [in MetaCoq.Induction.destruct_lemma]
createAppChain [in typing]
createAppChainOff [in MetaCoq.Induction.destruct_lemma]
createAppChainOff [in typing]
createElim [in MetaCoq.Induction.destruct_lemma]
createElim [in typing]
createElimType [in typing]
createFunction [in MetaCoq.Induction.helperGen]
createFunction [in MetaCoq.Induction.helperGen_test]
createFunction [in MetaCoq.Induction.show]
createShow [in MetaCoq.Induction.show]
createShowFunc [in MetaCoq.Induction.show]

D

defAssumption [in MetaCoq.Induction.standardNested]
defProof [in MetaCoq.Induction.standardNested]
deLift01 [in MetaCoq.Induction.removeNonAug_test]
deLift01 [in MetaCoq.Induction.removeNonAug]
deriveShowType [in MetaCoq.Induction.show]

E

Enat [in MetaCoq.Induction.test]
errorMessage [in MetaCoq.Induction.helperGen]
errorMessage [in MetaCoq.Induction.helperGen_test]
extendList [in MetaCoq.Induction.show]
extendName [in MetaCoq.Induction.destruct_lemma]
extractFunction [in MetaCoq.Induction.helperGen]
extractFunction [in MetaCoq.Induction.helperGen_test]

F

F [in MetaCoq.Induction.standardNested]
filteri [in typing]
findRec [in MetaCoq.Induction.helperGen]
findRec [in MetaCoq.Induction.helperGen_test]
findRecInd [in MetaCoq.Induction.helperGen]
findRecInd [in MetaCoq.Induction.helperGen_test]
findRel [in MetaCoq.Induction.destruct_lemma]
findRel [in typing]
foterm_induct [in MetaCoq.Induction.rose_ind_test]

G

generateInductiveAssumptions [in MetaCoq.Induction.destruct_lemma]
generatePCall2 [in MetaCoq.Induction.destruct_lemma]
getConstructName [in typing]
getConstructName [in MetaCoq.Induction.de_bruijn_print]
getCtors [in MetaCoq.Induction.constructorList]
getCtorsSimpl [in MetaCoq.Induction.constructorList]
getInd [in MetaCoq.Induction.helperGen]
getInd [in MetaCoq.Induction.helperGen_test]
getIndProp [in MetaCoq.Induction.addContainer]
getIndProp [in MetaCoq.Induction.addContainer]
getIndProp [in MetaCoq.Induction.addContainer_test2]
getInds [in MetaCoq.Induction.helperGen]
getInds [in MetaCoq.Induction.helperGen_test]
getInductiveCalls [in typing]
getInductiveName [in typing]
getInductiveName [in MetaCoq.Induction.de_bruijn_print]
getInner [in MetaCoq.Induction.destruct_lemma]
getMaxElim [in MetaCoq.Induction.destruct_lemma]
getMaxElim [in typing]
getMinChain [in MetaCoq.Induction.non_uniform_test]
getMinChain [in MetaCoq.Induction.non_uniform]
getMinChain [in typing]
getMode [in MetaCoq.Induction.Modes]
getMode [in MetaCoq.Induction.mode_test]
getName [in MetaCoq.Induction.Modes]
getName [in MetaCoq.Induction.MetaCoqInductionPrinciples]
getName [in typing]
getName [in MetaCoq.Induction.mode_test]
getP [in MetaCoq.Induction.non_uniform_test]
getP [in MetaCoq.Induction.non_uniform]
getP [in typing]
getParamCount [in MetaCoq.Induction.non_uniform_test]
getParamCount [in MetaCoq.Induction.non_uniform]
getParamCount [in typing]
getPCount [in MetaCoq.Induction.non_uniform_test]
getPCount [in MetaCoq.Induction.non_uniform]
getPCount [in typing]

H

H [in MetaCoq.Induction.implication]
hasSat [in MetaCoq.Induction.destruct_lemma]
hasSat [in typing]
H3 [in MetaCoq.Induction.implication]

I

id [in MetaCoq.Induction.destruct_lemma]
id [in typing]
isAugmentable [in MetaCoq.Induction.helperGen]
isAugmentable [in MetaCoq.Induction.helperGen_test]
isAugmentable [in MetaCoq.Induction.removeNonAug_test]
isAugmentable [in MetaCoq.Induction.removeNonAug]
isLetIn [in typing]
isProd [in MetaCoq.Induction.destruct_lemma]
isProd [in typing]

J

join [in typing]
join [in MetaCoq.Induction.de_bruijn_print]

L

lift01 [in MetaCoq.Induction.show]
linebreak [in typing]
linebreak [in MetaCoq.Induction.de_bruijn_print]
listAssumption [in MetaCoq.Induction.standardNested]
listAssumption2 [in MetaCoq.Induction.standardNested]
listCtors [in MetaCoq.Induction.constructorList]
listProof [in MetaCoq.Induction.standardNested]
listProof2 [in MetaCoq.Induction.standardNested]

M

mapProdToLambda [in MetaCoq.Induction.destruct_lemma]
mapProdToLambda [in typing]
mapProdToLambda2 [in typing]
map_context_lifting [in MetaCoq.Induction.show]
matchTypeType [in typing]
mfixpointAssumption [in MetaCoq.Induction.standardNested]
mfixpointProof [in MetaCoq.Induction.standardNested]
mkRel [in typing]
mkRelNum [in MetaCoq.Induction.destruct_lemma]

N

nameAppend [in MetaCoq.Induction.addContainer]
nameAppend [in MetaCoq.Induction.addContainer]
nameAppend [in MetaCoq.Induction.addContainer_test2]
nameToString [in typing]
nameToString [in MetaCoq.Induction.de_bruijn_print]
natCtors [in MetaCoq.Induction.constructorList]
natToChar [in typing]
natToChar [in MetaCoq.Induction.de_bruijn_print]
natToString [in typing]
natToString [in MetaCoq.Induction.de_bruijn_print]
nestedMode [in MetaCoq.Induction.helperGen]
nestedMode [in MetaCoq.Induction.helperGen_test]
nonAugInd [in MetaCoq.Induction.removeNonAug_test]
nonAugInd [in MetaCoq.Induction.removeNonAug]

O

on_fst [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]

P

pretty [in MetaCoq.Induction.show]
printer [in MetaCoq.Induction.interactive]
prodAssumption [in MetaCoq.Induction.standardNested]
prodProof [in MetaCoq.Induction.standardNested]
prodProof2 [in MetaCoq.Induction.standardNested]

Q

quantifyCases [in MetaCoq.Induction.destruct_lemma]
quantifyCases [in typing]

R

removeArgList [in MetaCoq.Induction.removeNonAug_test]
removeArgList [in MetaCoq.Induction.removeNonAug]
removeElements [in MetaCoq.Induction.removeNonAug_test]
removeElements [in MetaCoq.Induction.removeNonAug]
removeNonAugList [in MetaCoq.Induction.removeNonAug_test]
removeNonAugList [in MetaCoq.Induction.removeNonAug]
removeNonAugmentable [in MetaCoq.Induction.removeNonAug_test]
removeNonAugmentable [in MetaCoq.Induction.removeNonAug]
remove_prods [in typing]
remove_lambdas [in typing]
replaceLastLambda [in MetaCoq.Induction.destruct_lemma]
replaceLastLambda [in typing]
replaceLastLambda' [in MetaCoq.Induction.destruct_lemma]
replaceLastLambda' [in typing]
replaceLastOffset [in typing]
replaceLastProd [in MetaCoq.Induction.destruct_lemma]
replaceLastProd [in typing]
replaceLastProd' [in MetaCoq.Induction.destruct_lemma]
replaceLastProd' [in typing]
roseTreeO3_ind_MC [in MetaCoq.Induction.standardNested]
rtreeO3Proof [in MetaCoq.Induction.standardNested]
rtreeProof [in MetaCoq.Induction.standardNested]
rtreeProof2 [in MetaCoq.Induction.standardNested]
rtree_ind_MC_Test [in MetaCoq.Induction.standardNested]
runElim [in MetaCoq.Induction.destruct_lemma]
runElim [in typing]
runShow [in MetaCoq.Induction.show]

S

showFunction [in MetaCoq.Induction.show]
stringQ [in MetaCoq.Induction.show]
substAdd [in typing]
substApp [in typing]

T

termNegType [in MetaCoq.Induction.implication]
termsize [in MetaCoq.Induction.destruct_lemma]
term_size_ind [in MetaCoq.Induction.destruct_lemma]
testInd [in MetaCoq.Induction.helperGen_test]
trans [in MetaCoq.Induction.destruct_lemma]
trans [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans [in MetaCoq.Induction.show]
trans_def [in MetaCoq.Induction.other_files.PCUICToTemplateCorrectness]
trans_global [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_global_decls [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_global_decl [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_minductive_body [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_constant_body [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_one_ind_body [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_ctor [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_local [in MetaCoq.Induction.other_files.PCUICToTemplate]
trans_decl [in MetaCoq.Induction.other_files.PCUICToTemplate]
trivialPred [in MetaCoq.Induction.destruct_lemma]
trivialProof [in MetaCoq.Induction.destruct_lemma]
tr1 [in MetaCoq.Induction.destruct_lemma]
tr2 [in MetaCoq.Induction.destruct_lemma]
t1 [in MetaCoq.Induction.non_uniform_test]
t2 [in MetaCoq.Induction.non_uniform_test]

U

Unnamed_thm1 [in MetaCoq.Induction.rose_ind_test]
Unnamed_thm0 [in MetaCoq.Induction.rose_ind_test]
Unnamed_thm [in MetaCoq.Induction.rose_ind_test]

V

vec [in MetaCoq.Induction.standardNested]
vec [in MetaCoq.Induction.removeNonAug_test]
vecProof [in MetaCoq.Induction.standardNested]
vecProof2 [in MetaCoq.Induction.standardNested]
vecProof2' [in MetaCoq.Induction.standardNested]
vt1 [in MetaCoq.Induction.non_uniform_test]
vt2 [in MetaCoq.Induction.non_uniform_test]

X

xs1 [in MetaCoq.Induction.show]
xs2 [in MetaCoq.Induction.show]
xs3 [in MetaCoq.Induction.show]
xs4 [in MetaCoq.Induction.show]

---

Record Index

B

betterInd [in MetaCoq.Induction.destruct_lemma]

M

mode [in MetaCoq.Induction.Modes]
mode [in MetaCoq.Induction.mode_test]

R

registered [in MetaCoq.Induction.helperGen]
registered [in MetaCoq.Induction.helperGen_test]

---

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

(945 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

(18 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

(6 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

(43 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

(30 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

(133 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

(335 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

(6 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

(12 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

(95 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

(8 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

(11 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

(2 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

(241 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

(5 entries)

Generated by coqdoc and improved with CoqdocJS