Global Index

G

H

J

Q

X

Y

Z

_

(573 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(18 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

P

Q

R

T

U

V

W

X

Y

Z

_

other

(11 entries)

Library Index

A

B

C

E

F

G

H

I

J

L

N

P

Q

R

T

U

W

X

Y

Z

_

other

(10 entries)

Lemma Index

G

H

I

J

K

M

Q

V

X

Y

Z

_

other

(211 entries)

Constructor Index

C

F

G

H

I

J

K

M

N

P

Q

X

Y

Z

_

other

(153 entries)

Inductive Index

B

C

F

G

H

J

K

M

N

P

Q

X

Y

Z

_

other

(34 entries)

Section Index

G

H

I

J

K

N

Q

V

W

X

Y

Z

_

other

(26 entries)

Instance Index

A

B

D

G

H

I

J

K

M

N

P

Q

R

T

U

V

W

X

Y

Z

_

other

(25 entries)

Abbreviation Index

A

B

G

H

I

J

K

M

P

Q

R

T

U

V

W

X

Y

Z

_

other

(17 entries)

Definition Index

A

G

H

J

K

L

M

N

P

Q

X

Y

Z

_

other

(68 entries)

Global Index

A

Algorithmic [section, in Step]
avar [inductive, in VarDef]
avar_f [constructor, in VarDef]
avar_b [constructor, in VarDef]
avar_search_equiv [lemma, in Step]

B

BiSubtyProperties [section, in Stareat]
BisubtyStronger [section, in Step]
bnd_layer [definition, in Kernel]
bsubtyp [definition, in Stareat]
bsubtyp_sound [lemma, in Stareat]
bs'_bnd [constructor, in StrongKernel]
bs'_all [constructor, in StrongKernel]
bs'_sel_right [constructor, in StrongKernel]
bs'_sel_left [constructor, in StrongKernel]
bs'_sel_refl [constructor, in StrongKernel]
bs'_top [constructor, in StrongKernel]
bs'_bot [constructor, in StrongKernel]
bt_bnd [constructor, in Stareat]
bt_all [constructor, in Stareat]
bt_sel_right [constructor, in Stareat]
bt_sel_left [constructor, in Stareat]
bt_sel_refl [constructor, in Stareat]
bt_top [constructor, in Stareat]
bt_bot [constructor, in Stareat]
bv_search_idx [lemma, in Step]
bv_search_equiv [lemma, in Step]

C

CloseAvar [instance, in Definitions]
CloseTrm [instance, in Definitions]
CloseTyp [instance, in Definitions]
CloseVal [instance, in Definitions]
close_lc_val [lemma, in OperationProperties]
close_lc_trm [lemma, in OperationProperties]
close_lc_typ [lemma, in OperationProperties]
close_lc_avar [lemma, in OperationProperties]
close_lc [abbreviation, in OperationProperties]
close_rec_val [definition, in Definitions]
close_rec_trm [definition, in Definitions]
close_rec_typ [definition, in Definitions]
close_rec_avar [definition, in Definitions]
ClosingDefinitions [section, in Definitions]

D

dce_bnd [constructor, in Step]
dce_top [constructor, in Step]
dce_bot [constructor, in Step]
dc_bnd [constructor, in Stareat]
dc_top [constructor, in Stareat]
dc_bot [constructor, in Stareat]
Definitions [library]
denv [abbreviation, in Step]
denv_measure [definition, in Step]
denv_fv [definition, in Step]
de_bnd [constructor, in Kernel]
de_top [constructor, in Kernel]
de_bot [constructor, in Kernel]
downcast [inductive, in Stareat]
DowncastProperties [section, in Stareat]
downcast_f_dep_eq_downcast_f [lemma, in Stareat]
downcast_f_dep [definition, in Stareat]
downcast_f_u_eq [lemma, in Stareat]
downcast_f_u [definition, in Stareat]
downcast_func_decreases_measure [lemma, in Stareat]
downcast_func_sound_wrt_spec [lemma, in Stareat]
downcast_func [definition, in Stareat]
downcast_preserves_wf [lemma, in Stareat]
downcast_sound [lemma, in Stareat]
downcast_decreases_measure [lemma, in Stareat]
downcast_e'_to_downcast_e [lemma, in Kernel]
downcast_e' [inductive, in Kernel]
downcast_e_measure_decrease [lemma, in Step]
downcast_gives_prefix [lemma, in Step]
downcast_strengthening [lemma, in Step]
downcast_e_to_downcast [lemma, in Step]
downcast_e_preserves_lc [lemma, in Step]
downcast_e_preserves_wf [lemma, in Step]
downcast_e [inductive, in Step]

E

env [abbreviation, in Definitions]
env_measure_app [lemma, in Misc]
env_measure_cons [lemma, in Misc]
env_measure [definition, in Misc]
EqAvar [instance, in VarDef]
EqDecTyp [instance, in Definitions]
EquivalentRepr [section, in Step]
eq_typ_sel [definition, in Stareat]
exposure [inductive, in Step]
exposure_measure_decrease [lemma, in Step]
exposure_sound [lemma, in Step]
exposure_to_exposure' [lemma, in Step]
exposure_weakening [lemma, in Step]
exposure_preserves_lc [lemma, in Step]
exposure_preserves_wf [lemma, in Step]
exposure_strengthening [lemma, in Step]
exposure_to_revealing [lemma, in Step]
exposure_to_revealing_gen [lemma, in Step]
exposure' [inductive, in Step]
exposure'_to_subtysk [lemma, in StrongKernel]
exposure'_to_subtykn [lemma, in Kernel]
exposure'_equiv_exposure [lemma, in Step]
exposure'_to_exposure [lemma, in Step]
exposure'_weakening_gen [lemma, in Step]
exposure'_weakening [lemma, in Step]
exp_bnd [constructor, in Step]
exp_bot [constructor, in Step]
exp_top [constructor, in Step]
exp_stop [constructor, in Step]
ex_bnd [constructor, in Step]
ex_bot [constructor, in Step]
ex_top [constructor, in Step]
ex_stop [constructor, in Step]

F

FreeVariables [section, in Definitions]
free_all [lemma, in StructuralProperties]
fresh_inj [abbreviation, in OperationProperties]
FvAvar [instance, in Definitions]
FvClose [section, in OperationProperties]
FvDenv [instance, in Step]
FvEnv [instance, in Definitions]
FvOpen [section, in OperationProperties]
FvTrm [instance, in Definitions]
FvTyp [instance, in Definitions]
FvVal [instance, in Definitions]
fv_add_close_val [lemma, in OperationProperties]
fv_add_close_trm [lemma, in OperationProperties]
fv_add_close_typ [lemma, in OperationProperties]
fv_add_close_avar [lemma, in OperationProperties]
fv_add_close [abbreviation, in OperationProperties]
fv_close_val [lemma, in OperationProperties]
fv_close_trm [lemma, in OperationProperties]
fv_close_typ [lemma, in OperationProperties]
fv_close_avar [lemma, in OperationProperties]
fv_close [abbreviation, in OperationProperties]
fv_close_self_val [lemma, in OperationProperties]
fv_close_self_trm [lemma, in OperationProperties]
fv_close_self_typ [lemma, in OperationProperties]
fv_close_self_avar [lemma, in OperationProperties]
fv_close_self [abbreviation, in OperationProperties]
fv_open_val [lemma, in OperationProperties]
fv_open_trm [lemma, in OperationProperties]
fv_open_typ [lemma, in OperationProperties]
fv_open_avar [lemma, in OperationProperties]
fv_open [abbreviation, in OperationProperties]
fv_union [lemma, in Definitions]
fv_val [definition, in Definitions]
fv_trm [definition, in Definitions]
fv_typ [definition, in Definitions]
fv_avar [definition, in Definitions]
fv_unpack [lemma, in VarDef]
fv_values [definition, in VarDef]
fv_deapp [lemma, in Stareat]
fv_ignores_D [lemma, in Step]
fv_search_equiv [lemma, in Step]

I

incr_lc [inductive, in Step]
is_bnd_dec [definition, in Misc]
is_bnd [definition, in Misc]
is_all_dec [definition, in Misc]
is_all [definition, in Misc]
is_sel_dec [definition, in Misc]
is_sel [definition, in Misc]
is_bot_dec [definition, in Misc]
is_bot [definition, in Misc]
is_top_dec [definition, in Misc]
is_top [definition, in Misc]

K

Kernel [library]

L

layered_bot_trans [lemma, in StrongKernel]
layered_top_trans [lemma, in StrongKernel]
layered_bot_trans [lemma, in Kernel]
layered_top_trans [lemma, in Kernel]
LcAvar [instance, in Definitions]
LcOpenClosingProperties [section, in OperationProperties]
LcTrm [instance, in Definitions]
LcTyp [instance, in Definitions]
LcVal [instance, in Definitions]
lc_relax_val [lemma, in OperationProperties]
lc_relax_trm [lemma, in OperationProperties]
lc_relax_typ [lemma, in OperationProperties]
lc_relax_avar [lemma, in OperationProperties]
lc_relax [abbreviation, in OperationProperties]
lc_val_lam [constructor, in Definitions]
lc_val_bnd [constructor, in Definitions]
lc_val_at [inductive, in Definitions]
lc_trm_let [constructor, in Definitions]
lc_trm_app [constructor, in Definitions]
lc_trm_val [constructor, in Definitions]
lc_trm_var [constructor, in Definitions]
lc_trm_at [inductive, in Definitions]
lc_typ_bnd [constructor, in Definitions]
lc_typ_all [constructor, in Definitions]
lc_typ_sel [constructor, in Definitions]
lc_typ_bot [constructor, in Definitions]
lc_typ_top [constructor, in Definitions]
lc_typ_at [inductive, in Definitions]
lc_af [constructor, in Definitions]
lc_ab [constructor, in Definitions]
lc_avar_at [inductive, in Definitions]
lc_cons [constructor, in Step]
lc_nil [constructor, in Step]
LocalClosure [section, in Definitions]

M

MeasuresAndFacts [section, in Step]
Misc [library]

N

narrowing [abbreviation, in StructuralProperties]
narrow_subty [lemma, in StructuralProperties]
narrow_typing [lemma, in StructuralProperties]
narrow_subty_gen [lemma, in StructuralProperties]
narrow_typing_gen [lemma, in StructuralProperties]
narrow_var [lemma, in StructuralProperties]

O

OpenAvar [instance, in Definitions]
OpenFreshInj [section, in OperationProperties]
OpenFreshInj.z [variable, in OperationProperties]
OpeningDefinitions [section, in Definitions]
OpenTrm [instance, in Definitions]
OpenTyp [instance, in Definitions]
OpenVal [instance, in Definitions]
open_substi_rewrite2 [lemma, in OperationProperties]
open_substi_rewrite [lemma, in OperationProperties]
open_fresh_inj_val [lemma, in OperationProperties]
open_fresh_inj_trm [lemma, in OperationProperties]
open_fresh_inj_typ [lemma, in OperationProperties]
open_fresh_inj_avar [lemma, in OperationProperties]
open_left_inv_val [lemma, in OperationProperties]
open_left_inv_trm [lemma, in OperationProperties]
open_left_inv_typ [lemma, in OperationProperties]
open_left_inv_avar [lemma, in OperationProperties]
open_left_inv [abbreviation, in OperationProperties]
open_lc_inv_val [lemma, in OperationProperties]
open_lc_inv_trm [lemma, in OperationProperties]
open_lc_inv_typ [lemma, in OperationProperties]
open_lc_inv_avar [lemma, in OperationProperties]
open_lc_inv [abbreviation, in OperationProperties]
open_lc_le_val [lemma, in OperationProperties]
open_lc_le_trm [lemma, in OperationProperties]
open_lc_le_typ [lemma, in OperationProperties]
open_lc_le_avar [lemma, in OperationProperties]
open_lc_le [abbreviation, in OperationProperties]
open_lc_val [lemma, in OperationProperties]
open_lc_trm [lemma, in OperationProperties]
open_lc_typ [lemma, in OperationProperties]
open_lc_avar [lemma, in OperationProperties]
open_lc [abbreviation, in OperationProperties]
open_rec_val [definition, in Definitions]
open_rec_trm [definition, in Definitions]
open_rec_typ [definition, in Definitions]
open_rec_avar [definition, in Definitions]
open_subst_subty [lemma, in StructuralProperties]
open_subst_typing [lemma, in StructuralProperties]
open_val_same_measure [lemma, in Misc]
open_trm_same_measure [lemma, in Misc]
open_typ_same_measure [lemma, in Misc]
open_rec_D [definition, in Step]
OpeProperties [section, in OpeSub]
OperationProperties [library]
OpeSub [library]
ope_sub_stareat_sound [lemma, in Stareat]
ope_sub_app [lemma, in OpeSub]
ope_sub_nil [lemma, in OpeSub]
ope_sub_refl [lemma, in OpeSub]
ope_sub_trans [lemma, in OpeSub]
ope_narrow_subty [lemma, in OpeSub]
ope_narrow_trm [lemma, in OpeSub]
ope_narrow_var [lemma, in OpeSub]
ope_sub_length [lemma, in OpeSub]
ope_sub [inductive, in OpeSub]
ope_list_fv_env_subset [lemma, in Step]
os_keep [constructor, in OpeSub]
os_drop [constructor, in OpeSub]
os_nil [constructor, in OpeSub]

P

Predicates [section, in Misc]
prefix_wf_env [lemma, in Step]

R

renaming_fresh [lemma, in StructuralProperties]
renaming_subty [lemma, in StructuralProperties]
renaming_trm [lemma, in StructuralProperties]
revealing [inductive, in Stareat]
RevealingProperties [section, in Stareat]
RevealingSubsumesExposure [section, in Step]
revealing_to_subtysk [lemma, in StrongKernel]
revealing_fv_bound [lemma, in StrongKernel]
revealing_terminates [definition, in Stareat]
revealing_measure [lemma, in Stareat]
revealing_preserves_wf [lemma, in Stareat]
revealing_sound [lemma, in Stareat]
revealing_termination [inductive, in Stareat]
revealing_to_exposure [lemma, in Step]
revealing_strengthening [lemma, in Step]
revealing_sel_weakening_prefix [lemma, in Step]
revealing_sel_weakening [lemma, in Step]
revealing_gives_prefix [lemma, in Step]
reveal_func_sound_wrt_spec [lemma, in Stareat]
reveal_func [definition, in Stareat]
rt_bnd [constructor, in Stareat]
rt_bot [constructor, in Stareat]
rt_top [constructor, in Stareat]
rt_stop [constructor, in Stareat]
rv_bnd [constructor, in Stareat]
rv_bot [constructor, in Stareat]
rv_top [constructor, in Stareat]
rv_stop [constructor, in Stareat]

S

sa_bnd [constructor, in Stareat]
sa_all [constructor, in Stareat]
sa_sel_right [constructor, in Stareat]
sa_sel_left [constructor, in Stareat]
sa_sel_refl [constructor, in Stareat]
sa_top [constructor, in Stareat]
sa_bot [constructor, in Stareat]
sk_trans_on_bot [lemma, in StrongKernel]
sk_trans_on_top [lemma, in StrongKernel]
snf_sel2 [constructor, in Kernel]
snf_sel1 [constructor, in Kernel]
snf_all [constructor, in Kernel]
snf_bnd [constructor, in Kernel]
snf_bot [constructor, in Kernel]
snf_top [constructor, in Kernel]
snf_vrefl [constructor, in Kernel]
snf'_sel2 [constructor, in Kernel]
snf'_sel1 [constructor, in Kernel]
snf'_all [constructor, in Kernel]
snf'_bnd [constructor, in Kernel]
snf'_bot [constructor, in Kernel]
snf'_top [constructor, in Kernel]
snf'_refl [constructor, in Kernel]
ssk_sel2 [constructor, in StrongKernel]
ssk_sel1 [constructor, in StrongKernel]
ssk_all [constructor, in StrongKernel]
ssk_bnd [constructor, in StrongKernel]
ssk_bot [constructor, in StrongKernel]
ssk_top [constructor, in StrongKernel]
ssk_refl [constructor, in StrongKernel]
ssk'_sel2 [constructor, in StrongKernel]
ssk'_sel1 [constructor, in StrongKernel]
ssk'_all [constructor, in StrongKernel]
ssk'_bnd [constructor, in StrongKernel]
ssk'_bot [constructor, in StrongKernel]
ssk'_top [constructor, in StrongKernel]
ssk'_refl [constructor, in StrongKernel]
sst_all [constructor, in Step]
sst_bnd [constructor, in Step]
sst_sel_right [constructor, in Step]
sst_sel_left [constructor, in Step]
sst_sel_refl [constructor, in Step]
sst_bot [constructor, in Step]
sst_top [constructor, in Step]
ss_all [constructor, in Step]
ss_bnd [constructor, in Step]
ss_sel_right [constructor, in Step]
ss_sel_left [constructor, in Step]
ss_sel_refl [constructor, in Step]
ss_bot [constructor, in Step]
ss_top [constructor, in Step]
ss'_all [constructor, in Kernel]
ss'_bnd [constructor, in Kernel]
ss'_sel_right [constructor, in Kernel]
ss'_sel_left [constructor, in Kernel]
ss'_sel_refl [constructor, in Kernel]
ss'_bot [constructor, in Kernel]
ss'_top [constructor, in Kernel]
stareat [inductive, in Stareat]
Stareat [library]
stareat_cong_names [lemma, in StrongKernel]
stareat_to_subtysk [lemma, in StrongKernel]
stareat_to_stareat' [lemma, in StrongKernel]
stareat_terminates [definition, in Stareat]
stareat_termination [inductive, in Stareat]
stareat_refl [definition, in Stareat]
stareat_strengthening [lemma, in Step]
stareat' [inductive, in StrongKernel]
stareat'_to_subtysk [lemma, in StrongKernel]
stareat'_weakening_r [lemma, in StrongKernel]
stareat'_weakening_l [lemma, in StrongKernel]
stareat'_weakening_gen [lemma, in StrongKernel]
stareat'_to_stareat [lemma, in StrongKernel]
Step [library]
stp_subty'_to_stp_subty [lemma, in Kernel]
stp_subty'_refl [definition, in Kernel]
stp_subty' [inductive, in Kernel]
stp_subty_to_subtykn [lemma, in Kernel]
stp_subty_terminates [definition, in Step]
stp_subty_termination [inductive, in Step]
stp_subty_sound [lemma, in Step]
stp_subty_to_stareat [lemma, in Step]
stp_subty [inductive, in Step]
StrongKernel [library]
StructuralProperties [section, in StructuralProperties]
StructuralProperties [library]
_ ⪯ _ [notation, in StructuralProperties]
st_sel2 [constructor, in Definitions]
st_sel1 [constructor, in Definitions]
st_all [constructor, in Definitions]
st_bnd [constructor, in Definitions]
st_trans [constructor, in Definitions]
st_bot [constructor, in Definitions]
st_top [constructor, in Definitions]
st_refl [constructor, in Definitions]
subenv [inductive, in StructuralProperties]
subenv_implies_uniq [lemma, in StructuralProperties]
subenv_last [lemma, in StructuralProperties]
subenv_push [lemma, in StructuralProperties]
subenv_refl [lemma, in StructuralProperties]
subenv_grow [constructor, in StructuralProperties]
subenv_empty [constructor, in StructuralProperties]
SubstAvar [instance, in Definitions]
SubstFresh [section, in OperationProperties]
SubstFresh.x [variable, in OperationProperties]
SubstFresh.y [variable, in OperationProperties]
SubstFvarProps [section, in OperationProperties]
SubstFvarProps.subst_open_comm [variable, in OperationProperties]
SubstFvarProps.t [variable, in OperationProperties]
SubstFvarProps.T [variable, in OperationProperties]
SubstFvarProps.x [variable, in OperationProperties]
SubstFvarProps.y [variable, in OperationProperties]
SubstFvarProps.z [variable, in OperationProperties]
SubstiEnv [instance, in StructuralProperties]
SubstIntro [section, in OperationProperties]
Substitutions [section, in Definitions]
SubstOpenComm [section, in OperationProperties]
SubstOpenComm.x [variable, in OperationProperties]
SubstOpenComm.y [variable, in OperationProperties]
SubstTrm [instance, in Definitions]
SubstTyp [instance, in Definitions]
SubstVal [instance, in Definitions]
subst_intro_typ [lemma, in OperationProperties]
subst_intro_val [lemma, in OperationProperties]
subst_intro_trm [lemma, in OperationProperties]
subst_intro [abbreviation, in OperationProperties]
subst_open_comm_val [lemma, in OperationProperties]
subst_open_comm_trm [lemma, in OperationProperties]
subst_open_comm_typ [lemma, in OperationProperties]
subst_open_comm_avar [lemma, in OperationProperties]
subst_open_comm [abbreviation, in OperationProperties]
subst_fvar [definition, in OperationProperties]
subst_fresh_val [lemma, in OperationProperties]
subst_fresh_trm [lemma, in OperationProperties]
subst_fresh_typ [lemma, in OperationProperties]
subst_fresh_avar [lemma, in OperationProperties]
subst_fresh [abbreviation, in OperationProperties]
subst_val [definition, in Definitions]
subst_trm [definition, in Definitions]
subst_typ [definition, in Definitions]
subst_avar [definition, in Definitions]
subst_trm_var [lemma, in StructuralProperties]
subst_env [definition, in StructuralProperties]
subty [inductive, in Definitions]
subtykn [inductive, in Kernel]
subtykn_to_subtysk [lemma, in StrongKernel]
subtykn_equiv_stp_subty [lemma, in Kernel]
subtykn_to_stp_subty [lemma, in Kernel]
subtykn_to_stp_subty' [lemma, in Kernel]
subtykn_equiv_subtykn' [lemma, in Kernel]
subtykn_to_subtykn' [lemma, in Kernel]
subtykn_sound [lemma, in Kernel]
subtykn_refl [definition, in Kernel]
subtykn' [inductive, in Kernel]
subtykn'_conversions [definition, in Kernel]
subtykn'_to_subtykn [lemma, in Kernel]
subtysk [inductive, in StrongKernel]
subtysk_equiv_stareat [lemma, in StrongKernel]
subtysk_to_stareat [lemma, in StrongKernel]
subtysk_to_stareat' [lemma, in StrongKernel]
subtysk_equiv_subtysk' [lemma, in StrongKernel]
subtysk_to_subtysk' [lemma, in StrongKernel]
subtysk_sound [lemma, in StrongKernel]
subtysk_sound_gen [lemma, in StrongKernel]
subtysk_refl [definition, in StrongKernel]
subtysk' [inductive, in StrongKernel]
subtysk'_conversions [definition, in StrongKernel]
subtysk'_to_subtysk [lemma, in StrongKernel]
subty_subst [lemma, in StructuralProperties]
subty_subst_gen [lemma, in StructuralProperties]
subty_measure [definition, in Stareat]

T

Termination [section, in Stareat]
total [definition, in Misc]
total_app [lemma, in Misc]
trans_on_bot [lemma, in Kernel]
trans_on_top [lemma, in Kernel]
trm [inductive, in Definitions]
trm_let [constructor, in Definitions]
trm_app [constructor, in Definitions]
trm_val [constructor, in Definitions]
trm_var [constructor, in Definitions]
trm_struct_measure [definition, in Misc]
typ [inductive, in Definitions]
typing [inductive, in Definitions]
typing_subst [lemma, in StructuralProperties]
typing_subst_gen [lemma, in StructuralProperties]
typ_bnd [constructor, in Definitions]
typ_all [constructor, in Definitions]
typ_sel [constructor, in Definitions]
typ_bot [constructor, in Definitions]
typ_top [constructor, in Definitions]
typ_struct_measure_ge_1 [lemma, in Misc]
typ_struct_measure [definition, in Misc]
ty_sub [constructor, in Definitions]
ty_let [constructor, in Definitions]
ty_app [constructor, in Definitions]
ty_lam [constructor, in Definitions]
ty_bnd [constructor, in Definitions]
ty_var [constructor, in Definitions]

U

uce_bnd [constructor, in Step]
uce_bot [constructor, in Step]
uce_top [constructor, in Step]
uc_bnd [constructor, in Stareat]
uc_bot [constructor, in Stareat]
uc_top [constructor, in Stareat]
ue_bnd [constructor, in Kernel]
ue_bot [constructor, in Kernel]
ue_top [constructor, in Kernel]
upcast [inductive, in Stareat]
UpcastProperties [section, in Stareat]
upcast_f_dep_eq_upcast_f [lemma, in Stareat]
upcast_f_dep [definition, in Stareat]
upcast_f_u_eq [lemma, in Stareat]
upcast_f_u [definition, in Stareat]
upcast_func_decreases_measure [lemma, in Stareat]
upcast_func_sound_wrt_spec [lemma, in Stareat]
upcast_func [definition, in Stareat]
upcast_preserves_wf [lemma, in Stareat]
upcast_sound [lemma, in Stareat]
upcast_decreases_measure [lemma, in Stareat]
upcast_e'_to_upcast_e [lemma, in Kernel]
upcast_e' [inductive, in Kernel]
upcast_e_measure_decrease [lemma, in Step]
upcast_gives_prefix [lemma, in Step]
upcast_strengthening [lemma, in Step]
upcast_e_to_upcast [lemma, in Step]
upcast_e_preserves_lc [lemma, in Step]
upcast_e_preserves_wf [lemma, in Step]
upcast_e [inductive, in Step]

V

val [inductive, in Definitions]
val_lam [constructor, in Definitions]
val_bnd [constructor, in Definitions]
val_struct_measure [definition, in Misc]
VarDef [library]

W

weaken_subty [definition, in StructuralProperties]
weaken_typing [definition, in StructuralProperties]
weaken_subty_gen [lemma, in StructuralProperties]
weaken_typing_gen [lemma, in StructuralProperties]
weaken_subtykn [lemma, in Kernel]
weaken_subtykn_gen [lemma, in Kernel]
wf_fv_is_dom [lemma, in Misc]
wf_var_in [lemma, in Misc]
wf_uniq [lemma, in Misc]
wf_deapp [lemma, in Misc]
wf_decons [lemma, in Misc]
wf_cons [constructor, in Misc]
wf_nil [constructor, in Misc]
wf_env [inductive, in Misc]
wf_search_lookup [lemma, in Step]
wf_search_wf_ge_1 [lemma, in Step]
wf_open_shift [lemma, in Step]
wf_open_shift_gen [definition, in Step]
wf_search_impl_avar_f_eq [lemma, in Step]
wf_lookup_lt [lemma, in Step]
wf_search_weaken [lemma, in Step]
wf_search_weaken_gen [definition, in Step]
wf_weaken_measure [definition, in Step]
wf_search_fv_weaken [lemma, in Step]
wf_search_avar [definition, in Step]
wf_search_bv [definition, in Step]
wf_search_fv [definition, in Step]
wf_search [definition, in Step]
wf_search_impl [definition, in Step]
wf_measure [definition, in Step]

other

_ ⊢ _ <⦂ _ [notation, in Definitions]
_ ⊢ _ ⦂ _ [notation, in Definitions]
_ ⊢S _ <⦂ _ [notation, in Stareat]
_ ⊢ _ ↘ _ ⊢! _ [notation, in Stareat]
_ ⊢ _ ↗ _ ⊢! _ [notation, in Stareat]
_ ⊢ _ ⤊ _ ⊢! _ [notation, in Stareat]
_ ⊆<⦂ _ [notation, in OpeSub]
_ ⊢ _ ↘! _ [notation, in Step]
_ ⊢ _ ↗! _ [notation, in Step]
_ ⊢ _ ⇑ _ [notation, in Step]
[ _ , _ ] _ ⊢k _ <⦂ _ k⊣ _ [notation, in StrongKernel]
[ _ ] _ >> _ <⦂p _ << _ [notation, in StrongKernel]
[ _ ] _ ⊢k _ <⦂ _ k⊣ _ [notation, in StrongKernel]
[ _ ] _ >> _ <⦂ _ << _ [notation, in Stareat]
[ _ , _ ] _ ⊢k _ <⦂ _ [notation, in Kernel]
[ _ ] _ ⊢k _ <⦂ _ [notation, in Kernel]
[ _ ] _ ⊢s _ <⦂ _ [notation, in Step]

Notation Index

S

_ ⪯ _ [in StructuralProperties]

other

_ ⊢ _ <⦂ _ [in Definitions]
_ ⊢ _ ⦂ _ [in Definitions]
_ ⊢S _ <⦂ _ [in Stareat]
_ ⊢ _ ↘ _ ⊢! _ [in Stareat]
_ ⊢ _ ↗ _ ⊢! _ [in Stareat]
_ ⊢ _ ⤊ _ ⊢! _ [in Stareat]
_ ⊆<⦂ _ [in OpeSub]
_ ⊢ _ ↘! _ [in Step]
_ ⊢ _ ↗! _ [in Step]
_ ⊢ _ ⇑ _ [in Step]
[ _ , _ ] _ ⊢k _ <⦂ _ k⊣ _ [in StrongKernel]
[ _ ] _ >> _ <⦂p _ << _ [in StrongKernel]
[ _ ] _ ⊢k _ <⦂ _ k⊣ _ [in StrongKernel]
[ _ ] _ >> _ <⦂ _ << _ [in Stareat]
[ _ , _ ] _ ⊢k _ <⦂ _ [in Kernel]
[ _ ] _ ⊢k _ <⦂ _ [in Kernel]
[ _ ] _ ⊢s _ <⦂ _ [in Step]

Variable Index

O

OpenFreshInj.z [in OperationProperties]

S

SubstFresh.x [in OperationProperties]
SubstFresh.y [in OperationProperties]
SubstFvarProps.subst_open_comm [in OperationProperties]
SubstFvarProps.t [in OperationProperties]
SubstFvarProps.T [in OperationProperties]
SubstFvarProps.x [in OperationProperties]
SubstFvarProps.y [in OperationProperties]
SubstFvarProps.z [in OperationProperties]
SubstOpenComm.x [in OperationProperties]
SubstOpenComm.y [in OperationProperties]

Library Index

D

K

Kernel

M

Misc

O

OperationProperties
OpeSub

S

Stareat
Step
StrongKernel
StructuralProperties

V

VarDef

Lemma Index

A

avar_search_equiv [in Step]

B

bsubtyp_sound [in Stareat]
bv_search_idx [in Step]
bv_search_equiv [in Step]

C

close_lc_val [in OperationProperties]
close_lc_trm [in OperationProperties]
close_lc_typ [in OperationProperties]
close_lc_avar [in OperationProperties]

D

downcast_f_dep_eq_downcast_f [in Stareat]
downcast_f_u_eq [in Stareat]
downcast_func_decreases_measure [in Stareat]
downcast_func_sound_wrt_spec [in Stareat]
downcast_preserves_wf [in Stareat]
downcast_sound [in Stareat]
downcast_decreases_measure [in Stareat]
downcast_e'_to_downcast_e [in Kernel]
downcast_e_measure_decrease [in Step]
downcast_gives_prefix [in Step]
downcast_strengthening [in Step]
downcast_e_to_downcast [in Step]
downcast_e_preserves_lc [in Step]
downcast_e_preserves_wf [in Step]

E

env_measure_app [in Misc]
env_measure_cons [in Misc]
exposure_measure_decrease [in Step]
exposure_sound [in Step]
exposure_to_exposure' [in Step]
exposure_weakening [in Step]
exposure_preserves_lc [in Step]
exposure_preserves_wf [in Step]
exposure_strengthening [in Step]
exposure_to_revealing [in Step]
exposure_to_revealing_gen [in Step]
exposure'_to_subtysk [in StrongKernel]
exposure'_to_subtykn [in Kernel]
exposure'_equiv_exposure [in Step]
exposure'_to_exposure [in Step]
exposure'_weakening_gen [in Step]
exposure'_weakening [in Step]

F

free_all [in StructuralProperties]
fv_add_close_val [in OperationProperties]
fv_add_close_trm [in OperationProperties]
fv_add_close_typ [in OperationProperties]
fv_add_close_avar [in OperationProperties]
fv_close_val [in OperationProperties]
fv_close_trm [in OperationProperties]
fv_close_typ [in OperationProperties]
fv_close_avar [in OperationProperties]
fv_close_self_val [in OperationProperties]
fv_close_self_trm [in OperationProperties]
fv_close_self_typ [in OperationProperties]
fv_close_self_avar [in OperationProperties]
fv_open_val [in OperationProperties]
fv_open_trm [in OperationProperties]
fv_open_typ [in OperationProperties]
fv_open_avar [in OperationProperties]
fv_union [in Definitions]
fv_unpack [in VarDef]
fv_deapp [in Stareat]
fv_ignores_D [in Step]
fv_search_equiv [in Step]

L

layered_bot_trans [in StrongKernel]
layered_top_trans [in StrongKernel]
layered_bot_trans [in Kernel]
layered_top_trans [in Kernel]
lc_relax_val [in OperationProperties]
lc_relax_trm [in OperationProperties]
lc_relax_typ [in OperationProperties]
lc_relax_avar [in OperationProperties]

N

narrow_subty [in StructuralProperties]
narrow_typing [in StructuralProperties]
narrow_subty_gen [in StructuralProperties]
narrow_typing_gen [in StructuralProperties]
narrow_var [in StructuralProperties]

O

open_substi_rewrite2 [in OperationProperties]
open_substi_rewrite [in OperationProperties]
open_fresh_inj_val [in OperationProperties]
open_fresh_inj_trm [in OperationProperties]
open_fresh_inj_typ [in OperationProperties]
open_fresh_inj_avar [in OperationProperties]
open_left_inv_val [in OperationProperties]
open_left_inv_trm [in OperationProperties]
open_left_inv_typ [in OperationProperties]
open_left_inv_avar [in OperationProperties]
open_lc_inv_val [in OperationProperties]
open_lc_inv_trm [in OperationProperties]
open_lc_inv_typ [in OperationProperties]
open_lc_inv_avar [in OperationProperties]
open_lc_le_val [in OperationProperties]
open_lc_le_trm [in OperationProperties]
open_lc_le_typ [in OperationProperties]
open_lc_le_avar [in OperationProperties]
open_lc_val [in OperationProperties]
open_lc_trm [in OperationProperties]
open_lc_typ [in OperationProperties]
open_lc_avar [in OperationProperties]
open_subst_subty [in StructuralProperties]
open_subst_typing [in StructuralProperties]
open_val_same_measure [in Misc]
open_trm_same_measure [in Misc]
open_typ_same_measure [in Misc]
ope_sub_stareat_sound [in Stareat]
ope_sub_app [in OpeSub]
ope_sub_nil [in OpeSub]
ope_sub_refl [in OpeSub]
ope_sub_trans [in OpeSub]
ope_narrow_subty [in OpeSub]
ope_narrow_trm [in OpeSub]
ope_narrow_var [in OpeSub]
ope_sub_length [in OpeSub]
ope_list_fv_env_subset [in Step]

P

prefix_wf_env [in Step]

R

renaming_fresh [in StructuralProperties]
renaming_subty [in StructuralProperties]
renaming_trm [in StructuralProperties]
revealing_to_subtysk [in StrongKernel]
revealing_fv_bound [in StrongKernel]
revealing_measure [in Stareat]
revealing_preserves_wf [in Stareat]
revealing_sound [in Stareat]
revealing_to_exposure [in Step]
revealing_strengthening [in Step]
revealing_sel_weakening_prefix [in Step]
revealing_sel_weakening [in Step]
revealing_gives_prefix [in Step]
reveal_func_sound_wrt_spec [in Stareat]

S

sk_trans_on_bot [in StrongKernel]
sk_trans_on_top [in StrongKernel]
stareat_cong_names [in StrongKernel]
stareat_to_subtysk [in StrongKernel]
stareat_to_stareat' [in StrongKernel]
stareat_strengthening [in Step]
stareat'_to_subtysk [in StrongKernel]
stareat'_weakening_r [in StrongKernel]
stareat'_weakening_l [in StrongKernel]
stareat'_weakening_gen [in StrongKernel]
stareat'_to_stareat [in StrongKernel]
stp_subty'_to_stp_subty [in Kernel]
stp_subty_to_subtykn [in Kernel]
stp_subty_sound [in Step]
stp_subty_to_stareat [in Step]
subenv_implies_uniq [in StructuralProperties]
subenv_last [in StructuralProperties]
subenv_push [in StructuralProperties]
subenv_refl [in StructuralProperties]
subst_intro_typ [in OperationProperties]
subst_intro_val [in OperationProperties]
subst_intro_trm [in OperationProperties]
subst_open_comm_val [in OperationProperties]
subst_open_comm_trm [in OperationProperties]
subst_open_comm_typ [in OperationProperties]
subst_open_comm_avar [in OperationProperties]
subst_fresh_val [in OperationProperties]
subst_fresh_trm [in OperationProperties]
subst_fresh_typ [in OperationProperties]
subst_fresh_avar [in OperationProperties]
subst_trm_var [in StructuralProperties]
subtykn_to_subtysk [in StrongKernel]
subtykn_equiv_stp_subty [in Kernel]
subtykn_to_stp_subty [in Kernel]
subtykn_to_stp_subty' [in Kernel]
subtykn_equiv_subtykn' [in Kernel]
subtykn_to_subtykn' [in Kernel]
subtykn_sound [in Kernel]
subtykn'_to_subtykn [in Kernel]
subtysk_equiv_stareat [in StrongKernel]
subtysk_to_stareat [in StrongKernel]
subtysk_to_stareat' [in StrongKernel]
subtysk_equiv_subtysk' [in StrongKernel]
subtysk_to_subtysk' [in StrongKernel]
subtysk_sound [in StrongKernel]
subtysk_sound_gen [in StrongKernel]
subtysk'_to_subtysk [in StrongKernel]
subty_subst [in StructuralProperties]
subty_subst_gen [in StructuralProperties]

T

total_app [in Misc]
trans_on_bot [in Kernel]
trans_on_top [in Kernel]
typing_subst [in StructuralProperties]
typing_subst_gen [in StructuralProperties]
typ_struct_measure_ge_1 [in Misc]

U

upcast_f_dep_eq_upcast_f [in Stareat]
upcast_f_u_eq [in Stareat]
upcast_func_decreases_measure [in Stareat]
upcast_func_sound_wrt_spec [in Stareat]
upcast_preserves_wf [in Stareat]
upcast_sound [in Stareat]
upcast_decreases_measure [in Stareat]
upcast_e'_to_upcast_e [in Kernel]
upcast_e_measure_decrease [in Step]
upcast_gives_prefix [in Step]
upcast_strengthening [in Step]
upcast_e_to_upcast [in Step]
upcast_e_preserves_lc [in Step]
upcast_e_preserves_wf [in Step]

W

weaken_subty_gen [in StructuralProperties]
weaken_typing_gen [in StructuralProperties]
weaken_subtykn [in Kernel]
weaken_subtykn_gen [in Kernel]
wf_fv_is_dom [in Misc]
wf_var_in [in Misc]
wf_uniq [in Misc]
wf_deapp [in Misc]
wf_decons [in Misc]
wf_search_lookup [in Step]
wf_search_wf_ge_1 [in Step]
wf_open_shift [in Step]
wf_search_impl_avar_f_eq [in Step]
wf_lookup_lt [in Step]
wf_search_weaken [in Step]
wf_search_fv_weaken [in Step]

Constructor Index

A

avar_f [in VarDef]
avar_b [in VarDef]

B

bs'_bnd [in StrongKernel]
bs'_all [in StrongKernel]
bs'_sel_right [in StrongKernel]
bs'_sel_left [in StrongKernel]
bs'_sel_refl [in StrongKernel]
bs'_top [in StrongKernel]
bs'_bot [in StrongKernel]
bt_bnd [in Stareat]
bt_all [in Stareat]
bt_sel_right [in Stareat]
bt_sel_left [in Stareat]
bt_sel_refl [in Stareat]
bt_top [in Stareat]
bt_bot [in Stareat]

D

dce_bnd [in Step]
dce_top [in Step]
dce_bot [in Step]
dc_bnd [in Stareat]
dc_top [in Stareat]
dc_bot [in Stareat]
de_bnd [in Kernel]
de_top [in Kernel]
de_bot [in Kernel]

E

exp_bnd [in Step]
exp_bot [in Step]
exp_top [in Step]
exp_stop [in Step]
ex_bnd [in Step]
ex_bot [in Step]
ex_top [in Step]
ex_stop [in Step]

L

lc_val_lam [in Definitions]
lc_val_bnd [in Definitions]
lc_trm_let [in Definitions]
lc_trm_app [in Definitions]
lc_trm_val [in Definitions]
lc_trm_var [in Definitions]
lc_typ_bnd [in Definitions]
lc_typ_all [in Definitions]
lc_typ_sel [in Definitions]
lc_typ_bot [in Definitions]
lc_typ_top [in Definitions]
lc_af [in Definitions]
lc_ab [in Definitions]
lc_cons [in Step]
lc_nil [in Step]

O

os_keep [in OpeSub]
os_drop [in OpeSub]
os_nil [in OpeSub]

R

rt_bnd [in Stareat]
rt_bot [in Stareat]
rt_top [in Stareat]
rt_stop [in Stareat]
rv_bnd [in Stareat]
rv_bot [in Stareat]
rv_top [in Stareat]
rv_stop [in Stareat]

S

sa_bnd [in Stareat]
sa_all [in Stareat]
sa_sel_right [in Stareat]
sa_sel_left [in Stareat]
sa_sel_refl [in Stareat]
sa_top [in Stareat]
sa_bot [in Stareat]
snf_sel2 [in Kernel]
snf_sel1 [in Kernel]
snf_all [in Kernel]
snf_bnd [in Kernel]
snf_bot [in Kernel]
snf_top [in Kernel]
snf_vrefl [in Kernel]
snf'_sel2 [in Kernel]
snf'_sel1 [in Kernel]
snf'_all [in Kernel]
snf'_bnd [in Kernel]
snf'_bot [in Kernel]
snf'_top [in Kernel]
snf'_refl [in Kernel]
ssk_sel2 [in StrongKernel]
ssk_sel1 [in StrongKernel]
ssk_all [in StrongKernel]
ssk_bnd [in StrongKernel]
ssk_bot [in StrongKernel]
ssk_top [in StrongKernel]
ssk_refl [in StrongKernel]
ssk'_sel2 [in StrongKernel]
ssk'_sel1 [in StrongKernel]
ssk'_all [in StrongKernel]
ssk'_bnd [in StrongKernel]
ssk'_bot [in StrongKernel]
ssk'_top [in StrongKernel]
ssk'_refl [in StrongKernel]
sst_all [in Step]
sst_bnd [in Step]
sst_sel_right [in Step]
sst_sel_left [in Step]
sst_sel_refl [in Step]
sst_bot [in Step]
sst_top [in Step]
ss_all [in Step]
ss_bnd [in Step]
ss_sel_right [in Step]
ss_sel_left [in Step]
ss_sel_refl [in Step]
ss_bot [in Step]
ss_top [in Step]
ss'_all [in Kernel]
ss'_bnd [in Kernel]
ss'_sel_right [in Kernel]
ss'_sel_left [in Kernel]
ss'_sel_refl [in Kernel]
ss'_bot [in Kernel]
ss'_top [in Kernel]
st_sel2 [in Definitions]
st_sel1 [in Definitions]
st_all [in Definitions]
st_bnd [in Definitions]
st_trans [in Definitions]
st_bot [in Definitions]
st_top [in Definitions]
st_refl [in Definitions]
subenv_grow [in StructuralProperties]
subenv_empty [in StructuralProperties]

T

trm_let [in Definitions]
trm_app [in Definitions]
trm_val [in Definitions]
trm_var [in Definitions]
typ_bnd [in Definitions]
typ_all [in Definitions]
typ_sel [in Definitions]
typ_bot [in Definitions]
typ_top [in Definitions]
ty_sub [in Definitions]
ty_let [in Definitions]
ty_app [in Definitions]
ty_lam [in Definitions]
ty_bnd [in Definitions]
ty_var [in Definitions]

U

uce_bnd [in Step]
uce_bot [in Step]
uce_top [in Step]
uc_bnd [in Stareat]
uc_bot [in Stareat]
uc_top [in Stareat]
ue_bnd [in Kernel]
ue_bot [in Kernel]
ue_top [in Kernel]

V

val_lam [in Definitions]
val_bnd [in Definitions]

W

wf_cons [in Misc]
wf_nil [in Misc]

Inductive Index

A

avar [in VarDef]

D

downcast [in Stareat]
downcast_e' [in Kernel]
downcast_e [in Step]

E

exposure [in Step]
exposure' [in Step]

I

incr_lc [in Step]

L

lc_val_at [in Definitions]
lc_trm_at [in Definitions]
lc_typ_at [in Definitions]
lc_avar_at [in Definitions]

O

ope_sub [in OpeSub]

R

revealing [in Stareat]
revealing_termination [in Stareat]

S

stareat [in Stareat]
stareat_termination [in Stareat]
stareat' [in StrongKernel]
stp_subty' [in Kernel]
stp_subty_termination [in Step]
stp_subty [in Step]
subenv [in StructuralProperties]
subty [in Definitions]
subtykn [in Kernel]
subtykn' [in Kernel]
subtysk [in StrongKernel]
subtysk' [in StrongKernel]

T

trm [in Definitions]
typ [in Definitions]
typing [in Definitions]

U

upcast [in Stareat]
upcast_e' [in Kernel]
upcast_e [in Step]

V

val [in Definitions]

W

wf_env [in Misc]

Section Index

A

Algorithmic [in Step]

B

BiSubtyProperties [in Stareat]
BisubtyStronger [in Step]

C

ClosingDefinitions [in Definitions]

D

DowncastProperties [in Stareat]

E

EquivalentRepr [in Step]

F

FreeVariables [in Definitions]
FvClose [in OperationProperties]
FvOpen [in OperationProperties]

L

LcOpenClosingProperties [in OperationProperties]
LocalClosure [in Definitions]

M

MeasuresAndFacts [in Step]

O

OpenFreshInj [in OperationProperties]
OpeningDefinitions [in Definitions]
OpeProperties [in OpeSub]

P

Predicates [in Misc]

R

RevealingProperties [in Stareat]
RevealingSubsumesExposure [in Step]

S

StructuralProperties [in StructuralProperties]
SubstFresh [in OperationProperties]
SubstFvarProps [in OperationProperties]
SubstIntro [in OperationProperties]
Substitutions [in Definitions]
SubstOpenComm [in OperationProperties]

T

Termination [in Stareat]

U

UpcastProperties [in Stareat]

Instance Index

C

CloseAvar [in Definitions]
CloseTrm [in Definitions]
CloseTyp [in Definitions]
CloseVal [in Definitions]

E

EqAvar [in VarDef]
EqDecTyp [in Definitions]

F

FvAvar [in Definitions]
FvDenv [in Step]
FvEnv [in Definitions]
FvTrm [in Definitions]
FvTyp [in Definitions]
FvVal [in Definitions]

L

LcAvar [in Definitions]
LcTrm [in Definitions]
LcTyp [in Definitions]
LcVal [in Definitions]

O

OpenAvar [in Definitions]
OpenTrm [in Definitions]
OpenTyp [in Definitions]
OpenVal [in Definitions]

S

SubstAvar [in Definitions]
SubstiEnv [in StructuralProperties]
SubstTrm [in Definitions]
SubstTyp [in Definitions]
SubstVal [in Definitions]

Abbreviation Index

C

close_lc [in OperationProperties]

D

denv [in Step]

E

env [in Definitions]

F

fresh_inj [in OperationProperties]
fv_add_close [in OperationProperties]
fv_close [in OperationProperties]
fv_close_self [in OperationProperties]
fv_open [in OperationProperties]

L

lc_relax [in OperationProperties]

N

narrowing [in StructuralProperties]

O

open_left_inv [in OperationProperties]
open_lc_inv [in OperationProperties]
open_lc_le [in OperationProperties]
open_lc [in OperationProperties]

S

subst_intro [in OperationProperties]
subst_open_comm [in OperationProperties]
subst_fresh [in OperationProperties]

Definition Index

B

bnd_layer [in Kernel]
bsubtyp [in Stareat]

C

close_rec_val [in Definitions]
close_rec_trm [in Definitions]
close_rec_typ [in Definitions]
close_rec_avar [in Definitions]

D

denv_measure [in Step]
denv_fv [in Step]
downcast_f_dep [in Stareat]
downcast_f_u [in Stareat]
downcast_func [in Stareat]

E

env_measure [in Misc]
eq_typ_sel [in Stareat]

F

fv_val [in Definitions]
fv_trm [in Definitions]
fv_typ [in Definitions]
fv_avar [in Definitions]
fv_values [in VarDef]

I

is_bnd_dec [in Misc]
is_bnd [in Misc]
is_all_dec [in Misc]
is_all [in Misc]
is_sel_dec [in Misc]
is_sel [in Misc]
is_bot_dec [in Misc]
is_bot [in Misc]
is_top_dec [in Misc]
is_top [in Misc]

O

open_rec_val [in Definitions]
open_rec_trm [in Definitions]
open_rec_typ [in Definitions]
open_rec_avar [in Definitions]
open_rec_D [in Step]

R

revealing_terminates [in Stareat]
reveal_func [in Stareat]

S

stareat_terminates [in Stareat]
stareat_refl [in Stareat]
stp_subty'_refl [in Kernel]
stp_subty_terminates [in Step]
subst_fvar [in OperationProperties]
subst_val [in Definitions]
subst_trm [in Definitions]
subst_typ [in Definitions]
subst_avar [in Definitions]
subst_env [in StructuralProperties]
subtykn_refl [in Kernel]
subtykn'_conversions [in Kernel]
subtysk_refl [in StrongKernel]
subtysk'_conversions [in StrongKernel]
subty_measure [in Stareat]

T

total [in Misc]
trm_struct_measure [in Misc]
typ_struct_measure [in Misc]

U

upcast_f_dep [in Stareat]
upcast_f_u [in Stareat]
upcast_func [in Stareat]

V

val_struct_measure [in Misc]

W

weaken_subty [in StructuralProperties]
weaken_typing [in StructuralProperties]
wf_open_shift_gen [in Step]
wf_search_weaken_gen [in Step]
wf_weaken_measure [in Step]
wf_search_avar [in Step]
wf_search_bv [in Step]
wf_search_fv [in Step]
wf_search [in Step]
wf_search_impl [in Step]
wf_measure [in Step]

Global Index

G

H

J

Q

X

Y

Z

_

(573 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(18 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

P

Q

R

T

U

V

W

X

Y

Z

_

other

(11 entries)

Library Index

A

B

C

E

F

G

H

I

J

L

N

P

Q

R

T

U

W

X

Y

Z

_

other

(10 entries)

Lemma Index

G

H

I

J

K

M

Q

V

X

Y

Z

_

other

(211 entries)

Constructor Index

C

F

G

H

I

J

K

M

N

P

Q

X

Y

Z

_

other

(153 entries)

Inductive Index

B

C

F

G

H

J

K

M

N

P

Q

X

Y

Z

_

other

(34 entries)

Section Index

G

H

I

J

K

N

Q

V

W

X

Y

Z

_

other

(26 entries)

Instance Index

A

B

D

G

H

I

J

K

M

N

P

Q

R

T

U

V

W

X

Y

Z

_

other

(25 entries)

Abbreviation Index

A

B

G

H

I

J

K

M

P

Q

R

T

U

V

W

X

Y

Z

_

other

(17 entries)

Definition Index

A

G

H

J

K

L

M

N

P

Q

X

Y

Z

_

other

(68 entries)