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 _ (1667 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (93 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 _ (610 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 _ (510 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 _ (114 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 _ (271 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 _ (18 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (51 entries)

Global Index

A

add [axiom, in Lib_MyFSetInterface]
add_1 [axiom, in Lib_MyFSetInterface]
add_2 [axiom, in Lib_MyFSetInterface]
add_3 [axiom, in Lib_MyFSetInterface]
atm [axiom, in STLC_Exn_Definitions]
atm [axiom, in STLC_Ref_Definitions]


B

beta [inductive, in Lambda_Definitions]
beta [inductive, in CoC_Definitions]
beta_abs [constructor, in Lambda_Definitions]
beta_abs1 [constructor, in CoC_Definitions]
beta_abs2 [constructor, in CoC_Definitions]
beta_app1 [constructor, in Lambda_Definitions]
beta_app1 [constructor, in CoC_Definitions]
beta_app2 [constructor, in Lambda_Definitions]
beta_app2 [constructor, in CoC_Definitions]
beta_church_rosser [lemma, in Lambda_ChurchRosser]
beta_prod1 [constructor, in CoC_Definitions]
beta_prod2 [constructor, in CoC_Definitions]
beta_red [constructor, in CoC_Definitions]
beta_red [constructor, in Lambda_Definitions]
beta_red_out [lemma, in CoC_BetaStar]
beta_red_out [lemma, in Lambda_ChurchRosser]
beta_red_rename [lemma, in CoC_BetaStar]
beta_red_rename [lemma, in Lambda_ChurchRosser]
beta_star_abs [lemma, in Lambda_ChurchRosser]
beta_star_abs1 [lemma, in CoC_BetaStar]
beta_star_abs2 [lemma, in CoC_BetaStar]
beta_star_app1 [lemma, in Lambda_ChurchRosser]
beta_star_app1 [lemma, in CoC_BetaStar]
beta_star_app2 [lemma, in CoC_BetaStar]
beta_star_app2 [lemma, in Lambda_ChurchRosser]
beta_star_confluence [lemma, in Lambda_ChurchRosser]
beta_star_prod1 [lemma, in CoC_BetaStar]
beta_star_prod2 [lemma, in CoC_BetaStar]
beta_star_prod_any_inv [lemma, in CoC_Conversion]
beta_star_red_all [lemma, in CoC_BetaStar]
beta_star_red_all [lemma, in Lambda_ChurchRosser]
beta_star_red_in [lemma, in Lambda_ChurchRosser]
beta_star_red_in [lemma, in CoC_BetaStar]
beta_star_red_through [lemma, in Lambda_ChurchRosser]
beta_star_red_through [lemma, in CoC_BetaStar]
beta_star_to_para_iter [lemma, in CoC_ChurchRosser]
beta_star_to_para_iter [lemma, in Lambda_ChurchRosser]
beta_star_type_any_inv [lemma, in CoC_Conversion]
bind [inductive, in Fsub_Definitions]
bind [inductive, in Fsub_Part1A]
binds_typ_dec [lemma, in STLC_Dec_Decidability]
bind_sub [constructor, in Fsub_Part1A]
bind_sub [constructor, in Fsub_Definitions]
bind_typ [constructor, in Fsub_Definitions]
body [definition, in STLC_Dec_Infrastructure]
body [definition, in STLC_Core_WF_Infrastructure]
body [definition, in CoC_Definitions]
body [definition, in STLC_Exn_Infrastructure]
body [definition, in STLC_Core_Infrastructure]
body [definition, in STLC_Core_Light]
body [definition, in Lambda_Definitions]
body [definition, in STLC_Ref_Infrastructure]
bodys [definition, in STLC_Data_Definitions]
bodys [definition, in ML_Definitions]
body_abs2 [lemma, in CoC_Infrastructure]
body_prod2 [lemma, in CoC_Infrastructure]
body_prove [lemma, in CoC_Infrastructure]
body_subst [lemma, in CoC_Infrastructure]
body_to_term_abs [lemma, in STLC_Dec_Infrastructure]
body_to_term_abs [lemma, in STLC_Core_Infrastructure]
body_to_term_abs [lemma, in ML_Core_Infrastructure]
body_to_term_abs [lemma, in STLC_Core_WF_Infrastructure]
body_to_term_abs [lemma, in Lambda_Infrastructure]
body_to_term_abs [lemma, in STLC_Exn_Infrastructure]
body_to_term_abs [lemma, in STLC_Data_Infrastructure]
body_to_term_abs [lemma, in ML_Infrastructure]
body_to_term_abs [lemma, in STLC_Ref_Infrastructure]
body_to_term_fix [lemma, in STLC_Data_Infrastructure]
body_to_term_fix [lemma, in ML_Infrastructure]
body_to_term_let [lemma, in ML_Infrastructure]
body_to_term_let [lemma, in ML_Core_Infrastructure]
body_to_term_match [lemma, in ML_Infrastructure]
body_to_term_match [lemma, in STLC_Data_Infrastructure]


C

canonical_form_abs [lemma, in Fsub_Soundness]
canonical_form_tabs [lemma, in Fsub_Soundness]
cardinal [axiom, in Lib_MyFSetInterface]
cardinal_1 [axiom, in Lib_MyFSetInterface]
choose [axiom, in Lib_MyFSetInterface]
choose_1 [axiom, in Lib_MyFSetInterface]
choose_2 [axiom, in Lib_MyFSetInterface]
church_rosser [definition, in Lambda_Definitions]
church_rosser [definition, in CoC_Definitions]
church_rosser_beta [lemma, in CoC_ChurchRosser]
close_var [definition, in CoC_Infrastructure]
close_var [definition, in Lambda_Infrastructure]
close_var_body [lemma, in CoC_Infrastructure]
close_var_body [lemma, in Lambda_Infrastructure]
close_var_fresh [lemma, in CoC_Infrastructure]
close_var_fresh [lemma, in Lambda_Infrastructure]
close_var_open [lemma, in CoC_Infrastructure]
close_var_open [lemma, in Lambda_Infrastructure]
close_var_rec [definition, in CoC_Infrastructure]
close_var_rec [definition, in Lambda_Infrastructure]
close_var_spec [lemma, in Lambda_Infrastructure]
close_var_spec [lemma, in CoC_Infrastructure]
CoC_BetaStar [library]
CoC_ChurchRosser [library]
CoC_Conversion [library]
CoC_Definitions [library]
CoC_Infrastructure [library]
CoC_Preservation [library]
compare [axiom, in Lib_MyFSetInterface]
conf [definition, in STLC_Ref_Definitions]
conf [definition, in ML_Definitions]
confluence [definition, in CoC_Definitions]
confluence [definition, in Lambda_Definitions]
confluence_beta_star [lemma, in CoC_ChurchRosser]
contains_terms [definition, in CoC_Infrastructure]
conv [definition, in CoC_Definitions]
conv_from_beta_star [lemma, in CoC_Conversion]
conv_from_beta_star_trans [lemma, in CoC_Conversion]
conv_from_open_beta [lemma, in CoC_Conversion]
conv_prod_prod_inv [lemma, in CoC_Conversion]
conv_red_out [lemma, in CoC_Conversion]
conv_type_prod_inv [lemma, in CoC_Conversion]
conv_type_type_inv [lemma, in CoC_Conversion]
ctx [inductive, in STLC_Core_WF_Definitions]
ctx_app_1 [constructor, in STLC_Core_WF_Definitions]
ctx_app_2 [constructor, in STLC_Core_WF_Definitions]
ctx_hole [constructor, in STLC_Core_WF_Definitions]
ctx_of [definition, in STLC_Core_WF_Definitions]
ctx_regular [lemma, in STLC_Core_WF_Infrastructure]


D

diff [axiom, in Lib_MyFSetInterface]
diff_1 [axiom, in Lib_MyFSetInterface]
diff_2 [axiom, in Lib_MyFSetInterface]
diff_3 [axiom, in Lib_MyFSetInterface]


E

E [module, in Lib_MyFSetInterface]
E [module, in Lib_FinSet]
elements [axiom, in Lib_MyFSetInterface]
elements_1 [axiom, in Lib_MyFSetInterface]
elements_2 [axiom, in Lib_MyFSetInterface]
elements_3 [axiom, in Lib_MyFSetInterface]
elim_incl_app [lemma, in Lib_ListFacts]
elim_incl_cons [lemma, in Lib_ListFacts]
elim_not_In_app [lemma, in Lib_ListFacts]
elim_not_In_cons [lemma, in Lib_ListFacts]
empty [axiom, in Lib_MyFSetInterface]
empty_1 [axiom, in Lib_MyFSetInterface]
env [definition, in STLC_Dec_Definitions]
env [definition, in ML_Definitions]
env [definition, in CoC_Definitions]
env [definition, in ML_Core_Definitions]
env [definition, in STLC_Core_Light]
env [definition, in STLC_Data_Definitions]
env [definition, in Fsub_Part1A]
env [definition, in Fsub_Definitions]
env [definition, in STLC_Core_WF_Definitions]
env [definition, in STLC_Core_Definitions]
env [definition, in STLC_Ref_Definitions]
env [definition, in STLC_Exn_Definitions]
Env [module, in Metatheory_Env]
Env.binds [definition, in Metatheory_Env]
Env.binds_concat_fresh [lemma, in Metatheory_Env]
Env.binds_concat_inv [lemma, in Metatheory_Env]
Env.binds_concat_ok [lemma, in Metatheory_Env]
Env.binds_dec [lemma, in Metatheory_Env]
Env.binds_empty [lemma, in Metatheory_Env]
Env.binds_fresh [lemma, in Metatheory_Env]
Env.binds_func [lemma, in Metatheory_Env]
Env.binds_head [lemma, in Metatheory_Env]
Env.binds_inj [lemma, in Metatheory_Env]
Env.binds_map [lemma, in Metatheory_Env]
Env.binds_mid [lemma, in Metatheory_Env]
Env.binds_mid_eq [lemma, in Metatheory_Env]
Env.binds_prepend [lemma, in Metatheory_Env]
Env.binds_single_inv [lemma, in Metatheory_Env]
Env.binds_tail [lemma, in Metatheory_Env]
Env.binds_weaken [lemma, in Metatheory_Env]
Env.concat [definition, in Metatheory_Env]
Env.concat_assoc [lemma, in Metatheory_Env]
Env.concat_assoc_map_push [lemma, in Metatheory_Env]
Env.concat_empty [lemma, in Metatheory_Env]
Env.dom [definition, in Metatheory_Env]
Env.dom_concat [lemma, in Metatheory_Env]
Env.dom_cons [lemma, in Metatheory_Env]
Env.dom_empty [lemma, in Metatheory_Env]
Env.dom_map [lemma, in Metatheory_Env]
Env.dom_push [lemma, in Metatheory_Env]
Env.dom_single [lemma, in Metatheory_Env]
Env.empty [definition, in Metatheory_Env]
Env.env [definition, in Metatheory_Env]
Env.env_prop [definition, in Metatheory_Env]
Env.eq_empty_inv [lemma, in Metatheory_Env]
Env.eq_push_inv [lemma, in Metatheory_Env]
Env.extends [definition, in Metatheory_Env]
Env.extends_binds [lemma, in Metatheory_Env]
Env.extends_push [lemma, in Metatheory_Env]
Env.extends_self [lemma, in Metatheory_Env]
Env.fresh_mid [lemma, in Metatheory_Env]
Env.fv_in [definition, in Metatheory_Env]
Env.fv_in_spec [lemma, in Metatheory_Env]
Env.get [definition, in Metatheory_Env]
Env.iter_push [definition, in Metatheory_Env]
Env.iter_push_cons [lemma, in Metatheory_Env]
Env.iter_push_nil [lemma, in Metatheory_Env]
Env.map [definition, in Metatheory_Env]
Env.map_concat [lemma, in Metatheory_Env]
Env.ok [inductive, in Metatheory_Env]
Env.ok_concat_inv [lemma, in Metatheory_Env]
Env.ok_concat_iter_push [lemma, in Metatheory_Env]
Env.ok_empty [constructor, in Metatheory_Env]
Env.ok_map [lemma, in Metatheory_Env]
Env.ok_push [constructor, in Metatheory_Env]
Env.ok_remove [lemma, in Metatheory_Env]
Env.single [definition, in Metatheory_Env]
env_fv [definition, in ML_Infrastructure]
env_fv [definition, in ML_Core_Infrastructure]
env_less [inductive, in CoC_Preservation]
env_less_binds [lemma, in CoC_Preservation]
env_less_head [constructor, in CoC_Preservation]
env_less_tail [constructor, in CoC_Preservation]
epreservation [definition, in STLC_Core_Adequacy]
eprogress [definition, in STLC_Core_Adequacy]
equal [axiom, in Lib_MyFSetInterface]
equal_1 [axiom, in Lib_MyFSetInterface]
equal_2 [axiom, in Lib_MyFSetInterface]
equiv_ [inductive, in Lambda_Definitions]
equiv_ [inductive, in CoC_Definitions]
equiv_refl [constructor, in CoC_Definitions]
equiv_refl [constructor, in Lambda_Definitions]
equiv_step [constructor, in CoC_Definitions]
equiv_step [constructor, in Lambda_Definitions]
equiv_sym [constructor, in CoC_Definitions]
equiv_sym [constructor, in Lambda_Definitions]
equiv_trans [constructor, in Lambda_Definitions]
equiv_trans [constructor, in CoC_Definitions]
eq_ext [axiom, in Lib_FinSet]
eq_if_Equal [axiom, in Lib_FinSet]
eq_refl [axiom, in Lib_MyFSetInterface]
eq_sym [axiom, in Lib_MyFSetInterface]
eq_trans [axiom, in Lib_MyFSetInterface]
eq_typ_dec [lemma, in STLC_Dec_Decidability]
ered [inductive, in STLC_Core_Adequacy]
ered_app_1 [constructor, in STLC_Core_Adequacy]
ered_app_2 [constructor, in STLC_Core_Adequacy]
ered_beta [constructor, in STLC_Core_Adequacy]
ered_to_red [lemma, in STLC_Core_Adequacy]
eterm [inductive, in STLC_Core_Adequacy]
eterm_abs [constructor, in STLC_Core_Adequacy]
eterm_app [constructor, in STLC_Core_Adequacy]
eterm_to_term [lemma, in STLC_Core_Adequacy]
eterm_var [constructor, in STLC_Core_Adequacy]
etyping [inductive, in STLC_Core_Adequacy]
etyping_abs [constructor, in STLC_Core_Adequacy]
etyping_app [constructor, in STLC_Core_Adequacy]
etyping_to_typing [lemma, in STLC_Core_Adequacy]
etyping_var [constructor, in STLC_Core_Adequacy]
evalue [inductive, in STLC_Core_Adequacy]
evalue_abs [constructor, in STLC_Core_Adequacy]
evalue_to_value [lemma, in STLC_Core_Adequacy]
exists_ [axiom, in Lib_MyFSetInterface]
exists_1 [axiom, in Lib_MyFSetInterface]
exists_2 [axiom, in Lib_MyFSetInterface]
Export [module, in Metatheory_Var]


F

factorize_map [lemma, in ML_Soundness]
fails [inductive, in ML_Definitions]
fails [inductive, in STLC_Exn_Definitions]
fails_app_1 [constructor, in ML_Definitions]
fails_app_1 [constructor, in STLC_Exn_Definitions]
fails_app_2 [constructor, in ML_Definitions]
fails_app_2 [constructor, in STLC_Exn_Definitions]
fails_get_1 [constructor, in ML_Definitions]
fails_inj_1 [constructor, in ML_Definitions]
fails_inj_2 [constructor, in ML_Definitions]
fails_let_1 [constructor, in ML_Definitions]
fails_mat_1 [constructor, in ML_Definitions]
fails_new_1 [constructor, in ML_Definitions]
fails_pair_1 [constructor, in ML_Definitions]
fails_pair_2 [constructor, in ML_Definitions]
fails_raise_val [constructor, in STLC_Exn_Definitions]
fails_raise_val [constructor, in ML_Definitions]
fails_raise_1 [constructor, in ML_Definitions]
fails_raise_1 [constructor, in STLC_Exn_Definitions]
fails_regular [lemma, in STLC_Exn_Infrastructure]
fails_regular [lemma, in ML_Infrastructure]
fails_set_1 [constructor, in ML_Definitions]
fails_set_2 [constructor, in ML_Definitions]
fails_to_exception [lemma, in STLC_Exn_Soundness]
fails_to_exception [lemma, in ML_Soundness]
filter [axiom, in Lib_MyFSetInterface]
filter_1 [axiom, in Lib_MyFSetInterface]
filter_2 [axiom, in Lib_MyFSetInterface]
filter_3 [axiom, in Lib_MyFSetInterface]
FinSet [module, in Lib_FinSet]
FinSetFacts [module, in Lib_FinSet]
FinSet.E.S.elt [definition, in Lib_FinSet]
FinSet.E.S.FinSetFacts.in_empty [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.in_same [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.in_singleton [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.in_union [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_empty [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_same [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_singleton [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_union [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_empty_l [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_refl [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_singleton [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_trans [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_union_l [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_union_weak_l [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_union_weak_r [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_assoc [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_comm [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_comm_assoc [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_empty_l [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_empty_r [lemma, in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_same [lemma, in Lib_FinSet]
FinSet.E.S.fset [definition, in Lib_FinSet]
fold [axiom, in Lib_MyFSetInterface]
fold_1 [axiom, in Lib_MyFSetInterface]
for_all [axiom, in Lib_MyFSetInterface]
for_all_1 [axiom, in Lib_MyFSetInterface]
for_all_2 [axiom, in Lib_MyFSetInterface]
fresh_empty [lemma, in Metatheory_Fresh]
fresh_length [lemma, in Metatheory_Fresh]
fresh_resize [lemma, in Metatheory_Fresh]
fresh_union_l [lemma, in Metatheory_Fresh]
fresh_union_r [lemma, in Metatheory_Fresh]
Fsub_Definitions [library]
Fsub_Infrastructure [library]
Fsub_Part1A [library]
Fsub_Soundness [library]
fullred [inductive, in STLC_Core_FullBeta]
fullred_abs [constructor, in STLC_Core_FullBeta]
fullred_app1 [constructor, in STLC_Core_FullBeta]
fullred_app2 [constructor, in STLC_Core_FullBeta]
fullred_red [constructor, in STLC_Core_FullBeta]
fullred_regular [lemma, in STLC_Core_FullBeta]
fv [definition, in CoC_Infrastructure]
fv [definition, in STLC_Exn_Infrastructure]
fv [definition, in Lambda_Infrastructure]
fv [definition, in STLC_Core_WF_Infrastructure]
fv [definition, in STLC_Core_Light]
fv [definition, in STLC_Data_Infrastructure]
fv [definition, in STLC_Dec_Infrastructure]
fv [definition, in STLC_Ref_Infrastructure]
fv [definition, in STLC_Core_Infrastructure]
fv_ee [definition, in Fsub_Infrastructure]
fv_list [definition, in STLC_Data_Infrastructure]
fv_list_map [lemma, in STLC_Data_Infrastructure]
fv_list_map [lemma, in ML_Core_Infrastructure]
fv_open_var [lemma, in CoC_Infrastructure]
fv_te [definition, in Fsub_Infrastructure]
fv_tt [definition, in Fsub_Part1A]
fv_tt [definition, in Fsub_Infrastructure]


H

has_scheme [definition, in ML_Soundness]
has_scheme [definition, in ML_Core_Soundness]
has_scheme_from_typ [lemma, in ML_Core_Soundness]
has_scheme_from_typ [lemma, in ML_Soundness]
has_scheme_from_vars [lemma, in ML_Soundness]
has_scheme_from_vars [lemma, in ML_Core_Soundness]
has_scheme_vars [definition, in ML_Soundness]
has_scheme_vars [definition, in ML_Core_Soundness]


I

Import [module, in Metatheory_Var]
Import [module, in Lib_FinSetImpl]
Import [module, in Lib_FinSetImpl]
Import [module, in Metatheory_Var]
Import [module, in Metatheory_Var]
In [axiom, in Lib_MyFSetInterface]
InA_iff_In [lemma, in Lib_ListFacts]
incl_nil [lemma, in Lib_ListFacts]
incl_trans [lemma, in Lib_ListFacts]
inter [axiom, in Lib_MyFSetInterface]
inter_1 [axiom, in Lib_MyFSetInterface]
inter_2 [axiom, in Lib_MyFSetInterface]
inter_3 [axiom, in Lib_MyFSetInterface]
In_incl [lemma, in Lib_ListFacts]
In_1 [axiom, in Lib_MyFSetInterface]
is_empty [axiom, in Lib_MyFSetInterface]
is_empty_1 [axiom, in Lib_MyFSetInterface]
is_empty_2 [axiom, in Lib_MyFSetInterface]
iter_ [inductive, in CoC_ChurchRosser]
iter_ [inductive, in Lambda_Infrastructure]
iter_step [constructor, in CoC_ChurchRosser]
iter_step [constructor, in Lambda_Infrastructure]
iter_trans [constructor, in Lambda_Infrastructure]
iter_trans [constructor, in CoC_ChurchRosser]


L

Lambda_ChurchRosser [library]
Lambda_Definitions [library]
Lambda_Infrastructure [library]
lelistA_dec [lemma, in Lib_ListFacts]
less [inductive, in CoC_Definitions]
less_conv [constructor, in CoC_Definitions]
less_prod [constructor, in CoC_Definitions]
less_prod_any_inv [lemma, in CoC_Preservation]
less_prod_prod_inv [lemma, in CoC_Preservation]
less_red_out [lemma, in CoC_Preservation]
less_refl [constructor, in CoC_Definitions]
less_trans [constructor, in CoC_Definitions]
less_type_any_inv [lemma, in CoC_Preservation]
less_type_type_inv [lemma, in CoC_Preservation]
less_univ [constructor, in CoC_Definitions]
Lib_FinSet [library]
Lib_FinSetImpl [library]
Lib_ListFacts [library]
Lib_ListFactsMore [library]
Lib_MyFSetInterface [library]
Lib_Tactic [library]
list_concat_right [lemma, in Lib_ListFactsMore]
list_forall [inductive, in Lib_ListFactsMore]
list_forall_concat [lemma, in Lib_ListFactsMore]
list_forall_cons [constructor, in Lib_ListFactsMore]
list_forall_nil [constructor, in Lib_ListFactsMore]
list_for_n [definition, in Lib_ListFactsMore]
list_for_n_concat [lemma, in Lib_ListFactsMore]
list_map_id [lemma, in Lib_ListFactsMore]
list_map_nth [lemma, in Lib_ListFactsMore]
loc [definition, in STLC_Ref_Definitions]
loc [definition, in ML_Definitions]
lt [axiom, in Lib_MyFSetInterface]
lt_not_eq [axiom, in Lib_MyFSetInterface]
lt_trans [axiom, in Lib_MyFSetInterface]


M

Make [module, in Lib_FinSetImpl]
MakeRaw [module, in Lib_FinSetImpl]
MakeRaw.add [definition, in Lib_FinSetImpl]
MakeRaw.add_1 [lemma, in Lib_FinSetImpl]
MakeRaw.add_2 [lemma, in Lib_FinSetImpl]
MakeRaw.add_3 [lemma, in Lib_FinSetImpl]
MakeRaw.Build_slist' [definition, in Lib_FinSetImpl]
MakeRaw.cardinal [definition, in Lib_FinSetImpl]
MakeRaw.cardinal_1 [lemma, in Lib_FinSetImpl]
MakeRaw.choose [definition, in Lib_FinSetImpl]
MakeRaw.choose_1 [lemma, in Lib_FinSetImpl]
MakeRaw.choose_2 [lemma, in Lib_FinSetImpl]
MakeRaw.compare [definition, in Lib_FinSetImpl]
MakeRaw.diff [definition, in Lib_FinSetImpl]
MakeRaw.diff_1 [lemma, in Lib_FinSetImpl]
MakeRaw.diff_2 [lemma, in Lib_FinSetImpl]
MakeRaw.diff_3 [lemma, in Lib_FinSetImpl]
MakeRaw.elements [definition, in Lib_FinSetImpl]
MakeRaw.elements_1 [lemma, in Lib_FinSetImpl]
MakeRaw.elements_2 [lemma, in Lib_FinSetImpl]
MakeRaw.elements_3 [lemma, in Lib_FinSetImpl]
MakeRaw.elt [definition, in Lib_FinSetImpl]
MakeRaw.Empty [definition, in Lib_FinSetImpl]
MakeRaw.empty [definition, in Lib_FinSetImpl]
MakeRaw.empty_1 [lemma, in Lib_FinSetImpl]
MakeRaw.eq [definition, in Lib_FinSetImpl]
MakeRaw.Equal [definition, in Lib_FinSetImpl]
MakeRaw.equal [definition, in Lib_FinSetImpl]
MakeRaw.equal_1 [lemma, in Lib_FinSetImpl]
MakeRaw.equal_2 [lemma, in Lib_FinSetImpl]
MakeRaw.eq_refl [lemma, in Lib_FinSetImpl]
MakeRaw.eq_sym [lemma, in Lib_FinSetImpl]
MakeRaw.eq_trans [lemma, in Lib_FinSetImpl]
MakeRaw.Exists [definition, in Lib_FinSetImpl]
MakeRaw.exists_ [definition, in Lib_FinSetImpl]
MakeRaw.exists_1 [lemma, in Lib_FinSetImpl]
MakeRaw.exists_2 [lemma, in Lib_FinSetImpl]
MakeRaw.filter [definition, in Lib_FinSetImpl]
MakeRaw.filter_1 [lemma, in Lib_FinSetImpl]
MakeRaw.filter_2 [lemma, in Lib_FinSetImpl]
MakeRaw.filter_3 [lemma, in Lib_FinSetImpl]
MakeRaw.fold [definition, in Lib_FinSetImpl]
MakeRaw.fold_1 [lemma, in Lib_FinSetImpl]
MakeRaw.for_all [definition, in Lib_FinSetImpl]
MakeRaw.For_all [definition, in Lib_FinSetImpl]
MakeRaw.for_all_1 [lemma, in Lib_FinSetImpl]
MakeRaw.for_all_2 [lemma, in Lib_FinSetImpl]
MakeRaw.from_sorted [definition, in Lib_FinSetImpl]
MakeRaw.In [definition, in Lib_FinSetImpl]
MakeRaw.inter [definition, in Lib_FinSetImpl]
MakeRaw.inter_1 [lemma, in Lib_FinSetImpl]
MakeRaw.inter_2 [lemma, in Lib_FinSetImpl]
MakeRaw.inter_3 [lemma, in Lib_FinSetImpl]
MakeRaw.In_1 [lemma, in Lib_FinSetImpl]
MakeRaw.is_empty [definition, in Lib_FinSetImpl]
MakeRaw.is_empty_1 [lemma, in Lib_FinSetImpl]
MakeRaw.is_empty_2 [lemma, in Lib_FinSetImpl]
MakeRaw.lt [definition, in Lib_FinSetImpl]
MakeRaw.lt_not_eq [lemma, in Lib_FinSetImpl]
MakeRaw.lt_trans [lemma, in Lib_FinSetImpl]
MakeRaw.max_elt [definition, in Lib_FinSetImpl]
MakeRaw.max_elt_1 [lemma, in Lib_FinSetImpl]
MakeRaw.max_elt_2 [lemma, in Lib_FinSetImpl]
MakeRaw.max_elt_3 [lemma, in Lib_FinSetImpl]
MakeRaw.mem [definition, in Lib_FinSetImpl]
MakeRaw.mem_1 [lemma, in Lib_FinSetImpl]
MakeRaw.mem_2 [lemma, in Lib_FinSetImpl]
MakeRaw.min_elt [definition, in Lib_FinSetImpl]
MakeRaw.min_elt_1 [lemma, in Lib_FinSetImpl]
MakeRaw.min_elt_2 [lemma, in Lib_FinSetImpl]
MakeRaw.min_elt_3 [lemma, in Lib_FinSetImpl]
MakeRaw.partition [definition, in Lib_FinSetImpl]
MakeRaw.partition_1 [lemma, in Lib_FinSetImpl]
MakeRaw.partition_2 [lemma, in Lib_FinSetImpl]
MakeRaw.remove [definition, in Lib_FinSetImpl]
MakeRaw.remove_1 [lemma, in Lib_FinSetImpl]
MakeRaw.remove_2 [lemma, in Lib_FinSetImpl]
MakeRaw.remove_3 [lemma, in Lib_FinSetImpl]
MakeRaw.singleton [definition, in Lib_FinSetImpl]
MakeRaw.singleton_1 [lemma, in Lib_FinSetImpl]
MakeRaw.singleton_2 [lemma, in Lib_FinSetImpl]
MakeRaw.slist [inductive, in Lib_FinSetImpl]
MakeRaw.sort_bool [definition, in Lib_FinSetImpl]
MakeRaw.Subset [definition, in Lib_FinSetImpl]
MakeRaw.subset [definition, in Lib_FinSetImpl]
MakeRaw.subset_1 [lemma, in Lib_FinSetImpl]
MakeRaw.subset_2 [lemma, in Lib_FinSetImpl]
MakeRaw.t [definition, in Lib_FinSetImpl]
MakeRaw.to_sorted [definition, in Lib_FinSetImpl]
MakeRaw.union [definition, in Lib_FinSetImpl]
MakeRaw.union_1 [lemma, in Lib_FinSetImpl]
MakeRaw.union_2 [lemma, in Lib_FinSetImpl]
MakeRaw.union_3 [lemma, in Lib_FinSetImpl]
Make.Import.Import.bool_dec [lemma, in Lib_FinSetImpl]
Make.Import.Import.elt [definition, in Lib_FinSetImpl]
Make.Import.Import.eq_ext [lemma, in Lib_FinSetImpl]
Make.Import.Import.eq_if_Equal [lemma, in Lib_FinSetImpl]
Make.Import.Import.fset [definition, in Lib_FinSetImpl]
map_subst_tb_id [lemma, in Fsub_Infrastructure]
max_elt [axiom, in Lib_MyFSetInterface]
max_elt_1 [axiom, in Lib_MyFSetInterface]
max_elt_2 [axiom, in Lib_MyFSetInterface]
max_elt_3 [axiom, in Lib_MyFSetInterface]
mem [axiom, in Lib_MyFSetInterface]
mem_1 [axiom, in Lib_MyFSetInterface]
mem_2 [axiom, in Lib_MyFSetInterface]
Metatheory [library]
Metatheory_Env [library]
Metatheory_Fresh [library]
Metatheory_Var [library]
min_elt [axiom, in Lib_MyFSetInterface]
min_elt_1 [axiom, in Lib_MyFSetInterface]
min_elt_2 [axiom, in Lib_MyFSetInterface]
min_elt_3 [axiom, in Lib_MyFSetInterface]
ML_Core_Definitions [library]
ML_Core_Infrastructure [library]
ML_Core_Soundness [library]
ML_Definitions [library]
ML_Infrastructure [library]
ML_Soundness [library]
modus_ponens [lemma, in Lib_Tactic]


N

notin_fv_from_binds [lemma, in CoC_Infrastructure]
notin_fv_from_binds' [lemma, in CoC_Infrastructure]
notin_fv_from_wf [lemma, in CoC_Infrastructure]
notin_fv_wf [lemma, in Fsub_Infrastructure]
notin_singleton_l [lemma, in Metatheory_Fresh]
notin_singleton_r [lemma, in Metatheory_Fresh]
notin_singleton_swap [lemma, in Metatheory_Fresh]
notin_union_l [lemma, in Metatheory_Fresh]
notin_union_r [lemma, in Metatheory_Fresh]
not_InA_if_Sort_Inf [lemma, in Lib_ListFacts]
not_In_app [lemma, in Lib_ListFacts]
not_in_cons [lemma, in Lib_ListFacts]


O

okt [inductive, in Fsub_Part1A]
okt [inductive, in Fsub_Definitions]
okt_empty [constructor, in Fsub_Part1A]
okt_empty [constructor, in Fsub_Definitions]
okt_narrow [lemma, in Fsub_Part1A]
okt_narrow [lemma, in Fsub_Infrastructure]
okt_strengthen [lemma, in Fsub_Infrastructure]
okt_sub [constructor, in Fsub_Definitions]
okt_sub [constructor, in Fsub_Part1A]
okt_subst_tb [lemma, in Fsub_Infrastructure]
okt_typ [constructor, in Fsub_Definitions]
ok_from_okt [lemma, in Fsub_Infrastructure]
ok_from_okt [lemma, in Fsub_Part1A]
ok_from_wf [lemma, in CoC_Infrastructure]
ok_iter_push [lemma, in ML_Infrastructure]
open [definition, in CoC_Definitions]
open [definition, in ML_Definitions]
open [definition, in STLC_Core_Definitions]
open [definition, in STLC_Exn_Definitions]
open [definition, in STLC_Data_Definitions]
open [definition, in STLC_Dec_Definitions]
open [definition, in STLC_Ref_Definitions]
open [definition, in Lambda_Definitions]
open [definition, in STLC_Core_WF_Definitions]
open [definition, in STLC_Core_Light]
opens [definition, in STLC_Data_Definitions]
opens [definition, in ML_Definitions]
opens_rec [definition, in STLC_Data_Definitions]
opens_rec [definition, in ML_Definitions]
open_ee [definition, in Fsub_Definitions]
open_ee_rec [definition, in Fsub_Definitions]
open_rec [definition, in STLC_Ref_Definitions]
open_rec [definition, in STLC_Core_Light]
open_rec [definition, in STLC_Exn_Definitions]
open_rec [definition, in STLC_Dec_Definitions]
open_rec [definition, in Lambda_Definitions]
open_rec [definition, in STLC_Core_WF_Definitions]
open_rec [definition, in STLC_Core_Definitions]
open_rec [definition, in CoC_Definitions]
open_te [definition, in Fsub_Definitions]
open_term [lemma, in STLC_Exn_Infrastructure]
open_term [lemma, in STLC_Dec_Infrastructure]
open_term [lemma, in STLC_Core_WF_Infrastructure]
open_term [lemma, in STLC_Ref_Infrastructure]
open_term [lemma, in CoC_Infrastructure]
open_term [lemma, in Lambda_Infrastructure]
open_term [lemma, in STLC_Core_Infrastructure]
open_terms [lemma, in ML_Infrastructure]
open_terms [lemma, in STLC_Data_Infrastructure]
open_te_rec [definition, in Fsub_Definitions]
open_tt [definition, in Fsub_Part1A]
open_tt [definition, in Fsub_Definitions]
open_tt_rec [definition, in Fsub_Part1A]
open_tt_rec [definition, in Fsub_Definitions]
open_var_inj [lemma, in Lambda_Infrastructure]
open_var_inj [lemma, in CoC_Infrastructure]


P

para [inductive, in CoC_ChurchRosser]
para [inductive, in Lambda_Infrastructure]
para_abs [constructor, in Lambda_Infrastructure]
para_abs [constructor, in CoC_ChurchRosser]
para_abs_inv [lemma, in CoC_ChurchRosser]
para_abs_inv [lemma, in Lambda_ChurchRosser]
para_app [constructor, in Lambda_Infrastructure]
para_app [constructor, in CoC_ChurchRosser]
para_confluence [lemma, in Lambda_ChurchRosser]
para_confluence [lemma, in CoC_ChurchRosser]
para_iter_confluence [lemma, in CoC_ChurchRosser]
para_iter_confluence [lemma, in Lambda_ChurchRosser]
para_iter_parallelogram [lemma, in CoC_ChurchRosser]
para_iter_parallelogram [lemma, in Lambda_ChurchRosser]
para_iter_red_refl [lemma, in CoC_ChurchRosser]
para_iter_red_refl [lemma, in Lambda_ChurchRosser]
para_iter_to_beta_star [lemma, in CoC_ChurchRosser]
para_iter_to_beta_star [lemma, in Lambda_ChurchRosser]
para_prod [constructor, in CoC_ChurchRosser]
para_prod_inv [lemma, in CoC_ChurchRosser]
para_red [constructor, in Lambda_Infrastructure]
para_red [constructor, in CoC_ChurchRosser]
para_red_all [lemma, in CoC_ChurchRosser]
para_red_all [lemma, in Lambda_ChurchRosser]
para_red_out [lemma, in Lambda_ChurchRosser]
para_red_out [lemma, in CoC_ChurchRosser]
para_red_refl [lemma, in CoC_ChurchRosser]
para_red_refl [lemma, in Lambda_ChurchRosser]
para_red_rename [lemma, in CoC_ChurchRosser]
para_red_rename [lemma, in Lambda_ChurchRosser]
para_red_through [lemma, in Lambda_ChurchRosser]
para_red_through [lemma, in CoC_ChurchRosser]
para_srt [constructor, in CoC_ChurchRosser]
para_var [constructor, in Lambda_Infrastructure]
para_var [constructor, in CoC_ChurchRosser]
partition [axiom, in Lib_MyFSetInterface]
partition_1 [axiom, in Lib_MyFSetInterface]
partition_2 [axiom, in Lib_MyFSetInterface]
pat [inductive, in STLC_Data_Definitions]
pat [inductive, in ML_Definitions]
pattern_match_values [lemma, in ML_Soundness]
pat_arity [definition, in STLC_Data_Definitions]
pat_arity [definition, in ML_Definitions]
pat_bvar [constructor, in ML_Definitions]
pat_bvar [constructor, in STLC_Data_Definitions]
pat_inj1 [constructor, in ML_Definitions]
pat_inj1 [constructor, in STLC_Data_Definitions]
pat_inj2 [constructor, in STLC_Data_Definitions]
pat_inj2 [constructor, in ML_Definitions]
pat_match [definition, in STLC_Data_Definitions]
pat_match [definition, in ML_Definitions]
pat_match_terms [lemma, in STLC_Data_Infrastructure]
pat_match_terms [lemma, in ML_Infrastructure]
pat_pair [constructor, in ML_Definitions]
pat_pair [constructor, in STLC_Data_Definitions]
pat_typing [inductive, in STLC_Data_Definitions]
pat_typing [inductive, in ML_Definitions]
pat_typing_bvar [constructor, in ML_Definitions]
pat_typing_bvar [constructor, in STLC_Data_Definitions]
pat_typing_inj1 [constructor, in ML_Definitions]
pat_typing_inj1 [constructor, in STLC_Data_Definitions]
pat_typing_inj2 [constructor, in ML_Definitions]
pat_typing_inj2 [constructor, in STLC_Data_Definitions]
pat_typing_pair [constructor, in STLC_Data_Definitions]
pat_typing_pair [constructor, in ML_Definitions]
pat_typing_typ_subst [lemma, in ML_Soundness]
pat_typing_unit [constructor, in ML_Definitions]
pat_typing_unit [constructor, in STLC_Data_Definitions]
pat_typing_wild [constructor, in ML_Definitions]
pat_typing_wild [constructor, in STLC_Data_Definitions]
pat_unit [constructor, in ML_Definitions]
pat_unit [constructor, in STLC_Data_Definitions]
pat_wild [constructor, in STLC_Data_Definitions]
pat_wild [constructor, in ML_Definitions]
phi [definition, in STLC_Ref_Definitions]
phi [definition, in ML_Definitions]
phi_fv [definition, in ML_Infrastructure]
phi_ok [inductive, in ML_Definitions]
phi_ok_binds [lemma, in ML_Infrastructure]
phi_ok_empty [constructor, in ML_Definitions]
phi_ok_push [constructor, in ML_Definitions]
preservation [definition, in STLC_Exn_Definitions]
preservation [definition, in Fsub_Definitions]
preservation [definition, in STLC_Dec_Definitions]
preservation [definition, in ML_Definitions]
preservation [definition, in STLC_Ref_Definitions]
preservation [definition, in STLC_Core_WF_Definitions]
preservation [definition, in STLC_Core_Definitions]
preservation [definition, in ML_Core_Definitions]
preservation [definition, in STLC_Data_Definitions]
preservation_for_full_reduction [lemma, in STLC_Core_FullBeta]
preservation_result [lemma, in Fsub_Soundness]
preservation_result [lemma, in STLC_Core_WF_Soundness]
preservation_result [lemma, in STLC_Ref_Soundness]
preservation_result [lemma, in ML_Soundness]
preservation_result [lemma, in STLC_Dec_Soundness]
preservation_result [lemma, in ML_Core_Soundness]
preservation_result [lemma, in STLC_Exn_Soundness]
preservation_result [lemma, in STLC_Core_Light]
preservation_result [lemma, in STLC_Data_Soundness]
preservation_result [lemma, in STLC_Core_Soundness]
progress [definition, in STLC_Core_WF_Definitions]
progress [definition, in ML_Definitions]
progress [definition, in STLC_Ref_Definitions]
progress [definition, in Fsub_Definitions]
progress [definition, in STLC_Exn_Definitions]
progress [definition, in STLC_Core_Definitions]
progress [definition, in STLC_Dec_Definitions]
progress [definition, in STLC_Data_Definitions]
progress [definition, in ML_Core_Definitions]
progress_result [lemma, in STLC_Dec_Soundness]
progress_result [lemma, in STLC_Exn_Soundness]
progress_result [lemma, in STLC_Core_Light]
progress_result [lemma, in STLC_Core_WF_Soundness]
progress_result [lemma, in STLC_Ref_Soundness]
progress_result [lemma, in STLC_Data_Soundness]
progress_result [lemma, in ML_Soundness]
progress_result [lemma, in STLC_Core_Soundness]
progress_result [lemma, in ML_Core_Soundness]
progress_result [lemma, in Fsub_Soundness]


R

red [inductive, in ML_Core_Definitions]
red [inductive, in ML_Definitions]
red [inductive, in STLC_Core_WF_Definitions]
red [inductive, in STLC_Core_Definitions]
red [inductive, in STLC_Ref_Definitions]
red [inductive, in STLC_Dec_Definitions]
red [inductive, in Fsub_Definitions]
red [inductive, in STLC_Data_Definitions]
red [inductive, in STLC_Core_Light]
red [inductive, in STLC_Exn_Definitions]
red_abs [constructor, in Fsub_Definitions]
red_abs [constructor, in ML_Core_Definitions]
red_add [constructor, in ML_Definitions]
red_all [definition, in CoC_Infrastructure]
red_all [definition, in Lambda_Infrastructure]
red_all_to_out [lemma, in Lambda_ChurchRosser]
red_all_to_out [lemma, in CoC_BetaStar]
red_all_to_through [lemma, in Lambda_ChurchRosser]
red_all_to_through [lemma, in CoC_BetaStar]
red_app_1 [constructor, in Fsub_Definitions]
red_app_1 [constructor, in STLC_Core_Light]
red_app_1 [constructor, in ML_Core_Definitions]
red_app_1 [constructor, in STLC_Data_Definitions]
red_app_1 [constructor, in STLC_Ref_Definitions]
red_app_1 [constructor, in STLC_Core_Definitions]
red_app_1 [constructor, in ML_Definitions]
red_app_1 [constructor, in STLC_Dec_Definitions]
red_app_1 [constructor, in STLC_Exn_Definitions]
red_app_2 [constructor, in STLC_Core_Definitions]
red_app_2 [constructor, in STLC_Core_Light]
red_app_2 [constructor, in Fsub_Definitions]
red_app_2 [constructor, in ML_Core_Definitions]
red_app_2 [constructor, in STLC_Dec_Definitions]
red_app_2 [constructor, in ML_Definitions]
red_app_2 [constructor, in STLC_Ref_Definitions]
red_app_2 [constructor, in STLC_Exn_Definitions]
red_app_2 [constructor, in STLC_Data_Definitions]
red_beta [constructor, in STLC_Ref_Definitions]
red_beta [constructor, in STLC_Core_Light]
red_beta [constructor, in STLC_Core_WF_Definitions]
red_beta [constructor, in STLC_Exn_Definitions]
red_beta [constructor, in STLC_Core_Definitions]
red_beta [constructor, in ML_Definitions]
red_beta [constructor, in STLC_Data_Definitions]
red_beta [constructor, in STLC_Dec_Definitions]
red_catch_exn [constructor, in STLC_Exn_Definitions]
red_catch_exn [constructor, in ML_Definitions]
red_catch_val [constructor, in ML_Definitions]
red_catch_val [constructor, in STLC_Exn_Definitions]
red_catch_2 [constructor, in STLC_Exn_Definitions]
red_catch_2 [constructor, in ML_Definitions]
red_ctx [constructor, in STLC_Core_WF_Definitions]
red_fix [constructor, in STLC_Data_Definitions]
red_fix [constructor, in ML_Definitions]
red_get [constructor, in ML_Definitions]
red_get [constructor, in STLC_Ref_Definitions]
red_get_1 [constructor, in STLC_Ref_Definitions]
red_get_1 [constructor, in ML_Definitions]
red_in [definition, in Lambda_Infrastructure]
red_in [definition, in CoC_Infrastructure]
red_inj1_1 [constructor, in STLC_Data_Definitions]
red_inj1_1 [constructor, in ML_Definitions]
red_inj2_1 [constructor, in ML_Definitions]
red_inj2_1 [constructor, in STLC_Data_Definitions]
red_let [constructor, in ML_Core_Definitions]
red_let [constructor, in ML_Definitions]
red_let_1 [constructor, in ML_Core_Definitions]
red_match_none [constructor, in ML_Definitions]
red_match_none [constructor, in STLC_Data_Definitions]
red_match_some [constructor, in ML_Definitions]
red_match_some [constructor, in STLC_Data_Definitions]
red_match_1 [constructor, in STLC_Data_Definitions]
red_match_1 [constructor, in ML_Definitions]
red_new [constructor, in ML_Definitions]
red_new [constructor, in STLC_Ref_Definitions]
red_new_1 [constructor, in STLC_Ref_Definitions]
red_new_1 [constructor, in ML_Definitions]
red_out [definition, in Lambda_Infrastructure]
red_out [definition, in CoC_Infrastructure]
red_out_to_rename [lemma, in CoC_BetaStar]
red_out_to_rename [lemma, in Lambda_ChurchRosser]
red_pair_1 [constructor, in STLC_Data_Definitions]
red_pair_1 [constructor, in ML_Definitions]
red_pair_2 [constructor, in STLC_Data_Definitions]
red_pair_2 [constructor, in ML_Definitions]
red_raise_1 [constructor, in STLC_Exn_Definitions]
red_raise_1 [constructor, in ML_Definitions]
red_refl [definition, in CoC_Infrastructure]
red_refl [definition, in Lambda_Infrastructure]
red_regular [definition, in CoC_Infrastructure]
red_regular [lemma, in STLC_Data_Infrastructure]
red_regular [lemma, in STLC_Core_WF_Infrastructure]
red_regular [lemma, in STLC_Dec_Infrastructure]
red_regular [lemma, in ML_Infrastructure]
red_regular [definition, in Lambda_Infrastructure]
red_regular [lemma, in STLC_Ref_Infrastructure]
red_regular [lemma, in STLC_Core_Infrastructure]
red_regular [lemma, in STLC_Exn_Infrastructure]
red_regular [lemma, in Fsub_Infrastructure]
red_regular [lemma, in ML_Core_Infrastructure]
red_regular_beta [lemma, in Lambda_Infrastructure]
red_regular_beta [lemma, in CoC_Infrastructure]
red_regular_beta_star [lemma, in CoC_Infrastructure]
red_regular_beta_star [lemma, in Lambda_Infrastructure]
red_regular_conv [lemma, in CoC_Infrastructure]
red_regular_less [lemma, in CoC_Infrastructure]
red_regular_para [lemma, in Lambda_Infrastructure]
red_regular_para [lemma, in CoC_ChurchRosser]
red_regular_para_iter [lemma, in Lambda_Infrastructure]
red_regular_para_iter [lemma, in CoC_ChurchRosser]
red_rename [definition, in Lambda_Infrastructure]
red_rename [definition, in CoC_Infrastructure]
red_set [constructor, in STLC_Ref_Definitions]
red_set [constructor, in ML_Definitions]
red_set_1 [constructor, in ML_Definitions]
red_set_1 [constructor, in STLC_Ref_Definitions]
red_set_2 [constructor, in STLC_Ref_Definitions]
red_set_2 [constructor, in ML_Definitions]
red_tabs [constructor, in Fsub_Definitions]
red_tapp [constructor, in Fsub_Definitions]
red_through [definition, in Lambda_Infrastructure]
red_through [definition, in CoC_Infrastructure]
red_to_ered [lemma, in STLC_Core_Adequacy]
red_value_false [lemma, in ML_Soundness]
regular_typing [lemma, in CoC_Infrastructure]
relation [definition, in Lambda_Definitions]
relation [definition, in CoC_Definitions]
remove [axiom, in Lib_MyFSetInterface]
remove_1 [axiom, in Lib_MyFSetInterface]
remove_2 [axiom, in Lib_MyFSetInterface]
remove_3 [axiom, in Lib_MyFSetInterface]


S

S [module, in Lib_FinSet]
S [module, in Lib_MyFSetInterface]
sch [inductive, in ML_Core_Definitions]
sch [inductive, in ML_Definitions]
scheme [definition, in ML_Definitions]
scheme [definition, in ML_Core_Definitions]
sch_fv [definition, in ML_Core_Infrastructure]
sch_fv [definition, in ML_Infrastructure]
sch_open [definition, in ML_Definitions]
sch_open [definition, in ML_Core_Definitions]
sch_open_types [lemma, in ML_Infrastructure]
sch_open_types [lemma, in ML_Core_Infrastructure]
sch_open_vars [definition, in ML_Definitions]
sch_open_vars [definition, in ML_Core_Definitions]
sch_subst [definition, in ML_Core_Infrastructure]
sch_subst [definition, in ML_Infrastructure]
sch_substs [definition, in ML_Infrastructure]
sch_substs [definition, in ML_Core_Infrastructure]
sch_subst_arity [lemma, in ML_Infrastructure]
sch_subst_arity [lemma, in ML_Core_Infrastructure]
sch_subst_fold [lemma, in ML_Core_Infrastructure]
sch_subst_fold [lemma, in ML_Infrastructure]
sch_subst_fresh [lemma, in ML_Core_Infrastructure]
sch_subst_fresh [lemma, in ML_Infrastructure]
sch_subst_open [lemma, in ML_Core_Infrastructure]
sch_subst_open [lemma, in ML_Infrastructure]
sch_subst_open_vars [lemma, in ML_Core_Infrastructure]
sch_subst_open_vars [lemma, in ML_Infrastructure]
sch_subst_type [lemma, in ML_Infrastructure]
sch_subst_type [lemma, in ML_Core_Infrastructure]
simulated [definition, in CoC_Infrastructure]
simulated [definition, in Lambda_Infrastructure]
singleton [axiom, in Lib_MyFSetInterface]
singleton_1 [axiom, in Lib_MyFSetInterface]
singleton_2 [axiom, in Lib_MyFSetInterface]
skip [axiom, in Lib_Tactic]
sort_dec [lemma, in Lib_ListFacts]
Sort_eq_head [lemma, in Lib_ListFacts]
Sort_InA_eq_ext [lemma, in Lib_ListFacts]
star_ [inductive, in Lambda_Definitions]
star_ [inductive, in CoC_Definitions]
star_refl [constructor, in CoC_Definitions]
star_refl [constructor, in Lambda_Definitions]
star_step [constructor, in Lambda_Definitions]
star_step [constructor, in CoC_Definitions]
star_trans [constructor, in CoC_Definitions]
star_trans [constructor, in Lambda_Definitions]
STLC_Core_Adequacy [library]
STLC_Core_Definitions [library]
STLC_Core_FullBeta [library]
STLC_Core_Infrastructure [library]
STLC_Core_Light [library]
STLC_Core_Soundness [library]
STLC_Core_WF_Definitions [library]
STLC_Core_WF_Infrastructure [library]
STLC_Core_WF_Soundness [library]
STLC_Data_Definitions [library]
STLC_Data_Infrastructure [library]
STLC_Data_Soundness [library]
STLC_Dec_Decidability [library]
STLC_Dec_Definitions [library]
STLC_Dec_Infrastructure [library]
STLC_Dec_Soundness [library]
STLC_Exn_Definitions [library]
STLC_Exn_Infrastructure [library]
STLC_Exn_Soundness [library]
STLC_Ref_Definitions [library]
STLC_Ref_Infrastructure [library]
STLC_Ref_Soundness [library]
sto [definition, in STLC_Ref_Definitions]
sto [definition, in ML_Definitions]
sto_ok [inductive, in ML_Definitions]
sto_ok [inductive, in STLC_Ref_Definitions]
sto_ok_binds [lemma, in ML_Infrastructure]
sto_ok_binds [lemma, in STLC_Ref_Infrastructure]
sto_ok_empty [constructor, in STLC_Ref_Definitions]
sto_ok_empty [constructor, in ML_Definitions]
sto_ok_push [constructor, in STLC_Ref_Definitions]
sto_ok_push [constructor, in ML_Definitions]
sto_typing [definition, in ML_Definitions]
sto_typing [definition, in STLC_Ref_Definitions]
sto_typing_push [lemma, in ML_Soundness]
sto_typing_push [lemma, in STLC_Ref_Soundness]
sub [inductive, in Fsub_Part1A]
sub [inductive, in Fsub_Definitions]
subject_reduction [definition, in CoC_Definitions]
subject_reduction_ind [lemma, in CoC_Preservation]
subject_reduction_result [lemma, in CoC_Preservation]
subject_reduction_star_result [lemma, in CoC_Preservation]
subset [axiom, in Lib_MyFSetInterface]
subset_1 [axiom, in Lib_MyFSetInterface]
subset_2 [axiom, in Lib_MyFSetInterface]
subst [definition, in CoC_Infrastructure]
subst [definition, in STLC_Core_Infrastructure]
subst [definition, in STLC_Core_Light]
subst [definition, in Lambda_Infrastructure]
subst [definition, in STLC_Dec_Infrastructure]
subst [definition, in STLC_Core_WF_Infrastructure]
subst [definition, in STLC_Data_Infrastructure]
subst [definition, in STLC_Ref_Infrastructure]
subst [definition, in STLC_Exn_Infrastructure]
substitution [inductive, in ML_Definitions]
substs [definition, in STLC_Data_Infrastructure]
substs [definition, in ML_Infrastructure]
substs_fresh [lemma, in ML_Infrastructure]
substs_fresh [lemma, in STLC_Data_Infrastructure]
substs_intro [lemma, in STLC_Data_Infrastructure]
substs_intro [lemma, in ML_Infrastructure]
substs_intro_ind [lemma, in STLC_Data_Infrastructure]
substs_intro_ind [lemma, in ML_Infrastructure]
substs_terms [lemma, in STLC_Data_Infrastructure]
substs_terms [lemma, in ML_Infrastructure]
subst_body [lemma, in Lambda_Infrastructure]
subst_bodys [lemma, in ML_Infrastructure]
subst_ee [definition, in Fsub_Infrastructure]
subst_ee_fresh [lemma, in Fsub_Infrastructure]
subst_ee_intro [lemma, in Fsub_Infrastructure]
subst_ee_open_ee [lemma, in Fsub_Infrastructure]
subst_ee_open_ee_var [lemma, in Fsub_Infrastructure]
subst_ee_open_te_var [lemma, in Fsub_Infrastructure]
subst_ee_term [lemma, in Fsub_Infrastructure]
subst_fresh [lemma, in STLC_Data_Infrastructure]
subst_fresh [lemma, in STLC_Exn_Infrastructure]
subst_fresh [lemma, in Lambda_Infrastructure]
subst_fresh [lemma, in STLC_Ref_Infrastructure]
subst_fresh [lemma, in STLC_Core_WF_Infrastructure]
subst_fresh [lemma, in ML_Infrastructure]
subst_fresh [lemma, in STLC_Dec_Infrastructure]
subst_fresh [lemma, in STLC_Core_Infrastructure]
subst_fresh [lemma, in CoC_Infrastructure]
subst_fresh_list [lemma, in ML_Infrastructure]
subst_fresh_list [lemma, in STLC_Data_Infrastructure]
subst_fresh_trm_fvars [lemma, in ML_Infrastructure]
subst_fresh_trm_fvars [lemma, in STLC_Data_Infrastructure]
subst_intro [lemma, in STLC_Core_WF_Infrastructure]
subst_intro [lemma, in Lambda_Infrastructure]
subst_intro [lemma, in STLC_Ref_Infrastructure]
subst_intro [lemma, in STLC_Dec_Infrastructure]
subst_intro [lemma, in CoC_Infrastructure]
subst_intro [lemma, in STLC_Core_Infrastructure]
subst_intro [axiom, in STLC_Core_Light]
subst_intro [lemma, in STLC_Exn_Infrastructure]
subst_open [lemma, in STLC_Ref_Infrastructure]
subst_open [lemma, in Lambda_Infrastructure]
subst_open [lemma, in ML_Infrastructure]
subst_open [lemma, in STLC_Core_WF_Infrastructure]
subst_open [lemma, in STLC_Core_Infrastructure]
subst_open [lemma, in STLC_Data_Infrastructure]
subst_open [lemma, in STLC_Exn_Infrastructure]
subst_open [lemma, in STLC_Dec_Infrastructure]
subst_open [lemma, in CoC_Infrastructure]
subst_open_var [lemma, in STLC_Exn_Infrastructure]
subst_open_var [lemma, in CoC_Infrastructure]
subst_open_var [lemma, in Lambda_Infrastructure]
subst_open_var [lemma, in STLC_Ref_Infrastructure]
subst_open_var [axiom, in STLC_Core_Light]
subst_open_var [lemma, in STLC_Dec_Infrastructure]
subst_open_var [lemma, in STLC_Core_Infrastructure]
subst_open_var [lemma, in STLC_Core_WF_Infrastructure]
subst_open_vars [lemma, in STLC_Data_Infrastructure]
subst_open_vars [lemma, in ML_Infrastructure]
subst_tb [definition, in Fsub_Part1A]
subst_tb [definition, in Fsub_Infrastructure]
subst_te [definition, in Fsub_Infrastructure]
subst_term [lemma, in STLC_Dec_Infrastructure]
subst_term [lemma, in ML_Infrastructure]
subst_term [lemma, in Lambda_Infrastructure]
subst_term [lemma, in STLC_Exn_Infrastructure]
subst_term [lemma, in STLC_Core_WF_Infrastructure]
subst_term [lemma, in STLC_Core_Infrastructure]
subst_term [lemma, in STLC_Data_Infrastructure]
subst_term [lemma, in CoC_Infrastructure]
subst_term [lemma, in STLC_Ref_Infrastructure]
subst_te_fresh [lemma, in Fsub_Infrastructure]
subst_te_intro [lemma, in Fsub_Infrastructure]
subst_te_open_ee_var [lemma, in Fsub_Infrastructure]
subst_te_open_te [lemma, in Fsub_Infrastructure]
subst_te_open_te_var [lemma, in Fsub_Infrastructure]
subst_te_term [lemma, in Fsub_Infrastructure]
subst_tt [definition, in Fsub_Infrastructure]
subst_tt [definition, in Fsub_Part1A]
subst_tt_fresh [lemma, in Fsub_Infrastructure]
subst_tt_intro [lemma, in Fsub_Infrastructure]
subst_tt_open_tt [lemma, in Fsub_Infrastructure]
subst_tt_open_tt_var [lemma, in Fsub_Infrastructure]
subst_tt_type [lemma, in Fsub_Infrastructure]
sub_all [constructor, in Fsub_Definitions]
sub_all [constructor, in Fsub_Part1A]
sub_arrow [constructor, in Fsub_Definitions]
sub_arrow [constructor, in Fsub_Part1A]
sub_narrowing [lemma, in Fsub_Soundness]
sub_narrowing [lemma, in Fsub_Part1A]
sub_narrowing_aux [lemma, in Fsub_Soundness]
sub_narrowing_aux [lemma, in Fsub_Part1A]
sub_reflexivity [lemma, in Fsub_Part1A]
sub_reflexivity [lemma, in Fsub_Soundness]
sub_refl_tvar [constructor, in Fsub_Part1A]
sub_refl_tvar [constructor, in Fsub_Definitions]
sub_regular [lemma, in Fsub_Part1A]
sub_regular [lemma, in Fsub_Infrastructure]
sub_strengthening [lemma, in Fsub_Soundness]
sub_through_subst_tt [lemma, in Fsub_Soundness]
sub_top [constructor, in Fsub_Definitions]
sub_top [constructor, in Fsub_Part1A]
sub_transitivity [lemma, in Fsub_Part1A]
sub_transitivity [lemma, in Fsub_Soundness]
sub_trans_tvar [constructor, in Fsub_Definitions]
sub_trans_tvar [constructor, in Fsub_Part1A]
sub_weakening [lemma, in Fsub_Soundness]
sub_weakening [lemma, in Fsub_Part1A]
S.E.elt [definition, in Lib_MyFSetInterface]
S.E.Empty [definition, in Lib_MyFSetInterface]
S.E.eq [definition, in Lib_MyFSetInterface]
S.E.Equal [definition, in Lib_MyFSetInterface]
S.E.Exists [definition, in Lib_MyFSetInterface]
S.E.For_all [definition, in Lib_MyFSetInterface]
S.E.Subset [definition, in Lib_MyFSetInterface]


T

t [axiom, in Lib_MyFSetInterface]
term [inductive, in STLC_Dec_Definitions]
term [inductive, in CoC_Definitions]
term [inductive, in STLC_Core_Definitions]
term [inductive, in STLC_Core_Light]
term [inductive, in ML_Core_Definitions]
term [inductive, in Fsub_Definitions]
term [inductive, in STLC_Data_Definitions]
term [inductive, in STLC_Core_WF_Definitions]
term [inductive, in ML_Definitions]
term [inductive, in STLC_Exn_Definitions]
term [inductive, in STLC_Ref_Definitions]
term [inductive, in Lambda_Definitions]
terms [definition, in STLC_Data_Infrastructure]
terms [definition, in ML_Infrastructure]
term_abs [constructor, in STLC_Core_Light]
term_abs [constructor, in STLC_Core_WF_Definitions]
term_abs [constructor, in Fsub_Definitions]
term_abs [constructor, in Lambda_Definitions]
term_abs [constructor, in STLC_Core_Definitions]
term_abs [constructor, in ML_Core_Definitions]
term_abs [constructor, in STLC_Data_Definitions]
term_abs [constructor, in CoC_Definitions]
term_abs [constructor, in STLC_Exn_Definitions]
term_abs [constructor, in STLC_Ref_Definitions]
term_abs [constructor, in STLC_Dec_Definitions]
term_abs [constructor, in ML_Definitions]
term_abs1 [lemma, in CoC_Infrastructure]
term_abs_prove [lemma, in CoC_Infrastructure]
term_abs_to_body [lemma, in Lambda_Infrastructure]
term_abs_to_body [lemma, in STLC_Exn_Infrastructure]
term_abs_to_body [lemma, in ML_Core_Infrastructure]
term_abs_to_body [lemma, in STLC_Core_Infrastructure]
term_abs_to_body [lemma, in STLC_Ref_Infrastructure]
term_abs_to_body [lemma, in ML_Infrastructure]
term_abs_to_body [lemma, in STLC_Data_Infrastructure]
term_abs_to_body [lemma, in STLC_Core_WF_Infrastructure]
term_abs_to_body [lemma, in STLC_Dec_Infrastructure]
term_add [constructor, in ML_Definitions]
term_app [constructor, in Fsub_Definitions]
term_app [constructor, in STLC_Data_Definitions]
term_app [constructor, in STLC_Core_Light]
term_app [constructor, in CoC_Definitions]
term_app [constructor, in Lambda_Definitions]
term_app [constructor, in STLC_Core_Definitions]
term_app [constructor, in STLC_Exn_Definitions]
term_app [constructor, in STLC_Ref_Definitions]
term_app [constructor, in STLC_Dec_Definitions]
term_app [constructor, in ML_Definitions]
term_app [constructor, in STLC_Core_WF_Definitions]
term_app [constructor, in ML_Core_Definitions]
term_body [definition, in ML_Core_Definitions]
term_catch [constructor, in STLC_Exn_Definitions]
term_catch [constructor, in ML_Definitions]
term_fix [constructor, in STLC_Data_Definitions]
term_fix [constructor, in ML_Definitions]
term_fix_to_body [lemma, in ML_Infrastructure]
term_fix_to_body [lemma, in STLC_Data_Infrastructure]
term_from_binds_in_wf [lemma, in CoC_Infrastructure]
term_get [constructor, in ML_Definitions]
term_get [constructor, in STLC_Ref_Definitions]
term_inj1 [constructor, in ML_Definitions]
term_inj1 [constructor, in STLC_Data_Definitions]
term_inj2 [constructor, in STLC_Data_Definitions]
term_inj2 [constructor, in ML_Definitions]
term_let [constructor, in ML_Core_Definitions]
term_let [constructor, in ML_Definitions]
term_let_to_body [lemma, in ML_Infrastructure]
term_let_to_body [lemma, in ML_Core_Infrastructure]
term_loc [constructor, in STLC_Ref_Definitions]
term_loc [constructor, in ML_Definitions]
term_match [constructor, in STLC_Data_Definitions]
term_match [constructor, in ML_Definitions]
term_match_to_body [lemma, in STLC_Data_Infrastructure]
term_match_to_body [lemma, in ML_Infrastructure]
term_nat [constructor, in ML_Definitions]
term_new [constructor, in STLC_Ref_Definitions]
term_new [constructor, in ML_Definitions]
term_pair [constructor, in STLC_Data_Definitions]
term_pair [constructor, in ML_Definitions]
term_prod [constructor, in CoC_Definitions]
term_prod_prove [lemma, in CoC_Infrastructure]
term_raise [constructor, in STLC_Exn_Definitions]
term_raise [constructor, in ML_Definitions]
term_rename [lemma, in STLC_Core_Adequacy]
term_set [constructor, in STLC_Ref_Definitions]
term_set [constructor, in ML_Definitions]
term_tabs [constructor, in Fsub_Definitions]
term_tapp [constructor, in Fsub_Definitions]
term_to_eterm [lemma, in STLC_Core_Adequacy]
term_trm_unit [constructor, in STLC_Ref_Definitions]
term_type [constructor, in CoC_Definitions]
term_unit [constructor, in ML_Definitions]
term_unit [constructor, in STLC_Data_Definitions]
term_var [constructor, in CoC_Definitions]
term_var [constructor, in ML_Definitions]
term_var [constructor, in STLC_Dec_Definitions]
term_var [constructor, in STLC_Core_Definitions]
term_var [constructor, in Fsub_Definitions]
term_var [constructor, in Lambda_Definitions]
term_var [constructor, in STLC_Data_Definitions]
term_var [constructor, in ML_Core_Definitions]
term_var [constructor, in STLC_Core_WF_Definitions]
term_var [constructor, in STLC_Exn_Definitions]
term_var [constructor, in STLC_Ref_Definitions]
term_var [constructor, in STLC_Core_Light]
test_fresh_solve_1 [lemma, in Metatheory_Fresh]
test_fresh_solve_2 [lemma, in Metatheory_Fresh]
test_fresh_solve_3 [lemma, in Metatheory_Fresh]
test_fresh_solve_4 [lemma, in Metatheory_Fresh]
test_neq_solve [lemma, in Metatheory_Fresh]
test_notin_contradiction [lemma, in Metatheory_Fresh]
test_notin_solve_1 [lemma, in Metatheory_Fresh]
test_notin_solve_2 [lemma, in Metatheory_Fresh]
test_notin_solve_3 [lemma, in Metatheory_Fresh]
transitivity_on [definition, in Fsub_Soundness]
transitivity_on [definition, in Fsub_Part1A]
trm [inductive, in STLC_Core_WF_Definitions]
trm [inductive, in CoC_Definitions]
trm [inductive, in STLC_Core_Definitions]
trm [inductive, in Lambda_Definitions]
trm [inductive, in STLC_Ref_Definitions]
trm [inductive, in ML_Core_Definitions]
trm [inductive, in Fsub_Definitions]
trm [inductive, in ML_Definitions]
trm [inductive, in STLC_Data_Definitions]
trm [inductive, in STLC_Exn_Definitions]
trm [inductive, in STLC_Dec_Definitions]
trm [inductive, in STLC_Core_Light]
trm_abs [constructor, in CoC_Definitions]
trm_abs [constructor, in STLC_Core_Definitions]
trm_abs [constructor, in ML_Definitions]
trm_abs [constructor, in STLC_Core_WF_Definitions]
trm_abs [constructor, in STLC_Core_Light]
trm_abs [constructor, in Lambda_Definitions]
trm_abs [constructor, in ML_Core_Definitions]
trm_abs [constructor, in STLC_Ref_Definitions]
trm_abs [constructor, in STLC_Dec_Definitions]
trm_abs [constructor, in STLC_Data_Definitions]
trm_abs [constructor, in STLC_Exn_Definitions]
trm_abs [constructor, in Fsub_Definitions]
trm_add [constructor, in ML_Definitions]
trm_app [constructor, in Lambda_Definitions]
trm_app [constructor, in ML_Core_Definitions]
trm_app [constructor, in ML_Definitions]
trm_app [constructor, in STLC_Data_Definitions]
trm_app [constructor, in STLC_Ref_Definitions]
trm_app [constructor, in STLC_Core_WF_Definitions]
trm_app [constructor, in STLC_Core_Definitions]
trm_app [constructor, in STLC_Dec_Definitions]
trm_app [constructor, in STLC_Core_Light]
trm_app [constructor, in Fsub_Definitions]
trm_app [constructor, in CoC_Definitions]
trm_app [constructor, in STLC_Exn_Definitions]
trm_bvar [constructor, in STLC_Core_WF_Definitions]
trm_bvar [constructor, in Fsub_Definitions]
trm_bvar [constructor, in Lambda_Definitions]
trm_bvar [constructor, in ML_Definitions]
trm_bvar [constructor, in STLC_Ref_Definitions]
trm_bvar [constructor, in CoC_Definitions]
trm_bvar [constructor, in STLC_Dec_Definitions]
trm_bvar [constructor, in ML_Core_Definitions]
trm_bvar [constructor, in STLC_Core_Definitions]
trm_bvar [constructor, in STLC_Data_Definitions]
trm_bvar [constructor, in STLC_Exn_Definitions]
trm_bvar [constructor, in STLC_Core_Light]
trm_catch [constructor, in ML_Definitions]
trm_catch [constructor, in STLC_Exn_Definitions]
trm_def [definition, in ML_Definitions]
trm_def [definition, in STLC_Data_Definitions]
trm_def_fresh [lemma, in ML_Infrastructure]
trm_def_fresh [lemma, in STLC_Data_Infrastructure]
trm_fix [constructor, in STLC_Data_Definitions]
trm_fix [constructor, in ML_Definitions]
trm_fv [definition, in ML_Infrastructure]
trm_fv [definition, in ML_Core_Infrastructure]
trm_fvar [constructor, in STLC_Core_WF_Definitions]
trm_fvar [constructor, in Lambda_Definitions]
trm_fvar [constructor, in Fsub_Definitions]
trm_fvar [constructor, in STLC_Data_Definitions]
trm_fvar [constructor, in STLC_Ref_Definitions]
trm_fvar [constructor, in STLC_Core_Definitions]
trm_fvar [constructor, in ML_Core_Definitions]
trm_fvar [constructor, in STLC_Dec_Definitions]
trm_fvar [constructor, in ML_Definitions]
trm_fvar [constructor, in STLC_Core_Light]
trm_fvar [constructor, in STLC_Exn_Definitions]
trm_fvar [constructor, in CoC_Definitions]
trm_fvars [definition, in ML_Definitions]
trm_fvars [definition, in STLC_Data_Definitions]
trm_fv_list [definition, in ML_Infrastructure]
trm_fv_list_map [lemma, in ML_Infrastructure]
trm_get [constructor, in ML_Definitions]
trm_get [constructor, in STLC_Ref_Definitions]
trm_inj1 [constructor, in STLC_Data_Definitions]
trm_inj1 [constructor, in ML_Definitions]
trm_inj2 [constructor, in ML_Definitions]
trm_inj2 [constructor, in STLC_Data_Definitions]
trm_let [constructor, in ML_Core_Definitions]
trm_let [constructor, in ML_Definitions]
trm_loc [constructor, in STLC_Ref_Definitions]
trm_loc [constructor, in ML_Definitions]
trm_match [constructor, in ML_Definitions]
trm_match [constructor, in STLC_Data_Definitions]
trm_nat [constructor, in ML_Definitions]
trm_nth [definition, in STLC_Data_Definitions]
trm_nth [definition, in ML_Definitions]
trm_open [definition, in ML_Core_Definitions]
trm_open_rec [definition, in ML_Core_Definitions]
trm_open_term [lemma, in ML_Core_Infrastructure]
trm_pair [constructor, in ML_Definitions]
trm_pair [constructor, in STLC_Data_Definitions]
trm_prod [constructor, in CoC_Definitions]
trm_raise [constructor, in STLC_Exn_Definitions]
trm_raise [constructor, in ML_Definitions]
trm_ref [constructor, in STLC_Ref_Definitions]
trm_ref [constructor, in ML_Definitions]
trm_set [constructor, in STLC_Ref_Definitions]
trm_set [constructor, in ML_Definitions]
trm_subst [definition, in ML_Core_Infrastructure]
trm_subst [definition, in ML_Infrastructure]
trm_subst_fresh [lemma, in ML_Core_Infrastructure]
trm_subst_intro [lemma, in ML_Core_Infrastructure]
trm_subst_open [lemma, in ML_Core_Infrastructure]
trm_subst_open_var [lemma, in ML_Core_Infrastructure]
trm_subst_term [lemma, in ML_Core_Infrastructure]
trm_tabs [constructor, in Fsub_Definitions]
trm_tapp [constructor, in Fsub_Definitions]
trm_type [constructor, in CoC_Definitions]
trm_unit [constructor, in ML_Definitions]
trm_unit [constructor, in STLC_Ref_Definitions]
trm_unit [constructor, in STLC_Data_Definitions]
typ [inductive, in STLC_Data_Definitions]
typ [inductive, in Fsub_Part1A]
typ [inductive, in STLC_Ref_Definitions]
typ [inductive, in STLC_Core_Definitions]
typ [inductive, in STLC_Core_Light]
typ [inductive, in ML_Definitions]
typ [inductive, in STLC_Exn_Definitions]
typ [inductive, in ML_Core_Definitions]
typ [inductive, in STLC_Dec_Definitions]
typ [inductive, in STLC_Core_WF_Definitions]
typ [inductive, in Fsub_Definitions]
type [inductive, in ML_Core_Definitions]
type [inductive, in Fsub_Part1A]
type [inductive, in Fsub_Definitions]
type [inductive, in ML_Definitions]
types [definition, in ML_Core_Definitions]
types [definition, in ML_Definitions]
type_all [constructor, in Fsub_Definitions]
type_all [constructor, in Fsub_Part1A]
type_arrow [constructor, in ML_Definitions]
type_arrow [constructor, in Fsub_Definitions]
type_arrow [constructor, in Fsub_Part1A]
type_arrow [constructor, in ML_Core_Definitions]
type_from_wft [lemma, in Fsub_Part1A]
type_from_wft [lemma, in Fsub_Infrastructure]
type_fvar [constructor, in ML_Core_Definitions]
type_fvar [constructor, in ML_Definitions]
type_nat [constructor, in ML_Definitions]
type_prod [constructor, in ML_Definitions]
type_ref [constructor, in ML_Definitions]
type_sum [constructor, in ML_Definitions]
type_top [constructor, in Fsub_Definitions]
type_top [constructor, in Fsub_Part1A]
type_unit [constructor, in ML_Definitions]
type_var [constructor, in Fsub_Definitions]
type_var [constructor, in Fsub_Part1A]
typing [inductive, in STLC_Core_WF_Definitions]
typing [inductive, in ML_Core_Definitions]
typing [inductive, in STLC_Core_Light]
typing [inductive, in ML_Definitions]
typing [inductive, in STLC_Exn_Definitions]
typing [inductive, in STLC_Core_Definitions]
typing [inductive, in Fsub_Definitions]
typing [inductive, in STLC_Dec_Definitions]
typing [inductive, in CoC_Definitions]
typing [inductive, in STLC_Ref_Definitions]
typing [inductive, in STLC_Data_Definitions]
typings [inductive, in STLC_Data_Infrastructure]
typings [inductive, in ML_Infrastructure]
typings_concat [lemma, in ML_Infrastructure]
typings_concat [lemma, in STLC_Data_Infrastructure]
typings_cons [constructor, in STLC_Data_Infrastructure]
typings_cons [constructor, in ML_Infrastructure]
typings_nil [constructor, in ML_Infrastructure]
typings_nil [constructor, in STLC_Data_Infrastructure]
typing_abs [constructor, in STLC_Dec_Definitions]
typing_abs [constructor, in STLC_Ref_Definitions]
typing_abs [constructor, in STLC_Core_Definitions]
typing_abs [constructor, in ML_Definitions]
typing_abs [constructor, in STLC_Core_WF_Definitions]
typing_abs [constructor, in Fsub_Definitions]
typing_abs [constructor, in CoC_Definitions]
typing_abs [constructor, in STLC_Core_Light]
typing_abs [constructor, in STLC_Data_Definitions]
typing_abs [constructor, in ML_Core_Definitions]
typing_abs [constructor, in STLC_Exn_Definitions]
typing_abs_inv [lemma, in CoC_Preservation]
typing_app [constructor, in Fsub_Definitions]
typing_app [constructor, in STLC_Exn_Definitions]
typing_app [constructor, in CoC_Definitions]
typing_app [constructor, in STLC_Core_Definitions]
typing_app [constructor, in STLC_Data_Definitions]
typing_app [constructor, in STLC_Core_WF_Definitions]
typing_app [constructor, in ML_Core_Definitions]
typing_app [constructor, in STLC_Dec_Definitions]
typing_app [constructor, in STLC_Ref_Definitions]
typing_app [constructor, in STLC_Core_Light]
typing_catch [constructor, in STLC_Exn_Definitions]
typing_dec' [lemma, in STLC_Dec_Decidability]
typing_fix [constructor, in STLC_Data_Definitions]
typing_fix [constructor, in ML_Definitions]
typing_fresh [lemma, in CoC_Infrastructure]
typing_get [constructor, in STLC_Ref_Definitions]
typing_inj1 [constructor, in STLC_Data_Definitions]
typing_inj2 [constructor, in STLC_Data_Definitions]
typing_inv_abs [lemma, in Fsub_Soundness]
typing_inv_tabs [lemma, in Fsub_Soundness]
typing_let [constructor, in ML_Core_Definitions]
typing_let [constructor, in ML_Definitions]
typing_loc [constructor, in STLC_Ref_Definitions]
typing_match [constructor, in ML_Definitions]
typing_match [constructor, in STLC_Data_Definitions]
typing_narrowing [lemma, in Fsub_Soundness]
typing_new [constructor, in STLC_Ref_Definitions]
typing_pair [constructor, in STLC_Data_Definitions]
typing_pattern_match [lemma, in ML_Soundness]
typing_pattern_match [lemma, in STLC_Data_Soundness]
typing_prod [constructor, in CoC_Definitions]
typing_prod_inv [lemma, in CoC_Preservation]
typing_prod_type_inv [lemma, in CoC_Preservation]
typing_raise [constructor, in STLC_Exn_Definitions]
typing_regular [lemma, in ML_Infrastructure]
typing_regular [lemma, in STLC_Core_Infrastructure]
typing_regular [lemma, in STLC_Core_WF_Infrastructure]
typing_regular [lemma, in STLC_Ref_Infrastructure]
typing_regular [lemma, in STLC_Data_Infrastructure]
typing_regular [lemma, in STLC_Exn_Infrastructure]
typing_regular [lemma, in STLC_Dec_Infrastructure]
typing_regular [lemma, in Fsub_Infrastructure]
typing_regular [lemma, in ML_Core_Infrastructure]
typing_rename [lemma, in STLC_Core_Adequacy]
typing_rename [lemma, in STLC_Dec_Decidability]
typing_set [constructor, in STLC_Ref_Definitions]
typing_stability [lemma, in ML_Soundness]
typing_stability [lemma, in STLC_Ref_Soundness]
typing_sub [constructor, in CoC_Definitions]
typing_sub [constructor, in Fsub_Definitions]
typing_subst [lemma, in STLC_Core_WF_Soundness]
typing_subst [lemma, in STLC_Dec_Soundness]
typing_subst [lemma, in STLC_Ref_Soundness]
typing_subst [lemma, in STLC_Data_Soundness]
typing_subst [lemma, in STLC_Exn_Soundness]
typing_subst [lemma, in STLC_Core_Light]
typing_subst [lemma, in STLC_Core_Soundness]
typing_substitution [lemma, in CoC_Preservation]
typing_substs [lemma, in STLC_Data_Soundness]
typing_sub_env [lemma, in CoC_Preservation]
typing_tabs [constructor, in Fsub_Definitions]
typing_tapp [constructor, in Fsub_Definitions]
typing_through_subst_ee [lemma, in Fsub_Soundness]
typing_through_subst_te [lemma, in Fsub_Soundness]
typing_to_etyping [lemma, in STLC_Core_Adequacy]
typing_trm_subst [lemma, in ML_Core_Soundness]
typing_trm_subst [lemma, in ML_Soundness]
typing_trm_substs [lemma, in ML_Soundness]
typing_trm_unit [constructor, in STLC_Ref_Definitions]
typing_type [constructor, in CoC_Definitions]
typing_typ_subst [lemma, in ML_Core_Soundness]
typing_typ_subst [lemma, in ML_Soundness]
typing_typ_substs [lemma, in ML_Soundness]
typing_typ_substs [lemma, in ML_Core_Soundness]
typing_unit [constructor, in STLC_Data_Definitions]
typing_var [constructor, in CoC_Definitions]
typing_var [constructor, in STLC_Core_WF_Definitions]
typing_var [constructor, in STLC_Dec_Definitions]
typing_var [constructor, in Fsub_Definitions]
typing_var [constructor, in STLC_Data_Definitions]
typing_var [constructor, in ML_Core_Definitions]
typing_var [constructor, in ML_Definitions]
typing_var [constructor, in STLC_Ref_Definitions]
typing_var [constructor, in STLC_Exn_Definitions]
typing_var [constructor, in STLC_Core_Light]
typing_var [constructor, in STLC_Core_Definitions]
typing_weaken [lemma, in STLC_Exn_Soundness]
typing_weaken [lemma, in STLC_Data_Soundness]
typing_weaken [lemma, in STLC_Core_Light]
typing_weaken [lemma, in CoC_Preservation]
typing_weaken [lemma, in STLC_Core_WF_Soundness]
typing_weaken [lemma, in ML_Core_Soundness]
typing_weaken [lemma, in STLC_Dec_Soundness]
typing_weaken [lemma, in STLC_Core_Soundness]
typing_weaken [lemma, in STLC_Ref_Soundness]
typing_weaken [lemma, in ML_Soundness]
typing_weakening [lemma, in Fsub_Soundness]
typing_wf_from_context [lemma, in CoC_Preservation]
typing_wf_from_typing [lemma, in CoC_Preservation]
typ_all [constructor, in Fsub_Part1A]
typ_all [constructor, in Fsub_Definitions]
typ_arrow [constructor, in STLC_Exn_Definitions]
typ_arrow [constructor, in STLC_Ref_Definitions]
typ_arrow [constructor, in STLC_Core_WF_Definitions]
typ_arrow [constructor, in STLC_Core_Definitions]
typ_arrow [constructor, in Fsub_Definitions]
typ_arrow [constructor, in STLC_Core_Light]
typ_arrow [constructor, in STLC_Dec_Definitions]
typ_arrow [constructor, in ML_Core_Definitions]
typ_arrow [constructor, in Fsub_Part1A]
typ_arrow [constructor, in ML_Definitions]
typ_arrow [constructor, in STLC_Data_Definitions]
typ_body [definition, in ML_Definitions]
typ_body [definition, in ML_Core_Definitions]
typ_bvar [constructor, in ML_Definitions]
typ_bvar [constructor, in ML_Core_Definitions]
typ_bvar [constructor, in Fsub_Definitions]
typ_bvar [constructor, in Fsub_Part1A]
typ_def [definition, in ML_Core_Definitions]
typ_def [definition, in ML_Definitions]
typ_def_fresh [lemma, in ML_Core_Infrastructure]
typ_def_fresh [lemma, in ML_Infrastructure]
typ_exn [constructor, in STLC_Exn_Definitions]
typ_exn [axiom, in ML_Definitions]
typ_exn_fresh [axiom, in ML_Definitions]
typ_fv [definition, in ML_Core_Infrastructure]
typ_fv [definition, in ML_Definitions]
typ_fvar [constructor, in ML_Core_Definitions]
typ_fvar [constructor, in Fsub_Definitions]
typ_fvar [constructor, in ML_Definitions]
typ_fvar [constructor, in Fsub_Part1A]
typ_fvars [definition, in ML_Definitions]
typ_fvars [definition, in ML_Core_Definitions]
typ_fv_list [definition, in ML_Core_Infrastructure]
typ_fv_list [definition, in ML_Infrastructure]
typ_fv_list_map [lemma, in ML_Infrastructure]
typ_nat [constructor, in ML_Definitions]
typ_open [definition, in ML_Definitions]
typ_open [definition, in ML_Core_Definitions]
typ_open_type [lemma, in ML_Core_Infrastructure]
typ_open_type [lemma, in ML_Infrastructure]
typ_open_types [lemma, in ML_Core_Infrastructure]
typ_open_types [lemma, in ML_Infrastructure]
typ_open_vars [definition, in ML_Core_Definitions]
typ_open_vars [definition, in ML_Definitions]
typ_prod [constructor, in ML_Definitions]
typ_prod [constructor, in STLC_Data_Definitions]
typ_ref [constructor, in STLC_Ref_Definitions]
typ_ref [constructor, in ML_Definitions]
typ_subst [definition, in ML_Core_Infrastructure]
typ_subst [definition, in ML_Infrastructure]
typ_substs [definition, in ML_Infrastructure]
typ_substs [definition, in ML_Core_Infrastructure]
typ_substs_fresh [lemma, in ML_Infrastructure]
typ_substs_fresh [lemma, in ML_Core_Infrastructure]
typ_substs_intro [lemma, in ML_Core_Infrastructure]
typ_substs_intro [lemma, in ML_Infrastructure]
typ_substs_intro_ind [lemma, in ML_Core_Infrastructure]
typ_substs_intro_ind [lemma, in ML_Infrastructure]
typ_substs_types [lemma, in ML_Core_Infrastructure]
typ_substs_types [lemma, in ML_Infrastructure]
typ_subst_fresh [lemma, in ML_Infrastructure]
typ_subst_fresh [lemma, in ML_Core_Infrastructure]
typ_subst_fresh_list [lemma, in ML_Infrastructure]
typ_subst_fresh_list [lemma, in ML_Core_Infrastructure]
typ_subst_fresh_trm_fvars [lemma, in ML_Core_Infrastructure]
typ_subst_fresh_trm_fvars [lemma, in ML_Infrastructure]
typ_subst_open [lemma, in ML_Core_Infrastructure]
typ_subst_open [lemma, in ML_Infrastructure]
typ_subst_open_vars [lemma, in ML_Core_Infrastructure]
typ_subst_open_vars [lemma, in ML_Infrastructure]
typ_subst_type [lemma, in ML_Infrastructure]
typ_subst_type [lemma, in ML_Core_Infrastructure]
typ_subst_type_list [lemma, in ML_Core_Infrastructure]
typ_subst_type_list [lemma, in ML_Infrastructure]
typ_sum [constructor, in ML_Definitions]
typ_sum [constructor, in STLC_Data_Definitions]
typ_top [constructor, in Fsub_Part1A]
typ_top [constructor, in Fsub_Definitions]
typ_unit [constructor, in ML_Definitions]
typ_unit [constructor, in STLC_Ref_Definitions]
typ_unit [constructor, in STLC_Data_Definitions]
typ_var [constructor, in STLC_Core_WF_Definitions]
typ_var [constructor, in STLC_Core_Light]
typ_var [constructor, in STLC_Data_Definitions]
typ_var [constructor, in STLC_Core_Definitions]
typ_var [constructor, in STLC_Exn_Definitions]
typ_var [constructor, in STLC_Dec_Definitions]
typ_var [constructor, in STLC_Ref_Definitions]


U

union [axiom, in Lib_MyFSetInterface]
union_1 [axiom, in Lib_MyFSetInterface]
union_2 [axiom, in Lib_MyFSetInterface]
union_3 [axiom, in Lib_MyFSetInterface]


V

value [inductive, in Fsub_Definitions]
value [inductive, in STLC_Core_WF_Definitions]
value [inductive, in STLC_Exn_Definitions]
value [inductive, in STLC_Core_Definitions]
value [inductive, in STLC_Dec_Definitions]
value [inductive, in ML_Core_Definitions]
value [inductive, in STLC_Core_Light]
value [inductive, in STLC_Data_Definitions]
value [inductive, in STLC_Ref_Definitions]
value [inductive, in ML_Definitions]
value_abs [constructor, in STLC_Data_Definitions]
value_abs [constructor, in ML_Definitions]
value_abs [constructor, in STLC_Core_Light]
value_abs [constructor, in STLC_Core_Definitions]
value_abs [constructor, in ML_Core_Definitions]
value_abs [constructor, in STLC_Ref_Definitions]
value_abs [constructor, in STLC_Dec_Definitions]
value_abs [constructor, in STLC_Exn_Definitions]
value_abs [constructor, in Fsub_Definitions]
value_abs [constructor, in STLC_Core_WF_Definitions]
value_add [constructor, in ML_Definitions]
value_add_1 [constructor, in ML_Definitions]
value_fix [constructor, in STLC_Data_Definitions]
value_fix [constructor, in ML_Definitions]
value_fv [lemma, in ML_Soundness]
value_inj1 [constructor, in ML_Definitions]
value_inj1 [constructor, in STLC_Data_Definitions]
value_inj2 [constructor, in ML_Definitions]
value_inj2 [constructor, in STLC_Data_Definitions]
value_loc [constructor, in ML_Definitions]
value_loc [constructor, in STLC_Ref_Definitions]
value_nat [constructor, in ML_Definitions]
value_pair [constructor, in STLC_Data_Definitions]
value_pair [constructor, in ML_Definitions]
value_regular [lemma, in STLC_Core_WF_Infrastructure]
value_regular [lemma, in STLC_Core_Infrastructure]
value_regular [lemma, in ML_Core_Infrastructure]
value_regular [lemma, in STLC_Exn_Infrastructure]
value_regular [lemma, in STLC_Ref_Infrastructure]
value_regular [lemma, in STLC_Data_Infrastructure]
value_regular [lemma, in STLC_Dec_Infrastructure]
value_regular [lemma, in ML_Infrastructure]
value_regular [lemma, in Fsub_Infrastructure]
value_tabs [constructor, in Fsub_Definitions]
value_to_evalue [lemma, in STLC_Core_Adequacy]
value_trm_unit [constructor, in STLC_Ref_Definitions]
value_unit [constructor, in ML_Definitions]
value_unit [constructor, in STLC_Data_Definitions]
var [axiom, in Metatheory_Var]
VARIABLES [module, in Metatheory_Var]
Variables [module, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.eq_var_dec [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.fresh [definition, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.fresh_length [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.test_pick_fresh [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.var_freshes [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.finite_nat_list_max [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.finite_nat_list_max' [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.max_lt_l [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.vars [definition, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.var_fresh [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.var_generate [definition, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.var_generate_spec [lemma, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.var [definition, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.var_default [definition, in Metatheory_Var]
VARIABLES.Var_as_OT.Import.vars [definition, in Metatheory_Var]
VARIABLES.Var_as_OT.t [definition, in Metatheory_Var]
Var_as_OT [module, in Metatheory_Var]
var_default [axiom, in Metatheory_Var]
var_fresh [axiom, in Metatheory_Var]
var_generate [axiom, in Metatheory_Var]
var_generate_spec [axiom, in Metatheory_Var]


W

wf [inductive, in CoC_Definitions]
wft [inductive, in Fsub_Part1A]
wft [inductive, in Fsub_Definitions]
wft_all [constructor, in Fsub_Definitions]
wft_all [constructor, in Fsub_Part1A]
wft_arrow [constructor, in Fsub_Part1A]
wft_arrow [constructor, in Fsub_Definitions]
wft_from_env_has_sub [lemma, in Fsub_Part1A]
wft_from_env_has_sub [lemma, in Fsub_Infrastructure]
wft_from_env_has_typ [lemma, in Fsub_Infrastructure]
wft_from_okt_sub [lemma, in Fsub_Part1A]
wft_from_okt_sub [lemma, in Fsub_Infrastructure]
wft_from_okt_typ [lemma, in Fsub_Infrastructure]
wft_narrow [lemma, in Fsub_Part1A]
wft_narrow [lemma, in Fsub_Infrastructure]
wft_open [lemma, in Fsub_Infrastructure]
wft_strengthen [lemma, in Fsub_Infrastructure]
wft_subst_tb [lemma, in Fsub_Infrastructure]
wft_top [constructor, in Fsub_Part1A]
wft_top [constructor, in Fsub_Definitions]
wft_var [constructor, in Fsub_Part1A]
wft_var [constructor, in Fsub_Definitions]
wft_weaken [lemma, in Fsub_Infrastructure]
wft_weaken [lemma, in Fsub_Part1A]
wft_weaken_right [lemma, in Fsub_Infrastructure]
wf_cons [constructor, in CoC_Definitions]
wf_left [lemma, in CoC_Infrastructure]
wf_nil [constructor, in CoC_Definitions]



Axiom Index

A

add [in Lib_MyFSetInterface]
add_1 [in Lib_MyFSetInterface]
add_2 [in Lib_MyFSetInterface]
add_3 [in Lib_MyFSetInterface]
atm [in STLC_Exn_Definitions]
atm [in STLC_Ref_Definitions]


C

cardinal [in Lib_MyFSetInterface]
cardinal_1 [in Lib_MyFSetInterface]
choose [in Lib_MyFSetInterface]
choose_1 [in Lib_MyFSetInterface]
choose_2 [in Lib_MyFSetInterface]
compare [in Lib_MyFSetInterface]


D

diff [in Lib_MyFSetInterface]
diff_1 [in Lib_MyFSetInterface]
diff_2 [in Lib_MyFSetInterface]
diff_3 [in Lib_MyFSetInterface]


E

elements [in Lib_MyFSetInterface]
elements_1 [in Lib_MyFSetInterface]
elements_2 [in Lib_MyFSetInterface]
elements_3 [in Lib_MyFSetInterface]
empty [in Lib_MyFSetInterface]
empty_1 [in Lib_MyFSetInterface]
equal [in Lib_MyFSetInterface]
equal_1 [in Lib_MyFSetInterface]
equal_2 [in Lib_MyFSetInterface]
eq_ext [in Lib_FinSet]
eq_if_Equal [in Lib_FinSet]
eq_refl [in Lib_MyFSetInterface]
eq_sym [in Lib_MyFSetInterface]
eq_trans [in Lib_MyFSetInterface]
exists_ [in Lib_MyFSetInterface]
exists_1 [in Lib_MyFSetInterface]
exists_2 [in Lib_MyFSetInterface]


F

filter [in Lib_MyFSetInterface]
filter_1 [in Lib_MyFSetInterface]
filter_2 [in Lib_MyFSetInterface]
filter_3 [in Lib_MyFSetInterface]
fold [in Lib_MyFSetInterface]
fold_1 [in Lib_MyFSetInterface]
for_all [in Lib_MyFSetInterface]
for_all_1 [in Lib_MyFSetInterface]
for_all_2 [in Lib_MyFSetInterface]


I

In [in Lib_MyFSetInterface]
inter [in Lib_MyFSetInterface]
inter_1 [in Lib_MyFSetInterface]
inter_2 [in Lib_MyFSetInterface]
inter_3 [in Lib_MyFSetInterface]
In_1 [in Lib_MyFSetInterface]
is_empty [in Lib_MyFSetInterface]
is_empty_1 [in Lib_MyFSetInterface]
is_empty_2 [in Lib_MyFSetInterface]


L

lt [in Lib_MyFSetInterface]
lt_not_eq [in Lib_MyFSetInterface]
lt_trans [in Lib_MyFSetInterface]


M

max_elt [in Lib_MyFSetInterface]
max_elt_1 [in Lib_MyFSetInterface]
max_elt_2 [in Lib_MyFSetInterface]
max_elt_3 [in Lib_MyFSetInterface]
mem [in Lib_MyFSetInterface]
mem_1 [in Lib_MyFSetInterface]
mem_2 [in Lib_MyFSetInterface]
min_elt [in Lib_MyFSetInterface]
min_elt_1 [in Lib_MyFSetInterface]
min_elt_2 [in Lib_MyFSetInterface]
min_elt_3 [in Lib_MyFSetInterface]


P

partition [in Lib_MyFSetInterface]
partition_1 [in Lib_MyFSetInterface]
partition_2 [in Lib_MyFSetInterface]


R

remove [in Lib_MyFSetInterface]
remove_1 [in Lib_MyFSetInterface]
remove_2 [in Lib_MyFSetInterface]
remove_3 [in Lib_MyFSetInterface]


S

singleton [in Lib_MyFSetInterface]
singleton_1 [in Lib_MyFSetInterface]
singleton_2 [in Lib_MyFSetInterface]
skip [in Lib_Tactic]
subset [in Lib_MyFSetInterface]
subset_1 [in Lib_MyFSetInterface]
subset_2 [in Lib_MyFSetInterface]
subst_intro [in STLC_Core_Light]
subst_open_var [in STLC_Core_Light]


T

t [in Lib_MyFSetInterface]
typ_exn [in ML_Definitions]
typ_exn_fresh [in ML_Definitions]


U

union [in Lib_MyFSetInterface]
union_1 [in Lib_MyFSetInterface]
union_2 [in Lib_MyFSetInterface]
union_3 [in Lib_MyFSetInterface]


V

var [in Metatheory_Var]
var_default [in Metatheory_Var]
var_fresh [in Metatheory_Var]
var_generate [in Metatheory_Var]
var_generate_spec [in Metatheory_Var]



Lemma Index

B

beta_church_rosser [in Lambda_ChurchRosser]
beta_red_out [in CoC_BetaStar]
beta_red_out [in Lambda_ChurchRosser]
beta_red_rename [in CoC_BetaStar]
beta_red_rename [in Lambda_ChurchRosser]
beta_star_abs [in Lambda_ChurchRosser]
beta_star_abs1 [in CoC_BetaStar]
beta_star_abs2 [in CoC_BetaStar]
beta_star_app1 [in Lambda_ChurchRosser]
beta_star_app1 [in CoC_BetaStar]
beta_star_app2 [in CoC_BetaStar]
beta_star_app2 [in Lambda_ChurchRosser]
beta_star_confluence [in Lambda_ChurchRosser]
beta_star_prod1 [in CoC_BetaStar]
beta_star_prod2 [in CoC_BetaStar]
beta_star_prod_any_inv [in CoC_Conversion]
beta_star_red_all [in CoC_BetaStar]
beta_star_red_all [in Lambda_ChurchRosser]
beta_star_red_in [in Lambda_ChurchRosser]
beta_star_red_in [in CoC_BetaStar]
beta_star_red_through [in Lambda_ChurchRosser]
beta_star_red_through [in CoC_BetaStar]
beta_star_to_para_iter [in CoC_ChurchRosser]
beta_star_to_para_iter [in Lambda_ChurchRosser]
beta_star_type_any_inv [in CoC_Conversion]
binds_typ_dec [in STLC_Dec_Decidability]
body_abs2 [in CoC_Infrastructure]
body_prod2 [in CoC_Infrastructure]
body_prove [in CoC_Infrastructure]
body_subst [in CoC_Infrastructure]
body_to_term_abs [in STLC_Dec_Infrastructure]
body_to_term_abs [in STLC_Core_Infrastructure]
body_to_term_abs [in ML_Core_Infrastructure]
body_to_term_abs [in STLC_Core_WF_Infrastructure]
body_to_term_abs [in Lambda_Infrastructure]
body_to_term_abs [in STLC_Exn_Infrastructure]
body_to_term_abs [in STLC_Data_Infrastructure]
body_to_term_abs [in ML_Infrastructure]
body_to_term_abs [in STLC_Ref_Infrastructure]
body_to_term_fix [in STLC_Data_Infrastructure]
body_to_term_fix [in ML_Infrastructure]
body_to_term_let [in ML_Infrastructure]
body_to_term_let [in ML_Core_Infrastructure]
body_to_term_match [in ML_Infrastructure]
body_to_term_match [in STLC_Data_Infrastructure]


C

canonical_form_abs [in Fsub_Soundness]
canonical_form_tabs [in Fsub_Soundness]
church_rosser_beta [in CoC_ChurchRosser]
close_var_body [in CoC_Infrastructure]
close_var_body [in Lambda_Infrastructure]
close_var_fresh [in CoC_Infrastructure]
close_var_fresh [in Lambda_Infrastructure]
close_var_open [in CoC_Infrastructure]
close_var_open [in Lambda_Infrastructure]
close_var_spec [in Lambda_Infrastructure]
close_var_spec [in CoC_Infrastructure]
confluence_beta_star [in CoC_ChurchRosser]
conv_from_beta_star [in CoC_Conversion]
conv_from_beta_star_trans [in CoC_Conversion]
conv_from_open_beta [in CoC_Conversion]
conv_prod_prod_inv [in CoC_Conversion]
conv_red_out [in CoC_Conversion]
conv_type_prod_inv [in CoC_Conversion]
conv_type_type_inv [in CoC_Conversion]
ctx_regular [in STLC_Core_WF_Infrastructure]


E

elim_incl_app [in Lib_ListFacts]
elim_incl_cons [in Lib_ListFacts]
elim_not_In_app [in Lib_ListFacts]
elim_not_In_cons [in Lib_ListFacts]
Env.binds_concat_fresh [in Metatheory_Env]
Env.binds_concat_inv [in Metatheory_Env]
Env.binds_concat_ok [in Metatheory_Env]
Env.binds_dec [in Metatheory_Env]
Env.binds_empty [in Metatheory_Env]
Env.binds_fresh [in Metatheory_Env]
Env.binds_func [in Metatheory_Env]
Env.binds_head [in Metatheory_Env]
Env.binds_inj [in Metatheory_Env]
Env.binds_map [in Metatheory_Env]
Env.binds_mid [in Metatheory_Env]
Env.binds_mid_eq [in Metatheory_Env]
Env.binds_prepend [in Metatheory_Env]
Env.binds_single_inv [in Metatheory_Env]
Env.binds_tail [in Metatheory_Env]
Env.binds_weaken [in Metatheory_Env]
Env.concat_assoc [in Metatheory_Env]
Env.concat_assoc_map_push [in Metatheory_Env]
Env.concat_empty [in Metatheory_Env]
Env.dom_concat [in Metatheory_Env]
Env.dom_cons [in Metatheory_Env]
Env.dom_empty [in Metatheory_Env]
Env.dom_map [in Metatheory_Env]
Env.dom_push [in Metatheory_Env]
Env.dom_single [in Metatheory_Env]
Env.eq_empty_inv [in Metatheory_Env]
Env.eq_push_inv [in Metatheory_Env]
Env.extends_binds [in Metatheory_Env]
Env.extends_push [in Metatheory_Env]
Env.extends_self [in Metatheory_Env]
Env.fresh_mid [in Metatheory_Env]
Env.fv_in_spec [in Metatheory_Env]
Env.iter_push_cons [in Metatheory_Env]
Env.iter_push_nil [in Metatheory_Env]
Env.map_concat [in Metatheory_Env]
Env.ok_concat_inv [in Metatheory_Env]
Env.ok_concat_iter_push [in Metatheory_Env]
Env.ok_map [in Metatheory_Env]
Env.ok_remove [in Metatheory_Env]
env_less_binds [in CoC_Preservation]
eq_typ_dec [in STLC_Dec_Decidability]
ered_to_red [in STLC_Core_Adequacy]
eterm_to_term [in STLC_Core_Adequacy]
etyping_to_typing [in STLC_Core_Adequacy]
evalue_to_value [in STLC_Core_Adequacy]


F

factorize_map [in ML_Soundness]
fails_regular [in STLC_Exn_Infrastructure]
fails_regular [in ML_Infrastructure]
fails_to_exception [in STLC_Exn_Soundness]
fails_to_exception [in ML_Soundness]
FinSet.E.S.FinSetFacts.in_empty [in Lib_FinSet]
FinSet.E.S.FinSetFacts.in_same [in Lib_FinSet]
FinSet.E.S.FinSetFacts.in_singleton [in Lib_FinSet]
FinSet.E.S.FinSetFacts.in_union [in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_empty [in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_same [in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_singleton [in Lib_FinSet]
FinSet.E.S.FinSetFacts.notin_union [in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_empty_l [in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_refl [in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_singleton [in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_trans [in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_union_l [in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_union_weak_l [in Lib_FinSet]
FinSet.E.S.FinSetFacts.subset_union_weak_r [in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_assoc [in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_comm [in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_comm_assoc [in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_empty_l [in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_empty_r [in Lib_FinSet]
FinSet.E.S.FinSetFacts.union_same [in Lib_FinSet]
fresh_empty [in Metatheory_Fresh]
fresh_length [in Metatheory_Fresh]
fresh_resize [in Metatheory_Fresh]
fresh_union_l [in Metatheory_Fresh]
fresh_union_r [in Metatheory_Fresh]
fullred_regular [in STLC_Core_FullBeta]
fv_list_map [in STLC_Data_Infrastructure]
fv_list_map [in ML_Core_Infrastructure]
fv_open_var [in CoC_Infrastructure]


H

has_scheme_from_typ [in ML_Core_Soundness]
has_scheme_from_typ [in ML_Soundness]
has_scheme_from_vars [in ML_Soundness]
has_scheme_from_vars [in ML_Core_Soundness]


I

InA_iff_In [in Lib_ListFacts]
incl_nil [in Lib_ListFacts]
incl_trans [in Lib_ListFacts]
In_incl [in Lib_ListFacts]


L

lelistA_dec [in Lib_ListFacts]
less_prod_any_inv [in CoC_Preservation]
less_prod_prod_inv [in CoC_Preservation]
less_red_out [in CoC_Preservation]
less_type_any_inv [in CoC_Preservation]
less_type_type_inv [in CoC_Preservation]
list_concat_right [in Lib_ListFactsMore]
list_forall_concat [in Lib_ListFactsMore]
list_for_n_concat [in Lib_ListFactsMore]
list_map_id [in Lib_ListFactsMore]
list_map_nth [in Lib_ListFactsMore]


M

MakeRaw.add_1 [in Lib_FinSetImpl]
MakeRaw.add_2 [in Lib_FinSetImpl]
MakeRaw.add_3 [in Lib_FinSetImpl]
MakeRaw.cardinal_1 [in Lib_FinSetImpl]
MakeRaw.choose_1 [in Lib_FinSetImpl]
MakeRaw.choose_2 [in Lib_FinSetImpl]
MakeRaw.diff_1 [in Lib_FinSetImpl]
MakeRaw.diff_2 [in Lib_FinSetImpl]
MakeRaw.diff_3 [in Lib_FinSetImpl]
MakeRaw.elements_1 [in Lib_FinSetImpl]
MakeRaw.elements_2 [in Lib_FinSetImpl]
MakeRaw.elements_3 [in Lib_FinSetImpl]
MakeRaw.empty_1 [in Lib_FinSetImpl]
MakeRaw.equal_1 [in Lib_FinSetImpl]
MakeRaw.equal_2 [in Lib_FinSetImpl]
MakeRaw.eq_refl [in Lib_FinSetImpl]
MakeRaw.eq_sym [in Lib_FinSetImpl]
MakeRaw.eq_trans [in Lib_FinSetImpl]
MakeRaw.exists_1 [in Lib_FinSetImpl]
MakeRaw.exists_2 [in Lib_FinSetImpl]
MakeRaw.filter_1 [in Lib_FinSetImpl]
MakeRaw.filter_2 [in Lib_FinSetImpl]
MakeRaw.filter_3 [in Lib_FinSetImpl]
MakeRaw.fold_1 [in Lib_FinSetImpl]
MakeRaw.for_all_1 [in Lib_FinSetImpl]
MakeRaw.for_all_2 [in Lib_FinSetImpl]
MakeRaw.inter_1 [in Lib_FinSetImpl]
MakeRaw.inter_2 [in Lib_FinSetImpl]
MakeRaw.inter_3 [in Lib_FinSetImpl]
MakeRaw.In_1 [in Lib_FinSetImpl]
MakeRaw.is_empty_1 [in Lib_FinSetImpl]
MakeRaw.is_empty_2 [in Lib_FinSetImpl]
MakeRaw.lt_not_eq [in Lib_FinSetImpl]
MakeRaw.lt_trans [in Lib_FinSetImpl]
MakeRaw.max_elt_1 [in Lib_FinSetImpl]
MakeRaw.max_elt_2 [in Lib_FinSetImpl]
MakeRaw.max_elt_3 [in Lib_FinSetImpl]
MakeRaw.mem_1 [in Lib_FinSetImpl]
MakeRaw.mem_2 [in Lib_FinSetImpl]
MakeRaw.min_elt_1 [in Lib_FinSetImpl]
MakeRaw.min_elt_2 [in Lib_FinSetImpl]
MakeRaw.min_elt_3 [in Lib_FinSetImpl]
MakeRaw.partition_1 [in Lib_FinSetImpl]
MakeRaw.partition_2 [in Lib_FinSetImpl]
MakeRaw.remove_1 [in Lib_FinSetImpl]
MakeRaw.remove_2 [in Lib_FinSetImpl]
MakeRaw.remove_3 [in Lib_FinSetImpl]
MakeRaw.singleton_1 [in Lib_FinSetImpl]
MakeRaw.singleton_2 [in Lib_FinSetImpl]
MakeRaw.subset_1 [in Lib_FinSetImpl]
MakeRaw.subset_2 [in Lib_FinSetImpl]
MakeRaw.union_1 [in Lib_FinSetImpl]
MakeRaw.union_2 [in Lib_FinSetImpl]
MakeRaw.union_3 [in Lib_FinSetImpl]
Make.Import.Import.bool_dec [in Lib_FinSetImpl]
Make.Import.Import.eq_ext [in Lib_FinSetImpl]
Make.Import.Import.eq_if_Equal [in Lib_FinSetImpl]
map_subst_tb_id [in Fsub_Infrastructure]
modus_ponens [in Lib_Tactic]


N

notin_fv_from_binds [in CoC_Infrastructure]
notin_fv_from_binds' [in CoC_Infrastructure]
notin_fv_from_wf [in CoC_Infrastructure]
notin_fv_wf [in Fsub_Infrastructure]
notin_singleton_l [in Metatheory_Fresh]
notin_singleton_r [in Metatheory_Fresh]
notin_singleton_swap [in Metatheory_Fresh]
notin_union_l [in Metatheory_Fresh]
notin_union_r [in Metatheory_Fresh]
not_InA_if_Sort_Inf [in Lib_ListFacts]
not_In_app [in Lib_ListFacts]
not_in_cons [in Lib_ListFacts]


O

okt_narrow [in Fsub_Part1A]
okt_narrow [in Fsub_Infrastructure]
okt_strengthen [in Fsub_Infrastructure]
okt_subst_tb [in Fsub_Infrastructure]
ok_from_okt [in Fsub_Infrastructure]
ok_from_okt [in Fsub_Part1A]
ok_from_wf [in CoC_Infrastructure]
ok_iter_push [in ML_Infrastructure]
open_term [in STLC_Exn_Infrastructure]
open_term [in STLC_Dec_Infrastructure]
open_term [in STLC_Core_WF_Infrastructure]
open_term [in STLC_Ref_Infrastructure]
open_term [in CoC_Infrastructure]
open_term [in Lambda_Infrastructure]
open_term [in STLC_Core_Infrastructure]
open_terms [in ML_Infrastructure]
open_terms [in STLC_Data_Infrastructure]
open_var_inj [in Lambda_Infrastructure]
open_var_inj [in CoC_Infrastructure]


P

para_abs_inv [in CoC_ChurchRosser]
para_abs_inv [in Lambda_ChurchRosser]
para_confluence [in Lambda_ChurchRosser]
para_confluence [in CoC_ChurchRosser]
para_iter_confluence [in CoC_ChurchRosser]
para_iter_confluence [in Lambda_ChurchRosser]
para_iter_parallelogram [in CoC_ChurchRosser]
para_iter_parallelogram [in Lambda_ChurchRosser]
para_iter_red_refl [in CoC_ChurchRosser]
para_iter_red_refl [in Lambda_ChurchRosser]
para_iter_to_beta_star [in CoC_ChurchRosser]
para_iter_to_beta_star [in Lambda_ChurchRosser]
para_prod_inv [in CoC_ChurchRosser]
para_red_all [in CoC_ChurchRosser]
para_red_all [in Lambda_ChurchRosser]
para_red_out [in Lambda_ChurchRosser]
para_red_out [in CoC_ChurchRosser]
para_red_refl [in CoC_ChurchRosser]
para_red_refl [in Lambda_ChurchRosser]
para_red_rename [in CoC_ChurchRosser]
para_red_rename [in Lambda_ChurchRosser]
para_red_through [in Lambda_ChurchRosser]
para_red_through [in CoC_ChurchRosser]
pattern_match_values [in ML_Soundness]
pat_match_terms [in STLC_Data_Infrastructure]
pat_match_terms [in ML_Infrastructure]
pat_typing_typ_subst [in ML_Soundness]
phi_ok_binds [in ML_Infrastructure]
preservation_for_full_reduction [in STLC_Core_FullBeta]
preservation_result [in Fsub_Soundness]
preservation_result [in STLC_Core_WF_Soundness]
preservation_result [in STLC_Ref_Soundness]
preservation_result [in ML_Soundness]
preservation_result [in STLC_Dec_Soundness]
preservation_result [in ML_Core_Soundness]
preservation_result [in STLC_Exn_Soundness]
preservation_result [in STLC_Core_Light]
preservation_result [in STLC_Data_Soundness]
preservation_result [in STLC_Core_Soundness]
progress_result [in STLC_Dec_Soundness]
progress_result [in STLC_Exn_Soundness]
progress_result [in STLC_Core_Light]
progress_result [in STLC_Core_WF_Soundness]
progress_result [in STLC_Ref_Soundness]
progress_result [in STLC_Data_Soundness]
progress_result [in ML_Soundness]
progress_result [in STLC_Core_Soundness]
progress_result [in ML_Core_Soundness]
progress_result [in Fsub_Soundness]


R

red_all_to_out [in Lambda_ChurchRosser]
red_all_to_out [in CoC_BetaStar]
red_all_to_through [in Lambda_ChurchRosser]
red_all_to_through [in CoC_BetaStar]
red_out_to_rename [in CoC_BetaStar]
red_out_to_rename [in Lambda_ChurchRosser]
red_regular [in STLC_Data_Infrastructure]
red_regular [in STLC_Core_WF_Infrastructure]
red_regular [in STLC_Dec_Infrastructure]
red_regular [in ML_Infrastructure]
red_regular [in STLC_Ref_Infrastructure]
red_regular [in STLC_Core_Infrastructure]
red_regular [in STLC_Exn_Infrastructure]
red_regular [in Fsub_Infrastructure]
red_regular [in ML_Core_Infrastructure]
red_regular_beta [in Lambda_Infrastructure]
red_regular_beta [in CoC_Infrastructure]
red_regular_beta_star [in CoC_Infrastructure]
red_regular_beta_star [in Lambda_Infrastructure]
red_regular_conv [in CoC_Infrastructure]
red_regular_less [in CoC_Infrastructure]
red_regular_para [in Lambda_Infrastructure]
red_regular_para [in CoC_ChurchRosser]
red_regular_para_iter [in Lambda_Infrastructure]
red_regular_para_iter [in CoC_ChurchRosser]
red_to_ered [in STLC_Core_Adequacy]
red_value_false [in ML_Soundness]
regular_typing [in CoC_Infrastructure]


S

sch_open_types [in ML_Infrastructure]
sch_open_types [in ML_Core_Infrastructure]
sch_subst_arity [in ML_Infrastructure]
sch_subst_arity [in ML_Core_Infrastructure]
sch_subst_fold [in ML_Core_Infrastructure]
sch_subst_fold [in ML_Infrastructure]
sch_subst_fresh [in ML_Core_Infrastructure]
sch_subst_fresh [in ML_Infrastructure]
sch_subst_open [in ML_Core_Infrastructure]
sch_subst_open [in ML_Infrastructure]
sch_subst_open_vars [in ML_Core_Infrastructure]
sch_subst_open_vars [in ML_Infrastructure]
sch_subst_type [in ML_Infrastructure]
sch_subst_type [in ML_Core_Infrastructure]
sort_dec [in Lib_ListFacts]
Sort_eq_head [in Lib_ListFacts]
Sort_InA_eq_ext [in Lib_ListFacts]
sto_ok_binds [in ML_Infrastructure]
sto_ok_binds [in STLC_Ref_Infrastructure]
sto_typing_push [in ML_Soundness]
sto_typing_push [in STLC_Ref_Soundness]
subject_reduction_ind [in CoC_Preservation]
subject_reduction_result [in CoC_Preservation]
subject_reduction_star_result [in CoC_Preservation]
substs_fresh [in ML_Infrastructure]
substs_fresh [in STLC_Data_Infrastructure]
substs_intro [in STLC_Data_Infrastructure]
substs_intro [in ML_Infrastructure]
substs_intro_ind [in STLC_Data_Infrastructure]
substs_intro_ind [in ML_Infrastructure]
substs_terms [in STLC_Data_Infrastructure]
substs_terms [in ML_Infrastructure]
subst_body [in Lambda_Infrastructure]
subst_bodys [in ML_Infrastructure]
subst_ee_fresh [in Fsub_Infrastructure]
subst_ee_intro [in Fsub_Infrastructure]
subst_ee_open_ee [in Fsub_Infrastructure]
subst_ee_open_ee_var [in Fsub_Infrastructure]
subst_ee_open_te_var [in Fsub_Infrastructure]
subst_ee_term [in Fsub_Infrastructure]
subst_fresh [in STLC_Data_Infrastructure]
subst_fresh [in STLC_Exn_Infrastructure]
subst_fresh [in Lambda_Infrastructure]
subst_fresh [in STLC_Ref_Infrastructure]
subst_fresh [in STLC_Core_WF_Infrastructure]
subst_fresh [in ML_Infrastructure]
subst_fresh [in STLC_Dec_Infrastructure]
subst_fresh [in STLC_Core_Infrastructure]
subst_fresh [in CoC_Infrastructure]
subst_fresh_list [in ML_Infrastructure]
subst_fresh_list [in STLC_Data_Infrastructure]
subst_fresh_trm_fvars [in ML_Infrastructure]
subst_fresh_trm_fvars [in STLC_Data_Infrastructure]
subst_intro [in STLC_Core_WF_Infrastructure]
subst_intro [in Lambda_Infrastructure]
subst_intro [in STLC_Ref_Infrastructure]
subst_intro [in STLC_Dec_Infrastructure]
subst_intro [in CoC_Infrastructure]
subst_intro [in STLC_Core_Infrastructure]
subst_intro [in STLC_Exn_Infrastructure]
subst_open [in STLC_Ref_Infrastructure]
subst_open [in Lambda_Infrastructure]
subst_open [in ML_Infrastructure]
subst_open [in STLC_Core_WF_Infrastructure]
subst_open [in STLC_Core_Infrastructure]
subst_open [in STLC_Data_Infrastructure]
subst_open [in STLC_Exn_Infrastructure]
subst_open [in STLC_Dec_Infrastructure]
subst_open [in CoC_Infrastructure]
subst_open_var [in STLC_Exn_Infrastructure]
subst_open_var [in CoC_Infrastructure]
subst_open_var [in Lambda_Infrastructure]
subst_open_var [in STLC_Ref_Infrastructure]
subst_open_var [in STLC_Dec_Infrastructure]
subst_open_var [in STLC_Core_Infrastructure]
subst_open_var [in STLC_Core_WF_Infrastructure]
subst_open_vars [in STLC_Data_Infrastructure]
subst_open_vars [in ML_Infrastructure]
subst_term [in STLC_Dec_Infrastructure]
subst_term [in ML_Infrastructure]
subst_term [in Lambda_Infrastructure]
subst_term [in STLC_Exn_Infrastructure]
subst_term [in STLC_Core_WF_Infrastructure]
subst_term [in STLC_Core_Infrastructure]
subst_term [in STLC_Data_Infrastructure]
subst_term [in CoC_Infrastructure]
subst_term [in STLC_Ref_Infrastructure]
subst_te_fresh [in Fsub_Infrastructure]
subst_te_intro [in Fsub_Infrastructure]
subst_te_open_ee_var [in Fsub_Infrastructure]
subst_te_open_te [in Fsub_Infrastructure]
subst_te_open_te_var [in Fsub_Infrastructure]
subst_te_term [in Fsub_Infrastructure]
subst_tt_fresh [in Fsub_Infrastructure]
subst_tt_intro [in Fsub_Infrastructure]
subst_tt_open_tt [in Fsub_Infrastructure]
subst_tt_open_tt_var [in Fsub_Infrastructure]
subst_tt_type [in Fsub_Infrastructure]
sub_narrowing [in Fsub_Soundness]
sub_narrowing [in Fsub_Part1A]
sub_narrowing_aux [in Fsub_Soundness]
sub_narrowing_aux [in Fsub_Part1A]
sub_reflexivity [in Fsub_Part1A]
sub_reflexivity [in Fsub_Soundness]
sub_regular [in Fsub_Part1A]
sub_regular [in Fsub_Infrastructure]
sub_strengthening [in Fsub_Soundness]
sub_through_subst_tt [in Fsub_Soundness]
sub_transitivity [in Fsub_Part1A]
sub_transitivity [in Fsub_Soundness]
sub_weakening [in Fsub_Soundness]
sub_weakening [in Fsub_Part1A]


T

term_abs1 [in CoC_Infrastructure]
term_abs_prove [in CoC_Infrastructure]
term_abs_to_body [in Lambda_Infrastructure]
term_abs_to_body [in STLC_Exn_Infrastructure]
term_abs_to_body [in ML_Core_Infrastructure]
term_abs_to_body [in STLC_Core_Infrastructure]
term_abs_to_body [in STLC_Ref_Infrastructure]
term_abs_to_body [in ML_Infrastructure]
term_abs_to_body [in STLC_Data_Infrastructure]
term_abs_to_body [in STLC_Core_WF_Infrastructure]
term_abs_to_body [in STLC_Dec_Infrastructure]
term_fix_to_body [in ML_Infrastructure]
term_fix_to_body [in STLC_Data_Infrastructure]
term_from_binds_in_wf [in CoC_Infrastructure]
term_let_to_body [in ML_Infrastructure]
term_let_to_body [in ML_Core_Infrastructure]
term_match_to_body [in STLC_Data_Infrastructure]
term_match_to_body [in ML_Infrastructure]
term_prod_prove [in CoC_Infrastructure]
term_rename [in STLC_Core_Adequacy]
term_to_eterm [in STLC_Core_Adequacy]
test_fresh_solve_1 [in Metatheory_Fresh]
test_fresh_solve_2 [in Metatheory_Fresh]
test_fresh_solve_3 [in Metatheory_Fresh]
test_fresh_solve_4 [in Metatheory_Fresh]
test_neq_solve [in Metatheory_Fresh]
test_notin_contradiction [in Metatheory_Fresh]
test_notin_solve_1 [in Metatheory_Fresh]
test_notin_solve_2 [in Metatheory_Fresh]
test_notin_solve_3 [in Metatheory_Fresh]
trm_def_fresh [in ML_Infrastructure]
trm_def_fresh [in STLC_Data_Infrastructure]
trm_fv_list_map [in ML_Infrastructure]
trm_open_term [in ML_Core_Infrastructure]
trm_subst_fresh [in ML_Core_Infrastructure]
trm_subst_intro [in ML_Core_Infrastructure]
trm_subst_open [in ML_Core_Infrastructure]
trm_subst_open_var [in ML_Core_Infrastructure]
trm_subst_term [in ML_Core_Infrastructure]
type_from_wft [in Fsub_Part1A]
type_from_wft [in Fsub_Infrastructure]
typings_concat [in ML_Infrastructure]
typings_concat [in STLC_Data_Infrastructure]
typing_abs_inv [in CoC_Preservation]
typing_dec' [in STLC_Dec_Decidability]
typing_fresh [in CoC_Infrastructure]
typing_inv_abs [in Fsub_Soundness]
typing_inv_tabs [in Fsub_Soundness]
typing_narrowing [in Fsub_Soundness]
typing_pattern_match [in ML_Soundness]
typing_pattern_match [in STLC_Data_Soundness]
typing_prod_inv [in CoC_Preservation]
typing_prod_type_inv [in CoC_Preservation]
typing_regular [in ML_Infrastructure]
typing_regular [in STLC_Core_Infrastructure]
typing_regular [in STLC_Core_WF_Infrastructure]
typing_regular [in STLC_Ref_Infrastructure]
typing_regular [in STLC_Data_Infrastructure]
typing_regular [in STLC_Exn_Infrastructure]
typing_regular [in STLC_Dec_Infrastructure]
typing_regular [in Fsub_Infrastructure]
typing_regular [in ML_Core_Infrastructure]
typing_rename [in STLC_Core_Adequacy]
typing_rename [in STLC_Dec_Decidability]
typing_stability [in ML_Soundness]
typing_stability [in STLC_Ref_Soundness]
typing_subst [in STLC_Core_WF_Soundness]
typing_subst [in STLC_Dec_Soundness]
typing_subst [in STLC_Ref_Soundness]
typing_subst [in STLC_Data_Soundness]
typing_subst [in STLC_Exn_Soundness]
typing_subst [in STLC_Core_Light]
typing_subst [in STLC_Core_Soundness]
typing_substitution [in CoC_Preservation]
typing_substs [in STLC_Data_Soundness]
typing_sub_env [in CoC_Preservation]
typing_through_subst_ee [in Fsub_Soundness]
typing_through_subst_te [in Fsub_Soundness]
typing_to_etyping [in STLC_Core_Adequacy]
typing_trm_subst [in ML_Core_Soundness]
typing_trm_subst [in ML_Soundness]
typing_trm_substs [in ML_Soundness]
typing_typ_subst [in ML_Core_Soundness]
typing_typ_subst [in ML_Soundness]
typing_typ_substs [in ML_Soundness]
typing_typ_substs [in ML_Core_Soundness]
typing_weaken [in STLC_Exn_Soundness]
typing_weaken [in STLC_Data_Soundness]
typing_weaken [in STLC_Core_Light]
typing_weaken [in CoC_Preservation]
typing_weaken [in STLC_Core_WF_Soundness]
typing_weaken [in ML_Core_Soundness]
typing_weaken [in STLC_Dec_Soundness]
typing_weaken [in STLC_Core_Soundness]
typing_weaken [in STLC_Ref_Soundness]
typing_weaken [in ML_Soundness]
typing_weakening [in Fsub_Soundness]
typing_wf_from_context [in CoC_Preservation]
typing_wf_from_typing [in CoC_Preservation]
typ_def_fresh [in ML_Core_Infrastructure]
typ_def_fresh [in ML_Infrastructure]
typ_fv_list_map [in ML_Infrastructure]
typ_open_type [in ML_Core_Infrastructure]
typ_open_type [in ML_Infrastructure]
typ_open_types [in ML_Core_Infrastructure]
typ_open_types [in ML_Infrastructure]
typ_substs_fresh [in ML_Infrastructure]
typ_substs_fresh [in ML_Core_Infrastructure]
typ_substs_intro [in ML_Core_Infrastructure]
typ_substs_intro [in ML_Infrastructure]
typ_substs_intro_ind [in ML_Core_Infrastructure]
typ_substs_intro_ind [in ML_Infrastructure]
typ_substs_types [in ML_Core_Infrastructure]
typ_substs_types [in ML_Infrastructure]
typ_subst_fresh [in ML_Infrastructure]
typ_subst_fresh [in ML_Core_Infrastructure]
typ_subst_fresh_list [in ML_Infrastructure]
typ_subst_fresh_list [in ML_Core_Infrastructure]
typ_subst_fresh_trm_fvars [in ML_Core_Infrastructure]
typ_subst_fresh_trm_fvars [in ML_Infrastructure]
typ_subst_open [in ML_Core_Infrastructure]
typ_subst_open [in ML_Infrastructure]
typ_subst_open_vars [in ML_Core_Infrastructure]
typ_subst_open_vars [in ML_Infrastructure]
typ_subst_type [in ML_Infrastructure]
typ_subst_type [in ML_Core_Infrastructure]
typ_subst_type_list [in ML_Core_Infrastructure]
typ_subst_type_list [in ML_Infrastructure]


V

value_fv [in ML_Soundness]
value_regular [in STLC_Core_WF_Infrastructure]
value_regular [in STLC_Core_Infrastructure]
value_regular [in ML_Core_Infrastructure]
value_regular [in STLC_Exn_Infrastructure]
value_regular [in STLC_Ref_Infrastructure]
value_regular [in STLC_Data_Infrastructure]
value_regular [in STLC_Dec_Infrastructure]
value_regular [in ML_Infrastructure]
value_regular [in Fsub_Infrastructure]
value_to_evalue [in STLC_Core_Adequacy]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.eq_var_dec [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.fresh_length [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.test_pick_fresh [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.var_freshes [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.finite_nat_list_max [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.finite_nat_list_max' [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.max_lt_l [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.var_fresh [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.var_generate_spec [in Metatheory_Var]


W

wft_from_env_has_sub [in Fsub_Part1A]
wft_from_env_has_sub [in Fsub_Infrastructure]
wft_from_env_has_typ [in Fsub_Infrastructure]
wft_from_okt_sub [in Fsub_Part1A]
wft_from_okt_sub [in Fsub_Infrastructure]
wft_from_okt_typ [in Fsub_Infrastructure]
wft_narrow [in Fsub_Part1A]
wft_narrow [in Fsub_Infrastructure]
wft_open [in Fsub_Infrastructure]
wft_strengthen [in Fsub_Infrastructure]
wft_subst_tb [in Fsub_Infrastructure]
wft_weaken [in Fsub_Infrastructure]
wft_weaken [in Fsub_Part1A]
wft_weaken_right [in Fsub_Infrastructure]
wf_left [in CoC_Infrastructure]



Constructor Index

B

beta_abs [in Lambda_Definitions]
beta_abs1 [in CoC_Definitions]
beta_abs2 [in CoC_Definitions]
beta_app1 [in Lambda_Definitions]
beta_app1 [in CoC_Definitions]
beta_app2 [in Lambda_Definitions]
beta_app2 [in CoC_Definitions]
beta_prod1 [in CoC_Definitions]
beta_prod2 [in CoC_Definitions]
beta_red [in CoC_Definitions]
beta_red [in Lambda_Definitions]
bind_sub [in Fsub_Part1A]
bind_sub [in Fsub_Definitions]
bind_typ [in Fsub_Definitions]


C

ctx_app_1 [in STLC_Core_WF_Definitions]
ctx_app_2 [in STLC_Core_WF_Definitions]
ctx_hole [in STLC_Core_WF_Definitions]


E

Env.ok_empty [in Metatheory_Env]
Env.ok_push [in Metatheory_Env]
env_less_head [in CoC_Preservation]
env_less_tail [in CoC_Preservation]
equiv_refl [in CoC_Definitions]
equiv_refl [in Lambda_Definitions]
equiv_step [in CoC_Definitions]
equiv_step [in Lambda_Definitions]
equiv_sym [in CoC_Definitions]
equiv_sym [in Lambda_Definitions]
equiv_trans [in Lambda_Definitions]
equiv_trans [in CoC_Definitions]
ered_app_1 [in STLC_Core_Adequacy]
ered_app_2 [in STLC_Core_Adequacy]
ered_beta [in STLC_Core_Adequacy]
eterm_abs [in STLC_Core_Adequacy]
eterm_app [in STLC_Core_Adequacy]
eterm_var [in STLC_Core_Adequacy]
etyping_abs [in STLC_Core_Adequacy]
etyping_app [in STLC_Core_Adequacy]
etyping_var [in STLC_Core_Adequacy]
evalue_abs [in STLC_Core_Adequacy]


F

fails_app_1 [in ML_Definitions]
fails_app_1 [in STLC_Exn_Definitions]
fails_app_2 [in ML_Definitions]
fails_app_2 [in STLC_Exn_Definitions]
fails_get_1 [in ML_Definitions]
fails_inj_1 [in ML_Definitions]
fails_inj_2 [in ML_Definitions]
fails_let_1 [in ML_Definitions]
fails_mat_1 [in ML_Definitions]
fails_new_1 [in ML_Definitions]
fails_pair_1 [in ML_Definitions]
fails_pair_2 [in ML_Definitions]
fails_raise_val [in STLC_Exn_Definitions]
fails_raise_val [in ML_Definitions]
fails_raise_1 [in ML_Definitions]
fails_raise_1 [in STLC_Exn_Definitions]
fails_set_1 [in ML_Definitions]
fails_set_2 [in ML_Definitions]
fullred_abs [in STLC_Core_FullBeta]
fullred_app1 [in STLC_Core_FullBeta]
fullred_app2 [in STLC_Core_FullBeta]
fullred_red [in STLC_Core_FullBeta]


I

iter_step [in CoC_ChurchRosser]
iter_step [in Lambda_Infrastructure]
iter_trans [in Lambda_Infrastructure]
iter_trans [in CoC_ChurchRosser]


L

less_conv [in CoC_Definitions]
less_prod [in CoC_Definitions]
less_refl [in CoC_Definitions]
less_trans [in CoC_Definitions]
less_univ [in CoC_Definitions]
list_forall_cons [in Lib_ListFactsMore]
list_forall_nil [in Lib_ListFactsMore]


O

okt_empty [in Fsub_Part1A]
okt_empty [in Fsub_Definitions]
okt_sub [in Fsub_Definitions]
okt_sub [in Fsub_Part1A]
okt_typ [in Fsub_Definitions]


P

para_abs [in Lambda_Infrastructure]
para_abs [in CoC_ChurchRosser]
para_app [in Lambda_Infrastructure]
para_app [in CoC_ChurchRosser]
para_prod [in CoC_ChurchRosser]
para_red [in Lambda_Infrastructure]
para_red [in CoC_ChurchRosser]
para_srt [in CoC_ChurchRosser]
para_var [in Lambda_Infrastructure]
para_var [in CoC_ChurchRosser]
pat_bvar [in ML_Definitions]
pat_bvar [in STLC_Data_Definitions]
pat_inj1 [in ML_Definitions]
pat_inj1 [in STLC_Data_Definitions]
pat_inj2 [in STLC_Data_Definitions]
pat_inj2 [in ML_Definitions]
pat_pair [in ML_Definitions]
pat_pair [in STLC_Data_Definitions]
pat_typing_bvar [in ML_Definitions]
pat_typing_bvar [in STLC_Data_Definitions]
pat_typing_inj1 [in ML_Definitions]
pat_typing_inj1 [in STLC_Data_Definitions]
pat_typing_inj2 [in ML_Definitions]
pat_typing_inj2 [in STLC_Data_Definitions]
pat_typing_pair [in STLC_Data_Definitions]
pat_typing_pair [in ML_Definitions]
pat_typing_unit [in ML_Definitions]
pat_typing_unit [in STLC_Data_Definitions]
pat_typing_wild [in ML_Definitions]
pat_typing_wild [in STLC_Data_Definitions]
pat_unit [in ML_Definitions]
pat_unit [in STLC_Data_Definitions]
pat_wild [in STLC_Data_Definitions]
pat_wild [in ML_Definitions]
phi_ok_empty [in ML_Definitions]
phi_ok_push [in ML_Definitions]


R

red_abs [in Fsub_Definitions]
red_abs [in ML_Core_Definitions]
red_add [in ML_Definitions]
red_app_1 [in Fsub_Definitions]
red_app_1 [in STLC_Core_Light]
red_app_1 [in ML_Core_Definitions]
red_app_1 [in STLC_Data_Definitions]
red_app_1 [in STLC_Ref_Definitions]
red_app_1 [in STLC_Core_Definitions]
red_app_1 [in ML_Definitions]
red_app_1 [in STLC_Dec_Definitions]
red_app_1 [in STLC_Exn_Definitions]
red_app_2 [in STLC_Core_Definitions]
red_app_2 [in STLC_Core_Light]
red_app_2 [in Fsub_Definitions]
red_app_2 [in ML_Core_Definitions]
red_app_2 [in STLC_Dec_Definitions]
red_app_2 [in ML_Definitions]
red_app_2 [in STLC_Ref_Definitions]
red_app_2 [in STLC_Exn_Definitions]
red_app_2 [in STLC_Data_Definitions]
red_beta [in STLC_Ref_Definitions]
red_beta [in STLC_Core_Light]
red_beta [in STLC_Core_WF_Definitions]
red_beta [in STLC_Exn_Definitions]
red_beta [in STLC_Core_Definitions]
red_beta [in ML_Definitions]
red_beta [in STLC_Data_Definitions]
red_beta [in STLC_Dec_Definitions]
red_catch_exn [in STLC_Exn_Definitions]
red_catch_exn [in ML_Definitions]
red_catch_val [in ML_Definitions]
red_catch_val [in STLC_Exn_Definitions]
red_catch_2 [in STLC_Exn_Definitions]
red_catch_2 [in ML_Definitions]
red_ctx [in STLC_Core_WF_Definitions]
red_fix [in STLC_Data_Definitions]
red_fix [in ML_Definitions]
red_get [in ML_Definitions]
red_get [in STLC_Ref_Definitions]
red_get_1 [in STLC_Ref_Definitions]
red_get_1 [in ML_Definitions]
red_inj1_1 [in STLC_Data_Definitions]
red_inj1_1 [in ML_Definitions]
red_inj2_1 [in ML_Definitions]
red_inj2_1 [in STLC_Data_Definitions]
red_let [in ML_Core_Definitions]
red_let [in ML_Definitions]
red_let_1 [in ML_Core_Definitions]
red_match_none [in ML_Definitions]
red_match_none [in STLC_Data_Definitions]
red_match_some [in ML_Definitions]
red_match_some [in STLC_Data_Definitions]
red_match_1 [in STLC_Data_Definitions]
red_match_1 [in ML_Definitions]
red_new [in ML_Definitions]
red_new [in STLC_Ref_Definitions]
red_new_1 [in STLC_Ref_Definitions]
red_new_1 [in ML_Definitions]
red_pair_1 [in STLC_Data_Definitions]
red_pair_1 [in ML_Definitions]
red_pair_2 [in STLC_Data_Definitions]
red_pair_2 [in ML_Definitions]
red_raise_1 [in STLC_Exn_Definitions]
red_raise_1 [in ML_Definitions]
red_set [in STLC_Ref_Definitions]
red_set [in ML_Definitions]
red_set_1 [in ML_Definitions]
red_set_1 [in STLC_Ref_Definitions]
red_set_2 [in STLC_Ref_Definitions]
red_set_2 [in ML_Definitions]
red_tabs [in Fsub_Definitions]
red_tapp [in Fsub_Definitions]


S

star_refl [in CoC_Definitions]
star_refl [in Lambda_Definitions]
star_step [in Lambda_Definitions]
star_step [in CoC_Definitions]
star_trans [in CoC_Definitions]
star_trans [in Lambda_Definitions]
sto_ok_empty [in STLC_Ref_Definitions]
sto_ok_empty [in ML_Definitions]
sto_ok_push [in STLC_Ref_Definitions]
sto_ok_push [in ML_Definitions]
sub_all [in Fsub_Definitions]
sub_all [in Fsub_Part1A]
sub_arrow [in Fsub_Definitions]
sub_arrow [in Fsub_Part1A]
sub_refl_tvar [in Fsub_Part1A]
sub_refl_tvar [in Fsub_Definitions]
sub_top [in Fsub_Definitions]
sub_top [in Fsub_Part1A]
sub_trans_tvar [in Fsub_Definitions]
sub_trans_tvar [in Fsub_Part1A]


T

term_abs [in STLC_Core_Light]
term_abs [in STLC_Core_WF_Definitions]
term_abs [in Fsub_Definitions]
term_abs [in Lambda_Definitions]
term_abs [in STLC_Core_Definitions]
term_abs [in ML_Core_Definitions]
term_abs [in STLC_Data_Definitions]
term_abs [in CoC_Definitions]
term_abs [in STLC_Exn_Definitions]
term_abs [in STLC_Ref_Definitions]
term_abs [in STLC_Dec_Definitions]
term_abs [in ML_Definitions]
term_add [in ML_Definitions]
term_app [in Fsub_Definitions]
term_app [in STLC_Data_Definitions]
term_app [in STLC_Core_Light]
term_app [in CoC_Definitions]
term_app [in Lambda_Definitions]
term_app [in STLC_Core_Definitions]
term_app [in STLC_Exn_Definitions]
term_app [in STLC_Ref_Definitions]
term_app [in STLC_Dec_Definitions]
term_app [in ML_Definitions]
term_app [in STLC_Core_WF_Definitions]
term_app [in ML_Core_Definitions]
term_catch [in STLC_Exn_Definitions]
term_catch [in ML_Definitions]
term_fix [in STLC_Data_Definitions]
term_fix [in ML_Definitions]
term_get [in ML_Definitions]
term_get [in STLC_Ref_Definitions]
term_inj1 [in ML_Definitions]
term_inj1 [in STLC_Data_Definitions]
term_inj2 [in STLC_Data_Definitions]
term_inj2 [in ML_Definitions]
term_let [in ML_Core_Definitions]
term_let [in ML_Definitions]
term_loc [in STLC_Ref_Definitions]
term_loc [in ML_Definitions]
term_match [in STLC_Data_Definitions]
term_match [in ML_Definitions]
term_nat [in ML_Definitions]
term_new [in STLC_Ref_Definitions]
term_new [in ML_Definitions]
term_pair [in STLC_Data_Definitions]
term_pair [in ML_Definitions]
term_prod [in CoC_Definitions]
term_raise [in STLC_Exn_Definitions]
term_raise [in ML_Definitions]
term_set [in STLC_Ref_Definitions]
term_set [in ML_Definitions]
term_tabs [in Fsub_Definitions]
term_tapp [in Fsub_Definitions]
term_trm_unit [in STLC_Ref_Definitions]
term_type [in CoC_Definitions]
term_unit [in ML_Definitions]
term_unit [in STLC_Data_Definitions]
term_var [in CoC_Definitions]
term_var [in ML_Definitions]
term_var [in STLC_Dec_Definitions]
term_var [in STLC_Core_Definitions]
term_var [in Fsub_Definitions]
term_var [in Lambda_Definitions]
term_var [in STLC_Data_Definitions]
term_var [in ML_Core_Definitions]
term_var [in STLC_Core_WF_Definitions]
term_var [in STLC_Exn_Definitions]
term_var [in STLC_Ref_Definitions]
term_var [in STLC_Core_Light]
trm_abs [in CoC_Definitions]
trm_abs [in STLC_Core_Definitions]
trm_abs [in ML_Definitions]
trm_abs [in STLC_Core_WF_Definitions]
trm_abs [in STLC_Core_Light]
trm_abs [in Lambda_Definitions]
trm_abs [in ML_Core_Definitions]
trm_abs [in STLC_Ref_Definitions]
trm_abs [in STLC_Dec_Definitions]
trm_abs [in STLC_Data_Definitions]
trm_abs [in STLC_Exn_Definitions]
trm_abs [in Fsub_Definitions]
trm_add [in ML_Definitions]
trm_app [in Lambda_Definitions]
trm_app [in ML_Core_Definitions]
trm_app [in ML_Definitions]
trm_app [in STLC_Data_Definitions]
trm_app [in STLC_Ref_Definitions]
trm_app [in STLC_Core_WF_Definitions]
trm_app [in STLC_Core_Definitions]
trm_app [in STLC_Dec_Definitions]
trm_app [in STLC_Core_Light]
trm_app [in Fsub_Definitions]
trm_app [in CoC_Definitions]
trm_app [in STLC_Exn_Definitions]
trm_bvar [in STLC_Core_WF_Definitions]
trm_bvar [in Fsub_Definitions]
trm_bvar [in Lambda_Definitions]
trm_bvar [in ML_Definitions]
trm_bvar [in STLC_Ref_Definitions]
trm_bvar [in CoC_Definitions]
trm_bvar [in STLC_Dec_Definitions]
trm_bvar [in ML_Core_Definitions]
trm_bvar [in STLC_Core_Definitions]
trm_bvar [in STLC_Data_Definitions]
trm_bvar [in STLC_Exn_Definitions]
trm_bvar [in STLC_Core_Light]
trm_catch [in ML_Definitions]
trm_catch [in STLC_Exn_Definitions]
trm_fix [in STLC_Data_Definitions]
trm_fix [in ML_Definitions]
trm_fvar [in STLC_Core_WF_Definitions]
trm_fvar [in Lambda_Definitions]
trm_fvar [in Fsub_Definitions]
trm_fvar [in STLC_Data_Definitions]
trm_fvar [in STLC_Ref_Definitions]
trm_fvar [in STLC_Core_Definitions]
trm_fvar [in ML_Core_Definitions]
trm_fvar [in STLC_Dec_Definitions]
trm_fvar [in ML_Definitions]
trm_fvar [in STLC_Core_Light]
trm_fvar [in STLC_Exn_Definitions]
trm_fvar [in CoC_Definitions]
trm_get [in ML_Definitions]
trm_get [in STLC_Ref_Definitions]
trm_inj1 [in STLC_Data_Definitions]
trm_inj1 [in ML_Definitions]
trm_inj2 [in ML_Definitions]
trm_inj2 [in STLC_Data_Definitions]
trm_let [in ML_Core_Definitions]
trm_let [in ML_Definitions]
trm_loc [in STLC_Ref_Definitions]
trm_loc [in ML_Definitions]
trm_match [in ML_Definitions]
trm_match [in STLC_Data_Definitions]
trm_nat [in ML_Definitions]
trm_pair [in ML_Definitions]
trm_pair [in STLC_Data_Definitions]
trm_prod [in CoC_Definitions]
trm_raise [in STLC_Exn_Definitions]
trm_raise [in ML_Definitions]
trm_ref [in STLC_Ref_Definitions]
trm_ref [in ML_Definitions]
trm_set [in STLC_Ref_Definitions]
trm_set [in ML_Definitions]
trm_tabs [in Fsub_Definitions]
trm_tapp [in Fsub_Definitions]
trm_type [in CoC_Definitions]
trm_unit [in ML_Definitions]
trm_unit [in STLC_Ref_Definitions]
trm_unit [in STLC_Data_Definitions]
type_all [in Fsub_Definitions]
type_all [in Fsub_Part1A]
type_arrow [in ML_Definitions]
type_arrow [in Fsub_Definitions]
type_arrow [in Fsub_Part1A]
type_arrow [in ML_Core_Definitions]
type_fvar [in ML_Core_Definitions]
type_fvar [in ML_Definitions]
type_nat [in ML_Definitions]
type_prod [in ML_Definitions]
type_ref [in ML_Definitions]
type_sum [in ML_Definitions]
type_top [in Fsub_Definitions]
type_top [in Fsub_Part1A]
type_unit [in ML_Definitions]
type_var [in Fsub_Definitions]
type_var [in Fsub_Part1A]
typings_cons [in STLC_Data_Infrastructure]
typings_cons [in ML_Infrastructure]
typings_nil [in ML_Infrastructure]
typings_nil [in STLC_Data_Infrastructure]
typing_abs [in STLC_Dec_Definitions]
typing_abs [in STLC_Ref_Definitions]
typing_abs [in STLC_Core_Definitions]
typing_abs [in ML_Definitions]
typing_abs [in STLC_Core_WF_Definitions]
typing_abs [in Fsub_Definitions]
typing_abs [in CoC_Definitions]
typing_abs [in STLC_Core_Light]
typing_abs [in STLC_Data_Definitions]
typing_abs [in ML_Core_Definitions]
typing_abs [in STLC_Exn_Definitions]
typing_app [in Fsub_Definitions]
typing_app [in STLC_Exn_Definitions]
typing_app [in CoC_Definitions]
typing_app [in STLC_Core_Definitions]
typing_app [in STLC_Data_Definitions]
typing_app [in STLC_Core_WF_Definitions]
typing_app [in ML_Core_Definitions]
typing_app [in STLC_Dec_Definitions]
typing_app [in STLC_Ref_Definitions]
typing_app [in STLC_Core_Light]
typing_catch [in STLC_Exn_Definitions]
typing_fix [in STLC_Data_Definitions]
typing_fix [in ML_Definitions]
typing_get [in STLC_Ref_Definitions]
typing_inj1 [in STLC_Data_Definitions]
typing_inj2 [in STLC_Data_Definitions]
typing_let [in ML_Core_Definitions]
typing_let [in ML_Definitions]
typing_loc [in STLC_Ref_Definitions]
typing_match [in ML_Definitions]
typing_match [in STLC_Data_Definitions]
typing_new [in STLC_Ref_Definitions]
typing_pair [in STLC_Data_Definitions]
typing_prod [in CoC_Definitions]
typing_raise [in STLC_Exn_Definitions]
typing_set [in STLC_Ref_Definitions]
typing_sub [in CoC_Definitions]
typing_sub [in Fsub_Definitions]
typing_tabs [in Fsub_Definitions]
typing_tapp [in Fsub_Definitions]
typing_trm_unit [in STLC_Ref_Definitions]
typing_type [in CoC_Definitions]
typing_unit [in STLC_Data_Definitions]
typing_var [in CoC_Definitions]
typing_var [in STLC_Core_WF_Definitions]
typing_var [in STLC_Dec_Definitions]
typing_var [in Fsub_Definitions]
typing_var [in STLC_Data_Definitions]
typing_var [in ML_Core_Definitions]
typing_var [in ML_Definitions]
typing_var [in STLC_Ref_Definitions]
typing_var [in STLC_Exn_Definitions]
typing_var [in STLC_Core_Light]
typing_var [in STLC_Core_Definitions]
typ_all [in Fsub_Part1A]
typ_all [in Fsub_Definitions]
typ_arrow [in STLC_Exn_Definitions]
typ_arrow [in STLC_Ref_Definitions]
typ_arrow [in STLC_Core_WF_Definitions]
typ_arrow [in STLC_Core_Definitions]
typ_arrow [in Fsub_Definitions]
typ_arrow [in STLC_Core_Light]
typ_arrow [in STLC_Dec_Definitions]
typ_arrow [in ML_Core_Definitions]
typ_arrow [in Fsub_Part1A]
typ_arrow [in ML_Definitions]
typ_arrow [in STLC_Data_Definitions]
typ_bvar [in ML_Definitions]
typ_bvar [in ML_Core_Definitions]
typ_bvar [in Fsub_Definitions]
typ_bvar [in Fsub_Part1A]
typ_exn [in STLC_Exn_Definitions]
typ_fvar [in ML_Core_Definitions]
typ_fvar [in Fsub_Definitions]
typ_fvar [in ML_Definitions]
typ_fvar [in Fsub_Part1A]
typ_nat [in ML_Definitions]
typ_prod [in ML_Definitions]
typ_prod [in STLC_Data_Definitions]
typ_ref [in STLC_Ref_Definitions]
typ_ref [in ML_Definitions]
typ_sum [in ML_Definitions]
typ_sum [in STLC_Data_Definitions]
typ_top [in Fsub_Part1A]
typ_top [in Fsub_Definitions]
typ_unit [in ML_Definitions]
typ_unit [in STLC_Ref_Definitions]
typ_unit [in STLC_Data_Definitions]
typ_var [in STLC_Core_WF_Definitions]
typ_var [in STLC_Core_Light]
typ_var [in STLC_Data_Definitions]
typ_var [in STLC_Core_Definitions]
typ_var [in STLC_Exn_Definitions]
typ_var [in STLC_Dec_Definitions]
typ_var [in STLC_Ref_Definitions]


V

value_abs [in STLC_Data_Definitions]
value_abs [in ML_Definitions]
value_abs [in STLC_Core_Light]
value_abs [in STLC_Core_Definitions]
value_abs [in ML_Core_Definitions]
value_abs [in STLC_Ref_Definitions]
value_abs [in STLC_Dec_Definitions]
value_abs [in STLC_Exn_Definitions]
value_abs [in Fsub_Definitions]
value_abs [in STLC_Core_WF_Definitions]
value_add [in ML_Definitions]
value_add_1 [in ML_Definitions]
value_fix [in STLC_Data_Definitions]
value_fix [in ML_Definitions]
value_inj1 [in ML_Definitions]
value_inj1 [in STLC_Data_Definitions]
value_inj2 [in ML_Definitions]
value_inj2 [in STLC_Data_Definitions]
value_loc [in ML_Definitions]
value_loc [in STLC_Ref_Definitions]
value_nat [in ML_Definitions]
value_pair [in STLC_Data_Definitions]
value_pair [in ML_Definitions]
value_tabs [in Fsub_Definitions]
value_trm_unit [in STLC_Ref_Definitions]
value_unit [in ML_Definitions]
value_unit [in STLC_Data_Definitions]


W

wft_all [in Fsub_Definitions]
wft_all [in Fsub_Part1A]
wft_arrow [in Fsub_Part1A]
wft_arrow [in Fsub_Definitions]
wft_top [in Fsub_Part1A]
wft_top [in Fsub_Definitions]
wft_var [in Fsub_Part1A]
wft_var [in Fsub_Definitions]
wf_cons [in CoC_Definitions]
wf_nil [in CoC_Definitions]



Inductive Index

B

beta [in Lambda_Definitions]
beta [in CoC_Definitions]
bind [in Fsub_Definitions]
bind [in Fsub_Part1A]


C

ctx [in STLC_Core_WF_Definitions]


E

Env.ok [in Metatheory_Env]
env_less [in CoC_Preservation]
equiv_ [in Lambda_Definitions]
equiv_ [in CoC_Definitions]
ered [in STLC_Core_Adequacy]
eterm [in STLC_Core_Adequacy]
etyping [in STLC_Core_Adequacy]
evalue [in STLC_Core_Adequacy]


F

fails [in ML_Definitions]
fails [in STLC_Exn_Definitions]
fullred [in STLC_Core_FullBeta]


I

iter_ [in CoC_ChurchRosser]
iter_ [in Lambda_Infrastructure]


L

less [in CoC_Definitions]
list_forall [in Lib_ListFactsMore]


M

MakeRaw.slist [in Lib_FinSetImpl]


O

okt [in Fsub_Part1A]
okt [in Fsub_Definitions]


P

para [in CoC_ChurchRosser]
para [in Lambda_Infrastructure]
pat [in STLC_Data_Definitions]
pat [in ML_Definitions]
pat_typing [in STLC_Data_Definitions]
pat_typing [in ML_Definitions]
phi_ok [in ML_Definitions]


R

red [in ML_Core_Definitions]
red [in ML_Definitions]
red [in STLC_Core_WF_Definitions]
red [in STLC_Core_Definitions]
red [in STLC_Ref_Definitions]
red [in STLC_Dec_Definitions]
red [in Fsub_Definitions]
red [in STLC_Data_Definitions]
red [in STLC_Core_Light]
red [in STLC_Exn_Definitions]


S

sch [in ML_Core_Definitions]
sch [in ML_Definitions]
star_ [in Lambda_Definitions]
star_ [in CoC_Definitions]
sto_ok [in ML_Definitions]
sto_ok [in STLC_Ref_Definitions]
sub [in Fsub_Part1A]
sub [in Fsub_Definitions]
substitution [in ML_Definitions]


T

term [in STLC_Dec_Definitions]
term [in CoC_Definitions]
term [in STLC_Core_Definitions]
term [in STLC_Core_Light]
term [in ML_Core_Definitions]
term [in Fsub_Definitions]
term [in STLC_Data_Definitions]
term [in STLC_Core_WF_Definitions]
term [in ML_Definitions]
term [in STLC_Exn_Definitions]
term [in STLC_Ref_Definitions]
term [in Lambda_Definitions]
trm [in STLC_Core_WF_Definitions]
trm [in CoC_Definitions]
trm [in STLC_Core_Definitions]
trm [in Lambda_Definitions]
trm [in STLC_Ref_Definitions]
trm [in ML_Core_Definitions]
trm [in Fsub_Definitions]
trm [in ML_Definitions]
trm [in STLC_Data_Definitions]
trm [in STLC_Exn_Definitions]
trm [in STLC_Dec_Definitions]
trm [in STLC_Core_Light]
typ [in STLC_Data_Definitions]
typ [in Fsub_Part1A]
typ [in STLC_Ref_Definitions]
typ [in STLC_Core_Definitions]
typ [in STLC_Core_Light]
typ [in ML_Definitions]
typ [in STLC_Exn_Definitions]
typ [in ML_Core_Definitions]
typ [in STLC_Dec_Definitions]
typ [in STLC_Core_WF_Definitions]
typ [in Fsub_Definitions]
type [in ML_Core_Definitions]
type [in Fsub_Part1A]
type [in Fsub_Definitions]
type [in ML_Definitions]
typing [in STLC_Core_WF_Definitions]
typing [in ML_Core_Definitions]
typing [in STLC_Core_Light]
typing [in ML_Definitions]
typing [in STLC_Exn_Definitions]
typing [in STLC_Core_Definitions]
typing [in Fsub_Definitions]
typing [in STLC_Dec_Definitions]
typing [in CoC_Definitions]
typing [in STLC_Ref_Definitions]
typing [in STLC_Data_Definitions]
typings [in STLC_Data_Infrastructure]
typings [in ML_Infrastructure]


V

value [in Fsub_Definitions]
value [in STLC_Core_WF_Definitions]
value [in STLC_Exn_Definitions]
value [in STLC_Core_Definitions]
value [in STLC_Dec_Definitions]
value [in ML_Core_Definitions]
value [in STLC_Core_Light]
value [in STLC_Data_Definitions]
value [in STLC_Ref_Definitions]
value [in ML_Definitions]


W

wf [in CoC_Definitions]
wft [in Fsub_Part1A]
wft [in Fsub_Definitions]



Definition Index

B

body [in STLC_Dec_Infrastructure]
body [in STLC_Core_WF_Infrastructure]
body [in CoC_Definitions]
body [in STLC_Exn_Infrastructure]
body [in STLC_Core_Infrastructure]
body [in STLC_Core_Light]
body [in Lambda_Definitions]
body [in STLC_Ref_Infrastructure]
bodys [in STLC_Data_Definitions]
bodys [in ML_Definitions]


C

church_rosser [in Lambda_Definitions]
church_rosser [in CoC_Definitions]
close_var [in CoC_Infrastructure]
close_var [in Lambda_Infrastructure]
close_var_rec [in CoC_Infrastructure]
close_var_rec [in Lambda_Infrastructure]
conf [in STLC_Ref_Definitions]
conf [in ML_Definitions]
confluence [in CoC_Definitions]
confluence [in Lambda_Definitions]
contains_terms [in CoC_Infrastructure]
conv [in CoC_Definitions]
ctx_of [in STLC_Core_WF_Definitions]


E

env [in STLC_Dec_Definitions]
env [in ML_Definitions]
env [in CoC_Definitions]
env [in ML_Core_Definitions]
env [in STLC_Core_Light]
env [in STLC_Data_Definitions]
env [in Fsub_Part1A]
env [in Fsub_Definitions]
env [in STLC_Core_WF_Definitions]
env [in STLC_Core_Definitions]
env [in STLC_Ref_Definitions]
env [in STLC_Exn_Definitions]
Env.binds [in Metatheory_Env]
Env.concat [in Metatheory_Env]
Env.dom [in Metatheory_Env]
Env.empty [in Metatheory_Env]
Env.env [in Metatheory_Env]
Env.env_prop [in Metatheory_Env]
Env.extends [in Metatheory_Env]
Env.fv_in [in Metatheory_Env]
Env.get [in Metatheory_Env]
Env.iter_push [in Metatheory_Env]
Env.map [in Metatheory_Env]
Env.single [in Metatheory_Env]
env_fv [in ML_Infrastructure]
env_fv [in ML_Core_Infrastructure]
epreservation [in STLC_Core_Adequacy]
eprogress [in STLC_Core_Adequacy]


F

FinSet.E.S.elt [in Lib_FinSet]
FinSet.E.S.fset [in Lib_FinSet]
fv [in CoC_Infrastructure]
fv [in STLC_Exn_Infrastructure]
fv [in Lambda_Infrastructure]
fv [in STLC_Core_WF_Infrastructure]
fv [in STLC_Core_Light]
fv [in STLC_Data_Infrastructure]
fv [in STLC_Dec_Infrastructure]
fv [in STLC_Ref_Infrastructure]
fv [in STLC_Core_Infrastructure]
fv_ee [in Fsub_Infrastructure]
fv_list [in STLC_Data_Infrastructure]
fv_te [in Fsub_Infrastructure]
fv_tt [in Fsub_Part1A]
fv_tt [in Fsub_Infrastructure]


H

has_scheme [in ML_Soundness]
has_scheme [in ML_Core_Soundness]
has_scheme_vars [in ML_Soundness]
has_scheme_vars [in ML_Core_Soundness]


L

list_for_n [in Lib_ListFactsMore]
loc [in STLC_Ref_Definitions]
loc [in ML_Definitions]


M

MakeRaw.add [in Lib_FinSetImpl]
MakeRaw.Build_slist' [in Lib_FinSetImpl]
MakeRaw.cardinal [in Lib_FinSetImpl]
MakeRaw.choose [in Lib_FinSetImpl]
MakeRaw.compare [in Lib_FinSetImpl]
MakeRaw.diff [in Lib_FinSetImpl]
MakeRaw.elements [in Lib_FinSetImpl]
MakeRaw.elt [in Lib_FinSetImpl]
MakeRaw.Empty [in Lib_FinSetImpl]
MakeRaw.empty [in Lib_FinSetImpl]
MakeRaw.eq [in Lib_FinSetImpl]
MakeRaw.Equal [in Lib_FinSetImpl]
MakeRaw.equal [in Lib_FinSetImpl]
MakeRaw.Exists [in Lib_FinSetImpl]
MakeRaw.exists_ [in Lib_FinSetImpl]
MakeRaw.filter [in Lib_FinSetImpl]
MakeRaw.fold [in Lib_FinSetImpl]
MakeRaw.for_all [in Lib_FinSetImpl]
MakeRaw.For_all [in Lib_FinSetImpl]
MakeRaw.from_sorted [in Lib_FinSetImpl]
MakeRaw.In [in Lib_FinSetImpl]
MakeRaw.inter [in Lib_FinSetImpl]
MakeRaw.is_empty [in Lib_FinSetImpl]
MakeRaw.lt [in Lib_FinSetImpl]
MakeRaw.max_elt [in Lib_FinSetImpl]
MakeRaw.mem [in Lib_FinSetImpl]
MakeRaw.min_elt [in Lib_FinSetImpl]
MakeRaw.partition [in Lib_FinSetImpl]
MakeRaw.remove [in Lib_FinSetImpl]
MakeRaw.singleton [in Lib_FinSetImpl]
MakeRaw.sort_bool [in Lib_FinSetImpl]
MakeRaw.Subset [in Lib_FinSetImpl]
MakeRaw.subset [in Lib_FinSetImpl]
MakeRaw.t [in Lib_FinSetImpl]
MakeRaw.to_sorted [in Lib_FinSetImpl]
MakeRaw.union [in Lib_FinSetImpl]
Make.Import.Import.elt [in Lib_FinSetImpl]
Make.Import.Import.fset [in Lib_FinSetImpl]


O

open [in CoC_Definitions]
open [in ML_Definitions]
open [in STLC_Core_Definitions]
open [in STLC_Exn_Definitions]
open [in STLC_Data_Definitions]
open [in STLC_Dec_Definitions]
open [in STLC_Ref_Definitions]
open [in Lambda_Definitions]
open [in STLC_Core_WF_Definitions]
open [in STLC_Core_Light]
opens [in STLC_Data_Definitions]
opens [in ML_Definitions]
opens_rec [in STLC_Data_Definitions]
opens_rec [in ML_Definitions]
open_ee [in Fsub_Definitions]
open_ee_rec [in Fsub_Definitions]
open_rec [in STLC_Ref_Definitions]
open_rec [in STLC_Core_Light]
open_rec [in STLC_Exn_Definitions]
open_rec [in STLC_Dec_Definitions]
open_rec [in Lambda_Definitions]
open_rec [in STLC_Core_WF_Definitions]
open_rec [in STLC_Core_Definitions]
open_rec [in CoC_Definitions]
open_te [in Fsub_Definitions]
open_te_rec [in Fsub_Definitions]
open_tt [in Fsub_Part1A]
open_tt [in Fsub_Definitions]
open_tt_rec [in Fsub_Part1A]
open_tt_rec [in Fsub_Definitions]


P

pat_arity [in STLC_Data_Definitions]
pat_arity [in ML_Definitions]
pat_match [in STLC_Data_Definitions]
pat_match [in ML_Definitions]
phi [in STLC_Ref_Definitions]
phi [in ML_Definitions]
phi_fv [in ML_Infrastructure]
preservation [in STLC_Exn_Definitions]
preservation [in Fsub_Definitions]
preservation [in STLC_Dec_Definitions]
preservation [in ML_Definitions]
preservation [in STLC_Ref_Definitions]
preservation [in STLC_Core_WF_Definitions]
preservation [in STLC_Core_Definitions]
preservation [in ML_Core_Definitions]
preservation [in STLC_Data_Definitions]
progress [in STLC_Core_WF_Definitions]
progress [in ML_Definitions]
progress [in STLC_Ref_Definitions]
progress [in Fsub_Definitions]
progress [in STLC_Exn_Definitions]
progress [in STLC_Core_Definitions]
progress [in STLC_Dec_Definitions]
progress [in STLC_Data_Definitions]
progress [in ML_Core_Definitions]


R

red_all [in CoC_Infrastructure]
red_all [in Lambda_Infrastructure]
red_in [in Lambda_Infrastructure]
red_in [in CoC_Infrastructure]
red_out [in Lambda_Infrastructure]
red_out [in CoC_Infrastructure]
red_refl [in CoC_Infrastructure]
red_refl [in Lambda_Infrastructure]
red_regular [in CoC_Infrastructure]
red_regular [in Lambda_Infrastructure]
red_rename [in Lambda_Infrastructure]
red_rename [in CoC_Infrastructure]
red_through [in Lambda_Infrastructure]
red_through [in CoC_Infrastructure]
relation [in Lambda_Definitions]
relation [in CoC_Definitions]


S

scheme [in ML_Definitions]
scheme [in ML_Core_Definitions]
sch_fv [in ML_Core_Infrastructure]
sch_fv [in ML_Infrastructure]
sch_open [in ML_Definitions]
sch_open [in ML_Core_Definitions]
sch_open_vars [in ML_Definitions]
sch_open_vars [in ML_Core_Definitions]
sch_subst [in ML_Core_Infrastructure]
sch_subst [in ML_Infrastructure]
sch_substs [in ML_Infrastructure]
sch_substs [in ML_Core_Infrastructure]
simulated [in CoC_Infrastructure]
simulated [in Lambda_Infrastructure]
sto [in STLC_Ref_Definitions]
sto [in ML_Definitions]
sto_typing [in ML_Definitions]
sto_typing [in STLC_Ref_Definitions]
subject_reduction [in CoC_Definitions]
subst [in CoC_Infrastructure]
subst [in STLC_Core_Infrastructure]
subst [in STLC_Core_Light]
subst [in Lambda_Infrastructure]
subst [in STLC_Dec_Infrastructure]
subst [in STLC_Core_WF_Infrastructure]
subst [in STLC_Data_Infrastructure]
subst [in STLC_Ref_Infrastructure]
subst [in STLC_Exn_Infrastructure]
substs [in STLC_Data_Infrastructure]
substs [in ML_Infrastructure]
subst_ee [in Fsub_Infrastructure]
subst_tb [in Fsub_Part1A]
subst_tb [in Fsub_Infrastructure]
subst_te [in Fsub_Infrastructure]
subst_tt [in Fsub_Infrastructure]
subst_tt [in Fsub_Part1A]
S.E.elt [in Lib_MyFSetInterface]
S.E.Empty [in Lib_MyFSetInterface]
S.E.eq [in Lib_MyFSetInterface]
S.E.Equal [in Lib_MyFSetInterface]
S.E.Exists [in Lib_MyFSetInterface]
S.E.For_all [in Lib_MyFSetInterface]
S.E.Subset [in Lib_MyFSetInterface]


T

terms [in STLC_Data_Infrastructure]
terms [in ML_Infrastructure]
term_body [in ML_Core_Definitions]
transitivity_on [in Fsub_Soundness]
transitivity_on [in Fsub_Part1A]
trm_def [in ML_Definitions]
trm_def [in STLC_Data_Definitions]
trm_fv [in ML_Infrastructure]
trm_fv [in ML_Core_Infrastructure]
trm_fvars [in ML_Definitions]
trm_fvars [in STLC_Data_Definitions]
trm_fv_list [in ML_Infrastructure]
trm_nth [in STLC_Data_Definitions]
trm_nth [in ML_Definitions]
trm_open [in ML_Core_Definitions]
trm_open_rec [in ML_Core_Definitions]
trm_subst [in ML_Core_Infrastructure]
trm_subst [in ML_Infrastructure]
types [in ML_Core_Definitions]
types [in ML_Definitions]
typ_body [in ML_Definitions]
typ_body [in ML_Core_Definitions]
typ_def [in ML_Core_Definitions]
typ_def [in ML_Definitions]
typ_fv [in ML_Core_Infrastructure]
typ_fv [in ML_Definitions]
typ_fvars [in ML_Definitions]
typ_fvars [in ML_Core_Definitions]
typ_fv_list [in ML_Core_Infrastructure]
typ_fv_list [in ML_Infrastructure]
typ_open [in ML_Definitions]
typ_open [in ML_Core_Definitions]
typ_open_vars [in ML_Core_Definitions]
typ_open_vars [in ML_Definitions]
typ_subst [in ML_Core_Infrastructure]
typ_subst [in ML_Infrastructure]
typ_substs [in ML_Infrastructure]
typ_substs [in ML_Core_Infrastructure]


V

VARIABLES.Var_as_OT.Import.Variables.Import.Export.Import.fresh [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.vars [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.Import.var_generate [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.var [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.Variables.var_default [in Metatheory_Var]
VARIABLES.Var_as_OT.Import.vars [in Metatheory_Var]
VARIABLES.Var_as_OT.t [in Metatheory_Var]



Module Index

E

E [in Lib_MyFSetInterface]
E [in Lib_FinSet]
Env [in Metatheory_Env]
Export [in Metatheory_Var]


F

FinSet [in Lib_FinSet]
FinSetFacts [in Lib_FinSet]


I

Import [in Metatheory_Var]
Import [in Lib_FinSetImpl]
Import [in Lib_FinSetImpl]
Import [in Metatheory_Var]
Import [in Metatheory_Var]


M

Make [in Lib_FinSetImpl]
MakeRaw [in Lib_FinSetImpl]


S

S [in Lib_FinSet]
S [in Lib_MyFSetInterface]


V

VARIABLES [in Metatheory_Var]
Variables [in Metatheory_Var]
Var_as_OT [in Metatheory_Var]



Library Index

C

CoC_BetaStar
CoC_ChurchRosser
CoC_Conversion
CoC_Definitions
CoC_Infrastructure
CoC_Preservation


F

Fsub_Definitions
Fsub_Infrastructure
Fsub_Part1A
Fsub_Soundness


L

Lambda_ChurchRosser
Lambda_Definitions
Lambda_Infrastructure
Lib_FinSet
Lib_FinSetImpl
Lib_ListFacts
Lib_ListFactsMore
Lib_MyFSetInterface
Lib_Tactic


M

Metatheory
Metatheory_Env
Metatheory_Fresh
Metatheory_Var
ML_Core_Definitions
ML_Core_Infrastructure
ML_Core_Soundness
ML_Definitions
ML_Infrastructure
ML_Soundness


S

STLC_Core_Adequacy
STLC_Core_Definitions
STLC_Core_FullBeta
STLC_Core_Infrastructure
STLC_Core_Light
STLC_Core_Soundness
STLC_Core_WF_Definitions
STLC_Core_WF_Infrastructure
STLC_Core_WF_Soundness
STLC_Data_Definitions
STLC_Data_Infrastructure
STLC_Data_Soundness
STLC_Dec_Decidability
STLC_Dec_Definitions
STLC_Dec_Infrastructure
STLC_Dec_Soundness
STLC_Exn_Definitions
STLC_Exn_Infrastructure
STLC_Exn_Soundness
STLC_Ref_Definitions
STLC_Ref_Infrastructure
STLC_Ref_Soundness



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 _ (1667 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (93 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 _ (610 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 _ (510 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 _ (114 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 _ (271 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 _ (18 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (51 entries)

This page has been generated by coqdoc