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)

---

P (lemma)

params_subslet [in MetaCoq.PCUIC.PCUICNormal]
PathOf_proper_weight [in MetaCoq.Template.common.uGraph]
PathOf_proper [in MetaCoq.Template.common.uGraph]
pcuic_to_template [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
pcuic_consistent [in MetaCoq.SafeChecker.PCUICConsistency]
pcuic_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
permute_lift0 [in MetaCoq.Erasure.ELiftSubst]
permute_lift [in MetaCoq.Erasure.ELiftSubst]
permute_lift0 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
permute_lift [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
permute_lift0 [in MetaCoq.Template.LiftSubst]
permute_lift [in MetaCoq.Template.LiftSubst]
pick_hyp_def [in MetaCoq.Examples.tauto]
plookup_env_extends [in MetaCoq.PCUIC.PCUICFirstorder]
plookup_env_Some_not_fresh [in MetaCoq.PCUIC.PCUICFirstorder]
plookup_env_lookup_env [in MetaCoq.PCUIC.PCUICFirstorder]
plus_minus' [in MetaCoq.PCUIC.Syntax.PCUICClosed]
poscat_valid [in MetaCoq.PCUIC.Syntax.PCUICPosition]
poscat_atpos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_stack_pos_xpos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_xposition_inv [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_context_position_inv [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_poscat_nonil [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_trans [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_poscat [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positive_cstr_closed_indices' [in MetaCoq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_args [in MetaCoq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_args_subst_arities [in MetaCoq.PCUIC.PCUICInductiveInversion]
positive_cstr_arg_subst [in MetaCoq.PCUIC.PCUICInductiveInversion]
positive_cstr_arg_subst_instance [in MetaCoq.PCUIC.PCUICInductiveInversion]
positive_cstr_closed_indices [in MetaCoq.PCUIC.PCUICInductiveInversion]
positive_cstr_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICInductiveInversion]
positive_cstr_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_arg_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
positive_cstr_smash_middle [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
posR_trans [in MetaCoq.PCUIC.Syntax.PCUICPosition]
posR_Acc [in MetaCoq.PCUIC.Syntax.PCUICPosition]
precompose_subst_instance_global [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
precompose_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
pred_atom_inst [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_red [in MetaCoq.PCUIC.PCUICConfluence]
pred_rel_confluent [in MetaCoq.PCUIC.PCUICConfluence]
pred_on_free_vars [in MetaCoq.PCUIC.PCUICConfluence]
pred_subst_rho_fix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred_subst_rho_cofix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred_mkApps [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred_snd_nth [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred_atom_mkApps [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_subst_context [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_subst_up [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_subst_Upn [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_subst_vdef_Up [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_subst_Up [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_subst_ext [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_subst_pred1_ctx [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_rename [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_ctx_over_refl [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_refl [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_ctx_refl [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_refl_gen [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_pred1_ctx [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_ind_all_ctx [in MetaCoq.PCUIC.PCUICParallelReduction]
pred1_rel_alpha_confluent [in MetaCoq.PCUIC.PCUICConfluence]
pred1_upto_names [in MetaCoq.PCUIC.PCUICConfluence]
pred1_ctx_upto_names [in MetaCoq.PCUIC.PCUICConfluence]
pred1_upto_names_gen [in MetaCoq.PCUIC.PCUICConfluence]
pred1_rel_alpha_red1_rel_alpha [in MetaCoq.PCUIC.PCUICConfluence]
pred1_red' [in MetaCoq.PCUIC.PCUICConfluence]
pred1_ctx_red_ctx [in MetaCoq.PCUIC.PCUICConfluence]
pred1_rel_confluent [in MetaCoq.PCUIC.PCUICConfluence]
pred1_on_free_vars_on_free_vars_ctx [in MetaCoq.PCUIC.PCUICConfluence]
pred1_red_r [in MetaCoq.PCUIC.PCUICConfluence]
pred1_pred1_r' [in MetaCoq.PCUIC.PCUICConfluence]
pred1_pred1_r [in MetaCoq.PCUIC.PCUICConfluence]
pred1_red_r_gen' [in MetaCoq.PCUIC.PCUICConfluence]
pred1_red_r_gen [in MetaCoq.PCUIC.PCUICConfluence]
pred1_red [in MetaCoq.PCUIC.PCUICConfluence]
pred1_ctx_pred1_inv [in MetaCoq.PCUIC.PCUICConfluence]
pred1_ctx_over_assumption_context [in MetaCoq.PCUIC.PCUICConfluence]
pred1_ctx_assumption_context [in MetaCoq.PCUIC.PCUICConfluence]
pred1_ctx_pred1 [in MetaCoq.PCUIC.PCUICConfluence]
pred1_diamond [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_ctx_over_inst_case_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_ctx_over_refl_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_expand_lets [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_ext [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_subst_consn [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_rho_fix_context_2 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_fix_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_mfix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_over_on_ctx_free_vars [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_ctx [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_ctx_free_vars [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_on_free_vars_mfix_ind [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tCoFix_refl_inv [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tCoFix_inv [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tFix_refl_inv [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tFix_inv [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tConst_axiom [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tRel [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tInd [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_refl_tConstruct [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pred1_mkApps_tConstruct [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
preserves_wUnivalence [in MetaCoq.Translations.times_bool_fun]
preserves_UIP [in MetaCoq.Translations.times_bool_fun]
pres_let_bodies_ctx_refl [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
pres_let_bodies_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
pres_let_bodies_assumption_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
pres_bodies_rename' [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pres_bodies_rename [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pres_bodies_inst_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
pre_case_predicate_context_gen_eq [in MetaCoq.PCUIC.PCUICElimination]
pre_case_branch_context_eq [in MetaCoq.PCUIC.PCUICInductiveInversion]
pre_case_branch_context_length_args [in MetaCoq.PCUIC.PCUICCasesContexts]
pre_type_mkApps_arity [in MetaCoq.PCUIC.PCUICSpine]
principal_types [in MetaCoq.SafeChecker.PCUICSafeRetyping]
principal_type_ind [in MetaCoq.PCUIC.PCUICPrincipality]
principal_type [in MetaCoq.PCUIC.PCUICPrincipality]
principal_type [in MetaCoq.PCUIC.Bidirectional.BDUnique]
product_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
prod_ind [in MetaCoq.PCUIC.PCUICConfluence]
Prod_conv_cum_inv [in MetaCoq.PCUIC.PCUICConversion]
progress [in MetaCoq.PCUIC.PCUICProgress]
projection_subslet [in MetaCoq.PCUIC.PCUICInductives]
projection_cumulative_indices [in MetaCoq.PCUIC.PCUICInductiveInversion]
projection_context_gen_inst [in MetaCoq.PCUIC.PCUICInductiveInversion]
projs_subst_above [in MetaCoq.PCUIC.PCUICInductives]
projs_subst_instance [in MetaCoq.PCUIC.PCUICInductives]
projs_inst_lift [in MetaCoq.PCUIC.PCUICInductives]
projs_inst_length [in MetaCoq.PCUIC.PCUICInductives]
projs_inst_skipn [in MetaCoq.PCUIC.PCUICInductives]
projs_inst_subst [in MetaCoq.PCUIC.PCUICInductives]
projs_inst_0 [in MetaCoq.PCUIC.PCUICInductiveInversion]
Proj_Construct_ind_eq [in MetaCoq.PCUIC.PCUICSafeLemmata]
Proj_red_cond [in MetaCoq.PCUIC.PCUICSafeLemmata]
Proj_Construct_ind_eq [in MetaCoq.PCUIC.PCUICInductiveInversion]
prop_sort_eq [in MetaCoq.PCUIC.PCUICCumulProp]
psubst_pred1_subst [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_nth_error_None [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_nth_error' [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_nth_error [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_length' [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_length [in MetaCoq.PCUIC.PCUICParallelReduction]

---

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