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 (292 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 (2 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (6 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 (175 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (35 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 (13 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 (5 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (55 entries)

Global Index

A

abs [constructor, in Stlc.Definitions]
aeq [inductive, in Stlc.Nominal]
aeq_nom_to_exp [lemma, in Stlc.Connect]
aeq_app [constructor, in Stlc.Nominal]
aeq_abs_diff [constructor, in Stlc.Nominal]
aeq_abs_same [constructor, in Stlc.Nominal]
aeq_var [constructor, in Stlc.Nominal]
aeq1 [definition, in Stlc.Nominal]
app [constructor, in Stlc.Definitions]
append_assoc_demo [lemma, in Stlc.Lec2]
apply_stack_fresh_eq [lemma, in Stlc.Connect]
apply_heap_get [lemma, in Stlc.Connect]
apply_stack_cong [lemma, in Stlc.Connect]
apply_heap_open [lemma, in Stlc.Connect]
apply_heap_app [lemma, in Stlc.Connect]
apply_heap_abs [lemma, in Stlc.Connect]
apply_heap_lc [lemma, in Stlc.Connect]
apply_stack [definition, in Stlc.Connect]
apply_heap [definition, in Stlc.Connect]


B

binds_demo [lemma, in Stlc.Lec2]
body_exp_wrt_exp [definition, in Stlc.Lemmas]


C

close_exp_wrt_exp_freshen [lemma, in Stlc.Connect]
close_exp_wrt_exp_lc_exp [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_inj [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj_mutual [lemma, in Stlc.Lemmas]
close_exp_wrt_exp [definition, in Stlc.Lemmas]
close_exp_wrt_exp_rec [definition, in Stlc.Lemmas]
cofinite_exists [lemma, in Stlc.Lec2]
combine [lemma, in Stlc.Connect]
configuration [definition, in Stlc.Nominal]
conf1 [definition, in Stlc.Connect]
Connect [library]
ctx [definition, in Stlc.Definitions]


D

decode [definition, in Stlc.Connect]
decode_lc [lemma, in Stlc.Connect]
decode1 [definition, in Stlc.Connect]
Definitions [library]
degree_exp_wrt_exp_of_lc_exp [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_of_lc_exp_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_O [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_S [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_S_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_mutind [definition, in Stlc.Lemmas]
degree_exp_wrt_exp_ind' [definition, in Stlc.Lemmas]
degree_wrt_exp_app [constructor, in Stlc.Lemmas]
degree_wrt_exp_var_b [constructor, in Stlc.Lemmas]
degree_wrt_exp_var_f [constructor, in Stlc.Lemmas]
degree_wrt_exp_abs [constructor, in Stlc.Lemmas]
degree_exp_wrt_exp [inductive, in Stlc.Lemmas]
demo_lc [lemma, in Stlc.Lec1]
demo_open [lemma, in Stlc.Lec1]
demo_subst1 [definition, in Stlc.Lec1]
demo_rep3 [definition, in Stlc.Lec1]
demo_rep2 [definition, in Stlc.Lec1]
demo_rep1 [definition, in Stlc.Lec1]
demo_rep2 [definition, in Stlc.Nominal]
demo_rep1 [definition, in Stlc.Nominal]
dom_demo [lemma, in Stlc.Lec2]
Done [constructor, in Stlc.Nominal]


E

Error [constructor, in Stlc.Nominal]
exists_cofinite [lemma, in Stlc.Lec2]
exp [inductive, in Stlc.Definitions]
exp_mutrec [definition, in Stlc.Lemmas]
exp_rec' [definition, in Stlc.Lemmas]
exp_mutind [definition, in Stlc.Lemmas]
exp_ind' [definition, in Stlc.Lemmas]


F

frame [inductive, in Stlc.Nominal]
fsetdec_demo [lemma, in Stlc.Lec1]
fv_exp_open_exp_wrt_exp_upper [lemma, in Stlc.Lec1]
fv_exp_subst_exp_upper [lemma, in Stlc.Lec1]
fv_exp_subst_exp_fresh [lemma, in Stlc.Lec1]
fv_exp_subst_exp_notin [lemma, in Stlc.Lec1]
fv_stack [definition, in Stlc.Connect]
fv_nom_fv_exp_eq [lemma, in Stlc.Connect]
fv_in_dom [lemma, in Stlc.Lec2]
fv_nom_swap [lemma, in Stlc.Nominal]
fv_nom_rep1 [definition, in Stlc.Nominal]
fv_nom [definition, in Stlc.Nominal]
fv_exp [definition, in Stlc.Definitions]
fv_exp_subst_exp_upper [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_upper_mutual [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_notin [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_notin_mutual [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_lower [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_lower_mutual [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_fresh [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_fresh_mutual [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_upper [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper_mutual [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_lower [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower_mutual [lemma, in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]


H

heap [definition, in Stlc.Nominal]


I

initconf [definition, in Stlc.Nominal]
in_fv_nom_equivariance [lemma, in Stlc.Nominal]
isVal [definition, in Stlc.Nominal]
is_value [definition, in Stlc.Definitions]


L

lc_abs_exists [lemma, in Stlc.Lec1]
lc_app [constructor, in Stlc.Definitions]
lc_abs [constructor, in Stlc.Definitions]
lc_var_f [constructor, in Stlc.Definitions]
lc_exp [inductive, in Stlc.Definitions]
lc_body_abs_1 [lemma, in Stlc.Lemmas]
lc_body_exp_wrt_exp [lemma, in Stlc.Lemmas]
lc_abs_exists [lemma, in Stlc.Lemmas]
lc_exp_of_degree [lemma, in Stlc.Lemmas]
lc_exp_of_degree_size_mutual [lemma, in Stlc.Lemmas]
lc_exp_mutind [definition, in Stlc.Lemmas]
lc_exp_ind' [definition, in Stlc.Lemmas]
Lec1 [library]
Lec2 [library]
Lemmas [library]


M

machine_is_scoped [lemma, in Stlc.Connect]
machine_step [definition, in Stlc.Nominal]


N

Nominal [library]
nom_to_exp_eq_aeq [lemma, in Stlc.Connect]
nom_to_exp_lc [lemma, in Stlc.Connect]
nom_to_exp [definition, in Stlc.Connect]
notin_fv_nom_equivariance [lemma, in Stlc.Nominal]
n_app2 [constructor, in Stlc.Nominal]
n_app [constructor, in Stlc.Nominal]
n_abs [constructor, in Stlc.Nominal]
n_var [constructor, in Stlc.Nominal]
n_exp [inductive, in Stlc.Nominal]


O

open_exp_wrt_exp [definition, in Stlc.Definitions]
open_exp_wrt_exp_rec [definition, in Stlc.Definitions]
open_exp_wrt_exp_lc_exp [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_degree_exp_wrt_exp [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_inj [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj_mutual [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]


P

preservation [lemma, in Stlc.Lec2]
progress [lemma, in Stlc.Lec2]


S

scoped_conf_witness [constructor, in Stlc.Connect]
scoped_conf [inductive, in Stlc.Connect]
scoped_cons [constructor, in Stlc.Connect]
scoped_nil [constructor, in Stlc.Connect]
scoped_heap [inductive, in Stlc.Connect]
shuffle_swap [lemma, in Stlc.Nominal]
simpl_env_demo [lemma, in Stlc.Lec2]
simulate_error [lemma, in Stlc.Connect]
simulate_done [lemma, in Stlc.Connect]
simulate_step [lemma, in Stlc.Connect]
size [definition, in Stlc.Nominal]
size_exp_open_exp_wrt_exp_var [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var_mutual [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
size_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
size_exp_min [lemma, in Stlc.Lemmas]
size_exp_min_mutual [lemma, in Stlc.Lemmas]
size_typ_min [lemma, in Stlc.Lemmas]
size_typ_min_mutual [lemma, in Stlc.Lemmas]
size_exp [definition, in Stlc.Lemmas]
size_typ [definition, in Stlc.Lemmas]
stack [abbreviation, in Stlc.Nominal]
Step [inductive, in Stlc.Nominal]
step [inductive, in Stlc.Definitions]
step_lc_exp2 [lemma, in Stlc.Lec1]
step_lc_exp1 [lemma, in Stlc.Lec1]
step_app [constructor, in Stlc.Definitions]
step_beta [constructor, in Stlc.Definitions]
StlcNotations [module, in Stlc.Definitions]
StlcNotations.open [abbreviation, in Stlc.Definitions]
_ ^ _ (exp_scope) [notation, in Stlc.Definitions]
[ _ ~> _ ] _ (exp_scope) [notation, in Stlc.Definitions]
subst [definition, in Stlc.Nominal]
subst_exp_lc_exp [lemma, in Stlc.Lec1]
subst_lc0 [lemma, in Stlc.Lec1]
subst_exp_intro [lemma, in Stlc.Lec1]
subst_var [lemma, in Stlc.Lec1]
subst_exp_open_exp_wrt_exp [lemma, in Stlc.Lec1]
subst_exp_fresh_same [lemma, in Stlc.Lec1]
subst_exp_fresh_eq [lemma, in Stlc.Lec1]
subst_same [lemma, in Stlc.Lec1]
subst_neq_var [lemma, in Stlc.Lec1]
subst_eq_var [lemma, in Stlc.Lec1]
subst_abs [lemma, in Stlc.Nominal]
subst_app [lemma, in Stlc.Nominal]
subst_neq_var [lemma, in Stlc.Nominal]
subst_eq_var [lemma, in Stlc.Nominal]
subst_size [lemma, in Stlc.Nominal]
subst_rec [definition, in Stlc.Nominal]
subst_exp [definition, in Stlc.Definitions]
subst_exp_intro [lemma, in Stlc.Lemmas]
subst_exp_intro_rec [lemma, in Stlc.Lemmas]
subst_exp_abs [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
subst_exp_subst_exp [lemma, in Stlc.Lemmas]
subst_exp_subst_exp_mutual [lemma, in Stlc.Lemmas]
subst_exp_spec [lemma, in Stlc.Lemmas]
subst_exp_spec_rec [lemma, in Stlc.Lemmas]
subst_exp_spec_rec_mutual [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_var [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
subst_exp_lc_exp [lemma, in Stlc.Lemmas]
subst_exp_fresh [lemma, in Stlc.Lemmas]
subst_exp_fresh_mutual [lemma, in Stlc.Lemmas]
subst_exp_fresh_same [lemma, in Stlc.Lemmas]
subst_exp_fresh_same_mutual [lemma, in Stlc.Lemmas]
subst_exp_fresh_eq [lemma, in Stlc.Lemmas]
subst_exp_fresh_eq_mutual [lemma, in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp_mutual [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
swap [definition, in Stlc.Nominal]
swap_spec [lemma, in Stlc.Connect]
swap_spec_aux [lemma, in Stlc.Connect]
swap_size_eq [lemma, in Stlc.Nominal]
swap_equivariance [lemma, in Stlc.Nominal]
swap_var_equivariance [lemma, in Stlc.Nominal]
swap_involutive [lemma, in Stlc.Nominal]
swap_symmetric [lemma, in Stlc.Nominal]
swap_id [lemma, in Stlc.Nominal]
swap_var [definition, in Stlc.Nominal]
swap1 [definition, in Stlc.Nominal]
swap2 [definition, in Stlc.Nominal]
swap3 [definition, in Stlc.Nominal]


T

TakeStep [constructor, in Stlc.Nominal]
typ [inductive, in Stlc.Definitions]
typing [inductive, in Stlc.Definitions]
typing_to_lc_exp [lemma, in Stlc.Lec1]
typing_abs_exists [lemma, in Stlc.Lec2]
typing_rename [lemma, in Stlc.Lec2]
typing_uniq [lemma, in Stlc.Lec2]
typing_subst_simple [lemma, in Stlc.Lec2]
typing_subst [lemma, in Stlc.Lec2]
typing_subst_var_case [lemma, in Stlc.Lec2]
typing_weakening [lemma, in Stlc.Lec2]
typing_weakening_strengthened [lemma, in Stlc.Lec2]
typing_weakening_strengthened_1 [lemma, in Stlc.Lec2]
typing_weakening_strengthened_0 [lemma, in Stlc.Lec2]
typing_weakening_0 [lemma, in Stlc.Lec2]
typing_e_app [constructor, in Stlc.Lec2]
typing_e_abs [constructor, in Stlc.Lec2]
typing_e_var [constructor, in Stlc.Lec2]
typing_e [inductive, in Stlc.Lec2]
typing_app [constructor, in Stlc.Definitions]
typing_abs [constructor, in Stlc.Definitions]
typing_var [constructor, in Stlc.Definitions]
typ_arrow [constructor, in Stlc.Definitions]
typ_base [constructor, in Stlc.Definitions]
typ_mutrec [definition, in Stlc.Lemmas]
typ_rec' [definition, in Stlc.Lemmas]
typ_mutind [definition, in Stlc.Lemmas]
typ_ind' [definition, in Stlc.Lemmas]


U

uniq_demo [lemma, in Stlc.Lec2]


V

values_are_done [lemma, in Stlc.Nominal]
var_f [constructor, in Stlc.Definitions]
var_b [constructor, in Stlc.Definitions]


X

X [definition, in Stlc.Lec1]
X [abbreviation, in Stlc.Nominal]


Y

Y [definition, in Stlc.Lec1]
Y [abbreviation, in Stlc.Nominal]


Z

Z [definition, in Stlc.Lec1]
Z [abbreviation, in Stlc.Nominal]



Notation Index

S

_ ^ _ (exp_scope) [in Stlc.Definitions]
[ _ ~> _ ] _ (exp_scope) [in Stlc.Definitions]



Module Index

S

StlcNotations [in Stlc.Definitions]



Library Index

C

Connect


D

Definitions


L

Lec1
Lec2
Lemmas


N

Nominal



Lemma Index

A

aeq_nom_to_exp [in Stlc.Connect]
append_assoc_demo [in Stlc.Lec2]
apply_stack_fresh_eq [in Stlc.Connect]
apply_heap_get [in Stlc.Connect]
apply_stack_cong [in Stlc.Connect]
apply_heap_open [in Stlc.Connect]
apply_heap_app [in Stlc.Connect]
apply_heap_abs [in Stlc.Connect]
apply_heap_lc [in Stlc.Connect]


B

binds_demo [in Stlc.Lec2]


C

close_exp_wrt_exp_freshen [in Stlc.Connect]
close_exp_wrt_exp_lc_exp [in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp [in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [in Stlc.Lemmas]
close_exp_wrt_exp_open_exp_wrt_exp [in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
close_exp_wrt_exp_inj [in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj [in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj_mutual [in Stlc.Lemmas]
cofinite_exists [in Stlc.Lec2]
combine [in Stlc.Connect]


D

decode_lc [in Stlc.Connect]
degree_exp_wrt_exp_of_lc_exp [in Stlc.Lemmas]
degree_exp_wrt_exp_of_lc_exp_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_O [in Stlc.Lemmas]
degree_exp_wrt_exp_S [in Stlc.Lemmas]
degree_exp_wrt_exp_S_mutual [in Stlc.Lemmas]
demo_lc [in Stlc.Lec1]
demo_open [in Stlc.Lec1]
dom_demo [in Stlc.Lec2]


E

exists_cofinite [in Stlc.Lec2]


F

fsetdec_demo [in Stlc.Lec1]
fv_exp_open_exp_wrt_exp_upper [in Stlc.Lec1]
fv_exp_subst_exp_upper [in Stlc.Lec1]
fv_exp_subst_exp_fresh [in Stlc.Lec1]
fv_exp_subst_exp_notin [in Stlc.Lec1]
fv_nom_fv_exp_eq [in Stlc.Connect]
fv_in_dom [in Stlc.Lec2]
fv_nom_swap [in Stlc.Nominal]
fv_exp_subst_exp_upper [in Stlc.Lemmas]
fv_exp_subst_exp_upper_mutual [in Stlc.Lemmas]
fv_exp_subst_exp_notin [in Stlc.Lemmas]
fv_exp_subst_exp_notin_mutual [in Stlc.Lemmas]
fv_exp_subst_exp_lower [in Stlc.Lemmas]
fv_exp_subst_exp_lower_mutual [in Stlc.Lemmas]
fv_exp_subst_exp_fresh [in Stlc.Lemmas]
fv_exp_subst_exp_fresh_mutual [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_upper [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper_mutual [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_lower [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower_mutual [in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp [in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]


I

in_fv_nom_equivariance [in Stlc.Nominal]


L

lc_abs_exists [in Stlc.Lec1]
lc_body_abs_1 [in Stlc.Lemmas]
lc_body_exp_wrt_exp [in Stlc.Lemmas]
lc_abs_exists [in Stlc.Lemmas]
lc_exp_of_degree [in Stlc.Lemmas]
lc_exp_of_degree_size_mutual [in Stlc.Lemmas]


M

machine_is_scoped [in Stlc.Connect]


N

nom_to_exp_eq_aeq [in Stlc.Connect]
nom_to_exp_lc [in Stlc.Connect]
notin_fv_nom_equivariance [in Stlc.Nominal]


O

open_exp_wrt_exp_lc_exp [in Stlc.Lemmas]
open_exp_wrt_exp_rec_degree_exp_wrt_exp [in Stlc.Lemmas]
open_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [in Stlc.Lemmas]
open_exp_wrt_exp_inj [in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj [in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj_mutual [in Stlc.Lemmas]
open_exp_wrt_exp_close_exp_wrt_exp [in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec [in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]


P

preservation [in Stlc.Lec2]
progress [in Stlc.Lec2]


S

shuffle_swap [in Stlc.Nominal]
simpl_env_demo [in Stlc.Lec2]
simulate_error [in Stlc.Connect]
simulate_done [in Stlc.Connect]
simulate_step [in Stlc.Connect]
size_exp_open_exp_wrt_exp_var [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var_mutual [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
size_exp_close_exp_wrt_exp [in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
size_exp_min [in Stlc.Lemmas]
size_exp_min_mutual [in Stlc.Lemmas]
size_typ_min [in Stlc.Lemmas]
size_typ_min_mutual [in Stlc.Lemmas]
step_lc_exp2 [in Stlc.Lec1]
step_lc_exp1 [in Stlc.Lec1]
subst_exp_lc_exp [in Stlc.Lec1]
subst_lc0 [in Stlc.Lec1]
subst_exp_intro [in Stlc.Lec1]
subst_var [in Stlc.Lec1]
subst_exp_open_exp_wrt_exp [in Stlc.Lec1]
subst_exp_fresh_same [in Stlc.Lec1]
subst_exp_fresh_eq [in Stlc.Lec1]
subst_same [in Stlc.Lec1]
subst_neq_var [in Stlc.Lec1]
subst_eq_var [in Stlc.Lec1]
subst_abs [in Stlc.Nominal]
subst_app [in Stlc.Nominal]
subst_neq_var [in Stlc.Nominal]
subst_eq_var [in Stlc.Nominal]
subst_size [in Stlc.Nominal]
subst_exp_intro [in Stlc.Lemmas]
subst_exp_intro_rec [in Stlc.Lemmas]
subst_exp_abs [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_open_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
subst_exp_subst_exp [in Stlc.Lemmas]
subst_exp_subst_exp_mutual [in Stlc.Lemmas]
subst_exp_spec [in Stlc.Lemmas]
subst_exp_spec_rec [in Stlc.Lemmas]
subst_exp_spec_rec_mutual [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_var [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
subst_exp_lc_exp [in Stlc.Lemmas]
subst_exp_fresh [in Stlc.Lemmas]
subst_exp_fresh_mutual [in Stlc.Lemmas]
subst_exp_fresh_same [in Stlc.Lemmas]
subst_exp_fresh_same_mutual [in Stlc.Lemmas]
subst_exp_fresh_eq [in Stlc.Lemmas]
subst_exp_fresh_eq_mutual [in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp_mutual [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
swap_spec [in Stlc.Connect]
swap_spec_aux [in Stlc.Connect]
swap_size_eq [in Stlc.Nominal]
swap_equivariance [in Stlc.Nominal]
swap_var_equivariance [in Stlc.Nominal]
swap_involutive [in Stlc.Nominal]
swap_symmetric [in Stlc.Nominal]
swap_id [in Stlc.Nominal]


T

typing_to_lc_exp [in Stlc.Lec1]
typing_abs_exists [in Stlc.Lec2]
typing_rename [in Stlc.Lec2]
typing_uniq [in Stlc.Lec2]
typing_subst_simple [in Stlc.Lec2]
typing_subst [in Stlc.Lec2]
typing_subst_var_case [in Stlc.Lec2]
typing_weakening [in Stlc.Lec2]
typing_weakening_strengthened [in Stlc.Lec2]
typing_weakening_strengthened_1 [in Stlc.Lec2]
typing_weakening_strengthened_0 [in Stlc.Lec2]
typing_weakening_0 [in Stlc.Lec2]


U

uniq_demo [in Stlc.Lec2]


V

values_are_done [in Stlc.Nominal]



Constructor Index

A

abs [in Stlc.Definitions]
aeq_app [in Stlc.Nominal]
aeq_abs_diff [in Stlc.Nominal]
aeq_abs_same [in Stlc.Nominal]
aeq_var [in Stlc.Nominal]
app [in Stlc.Definitions]


D

degree_wrt_exp_app [in Stlc.Lemmas]
degree_wrt_exp_var_b [in Stlc.Lemmas]
degree_wrt_exp_var_f [in Stlc.Lemmas]
degree_wrt_exp_abs [in Stlc.Lemmas]
Done [in Stlc.Nominal]


E

Error [in Stlc.Nominal]


L

lc_app [in Stlc.Definitions]
lc_abs [in Stlc.Definitions]
lc_var_f [in Stlc.Definitions]


N

n_app2 [in Stlc.Nominal]
n_app [in Stlc.Nominal]
n_abs [in Stlc.Nominal]
n_var [in Stlc.Nominal]


S

scoped_conf_witness [in Stlc.Connect]
scoped_cons [in Stlc.Connect]
scoped_nil [in Stlc.Connect]
step_app [in Stlc.Definitions]
step_beta [in Stlc.Definitions]


T

TakeStep [in Stlc.Nominal]
typing_e_app [in Stlc.Lec2]
typing_e_abs [in Stlc.Lec2]
typing_e_var [in Stlc.Lec2]
typing_app [in Stlc.Definitions]
typing_abs [in Stlc.Definitions]
typing_var [in Stlc.Definitions]
typ_arrow [in Stlc.Definitions]
typ_base [in Stlc.Definitions]


V

var_f [in Stlc.Definitions]
var_b [in Stlc.Definitions]



Inductive Index

A

aeq [in Stlc.Nominal]


D

degree_exp_wrt_exp [in Stlc.Lemmas]


E

exp [in Stlc.Definitions]


F

frame [in Stlc.Nominal]


L

lc_exp [in Stlc.Definitions]


N

n_exp [in Stlc.Nominal]


S

scoped_conf [in Stlc.Connect]
scoped_heap [in Stlc.Connect]
Step [in Stlc.Nominal]
step [in Stlc.Definitions]


T

typ [in Stlc.Definitions]
typing [in Stlc.Definitions]
typing_e [in Stlc.Lec2]



Abbreviation Index

S

stack [in Stlc.Nominal]
StlcNotations.open [in Stlc.Definitions]


X

X [in Stlc.Nominal]


Y

Y [in Stlc.Nominal]


Z

Z [in Stlc.Nominal]



Definition Index

A

aeq1 [in Stlc.Nominal]
apply_stack [in Stlc.Connect]
apply_heap [in Stlc.Connect]


B

body_exp_wrt_exp [in Stlc.Lemmas]


C

close_exp_wrt_exp [in Stlc.Lemmas]
close_exp_wrt_exp_rec [in Stlc.Lemmas]
configuration [in Stlc.Nominal]
conf1 [in Stlc.Connect]
ctx [in Stlc.Definitions]


D

decode [in Stlc.Connect]
decode1 [in Stlc.Connect]
degree_exp_wrt_exp_mutind [in Stlc.Lemmas]
degree_exp_wrt_exp_ind' [in Stlc.Lemmas]
demo_subst1 [in Stlc.Lec1]
demo_rep3 [in Stlc.Lec1]
demo_rep2 [in Stlc.Lec1]
demo_rep1 [in Stlc.Lec1]
demo_rep2 [in Stlc.Nominal]
demo_rep1 [in Stlc.Nominal]


E

exp_mutrec [in Stlc.Lemmas]
exp_rec' [in Stlc.Lemmas]
exp_mutind [in Stlc.Lemmas]
exp_ind' [in Stlc.Lemmas]


F

fv_stack [in Stlc.Connect]
fv_nom_rep1 [in Stlc.Nominal]
fv_nom [in Stlc.Nominal]
fv_exp [in Stlc.Definitions]


H

heap [in Stlc.Nominal]


I

initconf [in Stlc.Nominal]
isVal [in Stlc.Nominal]
is_value [in Stlc.Definitions]


L

lc_exp_mutind [in Stlc.Lemmas]
lc_exp_ind' [in Stlc.Lemmas]


M

machine_step [in Stlc.Nominal]


N

nom_to_exp [in Stlc.Connect]


O

open_exp_wrt_exp [in Stlc.Definitions]
open_exp_wrt_exp_rec [in Stlc.Definitions]


S

size [in Stlc.Nominal]
size_exp [in Stlc.Lemmas]
size_typ [in Stlc.Lemmas]
subst [in Stlc.Nominal]
subst_rec [in Stlc.Nominal]
subst_exp [in Stlc.Definitions]
swap [in Stlc.Nominal]
swap_var [in Stlc.Nominal]
swap1 [in Stlc.Nominal]
swap2 [in Stlc.Nominal]
swap3 [in Stlc.Nominal]


T

typ_mutrec [in Stlc.Lemmas]
typ_rec' [in Stlc.Lemmas]
typ_mutind [in Stlc.Lemmas]
typ_ind' [in Stlc.Lemmas]


X

X [in Stlc.Lec1]


Y

Y [in Stlc.Lec1]


Z

Z [in Stlc.Lec1]



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 (292 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 (2 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (6 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 (175 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (35 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 (13 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 (5 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (55 entries)

This page has been generated by coqdoc