Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (640 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (51 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (235 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (13 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (103 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (42 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (65 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (17 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (29 entries)

Global Index

A

adequacy [definition, in Framework]
adequacy_cadequacy [lemma, in Framework]
agree_equiv [lemma, in Freevars]
agree_ty [lemma, in Freevars]
annot [definition, in Autosubst_Basics]
app [inductive, in Filters]
App [constructor, in Definitions]
app [constructor, in CL1]
arr [constructor, in STLC1]
arr [constructor, in T1]
arr [constructor, in F1]
Arr [constructor, in Definitions]
arr [constructor, in CL1]
Autosubst [library]
Autosubst_MMapInstances [library]
Autosubst_Classes [library]
Autosubst_Derive [library]
Autosubst_MMap [library]
Autosubst_Tactics [library]
Autosubst_Basics [library]
Autosubst_Lemmas [library]


B

base [constructor, in STLC1]
BASE [constructor, in Definitions]
base [constructor, in CL1]
basetype [inductive, in Definitions]
bot [definition, in Filters]
bot_filter [lemma, in Filters]


C

cadequacy [definition, in Framework]
cequi_typep [instance, in Types]
cint [definition, in Definitions]
cint_csub_r [lemma, in Contexts]
cint_csub_l [lemma, in Contexts]
cint_Empty [lemma, in Contexts]
cint_Gamma_Empty [lemma, in Contexts]
cint_Empty_Gamma [lemma, in Contexts]
CL [inductive, in CL1]
CLapp [constructor, in CL1]
CLC [definition, in CL1]
CLC_c [lemma, in CL1]
CLK [constructor, in CL1]
closed_leu [projection, in Filters]
closed_int [projection, in Filters]
closure [inductive, in Filters]
closure_closure_equiv [lemma, in Filters]
closure_filter_equiv [lemma, in Filters]
closure_filter [lemma, in Filters]
CLS [constructor, in CL1]
CL_stlc [lemma, in CL1]
CL_valid [lemma, in CL1]
cl_step_appR [constructor, in CL1]
cl_step_appL [constructor, in CL1]
cl_stepK [constructor, in CL1]
cl_stepS [constructor, in CL1]
cl_step [inductive, in CL1]
CL_ty [inductive, in CL1]
CL1 [library]
compA [lemma, in Autosubst_Basics]
compatible [definition, in Interpretation]
compatible_sub [lemma, in Interpretation]
compatible_sub_Gamma [lemma, in Interpretation]
compatible_cint [lemma, in Interpretation]
compatible_down [lemma, in Interpretation]
compatible_up [lemma, in Interpretation]
compile [definition, in T1]
compiler_consistency [definition, in Framework]
compile_subst [lemma, in T1]
compile_subst_full [lemma, in T1]
compile_ren_full [lemma, in T1]
comp_id [lemma, in Autosubst_Basics]
conj' [lemma, in Autosubst_Basics]
cons_drop_inv [lemma, in Contexts]
context [definition, in Definitions]
Contexts [library]
count [definition, in TypeEquivalence]
csplit [lemma, in Contexts]
csub [definition, in Definitions]
csub_ext [lemma, in Contexts]
csub_cint_proper [instance, in Contexts]
csub_cint_comp [lemma, in Contexts]
csub_comm [lemma, in Contexts]
csub_sub [lemma, in Contexts]
cte [definition, in Definitions]
cte_eq [lemma, in Contexts]
cte_ext_int [lemma, in Contexts]
cte_ext [lemma, in Contexts]
cte_csub_R [lemma, in Contexts]
cte_csub_L [lemma, in Contexts]
cte_csub_equiv [lemma, in Contexts]
cte_csub [instance, in Contexts]
cte_cint_proper [instance, in Contexts]
cte_equivalence [instance, in Contexts]
cte_trans [lemma, in Contexts]
cte_sym [lemma, in Contexts]
cte_pwr_refl [lemma, in Contexts]
cte_refl [lemma, in Contexts]
cte_comp_cint [lemma, in Contexts]
cte_assoc_cint [lemma, in Contexts]
cte_comm_cint [lemma, in Contexts]


D

Dec [record, in Decidable]
Dec [inductive, in Decidable]
dec [definition, in Decidable]
Decidable [library]
decide [projection, in Decidable]
decide [constructor, in Decidable]
decide_lt_nat [instance, in Decidable]
decide_le_nat [instance, in Decidable]
decide_eq_nat [instance, in Decidable]
Definitions [library]
drop [definition, in Definitions]


E

Empty [definition, in Definitions]
equal_f [lemma, in Autosubst_Basics]
equiv_comp_p [instance, in Filters]
equiv_app_comp [lemma, in Filters]
equiv_filter [lemma, in Filters]
equiv_e [instance, in Filters]
equiv_closure [lemma, in Filters]
equiv_rp_p [instance, in RealizorPredicates]
equiv_closed [projection, in RealizorPredicates]
equi_typep [instance, in Types]
equi_type [lemma, in Types]
excl_bot [projection, in RealizorPredicates]


F

fapp [constructor, in F1]
feq_eq [lemma, in Contexts]
feq_trans [lemma, in Contexts]
feq_ext_int [lemma, in Contexts]
feq_ext [lemma, in Contexts]
fgen [constructor, in F1]
Filters [library]
filter_filter_equiv [lemma, in Filters]
filter_equiv_trans [lemma, in Filters]
filter_equiv_sym [lemma, in Filters]
filter_equiv_refl [lemma, in Filters]
filter_equiv [definition, in Filters]
filter_ind_filter [lemma, in Filters]
flam [constructor, in F1]
fold_ren_cons [lemma, in Autosubst_Tactics]
Framework [library]
Freevars [library]
fromclosure_F [lemma, in Filters]
fspec [constructor, in F1]
Ftype [inductive, in F1]
funcomp [definition, in Autosubst_Basics]
FV [inductive, in Freevars]
FVAppL [constructor, in Freevars]
FVAppR [constructor, in Freevars]
fvar [constructor, in F1]
FVLam [constructor, in Freevars]
FVVar [constructor, in Freevars]
FV_dec [instance, in Freevars]
f_ty [inductive, in F1]
f_ctx [definition, in F1]
F1 [library]
F2 [library]


G

General_Termination.LambdaCurry.tty [variable, in Framework]
General_Termination.LambdaCurry [section, in Framework]
General_Termination.Compiler.tstep [variable, in Framework]
General_Termination.Compiler.vtty [variable, in Framework]
General_Termination.Compiler.ctty [variable, in Framework]
[| _ |] [notation, in Framework]
General_Termination.Compiler.compiler [variable, in Framework]
General_Termination.Compiler.tterm [variable, in Framework]
General_Termination.Compiler [section, in Framework]
[[ _ ]] _ [notation, in Framework]
General_Termination.int_ty [variable, in Framework]
General_Termination.ttype [variable, in Framework]
General_Termination [section, in Framework]
gsn [constructor, in Reduction]
GSN [inductive, in Reduction]


H

hcomp [definition, in Autosubst_Classes]
hcomp_dist_internal [lemma, in Autosubst_Derive]
hcomp_ren_internal [lemma, in Autosubst_Derive]
hcomp_lift_internal [lemma, in Autosubst_Derive]
hcomp_lift_n_internal [lemma, in Autosubst_Derive]
hsubst [projection, in Autosubst_Classes]
HSubst [record, in Autosubst_Classes]
hsubst [constructor, in Autosubst_Classes]
HSubst [inductive, in Autosubst_Classes]
HSubstHSubstComp [record, in Autosubst_Classes]
HSubstHSubstComp [inductive, in Autosubst_Classes]
HSubstHSubstInd [record, in Autosubst_Classes]
HSubstHSubstInd [inductive, in Autosubst_Classes]
HSubstLemmas [record, in Autosubst_Classes]
hsubst_hsubst_ind [projection, in Autosubst_Classes]
hsubst_hsubst_ind [constructor, in Autosubst_Classes]
hsubst_hsubst_comp [projection, in Autosubst_Classes]
hsubst_hsubst_comp [constructor, in Autosubst_Classes]
hsubst_comp [projection, in Autosubst_Classes]
hsubst_id [projection, in Autosubst_Classes]
hsubst_compR [lemma, in Autosubst_Tactics]
hsubst_compX [lemma, in Autosubst_Tactics]
hsubst_compI [lemma, in Autosubst_Tactics]
hsubst_idX [lemma, in Autosubst_Tactics]


I

id [definition, in Autosubst_Basics]
ids [projection, in Autosubst_Classes]
Ids [record, in Autosubst_Classes]
ids [constructor, in Autosubst_Classes]
Ids [inductive, in Autosubst_Classes]
Ids_Tterm [instance, in T1]
Ids_ftype [instance, in F1]
Ids_term [instance, in Definitions]
id_hsubst [projection, in Autosubst_Classes]
id_subst [projection, in Autosubst_Classes]
id_hsubstR [lemma, in Autosubst_Tactics]
id_hsubstX [lemma, in Autosubst_Tactics]
id_scompR [lemma, in Autosubst_Tactics]
id_scompX [lemma, in Autosubst_Tactics]
id_comp [lemma, in Autosubst_Basics]
IFilter [record, in Filters]
inApp [constructor, in Filters]
inc [definition, in Weakening]
inclosure_F [lemma, in Filters]
includes [inductive, in Subsumption]
includesDropL [constructor, in Subsumption]
includesDropR [constructor, in Subsumption]
includesF [constructor, in Subsumption]
incl_inv_sub [lemma, in Subsumption]
incl_top [projection, in RealizorPredicates]
inF [constructor, in Filters]
inI [constructor, in Filters]
inKtype [constructor, in T1]
int [definition, in Definitions]
Int [constructor, in Definitions]
InternalLemmas [section, in Autosubst_Derive]
InternalLemmasHSubst [section, in Autosubst_Derive]
Interpretation [library]
intersect [definition, in RealizorPredicates]
intersect_realizable [lemma, in RealizorPredicates]
intty [constructor, in Interpretation]
inttype [inductive, in Definitions]
int_lam [lemma, in Premodel]
int_st [lemma, in Premodel]
int_x [lemma, in Premodel]
int_ty_rp [lemma, in STLC1]
int_ty [definition, in STLC1]
int_ty_rp [lemma, in T1]
int_ty [definition, in T1]
int_nat_filter [lemma, in T1]
int_nat [inductive, in T1]
int_ty_beta [lemma, in F1]
int_ty_subst_equiv [lemma, in F1]
int_ty_ren_equiv [lemma, in F1]
int_ty_feq_equiv [lemma, in F1]
int_ty_rp [lemma, in F1]
int_ty [definition, in F1]
int_app [definition, in Filters]
int_ty_rp [lemma, in CL1]
int_ty [definition, in CL1]
int_eq_O [lemma, in TypeEquivalence]
int_comm_O [lemma, in TypeEquivalence]
int_O [lemma, in TypeEquivalence]
int_equiv [instance, in RealizorPredicates]
int_IF [lemma, in Interpretation]
int_t [inductive, in Interpretation]
invtyInt [lemma, in Types]
invtyVar [lemma, in Types]
in_int_ty [lemma, in STLC1]
in_int_ty [lemma, in T1]
in_int_ty [lemma, in F1]
in_int_ty [lemma, in CL1]
iterate [definition, in Autosubst_Basics]
iterate_0 [lemma, in Autosubst_Basics]
iterate_S [lemma, in Autosubst_Basics]
iter_param [lemma, in Autosubst_Derive]
iter_fp [lemma, in Autosubst_Derive]


K

K [constructor, in CL1]
Ktype [inductive, in T1]
k_nat [lemma, in T1]


L

Lam [constructor, in Definitions]
lcc [definition, in Framework]
lcc_c [lemma, in Framework]
LemmasForFun [section, in Autosubst_Basics]
LemmasForHSubst [section, in Autosubst_Tactics]
LemmasForMMap [section, in Autosubst_MMap]
LemmasForSubst [section, in Autosubst_Tactics]
lift [definition, in Autosubst_Basics]
lift_injn [lemma, in Autosubst_Lemmas]
lift_inj [lemma, in Autosubst_Lemmas]
lift_eta [lemma, in Autosubst_Basics]
lift_compR [lemma, in Autosubst_Basics]
lift_comp [lemma, in Autosubst_Basics]
lift_scons [lemma, in Autosubst_Basics]
lift0 [lemma, in Autosubst_Lemmas]
lift0 [lemma, in Autosubst_Basics]


M

mmap [projection, in Autosubst_MMap]
MMap [record, in Autosubst_MMap]
mmap [constructor, in Autosubst_MMap]
MMap [inductive, in Autosubst_MMap]
MMapConst [section, in Autosubst_MMap]
MMapExt [record, in Autosubst_MMap]
MMapExt [inductive, in Autosubst_MMap]
MMapExt_const [instance, in Autosubst_MMap]
MMapExt_refl [instance, in Autosubst_MMap]
MMapExt_fun [instance, in Autosubst_MMapInstances]
MMapExt_pair [instance, in Autosubst_MMapInstances]
MMapExt_list [instance, in Autosubst_MMapInstances]
MMapExt_option [instance, in Autosubst_MMapInstances]
MMapId [section, in Autosubst_MMap]
MMapInstances [section, in Autosubst_MMapInstances]
MMapInstances.A [variable, in Autosubst_MMapInstances]
MMapInstances.B [variable, in Autosubst_MMapInstances]
MMapInstances.C [variable, in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_C [variable, in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_B [variable, in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_C [variable, in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_B [variable, in Autosubst_MMapInstances]
MMapInstances.MMap_A_C [variable, in Autosubst_MMapInstances]
MMapInstances.MMap_A_B [variable, in Autosubst_MMapInstances]
MMapLemmas [record, in Autosubst_MMap]
MMapLemmas_const [instance, in Autosubst_MMap]
MMapLemmas_refl [instance, in Autosubst_MMap]
MMapLemmas_fun [instance, in Autosubst_MMapInstances]
MMapLemmas_pair [instance, in Autosubst_MMapInstances]
MMapLemmas_list [instance, in Autosubst_MMapInstances]
MMapLemmas_option [instance, in Autosubst_MMapInstances]
mmap_const_instE [lemma, in Autosubst_MMap]
MMap_const [instance, in Autosubst_MMap]
mmap_id_instE [lemma, in Autosubst_MMap]
MMap_refl [instance, in Autosubst_MMap]
mmap_compR [lemma, in Autosubst_MMap]
mmap_compX [lemma, in Autosubst_MMap]
mmap_idX [lemma, in Autosubst_MMap]
mmap_comp [projection, in Autosubst_MMap]
mmap_id [projection, in Autosubst_MMap]
mmap_ext [projection, in Autosubst_MMap]
mmap_ext [constructor, in Autosubst_MMap]
MMap_fun [instance, in Autosubst_MMapInstances]
MMap_pair [instance, in Autosubst_MMapInstances]
MMap_list [instance, in Autosubst_MMapInstances]
MMap_option [instance, in Autosubst_MMapInstances]
mmap_id_ext [lemma, in Autosubst_Derive]
more [constructor, in Reduction]


N

NAT [constructor, in T1]


O

OMEGA [constructor, in Definitions]
one [constructor, in Reduction]
only_filter [projection, in RealizorPredicates]
O_nat [constructor, in T1]


P

pi [constructor, in F1]
pi_equiv [definition, in RealizorPredicates]
plusA [lemma, in Autosubst_Basics]
plusnO [lemma, in Autosubst_Basics]
plusnS [lemma, in Autosubst_Basics]
plusOn [lemma, in Autosubst_Basics]
plusSn [lemma, in Autosubst_Basics]
possible_int_specialize [lemma, in RealizorPredicates]
possible_int_realizable [lemma, in RealizorPredicates]
possible_int [definition, in RealizorPredicates]
Premodel [library]
prod [definition, in RealizorPredicates]
prod_equiv [instance, in RealizorPredicates]
prod_realizable [lemma, in RealizorPredicates]
PWR [definition, in Definitions]


R

rc_ctx [definition, in Framework]
realizor [constructor, in RealizorPredicates]
realizorCandidate [definition, in RealizorPredicates]
realizorPredicate [record, in RealizorPredicates]
RealizorPredicates [library]
Reduction [library]
ren [definition, in Autosubst_Classes]
rename [projection, in Autosubst_Classes]
Rename [record, in Autosubst_Classes]
rename [constructor, in Autosubst_Classes]
Rename [inductive, in Autosubst_Classes]
Rename_Tterm [instance, in T1]
rename_subst [projection, in Autosubst_Classes]
rename_substX [lemma, in Autosubst_Tactics]
Rename_ftype [instance, in F1]
Rename_term [instance, in Definitions]
renS [lemma, in Autosubst_Lemmas]
ren_uncomp [lemma, in Autosubst_Lemmas]
rpe [instance, in RealizorPredicates]
rp_preservation [definition, in Framework]
rp_nat [lemma, in T1]
rp_equiv [definition, in RealizorPredicates]


S

S [constructor, in CL1]
scomp [definition, in Autosubst_Classes]
scomp_hcompR [lemma, in Autosubst_Tactics]
scomp_hcompX [lemma, in Autosubst_Tactics]
scomp_hcompI [lemma, in Autosubst_Tactics]
scons [definition, in Autosubst_Basics]
scons_eta [lemma, in Autosubst_Basics]
scons_comp [lemma, in Autosubst_Basics]
simpletype [inductive, in STLC1]
simpletype [inductive, in CL1]
sn [lemma, in Framework]
SN [definition, in Reduction]
sn_tsn [lemma, in Framework]
sn_stlc [lemma, in STLC1]
sn_T [lemma, in T1]
sn_gsn [lemma, in Reduction]
sn_system [lemma, in Termination]
sn_F [lemma, in F1]
step [inductive, in Reduction]
steps [inductive, in Reduction]
steps_appR [lemma, in Reduction]
steps_appL [lemma, in Reduction]
step_beta_eq [lemma, in Reduction]
step_lam [constructor, in Reduction]
step_appR [constructor, in Reduction]
step_appL [constructor, in Reduction]
step_beta [constructor, in Reduction]
step_ty [lemma, in Termination]
step_n [lemma, in Termination]
stlctyapp [constructor, in STLC1]
stlctylam [constructor, in STLC1]
stlctyvar [constructor, in STLC1]
stlc_ty [inductive, in STLC1]
stlc_ctx [definition, in STLC1]
STLC1 [library]
subst [projection, in Autosubst_Classes]
Subst [record, in Autosubst_Classes]
subst [constructor, in Autosubst_Classes]
Subst [inductive, in Autosubst_Classes]
SubstHSubstComp [record, in Autosubst_Classes]
SubstHSubstComp [inductive, in Autosubst_Classes]
Substitution [library]
SubstLemmas [record, in Autosubst_Classes]
SubstLemmas [section, in Autosubst_Lemmas]
SubstLemmas_Tterm [instance, in T1]
SubstLemmas_ftype [instance, in F1]
SubstLemmas_term [instance, in Definitions]
Subst_Tterm [instance, in T1]
subst_hsubst_comp [projection, in Autosubst_Classes]
subst_hsubst_comp [constructor, in Autosubst_Classes]
subst_comp [projection, in Autosubst_Classes]
subst_id [projection, in Autosubst_Classes]
subst_compR [lemma, in Autosubst_Tactics]
subst_compX [lemma, in Autosubst_Tactics]
subst_compI [lemma, in Autosubst_Tactics]
subst_idX [lemma, in Autosubst_Tactics]
Subst_ftype [instance, in F1]
Subst_term [instance, in Definitions]
subsumes [definition, in Definitions]
Subsumption [library]
sub_inv_int [lemma, in Subsumption]
sub_inv_F_G [lemma, in Subsumption]
sub_inv [lemma, in Subsumption]
sub_inv_O [lemma, in Subsumption]
sub_inv_A [lemma, in Subsumption]
sub_proper [instance, in Subsumption]
sub_comp_int [lemma, in Subsumption]
sub_Int_R [lemma, in Subsumption]
sub_Int_L [lemma, in Subsumption]
sub_O [lemma, in Subsumption]
sub_int [lemma, in Subsumption]
sub_equiv [lemma, in Subsumption]
sub_preorder [instance, in Subsumption]
sub_trans [lemma, in Subsumption]
sub_refl [lemma, in Subsumption]
S_nat [constructor, in T1]


T

Tapp [constructor, in T1]
TappL [constructor, in T1]
TappR [constructor, in T1]
Tbeta [constructor, in T1]
tcount [definition, in TypeEquivalence]
TC_c [lemma, in T1]
term [inductive, in Definitions]
Termination [library]
te_inv_incl [lemma, in Subsumption]
te_sub [instance, in Subsumption]
te_assoc_Int_rl [constructor, in Definitions]
te_assoc_Int_lr [constructor, in Definitions]
te_trans_ABC [constructor, in Definitions]
te_cong_Int [constructor, in Definitions]
te_comm_Int [constructor, in Definitions]
te_refl_OMEGA [constructor, in Definitions]
te_refl_F [constructor, in Definitions]
te_inv [lemma, in TypeEquivalence]
te_tcount_stable [lemma, in TypeEquivalence]
te_assoc_int [lemma, in TypeEquivalence]
te_comm_int [lemma, in TypeEquivalence]
te_Proper_int [instance, in TypeEquivalence]
te_comp_int [lemma, in TypeEquivalence]
te_comp_int_r [lemma, in TypeEquivalence]
te_comp_int_l [lemma, in TypeEquivalence]
te_inv_F [lemma, in TypeEquivalence]
te_O_r [lemma, in TypeEquivalence]
te_O_l [lemma, in TypeEquivalence]
te_inv_A [lemma, in TypeEquivalence]
te_inv_OMEGA [lemma, in TypeEquivalence]
te_equiv [instance, in TypeEquivalence]
te_trans [lemma, in TypeEquivalence]
te_sym [lemma, in TypeEquivalence]
te_refl [lemma, in TypeEquivalence]
Tlam [constructor, in T1]
TO [constructor, in T1]
top [definition, in Filters]
top_sigma_valuation [lemma, in Framework]
top_sigma [definition, in Framework]
top_rho_valid [lemma, in Framework]
top_rho [definition, in Framework]
top_nat [constructor, in T1]
top_app [lemma, in Filters]
top_filter [lemma, in Filters]
top_rp_realizable [lemma, in RealizorPredicates]
top_rp [definition, in RealizorPredicates]
Tprec [constructor, in T1]
TprecO [constructor, in T1]
TprecS [constructor, in T1]
translates [definition, in F1]
translates_skip [lemma, in F1]
TS [constructor, in T1]
tsn [lemma, in Framework]
TSN [definition, in Framework]
Tterm [inductive, in T1]
Ttyapp [constructor, in T1]
Ttylam [constructor, in T1]
TtyO [constructor, in T1]
Ttype [inductive, in T1]
Ttyprec [constructor, in T1]
TtyS [constructor, in T1]
Ttyvar [constructor, in T1]
Tvar [constructor, in T1]
tvar [constructor, in F1]
TVar [constructor, in Definitions]
ty [inductive, in Definitions]
tyAbs [constructor, in Definitions]
tyApp [constructor, in Definitions]
tycsub [lemma, in Types]
tyInt [constructor, in Definitions]
tymon [lemma, in Types]
tyO [constructor, in Definitions]
type [inductive, in Definitions]
typeable [definition, in T1]
TypeEquivalence [library]
Types [library]
type_equiv [inductive, in Definitions]
type_context [definition, in Interpretation]
tyren [inductive, in Weakening]
tyrenInv [constructor, in Weakening]
tyren_split [lemma, in Weakening]
tyren_var [lemma, in Weakening]
tyren_up [lemma, in Weakening]
tysub [inductive, in Substitution]
tysubA [lemma, in Types]
tysubCons [constructor, in Substitution]
tysubRen [constructor, in Substitution]
tysubst [lemma, in Substitution]
tysubst_var [lemma, in Substitution]
tysub_split [lemma, in Substitution]
tysub_up [lemma, in Substitution]
tysub_lift [lemma, in Substitution]
tysub_beta [lemma, in Substitution]
tyVar [constructor, in Definitions]
tyVarA [lemma, in Types]
tyVarU [lemma, in Types]
ty_S [lemma, in T1]
ty_equiv [lemma, in Types]
ty_subsume [lemma, in Types]
t_ctx [definition, in Framework]
T_valid [lemma, in T1]
T_ty [inductive, in T1]
T_ctx [definition, in T1]
T_step [inductive, in T1]
T1 [library]


U

up [definition, in Autosubst_Classes]
UpB [constructor, in Definitions]
upE [lemma, in Autosubst_Tactics]
UpI [constructor, in Definitions]
upn [abbreviation, in Autosubst_Classes]
upren [definition, in Autosubst_Classes]
upX [lemma, in Autosubst_Tactics]
up_comp_n [lemma, in Autosubst_Lemmas]
up_comp [lemma, in Autosubst_Lemmas]
up_liftn [lemma, in Autosubst_Lemmas]
up_lift1 [lemma, in Autosubst_Lemmas]
up_id_n [lemma, in Autosubst_Lemmas]
up_id [lemma, in Autosubst_Lemmas]
up_hcomp_n_internal [lemma, in Autosubst_Derive]
up_hcomp_internal [lemma, in Autosubst_Derive]
up_comp_n_internal [lemma, in Autosubst_Derive]
up_comp_internal [lemma, in Autosubst_Derive]
up_comp_subst_ren_n_internal [lemma, in Autosubst_Derive]
up_comp_subst_ren_internal [lemma, in Autosubst_Derive]
up_comp_ren_subst_n [lemma, in Autosubst_Derive]
up_comp_ren_subst [lemma, in Autosubst_Derive]
up_id_n_internal [lemma, in Autosubst_Derive]
up_id_internal [lemma, in Autosubst_Derive]
up_upren_n_internal [lemma, in Autosubst_Derive]
up_upren_internal [lemma, in Autosubst_Derive]


V

valid [definition, in Interpretation]
validates [definition, in Framework]
validates_up [lemma, in Framework]
validates_skip [lemma, in F1]
validation [definition, in Framework]
valid_up [lemma, in Interpretation]
valuation [definition, in Framework]
valuation_up [lemma, in Framework]
val_ty_v [lemma, in Framework]
val_ty_gamma [constructor, in Framework]
val_ty [inductive, in Framework]
val_ty_gamma [constructor, in T1]
val_ty [inductive, in T1]
var [definition, in Autosubst_Basics]


W

weaken [lemma, in Weakening]
weakening [lemma, in Weakening]
Weakening [library]


X

xe_closure [lemma, in Filters]


_

_bind [definition, in Autosubst_Classes]


other

{ bind _ } (bind_scope) [notation, in Autosubst_Classes]
{ bind _ in _ } (bind_scope) [notation, in Autosubst_Classes]
{ bind _ of _ } (bind_scope) [notation, in Autosubst_Classes]
{ bind _ of _ in _ } (bind_scope) [notation, in Autosubst_Classes]
_ ..|[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..|[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..|[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ .|[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .|[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .|[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ >>| _ (subst_scope) [notation, in Autosubst_Classes]
_ ..[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ ..[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ .[ _ , _ , .. , _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .[ _ /] (subst_scope) [notation, in Autosubst_Classes]
_ .[ _ ] (subst_scope) [notation, in Autosubst_Classes]
_ >> _ (subst_scope) [notation, in Autosubst_Classes]
_ .: _ (subst_scope) [notation, in Autosubst_Basics]
_ >>> _ (subst_scope) [notation, in Autosubst_Basics]
_ == _ (type_scope) [notation, in Definitions]
_ ==> _ [notation, in T1]
_ --> _ [notation, in T1]
_ ~ _ [notation, in Filters]
_ @ _ [notation, in Filters]
_ >=1 _ [notation, in Definitions]
_ ==1 _ [notation, in Definitions]
_ =1 _ [notation, in Definitions]
_ & _ [notation, in Definitions]
_ >= _ [notation, in Definitions]
_ * _ [notation, in Definitions]
_ o _ [notation, in Definitions]
_ --> _ [notation, in Definitions]
_ --> _ [notation, in CL1]
_ =R= _ [notation, in RealizorPredicates]
' _ [notation, in T1]
( + _ ) [notation, in Autosubst_Basics]
[ _ ] _ [notation, in Interpretation]
[[ _ ]] _ [notation, in STLC1]
[[ _ ]] [notation, in T1]
[[ _ ]] _ [notation, in F1]
[[ _ ]] _ [notation, in CL1]



Instance Index

C

cequi_typep [in Types]
csub_cint_proper [in Contexts]
cte_csub [in Contexts]
cte_cint_proper [in Contexts]
cte_equivalence [in Contexts]


D

decide_lt_nat [in Decidable]
decide_le_nat [in Decidable]
decide_eq_nat [in Decidable]


E

equiv_comp_p [in Filters]
equiv_e [in Filters]
equiv_rp_p [in RealizorPredicates]
equi_typep [in Types]


F

FV_dec [in Freevars]


I

Ids_Tterm [in T1]
Ids_ftype [in F1]
Ids_term [in Definitions]
int_equiv [in RealizorPredicates]


M

MMapExt_const [in Autosubst_MMap]
MMapExt_refl [in Autosubst_MMap]
MMapExt_fun [in Autosubst_MMapInstances]
MMapExt_pair [in Autosubst_MMapInstances]
MMapExt_list [in Autosubst_MMapInstances]
MMapExt_option [in Autosubst_MMapInstances]
MMapLemmas_const [in Autosubst_MMap]
MMapLemmas_refl [in Autosubst_MMap]
MMapLemmas_fun [in Autosubst_MMapInstances]
MMapLemmas_pair [in Autosubst_MMapInstances]
MMapLemmas_list [in Autosubst_MMapInstances]
MMapLemmas_option [in Autosubst_MMapInstances]
MMap_const [in Autosubst_MMap]
MMap_refl [in Autosubst_MMap]
MMap_fun [in Autosubst_MMapInstances]
MMap_pair [in Autosubst_MMapInstances]
MMap_list [in Autosubst_MMapInstances]
MMap_option [in Autosubst_MMapInstances]


P

prod_equiv [in RealizorPredicates]


R

Rename_Tterm [in T1]
Rename_ftype [in F1]
Rename_term [in Definitions]
rpe [in RealizorPredicates]


S

SubstLemmas_Tterm [in T1]
SubstLemmas_ftype [in F1]
SubstLemmas_term [in Definitions]
Subst_Tterm [in T1]
Subst_ftype [in F1]
Subst_term [in Definitions]
sub_proper [in Subsumption]
sub_preorder [in Subsumption]


T

te_sub [in Subsumption]
te_Proper_int [in TypeEquivalence]
te_equiv [in TypeEquivalence]



Projection Index

C

closed_leu [in Filters]
closed_int [in Filters]


D

decide [in Decidable]


E

equiv_closed [in RealizorPredicates]
excl_bot [in RealizorPredicates]


H

hsubst [in Autosubst_Classes]
hsubst_hsubst_ind [in Autosubst_Classes]
hsubst_hsubst_comp [in Autosubst_Classes]
hsubst_comp [in Autosubst_Classes]
hsubst_id [in Autosubst_Classes]


I

ids [in Autosubst_Classes]
id_hsubst [in Autosubst_Classes]
id_subst [in Autosubst_Classes]
incl_top [in RealizorPredicates]


M

mmap [in Autosubst_MMap]
mmap_comp [in Autosubst_MMap]
mmap_id [in Autosubst_MMap]
mmap_ext [in Autosubst_MMap]


O

only_filter [in RealizorPredicates]


R

rename [in Autosubst_Classes]
rename_subst [in Autosubst_Classes]


S

subst [in Autosubst_Classes]
subst_hsubst_comp [in Autosubst_Classes]
subst_comp [in Autosubst_Classes]
subst_id [in Autosubst_Classes]



Record Index

D

Dec [in Decidable]


H

HSubst [in Autosubst_Classes]
HSubstHSubstComp [in Autosubst_Classes]
HSubstHSubstInd [in Autosubst_Classes]
HSubstLemmas [in Autosubst_Classes]


I

Ids [in Autosubst_Classes]
IFilter [in Filters]


M

MMap [in Autosubst_MMap]
MMapExt [in Autosubst_MMap]
MMapLemmas [in Autosubst_MMap]


R

realizorPredicate [in RealizorPredicates]
Rename [in Autosubst_Classes]


S

Subst [in Autosubst_Classes]
SubstHSubstComp [in Autosubst_Classes]
SubstLemmas [in Autosubst_Classes]



Lemma Index

A

adequacy_cadequacy [in Framework]
agree_equiv [in Freevars]
agree_ty [in Freevars]


B

bot_filter [in Filters]


C

cint_csub_r [in Contexts]
cint_csub_l [in Contexts]
cint_Empty [in Contexts]
cint_Gamma_Empty [in Contexts]
cint_Empty_Gamma [in Contexts]
CLC_c [in CL1]
closure_closure_equiv [in Filters]
closure_filter_equiv [in Filters]
closure_filter [in Filters]
CL_stlc [in CL1]
CL_valid [in CL1]
compA [in Autosubst_Basics]
compatible_sub [in Interpretation]
compatible_sub_Gamma [in Interpretation]
compatible_cint [in Interpretation]
compatible_down [in Interpretation]
compatible_up [in Interpretation]
compile_subst [in T1]
compile_subst_full [in T1]
compile_ren_full [in T1]
comp_id [in Autosubst_Basics]
conj' [in Autosubst_Basics]
cons_drop_inv [in Contexts]
csplit [in Contexts]
csub_ext [in Contexts]
csub_cint_comp [in Contexts]
csub_comm [in Contexts]
csub_sub [in Contexts]
cte_eq [in Contexts]
cte_ext_int [in Contexts]
cte_ext [in Contexts]
cte_csub_R [in Contexts]
cte_csub_L [in Contexts]
cte_csub_equiv [in Contexts]
cte_trans [in Contexts]
cte_sym [in Contexts]
cte_pwr_refl [in Contexts]
cte_refl [in Contexts]
cte_comp_cint [in Contexts]
cte_assoc_cint [in Contexts]
cte_comm_cint [in Contexts]


E

equal_f [in Autosubst_Basics]
equiv_app_comp [in Filters]
equiv_filter [in Filters]
equiv_closure [in Filters]
equi_type [in Types]


F

feq_eq [in Contexts]
feq_trans [in Contexts]
feq_ext_int [in Contexts]
feq_ext [in Contexts]
filter_filter_equiv [in Filters]
filter_equiv_trans [in Filters]
filter_equiv_sym [in Filters]
filter_equiv_refl [in Filters]
filter_ind_filter [in Filters]
fold_ren_cons [in Autosubst_Tactics]
fromclosure_F [in Filters]


H

hcomp_dist_internal [in Autosubst_Derive]
hcomp_ren_internal [in Autosubst_Derive]
hcomp_lift_internal [in Autosubst_Derive]
hcomp_lift_n_internal [in Autosubst_Derive]
hsubst_compR [in Autosubst_Tactics]
hsubst_compX [in Autosubst_Tactics]
hsubst_compI [in Autosubst_Tactics]
hsubst_idX [in Autosubst_Tactics]


I

id_hsubstR [in Autosubst_Tactics]
id_hsubstX [in Autosubst_Tactics]
id_scompR [in Autosubst_Tactics]
id_scompX [in Autosubst_Tactics]
id_comp [in Autosubst_Basics]
inclosure_F [in Filters]
incl_inv_sub [in Subsumption]
intersect_realizable [in RealizorPredicates]
int_lam [in Premodel]
int_st [in Premodel]
int_x [in Premodel]
int_ty_rp [in STLC1]
int_ty_rp [in T1]
int_nat_filter [in T1]
int_ty_beta [in F1]
int_ty_subst_equiv [in F1]
int_ty_ren_equiv [in F1]
int_ty_feq_equiv [in F1]
int_ty_rp [in F1]
int_ty_rp [in CL1]
int_eq_O [in TypeEquivalence]
int_comm_O [in TypeEquivalence]
int_O [in TypeEquivalence]
int_IF [in Interpretation]
invtyInt [in Types]
invtyVar [in Types]
in_int_ty [in STLC1]
in_int_ty [in T1]
in_int_ty [in F1]
in_int_ty [in CL1]
iterate_0 [in Autosubst_Basics]
iterate_S [in Autosubst_Basics]
iter_param [in Autosubst_Derive]
iter_fp [in Autosubst_Derive]


K

k_nat [in T1]


L

lcc_c [in Framework]
lift_injn [in Autosubst_Lemmas]
lift_inj [in Autosubst_Lemmas]
lift_eta [in Autosubst_Basics]
lift_compR [in Autosubst_Basics]
lift_comp [in Autosubst_Basics]
lift_scons [in Autosubst_Basics]
lift0 [in Autosubst_Lemmas]
lift0 [in Autosubst_Basics]


M

mmap_const_instE [in Autosubst_MMap]
mmap_id_instE [in Autosubst_MMap]
mmap_compR [in Autosubst_MMap]
mmap_compX [in Autosubst_MMap]
mmap_idX [in Autosubst_MMap]
mmap_id_ext [in Autosubst_Derive]


P

plusA [in Autosubst_Basics]
plusnO [in Autosubst_Basics]
plusnS [in Autosubst_Basics]
plusOn [in Autosubst_Basics]
plusSn [in Autosubst_Basics]
possible_int_specialize [in RealizorPredicates]
possible_int_realizable [in RealizorPredicates]
prod_realizable [in RealizorPredicates]


R

rename_substX [in Autosubst_Tactics]
renS [in Autosubst_Lemmas]
ren_uncomp [in Autosubst_Lemmas]
rp_nat [in T1]


S

scomp_hcompR [in Autosubst_Tactics]
scomp_hcompX [in Autosubst_Tactics]
scomp_hcompI [in Autosubst_Tactics]
scons_eta [in Autosubst_Basics]
scons_comp [in Autosubst_Basics]
sn [in Framework]
sn_tsn [in Framework]
sn_stlc [in STLC1]
sn_T [in T1]
sn_gsn [in Reduction]
sn_system [in Termination]
sn_F [in F1]
steps_appR [in Reduction]
steps_appL [in Reduction]
step_beta_eq [in Reduction]
step_ty [in Termination]
step_n [in Termination]
subst_compR [in Autosubst_Tactics]
subst_compX [in Autosubst_Tactics]
subst_compI [in Autosubst_Tactics]
subst_idX [in Autosubst_Tactics]
sub_inv_int [in Subsumption]
sub_inv_F_G [in Subsumption]
sub_inv [in Subsumption]
sub_inv_O [in Subsumption]
sub_inv_A [in Subsumption]
sub_comp_int [in Subsumption]
sub_Int_R [in Subsumption]
sub_Int_L [in Subsumption]
sub_O [in Subsumption]
sub_int [in Subsumption]
sub_equiv [in Subsumption]
sub_trans [in Subsumption]
sub_refl [in Subsumption]


T

TC_c [in T1]
te_inv_incl [in Subsumption]
te_inv [in TypeEquivalence]
te_tcount_stable [in TypeEquivalence]
te_assoc_int [in TypeEquivalence]
te_comm_int [in TypeEquivalence]
te_comp_int [in TypeEquivalence]
te_comp_int_r [in TypeEquivalence]
te_comp_int_l [in TypeEquivalence]
te_inv_F [in TypeEquivalence]
te_O_r [in TypeEquivalence]
te_O_l [in TypeEquivalence]
te_inv_A [in TypeEquivalence]
te_inv_OMEGA [in TypeEquivalence]
te_trans [in TypeEquivalence]
te_sym [in TypeEquivalence]
te_refl [in TypeEquivalence]
top_sigma_valuation [in Framework]
top_rho_valid [in Framework]
top_app [in Filters]
top_filter [in Filters]
top_rp_realizable [in RealizorPredicates]
translates_skip [in F1]
tsn [in Framework]
tycsub [in Types]
tymon [in Types]
tyren_split [in Weakening]
tyren_var [in Weakening]
tyren_up [in Weakening]
tysubA [in Types]
tysubst [in Substitution]
tysubst_var [in Substitution]
tysub_split [in Substitution]
tysub_up [in Substitution]
tysub_lift [in Substitution]
tysub_beta [in Substitution]
tyVarA [in Types]
tyVarU [in Types]
ty_S [in T1]
ty_equiv [in Types]
ty_subsume [in Types]
T_valid [in T1]


U

upE [in Autosubst_Tactics]
upX [in Autosubst_Tactics]
up_comp_n [in Autosubst_Lemmas]
up_comp [in Autosubst_Lemmas]
up_liftn [in Autosubst_Lemmas]
up_lift1 [in Autosubst_Lemmas]
up_id_n [in Autosubst_Lemmas]
up_id [in Autosubst_Lemmas]
up_hcomp_n_internal [in Autosubst_Derive]
up_hcomp_internal [in Autosubst_Derive]
up_comp_n_internal [in Autosubst_Derive]
up_comp_internal [in Autosubst_Derive]
up_comp_subst_ren_n_internal [in Autosubst_Derive]
up_comp_subst_ren_internal [in Autosubst_Derive]
up_comp_ren_subst_n [in Autosubst_Derive]
up_comp_ren_subst [in Autosubst_Derive]
up_id_n_internal [in Autosubst_Derive]
up_id_internal [in Autosubst_Derive]
up_upren_n_internal [in Autosubst_Derive]
up_upren_internal [in Autosubst_Derive]


V

validates_up [in Framework]
validates_skip [in F1]
valid_up [in Interpretation]
valuation_up [in Framework]
val_ty_v [in Framework]


W

weaken [in Weakening]
weakening [in Weakening]


X

xe_closure [in Filters]



Section Index

G

General_Termination.LambdaCurry [in Framework]
General_Termination.Compiler [in Framework]
General_Termination [in Framework]


I

InternalLemmas [in Autosubst_Derive]
InternalLemmasHSubst [in Autosubst_Derive]


L

LemmasForFun [in Autosubst_Basics]
LemmasForHSubst [in Autosubst_Tactics]
LemmasForMMap [in Autosubst_MMap]
LemmasForSubst [in Autosubst_Tactics]


M

MMapConst [in Autosubst_MMap]
MMapId [in Autosubst_MMap]
MMapInstances [in Autosubst_MMapInstances]


S

SubstLemmas [in Autosubst_Lemmas]



Constructor Index

A

App [in Definitions]
app [in CL1]
arr [in STLC1]
arr [in T1]
arr [in F1]
Arr [in Definitions]
arr [in CL1]


B

base [in STLC1]
BASE [in Definitions]
base [in CL1]


C

CLapp [in CL1]
CLK [in CL1]
CLS [in CL1]
cl_step_appR [in CL1]
cl_step_appL [in CL1]
cl_stepK [in CL1]
cl_stepS [in CL1]


D

decide [in Decidable]


F

fapp [in F1]
fgen [in F1]
flam [in F1]
fspec [in F1]
FVAppL [in Freevars]
FVAppR [in Freevars]
fvar [in F1]
FVLam [in Freevars]
FVVar [in Freevars]


G

gsn [in Reduction]


H

hsubst [in Autosubst_Classes]
hsubst_hsubst_ind [in Autosubst_Classes]
hsubst_hsubst_comp [in Autosubst_Classes]


I

ids [in Autosubst_Classes]
inApp [in Filters]
includesDropL [in Subsumption]
includesDropR [in Subsumption]
includesF [in Subsumption]
inF [in Filters]
inI [in Filters]
inKtype [in T1]
Int [in Definitions]
intty [in Interpretation]


K

K [in CL1]


L

Lam [in Definitions]


M

mmap [in Autosubst_MMap]
mmap_ext [in Autosubst_MMap]
more [in Reduction]


N

NAT [in T1]


O

OMEGA [in Definitions]
one [in Reduction]
O_nat [in T1]


P

pi [in F1]


R

realizor [in RealizorPredicates]
rename [in Autosubst_Classes]


S

S [in CL1]
step_lam [in Reduction]
step_appR [in Reduction]
step_appL [in Reduction]
step_beta [in Reduction]
stlctyapp [in STLC1]
stlctylam [in STLC1]
stlctyvar [in STLC1]
subst [in Autosubst_Classes]
subst_hsubst_comp [in Autosubst_Classes]
S_nat [in T1]


T

Tapp [in T1]
TappL [in T1]
TappR [in T1]
Tbeta [in T1]
te_assoc_Int_rl [in Definitions]
te_assoc_Int_lr [in Definitions]
te_trans_ABC [in Definitions]
te_cong_Int [in Definitions]
te_comm_Int [in Definitions]
te_refl_OMEGA [in Definitions]
te_refl_F [in Definitions]
Tlam [in T1]
TO [in T1]
top_nat [in T1]
Tprec [in T1]
TprecO [in T1]
TprecS [in T1]
TS [in T1]
Ttyapp [in T1]
Ttylam [in T1]
TtyO [in T1]
Ttyprec [in T1]
TtyS [in T1]
Ttyvar [in T1]
Tvar [in T1]
tvar [in F1]
TVar [in Definitions]
tyAbs [in Definitions]
tyApp [in Definitions]
tyInt [in Definitions]
tyO [in Definitions]
tyrenInv [in Weakening]
tysubCons [in Substitution]
tysubRen [in Substitution]
tyVar [in Definitions]


U

UpB [in Definitions]
UpI [in Definitions]


V

val_ty_gamma [in Framework]
val_ty_gamma [in T1]



Notation Index

G

[| _ |] [in Framework]
[[ _ ]] _ [in Framework]


other

{ bind _ } (bind_scope) [in Autosubst_Classes]
{ bind _ in _ } (bind_scope) [in Autosubst_Classes]
{ bind _ of _ } (bind_scope) [in Autosubst_Classes]
{ bind _ of _ in _ } (bind_scope) [in Autosubst_Classes]
_ ..|[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ ..|[ _ /] (subst_scope) [in Autosubst_Classes]
_ ..|[ _ ] (subst_scope) [in Autosubst_Classes]
_ .|[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ .|[ _ /] (subst_scope) [in Autosubst_Classes]
_ .|[ _ ] (subst_scope) [in Autosubst_Classes]
_ >>| _ (subst_scope) [in Autosubst_Classes]
_ ..[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ ..[ _ /] (subst_scope) [in Autosubst_Classes]
_ ..[ _ ] (subst_scope) [in Autosubst_Classes]
_ .[ _ , _ , .. , _ /] (subst_scope) [in Autosubst_Classes]
_ .[ _ /] (subst_scope) [in Autosubst_Classes]
_ .[ _ ] (subst_scope) [in Autosubst_Classes]
_ >> _ (subst_scope) [in Autosubst_Classes]
_ .: _ (subst_scope) [in Autosubst_Basics]
_ >>> _ (subst_scope) [in Autosubst_Basics]
_ == _ (type_scope) [in Definitions]
_ ==> _ [in T1]
_ --> _ [in T1]
_ ~ _ [in Filters]
_ @ _ [in Filters]
_ >=1 _ [in Definitions]
_ ==1 _ [in Definitions]
_ =1 _ [in Definitions]
_ & _ [in Definitions]
_ >= _ [in Definitions]
_ * _ [in Definitions]
_ o _ [in Definitions]
_ --> _ [in Definitions]
_ --> _ [in CL1]
_ =R= _ [in RealizorPredicates]
' _ [in T1]
( + _ ) [in Autosubst_Basics]
[ _ ] _ [in Interpretation]
[[ _ ]] _ [in STLC1]
[[ _ ]] [in T1]
[[ _ ]] _ [in F1]
[[ _ ]] _ [in CL1]



Inductive Index

A

app [in Filters]


B

basetype [in Definitions]


C

CL [in CL1]
closure [in Filters]
cl_step [in CL1]
CL_ty [in CL1]


D

Dec [in Decidable]


F

Ftype [in F1]
FV [in Freevars]
f_ty [in F1]


G

GSN [in Reduction]


H

HSubst [in Autosubst_Classes]
HSubstHSubstComp [in Autosubst_Classes]
HSubstHSubstInd [in Autosubst_Classes]


I

Ids [in Autosubst_Classes]
includes [in Subsumption]
inttype [in Definitions]
int_nat [in T1]
int_t [in Interpretation]


K

Ktype [in T1]


M

MMap [in Autosubst_MMap]
MMapExt [in Autosubst_MMap]


R

Rename [in Autosubst_Classes]


S

simpletype [in STLC1]
simpletype [in CL1]
step [in Reduction]
steps [in Reduction]
stlc_ty [in STLC1]
Subst [in Autosubst_Classes]
SubstHSubstComp [in Autosubst_Classes]


T

term [in Definitions]
Tterm [in T1]
Ttype [in T1]
ty [in Definitions]
type [in Definitions]
type_equiv [in Definitions]
tyren [in Weakening]
tysub [in Substitution]
T_ty [in T1]
T_step [in T1]


V

val_ty [in Framework]
val_ty [in T1]



Abbreviation Index

U

upn [in Autosubst_Classes]



Definition Index

A

adequacy [in Framework]
annot [in Autosubst_Basics]


B

bot [in Filters]


C

cadequacy [in Framework]
cint [in Definitions]
CLC [in CL1]
compatible [in Interpretation]
compile [in T1]
compiler_consistency [in Framework]
context [in Definitions]
count [in TypeEquivalence]
csub [in Definitions]
cte [in Definitions]


D

dec [in Decidable]
drop [in Definitions]


E

Empty [in Definitions]


F

filter_equiv [in Filters]
funcomp [in Autosubst_Basics]
f_ctx [in F1]


H

hcomp [in Autosubst_Classes]


I

id [in Autosubst_Basics]
inc [in Weakening]
int [in Definitions]
intersect [in RealizorPredicates]
int_ty [in STLC1]
int_ty [in T1]
int_ty [in F1]
int_app [in Filters]
int_ty [in CL1]
iterate [in Autosubst_Basics]


L

lcc [in Framework]
lift [in Autosubst_Basics]


P

pi_equiv [in RealizorPredicates]
possible_int [in RealizorPredicates]
prod [in RealizorPredicates]
PWR [in Definitions]


R

rc_ctx [in Framework]
realizorCandidate [in RealizorPredicates]
ren [in Autosubst_Classes]
rp_preservation [in Framework]
rp_equiv [in RealizorPredicates]


S

scomp [in Autosubst_Classes]
scons [in Autosubst_Basics]
SN [in Reduction]
stlc_ctx [in STLC1]
subsumes [in Definitions]


T

tcount [in TypeEquivalence]
top [in Filters]
top_sigma [in Framework]
top_rho [in Framework]
top_rp [in RealizorPredicates]
translates [in F1]
TSN [in Framework]
typeable [in T1]
type_context [in Interpretation]
t_ctx [in Framework]
T_ctx [in T1]


U

up [in Autosubst_Classes]
upren [in Autosubst_Classes]


V

valid [in Interpretation]
validates [in Framework]
validation [in Framework]
valuation [in Framework]
var [in Autosubst_Basics]


_

_bind [in Autosubst_Classes]



Variable Index

G

General_Termination.LambdaCurry.tty [in Framework]
General_Termination.Compiler.tstep [in Framework]
General_Termination.Compiler.vtty [in Framework]
General_Termination.Compiler.ctty [in Framework]
General_Termination.Compiler.compiler [in Framework]
General_Termination.Compiler.tterm [in Framework]
General_Termination.int_ty [in Framework]
General_Termination.ttype [in Framework]


M

MMapInstances.A [in Autosubst_MMapInstances]
MMapInstances.B [in Autosubst_MMapInstances]
MMapInstances.C [in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_C [in Autosubst_MMapInstances]
MMapInstances.MMapExt_A_B [in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_C [in Autosubst_MMapInstances]
MMapInstances.MMapLemmas_A_B [in Autosubst_MMapInstances]
MMapInstances.MMap_A_C [in Autosubst_MMapInstances]
MMapInstances.MMap_A_B [in Autosubst_MMapInstances]



Library Index

A

Autosubst
Autosubst_MMapInstances
Autosubst_Classes
Autosubst_Derive
Autosubst_MMap
Autosubst_Tactics
Autosubst_Basics
Autosubst_Lemmas


C

CL1
Contexts


D

Decidable
Definitions


F

Filters
Framework
Freevars
F1
F2


I

Interpretation


P

Premodel


R

RealizorPredicates
Reduction


S

STLC1
Substitution
Subsumption


T

Termination
TypeEquivalence
Types
T1


W

Weakening



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (640 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (51 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (15 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (235 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (13 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (103 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (42 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (65 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (17 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (29 entries)

This page has been generated by coqdoc