Global Index

K

O

Q

W

X

Y

Z

_

(662 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(38 entries)

Module Index

A

B

C

D

E

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(10 entries)

Variable Index

A

B

C

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)

Library Index

B

C

E

F

G

H

I

J

K

M

N

O

Q

R

T

U

W

X

Y

Z

_

other

(9 entries)

Lemma Index

K

L

N

O

Q

R

W

X

Y

Z

_

other

(334 entries)

Constructor Index

B

E

F

G

J

K

M

N

O

Q

R

U

W

X

Y

Z

_

other

(97 entries)

Axiom Index

A

B

C

D

E

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Inductive Index

B

E

F

G

J

K

L

M

N

O

Q

R

U

W

X

Y

Z

_

other

(33 entries)

Projection Index

A

G

H

I

J

K

L

M

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Section Index

A

B

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Instance Index

A

B

C

E

G

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(42 entries)

Abbreviation Index

A

B

C

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Definition Index

A

K

L

M

N

O

Q

U

W

X

Y

Z

_

other

(69 entries)

Record Index

A

B

E

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Global Index

A

All [constructor, in RSC.sysf]
App [constructor, in RSC.sysf]
App [constructor, in RSC.stlc]
ARS [library]
atn [inductive, in RSC.lib]
atnd [inductive, in RSC.lib]
AtndS [constructor, in RSC.lib]
atnd_func [lemma, in RSC.lib]
atnd_getD [lemma, in RSC.lib]
Atnd0 [constructor, in RSC.lib]
AtnS [constructor, in RSC.lib]
atn_mmap [lemma, in RSC.lib]
atn_get [lemma, in RSC.lib]
Atn0 [constructor, in RSC.lib]

B

bfr [definition, in RSC.lib]
bfr_ushift [lemma, in RSC.lib]
bfr_shift [lemma, in RSC.lib]
bfr_up [lemma, in RSC.lib]
bind [projection, in RSC.lib]

C

cm_tmrel_beta_tm [lemma, in RSC.stlcCorrespondence]
cm_tmrel_rs_ext [lemma, in RSC.stlcCorrespondence]
cm_tmrel [definition, in RSC.stlcCorrespondence]
cm_tyrel_rs [lemma, in RSC.stlcCorrespondence]
cm_tyrel [definition, in RSC.stlcCorrespondence]
cm_tmrel_beta_tm [lemma, in RSC.sysfCorrespondence]
cm_tmrel_ext_rs [lemma, in RSC.sysfCorrespondence]
cm_tmrel_rs_ext [lemma, in RSC.sysfCorrespondence]
cm_tmrel [definition, in RSC.sysfCorrespondence]
cm_tyrel_beta [lemma, in RSC.sysfCorrespondence]
cm_tyrel_ext [lemma, in RSC.sysfCorrespondence]
cm_tyrel_rs [lemma, in RSC.sysfCorrespondence]
cm_tyrel [definition, in RSC.sysfCorrespondence]
Coincidence [section, in RSC.lib]
CoincidenceHSubst [section, in RSC.lib]
comb [definition, in RSC.lib]
comb_comp [lemma, in RSC.lib]
comb_cons [lemma, in RSC.lib]
composite [definition, in RSC.ARS]
confluent [definition, in RSC.ARS]
confluent_CR [lemma, in RSC.ARS]
confluent_semiconfluent [lemma, in RSC.ARS]
ContextRenamings [section, in RSC.lib]
conv [inductive, in RSC.ARS]
convCR [constructor, in RSC.ARS]
convCRi [constructor, in RSC.ARS]
convE [lemma, in RSC.ARS]
convR [constructor, in RSC.ARS]
convRC [lemma, in RSC.ARS]
convRCi [lemma, in RSC.ARS]
convS [lemma, in RSC.ARS]
convT [lemma, in RSC.ARS]
convTi [lemma, in RSC.ARS]
conv_proper2 [lemma, in RSC.ARS]
conv_proper [lemma, in RSC.ARS]
conv1 [lemma, in RSC.ARS]
conv1i [lemma, in RSC.ARS]
Countable [record, in RSC.Decidable]
countableProp [projection, in RSC.Decidable]
cr [definition, in RSC.lib]
CR [definition, in RSC.ARS]
cr_shift [lemma, in RSC.lib]
cr_up [lemma, in RSC.lib]
CR_confluent [lemma, in RSC.ARS]
CtxBoolFun [section, in RSC.lib]
ctxrel_AB [lemma, in RSC.stlcCorrespondence]
ctxrel_BA [lemma, in RSC.stlcCorrespondence]
ctxrel_AB [lemma, in RSC.sysfCorrespondence]
ctxrel_BA [lemma, in RSC.sysfCorrespondence]

D

Dec [record, in RSC.Decidable]
Dec [inductive, in RSC.Decidable]
dec [abbreviation, in RSC.Decidable]
Decidable [library]
decidable_neg [instance, in RSC.Decidable]
decide [projection, in RSC.Decidable]
decide [constructor, in RSC.Decidable]
decide_refl [lemma, in RSC.lib]
decide_eq_tm [instance, in RSC.sysf]
decide_eq_ty [instance, in RSC.sysf]
decide_eq_tm [instance, in RSC.stlc]
decide_eq_ty [instance, in RSC.stlc]
decide_eq_fin_domain [lemma, in RSC.Decidable]
Dec_eq_fin_domain [instance, in RSC.Decidable]
Dec_fin_quant [instance, in RSC.Decidable]
Dec_fin_quant_T [instance, in RSC.Decidable]
Dec_impl [instance, in RSC.Decidable]
Dec_or [instance, in RSC.Decidable]
Dec_and [instance, in RSC.Decidable]
Dec_lt_nat [instance, in RSC.Decidable]
Dec_le_nat [instance, in RSC.Decidable]
Dec_eq_option [instance, in RSC.Decidable]
Dec_eq_nat [instance, in RSC.Decidable]
Definitions [section, in RSC.ARS]
Definitions.R [variable, in RSC.ARS]
Definitions.X [variable, in RSC.ARS]
demo1 [lemma, in RSC.stlcCorrespondence]
demo1 [lemma, in RSC.sysfCorrespondence]
demo2 [lemma, in RSC.stlcCorrespondence]
demo2 [lemma, in RSC.sysfCorrespondence]
diamond [definition, in RSC.ARS]
diamond_star_confluent [lemma, in RSC.ARS]
diamond_confluent [lemma, in RSC.ARS]
diamond_semiconfluent [lemma, in RSC.ARS]

E

enum [projection, in RSC.Decidable]
equivalence [definition, in RSC.ARS]
eq_diamond [lemma, in RSC.ARS]
eq_dec [abbreviation, in RSC.Decidable]

F

Finite [record, in RSC.Decidable]
finiteProp [projection, in RSC.Decidable]
fmap [projection, in RSC.lib]
FPTS [module, in RSC.pts]
FPTS_sig.R_func [axiom, in RSC.pts]
FPTS_sig.A_func [axiom, in RSC.pts]
FPTS_sig [module, in RSC.pts]
FPTS.hastype_strengthen [lemma, in RSC.pts]
FPTS.hastype_pcr_str [lemma, in RSC.pts]
FPTS.hastype_pren [lemma, in RSC.pts]
FPTS.hastype_pren' [lemma, in RSC.pts]
FPTS.hastype_unique [lemma, in RSC.pts]
FPTS.hastype_unique_pren [lemma, in RSC.pts]
FPTS.hastype_pcr_up [lemma, in RSC.pts]
FPTS.hastype_pcr_id [lemma, in RSC.pts]
FPTS.hastype_pcr [definition, in RSC.pts]
Functor [record, in RSC.lib]
Functor_Monad [instance, in RSC.lib]

G

get [definition, in RSC.lib]
getD [definition, in RSC.lib]
getD_cons [lemma, in RSC.lib]
getD_get [lemma, in RSC.lib]
getD_atnd [lemma, in RSC.lib]
get_mmap_None [lemma, in RSC.lib]
get_mmap [lemma, in RSC.lib]
get_atn [lemma, in RSC.lib]

H

hastype [inductive, in RSC.sysf]
hastype [inductive, in RSC.stlc]
hastype_tylam [constructor, in RSC.sysf]
hastype_tyapp [constructor, in RSC.sysf]
hastype_lam [constructor, in RSC.sysf]
hastype_app [constructor, in RSC.sysf]
hastype_var [constructor, in RSC.sysf]
hastype_beta [lemma, in RSC.stlc]
hastype_cm_beta [lemma, in RSC.stlc]
hastype_subst [lemma, in RSC.stlc]
hastype_cm_up [lemma, in RSC.stlc]
hastype_cm_id [lemma, in RSC.stlc]
hastype_cm [definition, in RSC.stlc]
hastype_weaken [lemma, in RSC.stlc]
hastype_cr_shift [lemma, in RSC.stlc]
hastype_ren [lemma, in RSC.stlc]
hastype_cr_up [lemma, in RSC.stlc]
hastype_cr_id [lemma, in RSC.stlc]
hastype_cr [definition, in RSC.stlc]
hastype_lam [constructor, in RSC.stlc]
hastype_app [constructor, in RSC.stlc]
hastype_var [constructor, in RSC.stlc]
HSubstLemmas_termF [instance, in RSC.sysf]
HSubst_termF [instance, in RSC.sysf]

I

idR [definition, in RSC.vrel]
Ids_tm [instance, in RSC.sysf]
Ids_ty [instance, in RSC.sysf]
Ids_tm [instance, in RSC.stlc]
Ids_ty [instance, in RSC.stlc]
Imp [constructor, in RSC.sysf]
Imp [constructor, in RSC.stlc]
intern [definition, in RSC.sysf]
intern_correct [lemma, in RSC.sysf]
intern_ty [definition, in RSC.sysf]
intern_ctx_correct [lemma, in RSC.stlc]
intern_ctx [definition, in RSC.stlc]
inverse [definition, in RSC.ARS]
istype [inductive, in RSC.sysf]
istype [inductive, in RSC.stlc]
istype_beta [lemma, in RSC.sysf]
istype_cm_beta [lemma, in RSC.sysf]
istype_subst [lemma, in RSC.sysf]
istype_cm_up [lemma, in RSC.sysf]
istype_cm [definition, in RSC.sysf]
istype_weaken [lemma, in RSC.sysf]
istype_cr_shift [lemma, in RSC.sysf]
istype_ren [lemma, in RSC.sysf]
istype_cr_up [lemma, in RSC.sysf]
istype_cr [definition, in RSC.sysf]
istype_all [constructor, in RSC.sysf]
istype_imp [constructor, in RSC.sysf]
istype_tyvar [constructor, in RSC.sysf]
istype_weaken [lemma, in RSC.stlc]
istype_cr_shift [lemma, in RSC.stlc]
istype_ren [lemma, in RSC.stlc]
istype_cr [definition, in RSC.stlc]
istype_imp [constructor, in RSC.stlc]
istype_tyvar [constructor, in RSC.stlc]

J

joinable [definition, in RSC.ARS]
joinableS [lemma, in RSC.ARS]
join_conv [lemma, in RSC.ARS]

L

Lam [constructor, in RSC.sysf]
Lam [constructor, in RSC.stlc]
lib [library]
Lookup [section, in RSC.lib]

M

mmap_get_None [lemma, in RSC.lib]
mmap_get [lemma, in RSC.lib]
mmap_atn [lemma, in RSC.lib]
Monad [record, in RSC.lib]

N

numElems [projection, in RSC.Decidable]

P

Pred [definition, in RSC.ARS]
propagation [lemma, in RSC.stlc]
PTS [module, in RSC.pts]
pts [library]
PTS_sig.R [axiom, in RSC.pts]
PTS_sig.A [axiom, in RSC.pts]
PTS_sig.decide_eq_srt [axiom, in RSC.pts]
PTS_sig.S [axiom, in RSC.pts]
PTS_sig [module, in RSC.pts]
PTS.all [definition, in RSC.pts]
PTS.allCtx [definition, in RSC.pts]
PTS.allCtx_NZ [lemma, in RSC.pts]
PTS.allCtx_up [lemma, in RSC.pts]
PTS.all_NZ_shift [lemma, in RSC.pts]
PTS.all_TrueP [lemma, in RSC.pts]
PTS.all_full [lemma, in RSC.pts]
PTS.all_beta [lemma, in RSC.pts]
PTS.all_monotone [lemma, in RSC.pts]
PTS.all_ids [lemma, in RSC.pts]
PTS.all_subst [lemma, in RSC.pts]
PTS.all_up [lemma, in RSC.pts]
PTS.all_ren [lemma, in RSC.pts]
PTS.all_srt [lemma, in RSC.pts]
PTS.App [constructor, in RSC.pts]
PTS.app_eq_ren_inv [lemma, in RSC.pts]
PTS.bc_subst_beta [lemma, in RSC.pts]
PTS.bc_prod [lemma, in RSC.pts]
PTS.bc_srt [lemma, in RSC.pts]
PTS.bc_srt_prod [lemma, in RSC.pts]
PTS.bc_srt_normal_l [lemma, in RSC.pts]
PTS.bc_srt_normal_r [lemma, in RSC.pts]
PTS.bc_srt_l [lemma, in RSC.pts]
PTS.bc_srt_r [lemma, in RSC.pts]
PTS.bc_ssubst [lemma, in RSC.pts]
PTS.cpstepR [lemma, in RSC.pts]
PTS.cpstep_ext [lemma, in RSC.pts]
PTS.decide_eq_termL [instance, in RSC.pts]
PTS.hastype [inductive, in RSC.pts]
PTS.hastype_srt_srt [lemma, in RSC.pts]
PTS.hastype_tr [lemma, in RSC.pts]
PTS.hastype_sr [lemma, in RSC.pts]
PTS.hastype_beta_ty [lemma, in RSC.pts]
PTS.hastype_prod_inv [lemma, in RSC.pts]
PTS.hastype_beta [lemma, in RSC.pts]
PTS.hastype_cm_beta [lemma, in RSC.pts]
PTS.hastype_subst [lemma, in RSC.pts]
PTS.hastype_cm_up [lemma, in RSC.pts]
PTS.hastype_cm [definition, in RSC.pts]
PTS.hastype_weaken_srt [lemma, in RSC.pts]
PTS.hastype_weaken [lemma, in RSC.pts]
PTS.hastype_cr_shift [lemma, in RSC.pts]
PTS.hastype_ren [lemma, in RSC.pts]
PTS.hastype_cr_up [lemma, in RSC.pts]
PTS.hastype_cr [definition, in RSC.pts]
PTS.hastype_conv [constructor, in RSC.pts]
PTS.hastype_lam [constructor, in RSC.pts]
PTS.hastype_app [constructor, in RSC.pts]
PTS.hastype_prod [constructor, in RSC.pts]
PTS.hastype_var [constructor, in RSC.pts]
PTS.hastype_ax [constructor, in RSC.pts]
PTS.Ids_tm [instance, in RSC.pts]
PTS.Lam [constructor, in RSC.pts]
PTS.mpstep [definition, in RSC.pts]
PTS.neutral [inductive, in RSC.pts]
PTS.neutral_notLam [lemma, in RSC.pts]
PTS.neutral_step [lemma, in RSC.pts]
PTS.neutral_app [constructor, in RSC.pts]
PTS.neutral_prod [constructor, in RSC.pts]
PTS.neutral_srt [constructor, in RSC.pts]
PTS.neutral_var [constructor, in RSC.pts]
PTS.normal [inductive, in RSC.pts]
PTS.normal_bc [lemma, in RSC.pts]
PTS.normal_bc_red [lemma, in RSC.pts]
PTS.normal_red [lemma, in RSC.pts]
PTS.normal_step [lemma, in RSC.pts]
PTS.normal_var [lemma, in RSC.pts]
PTS.normal_srt [lemma, in RSC.pts]
PTS.normal_lam [constructor, in RSC.pts]
PTS.normal_nt [constructor, in RSC.pts]
PTS.no_ax_empty [lemma, in RSC.pts]
PTS.nrm_ntr_step [lemma, in RSC.pts]
PTS.nrm_ntr_ind [definition, in RSC.pts]
PTS.nrm_ntr [definition, in RSC.pts]
PTS.ntr_nrm [definition, in RSC.pts]
PTS.NZ [definition, in RSC.pts]
PTS.Prod [constructor, in RSC.pts]
PTS.prod_eq_ren_inv [lemma, in RSC.pts]
PTS.propagation [lemma, in RSC.pts]
PTS.pstep [inductive, in RSC.pts]
PTS.pstepS_sr [lemma, in RSC.pts]
PTS.pstep_sr [lemma, in RSC.pts]
PTS.pstep_triangle [lemma, in RSC.pts]
PTS.pstep_bc [lemma, in RSC.pts]
PTS.pstep_red [lemma, in RSC.pts]
PTS.pstep_subst_beta [lemma, in RSC.pts]
PTS.pstep_subst [lemma, in RSC.pts]
PTS.pstep_ssubst [lemma, in RSC.pts]
PTS.pstep_refl [lemma, in RSC.pts]
PTS.pstep_beta [constructor, in RSC.pts]
PTS.pstep_srt [constructor, in RSC.pts]
PTS.pstep_lam [constructor, in RSC.pts]
PTS.pstep_app [constructor, in RSC.pts]
PTS.pstep_prod [constructor, in RSC.pts]
PTS.pstep_var [constructor, in RSC.pts]
PTS.red_all [lemma, in RSC.pts]
PTS.red_subst_beta [lemma, in RSC.pts]
PTS.red_ssubst [lemma, in RSC.pts]
PTS.red_prod [lemma, in RSC.pts]
PTS.red_srt_eq [lemma, in RSC.pts]
PTS.Rename_tm [instance, in RSC.pts]
PTS.spstep_beta [lemma, in RSC.pts]
PTS.spstep_up [lemma, in RSC.pts]
PTS.Srt [constructor, in RSC.pts]
PTS.srt_normal [lemma, in RSC.pts]
PTS.srt_no_type [lemma, in RSC.pts]
PTS.srt_eq_ren_inv [lemma, in RSC.pts]
PTS.step [inductive, in RSC.pts]
PTS.step_all [lemma, in RSC.pts]
PTS.step_CR [lemma, in RSC.pts]
PTS.step_confluent [lemma, in RSC.pts]
PTS.step_pstep_star [lemma, in RSC.pts]
PTS.step_pstep [lemma, in RSC.pts]
PTS.step_ssubst [lemma, in RSC.pts]
PTS.step_beta [constructor, in RSC.pts]
PTS.step_lamB [constructor, in RSC.pts]
PTS.step_lamD [constructor, in RSC.pts]
PTS.step_appR [constructor, in RSC.pts]
PTS.step_appL [constructor, in RSC.pts]
PTS.step_prodB [constructor, in RSC.pts]
PTS.step_prodD [constructor, in RSC.pts]
PTS.strip_app [lemma, in RSC.pts]
PTS.strip_lam [lemma, in RSC.pts]
PTS.strip_prod [lemma, in RSC.pts]
PTS.strip_var [lemma, in RSC.pts]
PTS.strip_srt [lemma, in RSC.pts]
PTS.SubstLemmas_tm [instance, in RSC.pts]
PTS.Subst_tm [instance, in RSC.pts]
PTS.tm [inductive, in RSC.pts]
PTS.TrueP [definition, in RSC.pts]
PTS.valid [inductive, in RSC.pts]
PTS.valid_atnd_var [lemma, in RSC.pts]
PTS.valid_atnd [lemma, in RSC.pts]
PTS.valid_ext [constructor, in RSC.pts]
PTS.valid_nil [constructor, in RSC.pts]
PTS.Var [constructor, in RSC.pts]
PTS.var_eq_ren_inv [lemma, in RSC.pts]
_ [▷] _ [notation, in RSC.pts]
_ ▷▷ _ [notation, in RSC.pts]
_ ▷* _ [notation, in RSC.pts]
_ ▷ _ [notation, in RSC.pts]
_ ≡ _ [notation, in RSC.pts]
_ ≻* _ [notation, in RSC.pts]
_ ≻ _ [notation, in RSC.pts]

R

reflexive [definition, in RSC.ARS]
Rel [definition, in RSC.ARS]
rel_inj [definition, in RSC.lib]
rel_func [definition, in RSC.lib]
Rename_tm [instance, in RSC.sysf]
Rename_ty [instance, in RSC.sysf]
Rename_tm [instance, in RSC.stlc]
Rename_ty [instance, in RSC.stlc]
repr [projection, in RSC.Decidable]
ret [projection, in RSC.lib]

S

SA [module, in RSC.stlcCorrespondence]
SA [module, in RSC.sysfCorrespondence]
SA.F_spec.R_func [lemma, in RSC.sysfCorrespondence]
SA.F_spec.A_func [lemma, in RSC.sysfCorrespondence]
SA.F_spec.decide_eq_srt [instance, in RSC.sysfCorrespondence]
SA.F_spec.R [definition, in RSC.sysfCorrespondence]
SA.F_spec.A [definition, in RSC.sysfCorrespondence]
SA.F_spec.S [definition, in RSC.sysfCorrespondence]
SA.F_spec.rel2 [constructor, in RSC.sysfCorrespondence]
SA.F_spec.rl1 [constructor, in RSC.sysfCorrespondence]
SA.F_spec.rl [inductive, in RSC.sysfCorrespondence]
SA.F_spec.ax_base [constructor, in RSC.sysfCorrespondence]
SA.F_spec.ax [inductive, in RSC.sysfCorrespondence]
SA.F_spec.Typ [constructor, in RSC.sysfCorrespondence]
SA.F_spec.Prp [constructor, in RSC.sysfCorrespondence]
SA.F_spec.level [inductive, in RSC.sysfCorrespondence]
SA.F_spec [module, in RSC.sysfCorrespondence]
SA.hastype_type_strengthen [lemma, in RSC.stlcCorrespondence]
SA.hastype_normal_ty [lemma, in RSC.stlcCorrespondence]
SA.hastype_type_strengthen [lemma, in RSC.sysfCorrespondence]
SA.hastype_normal_ty [lemma, in RSC.sysfCorrespondence]
SA.intern [definition, in RSC.sysfCorrespondence]
SA.intern_correct [lemma, in RSC.sysfCorrespondence]
SA.prps [definition, in RSC.stlcCorrespondence]
SA.prps_atnd [lemma, in RSC.stlcCorrespondence]
SA.prps_valid [lemma, in RSC.stlcCorrespondence]
SA.prp_prp_contra [lemma, in RSC.stlcCorrespondence]
SA.prp_prp_contra [lemma, in RSC.sysfCorrespondence]
SA.STLC_spec.R_func [lemma, in RSC.stlcCorrespondence]
SA.STLC_spec.A_func [lemma, in RSC.stlcCorrespondence]
SA.STLC_spec.decide_eq_srt [instance, in RSC.stlcCorrespondence]
SA.STLC_spec.R [definition, in RSC.stlcCorrespondence]
SA.STLC_spec.A [definition, in RSC.stlcCorrespondence]
SA.STLC_spec.S [definition, in RSC.stlcCorrespondence]
SA.STLC_spec.rl1 [constructor, in RSC.stlcCorrespondence]
SA.STLC_spec.rl [inductive, in RSC.stlcCorrespondence]
SA.STLC_spec.ax_base [constructor, in RSC.stlcCorrespondence]
SA.STLC_spec.ax [inductive, in RSC.stlcCorrespondence]
SA.STLC_spec.Typ [constructor, in RSC.stlcCorrespondence]
SA.STLC_spec.Prp [constructor, in RSC.stlcCorrespondence]
SA.STLC_spec.level [inductive, in RSC.stlcCorrespondence]
SA.STLC_spec [module, in RSC.stlcCorrespondence]
SA.term_induction [lemma, in RSC.stlcCorrespondence]
SA.term_induction [lemma, in RSC.sysfCorrespondence]
SA.types_normal [lemma, in RSC.stlcCorrespondence]
SA.types_normal [lemma, in RSC.sysfCorrespondence]
SA.type_induction [lemma, in RSC.stlcCorrespondence]
SA.type_induction [lemma, in RSC.sysfCorrespondence]
SA.typ_degeneracy [lemma, in RSC.stlcCorrespondence]
SA.typ_no_type [lemma, in RSC.stlcCorrespondence]
SA.typ_degeneracy [lemma, in RSC.sysfCorrespondence]
SA.typ_no_type [lemma, in RSC.sysfCorrespondence]
∗ [notation, in RSC.stlcCorrespondence]
∗ [notation, in RSC.sysfCorrespondence]
⬜ [notation, in RSC.stlcCorrespondence]
⬜ [notation, in RSC.sysfCorrespondence]
SB [module, in RSC.stlcCorrespondence]
SB [module, in RSC.sysfCorrespondence]
semiconfluent [definition, in RSC.ARS]
semiconfluent_CR [lemma, in RSC.ARS]
semiconfluent_confluent [lemma, in RSC.ARS]
star [inductive, in RSC.ARS]
starL [lemma, in RSC.ARS]
starR [constructor, in RSC.ARS]
starRS [constructor, in RSC.ARS]
starSR [lemma, in RSC.ARS]
starT [lemma, in RSC.ARS]
star_proper2_inv [lemma, in RSC.ARS]
star_proper2 [lemma, in RSC.ARS]
star_proper [lemma, in RSC.ARS]
star_interpolate [lemma, in RSC.ARS]
star_idem [lemma, in RSC.ARS]
star_monotone [lemma, in RSC.ARS]
star_conv [lemma, in RSC.ARS]
star1 [lemma, in RSC.ARS]
stlc [library]
stlcCorrespondence [library]
SubstHSubstComp_typeF_termF [instance, in RSC.sysf]
SubstLemmas_tm [instance, in RSC.sysf]
SubstLemmas_ty [instance, in RSC.sysf]
SubstLemmas_tm [instance, in RSC.stlc]
SubstLemmas_ty [instance, in RSC.stlc]
subst_coinc_hcomp [lemma, in RSC.lib]
subst_coinc_hd_f [lemma, in RSC.lib]
subst_coinc_up [lemma, in RSC.lib]
subst_coinc_id [lemma, in RSC.lib]
subst_coinc [definition, in RSC.lib]
Subst_tm [instance, in RSC.sysf]
Subst_ty [instance, in RSC.sysf]
Subst_tm [instance, in RSC.stlc]
Subst_ty [instance, in RSC.stlc]
subT [lemma, in RSC.ARS]
sum2bool [definition, in RSC.lib]
symmetric [definition, in RSC.ARS]
sysf [library]
sysfCorrespondence [library]

T

tm [inductive, in RSC.sysf]
tm [inductive, in RSC.stlc]
tmrel [inductive, in RSC.stlcCorrespondence]
tmrel [inductive, in RSC.sysfCorrespondence]
tmrel_AB_total_preserving [lemma, in RSC.stlcCorrespondence]
tmrel_BA_total_preserving [lemma, in RSC.stlcCorrespondence]
tmrel_beta_tm [lemma, in RSC.stlcCorrespondence]
tmrel_subst_tm [lemma, in RSC.stlcCorrespondence]
tmrel_rs_ext [lemma, in RSC.stlcCorrespondence]
tmrel_weaken_tm [lemma, in RSC.stlcCorrespondence]
tmrel_mono_tm [lemma, in RSC.stlcCorrespondence]
tmrel_ren [lemma, in RSC.stlcCorrespondence]
tmrel_AB_tot_pres [lemma, in RSC.stlcCorrespondence]
tmrel_BA_tot_pres [lemma, in RSC.stlcCorrespondence]
tmrel_inj [lemma, in RSC.stlcCorrespondence]
tmrel_func [lemma, in RSC.stlcCorrespondence]
tmrel_lam [constructor, in RSC.stlcCorrespondence]
tmrel_app [constructor, in RSC.stlcCorrespondence]
tmrel_var [constructor, in RSC.stlcCorrespondence]
tmrel_AB_total_preserving [lemma, in RSC.sysfCorrespondence]
tmrel_BA_total_preserving [lemma, in RSC.sysfCorrespondence]
tmrel_beta_tm [lemma, in RSC.sysfCorrespondence]
tmrel_subst [lemma, in RSC.sysfCorrespondence]
tmrel_ext_rs [lemma, in RSC.sysfCorrespondence]
tmrel_rs_ext [lemma, in RSC.sysfCorrespondence]
tmrel_weaken_tm [lemma, in RSC.sysfCorrespondence]
tmrel_weaken_ty [lemma, in RSC.sysfCorrespondence]
tmrel_mono [lemma, in RSC.sysfCorrespondence]
tmrel_ren [lemma, in RSC.sysfCorrespondence]
tmrel_AB_tot_pres [lemma, in RSC.sysfCorrespondence]
tmrel_BA_tot_pres [lemma, in RSC.sysfCorrespondence]
tmrel_inj [lemma, in RSC.sysfCorrespondence]
tmrel_func [lemma, in RSC.sysfCorrespondence]
tmrel_tylam [constructor, in RSC.sysfCorrespondence]
tmrel_tyapp [constructor, in RSC.sysfCorrespondence]
tmrel_lam [constructor, in RSC.sysfCorrespondence]
tmrel_app [constructor, in RSC.sysfCorrespondence]
tmrel_var [constructor, in RSC.sysfCorrespondence]
transitive [definition, in RSC.ARS]
triangle [definition, in RSC.ARS]
triangle_confluent [lemma, in RSC.ARS]
triangle_diamond [lemma, in RSC.ARS]
TTML_confluence [lemma, in RSC.ARS]
ty [inductive, in RSC.sysf]
ty [inductive, in RSC.stlc]
TyApp [constructor, in RSC.sysf]
TyLam [constructor, in RSC.sysf]
tyrel [inductive, in RSC.stlcCorrespondence]
tyrel [inductive, in RSC.sysfCorrespondence]
tyrel_AB_total_preserving [lemma, in RSC.stlcCorrespondence]
tyrel_BA_total_preserving [lemma, in RSC.stlcCorrespondence]
tyrel_vrs_inv [lemma, in RSC.stlcCorrespondence]
tyrel_unmap [lemma, in RSC.stlcCorrespondence]
tyrel_subst [lemma, in RSC.stlcCorrespondence]
tyrel_ext [lemma, in RSC.stlcCorrespondence]
tyrel_rs [lemma, in RSC.stlcCorrespondence]
tyrel_weaken [lemma, in RSC.stlcCorrespondence]
tyrel_mono [lemma, in RSC.stlcCorrespondence]
tyrel_ren [lemma, in RSC.stlcCorrespondence]
tyrel_AB_tot_pres [lemma, in RSC.stlcCorrespondence]
tyrel_BA_tot_pres [lemma, in RSC.stlcCorrespondence]
tyrel_inj [lemma, in RSC.stlcCorrespondence]
tyrel_func [lemma, in RSC.stlcCorrespondence]
tyrel_imp [constructor, in RSC.stlcCorrespondence]
tyrel_var [constructor, in RSC.stlcCorrespondence]
tyrel_AB_total_preserving [lemma, in RSC.sysfCorrespondence]
tyrel_BA_total_preserving [lemma, in RSC.sysfCorrespondence]
tyrel_tmrel_disjoint [lemma, in RSC.sysfCorrespondence]
tyrel_vrs_inv [lemma, in RSC.sysfCorrespondence]
tyrel_unmap [lemma, in RSC.sysfCorrespondence]
tyrel_beta [lemma, in RSC.sysfCorrespondence]
tyrel_subst [lemma, in RSC.sysfCorrespondence]
tyrel_ext [lemma, in RSC.sysfCorrespondence]
tyrel_rs [lemma, in RSC.sysfCorrespondence]
tyrel_weaken [lemma, in RSC.sysfCorrespondence]
tyrel_mono [lemma, in RSC.sysfCorrespondence]
tyrel_ren [lemma, in RSC.sysfCorrespondence]
tyrel_AB_tot_pres [lemma, in RSC.sysfCorrespondence]
tyrel_BA_tot_pres [lemma, in RSC.sysfCorrespondence]
tyrel_inj [lemma, in RSC.sysfCorrespondence]
tyrel_func [lemma, in RSC.sysfCorrespondence]
tyrel_all [constructor, in RSC.sysfCorrespondence]
tyrel_imp [constructor, in RSC.sysfCorrespondence]
tyrel_var [constructor, in RSC.sysfCorrespondence]
TyVar [constructor, in RSC.sysf]
TyVar [constructor, in RSC.stlc]

U

upren_comb [lemma, in RSC.lib]

V

valid [inductive, in RSC.sysf]
valid [inductive, in RSC.stlc]
valid_shift [lemma, in RSC.sysf]
valid_ren [lemma, in RSC.sysf]
valid_valid' [lemma, in RSC.sysf]
valid_N_nil [lemma, in RSC.sysf]
valid_ext_tm [constructor, in RSC.sysf]
valid_ext_ty [constructor, in RSC.sysf]
valid_empty [constructor, in RSC.sysf]
valid_shift [lemma, in RSC.stlc]
valid_ren [lemma, in RSC.stlc]
valid_ext [constructor, in RSC.stlc]
valid_nil [constructor, in RSC.stlc]
valid' [inductive, in RSC.sysf]
valid'_ext_tm [constructor, in RSC.sysf]
valid'_nil [constructor, in RSC.sysf]
Var [constructor, in RSC.sysf]
Var [constructor, in RSC.stlc]
vEXT [definition, in RSC.vrel]
vext_mono [lemma, in RSC.vrel]
vext_tail [lemma, in RSC.vrel]
vext_head [lemma, in RSC.vrel]
vext_inv [lemma, in RSC.vrel]
vrdS [lemma, in RSC.vrel]
vrd_ext_rs [lemma, in RSC.vrel]
vrd_rs_ext [lemma, in RSC.vrel]
vrd_nil [lemma, in RSC.vrel]
vrd_nil_r [lemma, in RSC.vrel]
vrd_nil_l [lemma, in RSC.vrel]
vrel [definition, in RSC.vrel]
vrel [library]
vrm [definition, in RSC.vrel]
vrm_ext [lemma, in RSC.vrel]
vrm_rs [lemma, in RSC.vrel]
vrm_mono [lemma, in RSC.vrel]
vrm_comb [lemma, in RSC.vrel]
vrs [lemma, in RSC.vrel]
vRS [definition, in RSC.vrel]
vrs_inv [lemma, in RSC.vrel]
vr_tmctx_AB_prps [lemma, in RSC.stlcCorrespondence]
vr_tmctx_AB_nil [lemma, in RSC.stlcCorrespondence]
vr_tmctx_AB_ext_rs [lemma, in RSC.stlcCorrespondence]
vr_tmctx_AB_rs_ext [lemma, in RSC.stlcCorrespondence]
vr_tmctx_AB [definition, in RSC.stlcCorrespondence]
vr_tmctx_BA_nil [lemma, in RSC.stlcCorrespondence]
vr_tmctx_BA_ext_rs [lemma, in RSC.stlcCorrespondence]
vr_tmctx_BA_rs_ext [lemma, in RSC.stlcCorrespondence]
vr_tmctx_BA [definition, in RSC.stlcCorrespondence]
vr_tyctx_AB_idR [lemma, in RSC.stlcCorrespondence]
vr_tyctx_AB_nil [lemma, in RSC.stlcCorrespondence]
vr_tyctx_AB_ext [lemma, in RSC.stlcCorrespondence]
vr_tyctx_AB_rs [lemma, in RSC.stlcCorrespondence]
vr_tyctx_AB [definition, in RSC.stlcCorrespondence]
vr_tyctx_BA_idR [lemma, in RSC.stlcCorrespondence]
vr_tyctx_BA_nil [lemma, in RSC.stlcCorrespondence]
vr_tyctx_BA_ext [lemma, in RSC.stlcCorrespondence]
vr_tyctx_BA_rs [lemma, in RSC.stlcCorrespondence]
vr_tyctx_BA [definition, in RSC.stlcCorrespondence]
vr_tmctx_AB_nil [lemma, in RSC.sysfCorrespondence]
vr_tmctx_AB_ext_rs [lemma, in RSC.sysfCorrespondence]
vr_tmctx_AB_rs_ext [lemma, in RSC.sysfCorrespondence]
vr_tmctx_AB [definition, in RSC.sysfCorrespondence]
vr_tmctx_BA_nil [lemma, in RSC.sysfCorrespondence]
vr_tmctx_BA_ext_rs [lemma, in RSC.sysfCorrespondence]
vr_tmctx_BA_rs_ext [lemma, in RSC.sysfCorrespondence]
vr_tmctx_BA [definition, in RSC.sysfCorrespondence]
vr_tyctx_AB_nil [lemma, in RSC.sysfCorrespondence]
vr_tyctx_AB_ext [lemma, in RSC.sysfCorrespondence]
vr_tyctx_AB_rs [lemma, in RSC.sysfCorrespondence]
vr_tyctx_AB [definition, in RSC.sysfCorrespondence]
vr_tyctx_BA_nil [lemma, in RSC.sysfCorrespondence]
vr_tyctx_BA_ext [lemma, in RSC.sysfCorrespondence]
vr_tyctx_BA_rs [lemma, in RSC.sysfCorrespondence]
vr_tyctx_BA [definition, in RSC.sysfCorrespondence]
vr_func_idR [lemma, in RSC.vrel]
vr_inj_idR [lemma, in RSC.vrel]
vr_inj_ext [lemma, in RSC.vrel]
vr_inj_rs [lemma, in RSC.vrel]
vr_inj_nil [lemma, in RSC.vrel]
vr_inj [definition, in RSC.vrel]
vr_func_ext [lemma, in RSC.vrel]
vr_func_rs [lemma, in RSC.vrel]
vr_func_nil [lemma, in RSC.vrel]
vr_func [definition, in RSC.vrel]
vr_mono [lemma, in RSC.vrel]
vr_unmap [lemma, in RSC.vrel]
vr_map [lemma, in RSC.vrel]

other

_ ⊑ _ (list_scope) [notation, in RSC.vrel]
_ <$> _ [notation, in RSC.lib]
_ |- _ ∼ _ [notation, in RSC.stlcCorrespondence]
_ |- _ ∼ _ [notation, in RSC.sysfCorrespondence]
_ ∥ _ [notation, in RSC.vrel]
_ |- _ ≃ _ [notation, in RSC.vrel]
_ === _ [notation, in RSC.ARS]
_ <<= _ [notation, in RSC.ARS]
do _ <- _ ; _ [notation, in RSC.lib]
GET _ <- _ ; _ [notation, in RSC.lib]
$$( _ ) [notation, in RSC.lib]
$? [notation, in RSC.lib]
(-1) [notation, in RSC.lib]
[ ⟨ _ , _ ⟩ ; _ ↤ _ ] [notation, in RSC.stlcCorrespondence]
[ ⟨ _ , _ ⟩ ; _ ↦ _ ] [notation, in RSC.stlcCorrespondence]
[ _ ; _ ↤ _ ] [notation, in RSC.stlcCorrespondence]
[ _ ; _ ↦ _ ] [notation, in RSC.stlcCorrespondence]
[ ⟨ _ , _ ⟩ ; _ ↤ _ ] [notation, in RSC.sysfCorrespondence]
[ ⟨ _ , _ ⟩ ; _ ↦ _ ] [notation, in RSC.sysfCorrespondence]
[ _ ; _ ↤ _ ] [notation, in RSC.sysfCorrespondence]
[ _ ; _ ↦ _ ] [notation, in RSC.sysfCorrespondence]
∗ [notation, in RSC.stlcCorrespondence]
∗ [notation, in RSC.sysfCorrespondence]
⟨ _ , _ ⟩ |- _ ≈ _ [notation, in RSC.stlcCorrespondence]
⟨ _ , _ ⟩ |- _ ≈ _ [notation, in RSC.sysfCorrespondence]
⬜ [notation, in RSC.stlcCorrespondence]
⬜ [notation, in RSC.sysfCorrespondence]

Notation Index

P

_ [▷] _ [in RSC.pts]
_ ▷▷ _ [in RSC.pts]
_ ▷* _ [in RSC.pts]
_ ▷ _ [in RSC.pts]
_ ≡ _ [in RSC.pts]
_ ≻* _ [in RSC.pts]
_ ≻ _ [in RSC.pts]

S

∗ [in RSC.stlcCorrespondence]
∗ [in RSC.sysfCorrespondence]
⬜ [in RSC.stlcCorrespondence]
⬜ [in RSC.sysfCorrespondence]

other

_ ⊑ _ (list_scope) [in RSC.vrel]
_ <$> _ [in RSC.lib]
_ |- _ ∼ _ [in RSC.stlcCorrespondence]
_ |- _ ∼ _ [in RSC.sysfCorrespondence]
_ ∥ _ [in RSC.vrel]
_ |- _ ≃ _ [in RSC.vrel]
_ === _ [in RSC.ARS]
_ <<= _ [in RSC.ARS]
do _ <- _ ; _ [in RSC.lib]
GET _ <- _ ; _ [in RSC.lib]
$$( _ ) [in RSC.lib]
$? [in RSC.lib]
(-1) [in RSC.lib]
[ ⟨ _ , _ ⟩ ; _ ↤ _ ] [in RSC.stlcCorrespondence]
[ ⟨ _ , _ ⟩ ; _ ↦ _ ] [in RSC.stlcCorrespondence]
[ _ ; _ ↤ _ ] [in RSC.stlcCorrespondence]
[ _ ; _ ↦ _ ] [in RSC.stlcCorrespondence]
[ ⟨ _ , _ ⟩ ; _ ↤ _ ] [in RSC.sysfCorrespondence]
[ ⟨ _ , _ ⟩ ; _ ↦ _ ] [in RSC.sysfCorrespondence]
[ _ ; _ ↤ _ ] [in RSC.sysfCorrespondence]
[ _ ; _ ↦ _ ] [in RSC.sysfCorrespondence]
∗ [in RSC.stlcCorrespondence]
∗ [in RSC.sysfCorrespondence]
⟨ _ , _ ⟩ |- _ ≈ _ [in RSC.stlcCorrespondence]
⟨ _ , _ ⟩ |- _ ≈ _ [in RSC.sysfCorrespondence]
⬜ [in RSC.stlcCorrespondence]
⬜ [in RSC.sysfCorrespondence]

Module Index

F

FPTS [in RSC.pts]
FPTS_sig [in RSC.pts]

P

PTS [in RSC.pts]
PTS_sig [in RSC.pts]

S

SA [in RSC.stlcCorrespondence]
SA [in RSC.sysfCorrespondence]
SA.F_spec [in RSC.sysfCorrespondence]
SA.STLC_spec [in RSC.stlcCorrespondence]
SB [in RSC.stlcCorrespondence]
SB [in RSC.sysfCorrespondence]

Variable Index

D

Definitions.R [in RSC.ARS]
Definitions.X [in RSC.ARS]

Library Index

A

ARS

D

L

lib

P

pts

S

stlc
stlcCorrespondence
sysf
sysfCorrespondence

V

vrel

Lemma Index

A

atnd_func [in RSC.lib]
atnd_getD [in RSC.lib]
atn_mmap [in RSC.lib]
atn_get [in RSC.lib]

B

bfr_ushift [in RSC.lib]
bfr_shift [in RSC.lib]
bfr_up [in RSC.lib]

C

cm_tmrel_beta_tm [in RSC.stlcCorrespondence]
cm_tmrel_rs_ext [in RSC.stlcCorrespondence]
cm_tyrel_rs [in RSC.stlcCorrespondence]
cm_tmrel_beta_tm [in RSC.sysfCorrespondence]
cm_tmrel_ext_rs [in RSC.sysfCorrespondence]
cm_tmrel_rs_ext [in RSC.sysfCorrespondence]
cm_tyrel_beta [in RSC.sysfCorrespondence]
cm_tyrel_ext [in RSC.sysfCorrespondence]
cm_tyrel_rs [in RSC.sysfCorrespondence]
comb_comp [in RSC.lib]
comb_cons [in RSC.lib]
confluent_CR [in RSC.ARS]
confluent_semiconfluent [in RSC.ARS]
convE [in RSC.ARS]
convRC [in RSC.ARS]
convRCi [in RSC.ARS]
convS [in RSC.ARS]
convT [in RSC.ARS]
convTi [in RSC.ARS]
conv_proper2 [in RSC.ARS]
conv_proper [in RSC.ARS]
conv1 [in RSC.ARS]
conv1i [in RSC.ARS]
cr_shift [in RSC.lib]
cr_up [in RSC.lib]
CR_confluent [in RSC.ARS]
ctxrel_AB [in RSC.stlcCorrespondence]
ctxrel_BA [in RSC.stlcCorrespondence]
ctxrel_AB [in RSC.sysfCorrespondence]
ctxrel_BA [in RSC.sysfCorrespondence]

D

decide_refl [in RSC.lib]
decide_eq_fin_domain [in RSC.Decidable]
demo1 [in RSC.stlcCorrespondence]
demo1 [in RSC.sysfCorrespondence]
demo2 [in RSC.stlcCorrespondence]
demo2 [in RSC.sysfCorrespondence]
diamond_star_confluent [in RSC.ARS]
diamond_confluent [in RSC.ARS]
diamond_semiconfluent [in RSC.ARS]

E

eq_diamond [in RSC.ARS]

F

FPTS.hastype_strengthen [in RSC.pts]
FPTS.hastype_pcr_str [in RSC.pts]
FPTS.hastype_pren [in RSC.pts]
FPTS.hastype_pren' [in RSC.pts]
FPTS.hastype_unique [in RSC.pts]
FPTS.hastype_unique_pren [in RSC.pts]
FPTS.hastype_pcr_up [in RSC.pts]
FPTS.hastype_pcr_id [in RSC.pts]

G

getD_cons [in RSC.lib]
getD_get [in RSC.lib]
getD_atnd [in RSC.lib]
get_mmap_None [in RSC.lib]
get_mmap [in RSC.lib]
get_atn [in RSC.lib]

H

hastype_beta [in RSC.stlc]
hastype_cm_beta [in RSC.stlc]
hastype_subst [in RSC.stlc]
hastype_cm_up [in RSC.stlc]
hastype_cm_id [in RSC.stlc]
hastype_weaken [in RSC.stlc]
hastype_cr_shift [in RSC.stlc]
hastype_ren [in RSC.stlc]
hastype_cr_up [in RSC.stlc]
hastype_cr_id [in RSC.stlc]

I

intern_correct [in RSC.sysf]
intern_ctx_correct [in RSC.stlc]
istype_beta [in RSC.sysf]
istype_cm_beta [in RSC.sysf]
istype_subst [in RSC.sysf]
istype_cm_up [in RSC.sysf]
istype_weaken [in RSC.sysf]
istype_cr_shift [in RSC.sysf]
istype_ren [in RSC.sysf]
istype_cr_up [in RSC.sysf]
istype_weaken [in RSC.stlc]
istype_cr_shift [in RSC.stlc]
istype_ren [in RSC.stlc]

J

joinableS [in RSC.ARS]
join_conv [in RSC.ARS]

M

mmap_get_None [in RSC.lib]
mmap_get [in RSC.lib]
mmap_atn [in RSC.lib]

P

propagation [in RSC.stlc]
PTS.allCtx_NZ [in RSC.pts]
PTS.allCtx_up [in RSC.pts]
PTS.all_NZ_shift [in RSC.pts]
PTS.all_TrueP [in RSC.pts]
PTS.all_full [in RSC.pts]
PTS.all_beta [in RSC.pts]
PTS.all_monotone [in RSC.pts]
PTS.all_ids [in RSC.pts]
PTS.all_subst [in RSC.pts]
PTS.all_up [in RSC.pts]
PTS.all_ren [in RSC.pts]
PTS.all_srt [in RSC.pts]
PTS.app_eq_ren_inv [in RSC.pts]
PTS.bc_subst_beta [in RSC.pts]
PTS.bc_prod [in RSC.pts]
PTS.bc_srt [in RSC.pts]
PTS.bc_srt_prod [in RSC.pts]
PTS.bc_srt_normal_l [in RSC.pts]
PTS.bc_srt_normal_r [in RSC.pts]
PTS.bc_srt_l [in RSC.pts]
PTS.bc_srt_r [in RSC.pts]
PTS.bc_ssubst [in RSC.pts]
PTS.cpstepR [in RSC.pts]
PTS.cpstep_ext [in RSC.pts]
PTS.hastype_srt_srt [in RSC.pts]
PTS.hastype_tr [in RSC.pts]
PTS.hastype_sr [in RSC.pts]
PTS.hastype_beta_ty [in RSC.pts]
PTS.hastype_prod_inv [in RSC.pts]
PTS.hastype_beta [in RSC.pts]
PTS.hastype_cm_beta [in RSC.pts]
PTS.hastype_subst [in RSC.pts]
PTS.hastype_cm_up [in RSC.pts]
PTS.hastype_weaken_srt [in RSC.pts]
PTS.hastype_weaken [in RSC.pts]
PTS.hastype_cr_shift [in RSC.pts]
PTS.hastype_ren [in RSC.pts]
PTS.hastype_cr_up [in RSC.pts]
PTS.neutral_notLam [in RSC.pts]
PTS.neutral_step [in RSC.pts]
PTS.normal_bc [in RSC.pts]
PTS.normal_bc_red [in RSC.pts]
PTS.normal_red [in RSC.pts]
PTS.normal_step [in RSC.pts]
PTS.normal_var [in RSC.pts]
PTS.normal_srt [in RSC.pts]
PTS.no_ax_empty [in RSC.pts]
PTS.nrm_ntr_step [in RSC.pts]
PTS.prod_eq_ren_inv [in RSC.pts]
PTS.propagation [in RSC.pts]
PTS.pstepS_sr [in RSC.pts]
PTS.pstep_sr [in RSC.pts]
PTS.pstep_triangle [in RSC.pts]
PTS.pstep_bc [in RSC.pts]
PTS.pstep_red [in RSC.pts]
PTS.pstep_subst_beta [in RSC.pts]
PTS.pstep_subst [in RSC.pts]
PTS.pstep_ssubst [in RSC.pts]
PTS.pstep_refl [in RSC.pts]
PTS.red_all [in RSC.pts]
PTS.red_subst_beta [in RSC.pts]
PTS.red_ssubst [in RSC.pts]
PTS.red_prod [in RSC.pts]
PTS.red_srt_eq [in RSC.pts]
PTS.spstep_beta [in RSC.pts]
PTS.spstep_up [in RSC.pts]
PTS.srt_normal [in RSC.pts]
PTS.srt_no_type [in RSC.pts]
PTS.srt_eq_ren_inv [in RSC.pts]
PTS.step_all [in RSC.pts]
PTS.step_CR [in RSC.pts]
PTS.step_confluent [in RSC.pts]
PTS.step_pstep_star [in RSC.pts]
PTS.step_pstep [in RSC.pts]
PTS.step_ssubst [in RSC.pts]
PTS.strip_app [in RSC.pts]
PTS.strip_lam [in RSC.pts]
PTS.strip_prod [in RSC.pts]
PTS.strip_var [in RSC.pts]
PTS.strip_srt [in RSC.pts]
PTS.valid_atnd_var [in RSC.pts]
PTS.valid_atnd [in RSC.pts]
PTS.var_eq_ren_inv [in RSC.pts]

S

SA.F_spec.R_func [in RSC.sysfCorrespondence]
SA.F_spec.A_func [in RSC.sysfCorrespondence]
SA.hastype_type_strengthen [in RSC.stlcCorrespondence]
SA.hastype_normal_ty [in RSC.stlcCorrespondence]
SA.hastype_type_strengthen [in RSC.sysfCorrespondence]
SA.hastype_normal_ty [in RSC.sysfCorrespondence]
SA.intern_correct [in RSC.sysfCorrespondence]
SA.prps_atnd [in RSC.stlcCorrespondence]
SA.prps_valid [in RSC.stlcCorrespondence]
SA.prp_prp_contra [in RSC.stlcCorrespondence]
SA.prp_prp_contra [in RSC.sysfCorrespondence]
SA.STLC_spec.R_func [in RSC.stlcCorrespondence]
SA.STLC_spec.A_func [in RSC.stlcCorrespondence]
SA.term_induction [in RSC.stlcCorrespondence]
SA.term_induction [in RSC.sysfCorrespondence]
SA.types_normal [in RSC.stlcCorrespondence]
SA.types_normal [in RSC.sysfCorrespondence]
SA.type_induction [in RSC.stlcCorrespondence]
SA.type_induction [in RSC.sysfCorrespondence]
SA.typ_degeneracy [in RSC.stlcCorrespondence]
SA.typ_no_type [in RSC.stlcCorrespondence]
SA.typ_degeneracy [in RSC.sysfCorrespondence]
SA.typ_no_type [in RSC.sysfCorrespondence]
semiconfluent_CR [in RSC.ARS]
semiconfluent_confluent [in RSC.ARS]
starL [in RSC.ARS]
starSR [in RSC.ARS]
starT [in RSC.ARS]
star_proper2_inv [in RSC.ARS]
star_proper2 [in RSC.ARS]
star_proper [in RSC.ARS]
star_interpolate [in RSC.ARS]
star_idem [in RSC.ARS]
star_monotone [in RSC.ARS]
star_conv [in RSC.ARS]
star1 [in RSC.ARS]
subst_coinc_hcomp [in RSC.lib]
subst_coinc_hd_f [in RSC.lib]
subst_coinc_up [in RSC.lib]
subst_coinc_id [in RSC.lib]
subT [in RSC.ARS]

T

tmrel_AB_total_preserving [in RSC.stlcCorrespondence]
tmrel_BA_total_preserving [in RSC.stlcCorrespondence]
tmrel_beta_tm [in RSC.stlcCorrespondence]
tmrel_subst_tm [in RSC.stlcCorrespondence]
tmrel_rs_ext [in RSC.stlcCorrespondence]
tmrel_weaken_tm [in RSC.stlcCorrespondence]
tmrel_mono_tm [in RSC.stlcCorrespondence]
tmrel_ren [in RSC.stlcCorrespondence]
tmrel_AB_tot_pres [in RSC.stlcCorrespondence]
tmrel_BA_tot_pres [in RSC.stlcCorrespondence]
tmrel_inj [in RSC.stlcCorrespondence]
tmrel_func [in RSC.stlcCorrespondence]
tmrel_AB_total_preserving [in RSC.sysfCorrespondence]
tmrel_BA_total_preserving [in RSC.sysfCorrespondence]
tmrel_beta_tm [in RSC.sysfCorrespondence]
tmrel_subst [in RSC.sysfCorrespondence]
tmrel_ext_rs [in RSC.sysfCorrespondence]
tmrel_rs_ext [in RSC.sysfCorrespondence]
tmrel_weaken_tm [in RSC.sysfCorrespondence]
tmrel_weaken_ty [in RSC.sysfCorrespondence]
tmrel_mono [in RSC.sysfCorrespondence]
tmrel_ren [in RSC.sysfCorrespondence]
tmrel_AB_tot_pres [in RSC.sysfCorrespondence]
tmrel_BA_tot_pres [in RSC.sysfCorrespondence]
tmrel_inj [in RSC.sysfCorrespondence]
tmrel_func [in RSC.sysfCorrespondence]
triangle_confluent [in RSC.ARS]
triangle_diamond [in RSC.ARS]
TTML_confluence [in RSC.ARS]
tyrel_AB_total_preserving [in RSC.stlcCorrespondence]
tyrel_BA_total_preserving [in RSC.stlcCorrespondence]
tyrel_vrs_inv [in RSC.stlcCorrespondence]
tyrel_unmap [in RSC.stlcCorrespondence]
tyrel_subst [in RSC.stlcCorrespondence]
tyrel_ext [in RSC.stlcCorrespondence]
tyrel_rs [in RSC.stlcCorrespondence]
tyrel_weaken [in RSC.stlcCorrespondence]
tyrel_mono [in RSC.stlcCorrespondence]
tyrel_ren [in RSC.stlcCorrespondence]
tyrel_AB_tot_pres [in RSC.stlcCorrespondence]
tyrel_BA_tot_pres [in RSC.stlcCorrespondence]
tyrel_inj [in RSC.stlcCorrespondence]
tyrel_func [in RSC.stlcCorrespondence]
tyrel_AB_total_preserving [in RSC.sysfCorrespondence]
tyrel_BA_total_preserving [in RSC.sysfCorrespondence]
tyrel_tmrel_disjoint [in RSC.sysfCorrespondence]
tyrel_vrs_inv [in RSC.sysfCorrespondence]
tyrel_unmap [in RSC.sysfCorrespondence]
tyrel_beta [in RSC.sysfCorrespondence]
tyrel_subst [in RSC.sysfCorrespondence]
tyrel_ext [in RSC.sysfCorrespondence]
tyrel_rs [in RSC.sysfCorrespondence]
tyrel_weaken [in RSC.sysfCorrespondence]
tyrel_mono [in RSC.sysfCorrespondence]
tyrel_ren [in RSC.sysfCorrespondence]
tyrel_AB_tot_pres [in RSC.sysfCorrespondence]
tyrel_BA_tot_pres [in RSC.sysfCorrespondence]
tyrel_inj [in RSC.sysfCorrespondence]
tyrel_func [in RSC.sysfCorrespondence]

U

upren_comb [in RSC.lib]

V

valid_shift [in RSC.sysf]
valid_ren [in RSC.sysf]
valid_valid' [in RSC.sysf]
valid_N_nil [in RSC.sysf]
valid_shift [in RSC.stlc]
valid_ren [in RSC.stlc]
vext_mono [in RSC.vrel]
vext_tail [in RSC.vrel]
vext_head [in RSC.vrel]
vext_inv [in RSC.vrel]
vrdS [in RSC.vrel]
vrd_ext_rs [in RSC.vrel]
vrd_rs_ext [in RSC.vrel]
vrd_nil [in RSC.vrel]
vrd_nil_r [in RSC.vrel]
vrd_nil_l [in RSC.vrel]
vrm_ext [in RSC.vrel]
vrm_rs [in RSC.vrel]
vrm_mono [in RSC.vrel]
vrm_comb [in RSC.vrel]
vrs [in RSC.vrel]
vrs_inv [in RSC.vrel]
vr_tmctx_AB_prps [in RSC.stlcCorrespondence]
vr_tmctx_AB_nil [in RSC.stlcCorrespondence]
vr_tmctx_AB_ext_rs [in RSC.stlcCorrespondence]
vr_tmctx_AB_rs_ext [in RSC.stlcCorrespondence]
vr_tmctx_BA_nil [in RSC.stlcCorrespondence]
vr_tmctx_BA_ext_rs [in RSC.stlcCorrespondence]
vr_tmctx_BA_rs_ext [in RSC.stlcCorrespondence]
vr_tyctx_AB_idR [in RSC.stlcCorrespondence]
vr_tyctx_AB_nil [in RSC.stlcCorrespondence]
vr_tyctx_AB_ext [in RSC.stlcCorrespondence]
vr_tyctx_AB_rs [in RSC.stlcCorrespondence]
vr_tyctx_BA_idR [in RSC.stlcCorrespondence]
vr_tyctx_BA_nil [in RSC.stlcCorrespondence]
vr_tyctx_BA_ext [in RSC.stlcCorrespondence]
vr_tyctx_BA_rs [in RSC.stlcCorrespondence]
vr_tmctx_AB_nil [in RSC.sysfCorrespondence]
vr_tmctx_AB_ext_rs [in RSC.sysfCorrespondence]
vr_tmctx_AB_rs_ext [in RSC.sysfCorrespondence]
vr_tmctx_BA_nil [in RSC.sysfCorrespondence]
vr_tmctx_BA_ext_rs [in RSC.sysfCorrespondence]
vr_tmctx_BA_rs_ext [in RSC.sysfCorrespondence]
vr_tyctx_AB_nil [in RSC.sysfCorrespondence]
vr_tyctx_AB_ext [in RSC.sysfCorrespondence]
vr_tyctx_AB_rs [in RSC.sysfCorrespondence]
vr_tyctx_BA_nil [in RSC.sysfCorrespondence]
vr_tyctx_BA_ext [in RSC.sysfCorrespondence]
vr_tyctx_BA_rs [in RSC.sysfCorrespondence]
vr_func_idR [in RSC.vrel]
vr_inj_idR [in RSC.vrel]
vr_inj_ext [in RSC.vrel]
vr_inj_rs [in RSC.vrel]
vr_inj_nil [in RSC.vrel]
vr_func_ext [in RSC.vrel]
vr_func_rs [in RSC.vrel]
vr_func_nil [in RSC.vrel]
vr_mono [in RSC.vrel]
vr_unmap [in RSC.vrel]
vr_map [in RSC.vrel]

Constructor Index

A

All [in RSC.sysf]
App [in RSC.sysf]
App [in RSC.stlc]
AtndS [in RSC.lib]
Atnd0 [in RSC.lib]
AtnS [in RSC.lib]
Atn0 [in RSC.lib]

C

convCR [in RSC.ARS]
convCRi [in RSC.ARS]
convR [in RSC.ARS]

D

decide [in RSC.Decidable]

H

hastype_tylam [in RSC.sysf]
hastype_tyapp [in RSC.sysf]
hastype_lam [in RSC.sysf]
hastype_app [in RSC.sysf]
hastype_var [in RSC.sysf]
hastype_lam [in RSC.stlc]
hastype_app [in RSC.stlc]
hastype_var [in RSC.stlc]

I

Imp [in RSC.sysf]
Imp [in RSC.stlc]
istype_all [in RSC.sysf]
istype_imp [in RSC.sysf]
istype_tyvar [in RSC.sysf]
istype_imp [in RSC.stlc]
istype_tyvar [in RSC.stlc]

L

Lam [in RSC.sysf]
Lam [in RSC.stlc]

P

PTS.App [in RSC.pts]
PTS.hastype_conv [in RSC.pts]
PTS.hastype_lam [in RSC.pts]
PTS.hastype_app [in RSC.pts]
PTS.hastype_prod [in RSC.pts]
PTS.hastype_var [in RSC.pts]
PTS.hastype_ax [in RSC.pts]
PTS.Lam [in RSC.pts]
PTS.neutral_app [in RSC.pts]
PTS.neutral_prod [in RSC.pts]
PTS.neutral_srt [in RSC.pts]
PTS.neutral_var [in RSC.pts]
PTS.normal_lam [in RSC.pts]
PTS.normal_nt [in RSC.pts]
PTS.Prod [in RSC.pts]
PTS.pstep_beta [in RSC.pts]
PTS.pstep_srt [in RSC.pts]
PTS.pstep_lam [in RSC.pts]
PTS.pstep_app [in RSC.pts]
PTS.pstep_prod [in RSC.pts]
PTS.pstep_var [in RSC.pts]
PTS.Srt [in RSC.pts]
PTS.step_beta [in RSC.pts]
PTS.step_lamB [in RSC.pts]
PTS.step_lamD [in RSC.pts]
PTS.step_appR [in RSC.pts]
PTS.step_appL [in RSC.pts]
PTS.step_prodB [in RSC.pts]
PTS.step_prodD [in RSC.pts]
PTS.valid_ext [in RSC.pts]
PTS.valid_nil [in RSC.pts]
PTS.Var [in RSC.pts]

S

SA.F_spec.rel2 [in RSC.sysfCorrespondence]
SA.F_spec.rl1 [in RSC.sysfCorrespondence]
SA.F_spec.ax_base [in RSC.sysfCorrespondence]
SA.F_spec.Typ [in RSC.sysfCorrespondence]
SA.F_spec.Prp [in RSC.sysfCorrespondence]
SA.STLC_spec.rl1 [in RSC.stlcCorrespondence]
SA.STLC_spec.ax_base [in RSC.stlcCorrespondence]
SA.STLC_spec.Typ [in RSC.stlcCorrespondence]
SA.STLC_spec.Prp [in RSC.stlcCorrespondence]
starR [in RSC.ARS]
starRS [in RSC.ARS]

T

tmrel_lam [in RSC.stlcCorrespondence]
tmrel_app [in RSC.stlcCorrespondence]
tmrel_var [in RSC.stlcCorrespondence]
tmrel_tylam [in RSC.sysfCorrespondence]
tmrel_tyapp [in RSC.sysfCorrespondence]
tmrel_lam [in RSC.sysfCorrespondence]
tmrel_app [in RSC.sysfCorrespondence]
tmrel_var [in RSC.sysfCorrespondence]
TyApp [in RSC.sysf]
TyLam [in RSC.sysf]
tyrel_imp [in RSC.stlcCorrespondence]
tyrel_var [in RSC.stlcCorrespondence]
tyrel_all [in RSC.sysfCorrespondence]
tyrel_imp [in RSC.sysfCorrespondence]
tyrel_var [in RSC.sysfCorrespondence]
TyVar [in RSC.sysf]
TyVar [in RSC.stlc]

V

valid_ext_tm [in RSC.sysf]
valid_ext_ty [in RSC.sysf]
valid_empty [in RSC.sysf]
valid_ext [in RSC.stlc]
valid_nil [in RSC.stlc]
valid'_ext_tm [in RSC.sysf]
valid'_nil [in RSC.sysf]
Var [in RSC.sysf]
Var [in RSC.stlc]

Axiom Index

F

FPTS_sig.R_func [in RSC.pts]
FPTS_sig.A_func [in RSC.pts]

P

PTS_sig.R [in RSC.pts]
PTS_sig.A [in RSC.pts]
PTS_sig.decide_eq_srt [in RSC.pts]
PTS_sig.S [in RSC.pts]

Inductive Index

A

atn [in RSC.lib]
atnd [in RSC.lib]

C

conv [in RSC.ARS]

D

Dec [in RSC.Decidable]

H

hastype [in RSC.sysf]
hastype [in RSC.stlc]

I

istype [in RSC.sysf]
istype [in RSC.stlc]

P

PTS.hastype [in RSC.pts]
PTS.neutral [in RSC.pts]
PTS.normal [in RSC.pts]
PTS.pstep [in RSC.pts]
PTS.step [in RSC.pts]
PTS.tm [in RSC.pts]
PTS.valid [in RSC.pts]

S

SA.F_spec.rl [in RSC.sysfCorrespondence]
SA.F_spec.ax [in RSC.sysfCorrespondence]
SA.F_spec.level [in RSC.sysfCorrespondence]
SA.STLC_spec.rl [in RSC.stlcCorrespondence]
SA.STLC_spec.ax [in RSC.stlcCorrespondence]
SA.STLC_spec.level [in RSC.stlcCorrespondence]
star [in RSC.ARS]

T

tm [in RSC.sysf]
tm [in RSC.stlc]
tmrel [in RSC.stlcCorrespondence]
tmrel [in RSC.sysfCorrespondence]
ty [in RSC.sysf]
ty [in RSC.stlc]
tyrel [in RSC.stlcCorrespondence]
tyrel [in RSC.sysfCorrespondence]

V

valid [in RSC.sysf]
valid [in RSC.stlc]
valid' [in RSC.sysf]

Projection Index

B

bind [in RSC.lib]

C

countableProp [in RSC.Decidable]

D

decide [in RSC.Decidable]

E

enum [in RSC.Decidable]

F

finiteProp [in RSC.Decidable]
fmap [in RSC.lib]

N

numElems [in RSC.Decidable]

R

repr [in RSC.Decidable]
ret [in RSC.lib]

Section Index

C

Coincidence [in RSC.lib]
CoincidenceHSubst [in RSC.lib]
ContextRenamings [in RSC.lib]
CtxBoolFun [in RSC.lib]

D

Definitions [in RSC.ARS]

L

Lookup [in RSC.lib]

Instance Index

D

decidable_neg [in RSC.Decidable]
decide_eq_tm [in RSC.sysf]
decide_eq_ty [in RSC.sysf]
decide_eq_tm [in RSC.stlc]
decide_eq_ty [in RSC.stlc]
Dec_eq_fin_domain [in RSC.Decidable]
Dec_fin_quant [in RSC.Decidable]
Dec_fin_quant_T [in RSC.Decidable]
Dec_impl [in RSC.Decidable]
Dec_or [in RSC.Decidable]
Dec_and [in RSC.Decidable]
Dec_lt_nat [in RSC.Decidable]
Dec_le_nat [in RSC.Decidable]
Dec_eq_option [in RSC.Decidable]
Dec_eq_nat [in RSC.Decidable]

F

Functor_Monad [in RSC.lib]

H

HSubstLemmas_termF [in RSC.sysf]
HSubst_termF [in RSC.sysf]

I

Ids_tm [in RSC.sysf]
Ids_ty [in RSC.sysf]
Ids_tm [in RSC.stlc]
Ids_ty [in RSC.stlc]

P

PTS.decide_eq_termL [in RSC.pts]
PTS.Ids_tm [in RSC.pts]
PTS.Rename_tm [in RSC.pts]
PTS.SubstLemmas_tm [in RSC.pts]
PTS.Subst_tm [in RSC.pts]

R

Rename_tm [in RSC.sysf]
Rename_ty [in RSC.sysf]
Rename_tm [in RSC.stlc]
Rename_ty [in RSC.stlc]

S

SA.F_spec.decide_eq_srt [in RSC.sysfCorrespondence]
SA.STLC_spec.decide_eq_srt [in RSC.stlcCorrespondence]
SubstHSubstComp_typeF_termF [in RSC.sysf]
SubstLemmas_tm [in RSC.sysf]
SubstLemmas_ty [in RSC.sysf]
SubstLemmas_tm [in RSC.stlc]
SubstLemmas_ty [in RSC.stlc]
Subst_tm [in RSC.sysf]
Subst_ty [in RSC.sysf]
Subst_tm [in RSC.stlc]
Subst_ty [in RSC.stlc]

Abbreviation Index

D

dec [in RSC.Decidable]

E

eq_dec [in RSC.Decidable]

Definition Index

B

bfr [in RSC.lib]

C

cm_tmrel [in RSC.stlcCorrespondence]
cm_tyrel [in RSC.stlcCorrespondence]
cm_tmrel [in RSC.sysfCorrespondence]
cm_tyrel [in RSC.sysfCorrespondence]
comb [in RSC.lib]
composite [in RSC.ARS]
confluent [in RSC.ARS]
cr [in RSC.lib]
CR [in RSC.ARS]

D

diamond [in RSC.ARS]

E

equivalence [in RSC.ARS]

F

FPTS.hastype_pcr [in RSC.pts]

G

get [in RSC.lib]
getD [in RSC.lib]

H

hastype_cm [in RSC.stlc]
hastype_cr [in RSC.stlc]

I

idR [in RSC.vrel]
intern [in RSC.sysf]
intern_ty [in RSC.sysf]
intern_ctx [in RSC.stlc]
inverse [in RSC.ARS]
istype_cm [in RSC.sysf]
istype_cr [in RSC.sysf]
istype_cr [in RSC.stlc]

J

joinable [in RSC.ARS]

P

Pred [in RSC.ARS]
PTS.all [in RSC.pts]
PTS.allCtx [in RSC.pts]
PTS.hastype_cm [in RSC.pts]
PTS.hastype_cr [in RSC.pts]
PTS.mpstep [in RSC.pts]
PTS.nrm_ntr_ind [in RSC.pts]
PTS.nrm_ntr [in RSC.pts]
PTS.ntr_nrm [in RSC.pts]
PTS.NZ [in RSC.pts]
PTS.TrueP [in RSC.pts]

R

reflexive [in RSC.ARS]
Rel [in RSC.ARS]
rel_inj [in RSC.lib]
rel_func [in RSC.lib]

S

SA.F_spec.R [in RSC.sysfCorrespondence]
SA.F_spec.A [in RSC.sysfCorrespondence]
SA.F_spec.S [in RSC.sysfCorrespondence]
SA.intern [in RSC.sysfCorrespondence]
SA.prps [in RSC.stlcCorrespondence]
SA.STLC_spec.R [in RSC.stlcCorrespondence]
SA.STLC_spec.A [in RSC.stlcCorrespondence]
SA.STLC_spec.S [in RSC.stlcCorrespondence]
semiconfluent [in RSC.ARS]
subst_coinc [in RSC.lib]
sum2bool [in RSC.lib]
symmetric [in RSC.ARS]

T

transitive [in RSC.ARS]
triangle [in RSC.ARS]

V

vEXT [in RSC.vrel]
vrel [in RSC.vrel]
vrm [in RSC.vrel]
vRS [in RSC.vrel]
vr_tmctx_AB [in RSC.stlcCorrespondence]
vr_tmctx_BA [in RSC.stlcCorrespondence]
vr_tyctx_AB [in RSC.stlcCorrespondence]
vr_tyctx_BA [in RSC.stlcCorrespondence]
vr_tmctx_AB [in RSC.sysfCorrespondence]
vr_tmctx_BA [in RSC.sysfCorrespondence]
vr_tyctx_AB [in RSC.sysfCorrespondence]
vr_tyctx_BA [in RSC.sysfCorrespondence]
vr_inj [in RSC.vrel]
vr_func [in RSC.vrel]

Record Index

C

Countable [in RSC.Decidable]

D

Dec [in RSC.Decidable]

F

Finite [in RSC.Decidable]
Functor [in RSC.lib]

M

Monad [in RSC.lib]

Global Index

K

O

Q

W

X

Y

Z

_

(662 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(38 entries)

Module Index

A

B

C

D

E

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(10 entries)

Variable Index

A

B

C

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)

Library Index

B

C

E

F

G

H

I

J

K

M

N

O

Q

R

T

U

W

X

Y

Z

_

other

(9 entries)

Lemma Index

K

L

N

O

Q

R

W

X

Y

Z

_

other

(334 entries)

Constructor Index

B

E

F

G

J

K

M

N

O

Q

R

U

W

X

Y

Z

_

other

(97 entries)

Axiom Index

A

B

C

D

E

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Inductive Index

B

E

F

G

J

K

L

M

N

O

Q

R

U

W

X

Y

Z

_

other

(33 entries)

Projection Index

A

G

H

I

J

K

L

M

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Section Index

A

B

E

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Instance Index

A

B

C

E

G

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(42 entries)

Abbreviation Index

A

B

C

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Definition Index

A

K

L

M

N

O

Q

U

W

X

Y

Z

_

other

(69 entries)

Record Index

A

B

E

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)