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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(32 entries)

---

Global Index

A

ab [constructor, in SN.expressions]
ab_ [definition, in SN.expressions]
ap [definition, in fintype]
ap [definition, in SN.unscoped]
apc [definition, in fintype]
apc [definition, in SN.unscoped]
app [constructor, in Counting.section2_count]
App [definition, in GDTC.features]
app [constructor, in GDTC.features]
app [constructor, in Counting.section2_count_metacoq]
app [constructor, in SN.expressions]
app_ [definition, in Counting.section2_count]
app_ [definition, in Counting.section2_count_metacoq]
app_ [definition, in SN.expressions]
Arith [section, in Counting.section2_count]
Arith [section, in GDTC.features]
arith [module, in Counting.section2_count_metacoq]
Arith [section, in Counting.section2_count_metacoq]
arith_features [instance, in Counting.section2_count_metacoq]
Arith.count [variable, in Counting.section2_count]
Arith.count_gt [variable, in Counting.section2_count]
Arith.E [variable, in GDTC.features]
Arith.exp [variable, in Counting.section2_count]
Arith.exp [variable, in Counting.section2_count_metacoq]
Arith.T [variable, in GDTC.features]
Arith.V [variable, in GDTC.features]
Arr [constructor, in GDTC.features]
arr [constructor, in SN.expressions]
arr_ [definition, in SN.expressions]
atom [constructor, in TypeSafetyAgda.extensible_array]
atom_ [definition, in TypeSafetyAgda.extensible_array]
axioms [library]
axioms [library]

B

beq [definition, in GDTC.miniML_results]
beq [definition, in GDTC.miniML_nofix_results]
beq_correct [lemma, in GDTC.miniML_results]
beq_correct [lemma, in GDTC.miniML_nofix_results]
beq_ty_arith [definition, in GDTC.GDTC]
beq_ty_bool [definition, in GDTC.GDTC]
beq_ty_lam [definition, in GDTC.GDTC]
Bool [constructor, in GDTC.features]
bool [section, in Counting.section2_count_metacoq]
Boolean [constructor, in GDTC.features]
Booleans [section, in GDTC.features]
booleans [module, in Counting.section2_count_metacoq]
Booleans.E [variable, in GDTC.features]
Booleans.T [variable, in GDTC.features]
Booleans.V [variable, in GDTC.features]
boolTy [constructor, in SN.expressions]
boolTy_ [definition, in SN.expressions]
bool_features [instance, in Counting.section2_count_metacoq]
bool.exp [variable, in Counting.section2_count_metacoq]
buildImp [definition, in header_metacoq]
Bundle [record, in header_extensible]

C

Case [constructor, in GDTC.features]
Clos [constructor, in GDTC.features]
close_ren [lemma, in SN.sn_lam]
cns [definition, in header_metacoq]
cod [definition, in SN.axioms]
cod_comp [definition, in SN.axioms]
cod_ext [definition, in SN.axioms]
cod_id [definition, in SN.axioms]
cod_map [definition, in SN.axioms]
CommaNotation [module, in fintype]
_ , _ (subst_scope) [notation, in fintype]
comp [definition, in fintype]
compComp_exp' [lemma, in SN.expressions]
compComp_exp [lemma, in SN.expressions]
compComp_exp_var [lemma, in SN.expressions]
compComp_exp_case [lemma, in SN.expressions]
compComp_exp_bool [lemma, in SN.expressions]
compComp_exp_arith [lemma, in SN.expressions]
compComp_exp_lam [lemma, in SN.expressions]
compComp_exp [lemma, in SN.sn_lam]
compComp'_exp_var [lemma, in SN.expressions]
compComp'_exp_case [lemma, in SN.expressions]
compComp'_exp_bool [lemma, in SN.expressions]
compComp'_exp_arith [lemma, in SN.expressions]
compComp'_exp_lam [lemma, in SN.expressions]
compComp'_exp [lemma, in SN.sn_lam]
compose_fixpoint [definition, in header_metacoq]
compRenRen_exp [definition, in SN.expressions]
compRenRen_exp_var [definition, in SN.expressions]
compRenRen_exp_case [definition, in SN.expressions]
compRenRen_exp_bool [definition, in SN.expressions]
compRenRen_exp_arith [definition, in SN.expressions]
compRenRen_exp_lam [definition, in SN.expressions]
compRenSubst_exp [definition, in SN.expressions]
compRenSubst_exp_var [definition, in SN.expressions]
compRenSubst_exp_case [definition, in SN.expressions]
compRenSubst_exp_bool [definition, in SN.expressions]
compRenSubst_exp_arith [definition, in SN.expressions]
compRenSubst_exp_lam [definition, in SN.expressions]
compRen_exp [lemma, in SN.expressions]
compRen_exp_var [lemma, in SN.expressions]
compRen_exp_case [lemma, in SN.expressions]
compRen_exp_bool [lemma, in SN.expressions]
compRen_exp_arith [lemma, in SN.expressions]
compRen_exp_lam [lemma, in SN.expressions]
compRen_exp [lemma, in SN.sn_lam]
compRen'_exp [lemma, in SN.expressions]
compRen'_exp_var [lemma, in SN.expressions]
compRen'_exp_case [lemma, in SN.expressions]
compRen'_exp_bool [lemma, in SN.expressions]
compRen'_exp_arith [lemma, in SN.expressions]
compRen'_exp_lam [lemma, in SN.expressions]
compRen'_exp [lemma, in SN.sn_lam]
compSubstRen_exp [definition, in SN.expressions]
compSubstRen_exp_var [definition, in SN.expressions]
compSubstRen_exp_case [definition, in SN.expressions]
compSubstRen_exp_bool [definition, in SN.expressions]
compSubstRen_exp_arith [definition, in SN.expressions]
compSubstRen_exp_lam [definition, in SN.expressions]
compSubstSubst_exp [definition, in SN.expressions]
compSubstSubst_exp_var [definition, in SN.expressions]
compSubstSubst_exp_case [definition, in SN.expressions]
compSubstSubst_exp_bool [definition, in SN.expressions]
compSubstSubst_exp_arith [definition, in SN.expressions]
compSubstSubst_exp_lam [definition, in SN.expressions]
congr_inj [lemma, in header_extensible]
congr_In_exp_arith [lemma, in SN.expressions]
congr_In_exp_bool [lemma, in SN.expressions]
congr_In_exp_lam [lemma, in SN.expressions]
congr_In_exp_var [lemma, in SN.expressions]
congr_var_ [lemma, in SN.expressions]
congr_natCase_ [lemma, in SN.expressions]
congr_If_ [lemma, in SN.expressions]
congr_constBool_ [lemma, in SN.expressions]
congr_constNat_ [lemma, in SN.expressions]
congr_plus_ [lemma, in SN.expressions]
congr_app_ [lemma, in SN.expressions]
congr_ab_ [lemma, in SN.expressions]
congr_In_ty_arith [lemma, in SN.expressions]
congr_In_ty_bool [lemma, in SN.expressions]
congr_In_ty_lam [lemma, in SN.expressions]
congr_natTy_ [lemma, in SN.expressions]
congr_boolTy_ [lemma, in SN.expressions]
congr_arr_ [lemma, in SN.expressions]
congr_In_exp_opt [lemma, in TypeSafetyAgda.extensible_array]
congr_In_exp_arr [lemma, in TypeSafetyAgda.extensible_array]
congr_In_exp_plus [lemma, in TypeSafetyAgda.extensible_array]
congr_wr_ [lemma, in TypeSafetyAgda.extensible_array]
congr_rd_ [lemma, in TypeSafetyAgda.extensible_array]
congr_nil_ [lemma, in TypeSafetyAgda.extensible_array]
congr_some_ [lemma, in TypeSafetyAgda.extensible_array]
congr_none_ [lemma, in TypeSafetyAgda.extensible_array]
congr_plus_ [lemma, in TypeSafetyAgda.extensible_array]
congr_atom_ [lemma, in TypeSafetyAgda.extensible_array]
congr_TNat [lemma, in TypeSafetyAgda.extensible_array]
congr_TOption [lemma, in TypeSafetyAgda.extensible_array]
congr_TArray [lemma, in TypeSafetyAgda.extensible_array]
constBool [constructor, in Counting.section2_count]
constBool [constructor, in GDTC.features]
constBool [constructor, in Counting.section2_count_metacoq]
constBool [constructor, in SN.expressions]
constBool_ [definition, in Counting.section2_count]
constBool_ [definition, in Counting.section2_count_metacoq]
constBool_ [definition, in SN.expressions]
constNat [constructor, in Counting.section2_count]
constNat [constructor, in Counting.section2_count_metacoq]
constNat [constructor, in SN.expressions]
constNat_ [definition, in Counting.section2_count]
constNat_ [definition, in Counting.section2_count_metacoq]
constNat_ [definition, in SN.expressions]
count [section, in Counting.section2_count]
Count_gt'_bool [lemma, in Counting.section2_count]
Count_gt'_lam [lemma, in Counting.section2_count]
count_gt'_bool [lemma, in Counting.section2_count]
count_gt'_lam [lemma, in Counting.section2_count]
count_gt'_var [lemma, in Counting.section2_count]
count_again.count [variable, in Counting.section2_count]
count_again.exp [variable, in Counting.section2_count]
count_again [section, in Counting.section2_count]
Count_gt_arith [definition, in Counting.section2_count]
Count_arith [definition, in Counting.section2_count]
count_gt_arith [lemma, in Counting.section2_count]
count_arith [definition, in Counting.section2_count]
Count_gt_bool [definition, in Counting.section2_count]
Count_bool [definition, in Counting.section2_count]
Count_gt_lam [definition, in Counting.section2_count]
Count_lam [definition, in Counting.section2_count]
count_gt_bool [lemma, in Counting.section2_count]
count_gt_lam [lemma, in Counting.section2_count]
count_gt_var [lemma, in Counting.section2_count]
count_bool [definition, in Counting.section2_count]
count_lam [definition, in Counting.section2_count]
count_var [definition, in Counting.section2_count]
count_again.booleans [module, in Counting.section2_count_metacoq]
count_again.lambdas [module, in Counting.section2_count_metacoq]
count_again.count_gt'_var [lemma, in Counting.section2_count_metacoq]
count_again.count_var [definition, in Counting.section2_count_metacoq]
count_again.sec.exp [variable, in Counting.section2_count_metacoq]
count_again.sec [section, in Counting.section2_count_metacoq]
count_again [module, in Counting.section2_count_metacoq]
count_var [definition, in Counting.section2_count_metacoq]
count.count [variable, in Counting.section2_count]
count.count_gt [variable, in Counting.section2_count]
count.exp [variable, in Counting.section2_count]

D

defs [library]
destArity [definition, in header_metacoq]

E

E [definition, in SN.sn]
eval [definition, in GDTC.miniML_results]
eval [definition, in GDTC.miniML_nofix_results]
eval [inductive, in TypeSafetyAgda.TypeSafety]
eval_in_opt [constructor, in TypeSafetyAgda.TypeSafety]
eval_in_arr [constructor, in TypeSafetyAgda.TypeSafety]
eval_in_plus [constructor, in TypeSafetyAgda.TypeSafety]
eval_arr [inductive, in TypeSafetyAgda.TypeSafety]
eval_opt [inductive, in TypeSafetyAgda.TypeSafety]
eval_plus [inductive, in TypeSafetyAgda.TypeSafety]
eval_fix [definition, in GDTC.GDTC]
eval_case [definition, in GDTC.GDTC]
eval_arith [definition, in GDTC.GDTC]
eval_bool [definition, in GDTC.GDTC]
eval1 [lemma, in GDTC.miniML_results]
eval1 [lemma, in GDTC.miniML_nofix_results]
eval2 [lemma, in GDTC.miniML_results]
eval2 [lemma, in GDTC.miniML_nofix_results]
eval3 [lemma, in GDTC.miniML_results]
eval3 [lemma, in GDTC.miniML_nofix_results]
eval4 [lemma, in GDTC.miniML_results]
eval4 [lemma, in GDTC.miniML_nofix_results]
eval5 [lemma, in GDTC.miniML_results]
exp [inductive, in GDTC.miniML]
exp [inductive, in GDTC.miniML_nofix]
exp [inductive, in SN.expressions]
exp [section, in SN.expressions]
exp [inductive, in TypeSafetyAgda.extensible_array]
exp [section, in TypeSafetyAgda.extensible_array]
expressions [library]
Exp_bool_induction [definition, in Counting.section2_count]
Exp_lam_induction [definition, in Counting.section2_count]
Exp_arith [inductive, in Counting.section2_count]
Exp_bool [inductive, in Counting.section2_count]
Exp_lam [inductive, in Counting.section2_count]
exp_arith [inductive, in Counting.section2_count]
exp_bool [inductive, in Counting.section2_count]
exp_lam [inductive, in Counting.section2_count]
exp_var [inductive, in Counting.section2_count]
exp_fix [inductive, in GDTC.features]
exp_case [inductive, in GDTC.features]
exp_arith [inductive, in GDTC.features]
exp_bool [inductive, in GDTC.features]
exp_lam [inductive, in GDTC.features]
exp_fix_C [constructor, in GDTC.miniML]
exp_case_C [constructor, in GDTC.miniML]
exp_arith_C [constructor, in GDTC.miniML]
exp_bool_C [constructor, in GDTC.miniML]
exp_lam_C [constructor, in GDTC.miniML]
exp_case_C [constructor, in GDTC.miniML_nofix]
exp_arith_C [constructor, in GDTC.miniML_nofix]
exp_bool_C [constructor, in GDTC.miniML_nofix]
exp_lam_C [constructor, in GDTC.miniML_nofix]
exp_features [instance, in TypeSafetyAgda.TypeSafety]
Exp_bool_induction [definition, in Counting.section2_count_metacoq]
Exp_lam_induction [definition, in Counting.section2_count_metacoq]
Exp_arith [inductive, in Counting.section2_count_metacoq]
Exp_bool [inductive, in Counting.section2_count_metacoq]
Exp_lam [inductive, in Counting.section2_count_metacoq]
exp_arith [inductive, in Counting.section2_count_metacoq]
exp_bool [inductive, in Counting.section2_count_metacoq]
exp_lam [inductive, in Counting.section2_count_metacoq]
exp_var [inductive, in Counting.section2_count_metacoq]
exp_features [instance, in SN.sn]
exp_var.retract_subst_exp [variable, in SN.expressions]
exp_var.retract_ren_exp [variable, in SN.expressions]
exp_var.rinst_inst_exp [variable, in SN.expressions]
exp_var.rinstInst_up_exp_exp [variable, in SN.expressions]
exp_var.compSubstSubst_exp [variable, in SN.expressions]
exp_var.up_subst_subst_exp_exp [variable, in SN.expressions]
exp_var.compSubstRen_exp [variable, in SN.expressions]
exp_var.up_subst_ren_exp_exp [variable, in SN.expressions]
exp_var.compRenSubst_exp [variable, in SN.expressions]
exp_var.up_ren_subst_exp_exp [variable, in SN.expressions]
exp_var.compRenRen_exp [variable, in SN.expressions]
exp_var.up_ren_ren_exp_exp [variable, in SN.expressions]
exp_var.ext_exp [variable, in SN.expressions]
exp_var.upExt_exp_exp [variable, in SN.expressions]
exp_var.extRen_exp [variable, in SN.expressions]
exp_var.upExtRen_exp_exp [variable, in SN.expressions]
exp_var.idSubst_exp [variable, in SN.expressions]
exp_var.upId_exp_exp [variable, in SN.expressions]
exp_var.subst_exp [variable, in SN.expressions]
exp_var.up_exp_exp [variable, in SN.expressions]
exp_var.ren_exp [variable, in SN.expressions]
exp_var.upRen_exp_exp [variable, in SN.expressions]
exp_var.retract_exp_var [variable, in SN.expressions]
exp_var [inductive, in SN.expressions]
exp_var.exp [variable, in SN.expressions]
exp_var [section, in SN.expressions]
exp_case.retract_subst_exp [variable, in SN.expressions]
exp_case.retract_ren_exp [variable, in SN.expressions]
exp_case.retract_exp_case [variable, in SN.expressions]
exp_case [inductive, in SN.expressions]
exp_case.rinst_inst_exp [variable, in SN.expressions]
exp_case.rinstInst_up_exp_exp [variable, in SN.expressions]
exp_case.compSubstSubst_exp [variable, in SN.expressions]
exp_case.up_subst_subst_exp_exp [variable, in SN.expressions]
exp_case.compSubstRen_exp [variable, in SN.expressions]
exp_case.up_subst_ren_exp_exp [variable, in SN.expressions]
exp_case.compRenSubst_exp [variable, in SN.expressions]
exp_case.up_ren_subst_exp_exp [variable, in SN.expressions]
exp_case.compRenRen_exp [variable, in SN.expressions]
exp_case.up_ren_ren_exp_exp [variable, in SN.expressions]
exp_case.ext_exp [variable, in SN.expressions]
exp_case.upExt_exp_exp [variable, in SN.expressions]
exp_case.extRen_exp [variable, in SN.expressions]
exp_case.upExtRen_exp_exp [variable, in SN.expressions]
exp_case.idSubst_exp [variable, in SN.expressions]
exp_case.upId_exp_exp [variable, in SN.expressions]
exp_case.subst_exp [variable, in SN.expressions]
exp_case.up_exp_exp [variable, in SN.expressions]
exp_case.ren_exp [variable, in SN.expressions]
exp_case.upRen_exp_exp [variable, in SN.expressions]
exp_case.var_exp [variable, in SN.expressions]
exp_case.exp [variable, in SN.expressions]
exp_case [section, in SN.expressions]
exp_bool.retract_subst_exp [variable, in SN.expressions]
exp_bool.retract_ren_exp [variable, in SN.expressions]
exp_bool.retract_exp_bool [variable, in SN.expressions]
exp_bool [inductive, in SN.expressions]
exp_bool.rinst_inst_exp [variable, in SN.expressions]
exp_bool.rinstInst_up_exp_exp [variable, in SN.expressions]
exp_bool.compSubstSubst_exp [variable, in SN.expressions]
exp_bool.up_subst_subst_exp_exp [variable, in SN.expressions]
exp_bool.compSubstRen_exp [variable, in SN.expressions]
exp_bool.up_subst_ren_exp_exp [variable, in SN.expressions]
exp_bool.compRenSubst_exp [variable, in SN.expressions]
exp_bool.up_ren_subst_exp_exp [variable, in SN.expressions]
exp_bool.compRenRen_exp [variable, in SN.expressions]
exp_bool.up_ren_ren_exp_exp [variable, in SN.expressions]
exp_bool.ext_exp [variable, in SN.expressions]
exp_bool.upExt_exp_exp [variable, in SN.expressions]
exp_bool.extRen_exp [variable, in SN.expressions]
exp_bool.upExtRen_exp_exp [variable, in SN.expressions]
exp_bool.idSubst_exp [variable, in SN.expressions]
exp_bool.upId_exp_exp [variable, in SN.expressions]
exp_bool.subst_exp [variable, in SN.expressions]
exp_bool.up_exp_exp [variable, in SN.expressions]
exp_bool.ren_exp [variable, in SN.expressions]
exp_bool.upRen_exp_exp [variable, in SN.expressions]
exp_bool.var_exp [variable, in SN.expressions]
exp_bool.exp [variable, in SN.expressions]
exp_bool [section, in SN.expressions]
exp_arith.retract_subst_exp [variable, in SN.expressions]
exp_arith.retract_ren_exp [variable, in SN.expressions]
exp_arith.retract_exp_arith [variable, in SN.expressions]
exp_arith [inductive, in SN.expressions]
exp_arith.rinst_inst_exp [variable, in SN.expressions]
exp_arith.rinstInst_up_exp_exp [variable, in SN.expressions]
exp_arith.compSubstSubst_exp [variable, in SN.expressions]
exp_arith.up_subst_subst_exp_exp [variable, in SN.expressions]
exp_arith.compSubstRen_exp [variable, in SN.expressions]
exp_arith.up_subst_ren_exp_exp [variable, in SN.expressions]
exp_arith.compRenSubst_exp [variable, in SN.expressions]
exp_arith.up_ren_subst_exp_exp [variable, in SN.expressions]
exp_arith.compRenRen_exp [variable, in SN.expressions]
exp_arith.up_ren_ren_exp_exp [variable, in SN.expressions]
exp_arith.ext_exp [variable, in SN.expressions]
exp_arith.upExt_exp_exp [variable, in SN.expressions]
exp_arith.extRen_exp [variable, in SN.expressions]
exp_arith.upExtRen_exp_exp [variable, in SN.expressions]
exp_arith.idSubst_exp [variable, in SN.expressions]
exp_arith.upId_exp_exp [variable, in SN.expressions]
exp_arith.subst_exp [variable, in SN.expressions]
exp_arith.up_exp_exp [variable, in SN.expressions]
exp_arith.ren_exp [variable, in SN.expressions]
exp_arith.upRen_exp_exp [variable, in SN.expressions]
exp_arith.var_exp [variable, in SN.expressions]
exp_arith.exp [variable, in SN.expressions]
exp_arith [section, in SN.expressions]
exp_lam.retract_subst_exp [variable, in SN.expressions]
exp_lam.retract_ren_exp [variable, in SN.expressions]
exp_lam.retract_exp_lam [variable, in SN.expressions]
exp_lam [inductive, in SN.expressions]
exp_lam.rinst_inst_exp [variable, in SN.expressions]
exp_lam.rinstInst_up_exp_exp [variable, in SN.expressions]
exp_lam.compSubstSubst_exp [variable, in SN.expressions]
exp_lam.up_subst_subst_exp_exp [variable, in SN.expressions]
exp_lam.compSubstRen_exp [variable, in SN.expressions]
exp_lam.up_subst_ren_exp_exp [variable, in SN.expressions]
exp_lam.compRenSubst_exp [variable, in SN.expressions]
exp_lam.up_ren_subst_exp_exp [variable, in SN.expressions]
exp_lam.compRenRen_exp [variable, in SN.expressions]
exp_lam.up_ren_ren_exp_exp [variable, in SN.expressions]
exp_lam.ext_exp [variable, in SN.expressions]
exp_lam.upExt_exp_exp [variable, in SN.expressions]
exp_lam.extRen_exp [variable, in SN.expressions]
exp_lam.upExtRen_exp_exp [variable, in SN.expressions]
exp_lam.idSubst_exp [variable, in SN.expressions]
exp_lam.upId_exp_exp [variable, in SN.expressions]
exp_lam.subst_exp [variable, in SN.expressions]
exp_lam.up_exp_exp [variable, in SN.expressions]
exp_lam.ren_exp [variable, in SN.expressions]
exp_lam.upRen_exp_exp [variable, in SN.expressions]
exp_lam.var_exp [variable, in SN.expressions]
exp_lam.exp [variable, in SN.expressions]
exp_lam.ty [variable, in SN.expressions]
exp_lam [section, in SN.expressions]
exp_arr.retract_exp_arr [variable, in TypeSafetyAgda.extensible_array]
exp_arr [inductive, in TypeSafetyAgda.extensible_array]
exp_arr.exp [variable, in TypeSafetyAgda.extensible_array]
exp_arr [section, in TypeSafetyAgda.extensible_array]
exp_opt.retract_exp_opt [variable, in TypeSafetyAgda.extensible_array]
exp_opt [inductive, in TypeSafetyAgda.extensible_array]
exp_opt.exp [variable, in TypeSafetyAgda.extensible_array]
exp_opt [section, in TypeSafetyAgda.extensible_array]
exp_plus.retract_exp_plus [variable, in TypeSafetyAgda.extensible_array]
exp_plus [inductive, in TypeSafetyAgda.extensible_array]
exp_plus.exp [variable, in TypeSafetyAgda.extensible_array]
exp_plus [section, in TypeSafetyAgda.extensible_array]
extensible_array [library]
extRen_exp [definition, in SN.expressions]
extRen_exp_var [definition, in SN.expressions]
extRen_exp_case [definition, in SN.expressions]
extRen_exp_bool [definition, in SN.expressions]
extRen_exp_arith [definition, in SN.expressions]
extRen_exp_lam [definition, in SN.expressions]
ext_exp [definition, in SN.expressions]
ext_exp_var [definition, in SN.expressions]
ext_exp_case [definition, in SN.expressions]
ext_exp_bool [definition, in SN.expressions]
ext_exp_arith [definition, in SN.expressions]
ext_exp_lam [definition, in SN.expressions]
E_strong_base [lemma, in SN.sn_var]
E_strong_step [lemma, in SN.sn_var]
E_strong_sn [lemma, in SN.sn_var]
E_strong [definition, in SN.sn_var]
E_strong_In [constructor, in SN.sn_var]
E_strong' [inductive, in SN.sn_var]
E_ [definition, in SN.sn_var]
E_strong_var [lemma, in SN.sn]

F

features [projection, in header_metacoq]
features [constructor, in header_metacoq]
features [library]
fin [definition, in fintype]
fin [abbreviation, in SN.unscoped]
fintype [library]
Fix [section, in GDTC.features]
fixNames [definition, in header_metacoq]
fixp [constructor, in GDTC.features]
Fix.E [variable, in GDTC.features]
Fix.T [variable, in GDTC.features]
Fix.V [variable, in GDTC.features]
Forall [definition, in header_metacoq]
ForallN [definition, in header_metacoq]
Forall' [definition, in header_metacoq]
funcomp [definition, in fintype]
funcomp [definition, in SN.axioms]
funcomp [definition, in SN.unscoped]

G

G [definition, in SN.sn_var]
GDTC [library]
GenCons [constructor, in header_metacoq]
genCons [constructor, in header_metacoq]
genIH [definition, in header_metacoq]
GenList [inductive, in header_metacoq]
genList [inductive, in header_metacoq]
GenNil [constructor, in header_metacoq]
genNil [constructor, in header_metacoq]
genStatement [definition, in header_metacoq]
genStatement_Fix [definition, in header_metacoq]
genStatement_no_lt [definition, in header_metacoq]
getName [definition, in header_metacoq]
get_In [definition, in header_extensible]
get_lemmas_and_name [definition, in header_metacoq]
get_lemmas [definition, in header_metacoq]
get_name [definition, in header_metacoq]
get_name_of [definition, in header_metacoq]
get_features [definition, in header_metacoq]
G_strong [definition, in SN.sn_var]

H

hasty_If [constructor, in SN.sn_bool]
hasty_ConstBool [constructor, in SN.sn_bool]
hasty_plus [constructor, in SN.sn_arith]
hasty_ConstNat [constructor, in SN.sn_arith]
hasty_lam [constructor, in SN.sn_lam]
hasty_app [constructor, in SN.sn_lam]
has_ty_bool [inductive, in SN.sn_bool]
has_ty_arith [inductive, in SN.sn_arith]
has_ty_sem_strong [definition, in SN.sn_var]
has_ty_sem [definition, in SN.sn_var]
has_ty_subst_var [lemma, in SN.sn_var]
has_ty_ren_var [lemma, in SN.sn_var]
has_ty_var [inductive, in SN.sn_var]
has_ty_rev_arith [lemma, in SN.sn]
has_ty_rev_bool [lemma, in SN.sn]
has_ty_rev_lam [lemma, in SN.sn]
has_ty_rev_var [lemma, in SN.sn]
has_ty_features [instance, in SN.sn]
has_ty [inductive, in SN.sn]
has_ty_lam [inductive, in SN.sn_lam]
has_features [record, in header_metacoq]
has_features [inductive, in header_metacoq]
header_extensible [library]
header_metacoq [library]

I

id [definition, in fintype]
id [definition, in SN.unscoped]
idren [definition, in fintype]
ids [projection, in fintype]
ids [constructor, in fintype]
ids [projection, in SN.unscoped]
ids [constructor, in SN.unscoped]
idsRen [instance, in SN.unscoped]
idSubst_exp [definition, in SN.expressions]
idSubst_exp_var [definition, in SN.expressions]
idSubst_exp_case [definition, in SN.expressions]
idSubst_exp_bool [definition, in SN.expressions]
idSubst_exp_arith [definition, in SN.expressions]
idSubst_exp_lam [definition, in SN.expressions]
If [constructor, in Counting.section2_count]
If [constructor, in GDTC.features]
If [constructor, in Counting.section2_count_metacoq]
If [constructor, in SN.expressions]
if_ [definition, in Counting.section2_count]
if_ [definition, in Counting.section2_count_metacoq]
If_ [definition, in SN.expressions]
imp [projection, in tactics]
Imp [record, in tactics]
imp [constructor, in tactics]
Imp [inductive, in tactics]
imprev [projection, in tactics]
ImpRev [record, in tactics]
imprev [constructor, in tactics]
ImpRev [inductive, in tactics]
included [abbreviation, in GDTC.features]
included [abbreviation, in header_extensible]
inj [projection, in Counting.section2_count]
inj [projection, in Counting.section2_count_metacoq]
inj [abbreviation, in header_extensible]
inj_arith_arith [constructor, in Counting.section2_count]
inj_lam_arith [constructor, in Counting.section2_count]
inj_var_arith [constructor, in Counting.section2_count]
inj_bool_bool [constructor, in Counting.section2_count]
inj_lam_bool [constructor, in Counting.section2_count]
inj_var_bool [constructor, in Counting.section2_count]
inj_lam_lam [constructor, in Counting.section2_count]
inj_var_lam [constructor, in Counting.section2_count]
inj_arith_arith [constructor, in Counting.section2_count_metacoq]
inj_lam_arith [constructor, in Counting.section2_count_metacoq]
inj_var_arith [constructor, in Counting.section2_count_metacoq]
inj_bool_bool [constructor, in Counting.section2_count_metacoq]
inj_lam_bool [constructor, in Counting.section2_count_metacoq]
inj_var_bool [constructor, in Counting.section2_count_metacoq]
inj_lam_lam [constructor, in Counting.section2_count_metacoq]
inj_var_lam [constructor, in Counting.section2_count_metacoq]
inl_step_arith [constructor, in SN.sn]
inl_step_bool [constructor, in SN.sn]
inl_step_lam [constructor, in SN.sn]
inl_step_var [constructor, in SN.sn]
inl_has_ty_arith [constructor, in SN.sn]
inl_has_ty_bool [constructor, in SN.sn]
inl_has_ty_lam [constructor, in SN.sn]
inl_has_ty_var [constructor, in SN.sn]
InRelC [record, in header_metacoq]
instId_exp [lemma, in SN.expressions]
instId_exp_var [lemma, in SN.expressions]
instId_exp_case [lemma, in SN.expressions]
instId_exp_bool [lemma, in SN.expressions]
instId_exp_arith [lemma, in SN.expressions]
instId_exp_lam [lemma, in SN.expressions]
instId_exp [lemma, in SN.sn_lam]
in_bool [definition, in Counting.section2_count]
in_lam [definition, in Counting.section2_count]
in_var [definition, in Counting.section2_count]
In_fix [definition, in GDTC.features]
In_case [definition, in GDTC.features]
In_ty_arith [definition, in GDTC.features]
In_arith [definition, in GDTC.features]
In_bool [definition, in GDTC.features]
In_ty_bool [definition, in GDTC.features]
In_ty_lam' [instance, in GDTC.features]
In_lam [definition, in GDTC.features]
In_ty_lam [definition, in GDTC.features]
in_rel_bool [instance, in Counting.section2_count_metacoq]
in_bool [definition, in Counting.section2_count_metacoq]
in_rel_lam [instance, in Counting.section2_count_metacoq]
in_lam [definition, in Counting.section2_count_metacoq]
in_var [definition, in Counting.section2_count_metacoq]
In_exp_arith [constructor, in SN.expressions]
In_exp_bool [constructor, in SN.expressions]
In_exp_lam [constructor, in SN.expressions]
In_exp_var [constructor, in SN.expressions]
In_ty_arith [constructor, in SN.expressions]
In_ty_bool [constructor, in SN.expressions]
In_ty_lam [constructor, in SN.expressions]
in_rel [projection, in header_metacoq]
in_subtype [projection, in header_metacoq]
In_exp_opt [constructor, in TypeSafetyAgda.extensible_array]
In_exp_arr [constructor, in TypeSafetyAgda.extensible_array]
In_exp_plus [constructor, in TypeSafetyAgda.extensible_array]

L

L [inductive, in TypeSafetyAgda.TypeSafety]
L [definition, in SN.sn]
lam [constructor, in Counting.section2_count]
Lam [definition, in GDTC.features]
lam [constructor, in GDTC.features]
lam [section, in Counting.section2_count_metacoq]
lam [constructor, in Counting.section2_count_metacoq]
Lambdas [section, in GDTC.features]
lambdas [module, in Counting.section2_count_metacoq]
Lambdas.E [variable, in GDTC.features]
Lambdas.T [variable, in GDTC.features]
Lambdas.V [variable, in GDTC.features]
lam_ [definition, in Counting.section2_count]
lam_ [definition, in Counting.section2_count_metacoq]
lam_features [instance, in Counting.section2_count_metacoq]
lam.exp [variable, in Counting.section2_count_metacoq]
lift [definition, in header_extensible]
list_comp [definition, in SN.axioms]
list_id [definition, in SN.axioms]
list_ext [definition, in SN.axioms]
lookup [constructor, in TypeSafetyAgda.TypeSafety]
L_close_ren_bool [lemma, in SN.sn_bool]
L_close_ren_arith [lemma, in SN.sn_arith]
L_lemma [lemma, in TypeSafetyAgda.TypeSafety]
L_rec [constructor, in TypeSafetyAgda.TypeSafety]
L_notfound [constructor, in TypeSafetyAgda.TypeSafety]
L_read [constructor, in TypeSafetyAgda.TypeSafety]
L_close_ren [definition, in SN.sn]
L_strong [definition, in SN.sn]
L_ren [definition, in SN.sn]
L_strong_lam [definition, in SN.sn_lam]
L_val_lam [lemma, in SN.sn_lam]

M

make_Bundle [constructor, in header_extensible]
miniML [library]
MiniML_Bool.ren_preserves [variable, in SN.sn_bool]
MiniML_Bool.retract_L_strong [variable, in SN.sn_bool]
MiniML_Bool.whnf_whnf_bool [variable, in SN.sn_bool]
MiniML_Bool.retract_L [variable, in SN.sn_bool]
MiniML_Bool.retract_step_rev [variable, in SN.sn_bool]
MiniML_Bool.retract_step [variable, in SN.sn_bool]
MiniML_Bool.step [variable, in SN.sn_bool]
MiniML_Bool.retract_has_ty_rev [variable, in SN.sn_bool]
MiniML_Bool.retract_has_ty [variable, in SN.sn_bool]
MiniML_Bool.has_ty [variable, in SN.sn_bool]
MiniML_Bool.retract_subst_exp [variable, in SN.sn_bool]
MiniML_Bool.subst_exp [variable, in SN.sn_bool]
MiniML_Bool.retract_ren_exp [variable, in SN.sn_bool]
MiniML_Bool.ren_exp [variable, in SN.sn_bool]
MiniML_Bool.exp [variable, in SN.sn_bool]
MiniML_Bool.ty [variable, in SN.sn_bool]
MiniML_Bool [section, in SN.sn_bool]
MiniML_Arith.step_anti_renaming [variable, in SN.sn_arith]
MiniML_Arith.ren_preserves [variable, in SN.sn_arith]
MiniML_Arith.retract_L_strong [variable, in SN.sn_arith]
MiniML_Arith.whnf_whnf_arith [variable, in SN.sn_arith]
MiniML_Arith.retract_L [variable, in SN.sn_arith]
MiniML_Arith.retract_step_rev [variable, in SN.sn_arith]
MiniML_Arith.retract_step [variable, in SN.sn_arith]
MiniML_Arith.step [variable, in SN.sn_arith]
MiniML_Arith.retract_has_ty_rev [variable, in SN.sn_arith]
MiniML_Arith.retract_has_ty [variable, in SN.sn_arith]
MiniML_Arith.has_ty [variable, in SN.sn_arith]
MiniML_Arith.retract_subst_exp [variable, in SN.sn_arith]
MiniML_Arith.subst_exp [variable, in SN.sn_arith]
MiniML_Arith.retract_ren_exp [variable, in SN.sn_arith]
MiniML_Arith.ren_exp [variable, in SN.sn_arith]
MiniML_Arith.exp [variable, in SN.sn_arith]
MiniML_Arith.ty [variable, in SN.sn_arith]
MiniML_Arith [section, in SN.sn_arith]
MiniML_var.L_strong [variable, in SN.sn_var]
MiniML_var.L [variable, in SN.sn_var]
MiniML_var.ren_preserves [variable, in SN.sn_var]
MiniML_var.whnf_whnf_var [variable, in SN.sn_var]
MiniML_var.step [variable, in SN.sn_var]
MiniML_var.retract_has_ty_rev [variable, in SN.sn_var]
MiniML_var.retract_has_ty [variable, in SN.sn_var]
MiniML_var.has_ty [variable, in SN.sn_var]
MiniML_var.subst_id_exp [variable, in SN.sn_var]
MiniML_var.var_exp [variable, in SN.sn_var]
MiniML_var.retract_subst_exp [variable, in SN.sn_var]
MiniML_var.subst_exp [variable, in SN.sn_var]
MiniML_var.retract_ren_exp [variable, in SN.sn_var]
MiniML_var.ren_exp [variable, in SN.sn_var]
MiniML_var.ty [variable, in SN.sn_var]
MiniML_var.exp [variable, in SN.sn_var]
MiniML_var [section, in SN.sn_var]
MiniML_Lambda.E_strong_var [variable, in SN.sn_lam]
MiniML_Lambda.retract_L_strong [variable, in SN.sn_lam]
MiniML_Lambda.ren_var [variable, in SN.sn_lam]
MiniML_Lambda.ren_preserves [variable, in SN.sn_lam]
MiniML_Lambda.whnf_anti_renaming [variable, in SN.sn_lam]
MiniML_Lambda.L_strong [variable, in SN.sn_lam]
MiniML_Lambda.retract_whnf_lam [variable, in SN.sn_lam]
MiniML_Lambda.retract_L [variable, in SN.sn_lam]
MiniML_Lambda.L [variable, in SN.sn_lam]
MiniML_Lambda.retract_step_rev [variable, in SN.sn_lam]
MiniML_Lambda.retract_step [variable, in SN.sn_lam]
MiniML_Lambda.step [variable, in SN.sn_lam]
MiniML_Lambda.retract_has_ty_rev [variable, in SN.sn_lam]
MiniML_Lambda.retract_has_ty [variable, in SN.sn_lam]
MiniML_Lambda.hasty_var [variable, in SN.sn_lam]
MiniML_Lambda.has_ty [variable, in SN.sn_lam]
MiniML_Lambda.subst_exp_var [variable, in SN.sn_lam]
MiniML_Lambda.up_exp_exp_def' [variable, in SN.sn_lam]
MiniML_Lambda.up_exp_exp_def [variable, in SN.sn_lam]
MiniML_Lambda.upRen_exp_exp_def [variable, in SN.sn_lam]
MiniML_Lambda.retract_subst_exp [variable, in SN.sn_lam]
MiniML_Lambda.retract_ren_exp [variable, in SN.sn_lam]
MiniML_Lambda.rinst_inst_exp [variable, in SN.sn_lam]
MiniML_Lambda.rinstInst_up_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.compSubstSubst_exp [variable, in SN.sn_lam]
MiniML_Lambda.up_subst_subst_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.compSubstRen_exp [variable, in SN.sn_lam]
MiniML_Lambda.up_subst_ren_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.compRenSubst_exp [variable, in SN.sn_lam]
MiniML_Lambda.up_ren_subst_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.compRenRen_exp [variable, in SN.sn_lam]
MiniML_Lambda.up_ren_ren_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.ext_exp [variable, in SN.sn_lam]
MiniML_Lambda.upExt_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.extRen_exp [variable, in SN.sn_lam]
MiniML_Lambda.upExtRen_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.idSubst_exp [variable, in SN.sn_lam]
MiniML_Lambda.upId_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.subst_exp [variable, in SN.sn_lam]
MiniML_Lambda.up_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.ren_exp [variable, in SN.sn_lam]
MiniML_Lambda.upRen_exp_exp [variable, in SN.sn_lam]
MiniML_Lambda.exp [variable, in SN.sn_lam]
MiniML_Lambda.ty [variable, in SN.sn_lam]
MiniML_Lambda [section, in SN.sn_lam]
MiniML_Fix.vtypeis_inj' [variable, in GDTC.GDTC]
MiniML_Fix.vtypeis_inj [variable, in GDTC.GDTC]
MiniML_Fix.vtypeis [variable, in GDTC.GDTC]
MiniML_Fix.typeof_fix_inj' [variable, in GDTC.GDTC]
MiniML_Fix.typeof_fix_inj [variable, in GDTC.GDTC]
MiniML_Fix.beq_correct [variable, in GDTC.GDTC]
MiniML_Fix.typeof [variable, in GDTC.GDTC]
MiniML_Fix.beq [variable, in GDTC.GDTC]
MiniML_Fix.eval [variable, in GDTC.GDTC]
MiniML_Fix.V [variable, in GDTC.GDTC]
MiniML_Fix.E [variable, in GDTC.GDTC]
MiniML_Fix.T [variable, in GDTC.GDTC]
MiniML_Fix [section, in GDTC.GDTC]
MiniML_Case.vtypeis_inj [variable, in GDTC.GDTC]
MiniML_Case.vtypeis [variable, in GDTC.GDTC]
MiniML_Case.typeof [variable, in GDTC.GDTC]
MiniML_Case.beq_correct [variable, in GDTC.GDTC]
MiniML_Case.beq [variable, in GDTC.GDTC]
MiniML_Case.eval [variable, in GDTC.GDTC]
MiniML_Case.V [variable, in GDTC.GDTC]
MiniML_Case.T [variable, in GDTC.GDTC]
MiniML_Case.E [variable, in GDTC.GDTC]
MiniML_Case [section, in GDTC.GDTC]
MiniML_Arith.vtypeis_inj [variable, in GDTC.GDTC]
MiniML_Arith.vtypeis [variable, in GDTC.GDTC]
MiniML_Arith.typeof [variable, in GDTC.GDTC]
MiniML_Arith.beq_correct [variable, in GDTC.GDTC]
MiniML_Arith.beq [variable, in GDTC.GDTC]
MiniML_Arith.eval [variable, in GDTC.GDTC]
MiniML_Arith.T [variable, in GDTC.GDTC]
MiniML_Arith.V [variable, in GDTC.GDTC]
MiniML_Arith.E [variable, in GDTC.GDTC]
MiniML_Arith [section, in GDTC.GDTC]
MiniML_Bool.vtypeis_inj [variable, in GDTC.GDTC]
MiniML_Bool.vtypeis [variable, in GDTC.GDTC]
MiniML_Bool.typeof [variable, in GDTC.GDTC]
MiniML_Bool.beq_correct [variable, in GDTC.GDTC]
MiniML_Bool.beq [variable, in GDTC.GDTC]
MiniML_Bool.eval [variable, in GDTC.GDTC]
MiniML_Bool.V [variable, in GDTC.GDTC]
MiniML_Bool.E [variable, in GDTC.GDTC]
MiniML_Bool.T [variable, in GDTC.GDTC]
MiniML_Bool [section, in GDTC.GDTC]
MiniML_Lambda.vtypeis_inj [variable, in GDTC.GDTC]
MiniML_Lambda.vtypeis [variable, in GDTC.GDTC]
MiniML_Lambda.typeof [variable, in GDTC.GDTC]
MiniML_Lambda.beq_correct [variable, in GDTC.GDTC]
MiniML_Lambda.beq [variable, in GDTC.GDTC]
MiniML_Lambda.V [variable, in GDTC.GDTC]
MiniML_Lambda.E [variable, in GDTC.GDTC]
MiniML_Lambda.T [variable, in GDTC.GDTC]
MiniML_Lambda [section, in GDTC.GDTC]
miniML_results [library]
miniML_nofix [library]
miniML_nofix_results [library]
mkDefinitionType [definition, in header_metacoq]
mkLemma [definition, in header_metacoq]
mkVariable [definition, in header_metacoq]
ModularFixpointN [definition, in header_metacoq]
ModularFixpoint2 [definition, in header_metacoq]
monotone [lemma, in GDTC.miniML_results]
monotone [lemma, in GDTC.miniML_nofix_results]

N

name_after_dot [definition, in header_metacoq]
name_after_dot' [definition, in header_metacoq]
Nat [constructor, in GDTC.features]
NatCase [section, in GDTC.features]
natCase [constructor, in SN.expressions]
natCase_ [definition, in SN.expressions]
NatCase.E [variable, in GDTC.features]
NatCase.T [variable, in GDTC.features]
NatCase.V [variable, in GDTC.features]
natTy [constructor, in SN.expressions]
natTy_ [definition, in SN.expressions]
nat_subterm' [instance, in header_metacoq]
nil [constructor, in TypeSafetyAgda.extensible_array]
nil_ [definition, in TypeSafetyAgda.extensible_array]
none [constructor, in TypeSafetyAgda.extensible_array]
None [definition, in SN.unscoped]
none_ [definition, in TypeSafetyAgda.extensible_array]
null [definition, in fintype]
Num [constructor, in GDTC.features]
Number [constructor, in GDTC.features]

O

ok_ins [constructor, in TypeSafetyAgda.TypeSafety]
ok_lookup [constructor, in TypeSafetyAgda.TypeSafety]
ok_nil [constructor, in TypeSafetyAgda.TypeSafety]
ok_some [constructor, in TypeSafetyAgda.TypeSafety]
ok_none [constructor, in TypeSafetyAgda.TypeSafety]
ok_plus [constructor, in TypeSafetyAgda.TypeSafety]
ok_value [constructor, in TypeSafetyAgda.TypeSafety]
Option [section, in TypeSafetyAgda.TypeSafety]
Option.eval [variable, in TypeSafetyAgda.TypeSafety]
Option.exp [variable, in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty_rev' [variable, in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty' [variable, in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty_rev [variable, in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty [variable, in TypeSafetyAgda.TypeSafety]
Option.wtyped [variable, in TypeSafetyAgda.TypeSafety]

P

pext [axiom, in SN.axioms]
pext [axiom, in axioms]
pi [lemma, in SN.axioms]
pi [lemma, in axioms]
plus [constructor, in Counting.section2_count]
Plus [constructor, in GDTC.features]
Plus [section, in TypeSafetyAgda.TypeSafety]
plus [constructor, in Counting.section2_count_metacoq]
plus [constructor, in SN.expressions]
plus [constructor, in TypeSafetyAgda.extensible_array]
plus_ [definition, in Counting.section2_count]
plus_ [definition, in Counting.section2_count_metacoq]
plus_ [definition, in SN.expressions]
plus_ [definition, in TypeSafetyAgda.extensible_array]
Plus.eval [variable, in TypeSafetyAgda.TypeSafety]
Plus.exp [variable, in TypeSafetyAgda.TypeSafety]
Plus.retract_has_ty_rev [variable, in TypeSafetyAgda.TypeSafety]
Plus.retract_has_ty [variable, in TypeSafetyAgda.TypeSafety]
Plus.wtyped [variable, in TypeSafetyAgda.TypeSafety]
preservation_var [lemma, in SN.sn_var]
prod_comp [definition, in SN.axioms]
prod_ext [definition, in SN.axioms]
prod_id [definition, in SN.axioms]
prod_map [definition, in SN.axioms]

Q

quote_list [definition, in header_metacoq]

R

RClos [constructor, in GDTC.features]
rd [constructor, in TypeSafetyAgda.extensible_array]
rd_ [definition, in TypeSafetyAgda.extensible_array]
remove_suffix [definition, in header_metacoq]
remove_injs [definition, in header_metacoq]
ren [definition, in fintype]
renComp_exp [lemma, in SN.expressions]
renComp_exp_var [lemma, in SN.expressions]
renComp_exp_case [lemma, in SN.expressions]
renComp_exp_bool [lemma, in SN.expressions]
renComp_exp_arith [lemma, in SN.expressions]
renComp_exp_lam [lemma, in SN.expressions]
renComp_exp [lemma, in SN.sn_lam]
renComp'_exp [lemma, in SN.expressions]
renComp'_exp_var [lemma, in SN.expressions]
renComp'_exp_case [lemma, in SN.expressions]
renComp'_exp_bool [lemma, in SN.expressions]
renComp'_exp_arith [lemma, in SN.expressions]
renComp'_exp_lam [lemma, in SN.expressions]
renComp'_exp [lemma, in SN.sn_lam]
renRen_exp [lemma, in SN.expressions]
renRen_exp_var [lemma, in SN.expressions]
renRen_exp_case [lemma, in SN.expressions]
renRen_exp_bool [lemma, in SN.expressions]
renRen_exp_arith [lemma, in SN.expressions]
renRen_exp_lam [lemma, in SN.expressions]
renRen_exp [lemma, in SN.sn_lam]
renRen'_exp [lemma, in SN.expressions]
renRen'_exp_var [lemma, in SN.expressions]
renRen'_exp_case [lemma, in SN.expressions]
renRen'_exp_bool [lemma, in SN.expressions]
renRen'_exp_arith [lemma, in SN.expressions]
renRen'_exp_lam [lemma, in SN.expressions]
renRen'_exp [lemma, in SN.sn_lam]
ren_preserves_constBool [lemma, in SN.sn_bool]
ren_preserves_If [lemma, in SN.sn_bool]
ren_preserves_constNat [lemma, in SN.sn_arith]
ren_preserves_Plus [lemma, in SN.sn_arith]
ren_preserves_var [lemma, in SN.sn_var]
ren_preserves_arith [lemma, in SN.sn]
ren_preserves_bool [lemma, in SN.sn]
ren_preserves_lam [lemma, in SN.sn]
ren_preserves [lemma, in SN.sn]
Ren_exp [instance, in SN.expressions]
ren_exp [definition, in SN.expressions]
ren_exp_var [definition, in SN.expressions]
ren_exp_case [definition, in SN.expressions]
ren_exp_bool [definition, in SN.expressions]
ren_exp_arith [definition, in SN.expressions]
ren_exp_lam [definition, in SN.expressions]
ren_preserves_app [lemma, in SN.sn_lam]
ren_preserves_ab [lemma, in SN.sn_lam]
ren1 [projection, in fintype]
Ren1 [record, in fintype]
ren1 [constructor, in fintype]
Ren1 [inductive, in fintype]
ren1 [projection, in SN.unscoped]
Ren1 [record, in SN.unscoped]
ren1 [constructor, in SN.unscoped]
Ren1 [inductive, in SN.unscoped]
ren2 [projection, in fintype]
Ren2 [record, in fintype]
ren2 [constructor, in fintype]
Ren2 [inductive, in fintype]
ren2 [projection, in SN.unscoped]
Ren2 [record, in SN.unscoped]
ren2 [constructor, in SN.unscoped]
Ren2 [inductive, in SN.unscoped]
ren3 [projection, in fintype]
Ren3 [record, in fintype]
ren3 [constructor, in fintype]
Ren3 [inductive, in fintype]
ren3 [projection, in SN.unscoped]
Ren3 [record, in SN.unscoped]
ren3 [constructor, in SN.unscoped]
Ren3 [inductive, in SN.unscoped]
ren4 [projection, in fintype]
Ren4 [record, in fintype]
ren4 [constructor, in fintype]
Ren4 [inductive, in fintype]
ren4 [projection, in SN.unscoped]
Ren4 [record, in SN.unscoped]
ren4 [constructor, in SN.unscoped]
Ren4 [inductive, in SN.unscoped]
ren5 [projection, in fintype]
Ren5 [record, in fintype]
ren5 [constructor, in fintype]
Ren5 [inductive, in fintype]
ren5 [projection, in SN.unscoped]
Ren5 [record, in SN.unscoped]
ren5 [constructor, in SN.unscoped]
Ren5 [inductive, in SN.unscoped]
replace_ext [definition, in header_metacoq]
replace_consts [definition, in header_metacoq]
replace_terms [definition, in header_metacoq]
replace_const [definition, in header_metacoq]
replace_term [definition, in header_metacoq]
retr [projection, in Counting.section2_count]
retr [projection, in Counting.section2_count_metacoq]
retr [abbreviation, in header_extensible]
retract [record, in Counting.section2_count]
retract [record, in Counting.section2_count_metacoq]
retract [record, in header_extensible]
retract_bool_bool [instance, in Counting.section2_count]
retract_lam_bool [instance, in Counting.section2_count]
retract_var_bool [instance, in Counting.section2_count]
retract_lam_lam [instance, in Counting.section2_count]
retract_var_lam [instance, in Counting.section2_count]
retract_inj [lemma, in Counting.section2_count]
retract_tight [projection, in Counting.section2_count]
retract_works [projection, in Counting.section2_count]
retract_step_rev_instance [instance, in SN.sn_bool]
retract_step_instance [instance, in SN.sn_bool]
retract_has_ty_rev_instance [instance, in SN.sn_bool]
retract_has_ty_instance [instance, in SN.sn_bool]
retract_step_rev_instance [instance, in SN.sn_arith]
retract_step_instance [instance, in SN.sn_arith]
retract_has_ty_rev_instance [instance, in SN.sn_arith]
retract_has_ty_instance [instance, in SN.sn_arith]
retract_has_ty_rev_instance [instance, in SN.sn_var]
retract_has_ty_instance [instance, in SN.sn_var]
retract_has_ty_rev_instance' [instance, in TypeSafetyAgda.TypeSafety]
retract_has_ty_instance' [instance, in TypeSafetyAgda.TypeSafety]
retract_has_ty_rev_instance_opt [instance, in TypeSafetyAgda.TypeSafety]
retract_has_ty_instance_opt [instance, in TypeSafetyAgda.TypeSafety]
retract_has_ty_rev_instance [instance, in TypeSafetyAgda.TypeSafety]
retract_has_ty_instance [instance, in TypeSafetyAgda.TypeSafety]
retract_bool_bool [instance, in Counting.section2_count_metacoq]
retract_lam_bool [instance, in Counting.section2_count_metacoq]
retract_var_bool [instance, in Counting.section2_count_metacoq]
retract_lam_lam [instance, in Counting.section2_count_metacoq]
retract_var_lam [instance, in Counting.section2_count_metacoq]
retract_inj [lemma, in Counting.section2_count_metacoq]
retract_tight [projection, in Counting.section2_count_metacoq]
retract_works [projection, in Counting.section2_count_metacoq]
retract_step_arith [lemma, in SN.sn]
retract_step_bool [lemma, in SN.sn]
retract_step_lam [lemma, in SN.sn]
retract_option [instance, in header_extensible]
retract_inj [lemma, in header_extensible]
retract_tight [projection, in header_extensible]
retract_works [projection, in header_extensible]
retract_R [projection, in header_extensible]
retract_I [projection, in header_extensible]
retract_exp_bool_exp [instance, in SN.expressions]
retract_exp_arith_exp [instance, in SN.expressions]
retract_exp_lam_exp [instance, in SN.expressions]
retract_exp_var_exp [instance, in SN.expressions]
retract_ty_arith_ty [instance, in SN.expressions]
retract_ty_bool_ty [instance, in SN.expressions]
retract_ty_lam_ty [instance, in SN.expressions]
retract_step_rev_instance [instance, in SN.sn_lam]
retract_step_instance [instance, in SN.sn_lam]
retract_has_ty_rev_instance [instance, in SN.sn_lam]
retract_has_ty_instance [instance, in SN.sn_lam]
retract_exp_arr_exp [instance, in TypeSafetyAgda.extensible_array]
retract_exp_opt_exp [instance, in TypeSafetyAgda.extensible_array]
retract_exp_plus_exp [instance, in TypeSafetyAgda.extensible_array]
ret_ty_arith [instance, in GDTC.miniML]
ret_ty_bool [instance, in GDTC.miniML]
ret_ty_lam [instance, in GDTC.miniML]
ret_fix_arith [instance, in GDTC.miniML]
ret_value_arith [instance, in GDTC.miniML]
ret_value_bool [instance, in GDTC.miniML]
ret_value_lam [instance, in GDTC.miniML]
ret_exp_fix [instance, in GDTC.miniML]
ret_exp_case [instance, in GDTC.miniML]
ret_exp_arith [instance, in GDTC.miniML]
ret_exp_bool [instance, in GDTC.miniML]
ret_exp_lam [instance, in GDTC.miniML]
ret_ty_arith [instance, in GDTC.miniML_nofix]
ret_ty_bool [instance, in GDTC.miniML_nofix]
ret_ty_lam [instance, in GDTC.miniML_nofix]
ret_value_arith [instance, in GDTC.miniML_nofix]
ret_value_bool [instance, in GDTC.miniML_nofix]
ret_value_lam [instance, in GDTC.miniML_nofix]
ret_exp_case [instance, in GDTC.miniML_nofix]
ret_exp_arith [instance, in GDTC.miniML_nofix]
ret_exp_bool [instance, in GDTC.miniML_nofix]
ret_exp_lam [instance, in GDTC.miniML_nofix]
rinstId_exp [lemma, in SN.expressions]
rinstId_exp_var [lemma, in SN.expressions]
rinstId_exp_case [lemma, in SN.expressions]
rinstId_exp_bool [lemma, in SN.expressions]
rinstId_exp_arith [lemma, in SN.expressions]
rinstId_exp_lam [lemma, in SN.expressions]
rinstId_exp [lemma, in SN.sn_lam]
rinstInst_exp [lemma, in SN.expressions]
rinstInst_up_exp_exp [definition, in SN.expressions]
rinstInst_exp_var [lemma, in SN.expressions]
rinstInst_exp_case [lemma, in SN.expressions]
rinstInst_exp_bool [lemma, in SN.expressions]
rinstInst_exp_arith [lemma, in SN.expressions]
rinstInst_exp_lam [lemma, in SN.expressions]
rinstInst_exp [lemma, in SN.sn_lam]
rinst_inst_exp [definition, in SN.expressions]
rinst_inst_exp_var [definition, in SN.expressions]
rinst_inst_exp_case [definition, in SN.expressions]
rinst_inst_exp_bool [definition, in SN.expressions]
rinst_inst_exp_arith [definition, in SN.expressions]
rinst_inst_exp_lam [definition, in SN.expressions]

S

s [definition, in Counting.section2_count]
s [definition, in Counting.section2_count_metacoq]
scons [definition, in fintype]
scons [definition, in SN.unscoped]
scons_comp [lemma, in fintype]
scons_eta_id [lemma, in fintype]
scons_eta [lemma, in fintype]
scons_comp [lemma, in SN.unscoped]
scons_eta_id [lemma, in SN.unscoped]
scons_eta [lemma, in SN.unscoped]
section2_count_metacoq [library]
section2_count [library]
shift [definition, in fintype]
shift [definition, in SN.unscoped]
size_ind [lemma, in header_extensible]
SmartConstructors [section, in Counting.section2_count]
SmartConstructors [section, in Counting.section2_count_metacoq]
SmartConstructors.X [variable, in Counting.section2_count]
SmartConstructors.X [variable, in Counting.section2_count_metacoq]
sn [inductive, in SN.defs]
sn [library]
SNI [constructor, in SN.defs]
sn_fundamental_var [lemma, in SN.sn_var]
sn_lam [lemma, in SN.sn]
sn_lam [library]
sn_var [library]
sn_arith [library]
sn_bool [library]
some [constructor, in TypeSafetyAgda.extensible_array]
Some [definition, in SN.unscoped]
some_none_explosion [lemma, in header_extensible]
Some_inj [lemma, in header_extensible]
some_ [definition, in TypeSafetyAgda.extensible_array]
split_forall_impl [definition, in header_metacoq]
srefl [constructor, in SN.defs]
star [inductive, in SN.defs]
star_If1 [lemma, in SN.sn_bool]
star_plus2 [lemma, in SN.sn_arith]
star_plus1 [lemma, in SN.sn_arith]
star_trans [lemma, in SN.defs]
star_appR [lemma, in SN.sn_lam]
star_appL [lemma, in SN.sn_lam]
step [inductive, in SN.sn]
stepAppL [constructor, in SN.sn_lam]
stepAppR [constructor, in SN.sn_lam]
stepBeta [constructor, in SN.sn_lam]
stepBeta' [lemma, in SN.sn_lam]
stepIfBeta [constructor, in SN.sn_bool]
stepIf1 [constructor, in SN.sn_bool]
stepIf2 [constructor, in SN.sn_bool]
stepIf3 [constructor, in SN.sn_bool]
stepl [constructor, in TypeSafetyAgda.TypeSafety]
stepLam [constructor, in SN.sn_lam]
stepPlus [constructor, in SN.sn_arith]
stepPlus1 [constructor, in SN.sn_arith]
stepPlus2 [constructor, in SN.sn_arith]
stepr [constructor, in TypeSafetyAgda.TypeSafety]
steprd1 [constructor, in TypeSafetyAgda.TypeSafety]
steprd2 [constructor, in TypeSafetyAgda.TypeSafety]
stepsome [constructor, in TypeSafetyAgda.TypeSafety]
stepwr1 [constructor, in TypeSafetyAgda.TypeSafety]
stepwr2 [constructor, in TypeSafetyAgda.TypeSafety]
stepwr3 [constructor, in TypeSafetyAgda.TypeSafety]
step_bool [inductive, in SN.sn_bool]
step_arith [inductive, in SN.sn_arith]
step_inst_var [lemma, in SN.sn_var]
step_anti_renaming_var [lemma, in SN.sn_var]
step_var [inductive, in SN.sn_var]
step_features [instance, in SN.sn]
step_lam [inductive, in SN.sn_lam]
strans [constructor, in SN.defs]
Subst_exp [instance, in SN.expressions]
subst_exp [definition, in SN.expressions]
subst_exp_var [definition, in SN.expressions]
subst_exp_case [definition, in SN.expressions]
subst_exp_bool [definition, in SN.expressions]
subst_exp_arith [definition, in SN.expressions]
subst_exp_lam [definition, in SN.expressions]
subst1 [projection, in fintype]
Subst1 [record, in fintype]
subst1 [constructor, in fintype]
Subst1 [inductive, in fintype]
subst1 [projection, in SN.unscoped]
Subst1 [record, in SN.unscoped]
subst1 [constructor, in SN.unscoped]
Subst1 [inductive, in SN.unscoped]
subst2 [projection, in fintype]
Subst2 [record, in fintype]
subst2 [constructor, in fintype]
Subst2 [inductive, in fintype]
subst2 [projection, in SN.unscoped]
Subst2 [record, in SN.unscoped]
subst2 [constructor, in SN.unscoped]
Subst2 [inductive, in SN.unscoped]
subst3 [projection, in fintype]
Subst3 [record, in fintype]
subst3 [constructor, in fintype]
Subst3 [inductive, in fintype]
subst3 [projection, in SN.unscoped]
Subst3 [record, in SN.unscoped]
subst3 [constructor, in SN.unscoped]
Subst3 [inductive, in SN.unscoped]
subst4 [projection, in fintype]
Subst4 [record, in fintype]
subst4 [constructor, in fintype]
Subst4 [inductive, in fintype]
subst4 [projection, in SN.unscoped]
Subst4 [record, in SN.unscoped]
subst4 [constructor, in SN.unscoped]
Subst4 [inductive, in SN.unscoped]
subst5 [projection, in fintype]
Subst5 [record, in fintype]
subst5 [constructor, in fintype]
Subst5 [inductive, in fintype]
subst5 [projection, in SN.unscoped]
Subst5 [record, in SN.unscoped]
subst5 [constructor, in SN.unscoped]
Subst5 [inductive, in SN.unscoped]
subtermC [record, in header_metacoq]
subtermC [inductive, in header_metacoq]
subterm_ty_arith' [instance, in GDTC.features]
subterm_ty_arith [instance, in GDTC.features]
subterm_ty_bool [instance, in GDTC.features]
subterm_rel [projection, in header_metacoq]
subterm_rel [constructor, in header_metacoq]
subt_arith [instance, in GDTC.GDTC]
subt_bool [instance, in GDTC.GDTC]
sum [constructor, in TypeSafetyAgda.TypeSafety]

T

tactics [library]
TArray [constructor, in TypeSafetyAgda.extensible_array]
tmMkDefinition [definition, in header_metacoq]
tmTryInferInstance [definition, in header_metacoq]
TNat [constructor, in TypeSafetyAgda.extensible_array]
TOption [constructor, in TypeSafetyAgda.extensible_array]
ty [inductive, in GDTC.miniML]
ty [inductive, in GDTC.miniML_nofix]
ty [inductive, in SN.expressions]
ty [section, in SN.expressions]
ty [inductive, in TypeSafetyAgda.extensible_array]
ty [section, in TypeSafetyAgda.extensible_array]
typeof [definition, in GDTC.miniML_results]
typeof [definition, in GDTC.miniML_nofix_results]
typeof_sound [lemma, in GDTC.miniML_results]
typeof_sound [lemma, in GDTC.miniML_nofix_results]
typeof_fix [definition, in GDTC.GDTC]
typeof_case [definition, in GDTC.GDTC]
typeof_arith [definition, in GDTC.GDTC]
typeof_bool [definition, in GDTC.GDTC]
typeof_lam [definition, in GDTC.GDTC]
TypeSafety [library]
ty_arith [inductive, in GDTC.features]
ty_bool [inductive, in GDTC.features]
ty_lam [inductive, in GDTC.features]
ty_arith_C [constructor, in GDTC.miniML]
ty_bool_C [constructor, in GDTC.miniML]
ty_lam_C [constructor, in GDTC.miniML]
ty_induction [lemma, in GDTC.miniML_results]
ty_arith_C [constructor, in GDTC.miniML_nofix]
ty_bool_C [constructor, in GDTC.miniML_nofix]
ty_lam_C [constructor, in GDTC.miniML_nofix]
ty_induction [lemma, in GDTC.miniML_nofix_results]
ty_features [instance, in SN.sn]
ty_arith.retract_ty_arith [variable, in SN.expressions]
ty_arith [inductive, in SN.expressions]
ty_arith.ty [variable, in SN.expressions]
ty_arith [section, in SN.expressions]
ty_bool.retract_ty_bool [variable, in SN.expressions]
ty_bool [inductive, in SN.expressions]
ty_bool.ty [variable, in SN.expressions]
ty_bool [section, in SN.expressions]
ty_lam.retract_ty_lam [variable, in SN.expressions]
ty_lam [inductive, in SN.expressions]
ty_lam.ty [variable, in SN.expressions]
ty_lam [section, in SN.expressions]

U

unscoped [library]
upExtRen_exp_exp [definition, in SN.expressions]
upExt_exp_exp [definition, in SN.expressions]
upId_exp_exp [definition, in SN.expressions]
upRen_exp_exp [definition, in SN.expressions]
up_ren_ren [lemma, in fintype]
up_ren [definition, in fintype]
up_ren_ext [lemma, in SN.sn]
Up_exp_exp [instance, in SN.expressions]
up_exp [projection, in SN.expressions]
Up_exp [record, in SN.expressions]
up_exp [constructor, in SN.expressions]
Up_exp [inductive, in SN.expressions]
up_subst_subst_exp_exp [definition, in SN.expressions]
up_subst_ren_exp_exp [definition, in SN.expressions]
up_ren_subst_exp_exp [definition, in SN.expressions]
up_ren_ren_exp_exp [definition, in SN.expressions]
up_exp_exp [definition, in SN.expressions]
up_ren_ren [lemma, in SN.unscoped]
up_ren [definition, in SN.unscoped]

V

value [inductive, in GDTC.miniML]
value [inductive, in GDTC.miniML_nofix]
value_fix [inductive, in GDTC.features]
value_arith [inductive, in GDTC.features]
value_bool [inductive, in GDTC.features]
value_lam [inductive, in GDTC.features]
value_fix_C [constructor, in GDTC.miniML]
value_arith_C [constructor, in GDTC.miniML]
value_bool_C [constructor, in GDTC.miniML]
value_lam_C [constructor, in GDTC.miniML]
value_arith_C [constructor, in GDTC.miniML_nofix]
value_bool_C [constructor, in GDTC.miniML_nofix]
value_lam_C [constructor, in GDTC.miniML_nofix]
val_inclusion [lemma, in SN.sn_var]
var [constructor, in Counting.section2_count]
Var [definition, in GDTC.features]
var [constructor, in GDTC.features]
Var [record, in fintype]
Var [inductive, in fintype]
var [section, in Counting.section2_count_metacoq]
var [constructor, in Counting.section2_count_metacoq]
var [constructor, in SN.expressions]
Var [record, in SN.unscoped]
Var [inductive, in SN.unscoped]
VarInstance_exp [instance, in SN.expressions]
varLRen_exp [lemma, in SN.expressions]
varL_exp [lemma, in SN.expressions]
varL_exp [lemma, in SN.sn_lam]
var_ [definition, in Counting.section2_count]
var_has_ty [constructor, in SN.sn_var]
var_zero [definition, in fintype]
var_ [definition, in Counting.section2_count_metacoq]
var_ [definition, in SN.expressions]
var_exp [abbreviation, in SN.sn_lam]
var_zero [definition, in SN.unscoped]
var.count [variable, in Counting.section2_count_metacoq]
var.exp [variable, in Counting.section2_count_metacoq]
vtypeis [inductive, in GDTC.miniML_results]
vtypeis [inductive, in GDTC.miniML_nofix_results]
vtypeis_Fix [constructor, in GDTC.miniML_results]
vtypeis_Arith [constructor, in GDTC.miniML_results]
vtypeis_Bool [constructor, in GDTC.miniML_results]
vtypeis_Lam [constructor, in GDTC.miniML_results]
vtypeis_Arith [constructor, in GDTC.miniML_nofix_results]
vtypeis_Bool [constructor, in GDTC.miniML_nofix_results]
vtypeis_Lam [constructor, in GDTC.miniML_nofix_results]
vtypeis_inj_imprev_lam' [instance, in GDTC.GDTC]
vtypeis_inj_imp_lam' [instance, in GDTC.GDTC]
vtypeis_inj_imprev_fix [instance, in GDTC.GDTC]
vtypeis_inj_imp_fix [instance, in GDTC.GDTC]
vtypeis_fix [inductive, in GDTC.GDTC]
vtypeis_inj_imprev_arith' [instance, in GDTC.GDTC]
vtypeis_inj_imp_arith' [instance, in GDTC.GDTC]
vtypeis_inj_imprev_arith [instance, in GDTC.GDTC]
vtypeis_inj_imp_arith [instance, in GDTC.GDTC]
vtypeis_arith_C [constructor, in GDTC.GDTC]
vtypeis_arith [inductive, in GDTC.GDTC]
vtypeis_inj_imprev_bool [instance, in GDTC.GDTC]
vtypeis_inj_imp_bool [instance, in GDTC.GDTC]
vtypeis_bool_C [constructor, in GDTC.GDTC]
vtypeis_bool [inductive, in GDTC.GDTC]
vtypeis_inj_imprev [instance, in GDTC.GDTC]
vtypeis_inj_imp [instance, in GDTC.GDTC]
vtypeis_lam [inductive, in GDTC.GDTC]

W

wf_value_RC [constructor, in GDTC.GDTC]
wf_value_C [constructor, in GDTC.GDTC]
whnf [definition, in SN.sn]
whnf_anti_renaming_bool [lemma, in SN.sn_bool]
whnf_anti_renaming_arith [lemma, in SN.sn_arith]
whnf_anti_renaming_var [lemma, in SN.sn_var]
whnf_anti_renaming_lam [lemma, in SN.sn_lam]
wn [lemma, in SN.sn]
wn_fundamental_var [lemma, in SN.sn_var]
wr [constructor, in TypeSafetyAgda.extensible_array]
wr_ [definition, in TypeSafetyAgda.extensible_array]
wtyped [inductive, in TypeSafetyAgda.TypeSafety]
wtyped_inv_opt [lemma, in TypeSafetyAgda.TypeSafety]
wtyped_inv_arr [lemma, in TypeSafetyAgda.TypeSafety]
wtyped_inv_plus [lemma, in TypeSafetyAgda.TypeSafety]
wtyped_in_opt [constructor, in TypeSafetyAgda.TypeSafety]
wtyped_in_arr [constructor, in TypeSafetyAgda.TypeSafety]
wtyped_in_plus [constructor, in TypeSafetyAgda.TypeSafety]
wtyped_arr [inductive, in TypeSafetyAgda.TypeSafety]
wtyped_opt [inductive, in TypeSafetyAgda.TypeSafety]
wtyped_plus [inductive, in TypeSafetyAgda.TypeSafety]

other

⟨ _ ; _ ⟩ (fscope) [notation, in fintype]
⟨ _ ⟩ (fscope) [notation, in fintype]
⟨ _ ⟩ (fscope) [notation, in SN.expressions]
⟨ _ ⟩ (fscope) [notation, in SN.expressions]
⟨ _ ⟩ (fscope) [notation, in SN.expressions]
⟨ _ ; _ ⟩ (fscope) [notation, in SN.unscoped]
⟨ _ ⟩ (fscope) [notation, in SN.unscoped]
[~ _ ; _ ; .. ; _ ~] (list_scope) [notation, in header_metacoq]
[~ _ ~] (list_scope) [notation, in header_metacoq]
↑ (subst_scope) [notation, in fintype]
_ .. (subst_scope) [notation, in fintype]
_ .: _ (subst_scope) [notation, in fintype]
_ [ _ ; _ ] (subst_scope) [notation, in fintype]
_ [ _ ] (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in SN.expressions]
_ [ _ ] (subst_scope) [notation, in SN.expressions]
_ ⟨ _ ⟩ (subst_scope) [notation, in SN.expressions]
_ [ _ ] (subst_scope) [notation, in SN.expressions]
_ ⟨ _ ⟩ (subst_scope) [notation, in SN.expressions]
_ [ _ ] (subst_scope) [notation, in SN.expressions]
↑__exp (subst_scope) [notation, in SN.expressions]
↑__exp (subst_scope) [notation, in SN.expressions]
var (subst_scope) [notation, in SN.expressions]
_ __exp (subst_scope) [notation, in SN.expressions]
_ __exp (subst_scope) [notation, in SN.expressions]
_ .. (subst_scope) [notation, in SN.unscoped]
_ , _ (subst_scope) [notation, in SN.unscoped]
_ >> _ (subst_scope) [notation, in SN.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in SN.unscoped]
_ [ _ ] (subst_scope) [notation, in SN.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in SN.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in SN.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in SN.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in SN.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in SN.unscoped]
_ <: _ [notation, in Counting.section2_count]
_ .: _ [notation, in GDTC.features]
_ >> _ [notation, in fintype]
_ <: _ [notation, in Counting.section2_count_metacoq]
_ ~> _ [notation, in header_metacoq]
_ .: _ [notation, in SN.unscoped]
Compose Lemma _ on _ using _ : _ [notation, in header_metacoq]
Compose Lemma _ on _ by inversion : _ [notation, in header_metacoq]
Compose Lemma _ on _ : _ [notation, in header_metacoq]
Compose Fixpoint _ on _ : _ [notation, in header_metacoq]
list_map [notation, in SN.axioms]
Modular Fixpoint _ where _ extends _ := _ [notation, in header_metacoq]
Modular Fixpoint _ where _ extends _ with _ := _ [notation, in header_metacoq]
Modular Lemma _ where _ extends _ with _ : _ [notation, in header_metacoq]
Modular Lemma _ where _ extends _ at _ with _ : _ [notation, in header_metacoq]
↑ [notation, in SN.unscoped]

---

Notation Index

C

_ , _ (subst_scope) [in fintype]

other

⟨ _ ; _ ⟩ (fscope) [in fintype]
⟨ _ ⟩ (fscope) [in fintype]
⟨ _ ⟩ (fscope) [in SN.expressions]
⟨ _ ⟩ (fscope) [in SN.expressions]
⟨ _ ⟩ (fscope) [in SN.expressions]
⟨ _ ; _ ⟩ (fscope) [in SN.unscoped]
⟨ _ ⟩ (fscope) [in SN.unscoped]
[~ _ ; _ ; .. ; _ ~] (list_scope) [in header_metacoq]
[~ _ ~] (list_scope) [in header_metacoq]
↑ (subst_scope) [in fintype]
_ .. (subst_scope) [in fintype]
_ .: _ (subst_scope) [in fintype]
_ [ _ ; _ ] (subst_scope) [in fintype]
_ [ _ ] (subst_scope) [in fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ⟩ (subst_scope) [in SN.expressions]
_ [ _ ] (subst_scope) [in SN.expressions]
_ ⟨ _ ⟩ (subst_scope) [in SN.expressions]
_ [ _ ] (subst_scope) [in SN.expressions]
_ ⟨ _ ⟩ (subst_scope) [in SN.expressions]
_ [ _ ] (subst_scope) [in SN.expressions]
↑__exp (subst_scope) [in SN.expressions]
↑__exp (subst_scope) [in SN.expressions]
var (subst_scope) [in SN.expressions]
_ __exp (subst_scope) [in SN.expressions]
_ __exp (subst_scope) [in SN.expressions]
_ .. (subst_scope) [in SN.unscoped]
_ , _ (subst_scope) [in SN.unscoped]
_ >> _ (subst_scope) [in SN.unscoped]
_ [ _ ; _ ] (subst_scope) [in SN.unscoped]
_ [ _ ] (subst_scope) [in SN.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in SN.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in SN.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in SN.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in SN.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in SN.unscoped]
_ <: _ [in Counting.section2_count]
_ .: _ [in GDTC.features]
_ >> _ [in fintype]
_ <: _ [in Counting.section2_count_metacoq]
_ ~> _ [in header_metacoq]
_ .: _ [in SN.unscoped]
Compose Lemma _ on _ using _ : _ [in header_metacoq]
Compose Lemma _ on _ by inversion : _ [in header_metacoq]
Compose Lemma _ on _ : _ [in header_metacoq]
Compose Fixpoint _ on _ : _ [in header_metacoq]
list_map [in SN.axioms]
Modular Fixpoint _ where _ extends _ := _ [in header_metacoq]
Modular Fixpoint _ where _ extends _ with _ := _ [in header_metacoq]
Modular Lemma _ where _ extends _ with _ : _ [in header_metacoq]
Modular Lemma _ where _ extends _ at _ with _ : _ [in header_metacoq]
↑ [in SN.unscoped]

---

Module Index

A

arith [in Counting.section2_count_metacoq]

B

booleans [in Counting.section2_count_metacoq]

C

CommaNotation [in fintype]
count_again.booleans [in Counting.section2_count_metacoq]
count_again.lambdas [in Counting.section2_count_metacoq]
count_again [in Counting.section2_count_metacoq]

L

lambdas [in Counting.section2_count_metacoq]

---

Variable Index

A

Arith.count [in Counting.section2_count]
Arith.count_gt [in Counting.section2_count]
Arith.E [in GDTC.features]
Arith.exp [in Counting.section2_count]
Arith.exp [in Counting.section2_count_metacoq]
Arith.T [in GDTC.features]
Arith.V [in GDTC.features]

B

Booleans.E [in GDTC.features]
Booleans.T [in GDTC.features]
Booleans.V [in GDTC.features]
bool.exp [in Counting.section2_count_metacoq]

C

count_again.count [in Counting.section2_count]
count_again.exp [in Counting.section2_count]
count_again.sec.exp [in Counting.section2_count_metacoq]
count.count [in Counting.section2_count]
count.count_gt [in Counting.section2_count]
count.exp [in Counting.section2_count]

E

exp_var.retract_subst_exp [in SN.expressions]
exp_var.retract_ren_exp [in SN.expressions]
exp_var.rinst_inst_exp [in SN.expressions]
exp_var.rinstInst_up_exp_exp [in SN.expressions]
exp_var.compSubstSubst_exp [in SN.expressions]
exp_var.up_subst_subst_exp_exp [in SN.expressions]
exp_var.compSubstRen_exp [in SN.expressions]
exp_var.up_subst_ren_exp_exp [in SN.expressions]
exp_var.compRenSubst_exp [in SN.expressions]
exp_var.up_ren_subst_exp_exp [in SN.expressions]
exp_var.compRenRen_exp [in SN.expressions]
exp_var.up_ren_ren_exp_exp [in SN.expressions]
exp_var.ext_exp [in SN.expressions]
exp_var.upExt_exp_exp [in SN.expressions]
exp_var.extRen_exp [in SN.expressions]
exp_var.upExtRen_exp_exp [in SN.expressions]
exp_var.idSubst_exp [in SN.expressions]
exp_var.upId_exp_exp [in SN.expressions]
exp_var.subst_exp [in SN.expressions]
exp_var.up_exp_exp [in SN.expressions]
exp_var.ren_exp [in SN.expressions]
exp_var.upRen_exp_exp [in SN.expressions]
exp_var.retract_exp_var [in SN.expressions]
exp_var.exp [in SN.expressions]
exp_case.retract_subst_exp [in SN.expressions]
exp_case.retract_ren_exp [in SN.expressions]
exp_case.retract_exp_case [in SN.expressions]
exp_case.rinst_inst_exp [in SN.expressions]
exp_case.rinstInst_up_exp_exp [in SN.expressions]
exp_case.compSubstSubst_exp [in SN.expressions]
exp_case.up_subst_subst_exp_exp [in SN.expressions]
exp_case.compSubstRen_exp [in SN.expressions]
exp_case.up_subst_ren_exp_exp [in SN.expressions]
exp_case.compRenSubst_exp [in SN.expressions]
exp_case.up_ren_subst_exp_exp [in SN.expressions]
exp_case.compRenRen_exp [in SN.expressions]
exp_case.up_ren_ren_exp_exp [in SN.expressions]
exp_case.ext_exp [in SN.expressions]
exp_case.upExt_exp_exp [in SN.expressions]
exp_case.extRen_exp [in SN.expressions]
exp_case.upExtRen_exp_exp [in SN.expressions]
exp_case.idSubst_exp [in SN.expressions]
exp_case.upId_exp_exp [in SN.expressions]
exp_case.subst_exp [in SN.expressions]
exp_case.up_exp_exp [in SN.expressions]
exp_case.ren_exp [in SN.expressions]
exp_case.upRen_exp_exp [in SN.expressions]
exp_case.var_exp [in SN.expressions]
exp_case.exp [in SN.expressions]
exp_bool.retract_subst_exp [in SN.expressions]
exp_bool.retract_ren_exp [in SN.expressions]
exp_bool.retract_exp_bool [in SN.expressions]
exp_bool.rinst_inst_exp [in SN.expressions]
exp_bool.rinstInst_up_exp_exp [in SN.expressions]
exp_bool.compSubstSubst_exp [in SN.expressions]
exp_bool.up_subst_subst_exp_exp [in SN.expressions]
exp_bool.compSubstRen_exp [in SN.expressions]
exp_bool.up_subst_ren_exp_exp [in SN.expressions]
exp_bool.compRenSubst_exp [in SN.expressions]
exp_bool.up_ren_subst_exp_exp [in SN.expressions]
exp_bool.compRenRen_exp [in SN.expressions]
exp_bool.up_ren_ren_exp_exp [in SN.expressions]
exp_bool.ext_exp [in SN.expressions]
exp_bool.upExt_exp_exp [in SN.expressions]
exp_bool.extRen_exp [in SN.expressions]
exp_bool.upExtRen_exp_exp [in SN.expressions]
exp_bool.idSubst_exp [in SN.expressions]
exp_bool.upId_exp_exp [in SN.expressions]
exp_bool.subst_exp [in SN.expressions]
exp_bool.up_exp_exp [in SN.expressions]
exp_bool.ren_exp [in SN.expressions]
exp_bool.upRen_exp_exp [in SN.expressions]
exp_bool.var_exp [in SN.expressions]
exp_bool.exp [in SN.expressions]
exp_arith.retract_subst_exp [in SN.expressions]
exp_arith.retract_ren_exp [in SN.expressions]
exp_arith.retract_exp_arith [in SN.expressions]
exp_arith.rinst_inst_exp [in SN.expressions]
exp_arith.rinstInst_up_exp_exp [in SN.expressions]
exp_arith.compSubstSubst_exp [in SN.expressions]
exp_arith.up_subst_subst_exp_exp [in SN.expressions]
exp_arith.compSubstRen_exp [in SN.expressions]
exp_arith.up_subst_ren_exp_exp [in SN.expressions]
exp_arith.compRenSubst_exp [in SN.expressions]
exp_arith.up_ren_subst_exp_exp [in SN.expressions]
exp_arith.compRenRen_exp [in SN.expressions]
exp_arith.up_ren_ren_exp_exp [in SN.expressions]
exp_arith.ext_exp [in SN.expressions]
exp_arith.upExt_exp_exp [in SN.expressions]
exp_arith.extRen_exp [in SN.expressions]
exp_arith.upExtRen_exp_exp [in SN.expressions]
exp_arith.idSubst_exp [in SN.expressions]
exp_arith.upId_exp_exp [in SN.expressions]
exp_arith.subst_exp [in SN.expressions]
exp_arith.up_exp_exp [in SN.expressions]
exp_arith.ren_exp [in SN.expressions]
exp_arith.upRen_exp_exp [in SN.expressions]
exp_arith.var_exp [in SN.expressions]
exp_arith.exp [in SN.expressions]
exp_lam.retract_subst_exp [in SN.expressions]
exp_lam.retract_ren_exp [in SN.expressions]
exp_lam.retract_exp_lam [in SN.expressions]
exp_lam.rinst_inst_exp [in SN.expressions]
exp_lam.rinstInst_up_exp_exp [in SN.expressions]
exp_lam.compSubstSubst_exp [in SN.expressions]
exp_lam.up_subst_subst_exp_exp [in SN.expressions]
exp_lam.compSubstRen_exp [in SN.expressions]
exp_lam.up_subst_ren_exp_exp [in SN.expressions]
exp_lam.compRenSubst_exp [in SN.expressions]
exp_lam.up_ren_subst_exp_exp [in SN.expressions]
exp_lam.compRenRen_exp [in SN.expressions]
exp_lam.up_ren_ren_exp_exp [in SN.expressions]
exp_lam.ext_exp [in SN.expressions]
exp_lam.upExt_exp_exp [in SN.expressions]
exp_lam.extRen_exp [in SN.expressions]
exp_lam.upExtRen_exp_exp [in SN.expressions]
exp_lam.idSubst_exp [in SN.expressions]
exp_lam.upId_exp_exp [in SN.expressions]
exp_lam.subst_exp [in SN.expressions]
exp_lam.up_exp_exp [in SN.expressions]
exp_lam.ren_exp [in SN.expressions]
exp_lam.upRen_exp_exp [in SN.expressions]
exp_lam.var_exp [in SN.expressions]
exp_lam.exp [in SN.expressions]
exp_lam.ty [in SN.expressions]
exp_arr.retract_exp_arr [in TypeSafetyAgda.extensible_array]
exp_arr.exp [in TypeSafetyAgda.extensible_array]
exp_opt.retract_exp_opt [in TypeSafetyAgda.extensible_array]
exp_opt.exp [in TypeSafetyAgda.extensible_array]
exp_plus.retract_exp_plus [in TypeSafetyAgda.extensible_array]
exp_plus.exp [in TypeSafetyAgda.extensible_array]

F

Fix.E [in GDTC.features]
Fix.T [in GDTC.features]
Fix.V [in GDTC.features]

L

Lambdas.E [in GDTC.features]
Lambdas.T [in GDTC.features]
Lambdas.V [in GDTC.features]
lam.exp [in Counting.section2_count_metacoq]

M

MiniML_Bool.ren_preserves [in SN.sn_bool]
MiniML_Bool.retract_L_strong [in SN.sn_bool]
MiniML_Bool.whnf_whnf_bool [in SN.sn_bool]
MiniML_Bool.retract_L [in SN.sn_bool]
MiniML_Bool.retract_step_rev [in SN.sn_bool]
MiniML_Bool.retract_step [in SN.sn_bool]
MiniML_Bool.step [in SN.sn_bool]
MiniML_Bool.retract_has_ty_rev [in SN.sn_bool]
MiniML_Bool.retract_has_ty [in SN.sn_bool]
MiniML_Bool.has_ty [in SN.sn_bool]
MiniML_Bool.retract_subst_exp [in SN.sn_bool]
MiniML_Bool.subst_exp [in SN.sn_bool]
MiniML_Bool.retract_ren_exp [in SN.sn_bool]
MiniML_Bool.ren_exp [in SN.sn_bool]
MiniML_Bool.exp [in SN.sn_bool]
MiniML_Bool.ty [in SN.sn_bool]
MiniML_Arith.step_anti_renaming [in SN.sn_arith]
MiniML_Arith.ren_preserves [in SN.sn_arith]
MiniML_Arith.retract_L_strong [in SN.sn_arith]
MiniML_Arith.whnf_whnf_arith [in SN.sn_arith]
MiniML_Arith.retract_L [in SN.sn_arith]
MiniML_Arith.retract_step_rev [in SN.sn_arith]
MiniML_Arith.retract_step [in SN.sn_arith]
MiniML_Arith.step [in SN.sn_arith]
MiniML_Arith.retract_has_ty_rev [in SN.sn_arith]
MiniML_Arith.retract_has_ty [in SN.sn_arith]
MiniML_Arith.has_ty [in SN.sn_arith]
MiniML_Arith.retract_subst_exp [in SN.sn_arith]
MiniML_Arith.subst_exp [in SN.sn_arith]
MiniML_Arith.retract_ren_exp [in SN.sn_arith]
MiniML_Arith.ren_exp [in SN.sn_arith]
MiniML_Arith.exp [in SN.sn_arith]
MiniML_Arith.ty [in SN.sn_arith]
MiniML_var.L_strong [in SN.sn_var]
MiniML_var.L [in SN.sn_var]
MiniML_var.ren_preserves [in SN.sn_var]
MiniML_var.whnf_whnf_var [in SN.sn_var]
MiniML_var.step [in SN.sn_var]
MiniML_var.retract_has_ty_rev [in SN.sn_var]
MiniML_var.retract_has_ty [in SN.sn_var]
MiniML_var.has_ty [in SN.sn_var]
MiniML_var.subst_id_exp [in SN.sn_var]
MiniML_var.var_exp [in SN.sn_var]
MiniML_var.retract_subst_exp [in SN.sn_var]
MiniML_var.subst_exp [in SN.sn_var]
MiniML_var.retract_ren_exp [in SN.sn_var]
MiniML_var.ren_exp [in SN.sn_var]
MiniML_var.ty [in SN.sn_var]
MiniML_var.exp [in SN.sn_var]
MiniML_Lambda.E_strong_var [in SN.sn_lam]
MiniML_Lambda.retract_L_strong [in SN.sn_lam]
MiniML_Lambda.ren_var [in SN.sn_lam]
MiniML_Lambda.ren_preserves [in SN.sn_lam]
MiniML_Lambda.whnf_anti_renaming [in SN.sn_lam]
MiniML_Lambda.L_strong [in SN.sn_lam]
MiniML_Lambda.retract_whnf_lam [in SN.sn_lam]
MiniML_Lambda.retract_L [in SN.sn_lam]
MiniML_Lambda.L [in SN.sn_lam]
MiniML_Lambda.retract_step_rev [in SN.sn_lam]
MiniML_Lambda.retract_step [in SN.sn_lam]
MiniML_Lambda.step [in SN.sn_lam]
MiniML_Lambda.retract_has_ty_rev [in SN.sn_lam]
MiniML_Lambda.retract_has_ty [in SN.sn_lam]
MiniML_Lambda.hasty_var [in SN.sn_lam]
MiniML_Lambda.has_ty [in SN.sn_lam]
MiniML_Lambda.subst_exp_var [in SN.sn_lam]
MiniML_Lambda.up_exp_exp_def' [in SN.sn_lam]
MiniML_Lambda.up_exp_exp_def [in SN.sn_lam]
MiniML_Lambda.upRen_exp_exp_def [in SN.sn_lam]
MiniML_Lambda.retract_subst_exp [in SN.sn_lam]
MiniML_Lambda.retract_ren_exp [in SN.sn_lam]
MiniML_Lambda.rinst_inst_exp [in SN.sn_lam]
MiniML_Lambda.rinstInst_up_exp_exp [in SN.sn_lam]
MiniML_Lambda.compSubstSubst_exp [in SN.sn_lam]
MiniML_Lambda.up_subst_subst_exp_exp [in SN.sn_lam]
MiniML_Lambda.compSubstRen_exp [in SN.sn_lam]
MiniML_Lambda.up_subst_ren_exp_exp [in SN.sn_lam]
MiniML_Lambda.compRenSubst_exp [in SN.sn_lam]
MiniML_Lambda.up_ren_subst_exp_exp [in SN.sn_lam]
MiniML_Lambda.compRenRen_exp [in SN.sn_lam]
MiniML_Lambda.up_ren_ren_exp_exp [in SN.sn_lam]
MiniML_Lambda.ext_exp [in SN.sn_lam]
MiniML_Lambda.upExt_exp_exp [in SN.sn_lam]
MiniML_Lambda.extRen_exp [in SN.sn_lam]
MiniML_Lambda.upExtRen_exp_exp [in SN.sn_lam]
MiniML_Lambda.idSubst_exp [in SN.sn_lam]
MiniML_Lambda.upId_exp_exp [in SN.sn_lam]
MiniML_Lambda.subst_exp [in SN.sn_lam]
MiniML_Lambda.up_exp_exp [in SN.sn_lam]
MiniML_Lambda.ren_exp [in SN.sn_lam]
MiniML_Lambda.upRen_exp_exp [in SN.sn_lam]
MiniML_Lambda.exp [in SN.sn_lam]
MiniML_Lambda.ty [in SN.sn_lam]
MiniML_Fix.vtypeis_inj' [in GDTC.GDTC]
MiniML_Fix.vtypeis_inj [in GDTC.GDTC]
MiniML_Fix.vtypeis [in GDTC.GDTC]
MiniML_Fix.typeof_fix_inj' [in GDTC.GDTC]
MiniML_Fix.typeof_fix_inj [in GDTC.GDTC]
MiniML_Fix.beq_correct [in GDTC.GDTC]
MiniML_Fix.typeof [in GDTC.GDTC]
MiniML_Fix.beq [in GDTC.GDTC]
MiniML_Fix.eval [in GDTC.GDTC]
MiniML_Fix.V [in GDTC.GDTC]
MiniML_Fix.E [in GDTC.GDTC]
MiniML_Fix.T [in GDTC.GDTC]
MiniML_Case.vtypeis_inj [in GDTC.GDTC]
MiniML_Case.vtypeis [in GDTC.GDTC]
MiniML_Case.typeof [in GDTC.GDTC]
MiniML_Case.beq_correct [in GDTC.GDTC]
MiniML_Case.beq [in GDTC.GDTC]
MiniML_Case.eval [in GDTC.GDTC]
MiniML_Case.V [in GDTC.GDTC]
MiniML_Case.T [in GDTC.GDTC]
MiniML_Case.E [in GDTC.GDTC]
MiniML_Arith.vtypeis_inj [in GDTC.GDTC]
MiniML_Arith.vtypeis [in GDTC.GDTC]
MiniML_Arith.typeof [in GDTC.GDTC]
MiniML_Arith.beq_correct [in GDTC.GDTC]
MiniML_Arith.beq [in GDTC.GDTC]
MiniML_Arith.eval [in GDTC.GDTC]
MiniML_Arith.T [in GDTC.GDTC]
MiniML_Arith.V [in GDTC.GDTC]
MiniML_Arith.E [in GDTC.GDTC]
MiniML_Bool.vtypeis_inj [in GDTC.GDTC]
MiniML_Bool.vtypeis [in GDTC.GDTC]
MiniML_Bool.typeof [in GDTC.GDTC]
MiniML_Bool.beq_correct [in GDTC.GDTC]
MiniML_Bool.beq [in GDTC.GDTC]
MiniML_Bool.eval [in GDTC.GDTC]
MiniML_Bool.V [in GDTC.GDTC]
MiniML_Bool.E [in GDTC.GDTC]
MiniML_Bool.T [in GDTC.GDTC]
MiniML_Lambda.vtypeis_inj [in GDTC.GDTC]
MiniML_Lambda.vtypeis [in GDTC.GDTC]
MiniML_Lambda.typeof [in GDTC.GDTC]
MiniML_Lambda.beq_correct [in GDTC.GDTC]
MiniML_Lambda.beq [in GDTC.GDTC]
MiniML_Lambda.V [in GDTC.GDTC]
MiniML_Lambda.E [in GDTC.GDTC]
MiniML_Lambda.T [in GDTC.GDTC]

N

NatCase.E [in GDTC.features]
NatCase.T [in GDTC.features]
NatCase.V [in GDTC.features]

O

Option.eval [in TypeSafetyAgda.TypeSafety]
Option.exp [in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty_rev' [in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty' [in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty_rev [in TypeSafetyAgda.TypeSafety]
Option.retract_has_ty [in TypeSafetyAgda.TypeSafety]
Option.wtyped [in TypeSafetyAgda.TypeSafety]

P

Plus.eval [in TypeSafetyAgda.TypeSafety]
Plus.exp [in TypeSafetyAgda.TypeSafety]
Plus.retract_has_ty_rev [in TypeSafetyAgda.TypeSafety]
Plus.retract_has_ty [in TypeSafetyAgda.TypeSafety]
Plus.wtyped [in TypeSafetyAgda.TypeSafety]

S

SmartConstructors.X [in Counting.section2_count]
SmartConstructors.X [in Counting.section2_count_metacoq]

T

ty_arith.retract_ty_arith [in SN.expressions]
ty_arith.ty [in SN.expressions]
ty_bool.retract_ty_bool [in SN.expressions]
ty_bool.ty [in SN.expressions]
ty_lam.retract_ty_lam [in SN.expressions]
ty_lam.ty [in SN.expressions]

V

var.count [in Counting.section2_count_metacoq]
var.exp [in Counting.section2_count_metacoq]

---

Library Index

A

axioms
axioms

D

defs

E

expressions
extensible_array

F

features
fintype

G

GDTC

H

header_extensible
header_metacoq

M

miniML
miniML_results
miniML_nofix
miniML_nofix_results

S

section2_count_metacoq
section2_count
sn
sn_lam
sn_var
sn_arith
sn_bool

T

tactics
TypeSafety

U

unscoped

---

Lemma Index

B

beq_correct [in GDTC.miniML_results]
beq_correct [in GDTC.miniML_nofix_results]

C

close_ren [in SN.sn_lam]
compComp_exp' [in SN.expressions]
compComp_exp [in SN.expressions]
compComp_exp_var [in SN.expressions]
compComp_exp_case [in SN.expressions]
compComp_exp_bool [in SN.expressions]
compComp_exp_arith [in SN.expressions]
compComp_exp_lam [in SN.expressions]
compComp_exp [in SN.sn_lam]
compComp'_exp_var [in SN.expressions]
compComp'_exp_case [in SN.expressions]
compComp'_exp_bool [in SN.expressions]
compComp'_exp_arith [in SN.expressions]
compComp'_exp_lam [in SN.expressions]
compComp'_exp [in SN.sn_lam]
compRen_exp [in SN.expressions]
compRen_exp_var [in SN.expressions]
compRen_exp_case [in SN.expressions]
compRen_exp_bool [in SN.expressions]
compRen_exp_arith [in SN.expressions]
compRen_exp_lam [in SN.expressions]
compRen_exp [in SN.sn_lam]
compRen'_exp [in SN.expressions]
compRen'_exp_var [in SN.expressions]
compRen'_exp_case [in SN.expressions]
compRen'_exp_bool [in SN.expressions]
compRen'_exp_arith [in SN.expressions]
compRen'_exp_lam [in SN.expressions]
compRen'_exp [in SN.sn_lam]
congr_inj [in header_extensible]
congr_In_exp_arith [in SN.expressions]
congr_In_exp_bool [in SN.expressions]
congr_In_exp_lam [in SN.expressions]
congr_In_exp_var [in SN.expressions]
congr_var_ [in SN.expressions]
congr_natCase_ [in SN.expressions]
congr_If_ [in SN.expressions]
congr_constBool_ [in SN.expressions]
congr_constNat_ [in SN.expressions]
congr_plus_ [in SN.expressions]
congr_app_ [in SN.expressions]
congr_ab_ [in SN.expressions]
congr_In_ty_arith [in SN.expressions]
congr_In_ty_bool [in SN.expressions]
congr_In_ty_lam [in SN.expressions]
congr_natTy_ [in SN.expressions]
congr_boolTy_ [in SN.expressions]
congr_arr_ [in SN.expressions]
congr_In_exp_opt [in TypeSafetyAgda.extensible_array]
congr_In_exp_arr [in TypeSafetyAgda.extensible_array]
congr_In_exp_plus [in TypeSafetyAgda.extensible_array]
congr_wr_ [in TypeSafetyAgda.extensible_array]
congr_rd_ [in TypeSafetyAgda.extensible_array]
congr_nil_ [in TypeSafetyAgda.extensible_array]
congr_some_ [in TypeSafetyAgda.extensible_array]
congr_none_ [in TypeSafetyAgda.extensible_array]
congr_plus_ [in TypeSafetyAgda.extensible_array]
congr_atom_ [in TypeSafetyAgda.extensible_array]
congr_TNat [in TypeSafetyAgda.extensible_array]
congr_TOption [in TypeSafetyAgda.extensible_array]
congr_TArray [in TypeSafetyAgda.extensible_array]
Count_gt'_bool [in Counting.section2_count]
Count_gt'_lam [in Counting.section2_count]
count_gt'_bool [in Counting.section2_count]
count_gt'_lam [in Counting.section2_count]
count_gt'_var [in Counting.section2_count]
count_gt_arith [in Counting.section2_count]
count_gt_bool [in Counting.section2_count]
count_gt_lam [in Counting.section2_count]
count_gt_var [in Counting.section2_count]
count_again.count_gt'_var [in Counting.section2_count_metacoq]

E

eval1 [in GDTC.miniML_results]
eval1 [in GDTC.miniML_nofix_results]
eval2 [in GDTC.miniML_results]
eval2 [in GDTC.miniML_nofix_results]
eval3 [in GDTC.miniML_results]
eval3 [in GDTC.miniML_nofix_results]
eval4 [in GDTC.miniML_results]
eval4 [in GDTC.miniML_nofix_results]
eval5 [in GDTC.miniML_results]
E_strong_base [in SN.sn_var]
E_strong_step [in SN.sn_var]
E_strong_sn [in SN.sn_var]
E_strong_var [in SN.sn]

H

has_ty_subst_var [in SN.sn_var]
has_ty_ren_var [in SN.sn_var]
has_ty_rev_arith [in SN.sn]
has_ty_rev_bool [in SN.sn]
has_ty_rev_lam [in SN.sn]
has_ty_rev_var [in SN.sn]

I

instId_exp [in SN.expressions]
instId_exp_var [in SN.expressions]
instId_exp_case [in SN.expressions]
instId_exp_bool [in SN.expressions]
instId_exp_arith [in SN.expressions]
instId_exp_lam [in SN.expressions]
instId_exp [in SN.sn_lam]

L

L_close_ren_bool [in SN.sn_bool]
L_close_ren_arith [in SN.sn_arith]
L_lemma [in TypeSafetyAgda.TypeSafety]
L_val_lam [in SN.sn_lam]

M

monotone [in GDTC.miniML_results]
monotone [in GDTC.miniML_nofix_results]

P

pi [in SN.axioms]
pi [in axioms]
preservation_var [in SN.sn_var]

R

renComp_exp [in SN.expressions]
renComp_exp_var [in SN.expressions]
renComp_exp_case [in SN.expressions]
renComp_exp_bool [in SN.expressions]
renComp_exp_arith [in SN.expressions]
renComp_exp_lam [in SN.expressions]
renComp_exp [in SN.sn_lam]
renComp'_exp [in SN.expressions]
renComp'_exp_var [in SN.expressions]
renComp'_exp_case [in SN.expressions]
renComp'_exp_bool [in SN.expressions]
renComp'_exp_arith [in SN.expressions]
renComp'_exp_lam [in SN.expressions]
renComp'_exp [in SN.sn_lam]
renRen_exp [in SN.expressions]
renRen_exp_var [in SN.expressions]
renRen_exp_case [in SN.expressions]
renRen_exp_bool [in SN.expressions]
renRen_exp_arith [in SN.expressions]
renRen_exp_lam [in SN.expressions]
renRen_exp [in SN.sn_lam]
renRen'_exp [in SN.expressions]
renRen'_exp_var [in SN.expressions]
renRen'_exp_case [in SN.expressions]
renRen'_exp_bool [in SN.expressions]
renRen'_exp_arith [in SN.expressions]
renRen'_exp_lam [in SN.expressions]
renRen'_exp [in SN.sn_lam]
ren_preserves_constBool [in SN.sn_bool]
ren_preserves_If [in SN.sn_bool]
ren_preserves_constNat [in SN.sn_arith]
ren_preserves_Plus [in SN.sn_arith]
ren_preserves_var [in SN.sn_var]
ren_preserves_arith [in SN.sn]
ren_preserves_bool [in SN.sn]
ren_preserves_lam [in SN.sn]
ren_preserves [in SN.sn]
ren_preserves_app [in SN.sn_lam]
ren_preserves_ab [in SN.sn_lam]
retract_inj [in Counting.section2_count]
retract_inj [in Counting.section2_count_metacoq]
retract_step_arith [in SN.sn]
retract_step_bool [in SN.sn]
retract_step_lam [in SN.sn]
retract_inj [in header_extensible]
rinstId_exp [in SN.expressions]
rinstId_exp_var [in SN.expressions]
rinstId_exp_case [in SN.expressions]
rinstId_exp_bool [in SN.expressions]
rinstId_exp_arith [in SN.expressions]
rinstId_exp_lam [in SN.expressions]
rinstId_exp [in SN.sn_lam]
rinstInst_exp [in SN.expressions]
rinstInst_exp_var [in SN.expressions]
rinstInst_exp_case [in SN.expressions]
rinstInst_exp_bool [in SN.expressions]
rinstInst_exp_arith [in SN.expressions]
rinstInst_exp_lam [in SN.expressions]
rinstInst_exp [in SN.sn_lam]

S

scons_comp [in fintype]
scons_eta_id [in fintype]
scons_eta [in fintype]
scons_comp [in SN.unscoped]
scons_eta_id [in SN.unscoped]
scons_eta [in SN.unscoped]
size_ind [in header_extensible]
sn_fundamental_var [in SN.sn_var]
sn_lam [in SN.sn]
some_none_explosion [in header_extensible]
Some_inj [in header_extensible]
star_If1 [in SN.sn_bool]
star_plus2 [in SN.sn_arith]
star_plus1 [in SN.sn_arith]
star_trans [in SN.defs]
star_appR [in SN.sn_lam]
star_appL [in SN.sn_lam]
stepBeta' [in SN.sn_lam]
step_inst_var [in SN.sn_var]
step_anti_renaming_var [in SN.sn_var]

T

typeof_sound [in GDTC.miniML_results]
typeof_sound [in GDTC.miniML_nofix_results]
ty_induction [in GDTC.miniML_results]
ty_induction [in GDTC.miniML_nofix_results]

U

up_ren_ren [in fintype]
up_ren_ext [in SN.sn]
up_ren_ren [in SN.unscoped]

V

val_inclusion [in SN.sn_var]
varLRen_exp [in SN.expressions]
varL_exp [in SN.expressions]
varL_exp [in SN.sn_lam]

W

whnf_anti_renaming_bool [in SN.sn_bool]
whnf_anti_renaming_arith [in SN.sn_arith]
whnf_anti_renaming_var [in SN.sn_var]
whnf_anti_renaming_lam [in SN.sn_lam]
wn [in SN.sn]
wn_fundamental_var [in SN.sn_var]
wtyped_inv_opt [in TypeSafetyAgda.TypeSafety]
wtyped_inv_arr [in TypeSafetyAgda.TypeSafety]
wtyped_inv_plus [in TypeSafetyAgda.TypeSafety]

---

Constructor Index

A

ab [in SN.expressions]
app [in Counting.section2_count]
app [in GDTC.features]
app [in Counting.section2_count_metacoq]
app [in SN.expressions]
Arr [in GDTC.features]
arr [in SN.expressions]
atom [in TypeSafetyAgda.extensible_array]

B

Bool [in GDTC.features]
Boolean [in GDTC.features]
boolTy [in SN.expressions]

C

Case [in GDTC.features]
Clos [in GDTC.features]
constBool [in Counting.section2_count]
constBool [in GDTC.features]
constBool [in Counting.section2_count_metacoq]
constBool [in SN.expressions]
constNat [in Counting.section2_count]
constNat [in Counting.section2_count_metacoq]
constNat [in SN.expressions]

E

eval_in_opt [in TypeSafetyAgda.TypeSafety]
eval_in_arr [in TypeSafetyAgda.TypeSafety]
eval_in_plus [in TypeSafetyAgda.TypeSafety]
exp_fix_C [in GDTC.miniML]
exp_case_C [in GDTC.miniML]
exp_arith_C [in GDTC.miniML]
exp_bool_C [in GDTC.miniML]
exp_lam_C [in GDTC.miniML]
exp_case_C [in GDTC.miniML_nofix]
exp_arith_C [in GDTC.miniML_nofix]
exp_bool_C [in GDTC.miniML_nofix]
exp_lam_C [in GDTC.miniML_nofix]
E_strong_In [in SN.sn_var]

F

features [in header_metacoq]
fixp [in GDTC.features]

G

GenCons [in header_metacoq]
genCons [in header_metacoq]
GenNil [in header_metacoq]
genNil [in header_metacoq]

H

hasty_If [in SN.sn_bool]
hasty_ConstBool [in SN.sn_bool]
hasty_plus [in SN.sn_arith]
hasty_ConstNat [in SN.sn_arith]
hasty_lam [in SN.sn_lam]
hasty_app [in SN.sn_lam]

I

ids [in fintype]
ids [in SN.unscoped]
If [in Counting.section2_count]
If [in GDTC.features]
If [in Counting.section2_count_metacoq]
If [in SN.expressions]
imp [in tactics]
imprev [in tactics]
inj_arith_arith [in Counting.section2_count]
inj_lam_arith [in Counting.section2_count]
inj_var_arith [in Counting.section2_count]
inj_bool_bool [in Counting.section2_count]
inj_lam_bool [in Counting.section2_count]
inj_var_bool [in Counting.section2_count]
inj_lam_lam [in Counting.section2_count]
inj_var_lam [in Counting.section2_count]
inj_arith_arith [in Counting.section2_count_metacoq]
inj_lam_arith [in Counting.section2_count_metacoq]
inj_var_arith [in Counting.section2_count_metacoq]
inj_bool_bool [in Counting.section2_count_metacoq]
inj_lam_bool [in Counting.section2_count_metacoq]
inj_var_bool [in Counting.section2_count_metacoq]
inj_lam_lam [in Counting.section2_count_metacoq]
inj_var_lam [in Counting.section2_count_metacoq]
inl_step_arith [in SN.sn]
inl_step_bool [in SN.sn]
inl_step_lam [in SN.sn]
inl_step_var [in SN.sn]
inl_has_ty_arith [in SN.sn]
inl_has_ty_bool [in SN.sn]
inl_has_ty_lam [in SN.sn]
inl_has_ty_var [in SN.sn]
In_exp_arith [in SN.expressions]
In_exp_bool [in SN.expressions]
In_exp_lam [in SN.expressions]
In_exp_var [in SN.expressions]
In_ty_arith [in SN.expressions]
In_ty_bool [in SN.expressions]
In_ty_lam [in SN.expressions]
In_exp_opt [in TypeSafetyAgda.extensible_array]
In_exp_arr [in TypeSafetyAgda.extensible_array]
In_exp_plus [in TypeSafetyAgda.extensible_array]

L

lam [in Counting.section2_count]
lam [in GDTC.features]
lam [in Counting.section2_count_metacoq]
lookup [in TypeSafetyAgda.TypeSafety]
L_rec [in TypeSafetyAgda.TypeSafety]
L_notfound [in TypeSafetyAgda.TypeSafety]
L_read [in TypeSafetyAgda.TypeSafety]

M

make_Bundle [in header_extensible]

N

Nat [in GDTC.features]
natCase [in SN.expressions]
natTy [in SN.expressions]
nil [in TypeSafetyAgda.extensible_array]
none [in TypeSafetyAgda.extensible_array]
Num [in GDTC.features]
Number [in GDTC.features]

O

ok_ins [in TypeSafetyAgda.TypeSafety]
ok_lookup [in TypeSafetyAgda.TypeSafety]
ok_nil [in TypeSafetyAgda.TypeSafety]
ok_some [in TypeSafetyAgda.TypeSafety]
ok_none [in TypeSafetyAgda.TypeSafety]
ok_plus [in TypeSafetyAgda.TypeSafety]
ok_value [in TypeSafetyAgda.TypeSafety]

P

plus [in Counting.section2_count]
Plus [in GDTC.features]
plus [in Counting.section2_count_metacoq]
plus [in SN.expressions]
plus [in TypeSafetyAgda.extensible_array]

R

RClos [in GDTC.features]
rd [in TypeSafetyAgda.extensible_array]
ren1 [in fintype]
ren1 [in SN.unscoped]
ren2 [in fintype]
ren2 [in SN.unscoped]
ren3 [in fintype]
ren3 [in SN.unscoped]
ren4 [in fintype]
ren4 [in SN.unscoped]
ren5 [in fintype]
ren5 [in SN.unscoped]

S

SNI [in SN.defs]
some [in TypeSafetyAgda.extensible_array]
srefl [in SN.defs]
stepAppL [in SN.sn_lam]
stepAppR [in SN.sn_lam]
stepBeta [in SN.sn_lam]
stepIfBeta [in SN.sn_bool]
stepIf1 [in SN.sn_bool]
stepIf2 [in SN.sn_bool]
stepIf3 [in SN.sn_bool]
stepl [in TypeSafetyAgda.TypeSafety]
stepLam [in SN.sn_lam]
stepPlus [in SN.sn_arith]
stepPlus1 [in SN.sn_arith]
stepPlus2 [in SN.sn_arith]
stepr [in TypeSafetyAgda.TypeSafety]
steprd1 [in TypeSafetyAgda.TypeSafety]
steprd2 [in TypeSafetyAgda.TypeSafety]
stepsome [in TypeSafetyAgda.TypeSafety]
stepwr1 [in TypeSafetyAgda.TypeSafety]
stepwr2 [in TypeSafetyAgda.TypeSafety]
stepwr3 [in TypeSafetyAgda.TypeSafety]
strans [in SN.defs]
subst1 [in fintype]
subst1 [in SN.unscoped]
subst2 [in fintype]
subst2 [in SN.unscoped]
subst3 [in fintype]
subst3 [in SN.unscoped]
subst4 [in fintype]
subst4 [in SN.unscoped]
subst5 [in fintype]
subst5 [in SN.unscoped]
subterm_rel [in header_metacoq]
sum [in TypeSafetyAgda.TypeSafety]

T

TArray [in TypeSafetyAgda.extensible_array]
TNat [in TypeSafetyAgda.extensible_array]
TOption [in TypeSafetyAgda.extensible_array]
ty_arith_C [in GDTC.miniML]
ty_bool_C [in GDTC.miniML]
ty_lam_C [in GDTC.miniML]
ty_arith_C [in GDTC.miniML_nofix]
ty_bool_C [in GDTC.miniML_nofix]
ty_lam_C [in GDTC.miniML_nofix]

U

up_exp [in SN.expressions]

V

value_fix_C [in GDTC.miniML]
value_arith_C [in GDTC.miniML]
value_bool_C [in GDTC.miniML]
value_lam_C [in GDTC.miniML]
value_arith_C [in GDTC.miniML_nofix]
value_bool_C [in GDTC.miniML_nofix]
value_lam_C [in GDTC.miniML_nofix]
var [in Counting.section2_count]
var [in GDTC.features]
var [in Counting.section2_count_metacoq]
var [in SN.expressions]
var_has_ty [in SN.sn_var]
vtypeis_Fix [in GDTC.miniML_results]
vtypeis_Arith [in GDTC.miniML_results]
vtypeis_Bool [in GDTC.miniML_results]
vtypeis_Lam [in GDTC.miniML_results]
vtypeis_Arith [in GDTC.miniML_nofix_results]
vtypeis_Bool [in GDTC.miniML_nofix_results]
vtypeis_Lam [in GDTC.miniML_nofix_results]
vtypeis_arith_C [in GDTC.GDTC]
vtypeis_bool_C [in GDTC.GDTC]

W

wf_value_RC [in GDTC.GDTC]
wf_value_C [in GDTC.GDTC]
wr [in TypeSafetyAgda.extensible_array]
wtyped_in_opt [in TypeSafetyAgda.TypeSafety]
wtyped_in_arr [in TypeSafetyAgda.TypeSafety]
wtyped_in_plus [in TypeSafetyAgda.TypeSafety]

---

Axiom Index

P

pext [in SN.axioms]
pext [in axioms]

---

Projection Index

F

features [in header_metacoq]

I

ids [in fintype]
ids [in SN.unscoped]
imp [in tactics]
imprev [in tactics]
inj [in Counting.section2_count]
inj [in Counting.section2_count_metacoq]
in_rel [in header_metacoq]
in_subtype [in header_metacoq]

R

ren1 [in fintype]
ren1 [in SN.unscoped]
ren2 [in fintype]
ren2 [in SN.unscoped]
ren3 [in fintype]
ren3 [in SN.unscoped]
ren4 [in fintype]
ren4 [in SN.unscoped]
ren5 [in fintype]
ren5 [in SN.unscoped]
retr [in Counting.section2_count]
retr [in Counting.section2_count_metacoq]
retract_tight [in Counting.section2_count]
retract_works [in Counting.section2_count]
retract_tight [in Counting.section2_count_metacoq]
retract_works [in Counting.section2_count_metacoq]
retract_tight [in header_extensible]
retract_works [in header_extensible]
retract_R [in header_extensible]
retract_I [in header_extensible]

S

subst1 [in fintype]
subst1 [in SN.unscoped]
subst2 [in fintype]
subst2 [in SN.unscoped]
subst3 [in fintype]
subst3 [in SN.unscoped]
subst4 [in fintype]
subst4 [in SN.unscoped]
subst5 [in fintype]
subst5 [in SN.unscoped]
subterm_rel [in header_metacoq]

U

up_exp [in SN.expressions]

---

Inductive Index

E

eval [in TypeSafetyAgda.TypeSafety]
eval_arr [in TypeSafetyAgda.TypeSafety]
eval_opt [in TypeSafetyAgda.TypeSafety]
eval_plus [in TypeSafetyAgda.TypeSafety]
exp [in GDTC.miniML]
exp [in GDTC.miniML_nofix]
exp [in SN.expressions]
exp [in TypeSafetyAgda.extensible_array]
Exp_arith [in Counting.section2_count]
Exp_bool [in Counting.section2_count]
Exp_lam [in Counting.section2_count]
exp_arith [in Counting.section2_count]
exp_bool [in Counting.section2_count]
exp_lam [in Counting.section2_count]
exp_var [in Counting.section2_count]
exp_fix [in GDTC.features]
exp_case [in GDTC.features]
exp_arith [in GDTC.features]
exp_bool [in GDTC.features]
exp_lam [in GDTC.features]
Exp_arith [in Counting.section2_count_metacoq]
Exp_bool [in Counting.section2_count_metacoq]
Exp_lam [in Counting.section2_count_metacoq]
exp_arith [in Counting.section2_count_metacoq]
exp_bool [in Counting.section2_count_metacoq]
exp_lam [in Counting.section2_count_metacoq]
exp_var [in Counting.section2_count_metacoq]
exp_var [in SN.expressions]
exp_case [in SN.expressions]
exp_bool [in SN.expressions]
exp_arith [in SN.expressions]
exp_lam [in SN.expressions]
exp_arr [in TypeSafetyAgda.extensible_array]
exp_opt [in TypeSafetyAgda.extensible_array]
exp_plus [in TypeSafetyAgda.extensible_array]
E_strong' [in SN.sn_var]

G

GenList [in header_metacoq]
genList [in header_metacoq]

H

has_ty_bool [in SN.sn_bool]
has_ty_arith [in SN.sn_arith]
has_ty_var [in SN.sn_var]
has_ty [in SN.sn]
has_ty_lam [in SN.sn_lam]
has_features [in header_metacoq]

I

Imp [in tactics]
ImpRev [in tactics]

L

L [in TypeSafetyAgda.TypeSafety]

R

Ren1 [in fintype]
Ren1 [in SN.unscoped]
Ren2 [in fintype]
Ren2 [in SN.unscoped]
Ren3 [in fintype]
Ren3 [in SN.unscoped]
Ren4 [in fintype]
Ren4 [in SN.unscoped]
Ren5 [in fintype]
Ren5 [in SN.unscoped]

S

sn [in SN.defs]
star [in SN.defs]
step [in SN.sn]
step_bool [in SN.sn_bool]
step_arith [in SN.sn_arith]
step_var [in SN.sn_var]
step_lam [in SN.sn_lam]
Subst1 [in fintype]
Subst1 [in SN.unscoped]
Subst2 [in fintype]
Subst2 [in SN.unscoped]
Subst3 [in fintype]
Subst3 [in SN.unscoped]
Subst4 [in fintype]
Subst4 [in SN.unscoped]
Subst5 [in fintype]
Subst5 [in SN.unscoped]
subtermC [in header_metacoq]

T

ty [in GDTC.miniML]
ty [in GDTC.miniML_nofix]
ty [in SN.expressions]
ty [in TypeSafetyAgda.extensible_array]
ty_arith [in GDTC.features]
ty_bool [in GDTC.features]
ty_lam [in GDTC.features]
ty_arith [in SN.expressions]
ty_bool [in SN.expressions]
ty_lam [in SN.expressions]

U

Up_exp [in SN.expressions]

V

value [in GDTC.miniML]
value [in GDTC.miniML_nofix]
value_fix [in GDTC.features]
value_arith [in GDTC.features]
value_bool [in GDTC.features]
value_lam [in GDTC.features]
Var [in fintype]
Var [in SN.unscoped]
vtypeis [in GDTC.miniML_results]
vtypeis [in GDTC.miniML_nofix_results]
vtypeis_fix [in GDTC.GDTC]
vtypeis_arith [in GDTC.GDTC]
vtypeis_bool [in GDTC.GDTC]
vtypeis_lam [in GDTC.GDTC]

W

wtyped [in TypeSafetyAgda.TypeSafety]
wtyped_arr [in TypeSafetyAgda.TypeSafety]
wtyped_opt [in TypeSafetyAgda.TypeSafety]
wtyped_plus [in TypeSafetyAgda.TypeSafety]

---

Section Index

A

Arith [in Counting.section2_count]
Arith [in GDTC.features]
Arith [in Counting.section2_count_metacoq]

B

bool [in Counting.section2_count_metacoq]
Booleans [in GDTC.features]

C

count [in Counting.section2_count]
count_again [in Counting.section2_count]
count_again.sec [in Counting.section2_count_metacoq]

E

exp [in SN.expressions]
exp [in TypeSafetyAgda.extensible_array]
exp_var [in SN.expressions]
exp_case [in SN.expressions]
exp_bool [in SN.expressions]
exp_arith [in SN.expressions]
exp_lam [in SN.expressions]
exp_arr [in TypeSafetyAgda.extensible_array]
exp_opt [in TypeSafetyAgda.extensible_array]
exp_plus [in TypeSafetyAgda.extensible_array]

F

Fix [in GDTC.features]

L

lam [in Counting.section2_count_metacoq]
Lambdas [in GDTC.features]

M

MiniML_Bool [in SN.sn_bool]
MiniML_Arith [in SN.sn_arith]
MiniML_var [in SN.sn_var]
MiniML_Lambda [in SN.sn_lam]
MiniML_Fix [in GDTC.GDTC]
MiniML_Case [in GDTC.GDTC]
MiniML_Arith [in GDTC.GDTC]
MiniML_Bool [in GDTC.GDTC]
MiniML_Lambda [in GDTC.GDTC]

N

NatCase [in GDTC.features]

O

Option [in TypeSafetyAgda.TypeSafety]

P

Plus [in TypeSafetyAgda.TypeSafety]

S

SmartConstructors [in Counting.section2_count]
SmartConstructors [in Counting.section2_count_metacoq]

T

ty [in SN.expressions]
ty [in TypeSafetyAgda.extensible_array]
ty_arith [in SN.expressions]
ty_bool [in SN.expressions]
ty_lam [in SN.expressions]

V

var [in Counting.section2_count_metacoq]

---

Instance Index

A

arith_features [in Counting.section2_count_metacoq]

B

bool_features [in Counting.section2_count_metacoq]

E

exp_features [in TypeSafetyAgda.TypeSafety]
exp_features [in SN.sn]

H

has_ty_features [in SN.sn]

I

idsRen [in SN.unscoped]
In_ty_lam' [in GDTC.features]
in_rel_bool [in Counting.section2_count_metacoq]
in_rel_lam [in Counting.section2_count_metacoq]

L

lam_features [in Counting.section2_count_metacoq]

N

nat_subterm' [in header_metacoq]

R

Ren_exp [in SN.expressions]
retract_bool_bool [in Counting.section2_count]
retract_lam_bool [in Counting.section2_count]
retract_var_bool [in Counting.section2_count]
retract_lam_lam [in Counting.section2_count]
retract_var_lam [in Counting.section2_count]
retract_step_rev_instance [in SN.sn_bool]
retract_step_instance [in SN.sn_bool]
retract_has_ty_rev_instance [in SN.sn_bool]
retract_has_ty_instance [in SN.sn_bool]
retract_step_rev_instance [in SN.sn_arith]
retract_step_instance [in SN.sn_arith]
retract_has_ty_rev_instance [in SN.sn_arith]
retract_has_ty_instance [in SN.sn_arith]
retract_has_ty_rev_instance [in SN.sn_var]
retract_has_ty_instance [in SN.sn_var]
retract_has_ty_rev_instance' [in TypeSafetyAgda.TypeSafety]
retract_has_ty_instance' [in TypeSafetyAgda.TypeSafety]
retract_has_ty_rev_instance_opt [in TypeSafetyAgda.TypeSafety]
retract_has_ty_instance_opt [in TypeSafetyAgda.TypeSafety]
retract_has_ty_rev_instance [in TypeSafetyAgda.TypeSafety]
retract_has_ty_instance [in TypeSafetyAgda.TypeSafety]
retract_bool_bool [in Counting.section2_count_metacoq]
retract_lam_bool [in Counting.section2_count_metacoq]
retract_var_bool [in Counting.section2_count_metacoq]
retract_lam_lam [in Counting.section2_count_metacoq]
retract_var_lam [in Counting.section2_count_metacoq]
retract_option [in header_extensible]
retract_exp_bool_exp [in SN.expressions]
retract_exp_arith_exp [in SN.expressions]
retract_exp_lam_exp [in SN.expressions]
retract_exp_var_exp [in SN.expressions]
retract_ty_arith_ty [in SN.expressions]
retract_ty_bool_ty [in SN.expressions]
retract_ty_lam_ty [in SN.expressions]
retract_step_rev_instance [in SN.sn_lam]
retract_step_instance [in SN.sn_lam]
retract_has_ty_rev_instance [in SN.sn_lam]
retract_has_ty_instance [in SN.sn_lam]
retract_exp_arr_exp [in TypeSafetyAgda.extensible_array]
retract_exp_opt_exp [in TypeSafetyAgda.extensible_array]
retract_exp_plus_exp [in TypeSafetyAgda.extensible_array]
ret_ty_arith [in GDTC.miniML]
ret_ty_bool [in GDTC.miniML]
ret_ty_lam [in GDTC.miniML]
ret_fix_arith [in GDTC.miniML]
ret_value_arith [in GDTC.miniML]
ret_value_bool [in GDTC.miniML]
ret_value_lam [in GDTC.miniML]
ret_exp_fix [in GDTC.miniML]
ret_exp_case [in GDTC.miniML]
ret_exp_arith [in GDTC.miniML]
ret_exp_bool [in GDTC.miniML]
ret_exp_lam [in GDTC.miniML]
ret_ty_arith [in GDTC.miniML_nofix]
ret_ty_bool [in GDTC.miniML_nofix]
ret_ty_lam [in GDTC.miniML_nofix]
ret_value_arith [in GDTC.miniML_nofix]
ret_value_bool [in GDTC.miniML_nofix]
ret_value_lam [in GDTC.miniML_nofix]
ret_exp_case [in GDTC.miniML_nofix]
ret_exp_arith [in GDTC.miniML_nofix]
ret_exp_bool [in GDTC.miniML_nofix]
ret_exp_lam [in GDTC.miniML_nofix]

S

step_features [in SN.sn]
Subst_exp [in SN.expressions]
subterm_ty_arith' [in GDTC.features]
subterm_ty_arith [in GDTC.features]
subterm_ty_bool [in GDTC.features]
subt_arith [in GDTC.GDTC]
subt_bool [in GDTC.GDTC]

T

ty_features [in SN.sn]

U

Up_exp_exp [in SN.expressions]

V

VarInstance_exp [in SN.expressions]
vtypeis_inj_imprev_lam' [in GDTC.GDTC]
vtypeis_inj_imp_lam' [in GDTC.GDTC]
vtypeis_inj_imprev_fix [in GDTC.GDTC]
vtypeis_inj_imp_fix [in GDTC.GDTC]
vtypeis_inj_imprev_arith' [in GDTC.GDTC]
vtypeis_inj_imp_arith' [in GDTC.GDTC]
vtypeis_inj_imprev_arith [in GDTC.GDTC]
vtypeis_inj_imp_arith [in GDTC.GDTC]
vtypeis_inj_imprev_bool [in GDTC.GDTC]
vtypeis_inj_imp_bool [in GDTC.GDTC]
vtypeis_inj_imprev [in GDTC.GDTC]
vtypeis_inj_imp [in GDTC.GDTC]

---

Abbreviation Index

F

fin [in SN.unscoped]

I

included [in GDTC.features]
included [in header_extensible]
inj [in header_extensible]

R

retr [in header_extensible]

V

var_exp [in SN.sn_lam]

---

Definition Index

A

ab_ [in SN.expressions]
ap [in fintype]
ap [in SN.unscoped]
apc [in fintype]
apc [in SN.unscoped]
App [in GDTC.features]
app_ [in Counting.section2_count]
app_ [in Counting.section2_count_metacoq]
app_ [in SN.expressions]
arr_ [in SN.expressions]
atom_ [in TypeSafetyAgda.extensible_array]

B

beq [in GDTC.miniML_results]
beq [in GDTC.miniML_nofix_results]
beq_ty_arith [in GDTC.GDTC]
beq_ty_bool [in GDTC.GDTC]
beq_ty_lam [in GDTC.GDTC]
boolTy_ [in SN.expressions]
buildImp [in header_metacoq]

C

cns [in header_metacoq]
cod [in SN.axioms]
cod_comp [in SN.axioms]
cod_ext [in SN.axioms]
cod_id [in SN.axioms]
cod_map [in SN.axioms]
comp [in fintype]
compose_fixpoint [in header_metacoq]
compRenRen_exp [in SN.expressions]
compRenRen_exp_var [in SN.expressions]
compRenRen_exp_case [in SN.expressions]
compRenRen_exp_bool [in SN.expressions]
compRenRen_exp_arith [in SN.expressions]
compRenRen_exp_lam [in SN.expressions]
compRenSubst_exp [in SN.expressions]
compRenSubst_exp_var [in SN.expressions]
compRenSubst_exp_case [in SN.expressions]
compRenSubst_exp_bool [in SN.expressions]
compRenSubst_exp_arith [in SN.expressions]
compRenSubst_exp_lam [in SN.expressions]
compSubstRen_exp [in SN.expressions]
compSubstRen_exp_var [in SN.expressions]
compSubstRen_exp_case [in SN.expressions]
compSubstRen_exp_bool [in SN.expressions]
compSubstRen_exp_arith [in SN.expressions]
compSubstRen_exp_lam [in SN.expressions]
compSubstSubst_exp [in SN.expressions]
compSubstSubst_exp_var [in SN.expressions]
compSubstSubst_exp_case [in SN.expressions]
compSubstSubst_exp_bool [in SN.expressions]
compSubstSubst_exp_arith [in SN.expressions]
compSubstSubst_exp_lam [in SN.expressions]
constBool_ [in Counting.section2_count]
constBool_ [in Counting.section2_count_metacoq]
constBool_ [in SN.expressions]
constNat_ [in Counting.section2_count]
constNat_ [in Counting.section2_count_metacoq]
constNat_ [in SN.expressions]
Count_gt_arith [in Counting.section2_count]
Count_arith [in Counting.section2_count]
count_arith [in Counting.section2_count]
Count_gt_bool [in Counting.section2_count]
Count_bool [in Counting.section2_count]
Count_gt_lam [in Counting.section2_count]
Count_lam [in Counting.section2_count]
count_bool [in Counting.section2_count]
count_lam [in Counting.section2_count]
count_var [in Counting.section2_count]
count_again.count_var [in Counting.section2_count_metacoq]
count_var [in Counting.section2_count_metacoq]

D

destArity [in header_metacoq]

E

E [in SN.sn]
eval [in GDTC.miniML_results]
eval [in GDTC.miniML_nofix_results]
eval_fix [in GDTC.GDTC]
eval_case [in GDTC.GDTC]
eval_arith [in GDTC.GDTC]
eval_bool [in GDTC.GDTC]
Exp_bool_induction [in Counting.section2_count]
Exp_lam_induction [in Counting.section2_count]
Exp_bool_induction [in Counting.section2_count_metacoq]
Exp_lam_induction [in Counting.section2_count_metacoq]
extRen_exp [in SN.expressions]
extRen_exp_var [in SN.expressions]
extRen_exp_case [in SN.expressions]
extRen_exp_bool [in SN.expressions]
extRen_exp_arith [in SN.expressions]
extRen_exp_lam [in SN.expressions]
ext_exp [in SN.expressions]
ext_exp_var [in SN.expressions]
ext_exp_case [in SN.expressions]
ext_exp_bool [in SN.expressions]
ext_exp_arith [in SN.expressions]
ext_exp_lam [in SN.expressions]
E_strong [in SN.sn_var]
E_ [in SN.sn_var]

F

fin [in fintype]
fixNames [in header_metacoq]
Forall [in header_metacoq]
ForallN [in header_metacoq]
Forall' [in header_metacoq]
funcomp [in fintype]
funcomp [in SN.axioms]
funcomp [in SN.unscoped]

G

G [in SN.sn_var]
genIH [in header_metacoq]
genStatement [in header_metacoq]
genStatement_Fix [in header_metacoq]
genStatement_no_lt [in header_metacoq]
getName [in header_metacoq]
get_In [in header_extensible]
get_lemmas_and_name [in header_metacoq]
get_lemmas [in header_metacoq]
get_name [in header_metacoq]
get_name_of [in header_metacoq]
get_features [in header_metacoq]
G_strong [in SN.sn_var]

H

has_ty_sem_strong [in SN.sn_var]
has_ty_sem [in SN.sn_var]

I

id [in fintype]
id [in SN.unscoped]
idren [in fintype]
idSubst_exp [in SN.expressions]
idSubst_exp_var [in SN.expressions]
idSubst_exp_case [in SN.expressions]
idSubst_exp_bool [in SN.expressions]
idSubst_exp_arith [in SN.expressions]
idSubst_exp_lam [in SN.expressions]
if_ [in Counting.section2_count]
if_ [in Counting.section2_count_metacoq]
If_ [in SN.expressions]
in_bool [in Counting.section2_count]
in_lam [in Counting.section2_count]
in_var [in Counting.section2_count]
In_fix [in GDTC.features]
In_case [in GDTC.features]
In_ty_arith [in GDTC.features]
In_arith [in GDTC.features]
In_bool [in GDTC.features]
In_ty_bool [in GDTC.features]
In_lam [in GDTC.features]
In_ty_lam [in GDTC.features]
in_bool [in Counting.section2_count_metacoq]
in_lam [in Counting.section2_count_metacoq]
in_var [in Counting.section2_count_metacoq]

L

L [in SN.sn]
Lam [in GDTC.features]
lam_ [in Counting.section2_count]
lam_ [in Counting.section2_count_metacoq]
lift [in header_extensible]
list_comp [in SN.axioms]
list_id [in SN.axioms]
list_ext [in SN.axioms]
L_close_ren [in SN.sn]
L_strong [in SN.sn]
L_ren [in SN.sn]
L_strong_lam [in SN.sn_lam]

M

mkDefinitionType [in header_metacoq]
mkLemma [in header_metacoq]
mkVariable [in header_metacoq]
ModularFixpointN [in header_metacoq]
ModularFixpoint2 [in header_metacoq]

N

name_after_dot [in header_metacoq]
name_after_dot' [in header_metacoq]
natCase_ [in SN.expressions]
natTy_ [in SN.expressions]
nil_ [in TypeSafetyAgda.extensible_array]
None [in SN.unscoped]
none_ [in TypeSafetyAgda.extensible_array]
null [in fintype]

P

plus_ [in Counting.section2_count]
plus_ [in Counting.section2_count_metacoq]
plus_ [in SN.expressions]
plus_ [in TypeSafetyAgda.extensible_array]
prod_comp [in SN.axioms]
prod_ext [in SN.axioms]
prod_id [in SN.axioms]
prod_map [in SN.axioms]

Q

quote_list [in header_metacoq]

R

rd_ [in TypeSafetyAgda.extensible_array]
remove_suffix [in header_metacoq]
remove_injs [in header_metacoq]
ren [in fintype]
ren_exp [in SN.expressions]
ren_exp_var [in SN.expressions]
ren_exp_case [in SN.expressions]
ren_exp_bool [in SN.expressions]
ren_exp_arith [in SN.expressions]
ren_exp_lam [in SN.expressions]
replace_ext [in header_metacoq]
replace_consts [in header_metacoq]
replace_terms [in header_metacoq]
replace_const [in header_metacoq]
replace_term [in header_metacoq]
rinstInst_up_exp_exp [in SN.expressions]
rinst_inst_exp [in SN.expressions]
rinst_inst_exp_var [in SN.expressions]
rinst_inst_exp_case [in SN.expressions]
rinst_inst_exp_bool [in SN.expressions]
rinst_inst_exp_arith [in SN.expressions]
rinst_inst_exp_lam [in SN.expressions]

S

s [in Counting.section2_count]
s [in Counting.section2_count_metacoq]
scons [in fintype]
scons [in SN.unscoped]
shift [in fintype]
shift [in SN.unscoped]
Some [in SN.unscoped]
some_ [in TypeSafetyAgda.extensible_array]
split_forall_impl [in header_metacoq]
subst_exp [in SN.expressions]
subst_exp_var [in SN.expressions]
subst_exp_case [in SN.expressions]
subst_exp_bool [in SN.expressions]
subst_exp_arith [in SN.expressions]
subst_exp_lam [in SN.expressions]

T

tmMkDefinition [in header_metacoq]
tmTryInferInstance [in header_metacoq]
typeof [in GDTC.miniML_results]
typeof [in GDTC.miniML_nofix_results]
typeof_fix [in GDTC.GDTC]
typeof_case [in GDTC.GDTC]
typeof_arith [in GDTC.GDTC]
typeof_bool [in GDTC.GDTC]
typeof_lam [in GDTC.GDTC]

U

upExtRen_exp_exp [in SN.expressions]
upExt_exp_exp [in SN.expressions]
upId_exp_exp [in SN.expressions]
upRen_exp_exp [in SN.expressions]
up_ren [in fintype]
up_subst_subst_exp_exp [in SN.expressions]
up_subst_ren_exp_exp [in SN.expressions]
up_ren_subst_exp_exp [in SN.expressions]
up_ren_ren_exp_exp [in SN.expressions]
up_exp_exp [in SN.expressions]
up_ren [in SN.unscoped]

V

Var [in GDTC.features]
var_ [in Counting.section2_count]
var_zero [in fintype]
var_ [in Counting.section2_count_metacoq]
var_ [in SN.expressions]
var_zero [in SN.unscoped]

W

whnf [in SN.sn]
wr_ [in TypeSafetyAgda.extensible_array]

---

Record Index

B

Bundle [in header_extensible]

H

has_features [in header_metacoq]

I

Imp [in tactics]
ImpRev [in tactics]
InRelC [in header_metacoq]

R

Ren1 [in fintype]
Ren1 [in SN.unscoped]
Ren2 [in fintype]
Ren2 [in SN.unscoped]
Ren3 [in fintype]
Ren3 [in SN.unscoped]
Ren4 [in fintype]
Ren4 [in SN.unscoped]
Ren5 [in fintype]
Ren5 [in SN.unscoped]
retract [in Counting.section2_count]
retract [in Counting.section2_count_metacoq]
retract [in header_extensible]

S

Subst1 [in fintype]
Subst1 [in SN.unscoped]
Subst2 [in fintype]
Subst2 [in SN.unscoped]
Subst3 [in fintype]
Subst3 [in SN.unscoped]
Subst4 [in fintype]
Subst4 [in SN.unscoped]
Subst5 [in fintype]
Subst5 [in SN.unscoped]
subtermC [in header_metacoq]

U

Up_exp [in SN.expressions]

V

Var [in fintype]
Var [in SN.unscoped]

---

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(32 entries)