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 (437 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 (9 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 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 (47 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 (18 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 _ other (2 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 (28 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 (31 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 (116 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 (1 entry)
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)
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 (28 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (151 entries)

Global Index

A

all [constructor, in Autosubst.SystemF_cbv]
ap [definition, in Autosubst.Autosubst2]
apc [definition, in Autosubst.Autosubst2]
app [constructor, in Autosubst.SystemF_cbv]
arr [constructor, in Autosubst.SystemF_cbv]
Asimpl [record, in Autosubst.Autosubst2]
Asimpl [inductive, in Autosubst.Autosubst2]
AsimplAsimplInst_vl [instance, in Autosubst.SystemF_cbv]
AsimplAsimplInst_tm [instance, in Autosubst.SystemF_cbv]
AsimplAsimplInst_ty [instance, in Autosubst.SystemF_cbv]
AsimplCast_vl_ty [instance, in Autosubst.SystemF_cbv]
AsimplCast_tm_vl [instance, in Autosubst.SystemF_cbv]
AsimplCast_tm_ty [instance, in Autosubst.SystemF_cbv]
AsimplComp [record, in Autosubst.Autosubst2]
AsimplComp [inductive, in Autosubst.Autosubst2]
AsimplCompAsso [instance, in Autosubst.Autosubst2]
AsimplCompAsso_vl [instance, in Autosubst.SystemF_cbv]
AsimplCompAsso_tm [instance, in Autosubst.SystemF_cbv]
AsimplCompAsso_ty [instance, in Autosubst.SystemF_cbv]
AsimplCompCongr_vl [instance, in Autosubst.SystemF_cbv]
AsimplCompCongr_tm [instance, in Autosubst.SystemF_cbv]
AsimplCompCongr_ty [instance, in Autosubst.SystemF_cbv]
AsimplCompCongr'_vl [instance, in Autosubst.SystemF_cbv]
AsimplCompCongr'_tm [instance, in Autosubst.SystemF_cbv]
AsimplCompCongr'_ty [instance, in Autosubst.SystemF_cbv]
AsimplCompConsL [instance, in Autosubst.Autosubst2]
asimplCompEqn [projection, in Autosubst.Autosubst2]
asimplCompEqn [constructor, in Autosubst.Autosubst2]
asimplCompEqn_vl [projection, in Autosubst.SystemF_cbv]
asimplCompEqn_vl [constructor, in Autosubst.SystemF_cbv]
asimplCompEqn_tm [projection, in Autosubst.SystemF_cbv]
asimplCompEqn_tm [constructor, in Autosubst.SystemF_cbv]
asimplCompEqn_ty [projection, in Autosubst.SystemF_cbv]
asimplCompEqn_ty [constructor, in Autosubst.SystemF_cbv]
AsimplCompIdL [instance, in Autosubst.Autosubst2]
AsimplCompIdL_vl [instance, in Autosubst.SystemF_cbv]
AsimplCompIdL_ty [instance, in Autosubst.SystemF_cbv]
AsimplCompIdR [instance, in Autosubst.Autosubst2]
AsimplCompIdR_vl [instance, in Autosubst.SystemF_cbv]
AsimplCompIdR_tm [instance, in Autosubst.SystemF_cbv]
AsimplCompIdR_ty [instance, in Autosubst.SystemF_cbv]
AsimplCompRefl [instance, in Autosubst.Autosubst2]
AsimplCompRefl_vl [instance, in Autosubst.SystemF_cbv]
AsimplCompRefl_tm [instance, in Autosubst.SystemF_cbv]
AsimplCompRefl_ty [instance, in Autosubst.SystemF_cbv]
AsimplCompS' [instance, in Autosubst.Autosubst2]
AsimplComp_vl [record, in Autosubst.SystemF_cbv]
AsimplComp_vl [inductive, in Autosubst.SystemF_cbv]
AsimplComp_tm [record, in Autosubst.SystemF_cbv]
AsimplComp_tm [inductive, in Autosubst.SystemF_cbv]
AsimplComp_ty [record, in Autosubst.SystemF_cbv]
AsimplComp_ty [inductive, in Autosubst.SystemF_cbv]
AsimplCons [record, in Autosubst.Autosubst2]
AsimplCons [inductive, in Autosubst.Autosubst2]
asimplConsEqn [projection, in Autosubst.Autosubst2]
asimplConsEqn [constructor, in Autosubst.Autosubst2]
AsimplConsEta [instance, in Autosubst.Autosubst2]
AsimplConsRefl [instance, in Autosubst.Autosubst2]
asimplEqn [projection, in Autosubst.Autosubst2]
asimplEqn [constructor, in Autosubst.Autosubst2]
AsimplGen [record, in Autosubst.Autosubst2]
AsimplGen [inductive, in Autosubst.Autosubst2]
AsimplGenComp_vl [instance, in Autosubst.SystemF_cbv]
AsimplGenComp_tm [instance, in Autosubst.SystemF_cbv]
AsimplGenComp_ty [instance, in Autosubst.SystemF_cbv]
AsimplGenCons [instance, in Autosubst.Autosubst2]
asimplGenEqn [projection, in Autosubst.Autosubst2]
asimplGenEqn [constructor, in Autosubst.Autosubst2]
AsimplGenInst [record, in Autosubst.Autosubst2]
AsimplGenInst [inductive, in Autosubst.Autosubst2]
AsimplGenInstConsS [instance, in Autosubst.Autosubst2]
AsimplGenInstCons0 [instance, in Autosubst.Autosubst2]
asimplGenInstEqn [projection, in Autosubst.Autosubst2]
asimplGenInstEqn [constructor, in Autosubst.Autosubst2]
AsimplGenInstIdren [instance, in Autosubst.Autosubst2]
AsimplGenInstRefl [instance, in Autosubst.Autosubst2]
AsimplGenInstShift [instance, in Autosubst.Autosubst2]
AsimplGenInstShiftComp [instance, in Autosubst.Autosubst2]
AsimplGenRefl [instance, in Autosubst.Autosubst2]
AsimplGenRen [instance, in Autosubst.Autosubst2]
AsimplGen_Asimpl_Ext [instance, in Autosubst.Autosubst2]
AsimplGen_Asimpl [instance, in Autosubst.Autosubst2]
AsimplId_vl [instance, in Autosubst.SystemF_cbv]
AsimplId_tm [instance, in Autosubst.SystemF_cbv]
AsimplId_ty [instance, in Autosubst.SystemF_cbv]
AsimplIndex [record, in Autosubst.Autosubst2]
AsimplIndex [inductive, in Autosubst.Autosubst2]
AsimplIndex [module, in Autosubst.Autosubst2]
asimplIndexEqn [projection, in Autosubst.Autosubst2]
asimplIndexEqn [constructor, in Autosubst.Autosubst2]
AsimplIndexRefl [instance, in Autosubst.Autosubst2]
AsimplIndex.EO [constructor, in Autosubst.Autosubst2]
AsimplIndex.EPlus [constructor, in Autosubst.Autosubst2]
AsimplIndex.ES [constructor, in Autosubst.Autosubst2]
AsimplIndex.eval_nfE [lemma, in Autosubst.Autosubst2]
AsimplIndex.eval_nf [definition, in Autosubst.Autosubst2]
AsimplIndex.eval_exp [definition, in Autosubst.Autosubst2]
AsimplIndex.EVar [constructor, in Autosubst.Autosubst2]
AsimplIndex.exp [inductive, in Autosubst.Autosubst2]
AsimplIndex.flatten [definition, in Autosubst.Autosubst2]
AsimplIndex.flatten_cat [lemma, in Autosubst.Autosubst2]
AsimplIndex.nf [definition, in Autosubst.Autosubst2]
AsimplIndex.normalize [definition, in Autosubst.Autosubst2]
AsimplIndex.normalize_sound [lemma, in Autosubst.Autosubst2]
AsimplIndex.ReifyExp [record, in Autosubst.Autosubst2]
AsimplIndex.ReifyO [instance, in Autosubst.Autosubst2]
AsimplIndex.ReifyPlus [instance, in Autosubst.Autosubst2]
AsimplIndex.ReifyS [instance, in Autosubst.Autosubst2]
AsimplIndex.ReifyVar [instance, in Autosubst.Autosubst2]
asimplInstEqn_vl [projection, in Autosubst.SystemF_cbv]
asimplInstEqn_vl [constructor, in Autosubst.SystemF_cbv]
asimplInstEqn_tm [projection, in Autosubst.SystemF_cbv]
asimplInstEqn_tm [constructor, in Autosubst.SystemF_cbv]
asimplInstEqn_ty [projection, in Autosubst.SystemF_cbv]
asimplInstEqn_ty [constructor, in Autosubst.SystemF_cbv]
AsimplInstInst_vl [instance, in Autosubst.SystemF_cbv]
AsimplInstInst_tm [instance, in Autosubst.SystemF_cbv]
AsimplInstInst_ty [instance, in Autosubst.SystemF_cbv]
AsimplInstRefl_vl [instance, in Autosubst.SystemF_cbv]
AsimplInstRefl_tm [instance, in Autosubst.SystemF_cbv]
AsimplInstRefl_ty [instance, in Autosubst.SystemF_cbv]
AsimplInstVar_vl [instance, in Autosubst.SystemF_cbv]
AsimplInstVar_ty [instance, in Autosubst.SystemF_cbv]
asimplInst_tlam [instance, in Autosubst.SystemF_cbv]
asimplInst_lam [instance, in Autosubst.SystemF_cbv]
asimplInst_vt [instance, in Autosubst.SystemF_cbv]
asimplInst_tapp [instance, in Autosubst.SystemF_cbv]
asimplInst_app [instance, in Autosubst.SystemF_cbv]
AsimplInst_vl [record, in Autosubst.SystemF_cbv]
AsimplInst_vl [inductive, in Autosubst.SystemF_cbv]
AsimplInst_tm [record, in Autosubst.SystemF_cbv]
AsimplInst_tm [inductive, in Autosubst.SystemF_cbv]
asimplInst_all [instance, in Autosubst.SystemF_cbv]
asimplInst_arr [instance, in Autosubst.SystemF_cbv]
AsimplInst_ty [record, in Autosubst.SystemF_cbv]
AsimplInst_ty [inductive, in Autosubst.SystemF_cbv]
AsimplRec [record, in Autosubst.Autosubst2]
AsimplRec [inductive, in Autosubst.Autosubst2]
asimplRecEqn [projection, in Autosubst.Autosubst2]
asimplRecEqn [constructor, in Autosubst.Autosubst2]
AsimplRefl_vl [instance, in Autosubst.SystemF_cbv]
AsimplRefl_tm [instance, in Autosubst.SystemF_cbv]
AsimplRefl_ty [instance, in Autosubst.SystemF_cbv]
AsimplRen [record, in Autosubst.Autosubst2]
AsimplRen [inductive, in Autosubst.Autosubst2]
AsimplRenComp [record, in Autosubst.Autosubst2]
AsimplRenComp [inductive, in Autosubst.Autosubst2]
AsimplRenCompComp [instance, in Autosubst.Autosubst2]
AsimplRenCompCons [instance, in Autosubst.Autosubst2]
asimplRenCompEqn [projection, in Autosubst.Autosubst2]
asimplRenCompEqn [constructor, in Autosubst.Autosubst2]
AsimplRenCompIdL [instance, in Autosubst.Autosubst2]
AsimplRenCompIdR [instance, in Autosubst.Autosubst2]
AsimplRenCompRefl [instance, in Autosubst.Autosubst2]
AsimplRenCompShift [instance, in Autosubst.Autosubst2]
AsimplRenCompShift0 [instance, in Autosubst.Autosubst2]
AsimplRenCons [record, in Autosubst.Autosubst2]
AsimplRenCons [inductive, in Autosubst.Autosubst2]
AsimplRenConsDef [instance, in Autosubst.Autosubst2]
asimplRenConsEqn [projection, in Autosubst.Autosubst2]
asimplRenConsEqn [constructor, in Autosubst.Autosubst2]
AsimplRenConsEta [instance, in Autosubst.Autosubst2]
asimplRenEqn [projection, in Autosubst.Autosubst2]
asimplRenEqn [constructor, in Autosubst.Autosubst2]
AsimplRenInst [record, in Autosubst.Autosubst2]
AsimplRenInst [inductive, in Autosubst.Autosubst2]
AsimplRenInstConsS [instance, in Autosubst.Autosubst2]
AsimplRenInstCons0 [instance, in Autosubst.Autosubst2]
asimplRenInstEqn [projection, in Autosubst.Autosubst2]
asimplRenInstEqn [constructor, in Autosubst.Autosubst2]
AsimplRenInstIdren [instance, in Autosubst.Autosubst2]
AsimplRenInstRefl [instance, in Autosubst.Autosubst2]
AsimplRenInstShift [instance, in Autosubst.Autosubst2]
AsimplRenInstShiftComp [instance, in Autosubst.Autosubst2]
AsimplRenRefl [instance, in Autosubst.Autosubst2]
AsimplRenScons [instance, in Autosubst.Autosubst2]
AsimplRenShift [record, in Autosubst.Autosubst2]
AsimplRenShift [inductive, in Autosubst.Autosubst2]
AsimplRenShiftDef [instance, in Autosubst.Autosubst2]
asimplRenShiftEqn [projection, in Autosubst.Autosubst2]
asimplRenShiftEqn [constructor, in Autosubst.Autosubst2]
AsimplRenShiftIdren [instance, in Autosubst.Autosubst2]
AsimplRenSShift [instance, in Autosubst.Autosubst2]
AsimplSubstCompRen [record, in Autosubst.Autosubst2]
AsimplSubstCompRen [inductive, in Autosubst.Autosubst2]
AsimplSubstCompRenAssoc [instance, in Autosubst.Autosubst2]
asimplSubstCompRenEqn [projection, in Autosubst.Autosubst2]
asimplSubstCompRenEqn [constructor, in Autosubst.Autosubst2]
AsimplSubstCompRenRefl [instance, in Autosubst.Autosubst2]
AsimplSubstComp_vl [instance, in Autosubst.SystemF_cbv]
AsimplSubstComp_tm [instance, in Autosubst.SystemF_cbv]
AsimplSubstComp_ty [instance, in Autosubst.SystemF_cbv]
AsimplSubstCongr_vl [instance, in Autosubst.SystemF_cbv]
AsimplSubstCongr_tm [instance, in Autosubst.SystemF_cbv]
AsimplSubstCongr_ty [instance, in Autosubst.SystemF_cbv]
asimplSubstEqn_vl [projection, in Autosubst.SystemF_cbv]
asimplSubstEqn_vl [constructor, in Autosubst.SystemF_cbv]
asimplSubstEqn_tm [projection, in Autosubst.SystemF_cbv]
asimplSubstEqn_tm [constructor, in Autosubst.SystemF_cbv]
asimplSubstEqn_ty [projection, in Autosubst.SystemF_cbv]
asimplSubstEqn_ty [constructor, in Autosubst.SystemF_cbv]
AsimplSubstRefl_vl [instance, in Autosubst.SystemF_cbv]
AsimplSubstRefl_tm [instance, in Autosubst.SystemF_cbv]
AsimplSubstRefl_ty [instance, in Autosubst.SystemF_cbv]
AsimplSubstUp_vl_vl [instance, in Autosubst.SystemF_cbv]
AsimplSubstUp_vl_ty [instance, in Autosubst.SystemF_cbv]
AsimplSubstUp_tm_vl [instance, in Autosubst.SystemF_cbv]
AsimplSubstUp_tm_ty [instance, in Autosubst.SystemF_cbv]
AsimplSubstUp_ty_ty [instance, in Autosubst.SystemF_cbv]
AsimplSubst_vl [record, in Autosubst.SystemF_cbv]
AsimplSubst_vl [inductive, in Autosubst.SystemF_cbv]
AsimplSubst_tm [record, in Autosubst.SystemF_cbv]
AsimplSubst_tm [inductive, in Autosubst.SystemF_cbv]
AsimplSubst_ty [record, in Autosubst.SystemF_cbv]
AsimplSubst_ty [inductive, in Autosubst.SystemF_cbv]
AsimplToVar_vl [instance, in Autosubst.SystemF_cbv]
AsimplToVar_ty [instance, in Autosubst.SystemF_cbv]
AsimplVarInst [record, in Autosubst.Autosubst2]
AsimplVarInst [inductive, in Autosubst.Autosubst2]
AsimplVarInstConsS [instance, in Autosubst.Autosubst2]
AsimplVarInstCons0 [instance, in Autosubst.Autosubst2]
asimplVarInstEqn [projection, in Autosubst.Autosubst2]
asimplVarInstEqn [constructor, in Autosubst.Autosubst2]
AsimplVarInstRefl [instance, in Autosubst.Autosubst2]
AsimplVarInstShiftComp [instance, in Autosubst.Autosubst2]
Autosubst2 [library]
axioms [library]


C

castren_vl_tm [definition, in Autosubst.SystemF_cbv]
castren_vl_ty [definition, in Autosubst.SystemF_cbv]
castren_tm_vl [definition, in Autosubst.SystemF_cbv]
castren_tm_ty [definition, in Autosubst.SystemF_cbv]
cast_vl_tm [definition, in Autosubst.SystemF_cbv]
cast_vl_ty [definition, in Autosubst.SystemF_cbv]
cast_tm_vl [definition, in Autosubst.SystemF_cbv]
cast_tm_ty [definition, in Autosubst.SystemF_cbv]
comp [definition, in Autosubst.Autosubst2]
compE_subst_subst_vl [definition, in Autosubst.SystemF_cbv]
compE_subst_subst_tm [definition, in Autosubst.SystemF_cbv]
compE_subst_ren_vl [definition, in Autosubst.SystemF_cbv]
compE_subst_ren_tm [definition, in Autosubst.SystemF_cbv]
compE_ren_subst_vl [definition, in Autosubst.SystemF_cbv]
compE_ren_subst_tm [definition, in Autosubst.SystemF_cbv]
compE_ren_ren_vl [definition, in Autosubst.SystemF_cbv]
compE_ren_ren_tm [definition, in Autosubst.SystemF_cbv]
compE_subst_subst_ty [definition, in Autosubst.SystemF_cbv]
compE_subst_ren_ty [definition, in Autosubst.SystemF_cbv]
compE_ren_subst_ty [definition, in Autosubst.SystemF_cbv]
compE_ren_ren_ty [definition, in Autosubst.SystemF_cbv]
compren_vl [definition, in Autosubst.SystemF_cbv]
compren_tm [definition, in Autosubst.SystemF_cbv]
compren_ty [definition, in Autosubst.SystemF_cbv]
compTrans_subst_subst_vl [definition, in Autosubst.SystemF_cbv]
compTrans_subst_subst_tm [definition, in Autosubst.SystemF_cbv]
compTrans_subst_ren_vl [definition, in Autosubst.SystemF_cbv]
compTrans_subst_ren_tm [definition, in Autosubst.SystemF_cbv]
compTrans_ren_subst_vl [definition, in Autosubst.SystemF_cbv]
compTrans_ren_subst_tm [definition, in Autosubst.SystemF_cbv]
compTrans_ren_ren_vl [definition, in Autosubst.SystemF_cbv]
compTrans_ren_ren_tm [definition, in Autosubst.SystemF_cbv]
compTrans_subst_subst_ty [definition, in Autosubst.SystemF_cbv]
compTrans_subst_ren_ty [definition, in Autosubst.SystemF_cbv]
compTrans_ren_subst_ty [definition, in Autosubst.SystemF_cbv]
compTrans_ren_ren_ty [definition, in Autosubst.SystemF_cbv]
comp_vl [definition, in Autosubst.SystemF_cbv]
comp_tm [definition, in Autosubst.SystemF_cbv]
comp_ty [definition, in Autosubst.SystemF_cbv]
congr_tlam [definition, in Autosubst.SystemF_cbv]
congr_lam [definition, in Autosubst.SystemF_cbv]
congr_vt [definition, in Autosubst.SystemF_cbv]
congr_tapp [definition, in Autosubst.SystemF_cbv]
congr_app [definition, in Autosubst.SystemF_cbv]
congr_all [definition, in Autosubst.SystemF_cbv]
congr_arr [definition, in Autosubst.SystemF_cbv]
consistency [lemma, in Autosubst.sem]
ctx [definition, in Autosubst.sem]


E

E [abbreviation, in Autosubst.sem]
eq_of_subst [definition, in Autosubst.Autosubst2]
eq_up_vl_vl [definition, in Autosubst.SystemF_cbv]
eq_up_vl_ty [definition, in Autosubst.SystemF_cbv]
eq_up_tm_vl [definition, in Autosubst.SystemF_cbv]
eq_up_tm_ty [definition, in Autosubst.SystemF_cbv]
eq_cast_vl_tm [definition, in Autosubst.SystemF_cbv]
eq_cast_vl_ty [definition, in Autosubst.SystemF_cbv]
eq_cast_tm_vl [definition, in Autosubst.SystemF_cbv]
eq_cast_tm_ty [definition, in Autosubst.SystemF_cbv]
eq_toVar_vl [definition, in Autosubst.SystemF_cbv]
eq_up_ty_ty [definition, in Autosubst.SystemF_cbv]
eq_toVar_ty [definition, in Autosubst.SystemF_cbv]
eval [inductive, in Autosubst.sem]
eval_val [constructor, in Autosubst.sem]
eval_tapp [constructor, in Autosubst.sem]
eval_app [constructor, in Autosubst.sem]
E_subst1 [lemma, in Autosubst.sem]


F

fext [definition, in Autosubst.axioms]
funcomp [definition, in Autosubst.Autosubst2]
functional_extensionality [axiom, in Autosubst.axioms]
funext [projection, in Autosubst.Autosubst2]
Funext [record, in Autosubst.Autosubst2]
funext [constructor, in Autosubst.Autosubst2]
Funext [inductive, in Autosubst.Autosubst2]


G

get [definition, in Autosubst.sem]
get_map [lemma, in Autosubst.sem]


H

has_ty_ind [definition, in Autosubst.sem]


I

idren [definition, in Autosubst.Autosubst2]
id_vl [definition, in Autosubst.SystemF_cbv]
id_tm [definition, in Autosubst.SystemF_cbv]
id_ty [definition, in Autosubst.SystemF_cbv]
index [definition, in Autosubst.Autosubst2]
inst [definition, in Autosubst.Autosubst2]
inst_of_substType [projection, in Autosubst.Autosubst2]


L

L [definition, in Autosubst.sem]
lam [constructor, in Autosubst.SystemF_cbv]
lift [definition, in Autosubst.Autosubst2]


M

mixin_of_substType [projection, in Autosubst.Autosubst2]


N

nilA [definition, in Autosubst.sem]
normalization [lemma, in Autosubst.sem]


P

Pack [constructor, in Autosubst.Autosubst2]
pext [lemma, in Autosubst.axioms]
propositional_extensionality [axiom, in Autosubst.axioms]


Q

QuoteLookup [record, in Autosubst.Autosubst2]
quote_lookup_further [instance, in Autosubst.Autosubst2]
quote_lookup_end [instance, in Autosubst.Autosubst2]
quote_lookup_here [instance, in Autosubst.Autosubst2]
quote_lookup [section, in Autosubst.Autosubst2]


R

ren [definition, in Autosubst.Autosubst2]
ren_of [definition, in Autosubst.Autosubst2]
ren_inst_vl [definition, in Autosubst.SystemF_cbv]
ren_inst_tm [definition, in Autosubst.SystemF_cbv]
ren_vl [definition, in Autosubst.SystemF_cbv]
ren_tm [definition, in Autosubst.SystemF_cbv]
ren_inst_ty [lemma, in Autosubst.SystemF_cbv]
ren_ty [definition, in Autosubst.SystemF_cbv]


S

scons [definition, in Autosubst.Autosubst2]
sem [library]
soundness [lemma, in Autosubst.sem]
soundness_nil [lemma, in Autosubst.sem]
substEq [definition, in Autosubst.Autosubst2]
substMixin [record, in Autosubst.Autosubst2]
substMixin_vl [definition, in Autosubst.SystemF_cbv]
substMixin_tm [definition, in Autosubst.SystemF_cbv]
substMixin_ty [definition, in Autosubst.SystemF_cbv]
substType [record, in Autosubst.Autosubst2]
substType_vl [definition, in Autosubst.SystemF_cbv]
substType_tm [definition, in Autosubst.SystemF_cbv]
substType_ty [definition, in Autosubst.SystemF_cbv]
subst_ofType [projection, in Autosubst.Autosubst2]
subst_of_substType [projection, in Autosubst.Autosubst2]
subst_of [definition, in Autosubst.Autosubst2]
subst_eq_vl [definition, in Autosubst.SystemF_cbv]
subst_eq_tm [definition, in Autosubst.SystemF_cbv]
subst_vl [definition, in Autosubst.SystemF_cbv]
subst_tm [definition, in Autosubst.SystemF_cbv]
subst_of_vl [definition, in Autosubst.SystemF_cbv]
subst_of_tm [definition, in Autosubst.SystemF_cbv]
subst_eq_ty [definition, in Autosubst.SystemF_cbv]
subst_ty [definition, in Autosubst.SystemF_cbv]
subst_of_ty [definition, in Autosubst.SystemF_cbv]
SystemF_cbv [library]


T

tapp [constructor, in Autosubst.SystemF_cbv]
tlam [constructor, in Autosubst.SystemF_cbv]
tm [inductive, in Autosubst.SystemF_cbv]
tm_ty_ind [definition, in Autosubst.sem]
tm_ty [inductive, in Autosubst.sem]
toSubst_vl [definition, in Autosubst.SystemF_cbv]
toSubst_tm [definition, in Autosubst.SystemF_cbv]
toSubst_ty [definition, in Autosubst.SystemF_cbv]
toVarRen_vl [definition, in Autosubst.SystemF_cbv]
toVarRen_tm [definition, in Autosubst.SystemF_cbv]
toVarRen_ty [definition, in Autosubst.SystemF_cbv]
toVar_vl [definition, in Autosubst.SystemF_cbv]
toVar_tm [definition, in Autosubst.SystemF_cbv]
toVar_ty [definition, in Autosubst.SystemF_cbv]
ty [inductive, in Autosubst.SystemF_cbv]
ty_tlam [constructor, in Autosubst.sem]
ty_lam [constructor, in Autosubst.sem]
ty_var [constructor, in Autosubst.sem]
ty_val [constructor, in Autosubst.sem]
ty_tapp [constructor, in Autosubst.sem]
ty_app [constructor, in Autosubst.sem]


U

upId_vl_vl [definition, in Autosubst.SystemF_cbv]
upId_vl_ty [definition, in Autosubst.SystemF_cbv]
upId_tm_vl [definition, in Autosubst.SystemF_cbv]
upId_tm_ty [definition, in Autosubst.SystemF_cbv]
upId_ty_ty [definition, in Autosubst.SystemF_cbv]
upren_vl_vl [definition, in Autosubst.SystemF_cbv]
upren_vl_ty [definition, in Autosubst.SystemF_cbv]
upren_tm_vl [definition, in Autosubst.SystemF_cbv]
upren_tm_ty [definition, in Autosubst.SystemF_cbv]
upren_ty_ty [definition, in Autosubst.SystemF_cbv]
up_ren_ren [definition, in Autosubst.Autosubst2]
up_ren [definition, in Autosubst.Autosubst2]
up_ren_up_vl_ty [definition, in Autosubst.SystemF_cbv]
up_ren_up_vl_vl [definition, in Autosubst.SystemF_cbv]
up_subst_subst_vl_vl [definition, in Autosubst.SystemF_cbv]
up_subst_subst_vl_ty [definition, in Autosubst.SystemF_cbv]
up_subst_subst_tm_vl [definition, in Autosubst.SystemF_cbv]
up_subst_subst_tm_ty [definition, in Autosubst.SystemF_cbv]
up_subst_ren_vl_vl [definition, in Autosubst.SystemF_cbv]
up_subst_ren_vl_ty [definition, in Autosubst.SystemF_cbv]
up_subst_ren_tm_vl [definition, in Autosubst.SystemF_cbv]
up_subst_ren_tm_ty [definition, in Autosubst.SystemF_cbv]
up_ren_subst_vl_vl [definition, in Autosubst.SystemF_cbv]
up_ren_subst_vl_ty [definition, in Autosubst.SystemF_cbv]
up_ren_subst_tm_vl [definition, in Autosubst.SystemF_cbv]
up_ren_subst_tm_ty [definition, in Autosubst.SystemF_cbv]
up_vl_vl [definition, in Autosubst.SystemF_cbv]
up_vl_ty [definition, in Autosubst.SystemF_cbv]
up_tm_vl [definition, in Autosubst.SystemF_cbv]
up_tm_ty [definition, in Autosubst.SystemF_cbv]
up_ren_up [lemma, in Autosubst.SystemF_cbv]
up_subst_subst_ty_ty [definition, in Autosubst.SystemF_cbv]
up_subst_ren_ty_ty [definition, in Autosubst.SystemF_cbv]
up_ren_subst_ty_ty [definition, in Autosubst.SystemF_cbv]
up_ty_ty [definition, in Autosubst.SystemF_cbv]


V

V [definition, in Autosubst.sem]
var_vl [constructor, in Autosubst.SystemF_cbv]
var_ty [constructor, in Autosubst.SystemF_cbv]
VG [definition, in Autosubst.sem]
vl [inductive, in Autosubst.SystemF_cbv]
vl_ty_ind [definition, in Autosubst.sem]
vl_ty [inductive, in Autosubst.sem]
vt [constructor, in Autosubst.SystemF_cbv]
V_subst [lemma, in Autosubst.sem]
V_weak [lemma, in Autosubst.sem]
V_ren [lemma, in Autosubst.sem]


X

xi_extS [lemma, in Autosubst.axioms]
xi_extP [lemma, in Autosubst.axioms]
xi_ext [lemma, in Autosubst.axioms]


other

_ >> _ (subst_scope) [notation, in Autosubst.Autosubst2]
_ .[ _ ] (subst_scope) [notation, in Autosubst.Autosubst2]
( + _ ) (subst_scope) [notation, in Autosubst.Autosubst2]
_ .: _ (subst_scope) [notation, in Autosubst.Autosubst2]
_ >>> _ (subst_scope) [notation, in Autosubst.Autosubst2]
_ .[ _ , _ ] (subst_scope) [notation, in Autosubst.sem]
_ == _ [notation, in Autosubst.Autosubst2]
_ `_ _ [notation, in Autosubst.sem]
ren _ [notation, in Autosubst.sem]



Notation Index

other

_ >> _ (subst_scope) [in Autosubst.Autosubst2]
_ .[ _ ] (subst_scope) [in Autosubst.Autosubst2]
( + _ ) (subst_scope) [in Autosubst.Autosubst2]
_ .: _ (subst_scope) [in Autosubst.Autosubst2]
_ >>> _ (subst_scope) [in Autosubst.Autosubst2]
_ .[ _ , _ ] (subst_scope) [in Autosubst.sem]
_ == _ [in Autosubst.Autosubst2]
_ `_ _ [in Autosubst.sem]
ren _ [in Autosubst.sem]



Module Index

A

AsimplIndex [in Autosubst.Autosubst2]



Library Index

A

Autosubst2
axioms


S

sem
SystemF_cbv



Constructor Index

A

all [in Autosubst.SystemF_cbv]
app [in Autosubst.SystemF_cbv]
arr [in Autosubst.SystemF_cbv]
asimplCompEqn [in Autosubst.Autosubst2]
asimplCompEqn_vl [in Autosubst.SystemF_cbv]
asimplCompEqn_tm [in Autosubst.SystemF_cbv]
asimplCompEqn_ty [in Autosubst.SystemF_cbv]
asimplConsEqn [in Autosubst.Autosubst2]
asimplEqn [in Autosubst.Autosubst2]
asimplGenEqn [in Autosubst.Autosubst2]
asimplGenInstEqn [in Autosubst.Autosubst2]
asimplIndexEqn [in Autosubst.Autosubst2]
AsimplIndex.EO [in Autosubst.Autosubst2]
AsimplIndex.EPlus [in Autosubst.Autosubst2]
AsimplIndex.ES [in Autosubst.Autosubst2]
AsimplIndex.EVar [in Autosubst.Autosubst2]
asimplInstEqn_vl [in Autosubst.SystemF_cbv]
asimplInstEqn_tm [in Autosubst.SystemF_cbv]
asimplInstEqn_ty [in Autosubst.SystemF_cbv]
asimplRecEqn [in Autosubst.Autosubst2]
asimplRenCompEqn [in Autosubst.Autosubst2]
asimplRenConsEqn [in Autosubst.Autosubst2]
asimplRenEqn [in Autosubst.Autosubst2]
asimplRenInstEqn [in Autosubst.Autosubst2]
asimplRenShiftEqn [in Autosubst.Autosubst2]
asimplSubstCompRenEqn [in Autosubst.Autosubst2]
asimplSubstEqn_vl [in Autosubst.SystemF_cbv]
asimplSubstEqn_tm [in Autosubst.SystemF_cbv]
asimplSubstEqn_ty [in Autosubst.SystemF_cbv]
asimplVarInstEqn [in Autosubst.Autosubst2]


E

eval_val [in Autosubst.sem]
eval_tapp [in Autosubst.sem]
eval_app [in Autosubst.sem]


F

funext [in Autosubst.Autosubst2]


L

lam [in Autosubst.SystemF_cbv]


P

Pack [in Autosubst.Autosubst2]


T

tapp [in Autosubst.SystemF_cbv]
tlam [in Autosubst.SystemF_cbv]
ty_tlam [in Autosubst.sem]
ty_lam [in Autosubst.sem]
ty_var [in Autosubst.sem]
ty_val [in Autosubst.sem]
ty_tapp [in Autosubst.sem]
ty_app [in Autosubst.sem]


V

var_vl [in Autosubst.SystemF_cbv]
var_ty [in Autosubst.SystemF_cbv]
vt [in Autosubst.SystemF_cbv]



Lemma Index

A

AsimplIndex.eval_nfE [in Autosubst.Autosubst2]
AsimplIndex.flatten_cat [in Autosubst.Autosubst2]
AsimplIndex.normalize_sound [in Autosubst.Autosubst2]


C

consistency [in Autosubst.sem]


E

E_subst1 [in Autosubst.sem]


G

get_map [in Autosubst.sem]


N

normalization [in Autosubst.sem]


P

pext [in Autosubst.axioms]


R

ren_inst_ty [in Autosubst.SystemF_cbv]


S

soundness [in Autosubst.sem]
soundness_nil [in Autosubst.sem]


U

up_ren_up [in Autosubst.SystemF_cbv]


V

V_subst [in Autosubst.sem]
V_weak [in Autosubst.sem]
V_ren [in Autosubst.sem]


X

xi_extS [in Autosubst.axioms]
xi_extP [in Autosubst.axioms]
xi_ext [in Autosubst.axioms]



Axiom Index

F

functional_extensionality [in Autosubst.axioms]


P

propositional_extensionality [in Autosubst.axioms]



Projection Index

A

asimplCompEqn [in Autosubst.Autosubst2]
asimplCompEqn_vl [in Autosubst.SystemF_cbv]
asimplCompEqn_tm [in Autosubst.SystemF_cbv]
asimplCompEqn_ty [in Autosubst.SystemF_cbv]
asimplConsEqn [in Autosubst.Autosubst2]
asimplEqn [in Autosubst.Autosubst2]
asimplGenEqn [in Autosubst.Autosubst2]
asimplGenInstEqn [in Autosubst.Autosubst2]
asimplIndexEqn [in Autosubst.Autosubst2]
asimplInstEqn_vl [in Autosubst.SystemF_cbv]
asimplInstEqn_tm [in Autosubst.SystemF_cbv]
asimplInstEqn_ty [in Autosubst.SystemF_cbv]
asimplRecEqn [in Autosubst.Autosubst2]
asimplRenCompEqn [in Autosubst.Autosubst2]
asimplRenConsEqn [in Autosubst.Autosubst2]
asimplRenEqn [in Autosubst.Autosubst2]
asimplRenInstEqn [in Autosubst.Autosubst2]
asimplRenShiftEqn [in Autosubst.Autosubst2]
asimplSubstCompRenEqn [in Autosubst.Autosubst2]
asimplSubstEqn_vl [in Autosubst.SystemF_cbv]
asimplSubstEqn_tm [in Autosubst.SystemF_cbv]
asimplSubstEqn_ty [in Autosubst.SystemF_cbv]
asimplVarInstEqn [in Autosubst.Autosubst2]


F

funext [in Autosubst.Autosubst2]


I

inst_of_substType [in Autosubst.Autosubst2]


M

mixin_of_substType [in Autosubst.Autosubst2]


S

subst_ofType [in Autosubst.Autosubst2]
subst_of_substType [in Autosubst.Autosubst2]



Inductive Index

A

Asimpl [in Autosubst.Autosubst2]
AsimplComp [in Autosubst.Autosubst2]
AsimplComp_vl [in Autosubst.SystemF_cbv]
AsimplComp_tm [in Autosubst.SystemF_cbv]
AsimplComp_ty [in Autosubst.SystemF_cbv]
AsimplCons [in Autosubst.Autosubst2]
AsimplGen [in Autosubst.Autosubst2]
AsimplGenInst [in Autosubst.Autosubst2]
AsimplIndex [in Autosubst.Autosubst2]
AsimplIndex.exp [in Autosubst.Autosubst2]
AsimplInst_vl [in Autosubst.SystemF_cbv]
AsimplInst_tm [in Autosubst.SystemF_cbv]
AsimplInst_ty [in Autosubst.SystemF_cbv]
AsimplRec [in Autosubst.Autosubst2]
AsimplRen [in Autosubst.Autosubst2]
AsimplRenComp [in Autosubst.Autosubst2]
AsimplRenCons [in Autosubst.Autosubst2]
AsimplRenInst [in Autosubst.Autosubst2]
AsimplRenShift [in Autosubst.Autosubst2]
AsimplSubstCompRen [in Autosubst.Autosubst2]
AsimplSubst_vl [in Autosubst.SystemF_cbv]
AsimplSubst_tm [in Autosubst.SystemF_cbv]
AsimplSubst_ty [in Autosubst.SystemF_cbv]
AsimplVarInst [in Autosubst.Autosubst2]


E

eval [in Autosubst.sem]


F

Funext [in Autosubst.Autosubst2]


T

tm [in Autosubst.SystemF_cbv]
tm_ty [in Autosubst.sem]
ty [in Autosubst.SystemF_cbv]


V

vl [in Autosubst.SystemF_cbv]
vl_ty [in Autosubst.sem]



Instance Index

A

AsimplAsimplInst_vl [in Autosubst.SystemF_cbv]
AsimplAsimplInst_tm [in Autosubst.SystemF_cbv]
AsimplAsimplInst_ty [in Autosubst.SystemF_cbv]
AsimplCast_vl_ty [in Autosubst.SystemF_cbv]
AsimplCast_tm_vl [in Autosubst.SystemF_cbv]
AsimplCast_tm_ty [in Autosubst.SystemF_cbv]
AsimplCompAsso [in Autosubst.Autosubst2]
AsimplCompAsso_vl [in Autosubst.SystemF_cbv]
AsimplCompAsso_tm [in Autosubst.SystemF_cbv]
AsimplCompAsso_ty [in Autosubst.SystemF_cbv]
AsimplCompCongr_vl [in Autosubst.SystemF_cbv]
AsimplCompCongr_tm [in Autosubst.SystemF_cbv]
AsimplCompCongr_ty [in Autosubst.SystemF_cbv]
AsimplCompCongr'_vl [in Autosubst.SystemF_cbv]
AsimplCompCongr'_tm [in Autosubst.SystemF_cbv]
AsimplCompCongr'_ty [in Autosubst.SystemF_cbv]
AsimplCompConsL [in Autosubst.Autosubst2]
AsimplCompIdL [in Autosubst.Autosubst2]
AsimplCompIdL_vl [in Autosubst.SystemF_cbv]
AsimplCompIdL_ty [in Autosubst.SystemF_cbv]
AsimplCompIdR [in Autosubst.Autosubst2]
AsimplCompIdR_vl [in Autosubst.SystemF_cbv]
AsimplCompIdR_tm [in Autosubst.SystemF_cbv]
AsimplCompIdR_ty [in Autosubst.SystemF_cbv]
AsimplCompRefl [in Autosubst.Autosubst2]
AsimplCompRefl_vl [in Autosubst.SystemF_cbv]
AsimplCompRefl_tm [in Autosubst.SystemF_cbv]
AsimplCompRefl_ty [in Autosubst.SystemF_cbv]
AsimplCompS' [in Autosubst.Autosubst2]
AsimplConsEta [in Autosubst.Autosubst2]
AsimplConsRefl [in Autosubst.Autosubst2]
AsimplGenComp_vl [in Autosubst.SystemF_cbv]
AsimplGenComp_tm [in Autosubst.SystemF_cbv]
AsimplGenComp_ty [in Autosubst.SystemF_cbv]
AsimplGenCons [in Autosubst.Autosubst2]
AsimplGenInstConsS [in Autosubst.Autosubst2]
AsimplGenInstCons0 [in Autosubst.Autosubst2]
AsimplGenInstIdren [in Autosubst.Autosubst2]
AsimplGenInstRefl [in Autosubst.Autosubst2]
AsimplGenInstShift [in Autosubst.Autosubst2]
AsimplGenInstShiftComp [in Autosubst.Autosubst2]
AsimplGenRefl [in Autosubst.Autosubst2]
AsimplGenRen [in Autosubst.Autosubst2]
AsimplGen_Asimpl_Ext [in Autosubst.Autosubst2]
AsimplGen_Asimpl [in Autosubst.Autosubst2]
AsimplId_vl [in Autosubst.SystemF_cbv]
AsimplId_tm [in Autosubst.SystemF_cbv]
AsimplId_ty [in Autosubst.SystemF_cbv]
AsimplIndexRefl [in Autosubst.Autosubst2]
AsimplIndex.ReifyO [in Autosubst.Autosubst2]
AsimplIndex.ReifyPlus [in Autosubst.Autosubst2]
AsimplIndex.ReifyS [in Autosubst.Autosubst2]
AsimplIndex.ReifyVar [in Autosubst.Autosubst2]
AsimplInstInst_vl [in Autosubst.SystemF_cbv]
AsimplInstInst_tm [in Autosubst.SystemF_cbv]
AsimplInstInst_ty [in Autosubst.SystemF_cbv]
AsimplInstRefl_vl [in Autosubst.SystemF_cbv]
AsimplInstRefl_tm [in Autosubst.SystemF_cbv]
AsimplInstRefl_ty [in Autosubst.SystemF_cbv]
AsimplInstVar_vl [in Autosubst.SystemF_cbv]
AsimplInstVar_ty [in Autosubst.SystemF_cbv]
asimplInst_tlam [in Autosubst.SystemF_cbv]
asimplInst_lam [in Autosubst.SystemF_cbv]
asimplInst_vt [in Autosubst.SystemF_cbv]
asimplInst_tapp [in Autosubst.SystemF_cbv]
asimplInst_app [in Autosubst.SystemF_cbv]
asimplInst_all [in Autosubst.SystemF_cbv]
asimplInst_arr [in Autosubst.SystemF_cbv]
AsimplRefl_vl [in Autosubst.SystemF_cbv]
AsimplRefl_tm [in Autosubst.SystemF_cbv]
AsimplRefl_ty [in Autosubst.SystemF_cbv]
AsimplRenCompComp [in Autosubst.Autosubst2]
AsimplRenCompCons [in Autosubst.Autosubst2]
AsimplRenCompIdL [in Autosubst.Autosubst2]
AsimplRenCompIdR [in Autosubst.Autosubst2]
AsimplRenCompRefl [in Autosubst.Autosubst2]
AsimplRenCompShift [in Autosubst.Autosubst2]
AsimplRenCompShift0 [in Autosubst.Autosubst2]
AsimplRenConsDef [in Autosubst.Autosubst2]
AsimplRenConsEta [in Autosubst.Autosubst2]
AsimplRenInstConsS [in Autosubst.Autosubst2]
AsimplRenInstCons0 [in Autosubst.Autosubst2]
AsimplRenInstIdren [in Autosubst.Autosubst2]
AsimplRenInstRefl [in Autosubst.Autosubst2]
AsimplRenInstShift [in Autosubst.Autosubst2]
AsimplRenInstShiftComp [in Autosubst.Autosubst2]
AsimplRenRefl [in Autosubst.Autosubst2]
AsimplRenScons [in Autosubst.Autosubst2]
AsimplRenShiftDef [in Autosubst.Autosubst2]
AsimplRenShiftIdren [in Autosubst.Autosubst2]
AsimplRenSShift [in Autosubst.Autosubst2]
AsimplSubstCompRenAssoc [in Autosubst.Autosubst2]
AsimplSubstCompRenRefl [in Autosubst.Autosubst2]
AsimplSubstComp_vl [in Autosubst.SystemF_cbv]
AsimplSubstComp_tm [in Autosubst.SystemF_cbv]
AsimplSubstComp_ty [in Autosubst.SystemF_cbv]
AsimplSubstCongr_vl [in Autosubst.SystemF_cbv]
AsimplSubstCongr_tm [in Autosubst.SystemF_cbv]
AsimplSubstCongr_ty [in Autosubst.SystemF_cbv]
AsimplSubstRefl_vl [in Autosubst.SystemF_cbv]
AsimplSubstRefl_tm [in Autosubst.SystemF_cbv]
AsimplSubstRefl_ty [in Autosubst.SystemF_cbv]
AsimplSubstUp_vl_vl [in Autosubst.SystemF_cbv]
AsimplSubstUp_vl_ty [in Autosubst.SystemF_cbv]
AsimplSubstUp_tm_vl [in Autosubst.SystemF_cbv]
AsimplSubstUp_tm_ty [in Autosubst.SystemF_cbv]
AsimplSubstUp_ty_ty [in Autosubst.SystemF_cbv]
AsimplToVar_vl [in Autosubst.SystemF_cbv]
AsimplToVar_ty [in Autosubst.SystemF_cbv]
AsimplVarInstConsS [in Autosubst.Autosubst2]
AsimplVarInstCons0 [in Autosubst.Autosubst2]
AsimplVarInstRefl [in Autosubst.Autosubst2]
AsimplVarInstShiftComp [in Autosubst.Autosubst2]


Q

quote_lookup_further [in Autosubst.Autosubst2]
quote_lookup_end [in Autosubst.Autosubst2]
quote_lookup_here [in Autosubst.Autosubst2]



Section Index

Q

quote_lookup [in Autosubst.Autosubst2]



Abbreviation Index

E

E [in Autosubst.sem]



Record Index

A

Asimpl [in Autosubst.Autosubst2]
AsimplComp [in Autosubst.Autosubst2]
AsimplComp_vl [in Autosubst.SystemF_cbv]
AsimplComp_tm [in Autosubst.SystemF_cbv]
AsimplComp_ty [in Autosubst.SystemF_cbv]
AsimplCons [in Autosubst.Autosubst2]
AsimplGen [in Autosubst.Autosubst2]
AsimplGenInst [in Autosubst.Autosubst2]
AsimplIndex [in Autosubst.Autosubst2]
AsimplIndex.ReifyExp [in Autosubst.Autosubst2]
AsimplInst_vl [in Autosubst.SystemF_cbv]
AsimplInst_tm [in Autosubst.SystemF_cbv]
AsimplInst_ty [in Autosubst.SystemF_cbv]
AsimplRec [in Autosubst.Autosubst2]
AsimplRen [in Autosubst.Autosubst2]
AsimplRenComp [in Autosubst.Autosubst2]
AsimplRenCons [in Autosubst.Autosubst2]
AsimplRenInst [in Autosubst.Autosubst2]
AsimplRenShift [in Autosubst.Autosubst2]
AsimplSubstCompRen [in Autosubst.Autosubst2]
AsimplSubst_vl [in Autosubst.SystemF_cbv]
AsimplSubst_tm [in Autosubst.SystemF_cbv]
AsimplSubst_ty [in Autosubst.SystemF_cbv]
AsimplVarInst [in Autosubst.Autosubst2]


F

Funext [in Autosubst.Autosubst2]


Q

QuoteLookup [in Autosubst.Autosubst2]


S

substMixin [in Autosubst.Autosubst2]
substType [in Autosubst.Autosubst2]



Definition Index

A

ap [in Autosubst.Autosubst2]
apc [in Autosubst.Autosubst2]
AsimplIndex.eval_nf [in Autosubst.Autosubst2]
AsimplIndex.eval_exp [in Autosubst.Autosubst2]
AsimplIndex.flatten [in Autosubst.Autosubst2]
AsimplIndex.nf [in Autosubst.Autosubst2]
AsimplIndex.normalize [in Autosubst.Autosubst2]


C

castren_vl_tm [in Autosubst.SystemF_cbv]
castren_vl_ty [in Autosubst.SystemF_cbv]
castren_tm_vl [in Autosubst.SystemF_cbv]
castren_tm_ty [in Autosubst.SystemF_cbv]
cast_vl_tm [in Autosubst.SystemF_cbv]
cast_vl_ty [in Autosubst.SystemF_cbv]
cast_tm_vl [in Autosubst.SystemF_cbv]
cast_tm_ty [in Autosubst.SystemF_cbv]
comp [in Autosubst.Autosubst2]
compE_subst_subst_vl [in Autosubst.SystemF_cbv]
compE_subst_subst_tm [in Autosubst.SystemF_cbv]
compE_subst_ren_vl [in Autosubst.SystemF_cbv]
compE_subst_ren_tm [in Autosubst.SystemF_cbv]
compE_ren_subst_vl [in Autosubst.SystemF_cbv]
compE_ren_subst_tm [in Autosubst.SystemF_cbv]
compE_ren_ren_vl [in Autosubst.SystemF_cbv]
compE_ren_ren_tm [in Autosubst.SystemF_cbv]
compE_subst_subst_ty [in Autosubst.SystemF_cbv]
compE_subst_ren_ty [in Autosubst.SystemF_cbv]
compE_ren_subst_ty [in Autosubst.SystemF_cbv]
compE_ren_ren_ty [in Autosubst.SystemF_cbv]
compren_vl [in Autosubst.SystemF_cbv]
compren_tm [in Autosubst.SystemF_cbv]
compren_ty [in Autosubst.SystemF_cbv]
compTrans_subst_subst_vl [in Autosubst.SystemF_cbv]
compTrans_subst_subst_tm [in Autosubst.SystemF_cbv]
compTrans_subst_ren_vl [in Autosubst.SystemF_cbv]
compTrans_subst_ren_tm [in Autosubst.SystemF_cbv]
compTrans_ren_subst_vl [in Autosubst.SystemF_cbv]
compTrans_ren_subst_tm [in Autosubst.SystemF_cbv]
compTrans_ren_ren_vl [in Autosubst.SystemF_cbv]
compTrans_ren_ren_tm [in Autosubst.SystemF_cbv]
compTrans_subst_subst_ty [in Autosubst.SystemF_cbv]
compTrans_subst_ren_ty [in Autosubst.SystemF_cbv]
compTrans_ren_subst_ty [in Autosubst.SystemF_cbv]
compTrans_ren_ren_ty [in Autosubst.SystemF_cbv]
comp_vl [in Autosubst.SystemF_cbv]
comp_tm [in Autosubst.SystemF_cbv]
comp_ty [in Autosubst.SystemF_cbv]
congr_tlam [in Autosubst.SystemF_cbv]
congr_lam [in Autosubst.SystemF_cbv]
congr_vt [in Autosubst.SystemF_cbv]
congr_tapp [in Autosubst.SystemF_cbv]
congr_app [in Autosubst.SystemF_cbv]
congr_all [in Autosubst.SystemF_cbv]
congr_arr [in Autosubst.SystemF_cbv]
ctx [in Autosubst.sem]


E

eq_of_subst [in Autosubst.Autosubst2]
eq_up_vl_vl [in Autosubst.SystemF_cbv]
eq_up_vl_ty [in Autosubst.SystemF_cbv]
eq_up_tm_vl [in Autosubst.SystemF_cbv]
eq_up_tm_ty [in Autosubst.SystemF_cbv]
eq_cast_vl_tm [in Autosubst.SystemF_cbv]
eq_cast_vl_ty [in Autosubst.SystemF_cbv]
eq_cast_tm_vl [in Autosubst.SystemF_cbv]
eq_cast_tm_ty [in Autosubst.SystemF_cbv]
eq_toVar_vl [in Autosubst.SystemF_cbv]
eq_up_ty_ty [in Autosubst.SystemF_cbv]
eq_toVar_ty [in Autosubst.SystemF_cbv]


F

fext [in Autosubst.axioms]
funcomp [in Autosubst.Autosubst2]


G

get [in Autosubst.sem]


H

has_ty_ind [in Autosubst.sem]


I

idren [in Autosubst.Autosubst2]
id_vl [in Autosubst.SystemF_cbv]
id_tm [in Autosubst.SystemF_cbv]
id_ty [in Autosubst.SystemF_cbv]
index [in Autosubst.Autosubst2]
inst [in Autosubst.Autosubst2]


L

L [in Autosubst.sem]
lift [in Autosubst.Autosubst2]


N

nilA [in Autosubst.sem]


R

ren [in Autosubst.Autosubst2]
ren_of [in Autosubst.Autosubst2]
ren_inst_vl [in Autosubst.SystemF_cbv]
ren_inst_tm [in Autosubst.SystemF_cbv]
ren_vl [in Autosubst.SystemF_cbv]
ren_tm [in Autosubst.SystemF_cbv]
ren_ty [in Autosubst.SystemF_cbv]


S

scons [in Autosubst.Autosubst2]
substEq [in Autosubst.Autosubst2]
substMixin_vl [in Autosubst.SystemF_cbv]
substMixin_tm [in Autosubst.SystemF_cbv]
substMixin_ty [in Autosubst.SystemF_cbv]
substType_vl [in Autosubst.SystemF_cbv]
substType_tm [in Autosubst.SystemF_cbv]
substType_ty [in Autosubst.SystemF_cbv]
subst_of [in Autosubst.Autosubst2]
subst_eq_vl [in Autosubst.SystemF_cbv]
subst_eq_tm [in Autosubst.SystemF_cbv]
subst_vl [in Autosubst.SystemF_cbv]
subst_tm [in Autosubst.SystemF_cbv]
subst_of_vl [in Autosubst.SystemF_cbv]
subst_of_tm [in Autosubst.SystemF_cbv]
subst_eq_ty [in Autosubst.SystemF_cbv]
subst_ty [in Autosubst.SystemF_cbv]
subst_of_ty [in Autosubst.SystemF_cbv]


T

tm_ty_ind [in Autosubst.sem]
toSubst_vl [in Autosubst.SystemF_cbv]
toSubst_tm [in Autosubst.SystemF_cbv]
toSubst_ty [in Autosubst.SystemF_cbv]
toVarRen_vl [in Autosubst.SystemF_cbv]
toVarRen_tm [in Autosubst.SystemF_cbv]
toVarRen_ty [in Autosubst.SystemF_cbv]
toVar_vl [in Autosubst.SystemF_cbv]
toVar_tm [in Autosubst.SystemF_cbv]
toVar_ty [in Autosubst.SystemF_cbv]


U

upId_vl_vl [in Autosubst.SystemF_cbv]
upId_vl_ty [in Autosubst.SystemF_cbv]
upId_tm_vl [in Autosubst.SystemF_cbv]
upId_tm_ty [in Autosubst.SystemF_cbv]
upId_ty_ty [in Autosubst.SystemF_cbv]
upren_vl_vl [in Autosubst.SystemF_cbv]
upren_vl_ty [in Autosubst.SystemF_cbv]
upren_tm_vl [in Autosubst.SystemF_cbv]
upren_tm_ty [in Autosubst.SystemF_cbv]
upren_ty_ty [in Autosubst.SystemF_cbv]
up_ren_ren [in Autosubst.Autosubst2]
up_ren [in Autosubst.Autosubst2]
up_ren_up_vl_ty [in Autosubst.SystemF_cbv]
up_ren_up_vl_vl [in Autosubst.SystemF_cbv]
up_subst_subst_vl_vl [in Autosubst.SystemF_cbv]
up_subst_subst_vl_ty [in Autosubst.SystemF_cbv]
up_subst_subst_tm_vl [in Autosubst.SystemF_cbv]
up_subst_subst_tm_ty [in Autosubst.SystemF_cbv]
up_subst_ren_vl_vl [in Autosubst.SystemF_cbv]
up_subst_ren_vl_ty [in Autosubst.SystemF_cbv]
up_subst_ren_tm_vl [in Autosubst.SystemF_cbv]
up_subst_ren_tm_ty [in Autosubst.SystemF_cbv]
up_ren_subst_vl_vl [in Autosubst.SystemF_cbv]
up_ren_subst_vl_ty [in Autosubst.SystemF_cbv]
up_ren_subst_tm_vl [in Autosubst.SystemF_cbv]
up_ren_subst_tm_ty [in Autosubst.SystemF_cbv]
up_vl_vl [in Autosubst.SystemF_cbv]
up_vl_ty [in Autosubst.SystemF_cbv]
up_tm_vl [in Autosubst.SystemF_cbv]
up_tm_ty [in Autosubst.SystemF_cbv]
up_subst_subst_ty_ty [in Autosubst.SystemF_cbv]
up_subst_ren_ty_ty [in Autosubst.SystemF_cbv]
up_ren_subst_ty_ty [in Autosubst.SystemF_cbv]
up_ty_ty [in Autosubst.SystemF_cbv]


V

V [in Autosubst.sem]
VG [in Autosubst.sem]
vl_ty_ind [in Autosubst.sem]



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 (437 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 (9 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 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 (47 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 (18 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 _ other (2 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 (28 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 (31 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 (116 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 (1 entry)
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)
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 (28 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (151 entries)