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 (185 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 (23 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 (4 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 (44 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)
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 (31 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 (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 (18 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 (4 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)
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 (37 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 (11 entries)

Global Index

A

algeq [inductive, in LOG.logrel]
algeqNeu [inductive, in LOG.logrel]
algeqNeu_ind_2 [definition, in LOG.logrel]
algeq_trans [lemma, in LOG.logrel]
algeq_sym [lemma, in LOG.logrel]
algeq_backward_closure [lemma, in LOG.logrel]
algEq_monotone [lemma, in LOG.logrel]
algeq_mut_ind [definition, in LOG.logrel]
algeq_ind_2 [definition, in LOG.logrel]
alg_app [constructor, in LOG.logrel]
alg_var [constructor, in LOG.logrel]
alg_arr [constructor, in LOG.logrel]
alg_base [constructor, in LOG.logrel]
ap [definition, in LOG.unscoped]
apc [definition, in LOG.unscoped]
app [constructor, in LOG.Syntax]
arr [constructor, in LOG.Syntax]
axioms [library]


B

Base [constructor, in LOG.Syntax]
beta [constructor, in LOG.logrel]


C

compComp_tm [lemma, in LOG.Syntax]
compComp'_tm [lemma, in LOG.Syntax]
completeness [lemma, in LOG.logrel]
compRenRen_tm [definition, in LOG.Syntax]
compRenSubst_tm [definition, in LOG.Syntax]
compRen_tm [lemma, in LOG.Syntax]
compRen'_tm [lemma, in LOG.Syntax]
compSubstRen__tm [definition, in LOG.Syntax]
compSubstSubst_tm [definition, in LOG.Syntax]
confluence [lemma, in LOG.logrel]
congr_lam [lemma, in LOG.Syntax]
congr_app [lemma, in LOG.Syntax]
congr_arr [lemma, in LOG.Syntax]
congr_Base [lemma, in LOG.Syntax]
cont_ext_id [lemma, in LOG.logrel]
cont_ext_cons [lemma, in LOG.logrel]
cont_ext_shift [lemma, in LOG.logrel]
cont_ext [definition, in LOG.logrel]
ctx [definition, in LOG.logrel]


D

DecApp [constructor, in LOG.logrel]
DecBeta [constructor, in LOG.logrel]
DecExt [constructor, in LOG.logrel]
DecLam [constructor, in LOG.logrel]
decleq [inductive, in LOG.logrel]
DecSym [constructor, in LOG.logrel]
DecTrans [constructor, in LOG.logrel]
DecVar [constructor, in LOG.logrel]


E

extRen_tm [definition, in LOG.Syntax]
ext_tm [definition, in LOG.Syntax]


F

fin [abbreviation, in LOG.unscoped]
funcomp [definition, in LOG.unscoped]
fundamental [lemma, in LOG.logrel]


G

get [definition, in LOG.logrel]


I

id [definition, in LOG.unscoped]
ids [projection, in LOG.unscoped]
ids [constructor, in LOG.unscoped]
idsRen [instance, in LOG.unscoped]
idSubst_tm [definition, in LOG.Syntax]
instId_tm [lemma, in LOG.Syntax]


L

lam [constructor, in LOG.Syntax]
logeq [definition, in LOG.logrel]
logeq_rel [definition, in LOG.logrel]
logeq_trans [lemma, in LOG.logrel]
logeq_sym [lemma, in LOG.logrel]
logeq_backward_closure [lemma, in LOG.logrel]
logEq_monotone [lemma, in LOG.logrel]
logrel [library]


M

main [lemma, in LOG.logrel]
mstep [inductive, in LOG.logrel]
mstepR [constructor, in LOG.logrel]
mstepS [constructor, in LOG.logrel]
mstep_ren [lemma, in LOG.logrel]
mstep_trans [lemma, in LOG.logrel]
mstep_appL [lemma, in LOG.logrel]


N

neutral_mstep [lemma, in LOG.logrel]
neutral_step [lemma, in LOG.logrel]
None [definition, in LOG.unscoped]


P

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


R

renComp_tm [lemma, in LOG.Syntax]
renComp'_tm [lemma, in LOG.Syntax]
renRen_tm [lemma, in LOG.Syntax]
renRen'_tm [lemma, in LOG.Syntax]
Ren_tm [instance, in LOG.Syntax]
ren_tm [definition, in LOG.Syntax]
ren1 [projection, in LOG.unscoped]
Ren1 [record, in LOG.unscoped]
ren1 [constructor, in LOG.unscoped]
Ren1 [inductive, in LOG.unscoped]
ren2 [projection, in LOG.unscoped]
Ren2 [record, in LOG.unscoped]
ren2 [constructor, in LOG.unscoped]
Ren2 [inductive, in LOG.unscoped]
ren3 [projection, in LOG.unscoped]
Ren3 [record, in LOG.unscoped]
ren3 [constructor, in LOG.unscoped]
Ren3 [inductive, in LOG.unscoped]
ren4 [projection, in LOG.unscoped]
Ren4 [record, in LOG.unscoped]
ren4 [constructor, in LOG.unscoped]
Ren4 [inductive, in LOG.unscoped]
ren5 [projection, in LOG.unscoped]
Ren5 [record, in LOG.unscoped]
ren5 [constructor, in LOG.unscoped]
Ren5 [inductive, in LOG.unscoped]
rinstId_tm [lemma, in LOG.Syntax]
rinstInst_tm [lemma, in LOG.Syntax]
rinstInst_up_tm_tm [definition, in LOG.Syntax]
rinst_inst_tm [definition, in LOG.Syntax]


S

scons [definition, in LOG.unscoped]
scons_comp [lemma, in LOG.unscoped]
scons_eta_id [lemma, in LOG.unscoped]
scons_eta [lemma, in LOG.unscoped]
shift [definition, in LOG.unscoped]
Some [definition, in LOG.unscoped]
step [inductive, in LOG.logrel]
stepapp [constructor, in LOG.logrel]
step_ren [lemma, in LOG.logrel]
Subst_tm [instance, in LOG.Syntax]
subst_tm [definition, in LOG.Syntax]
subst1 [projection, in LOG.unscoped]
Subst1 [record, in LOG.unscoped]
subst1 [constructor, in LOG.unscoped]
Subst1 [inductive, in LOG.unscoped]
subst2 [projection, in LOG.unscoped]
Subst2 [record, in LOG.unscoped]
subst2 [constructor, in LOG.unscoped]
Subst2 [inductive, in LOG.unscoped]
subst3 [projection, in LOG.unscoped]
Subst3 [record, in LOG.unscoped]
subst3 [constructor, in LOG.unscoped]
Subst3 [inductive, in LOG.unscoped]
subst4 [projection, in LOG.unscoped]
Subst4 [record, in LOG.unscoped]
subst4 [constructor, in LOG.unscoped]
Subst4 [inductive, in LOG.unscoped]
subst5 [projection, in LOG.unscoped]
Subst5 [record, in LOG.unscoped]
subst5 [constructor, in LOG.unscoped]
Subst5 [inductive, in LOG.unscoped]
Syntax [library]


T

tm [inductive, in LOG.Syntax]
ty [inductive, in LOG.Syntax]
type_unique [lemma, in LOG.logrel]


U

unscoped [library]
upExtRen_tm_tm [definition, in LOG.Syntax]
upExt_tm_tm [definition, in LOG.Syntax]
upId_tm_tm [definition, in LOG.Syntax]
upRen_tm_tm [definition, in LOG.Syntax]
up_ren_ren [lemma, in LOG.unscoped]
up_ren [definition, in LOG.unscoped]
up_subst_subst_tm_tm [definition, in LOG.Syntax]
up_subst_ren_tm_tm [definition, in LOG.Syntax]
up_ren_subst_tm_tm [definition, in LOG.Syntax]
up_tm_tm [definition, in LOG.Syntax]


V

Var [record, in LOG.unscoped]
Var [inductive, in LOG.unscoped]
VarInstance_tm [instance, in LOG.Syntax]
varLRen_tm [lemma, in LOG.Syntax]
varL_tm [lemma, in LOG.Syntax]
var_zero [definition, in LOG.unscoped]
var_tm [constructor, in LOG.Syntax]


other

[ _ ] (fscope) [notation, in LOG.Syntax]
⟨ _ ; _ ⟩ (fscope) [notation, in LOG.unscoped]
⟨ _ ⟩ (fscope) [notation, in LOG.unscoped]
⟨ _ ⟩ (fscope) [notation, in LOG.Syntax]
_ .. (subst_scope) [notation, in LOG.unscoped]
_ , _ (subst_scope) [notation, in LOG.unscoped]
_ >> _ (subst_scope) [notation, in LOG.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in LOG.unscoped]
_ [ _ ] (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in LOG.Syntax]
_ [ _ ] (subst_scope) [notation, in LOG.Syntax]
⇑__tm (subst_scope) [notation, in LOG.Syntax]
var (subst_scope) [notation, in LOG.Syntax]
_ __tm (subst_scope) [notation, in LOG.Syntax]
_ __tm (subst_scope) [notation, in LOG.Syntax]
_ .: _ [notation, in LOG.unscoped]
_ `_ _ [notation, in LOG.logrel]
[notation, in LOG.unscoped]



Notation Index

other

[ _ ] (fscope) [in LOG.Syntax]
⟨ _ ; _ ⟩ (fscope) [in LOG.unscoped]
⟨ _ ⟩ (fscope) [in LOG.unscoped]
⟨ _ ⟩ (fscope) [in LOG.Syntax]
_ .. (subst_scope) [in LOG.unscoped]
_ , _ (subst_scope) [in LOG.unscoped]
_ >> _ (subst_scope) [in LOG.unscoped]
_ [ _ ; _ ] (subst_scope) [in LOG.unscoped]
_ [ _ ] (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in LOG.Syntax]
_ [ _ ] (subst_scope) [in LOG.Syntax]
⇑__tm (subst_scope) [in LOG.Syntax]
var (subst_scope) [in LOG.Syntax]
_ __tm (subst_scope) [in LOG.Syntax]
_ __tm (subst_scope) [in LOG.Syntax]
_ .: _ [in LOG.unscoped]
_ `_ _ [in LOG.logrel]
[in LOG.unscoped]



Library Index

A

axioms


L

logrel


S

Syntax


U

unscoped



Lemma Index

A

algeq_trans [in LOG.logrel]
algeq_sym [in LOG.logrel]
algeq_backward_closure [in LOG.logrel]
algEq_monotone [in LOG.logrel]


C

compComp_tm [in LOG.Syntax]
compComp'_tm [in LOG.Syntax]
completeness [in LOG.logrel]
compRen_tm [in LOG.Syntax]
compRen'_tm [in LOG.Syntax]
confluence [in LOG.logrel]
congr_lam [in LOG.Syntax]
congr_app [in LOG.Syntax]
congr_arr [in LOG.Syntax]
congr_Base [in LOG.Syntax]
cont_ext_id [in LOG.logrel]
cont_ext_cons [in LOG.logrel]
cont_ext_shift [in LOG.logrel]


F

fundamental [in LOG.logrel]


I

instId_tm [in LOG.Syntax]


L

logeq_trans [in LOG.logrel]
logeq_sym [in LOG.logrel]
logeq_backward_closure [in LOG.logrel]
logEq_monotone [in LOG.logrel]


M

main [in LOG.logrel]
mstep_ren [in LOG.logrel]
mstep_trans [in LOG.logrel]
mstep_appL [in LOG.logrel]


N

neutral_mstep [in LOG.logrel]
neutral_step [in LOG.logrel]


P

pi [in LOG.axioms]


R

renComp_tm [in LOG.Syntax]
renComp'_tm [in LOG.Syntax]
renRen_tm [in LOG.Syntax]
renRen'_tm [in LOG.Syntax]
rinstId_tm [in LOG.Syntax]
rinstInst_tm [in LOG.Syntax]


S

scons_comp [in LOG.unscoped]
scons_eta_id [in LOG.unscoped]
scons_eta [in LOG.unscoped]
step_ren [in LOG.logrel]


T

type_unique [in LOG.logrel]


U

up_ren_ren [in LOG.unscoped]


V

varLRen_tm [in LOG.Syntax]
varL_tm [in LOG.Syntax]



Axiom Index

P

pext [in LOG.axioms]



Constructor Index

A

alg_app [in LOG.logrel]
alg_var [in LOG.logrel]
alg_arr [in LOG.logrel]
alg_base [in LOG.logrel]
app [in LOG.Syntax]
arr [in LOG.Syntax]


B

Base [in LOG.Syntax]
beta [in LOG.logrel]


D

DecApp [in LOG.logrel]
DecBeta [in LOG.logrel]
DecExt [in LOG.logrel]
DecLam [in LOG.logrel]
DecSym [in LOG.logrel]
DecTrans [in LOG.logrel]
DecVar [in LOG.logrel]


I

ids [in LOG.unscoped]


L

lam [in LOG.Syntax]


M

mstepR [in LOG.logrel]
mstepS [in LOG.logrel]


R

ren1 [in LOG.unscoped]
ren2 [in LOG.unscoped]
ren3 [in LOG.unscoped]
ren4 [in LOG.unscoped]
ren5 [in LOG.unscoped]


S

stepapp [in LOG.logrel]
subst1 [in LOG.unscoped]
subst2 [in LOG.unscoped]
subst3 [in LOG.unscoped]
subst4 [in LOG.unscoped]
subst5 [in LOG.unscoped]


V

var_tm [in LOG.Syntax]



Projection Index

I

ids [in LOG.unscoped]


R

ren1 [in LOG.unscoped]
ren2 [in LOG.unscoped]
ren3 [in LOG.unscoped]
ren4 [in LOG.unscoped]
ren5 [in LOG.unscoped]


S

subst1 [in LOG.unscoped]
subst2 [in LOG.unscoped]
subst3 [in LOG.unscoped]
subst4 [in LOG.unscoped]
subst5 [in LOG.unscoped]



Inductive Index

A

algeq [in LOG.logrel]
algeqNeu [in LOG.logrel]


D

decleq [in LOG.logrel]


M

mstep [in LOG.logrel]


R

Ren1 [in LOG.unscoped]
Ren2 [in LOG.unscoped]
Ren3 [in LOG.unscoped]
Ren4 [in LOG.unscoped]
Ren5 [in LOG.unscoped]


S

step [in LOG.logrel]
Subst1 [in LOG.unscoped]
Subst2 [in LOG.unscoped]
Subst3 [in LOG.unscoped]
Subst4 [in LOG.unscoped]
Subst5 [in LOG.unscoped]


T

tm [in LOG.Syntax]
ty [in LOG.Syntax]


V

Var [in LOG.unscoped]



Instance Index

I

idsRen [in LOG.unscoped]


R

Ren_tm [in LOG.Syntax]


S

Subst_tm [in LOG.Syntax]


V

VarInstance_tm [in LOG.Syntax]



Abbreviation Index

F

fin [in LOG.unscoped]



Definition Index

A

algeqNeu_ind_2 [in LOG.logrel]
algeq_mut_ind [in LOG.logrel]
algeq_ind_2 [in LOG.logrel]
ap [in LOG.unscoped]
apc [in LOG.unscoped]


C

compRenRen_tm [in LOG.Syntax]
compRenSubst_tm [in LOG.Syntax]
compSubstRen__tm [in LOG.Syntax]
compSubstSubst_tm [in LOG.Syntax]
cont_ext [in LOG.logrel]
ctx [in LOG.logrel]


E

extRen_tm [in LOG.Syntax]
ext_tm [in LOG.Syntax]


F

funcomp [in LOG.unscoped]


G

get [in LOG.logrel]


I

id [in LOG.unscoped]
idSubst_tm [in LOG.Syntax]


L

logeq [in LOG.logrel]
logeq_rel [in LOG.logrel]


N

None [in LOG.unscoped]


R

ren_tm [in LOG.Syntax]
rinstInst_up_tm_tm [in LOG.Syntax]
rinst_inst_tm [in LOG.Syntax]


S

scons [in LOG.unscoped]
shift [in LOG.unscoped]
Some [in LOG.unscoped]
subst_tm [in LOG.Syntax]


U

upExtRen_tm_tm [in LOG.Syntax]
upExt_tm_tm [in LOG.Syntax]
upId_tm_tm [in LOG.Syntax]
upRen_tm_tm [in LOG.Syntax]
up_ren [in LOG.unscoped]
up_subst_subst_tm_tm [in LOG.Syntax]
up_subst_ren_tm_tm [in LOG.Syntax]
up_ren_subst_tm_tm [in LOG.Syntax]
up_tm_tm [in LOG.Syntax]


V

var_zero [in LOG.unscoped]



Record Index

R

Ren1 [in LOG.unscoped]
Ren2 [in LOG.unscoped]
Ren3 [in LOG.unscoped]
Ren4 [in LOG.unscoped]
Ren5 [in LOG.unscoped]


S

Subst1 [in LOG.unscoped]
Subst2 [in LOG.unscoped]
Subst3 [in LOG.unscoped]
Subst4 [in LOG.unscoped]
Subst5 [in LOG.unscoped]


V

Var [in LOG.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 (185 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 (23 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 (4 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 (44 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)
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 (31 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 (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 (18 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 (4 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)
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 (37 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 (11 entries)