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

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

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

(1 entry)

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

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

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

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

(1 entry)

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

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

(17 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(8 entries)

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

(1 entry)

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

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

(90 entries)

---

Global Index

A

all [constructor, in Autosubst.SystemFCBV]
ap [definition, in Autosubst.fintype]
apc [definition, in Autosubst.fintype]
app [constructor, in Autosubst.SystemFCBV]
arr [constructor, in Autosubst.SystemFCBV]
axioms [library]

C

CommaNotation [module, in Autosubst.fintype]
_ , _ (subst_scope) [notation, in Autosubst.fintype]
comp [definition, in Autosubst.fintype]
compComp_vl [lemma, in Autosubst.SystemFCBV]
compComp_tm [lemma, in Autosubst.SystemFCBV]
compComp_ty [lemma, in Autosubst.SystemFCBV]
compComp'_vl [lemma, in Autosubst.SystemFCBV]
compComp'_tm [lemma, in Autosubst.SystemFCBV]
compComp'_ty [lemma, in Autosubst.SystemFCBV]
compRenRen_vl [definition, in Autosubst.SystemFCBV]
compRenRen_tm [definition, in Autosubst.SystemFCBV]
compRenRen_ty [definition, in Autosubst.SystemFCBV]
compRenSubst_vl [definition, in Autosubst.SystemFCBV]
compRenSubst_tm [definition, in Autosubst.SystemFCBV]
compRenSubst_ty [definition, in Autosubst.SystemFCBV]
compRen_vl [lemma, in Autosubst.SystemFCBV]
compRen_tm [lemma, in Autosubst.SystemFCBV]
compRen_ty [lemma, in Autosubst.SystemFCBV]
compRen'_vl [lemma, in Autosubst.SystemFCBV]
compRen'_tm [lemma, in Autosubst.SystemFCBV]
compRen'_ty [lemma, in Autosubst.SystemFCBV]
compSubstRen__vl [definition, in Autosubst.SystemFCBV]
compSubstRen__tm [definition, in Autosubst.SystemFCBV]
compSubstRen__ty [definition, in Autosubst.SystemFCBV]
compSubstSubst_vl [definition, in Autosubst.SystemFCBV]
compSubstSubst_tm [definition, in Autosubst.SystemFCBV]
compSubstSubst_ty [definition, in Autosubst.SystemFCBV]
congr_tlam [lemma, in Autosubst.SystemFCBV]
congr_lam [lemma, in Autosubst.SystemFCBV]
congr_vt [lemma, in Autosubst.SystemFCBV]
congr_tapp [lemma, in Autosubst.SystemFCBV]
congr_app [lemma, in Autosubst.SystemFCBV]
congr_all [lemma, in Autosubst.SystemFCBV]
congr_arr [lemma, in Autosubst.SystemFCBV]
consistency [lemma, in Autosubst.sem]
ctx [definition, in Autosubst.sem]

E

E [abbreviation, in Autosubst.sem]
empty [definition, in Autosubst.sem]
eval [inductive, in Autosubst.sem]
eval_val [constructor, in Autosubst.sem]
eval_tapp [constructor, in Autosubst.sem]
eval_app [constructor, in Autosubst.sem]
extRen_vl [definition, in Autosubst.SystemFCBV]
extRen_tm [definition, in Autosubst.SystemFCBV]
extRen_ty [definition, in Autosubst.SystemFCBV]
ext_vl [definition, in Autosubst.SystemFCBV]
ext_tm [definition, in Autosubst.SystemFCBV]
ext_ty [definition, in Autosubst.SystemFCBV]
E_subst1 [lemma, in Autosubst.sem]

F

fin [definition, in Autosubst.fintype]
fintype [library]
funcomp [definition, in Autosubst.fintype]

H

has_ty_ind [definition, in Autosubst.sem]

I

id [definition, in Autosubst.fintype]
idren [definition, in Autosubst.fintype]
ids [projection, in Autosubst.fintype]
ids [constructor, in Autosubst.fintype]
idSubst_vl [definition, in Autosubst.SystemFCBV]
idSubst_tm [definition, in Autosubst.SystemFCBV]
idSubst_ty [definition, in Autosubst.SystemFCBV]
instId_vl [lemma, in Autosubst.SystemFCBV]
instId_tm [lemma, in Autosubst.SystemFCBV]
instId_ty [lemma, in Autosubst.SystemFCBV]

L

L [definition, in Autosubst.sem]
lam [constructor, in Autosubst.SystemFCBV]
lt_ctx [definition, in Autosubst.sem]
lt_ctx_ren [definition, in Autosubst.sem]

N

nilA [definition, in Autosubst.sem]
normalization [lemma, in Autosubst.sem]
null [definition, in Autosubst.fintype]

P

pext [axiom, in Autosubst.axioms]
pi [lemma, in Autosubst.axioms]

R

ren [definition, in Autosubst.fintype]
renComp_vl [lemma, in Autosubst.SystemFCBV]
renComp_tm [lemma, in Autosubst.SystemFCBV]
renComp_ty [lemma, in Autosubst.SystemFCBV]
renComp'_vl [lemma, in Autosubst.SystemFCBV]
renComp'_tm [lemma, in Autosubst.SystemFCBV]
renComp'_ty [lemma, in Autosubst.SystemFCBV]
renRen_vl [lemma, in Autosubst.SystemFCBV]
renRen_tm [lemma, in Autosubst.SystemFCBV]
renRen_ty [lemma, in Autosubst.SystemFCBV]
renRen'_vl [lemma, in Autosubst.SystemFCBV]
renRen'_tm [lemma, in Autosubst.SystemFCBV]
renRen'_ty [lemma, in Autosubst.SystemFCBV]
Ren_vl [instance, in Autosubst.SystemFCBV]
Ren_tm [instance, in Autosubst.SystemFCBV]
Ren_ty [instance, in Autosubst.SystemFCBV]
ren_vl [definition, in Autosubst.SystemFCBV]
ren_tm [definition, in Autosubst.SystemFCBV]
ren_ty [definition, in Autosubst.SystemFCBV]
ren1 [projection, in Autosubst.fintype]
Ren1 [record, in Autosubst.fintype]
ren1 [constructor, in Autosubst.fintype]
Ren1 [inductive, in Autosubst.fintype]
ren2 [projection, in Autosubst.fintype]
Ren2 [record, in Autosubst.fintype]
ren2 [constructor, in Autosubst.fintype]
Ren2 [inductive, in Autosubst.fintype]
ren3 [projection, in Autosubst.fintype]
Ren3 [record, in Autosubst.fintype]
ren3 [constructor, in Autosubst.fintype]
Ren3 [inductive, in Autosubst.fintype]
ren4 [projection, in Autosubst.fintype]
Ren4 [record, in Autosubst.fintype]
ren4 [constructor, in Autosubst.fintype]
Ren4 [inductive, in Autosubst.fintype]
ren5 [projection, in Autosubst.fintype]
Ren5 [record, in Autosubst.fintype]
ren5 [constructor, in Autosubst.fintype]
Ren5 [inductive, in Autosubst.fintype]
rinstId_vl [lemma, in Autosubst.SystemFCBV]
rinstId_tm [lemma, in Autosubst.SystemFCBV]
rinstId_ty [lemma, in Autosubst.SystemFCBV]
rinstInst_vl [lemma, in Autosubst.SystemFCBV]
rinstInst_tm [lemma, in Autosubst.SystemFCBV]
rinstInst_up_vl_vl [definition, in Autosubst.SystemFCBV]
rinstInst_up_vl_ty [definition, in Autosubst.SystemFCBV]
rinstInst_up_ty_vl [definition, in Autosubst.SystemFCBV]
rinstInst_ty [lemma, in Autosubst.SystemFCBV]
rinstInst_up_ty_ty [definition, in Autosubst.SystemFCBV]
rinst_inst_vl [definition, in Autosubst.SystemFCBV]
rinst_inst_tm [definition, in Autosubst.SystemFCBV]
rinst_inst_ty [definition, in Autosubst.SystemFCBV]

S

scons [definition, in Autosubst.fintype]
scons_comp [lemma, in Autosubst.fintype]
scons_eta_id [lemma, in Autosubst.fintype]
scons_eta [lemma, in Autosubst.fintype]
sem [library]
shift [definition, in Autosubst.fintype]
soundness [lemma, in Autosubst.sem]
soundness_nil [lemma, in Autosubst.sem]
Subst_vl [instance, in Autosubst.SystemFCBV]
Subst_tm [instance, in Autosubst.SystemFCBV]
Subst_ty [instance, in Autosubst.SystemFCBV]
subst_vl [definition, in Autosubst.SystemFCBV]
subst_tm [definition, in Autosubst.SystemFCBV]
subst_ty [definition, in Autosubst.SystemFCBV]
subst1 [projection, in Autosubst.fintype]
Subst1 [record, in Autosubst.fintype]
subst1 [constructor, in Autosubst.fintype]
Subst1 [inductive, in Autosubst.fintype]
subst2 [projection, in Autosubst.fintype]
Subst2 [record, in Autosubst.fintype]
subst2 [constructor, in Autosubst.fintype]
Subst2 [inductive, in Autosubst.fintype]
subst3 [projection, in Autosubst.fintype]
Subst3 [record, in Autosubst.fintype]
subst3 [constructor, in Autosubst.fintype]
Subst3 [inductive, in Autosubst.fintype]
subst4 [projection, in Autosubst.fintype]
Subst4 [record, in Autosubst.fintype]
subst4 [constructor, in Autosubst.fintype]
Subst4 [inductive, in Autosubst.fintype]
subst5 [projection, in Autosubst.fintype]
Subst5 [record, in Autosubst.fintype]
subst5 [constructor, in Autosubst.fintype]
Subst5 [inductive, in Autosubst.fintype]
SystemFCBV [library]

T

tapp [constructor, in Autosubst.SystemFCBV]
tlam [constructor, in Autosubst.SystemFCBV]
tm [inductive, in Autosubst.SystemFCBV]
tm_ty_ind [definition, in Autosubst.sem]
tm_ty [inductive, in Autosubst.sem]
ty [inductive, in Autosubst.SystemFCBV]
typing_subst [lemma, in Autosubst.sem]
typing_ren [lemma, in Autosubst.sem]
ty_tlam [constructor, in Autosubst.sem]
ty_lam [constructor, in Autosubst.sem]
ty_var [constructor, in Autosubst.sem]
ty_val [constructor, in Autosubst.sem]
ty_tapp [constructor, in Autosubst.sem]
ty_app [constructor, in Autosubst.sem]

U

upExtRen_vl_vl [definition, in Autosubst.SystemFCBV]
upExtRen_vl_ty [definition, in Autosubst.SystemFCBV]
upExtRen_ty_vl [definition, in Autosubst.SystemFCBV]
upExtRen_ty_ty [definition, in Autosubst.SystemFCBV]
upExt_vl_vl [definition, in Autosubst.SystemFCBV]
upExt_vl_ty [definition, in Autosubst.SystemFCBV]
upExt_ty_vl [definition, in Autosubst.SystemFCBV]
upExt_ty_ty [definition, in Autosubst.SystemFCBV]
upId_vl_vl [definition, in Autosubst.SystemFCBV]
upId_vl_ty [definition, in Autosubst.SystemFCBV]
upId_ty_vl [definition, in Autosubst.SystemFCBV]
upId_ty_ty [definition, in Autosubst.SystemFCBV]
upRen_vl_vl [definition, in Autosubst.SystemFCBV]
upRen_vl_ty [definition, in Autosubst.SystemFCBV]
upRen_ty_vl [definition, in Autosubst.SystemFCBV]
upRen_ty_ty [definition, in Autosubst.SystemFCBV]
up_ren_ren [lemma, in Autosubst.fintype]
up_ren [definition, in Autosubst.fintype]
up_subst_subst_vl_vl [definition, in Autosubst.SystemFCBV]
up_subst_subst_vl_ty [definition, in Autosubst.SystemFCBV]
up_subst_subst_ty_vl [definition, in Autosubst.SystemFCBV]
up_subst_ren_vl_vl [definition, in Autosubst.SystemFCBV]
up_subst_ren_vl_ty [definition, in Autosubst.SystemFCBV]
up_subst_ren_ty_vl [definition, in Autosubst.SystemFCBV]
up_ren_subst_vl_vl [definition, in Autosubst.SystemFCBV]
up_ren_subst_vl_ty [definition, in Autosubst.SystemFCBV]
up_ren_subst_ty_vl [definition, in Autosubst.SystemFCBV]
up_vl_vl [definition, in Autosubst.SystemFCBV]
up_vl_ty [definition, in Autosubst.SystemFCBV]
up_ty_vl [definition, in Autosubst.SystemFCBV]
up_subst_subst_ty_ty [definition, in Autosubst.SystemFCBV]
up_subst_ren_ty_ty [definition, in Autosubst.SystemFCBV]
up_ren_subst_ty_ty [definition, in Autosubst.SystemFCBV]
up_ty_ty [definition, in Autosubst.SystemFCBV]

V

V [definition, in Autosubst.sem]
Var [record, in Autosubst.fintype]
Var [inductive, in Autosubst.fintype]
VarInstance_vl [instance, in Autosubst.SystemFCBV]
VarInstance_ty [instance, in Autosubst.SystemFCBV]
varLRen_vl [lemma, in Autosubst.SystemFCBV]
varLRen_ty [lemma, in Autosubst.SystemFCBV]
varL_vl [lemma, in Autosubst.SystemFCBV]
varL_ty [lemma, in Autosubst.SystemFCBV]
var_zero [definition, in Autosubst.fintype]
var_vl [constructor, in Autosubst.SystemFCBV]
var_ty [constructor, in Autosubst.SystemFCBV]
VG [definition, in Autosubst.sem]
vl [inductive, in Autosubst.SystemFCBV]
vl_ty_ind [definition, in Autosubst.sem]
vl_ty [inductive, in Autosubst.sem]
vt [constructor, in Autosubst.SystemFCBV]
V_subst [lemma, in Autosubst.sem]
V_weak [lemma, in Autosubst.sem]
V_ren [lemma, in Autosubst.sem]

other

[ _ ; _ ] (fscope) [notation, in Autosubst.SystemFCBV]
[ _ ; _ ] (fscope) [notation, in Autosubst.SystemFCBV]
[ _ ] (fscope) [notation, in Autosubst.SystemFCBV]
⟨ _ ; _ ⟩ (fscope) [notation, in Autosubst.fintype]
⟨ _ ⟩ (fscope) [notation, in Autosubst.fintype]
⟨ _ ; _ ⟩ (fscope) [notation, in Autosubst.SystemFCBV]
⟨ _ ; _ ⟩ (fscope) [notation, in Autosubst.SystemFCBV]
⟨ _ ⟩ (fscope) [notation, in Autosubst.SystemFCBV]
↑ (subst_scope) [notation, in Autosubst.fintype]
_ .. (subst_scope) [notation, in Autosubst.fintype]
_ .: _ (subst_scope) [notation, in Autosubst.fintype]
_ [ _ ; _ ] (subst_scope) [notation, in Autosubst.fintype]
_ [ _ ] (subst_scope) [notation, in Autosubst.fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in Autosubst.fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in Autosubst.fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in Autosubst.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Autosubst.fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in Autosubst.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Autosubst.SystemFCBV]
_ [ _ ; _ ] (subst_scope) [notation, in Autosubst.SystemFCBV]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Autosubst.SystemFCBV]
_ [ _ ; _ ] (subst_scope) [notation, in Autosubst.SystemFCBV]
_ ⟨ _ ⟩ (subst_scope) [notation, in Autosubst.SystemFCBV]
_ [ _ ] (subst_scope) [notation, in Autosubst.SystemFCBV]
⇑__vl (subst_scope) [notation, in Autosubst.SystemFCBV]
⇑__vl (subst_scope) [notation, in Autosubst.SystemFCBV]
⇑__ty (subst_scope) [notation, in Autosubst.SystemFCBV]
⇑__ty (subst_scope) [notation, in Autosubst.SystemFCBV]
⇑__ty (subst_scope) [notation, in Autosubst.SystemFCBV]
var (subst_scope) [notation, in Autosubst.SystemFCBV]
_ __vl (subst_scope) [notation, in Autosubst.SystemFCBV]
_ __vl (subst_scope) [notation, in Autosubst.SystemFCBV]
var (subst_scope) [notation, in Autosubst.SystemFCBV]
_ __ty (subst_scope) [notation, in Autosubst.SystemFCBV]
_ __ty (subst_scope) [notation, in Autosubst.SystemFCBV]
_ >> _ [notation, in Autosubst.fintype]

---

Notation Index

C

_ , _ (subst_scope) [in Autosubst.fintype]

other

[ _ ; _ ] (fscope) [in Autosubst.SystemFCBV]
[ _ ; _ ] (fscope) [in Autosubst.SystemFCBV]
[ _ ] (fscope) [in Autosubst.SystemFCBV]
⟨ _ ; _ ⟩ (fscope) [in Autosubst.fintype]
⟨ _ ⟩ (fscope) [in Autosubst.fintype]
⟨ _ ; _ ⟩ (fscope) [in Autosubst.SystemFCBV]
⟨ _ ; _ ⟩ (fscope) [in Autosubst.SystemFCBV]
⟨ _ ⟩ (fscope) [in Autosubst.SystemFCBV]
↑ (subst_scope) [in Autosubst.fintype]
_ .. (subst_scope) [in Autosubst.fintype]
_ .: _ (subst_scope) [in Autosubst.fintype]
_ [ _ ; _ ] (subst_scope) [in Autosubst.fintype]
_ [ _ ] (subst_scope) [in Autosubst.fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in Autosubst.fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in Autosubst.fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in Autosubst.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Autosubst.fintype]
_ ⟨ _ ⟩ (subst_scope) [in Autosubst.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Autosubst.SystemFCBV]
_ [ _ ; _ ] (subst_scope) [in Autosubst.SystemFCBV]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Autosubst.SystemFCBV]
_ [ _ ; _ ] (subst_scope) [in Autosubst.SystemFCBV]
_ ⟨ _ ⟩ (subst_scope) [in Autosubst.SystemFCBV]
_ [ _ ] (subst_scope) [in Autosubst.SystemFCBV]
⇑__vl (subst_scope) [in Autosubst.SystemFCBV]
⇑__vl (subst_scope) [in Autosubst.SystemFCBV]
⇑__ty (subst_scope) [in Autosubst.SystemFCBV]
⇑__ty (subst_scope) [in Autosubst.SystemFCBV]
⇑__ty (subst_scope) [in Autosubst.SystemFCBV]
var (subst_scope) [in Autosubst.SystemFCBV]
_ __vl (subst_scope) [in Autosubst.SystemFCBV]
_ __vl (subst_scope) [in Autosubst.SystemFCBV]
var (subst_scope) [in Autosubst.SystemFCBV]
_ __ty (subst_scope) [in Autosubst.SystemFCBV]
_ __ty (subst_scope) [in Autosubst.SystemFCBV]
_ >> _ [in Autosubst.fintype]

---

Module Index

C

CommaNotation [in Autosubst.fintype]

---

Library Index

A

axioms

F

fintype

S

sem
SystemFCBV

---

Constructor Index

A

all [in Autosubst.SystemFCBV]
app [in Autosubst.SystemFCBV]
arr [in Autosubst.SystemFCBV]

E

eval_val [in Autosubst.sem]
eval_tapp [in Autosubst.sem]
eval_app [in Autosubst.sem]

I

ids [in Autosubst.fintype]

L

lam [in Autosubst.SystemFCBV]

R

ren1 [in Autosubst.fintype]
ren2 [in Autosubst.fintype]
ren3 [in Autosubst.fintype]
ren4 [in Autosubst.fintype]
ren5 [in Autosubst.fintype]

S

subst1 [in Autosubst.fintype]
subst2 [in Autosubst.fintype]
subst3 [in Autosubst.fintype]
subst4 [in Autosubst.fintype]
subst5 [in Autosubst.fintype]

T

tapp [in Autosubst.SystemFCBV]
tlam [in Autosubst.SystemFCBV]
ty_tlam [in Autosubst.sem]
ty_lam [in Autosubst.sem]
ty_var [in Autosubst.sem]
ty_val [in Autosubst.sem]
ty_tapp [in Autosubst.sem]
ty_app [in Autosubst.sem]

V

var_vl [in Autosubst.SystemFCBV]
var_ty [in Autosubst.SystemFCBV]
vt [in Autosubst.SystemFCBV]

---

Lemma Index

C

compComp_vl [in Autosubst.SystemFCBV]
compComp_tm [in Autosubst.SystemFCBV]
compComp_ty [in Autosubst.SystemFCBV]
compComp'_vl [in Autosubst.SystemFCBV]
compComp'_tm [in Autosubst.SystemFCBV]
compComp'_ty [in Autosubst.SystemFCBV]
compRen_vl [in Autosubst.SystemFCBV]
compRen_tm [in Autosubst.SystemFCBV]
compRen_ty [in Autosubst.SystemFCBV]
compRen'_vl [in Autosubst.SystemFCBV]
compRen'_tm [in Autosubst.SystemFCBV]
compRen'_ty [in Autosubst.SystemFCBV]
congr_tlam [in Autosubst.SystemFCBV]
congr_lam [in Autosubst.SystemFCBV]
congr_vt [in Autosubst.SystemFCBV]
congr_tapp [in Autosubst.SystemFCBV]
congr_app [in Autosubst.SystemFCBV]
congr_all [in Autosubst.SystemFCBV]
congr_arr [in Autosubst.SystemFCBV]
consistency [in Autosubst.sem]

E

E_subst1 [in Autosubst.sem]

I

instId_vl [in Autosubst.SystemFCBV]
instId_tm [in Autosubst.SystemFCBV]
instId_ty [in Autosubst.SystemFCBV]

N

normalization [in Autosubst.sem]

P

pi [in Autosubst.axioms]

R

renComp_vl [in Autosubst.SystemFCBV]
renComp_tm [in Autosubst.SystemFCBV]
renComp_ty [in Autosubst.SystemFCBV]
renComp'_vl [in Autosubst.SystemFCBV]
renComp'_tm [in Autosubst.SystemFCBV]
renComp'_ty [in Autosubst.SystemFCBV]
renRen_vl [in Autosubst.SystemFCBV]
renRen_tm [in Autosubst.SystemFCBV]
renRen_ty [in Autosubst.SystemFCBV]
renRen'_vl [in Autosubst.SystemFCBV]
renRen'_tm [in Autosubst.SystemFCBV]
renRen'_ty [in Autosubst.SystemFCBV]
rinstId_vl [in Autosubst.SystemFCBV]
rinstId_tm [in Autosubst.SystemFCBV]
rinstId_ty [in Autosubst.SystemFCBV]
rinstInst_vl [in Autosubst.SystemFCBV]
rinstInst_tm [in Autosubst.SystemFCBV]
rinstInst_ty [in Autosubst.SystemFCBV]

S

scons_comp [in Autosubst.fintype]
scons_eta_id [in Autosubst.fintype]
scons_eta [in Autosubst.fintype]
soundness [in Autosubst.sem]
soundness_nil [in Autosubst.sem]

T

typing_subst [in Autosubst.sem]
typing_ren [in Autosubst.sem]

U

up_ren_ren [in Autosubst.fintype]

V

varLRen_vl [in Autosubst.SystemFCBV]
varLRen_ty [in Autosubst.SystemFCBV]
varL_vl [in Autosubst.SystemFCBV]
varL_ty [in Autosubst.SystemFCBV]
V_subst [in Autosubst.sem]
V_weak [in Autosubst.sem]
V_ren [in Autosubst.sem]

---

Axiom Index

P

pext [in Autosubst.axioms]

---

Projection Index

I

ids [in Autosubst.fintype]

R

ren1 [in Autosubst.fintype]
ren2 [in Autosubst.fintype]
ren3 [in Autosubst.fintype]
ren4 [in Autosubst.fintype]
ren5 [in Autosubst.fintype]

S

subst1 [in Autosubst.fintype]
subst2 [in Autosubst.fintype]
subst3 [in Autosubst.fintype]
subst4 [in Autosubst.fintype]
subst5 [in Autosubst.fintype]

---

Inductive Index

E

eval [in Autosubst.sem]

R

Ren1 [in Autosubst.fintype]
Ren2 [in Autosubst.fintype]
Ren3 [in Autosubst.fintype]
Ren4 [in Autosubst.fintype]
Ren5 [in Autosubst.fintype]

S

Subst1 [in Autosubst.fintype]
Subst2 [in Autosubst.fintype]
Subst3 [in Autosubst.fintype]
Subst4 [in Autosubst.fintype]
Subst5 [in Autosubst.fintype]

T

tm [in Autosubst.SystemFCBV]
tm_ty [in Autosubst.sem]
ty [in Autosubst.SystemFCBV]

V

Var [in Autosubst.fintype]
vl [in Autosubst.SystemFCBV]
vl_ty [in Autosubst.sem]

---

Instance Index

R

Ren_vl [in Autosubst.SystemFCBV]
Ren_tm [in Autosubst.SystemFCBV]
Ren_ty [in Autosubst.SystemFCBV]

S

Subst_vl [in Autosubst.SystemFCBV]
Subst_tm [in Autosubst.SystemFCBV]
Subst_ty [in Autosubst.SystemFCBV]

V

VarInstance_vl [in Autosubst.SystemFCBV]
VarInstance_ty [in Autosubst.SystemFCBV]

---

Abbreviation Index

E

E [in Autosubst.sem]

---

Record Index

R

Ren1 [in Autosubst.fintype]
Ren2 [in Autosubst.fintype]
Ren3 [in Autosubst.fintype]
Ren4 [in Autosubst.fintype]
Ren5 [in Autosubst.fintype]

S

Subst1 [in Autosubst.fintype]
Subst2 [in Autosubst.fintype]
Subst3 [in Autosubst.fintype]
Subst4 [in Autosubst.fintype]
Subst5 [in Autosubst.fintype]

V

Var [in Autosubst.fintype]

---

Definition Index

A

ap [in Autosubst.fintype]
apc [in Autosubst.fintype]

C

comp [in Autosubst.fintype]
compRenRen_vl [in Autosubst.SystemFCBV]
compRenRen_tm [in Autosubst.SystemFCBV]
compRenRen_ty [in Autosubst.SystemFCBV]
compRenSubst_vl [in Autosubst.SystemFCBV]
compRenSubst_tm [in Autosubst.SystemFCBV]
compRenSubst_ty [in Autosubst.SystemFCBV]
compSubstRen__vl [in Autosubst.SystemFCBV]
compSubstRen__tm [in Autosubst.SystemFCBV]
compSubstRen__ty [in Autosubst.SystemFCBV]
compSubstSubst_vl [in Autosubst.SystemFCBV]
compSubstSubst_tm [in Autosubst.SystemFCBV]
compSubstSubst_ty [in Autosubst.SystemFCBV]
ctx [in Autosubst.sem]

E

empty [in Autosubst.sem]
extRen_vl [in Autosubst.SystemFCBV]
extRen_tm [in Autosubst.SystemFCBV]
extRen_ty [in Autosubst.SystemFCBV]
ext_vl [in Autosubst.SystemFCBV]
ext_tm [in Autosubst.SystemFCBV]
ext_ty [in Autosubst.SystemFCBV]

F

fin [in Autosubst.fintype]
funcomp [in Autosubst.fintype]

H

has_ty_ind [in Autosubst.sem]

I

id [in Autosubst.fintype]
idren [in Autosubst.fintype]
idSubst_vl [in Autosubst.SystemFCBV]
idSubst_tm [in Autosubst.SystemFCBV]
idSubst_ty [in Autosubst.SystemFCBV]

L

L [in Autosubst.sem]
lt_ctx [in Autosubst.sem]
lt_ctx_ren [in Autosubst.sem]

N

nilA [in Autosubst.sem]
null [in Autosubst.fintype]

R

ren [in Autosubst.fintype]
ren_vl [in Autosubst.SystemFCBV]
ren_tm [in Autosubst.SystemFCBV]
ren_ty [in Autosubst.SystemFCBV]
rinstInst_up_vl_vl [in Autosubst.SystemFCBV]
rinstInst_up_vl_ty [in Autosubst.SystemFCBV]
rinstInst_up_ty_vl [in Autosubst.SystemFCBV]
rinstInst_up_ty_ty [in Autosubst.SystemFCBV]
rinst_inst_vl [in Autosubst.SystemFCBV]
rinst_inst_tm [in Autosubst.SystemFCBV]
rinst_inst_ty [in Autosubst.SystemFCBV]

S

scons [in Autosubst.fintype]
shift [in Autosubst.fintype]
subst_vl [in Autosubst.SystemFCBV]
subst_tm [in Autosubst.SystemFCBV]
subst_ty [in Autosubst.SystemFCBV]

T

tm_ty_ind [in Autosubst.sem]

U

upExtRen_vl_vl [in Autosubst.SystemFCBV]
upExtRen_vl_ty [in Autosubst.SystemFCBV]
upExtRen_ty_vl [in Autosubst.SystemFCBV]
upExtRen_ty_ty [in Autosubst.SystemFCBV]
upExt_vl_vl [in Autosubst.SystemFCBV]
upExt_vl_ty [in Autosubst.SystemFCBV]
upExt_ty_vl [in Autosubst.SystemFCBV]
upExt_ty_ty [in Autosubst.SystemFCBV]
upId_vl_vl [in Autosubst.SystemFCBV]
upId_vl_ty [in Autosubst.SystemFCBV]
upId_ty_vl [in Autosubst.SystemFCBV]
upId_ty_ty [in Autosubst.SystemFCBV]
upRen_vl_vl [in Autosubst.SystemFCBV]
upRen_vl_ty [in Autosubst.SystemFCBV]
upRen_ty_vl [in Autosubst.SystemFCBV]
upRen_ty_ty [in Autosubst.SystemFCBV]
up_ren [in Autosubst.fintype]
up_subst_subst_vl_vl [in Autosubst.SystemFCBV]
up_subst_subst_vl_ty [in Autosubst.SystemFCBV]
up_subst_subst_ty_vl [in Autosubst.SystemFCBV]
up_subst_ren_vl_vl [in Autosubst.SystemFCBV]
up_subst_ren_vl_ty [in Autosubst.SystemFCBV]
up_subst_ren_ty_vl [in Autosubst.SystemFCBV]
up_ren_subst_vl_vl [in Autosubst.SystemFCBV]
up_ren_subst_vl_ty [in Autosubst.SystemFCBV]
up_ren_subst_ty_vl [in Autosubst.SystemFCBV]
up_vl_vl [in Autosubst.SystemFCBV]
up_vl_ty [in Autosubst.SystemFCBV]
up_ty_vl [in Autosubst.SystemFCBV]
up_subst_subst_ty_ty [in Autosubst.SystemFCBV]
up_subst_ren_ty_ty [in Autosubst.SystemFCBV]
up_ren_subst_ty_ty [in Autosubst.SystemFCBV]
up_ty_ty [in Autosubst.SystemFCBV]

V

V [in Autosubst.sem]
var_zero [in Autosubst.fintype]
VG [in Autosubst.sem]
vl_ty_ind [in Autosubst.sem]

---

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

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

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

(1 entry)

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

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

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

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

(1 entry)

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

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

(17 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(8 entries)

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

(1 entry)

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

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

(90 entries)

---

This page has been generated by coqdoc