| 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
Autosubst2axioms
S
semSystemF_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) |