| 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 | (2746 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 | (255 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 | (6 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 | (192 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 | (43 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 | (668 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 | (386 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 | (59 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 | (148 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 | (101 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 | (35 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (792 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 | (56 entries) |
Global Index
A
ab [constructor, in Chapter7.expressions]abs [constructor, in Chapter10.sysf]
abs [constructor, in Chapter10.sysf_pat]
ab_ [definition, in Chapter7.expressions]
algeq [inductive, in Chapter9.equivalence]
algeqNeu [inductive, in Chapter9.equivalence]
algeqNeu_ind_2 [definition, in Chapter9.equivalence]
algeq_trans [lemma, in Chapter9.equivalence]
algeq_sym [lemma, in Chapter9.equivalence]
algeq_backward_closure [lemma, in Chapter9.equivalence]
algEq_monotone [lemma, in Chapter9.equivalence]
algeq_mut_ind [definition, in Chapter9.equivalence]
algeq_ind_2 [definition, in Chapter9.equivalence]
alg_app [constructor, in Chapter9.equivalence]
alg_var [constructor, in Chapter9.equivalence]
alg_arr [constructor, in Chapter9.equivalence]
alg_base [constructor, in Chapter9.equivalence]
all [constructor, in Chapter6.sysf_cbv]
all [constructor, in Chapter6.fol]
all [constructor, in Chapter10.sysf]
all [constructor, in Chapter6.recty]
all [constructor, in Chapter10.sysf_pat]
anti_rename [lemma, in Chapter9.sn_raamsdonk]
ap [definition, in unscoped]
ap [definition, in fintype]
ap [definition, in fintype_variadic]
apc [definition, in unscoped]
apc [definition, in fintype]
apc [definition, in fintype_variadic]
app [constructor, in Chapter3.utlc_scoped]
app [constructor, in Chapter6.variadic_list]
app [constructor, in Chapter7.expressions]
app [constructor, in Chapter6.variadic_fin]
app [constructor, in Chapter6.sysf_cbv]
app [constructor, in Chapter9.stlc]
app [constructor, in Chapter6.utlc_pairs]
app [constructor, in Chapter3.utlc_pure]
app [constructor, in Chapter10.sysf]
App [constructor, in Chapter4.sigmacalculus]
app [constructor, in Chapter10.sysf_pat]
app_ [definition, in Chapter7.expressions]
arr [constructor, in Chapter7.expressions]
arr [constructor, in Chapter6.sysf_cbv]
arr [constructor, in Chapter9.equivalence]
arr [constructor, in Chapter10.sysf]
arr [constructor, in Chapter6.recty]
arr [constructor, in Chapter9.variadic_preservation]
arr [constructor, in Chapter10.sysf_pat]
arr_ [definition, in Chapter7.expressions]
ARS [library]
atom [constructor, in Chapter6.fol]
axioms [library]
B
Bang [constructor, in Chapter6.picalculus]Base [constructor, in Chapter9.stlc]
Base [constructor, in Chapter9.equivalence]
Base [constructor, in Chapter9.variadic_preservation]
BaseClosure [constructor, in Chapter4.termination]
beta [constructor, in Chapter9.equivalence]
beta_closure [lemma, in Chapter9.girard]
boolTy [constructor, in Chapter7.expressions]
boolTy_ [definition, in Chapter7.expressions]
buildImp [definition, in header_metacoq]
Bundle [record, in header_extensible]
C
cand [definition, in Chapter9.girard]can_form_rectm [lemma, in Chapter10.POPLMark22]
can_form_all [lemma, in Chapter10.POPLMark22]
can_form_arr [lemma, in Chapter10.POPLMark22]
can_form_rectm [lemma, in Chapter10.POPLMark21]
can_form_all [lemma, in Chapter10.POPLMark21]
can_form_arr [lemma, in Chapter10.POPLMark21]
can_form_all [lemma, in Chapter10.POPLMark1]
can_form_arr [lemma, in Chapter10.POPLMark1]
CCompL [constructor, in Chapter4.termination]
CCompR [constructor, in Chapter4.termination]
chan [inductive, in Chapter6.picalculus]
chan [section, in Chapter6.picalculus]
CLam [constructor, in Chapter4.termination]
closed_appR [lemma, in Chapter9.sn_raamsdonk]
closed_lam [lemma, in Chapter9.sn_raamsdonk]
close_ren [lemma, in Chapter9.sn]
close_ren [lemma, in Chapter9.sn_lam]
closure [inductive, in Chapter4.termination]
cns [definition, in header_metacoq]
cod [definition, in axioms]
cod_comp [definition, in axioms]
cod_ext [definition, in axioms]
cod_id [definition, in axioms]
cod_map [definition, in axioms]
comb_equiv_ind [definition, in Chapter4.sigmacalculus]
comb_exp_ind [definition, in Chapter4.sigmacalculus]
CommaNotation [module, in fintype]
CommaNotation [module, in fintype_variadic]
_ , _ (subst_scope) [notation, in fintype]
_ , _ (subst_scope) [notation, in fintype_variadic]
comp [definition, in fintype]
comp [definition, in fintype_variadic]
comp [constructor, in Chapter4.termination]
Comp [constructor, in Chapter4.sigmacalculus]
compComp_tm [lemma, in Chapter3.utlc_scoped]
compComp_tm [lemma, in Chapter6.variadic_list]
compComp_exp [lemma, in Chapter7.expressions]
compComp_exp_var [lemma, in Chapter7.expressions]
compComp_exp_bool [lemma, in Chapter7.expressions]
compComp_exp_arith [lemma, in Chapter7.expressions]
compComp_exp_lam [lemma, in Chapter7.expressions]
compComp_tm [lemma, in Chapter6.variadic_fin]
compComp_vl [lemma, in Chapter6.sysf_cbv]
compComp_tm [lemma, in Chapter6.sysf_cbv]
compComp_ty [lemma, in Chapter6.sysf_cbv]
compComp_tm [lemma, in Chapter9.stlc]
compComp_tm [lemma, in Chapter6.utlc_pairs]
compComp_form [lemma, in Chapter6.fol]
compComp_tm [lemma, in Chapter6.fol]
compComp_exp [lemma, in Chapter9.sn_lam]
compComp_tm [lemma, in Chapter3.utlc_pure]
compComp_tm [lemma, in Chapter10.sysf]
compComp_ty [lemma, in Chapter10.sysf]
compComp_ty [lemma, in Chapter6.recty]
compComp_tm [lemma, in Chapter10.sysf_pat]
compComp_pat [lemma, in Chapter10.sysf_pat]
compComp_ty [lemma, in Chapter10.sysf_pat]
compComp'_tm [lemma, in Chapter3.utlc_scoped]
compComp'_tm [lemma, in Chapter6.variadic_list]
compComp'_exp [lemma, in Chapter7.expressions]
compComp'_exp_var [lemma, in Chapter7.expressions]
compComp'_exp_bool [lemma, in Chapter7.expressions]
compComp'_exp_arith [lemma, in Chapter7.expressions]
compComp'_exp_lam [lemma, in Chapter7.expressions]
compComp'_tm [lemma, in Chapter6.variadic_fin]
compComp'_vl [lemma, in Chapter6.sysf_cbv]
compComp'_tm [lemma, in Chapter6.sysf_cbv]
compComp'_ty [lemma, in Chapter6.sysf_cbv]
compComp'_tm [lemma, in Chapter9.stlc]
compComp'_tm [lemma, in Chapter6.utlc_pairs]
compComp'_form [lemma, in Chapter6.fol]
compComp'_tm [lemma, in Chapter6.fol]
compComp'_exp [lemma, in Chapter9.sn_lam]
compComp'_tm [lemma, in Chapter3.utlc_pure]
compComp'_tm [lemma, in Chapter10.sysf]
compComp'_ty [lemma, in Chapter10.sysf]
compComp'_ty [lemma, in Chapter6.recty]
compComp'_tm [lemma, in Chapter10.sysf_pat]
compComp'_pat [lemma, in Chapter10.sysf_pat]
compComp'_ty [lemma, in Chapter10.sysf_pat]
completeness [lemma, in Chapter9.equivalence]
compose_fixpoint [definition, in header_metacoq]
compRel [inductive, in Chapter4.termination]
compRelPair [constructor, in Chapter4.termination]
compRelSingleton [constructor, in Chapter4.termination]
compRelTerm [constructor, in Chapter4.termination]
CompRen [constructor, in Chapter4.termination]
compRenRen_tm [definition, in Chapter3.utlc_scoped]
compRenRen_tm [definition, in Chapter6.variadic_list]
compRenRen_exp [definition, in Chapter7.expressions]
compRenRen_exp_var [definition, in Chapter7.expressions]
compRenRen_exp_bool [definition, in Chapter7.expressions]
compRenRen_exp_arith [definition, in Chapter7.expressions]
compRenRen_exp_lam [definition, in Chapter7.expressions]
compRenRen_tm [definition, in Chapter6.variadic_fin]
compRenRen_vl [definition, in Chapter6.sysf_cbv]
compRenRen_tm [definition, in Chapter6.sysf_cbv]
compRenRen_ty [definition, in Chapter6.sysf_cbv]
compRenRen_tm [definition, in Chapter9.stlc]
compRenRen_tm [definition, in Chapter6.utlc_pairs]
compRenRen_tm [definition, in Chapter3.utlc_pure]
compRenRen_tm [definition, in Chapter10.sysf]
compRenRen_ty [definition, in Chapter10.sysf]
compRenRen_proc [definition, in Chapter6.picalculus]
compRenRen_chan [definition, in Chapter6.picalculus]
compRenRen_ty [definition, in Chapter6.recty]
compRenRen_tm [definition, in Chapter10.sysf_pat]
compRenRen_pat [definition, in Chapter10.sysf_pat]
compRenRen_ty [definition, in Chapter10.sysf_pat]
compRenSubst_tm [definition, in Chapter3.utlc_scoped]
compRenSubst_tm [definition, in Chapter6.variadic_list]
compRenSubst_exp [definition, in Chapter7.expressions]
compRenSubst_exp_var [definition, in Chapter7.expressions]
compRenSubst_exp_bool [definition, in Chapter7.expressions]
compRenSubst_exp_arith [definition, in Chapter7.expressions]
compRenSubst_exp_lam [definition, in Chapter7.expressions]
compRenSubst_tm [definition, in Chapter6.variadic_fin]
compRenSubst_vl [definition, in Chapter6.sysf_cbv]
compRenSubst_tm [definition, in Chapter6.sysf_cbv]
compRenSubst_ty [definition, in Chapter6.sysf_cbv]
compRenSubst_tm [definition, in Chapter9.stlc]
compRenSubst_tm [definition, in Chapter6.utlc_pairs]
compRenSubst_tm [definition, in Chapter3.utlc_pure]
compRenSubst_tm [definition, in Chapter10.sysf]
compRenSubst_ty [definition, in Chapter10.sysf]
compRenSubst_ty [definition, in Chapter6.recty]
compRenSubst_tm [definition, in Chapter10.sysf_pat]
compRenSubst_pat [definition, in Chapter10.sysf_pat]
compRenSubst_ty [definition, in Chapter10.sysf_pat]
compRen_tm [lemma, in Chapter3.utlc_scoped]
compRen_tm [lemma, in Chapter6.variadic_list]
compRen_exp [lemma, in Chapter7.expressions]
compRen_exp_var [lemma, in Chapter7.expressions]
compRen_exp_bool [lemma, in Chapter7.expressions]
compRen_exp_arith [lemma, in Chapter7.expressions]
compRen_exp_lam [lemma, in Chapter7.expressions]
compRen_tm [lemma, in Chapter6.variadic_fin]
compRen_vl [lemma, in Chapter6.sysf_cbv]
compRen_tm [lemma, in Chapter6.sysf_cbv]
compRen_ty [lemma, in Chapter6.sysf_cbv]
compRen_tm [lemma, in Chapter9.stlc]
compRen_tm [lemma, in Chapter6.utlc_pairs]
compRen_exp [lemma, in Chapter9.sn_lam]
compRen_tm [lemma, in Chapter3.utlc_pure]
compRen_tm [lemma, in Chapter10.sysf]
compRen_ty [lemma, in Chapter10.sysf]
compRen_ty [lemma, in Chapter6.recty]
compRen_tm [lemma, in Chapter10.sysf_pat]
compRen_pat [lemma, in Chapter10.sysf_pat]
compRen_ty [lemma, in Chapter10.sysf_pat]
compRen'_tm [lemma, in Chapter3.utlc_scoped]
compRen'_tm [lemma, in Chapter6.variadic_list]
compRen'_exp [lemma, in Chapter7.expressions]
compRen'_exp_var [lemma, in Chapter7.expressions]
compRen'_exp_bool [lemma, in Chapter7.expressions]
compRen'_exp_arith [lemma, in Chapter7.expressions]
compRen'_exp_lam [lemma, in Chapter7.expressions]
compRen'_tm [lemma, in Chapter6.variadic_fin]
compRen'_vl [lemma, in Chapter6.sysf_cbv]
compRen'_tm [lemma, in Chapter6.sysf_cbv]
compRen'_ty [lemma, in Chapter6.sysf_cbv]
compRen'_tm [lemma, in Chapter9.stlc]
compRen'_tm [lemma, in Chapter6.utlc_pairs]
compRen'_exp [lemma, in Chapter9.sn_lam]
compRen'_tm [lemma, in Chapter3.utlc_pure]
compRen'_tm [lemma, in Chapter10.sysf]
compRen'_ty [lemma, in Chapter10.sysf]
compRen'_ty [lemma, in Chapter6.recty]
compRen'_tm [lemma, in Chapter10.sysf_pat]
compRen'_pat [lemma, in Chapter10.sysf_pat]
compRen'_ty [lemma, in Chapter10.sysf_pat]
compSubstRen_tm [definition, in Chapter3.utlc_scoped]
compSubstRen_tm [definition, in Chapter6.variadic_list]
compSubstRen_exp [definition, in Chapter7.expressions]
compSubstRen_exp_var [definition, in Chapter7.expressions]
compSubstRen_exp_bool [definition, in Chapter7.expressions]
compSubstRen_exp_arith [definition, in Chapter7.expressions]
compSubstRen_exp_lam [definition, in Chapter7.expressions]
compSubstRen_tm [definition, in Chapter6.variadic_fin]
compSubstRen_vl [definition, in Chapter6.sysf_cbv]
compSubstRen_tm [definition, in Chapter6.sysf_cbv]
compSubstRen_ty [definition, in Chapter6.sysf_cbv]
compSubstRen_tm [definition, in Chapter9.stlc]
compSubstRen_tm [definition, in Chapter6.utlc_pairs]
compSubstRen_tm [definition, in Chapter3.utlc_pure]
compSubstRen_tm [definition, in Chapter10.sysf]
compSubstRen_ty [definition, in Chapter10.sysf]
compSubstRen_ty [definition, in Chapter6.recty]
compSubstRen_tm [definition, in Chapter10.sysf_pat]
compSubstRen_pat [definition, in Chapter10.sysf_pat]
compSubstRen_ty [definition, in Chapter10.sysf_pat]
compSubstSubst_tm [definition, in Chapter3.utlc_scoped]
compSubstSubst_tm [definition, in Chapter6.variadic_list]
compSubstSubst_exp [definition, in Chapter7.expressions]
compSubstSubst_exp_var [definition, in Chapter7.expressions]
compSubstSubst_exp_bool [definition, in Chapter7.expressions]
compSubstSubst_exp_arith [definition, in Chapter7.expressions]
compSubstSubst_exp_lam [definition, in Chapter7.expressions]
compSubstSubst_tm [definition, in Chapter6.variadic_fin]
compSubstSubst_vl [definition, in Chapter6.sysf_cbv]
compSubstSubst_tm [definition, in Chapter6.sysf_cbv]
compSubstSubst_ty [definition, in Chapter6.sysf_cbv]
compSubstSubst_tm [definition, in Chapter9.stlc]
compSubstSubst_tm [definition, in Chapter6.utlc_pairs]
compSubstSubst_form [definition, in Chapter6.fol]
compSubstSubst_tm [definition, in Chapter6.fol]
compSubstSubst_tm [definition, in Chapter3.utlc_pure]
compSubstSubst_tm [definition, in Chapter10.sysf]
compSubstSubst_ty [definition, in Chapter10.sysf]
compSubstSubst_ty [definition, in Chapter6.recty]
compSubstSubst_tm [definition, in Chapter10.sysf_pat]
compSubstSubst_pat [definition, in Chapter10.sysf_pat]
compSubstSubst_ty [definition, in Chapter10.sysf_pat]
comp_I [constructor, in Chapter4.sigmacalculus]
comp_cons [constructor, in Chapter4.sigmacalculus]
comp_assoc [constructor, in Chapter4.sigmacalculus]
comp_right [constructor, in Chapter4.sigmacalculus]
comp_left [constructor, in Chapter4.sigmacalculus]
comp_S [constructor, in Chapter4.sigmacalculus]
confluence [lemma, in Chapter9.equivalence]
confluence [library]
confluent [definition, in ARS]
congr_lam [lemma, in Chapter3.utlc_scoped]
congr_app [lemma, in Chapter3.utlc_scoped]
congr_lam [lemma, in Chapter6.variadic_list]
congr_app [lemma, in Chapter6.variadic_list]
congr_In_exp_arith [lemma, in Chapter7.expressions]
congr_In_exp_bool [lemma, in Chapter7.expressions]
congr_In_exp_lam [lemma, in Chapter7.expressions]
congr_In_exp_var [lemma, in Chapter7.expressions]
congr_If_ [lemma, in Chapter7.expressions]
congr_constBool_ [lemma, in Chapter7.expressions]
congr_constNat_ [lemma, in Chapter7.expressions]
congr_plus_ [lemma, in Chapter7.expressions]
congr_app_ [lemma, in Chapter7.expressions]
congr_ab_ [lemma, in Chapter7.expressions]
congr_In_ty_arith [lemma, in Chapter7.expressions]
congr_In_ty_bool [lemma, in Chapter7.expressions]
congr_In_ty_lam [lemma, in Chapter7.expressions]
congr_natTy_ [lemma, in Chapter7.expressions]
congr_boolTy_ [lemma, in Chapter7.expressions]
congr_arr_ [lemma, in Chapter7.expressions]
congr_lam [lemma, in Chapter6.variadic_fin]
congr_app [lemma, in Chapter6.variadic_fin]
congr_tlam [lemma, in Chapter6.sysf_cbv]
congr_lam [lemma, in Chapter6.sysf_cbv]
congr_vt [lemma, in Chapter6.sysf_cbv]
congr_tapp [lemma, in Chapter6.sysf_cbv]
congr_app [lemma, in Chapter6.sysf_cbv]
congr_all [lemma, in Chapter6.sysf_cbv]
congr_arr [lemma, in Chapter6.sysf_cbv]
congr_lam [lemma, in Chapter9.stlc]
congr_app [lemma, in Chapter9.stlc]
congr_Fun [lemma, in Chapter9.stlc]
congr_Base [lemma, in Chapter9.stlc]
congr_matchpair [lemma, in Chapter6.utlc_pairs]
congr_pair [lemma, in Chapter6.utlc_pairs]
congr_lam [lemma, in Chapter6.utlc_pairs]
congr_app [lemma, in Chapter6.utlc_pairs]
congr_all [lemma, in Chapter6.fol]
congr_pred [lemma, in Chapter6.fol]
congr_fal [lemma, in Chapter6.fol]
congr_plus [lemma, in Chapter6.fol]
congr_atom [lemma, in Chapter6.fol]
congr_lam [lemma, in Chapter3.utlc_pure]
congr_app [lemma, in Chapter3.utlc_pure]
congr_tabs [definition, in Chapter10.sysf]
congr_abs [definition, in Chapter10.sysf]
congr_vt [definition, in Chapter10.sysf]
congr_tapp [definition, in Chapter10.sysf]
congr_app [definition, in Chapter10.sysf]
congr_all [definition, in Chapter10.sysf]
congr_arr [definition, in Chapter10.sysf]
congr_top [definition, in Chapter10.sysf]
congr_Out [lemma, in Chapter6.picalculus]
congr_In [lemma, in Chapter6.picalculus]
congr_Par [lemma, in Chapter6.picalculus]
congr_Res [lemma, in Chapter6.picalculus]
congr_Bang [lemma, in Chapter6.picalculus]
congr_Nil [lemma, in Chapter6.picalculus]
congr_pairR [lemma, in Chapter4.termination]
congr_pairL [lemma, in Chapter4.termination]
congr_compR [lemma, in Chapter4.termination]
congr_compL [lemma, in Chapter4.termination]
congr_lam [lemma, in Chapter4.termination]
congr_recty [lemma, in Chapter6.recty]
congr_all [lemma, in Chapter6.recty]
congr_arr [lemma, in Chapter6.recty]
congr_top [lemma, in Chapter6.recty]
congr_inj [lemma, in header_extensible]
congr_letpat [lemma, in Chapter10.sysf_pat]
congr_proj [lemma, in Chapter10.sysf_pat]
congr_rectm [lemma, in Chapter10.sysf_pat]
congr_tabs [lemma, in Chapter10.sysf_pat]
congr_abs [lemma, in Chapter10.sysf_pat]
congr_tapp [lemma, in Chapter10.sysf_pat]
congr_app [lemma, in Chapter10.sysf_pat]
congr_patlist [lemma, in Chapter10.sysf_pat]
congr_patvar [lemma, in Chapter10.sysf_pat]
congr_recty [lemma, in Chapter10.sysf_pat]
congr_all [lemma, in Chapter10.sysf_pat]
congr_arr [lemma, in Chapter10.sysf_pat]
congr_top [lemma, in Chapter10.sysf_pat]
Cons [constructor, in Chapter4.sigmacalculus]
constBool [constructor, in Chapter7.expressions]
constBool_ [definition, in Chapter7.expressions]
constNat [constructor, in Chapter7.expressions]
constNat_ [definition, in Chapter7.expressions]
cons_eta [constructor, in Chapter4.sigmacalculus]
context_morphism_lemma [lemma, in Chapter10.POPLMark22]
context_renaming_lemma' [lemma, in Chapter10.POPLMark22]
context_renaming_lemma [lemma, in Chapter10.POPLMark22]
context_morphism_lemma [lemma, in Chapter10.POPLMark21]
context_renaming_lemma' [lemma, in Chapter10.POPLMark21]
context_renaming_lemma [lemma, in Chapter10.POPLMark21]
context_morphism_lemma [lemma, in Chapter10.POPLMark1]
context_renaming_lemma [lemma, in Chapter10.POPLMark1]
cont_ext_id [lemma, in Chapter9.equivalence]
cont_ext_cons [lemma, in Chapter9.equivalence]
cont_ext_shift [lemma, in Chapter9.equivalence]
cont_ext [definition, in Chapter9.equivalence]
CPair [constructor, in Chapter4.termination]
cr [lemma, in Chapter9.sn_raamsdonk]
ctx [definition, in Chapter10.POPLMark22]
ctx [definition, in Chapter9.equivalence]
ctx [definition, in Chapter9.preservation]
ctx [inductive, in Chapter4.termination]
ctx [definition, in Chapter9.variadic_preservation]
ctx [definition, in Chapter10.POPLMark21]
ctx [definition, in Chapter10.POPLMark1]
CZero [constructor, in Chapter4.termination]
D
dctx [definition, in Chapter10.POPLMark22]dctx [definition, in Chapter10.POPLMark21]
dctx [definition, in Chapter10.POPLMark1]
DecApp [constructor, in Chapter9.equivalence]
DecBeta [constructor, in Chapter9.equivalence]
DecExt [constructor, in Chapter9.equivalence]
DecLam [constructor, in Chapter9.equivalence]
decleq [inductive, in Chapter9.equivalence]
DecSym [constructor, in Chapter9.equivalence]
DecTrans [constructor, in Chapter9.equivalence]
DecVar [constructor, in Chapter9.equivalence]
Definitions [section, in ARS]
Definitions.e [variable, in ARS]
Definitions.T [variable, in ARS]
defs [library]
den [definition, in Chapter4.soundness]
den_subst [definition, in Chapter4.soundness]
destArity [definition, in header_metacoq]
destruct_fin [lemma, in fintype]
destruct_fin [lemma, in fintype_variadic]
E
E [definition, in Chapter9.sn_mod]empty [definition, in Chapter10.POPLMark22]
empty [definition, in Chapter10.POPLMark21]
empty [definition, in Chapter10.POPLMark1]
equivalence [library]
equiv_confluent [lemma, in Chapter4.confluence]
equiv_locally_confluent [lemma, in Chapter4.confluence]
equiv_den_subst [definition, in Chapter4.soundness]
equiv_den [definition, in Chapter4.soundness]
equiv_uquiv [lemma, in Chapter4.termination]
equiv_s_ind' [definition, in Chapter4.sigmacalculus]
equiv_ind' [definition, in Chapter4.sigmacalculus]
equiv_consR [constructor, in Chapter4.sigmacalculus]
equiv_consL [constructor, in Chapter4.sigmacalculus]
equiv_compR [constructor, in Chapter4.sigmacalculus]
equiv_compL [constructor, in Chapter4.sigmacalculus]
equiv_axiom_subst [inductive, in Chapter4.sigmacalculus]
equiv_instR [constructor, in Chapter4.sigmacalculus]
equiv_instL [constructor, in Chapter4.sigmacalculus]
equiv_lam [constructor, in Chapter4.sigmacalculus]
equiv_appR [constructor, in Chapter4.sigmacalculus]
equiv_appL [constructor, in Chapter4.sigmacalculus]
equiv_inst_inst [constructor, in Chapter4.sigmacalculus]
equiv_inst_I [constructor, in Chapter4.sigmacalculus]
equiv_Zero [constructor, in Chapter4.sigmacalculus]
equiv_Lam [constructor, in Chapter4.sigmacalculus]
equiv_App [constructor, in Chapter4.sigmacalculus]
equiv_axiom [inductive, in Chapter4.sigmacalculus]
eval [inductive, in Chapter10.POPLMark22]
eval [inductive, in Chapter10.POPLMark21]
eval [inductive, in Chapter10.POPLMark1]
ev_progress [lemma, in Chapter10.POPLMark22]
ev_progress [lemma, in Chapter10.POPLMark21]
ev_progress [lemma, in Chapter10.POPLMark1]
exchangeability [lemma, in Chapter4.termination]
exp [inductive, in Chapter7.expressions]
exp [section, in Chapter7.expressions]
exp [inductive, in Chapter4.sigmacalculus]
expressions [library]
exp_var.retract_subst_exp [variable, in Chapter7.expressions]
exp_var.retract_ren_exp [variable, in Chapter7.expressions]
exp_var.retract_exp_var [variable, in Chapter7.expressions]
exp_var [inductive, in Chapter7.expressions]
exp_var.subst_exp [variable, in Chapter7.expressions]
exp_var.ren_exp [variable, in Chapter7.expressions]
exp_var.exp [variable, in Chapter7.expressions]
exp_var [section, in Chapter7.expressions]
exp_bool.retract_subst_exp [variable, in Chapter7.expressions]
exp_bool.retract_ren_exp [variable, in Chapter7.expressions]
exp_bool.retract_exp_bool [variable, in Chapter7.expressions]
exp_bool [inductive, in Chapter7.expressions]
exp_bool.rinst_inst_exp [variable, in Chapter7.expressions]
exp_bool.rinstInst_up_exp_exp [variable, in Chapter7.expressions]
exp_bool.compSubstSubst_exp [variable, in Chapter7.expressions]
exp_bool.up_subst_subst_exp_exp [variable, in Chapter7.expressions]
exp_bool.compSubstRen_exp [variable, in Chapter7.expressions]
exp_bool.up_subst_ren_exp_exp [variable, in Chapter7.expressions]
exp_bool.compRenSubst_exp [variable, in Chapter7.expressions]
exp_bool.up_ren_subst_exp_exp [variable, in Chapter7.expressions]
exp_bool.compRenRen_exp [variable, in Chapter7.expressions]
exp_bool.up_ren_ren_exp_exp [variable, in Chapter7.expressions]
exp_bool.ext_exp [variable, in Chapter7.expressions]
exp_bool.upExt_exp_exp [variable, in Chapter7.expressions]
exp_bool.extRen_exp [variable, in Chapter7.expressions]
exp_bool.upExtRen_exp_exp [variable, in Chapter7.expressions]
exp_bool.idSubst_exp [variable, in Chapter7.expressions]
exp_bool.upId_exp_exp [variable, in Chapter7.expressions]
exp_bool.subst_exp [variable, in Chapter7.expressions]
exp_bool.up_exp_exp [variable, in Chapter7.expressions]
exp_bool.ren_exp [variable, in Chapter7.expressions]
exp_bool.upRen_exp_exp [variable, in Chapter7.expressions]
exp_bool.var_exp [variable, in Chapter7.expressions]
exp_bool.exp [variable, in Chapter7.expressions]
exp_bool [section, in Chapter7.expressions]
exp_arith.retract_subst_exp [variable, in Chapter7.expressions]
exp_arith.retract_ren_exp [variable, in Chapter7.expressions]
exp_arith.retract_exp_arith [variable, in Chapter7.expressions]
exp_arith [inductive, in Chapter7.expressions]
exp_arith.rinst_inst_exp [variable, in Chapter7.expressions]
exp_arith.rinstInst_up_exp_exp [variable, in Chapter7.expressions]
exp_arith.compSubstSubst_exp [variable, in Chapter7.expressions]
exp_arith.up_subst_subst_exp_exp [variable, in Chapter7.expressions]
exp_arith.compSubstRen_exp [variable, in Chapter7.expressions]
exp_arith.up_subst_ren_exp_exp [variable, in Chapter7.expressions]
exp_arith.compRenSubst_exp [variable, in Chapter7.expressions]
exp_arith.up_ren_subst_exp_exp [variable, in Chapter7.expressions]
exp_arith.compRenRen_exp [variable, in Chapter7.expressions]
exp_arith.up_ren_ren_exp_exp [variable, in Chapter7.expressions]
exp_arith.ext_exp [variable, in Chapter7.expressions]
exp_arith.upExt_exp_exp [variable, in Chapter7.expressions]
exp_arith.extRen_exp [variable, in Chapter7.expressions]
exp_arith.upExtRen_exp_exp [variable, in Chapter7.expressions]
exp_arith.idSubst_exp [variable, in Chapter7.expressions]
exp_arith.upId_exp_exp [variable, in Chapter7.expressions]
exp_arith.subst_exp [variable, in Chapter7.expressions]
exp_arith.up_exp_exp [variable, in Chapter7.expressions]
exp_arith.ren_exp [variable, in Chapter7.expressions]
exp_arith.upRen_exp_exp [variable, in Chapter7.expressions]
exp_arith.var_exp [variable, in Chapter7.expressions]
exp_arith.exp [variable, in Chapter7.expressions]
exp_arith [section, in Chapter7.expressions]
exp_lam.retract_subst_exp [variable, in Chapter7.expressions]
exp_lam.retract_ren_exp [variable, in Chapter7.expressions]
exp_lam.retract_exp_lam [variable, in Chapter7.expressions]
exp_lam [inductive, in Chapter7.expressions]
exp_lam.rinst_inst_exp [variable, in Chapter7.expressions]
exp_lam.rinstInst_up_exp_exp [variable, in Chapter7.expressions]
exp_lam.compSubstSubst_exp [variable, in Chapter7.expressions]
exp_lam.up_subst_subst_exp_exp [variable, in Chapter7.expressions]
exp_lam.compSubstRen_exp [variable, in Chapter7.expressions]
exp_lam.up_subst_ren_exp_exp [variable, in Chapter7.expressions]
exp_lam.compRenSubst_exp [variable, in Chapter7.expressions]
exp_lam.up_ren_subst_exp_exp [variable, in Chapter7.expressions]
exp_lam.compRenRen_exp [variable, in Chapter7.expressions]
exp_lam.up_ren_ren_exp_exp [variable, in Chapter7.expressions]
exp_lam.ext_exp [variable, in Chapter7.expressions]
exp_lam.upExt_exp_exp [variable, in Chapter7.expressions]
exp_lam.extRen_exp [variable, in Chapter7.expressions]
exp_lam.upExtRen_exp_exp [variable, in Chapter7.expressions]
exp_lam.idSubst_exp [variable, in Chapter7.expressions]
exp_lam.upId_exp_exp [variable, in Chapter7.expressions]
exp_lam.subst_exp [variable, in Chapter7.expressions]
exp_lam.up_exp_exp [variable, in Chapter7.expressions]
exp_lam.ren_exp [variable, in Chapter7.expressions]
exp_lam.upRen_exp_exp [variable, in Chapter7.expressions]
exp_lam.var_exp [variable, in Chapter7.expressions]
exp_lam.exp [variable, in Chapter7.expressions]
exp_lam [section, in Chapter7.expressions]
exp_features [instance, in Chapter9.sn_mod]
exp_uexp [definition, in Chapter4.termination]
exp_s_ind' [definition, in Chapter4.sigmacalculus]
exp_ind' [definition, in Chapter4.sigmacalculus]
extRen_tm [definition, in Chapter3.utlc_scoped]
extRen_tm [definition, in Chapter6.variadic_list]
extRen_exp [definition, in Chapter7.expressions]
extRen_exp_var [definition, in Chapter7.expressions]
extRen_exp_bool [definition, in Chapter7.expressions]
extRen_exp_arith [definition, in Chapter7.expressions]
extRen_exp_lam [definition, in Chapter7.expressions]
extRen_tm [definition, in Chapter6.variadic_fin]
extRen_vl [definition, in Chapter6.sysf_cbv]
extRen_tm [definition, in Chapter6.sysf_cbv]
extRen_ty [definition, in Chapter6.sysf_cbv]
extRen_tm [definition, in Chapter9.stlc]
extRen_tm [definition, in Chapter6.utlc_pairs]
extRen_tm [definition, in Chapter3.utlc_pure]
extRen_tm [definition, in Chapter10.sysf]
extRen_ty [definition, in Chapter10.sysf]
extRen_proc [definition, in Chapter6.picalculus]
extRen_chan [definition, in Chapter6.picalculus]
extRen_ty [definition, in Chapter6.recty]
extRen_tm [definition, in Chapter10.sysf_pat]
extRen_pat [definition, in Chapter10.sysf_pat]
extRen_ty [definition, in Chapter10.sysf_pat]
ext_tm [definition, in Chapter3.utlc_scoped]
ext_tm [definition, in Chapter6.variadic_list]
ext_exp [definition, in Chapter7.expressions]
ext_exp_var [definition, in Chapter7.expressions]
ext_exp_bool [definition, in Chapter7.expressions]
ext_exp_arith [definition, in Chapter7.expressions]
ext_exp_lam [definition, in Chapter7.expressions]
ext_SN [lemma, in Chapter9.sn_raamsdonk]
ext_tm [definition, in Chapter6.variadic_fin]
ext_vl [definition, in Chapter6.sysf_cbv]
ext_tm [definition, in Chapter6.sysf_cbv]
ext_ty [definition, in Chapter6.sysf_cbv]
ext_tm [definition, in Chapter9.stlc]
ext_tm [definition, in Chapter6.utlc_pairs]
ext_form [definition, in Chapter6.fol]
ext_tm [definition, in Chapter6.fol]
ext_tm [definition, in Chapter3.utlc_pure]
ext_tm [definition, in Chapter10.sysf]
ext_ty [definition, in Chapter10.sysf]
ext_ty [definition, in Chapter6.recty]
ext_tm [definition, in Chapter10.sysf_pat]
ext_pat [definition, in Chapter10.sysf_pat]
ext_ty [definition, in Chapter10.sysf_pat]
E_LetL [constructor, in Chapter10.POPLMark22]
E_Rec [constructor, in Chapter10.POPLMark22]
E_Proj [constructor, in Chapter10.POPLMark22]
E_TyFun [constructor, in Chapter10.POPLMark22]
E_appArg [constructor, in Chapter10.POPLMark22]
E_appFun [constructor, in Chapter10.POPLMark22]
E_RecProj [constructor, in Chapter10.POPLMark22]
E_Tapptabs [constructor, in Chapter10.POPLMark22]
E_appabs [constructor, in Chapter10.POPLMark22]
E_strong_base [lemma, in Chapter9.sn_var]
E_strong_step [lemma, in Chapter9.sn_var]
E_strong_sn [lemma, in Chapter9.sn_var]
E_strong [definition, in Chapter9.sn_var]
E_strong_In [constructor, in Chapter9.sn_var]
E_strong' [inductive, in Chapter9.sn_var]
E_ [definition, in Chapter9.sn_var]
E_strong_var [lemma, in Chapter9.sn]
E_strong_base [lemma, in Chapter9.sn]
E_strong_step [lemma, in Chapter9.sn]
E_strong_sn [lemma, in Chapter9.sn]
E_strong [definition, in Chapter9.sn]
E_strong_In [constructor, in Chapter9.sn]
E_strong' [inductive, in Chapter9.sn]
E_strong_var [lemma, in Chapter9.sn_mod]
E_LetL [constructor, in Chapter10.POPLMark21]
E_Rec [constructor, in Chapter10.POPLMark21]
E_Proj [constructor, in Chapter10.POPLMark21]
E_TyFun [constructor, in Chapter10.POPLMark21]
E_appArg [constructor, in Chapter10.POPLMark21]
E_appFun [constructor, in Chapter10.POPLMark21]
E_RecProj [constructor, in Chapter10.POPLMark21]
E_Tapptabs [constructor, in Chapter10.POPLMark21]
E_appabs [constructor, in Chapter10.POPLMark21]
E_ [definition, in Chapter9.wn]
E_TyFun [constructor, in Chapter10.POPLMark1]
E_appArg [constructor, in Chapter10.POPLMark1]
E_appFun [constructor, in Chapter10.POPLMark1]
E_Tapptabs [constructor, in Chapter10.POPLMark1]
E_appabs [constructor, in Chapter10.POPLMark1]
F
fal [constructor, in Chapter6.fol]features [projection, in header_metacoq]
features [constructor, in header_metacoq]
fill [definition, in Chapter4.termination]
fin [abbreviation, in unscoped]
fin [definition, in fintype]
fin [definition, in fintype_variadic]
fintype [library]
fintype_variadic [library]
fin_eta [lemma, in fintype]
fin_eta [lemma, in fintype_variadic]
fixNames [definition, in header_metacoq]
fol [library]
Forall [definition, in header_metacoq]
ForallN [definition, in header_metacoq]
Forall' [definition, in header_metacoq]
form [inductive, in Chapter6.fol]
form [section, in Chapter6.fol]
Fun [constructor, in Chapter9.stlc]
funcomp [definition, in unscoped]
funcomp [definition, in axioms]
fundamental [lemma, in Chapter9.equivalence]
fundamental_backwards [lemma, in Chapter9.sn_raamsdonk]
fundamental_theorem [lemma, in Chapter9.girard]
G
G [definition, in Chapter9.sn_var]G [definition, in Chapter9.wn]
GenCons [constructor, in header_metacoq]
genCons [constructor, in header_metacoq]
genIH [definition, in header_metacoq]
GenList [inductive, in header_metacoq]
genList [inductive, in header_metacoq]
GenNil [constructor, in header_metacoq]
genNil [constructor, in header_metacoq]
genStatement [definition, in header_metacoq]
genStatement_Fix [definition, in header_metacoq]
genStatement_no_lt [definition, in header_metacoq]
get [definition, in Chapter9.equivalence]
getName [definition, in header_metacoq]
get_In [definition, in header_extensible]
get_lemmas_and_name [definition, in header_metacoq]
get_lemmas [definition, in header_metacoq]
get_name [definition, in header_metacoq]
get_name_of [definition, in header_metacoq]
get_features [definition, in header_metacoq]
girard [library]
G_strong [definition, in Chapter9.sn_var]
G_strong [definition, in Chapter9.sn]
H
hasty_lam [constructor, in Chapter9.sn_lam]hasty_app [constructor, in Chapter9.sn_lam]
hasty_If [constructor, in Chapter9.sn_bool]
hasty_ConstBool [constructor, in Chapter9.sn_bool]
hasty_plus [constructor, in Chapter9.sn_arith]
hasty_ConstNat [constructor, in Chapter9.sn_arith]
has_ty [inductive, in Chapter10.POPLMark22]
has_ty_sem_strong [definition, in Chapter9.sn_var]
has_ty_sem [definition, in Chapter9.sn_var]
has_ty_subst_var [lemma, in Chapter9.sn_var]
has_ty_ren_var [lemma, in Chapter9.sn_var]
has_ty_var [inductive, in Chapter9.sn_var]
has_ty_sem_strong [definition, in Chapter9.sn]
has_type [inductive, in Chapter9.preservation]
has_ty_lam [inductive, in Chapter9.sn_lam]
has_ty_rev_arith [lemma, in Chapter9.sn_mod]
has_ty_rev_bool [lemma, in Chapter9.sn_mod]
has_ty_rev_lam [lemma, in Chapter9.sn_mod]
has_ty_rev_var [lemma, in Chapter9.sn_mod]
has_ty_features [instance, in Chapter9.sn_mod]
has_ty [inductive, in Chapter9.sn_mod]
has_ty_bool [inductive, in Chapter9.sn_bool]
has_ty_arith [inductive, in Chapter9.sn_arith]
has_type [inductive, in Chapter9.variadic_preservation]
has_ty [inductive, in Chapter10.POPLMark21]
has_features [record, in header_metacoq]
has_features [inductive, in header_metacoq]
has_ty_sem [definition, in Chapter9.wn]
has_ty [inductive, in Chapter10.POPLMark1]
header_extensible [library]
header_metacoq [library]
Hole [constructor, in Chapter4.termination]
I
I [constructor, in Chapter4.sigmacalculus]id [definition, in unscoped]
id [definition, in fintype]
id [definition, in fintype_variadic]
idren [definition, in fintype]
idren [definition, in fintype_variadic]
ids [projection, in unscoped]
ids [constructor, in unscoped]
ids [projection, in fintype]
ids [constructor, in fintype]
ids [projection, in fintype_variadic]
ids [constructor, in fintype_variadic]
idsRen [instance, in unscoped]
idSubst_tm [definition, in Chapter3.utlc_scoped]
idSubst_tm [definition, in Chapter6.variadic_list]
idSubst_exp [definition, in Chapter7.expressions]
idSubst_exp_var [definition, in Chapter7.expressions]
idSubst_exp_bool [definition, in Chapter7.expressions]
idSubst_exp_arith [definition, in Chapter7.expressions]
idSubst_exp_lam [definition, in Chapter7.expressions]
idSubst_tm [definition, in Chapter6.variadic_fin]
idSubst_vl [definition, in Chapter6.sysf_cbv]
idSubst_tm [definition, in Chapter6.sysf_cbv]
idSubst_ty [definition, in Chapter6.sysf_cbv]
idSubst_tm [definition, in Chapter9.stlc]
idSubst_tm [definition, in Chapter6.utlc_pairs]
idSubst_form [definition, in Chapter6.fol]
idSubst_tm [definition, in Chapter6.fol]
idSubst_tm [definition, in Chapter3.utlc_pure]
idSubst_tm [definition, in Chapter10.sysf]
idSubst_ty [definition, in Chapter10.sysf]
idSubst_ty [definition, in Chapter6.recty]
idSubst_tm [definition, in Chapter10.sysf_pat]
idSubst_pat [definition, in Chapter10.sysf_pat]
idSubst_ty [definition, in Chapter10.sysf_pat]
id_red [lemma, in Chapter9.sn_raamsdonk]
If [constructor, in Chapter7.expressions]
If_ [definition, in Chapter7.expressions]
imp [projection, in tactics]
Imp [record, in tactics]
imp [constructor, in tactics]
Imp [inductive, in tactics]
imprev [projection, in tactics]
ImpRev [record, in tactics]
imprev [constructor, in tactics]
ImpRev [inductive, in tactics]
In [constructor, in Chapter6.picalculus]
included [abbreviation, in header_extensible]
inj [abbreviation, in header_extensible]
Inl [constructor, in ARS]
inl_step_arith [constructor, in Chapter9.sn_mod]
inl_step_bool [constructor, in Chapter9.sn_mod]
inl_step_lam [constructor, in Chapter9.sn_mod]
inl_step_var [constructor, in Chapter9.sn_mod]
inl_has_ty_arith [constructor, in Chapter9.sn_mod]
inl_has_ty_bool [constructor, in Chapter9.sn_mod]
inl_has_ty_lam [constructor, in Chapter9.sn_mod]
inl_has_ty_var [constructor, in Chapter9.sn_mod]
Inr [constructor, in ARS]
InRelC [record, in header_metacoq]
Inst [constructor, in Chapter4.sigmacalculus]
instId_tm [lemma, in Chapter3.utlc_scoped]
instId_tm [lemma, in Chapter6.variadic_list]
instId_exp [lemma, in Chapter7.expressions]
instId_exp_var [lemma, in Chapter7.expressions]
instId_exp_bool [lemma, in Chapter7.expressions]
instId_exp_arith [lemma, in Chapter7.expressions]
instId_exp_lam [lemma, in Chapter7.expressions]
instId_tm [lemma, in Chapter6.variadic_fin]
instId_vl [lemma, in Chapter6.sysf_cbv]
instId_tm [lemma, in Chapter6.sysf_cbv]
instId_ty [lemma, in Chapter6.sysf_cbv]
instId_tm [lemma, in Chapter9.stlc]
instId_tm [lemma, in Chapter6.utlc_pairs]
instId_form [lemma, in Chapter6.fol]
instId_tm [lemma, in Chapter6.fol]
instId_exp [lemma, in Chapter9.sn_lam]
instId_tm [lemma, in Chapter3.utlc_pure]
instId_tm [lemma, in Chapter10.sysf]
instId_ty [lemma, in Chapter10.sysf]
instId_ty [lemma, in Chapter6.recty]
instId_tm [lemma, in Chapter10.sysf_pat]
instId_pat [lemma, in Chapter10.sysf_pat]
instId_ty [lemma, in Chapter10.sysf_pat]
In_exp_arith [constructor, in Chapter7.expressions]
In_exp_bool [constructor, in Chapter7.expressions]
In_exp_lam [constructor, in Chapter7.expressions]
In_exp_var [constructor, in Chapter7.expressions]
In_ty_arith [constructor, in Chapter7.expressions]
In_ty_bool [constructor, in Chapter7.expressions]
In_ty_lam [constructor, in Chapter7.expressions]
in_map [lemma, in Chapter10.POPLMark22]
in_map [lemma, in Chapter10.POPLMark21]
in_rel [projection, in header_metacoq]
in_subtype [projection, in header_metacoq]
isIn_exp_exp_var [definition, in Chapter7.expressions]
isIn_exp_exp_bool [definition, in Chapter7.expressions]
isIn_exp_exp_arith [definition, in Chapter7.expressions]
isIn_exp_exp_lam [definition, in Chapter7.expressions]
L
L [module, in Chapter9.girard]L [definition, in Chapter9.girard]
L [definition, in Chapter9.sn_mod]
L [definition, in Chapter9.wn]
label_equiv_map [lemma, in Chapter10.POPLMark22]
label_equiv [definition, in Chapter10.POPLMark22]
label_equiv_map [lemma, in Chapter10.POPLMark21]
label_equiv [definition, in Chapter10.POPLMark21]
lam [constructor, in Chapter3.utlc_scoped]
lam [constructor, in Chapter6.variadic_list]
lam [constructor, in Chapter6.variadic_fin]
lam [constructor, in Chapter6.sysf_cbv]
lam [constructor, in Chapter9.stlc]
lam [constructor, in Chapter6.utlc_pairs]
lam [constructor, in Chapter3.utlc_pure]
lam [constructor, in Chapter4.termination]
Lam [constructor, in Chapter4.sigmacalculus]
leafPairL [constructor, in Chapter4.termination]
leafPairR [constructor, in Chapter4.termination]
leafSingleton [constructor, in Chapter4.termination]
leafTermStep [constructor, in Chapter4.termination]
leaf_step [inductive, in Chapter4.termination]
letpat [constructor, in Chapter10.sysf_pat]
letpat_eval [constructor, in Chapter10.POPLMark22]
letpat_ty [constructor, in Chapter10.POPLMark22]
letpat_eval [constructor, in Chapter10.POPLMark21]
letpat_ty [constructor, in Chapter10.POPLMark21]
lift [definition, in header_extensible]
list_dec [lemma, in Chapter10.POPLMark22]
list_dec [lemma, in Chapter10.POPLMark21]
list_comp [definition, in axioms]
list_id [definition, in axioms]
list_ext [definition, in axioms]
locally_confluent [definition, in ARS]
logeq [definition, in Chapter9.equivalence]
logeq_id [lemma, in Chapter9.equivalence]
logeq_rel [definition, in Chapter9.equivalence]
logeq_trans [lemma, in Chapter9.equivalence]
logeq_sym [lemma, in Chapter9.equivalence]
logeq_backward_closure [lemma, in Chapter9.equivalence]
logEq_monotone [lemma, in Chapter9.equivalence]
ltc [definition, in Chapter9.preservation]
ltc [definition, in Chapter9.variadic_preservation]
L_close_ren_lam [lemma, in Chapter9.sn]
L_strong [definition, in Chapter9.sn]
L_strong_lam [definition, in Chapter9.sn_lam]
L_val_lam [lemma, in Chapter9.sn_lam]
L_close_ren [definition, in Chapter9.sn_mod]
L_strong [definition, in Chapter9.sn_mod]
L_ren [definition, in Chapter9.sn_mod]
L_close_ren_bool [lemma, in Chapter9.sn_bool]
L_close_ren_arith [lemma, in Chapter9.sn_arith]
L_ren [lemma, in Chapter9.wn]
L.Girard [lemma, in Chapter9.girard]
L.L_typing [lemma, in Chapter9.girard]
L.neutral [definition, in Chapter9.girard]
L.preservation [lemma, in Chapter9.girard]
L.preservation_mstep [lemma, in Chapter9.girard]
L.ren [lemma, in Chapter9.girard]
L.sn [lemma, in Chapter9.girard]
L.var [lemma, in Chapter9.girard]
M
main [lemma, in Chapter9.equivalence]main_lemma [lemma, in Chapter9.sn_raamsdonk]
make_Bundle [constructor, in header_extensible]
matchpair [constructor, in Chapter6.utlc_pairs]
MiniML_var.L_strong [variable, in Chapter9.sn_var]
MiniML_var.L [variable, in Chapter9.sn_var]
MiniML_var.ren_preserves [variable, in Chapter9.sn_var]
MiniML_var.whnf_whnf_var [variable, in Chapter9.sn_var]
MiniML_var.step [variable, in Chapter9.sn_var]
MiniML_var.retract_has_ty_rev [variable, in Chapter9.sn_var]
MiniML_var.retract_has_ty [variable, in Chapter9.sn_var]
MiniML_var.has_ty [variable, in Chapter9.sn_var]
MiniML_var.subst_id_exp [variable, in Chapter9.sn_var]
MiniML_var.retract_subst_exp [variable, in Chapter9.sn_var]
MiniML_var.subst_exp [variable, in Chapter9.sn_var]
MiniML_var.retract_ren_exp [variable, in Chapter9.sn_var]
MiniML_var.ren_exp [variable, in Chapter9.sn_var]
MiniML_var.ty [variable, in Chapter9.sn_var]
MiniML_var.exp [variable, in Chapter9.sn_var]
MiniML_var [section, in Chapter9.sn_var]
MiniML_Lambda.E_strong_var [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_L_strong [variable, in Chapter9.sn_lam]
MiniML_Lambda.ren_var [variable, in Chapter9.sn_lam]
MiniML_Lambda.ren_preserves [variable, in Chapter9.sn_lam]
MiniML_Lambda.whnf_anti_renaming [variable, in Chapter9.sn_lam]
MiniML_Lambda.L_strong [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_whnf_lam [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_L [variable, in Chapter9.sn_lam]
MiniML_Lambda.L [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_step_rev [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_step [variable, in Chapter9.sn_lam]
MiniML_Lambda.step [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_has_ty_rev [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_has_ty [variable, in Chapter9.sn_lam]
MiniML_Lambda.hasty_var [variable, in Chapter9.sn_lam]
MiniML_Lambda.has_ty [variable, in Chapter9.sn_lam]
MiniML_Lambda.subst_exp_var [variable, in Chapter9.sn_lam]
MiniML_Lambda.up_exp_exp_def' [variable, in Chapter9.sn_lam]
MiniML_Lambda.up_exp_exp_def [variable, in Chapter9.sn_lam]
MiniML_Lambda.upRen_exp_exp_def [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_subst_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.retract_ren_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.rinst_inst_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.rinstInst_up_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.compSubstSubst_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.up_subst_subst_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.compSubstRen_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.up_subst_ren_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.compRenSubst_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.up_ren_subst_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.compRenRen_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.up_ren_ren_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.ext_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.upExt_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.extRen_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.upExtRen_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.idSubst_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.upId_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.subst_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.up_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.ren_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.upRen_exp_exp [variable, in Chapter9.sn_lam]
MiniML_Lambda.exp [variable, in Chapter9.sn_lam]
MiniML_Lambda [section, in Chapter9.sn_lam]
MiniML_Bool.ren_preserves [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_L_strong [variable, in Chapter9.sn_bool]
MiniML_Bool.whnf_whnf_bool [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_L [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_step_rev [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_step [variable, in Chapter9.sn_bool]
MiniML_Bool.step [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_has_ty_rev [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_has_ty [variable, in Chapter9.sn_bool]
MiniML_Bool.has_ty [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_subst_exp [variable, in Chapter9.sn_bool]
MiniML_Bool.subst_exp [variable, in Chapter9.sn_bool]
MiniML_Bool.retract_ren_exp [variable, in Chapter9.sn_bool]
MiniML_Bool.ren_exp [variable, in Chapter9.sn_bool]
MiniML_Bool.exp [variable, in Chapter9.sn_bool]
MiniML_Bool.ty [variable, in Chapter9.sn_bool]
MiniML_Bool [section, in Chapter9.sn_bool]
MiniML_Arith.step_anti_renaming [variable, in Chapter9.sn_arith]
MiniML_Arith.ren_preserves [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_L_strong [variable, in Chapter9.sn_arith]
MiniML_Arith.whnf_whnf_arith [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_L [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_step_rev [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_step [variable, in Chapter9.sn_arith]
MiniML_Arith.step [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_has_ty_rev [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_has_ty [variable, in Chapter9.sn_arith]
MiniML_Arith.has_ty [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_subst_exp [variable, in Chapter9.sn_arith]
MiniML_Arith.subst_exp [variable, in Chapter9.sn_arith]
MiniML_Arith.retract_ren_exp [variable, in Chapter9.sn_arith]
MiniML_Arith.ren_exp [variable, in Chapter9.sn_arith]
MiniML_Arith.exp [variable, in Chapter9.sn_arith]
MiniML_Arith.ty [variable, in Chapter9.sn_arith]
MiniML_Arith [section, in Chapter9.sn_arith]
mkDefinitionType [definition, in header_metacoq]
mkLemma [definition, in header_metacoq]
mkVariable [definition, in header_metacoq]
ModularFixpointN [definition, in header_metacoq]
ModularFixpoint2 [definition, in header_metacoq]
morphism [definition, in ARS]
mstep_beta [lemma, in Chapter9.reduction]
mstep_subst [lemma, in Chapter9.reduction]
mstep_inst [lemma, in Chapter9.reduction]
mstep_app [lemma, in Chapter9.reduction]
mstep_lam [lemma, in Chapter9.reduction]
mstep_inst [lemma, in Chapter9.variadic_preservation]
mwhr [inductive, in Chapter9.equivalence]
mwhrR [constructor, in Chapter9.equivalence]
mwhrS [constructor, in Chapter9.equivalence]
mwhr_ren [lemma, in Chapter9.equivalence]
mwhr_trans [lemma, in Chapter9.equivalence]
mwhr_appL [lemma, in Chapter9.equivalence]
N
name_after_dot [definition, in header_metacoq]name_after_dot' [definition, in header_metacoq]
natequiv_update [lemma, in Chapter10.POPLMark22]
natequiv_update [lemma, in Chapter10.POPLMark21]
natTy [constructor, in Chapter7.expressions]
natTy_ [definition, in Chapter7.expressions]
nat_subterm' [instance, in header_metacoq]
neutral [definition, in Chapter9.sn_raamsdonk]
neutral_preservation [lemma, in Chapter9.sn_raamsdonk]
neutral_mwhr [lemma, in Chapter9.equivalence]
neutral_whr [lemma, in Chapter9.equivalence]
newman [lemma, in ARS]
Nil [constructor, in Chapter6.picalculus]
None [definition, in unscoped]
norm [lemma, in Chapter9.sn_raamsdonk]
null [definition, in fintype]
null [definition, in fintype_variadic]
O
Or [inductive, in ARS]Out [constructor, in Chapter6.picalculus]
P
pair [constructor, in Chapter6.utlc_pairs]Pair [constructor, in Chapter4.termination]
pair [constructor, in Chapter4.termination]
PairRen [constructor, in Chapter4.termination]
PairRenaming [constructor, in Chapter4.termination]
Par [constructor, in Chapter6.picalculus]
pat [inductive, in Chapter4.termination]
pat [inductive, in Chapter10.sysf_pat]
pat [section, in Chapter10.sysf_pat]
patlist [constructor, in Chapter10.sysf_pat]
patPairL [constructor, in Chapter4.termination]
patPairR [constructor, in Chapter4.termination]
patSingleton [constructor, in Chapter4.termination]
patSplitApp [constructor, in Chapter4.termination]
patSplitComp [constructor, in Chapter4.termination]
patSplitLambda [constructor, in Chapter4.termination]
Pattern [section, in Chapter10.POPLMark22]
Pattern [section, in Chapter10.POPLMark21]
Pattern.pat_ty_eval [variable, in Chapter10.POPLMark22]
Pattern.pat_progress [variable, in Chapter10.POPLMark22]
Pattern.pat_ty_subst [variable, in Chapter10.POPLMark22]
Pattern.pat_eval [variable, in Chapter10.POPLMark22]
Pattern.pat_ty [variable, in Chapter10.POPLMark22]
Pattern.pat_ty_eval [variable, in Chapter10.POPLMark21]
Pattern.pat_progress [variable, in Chapter10.POPLMark21]
Pattern.pat_ty_subst [variable, in Chapter10.POPLMark21]
Pattern.pat_eval [variable, in Chapter10.POPLMark21]
Pattern.pat_ty [variable, in Chapter10.POPLMark21]
Pattern.sub_refl [variable, in Chapter10.POPLMark22]
Pattern.sub_refl [variable, in Chapter10.POPLMark21]
EV _ => _ [notation, in Chapter10.POPLMark22]
EV _ => _ [notation, in Chapter10.POPLMark21]
TY _ ; _ |- _ : _ [notation, in Chapter10.POPLMark22]
TY _ ; _ |- _ : _ [notation, in Chapter10.POPLMark21]
patvar [constructor, in Chapter10.sysf_pat]
picalculus [library]
plus [constructor, in Chapter7.expressions]
plus [constructor, in Chapter6.fol]
plus [inductive, in ARS]
plusR [constructor, in ARS]
plus_ [definition, in Chapter7.expressions]
polyadic [module, in Chapter6.reductions]
polyadic.beta [constructor, in Chapter6.reductions]
polyadic.beta_match [constructor, in Chapter6.reductions]
polyadic.polyadic [section, in Chapter6.reductions]
polyadic.step [inductive, in Chapter6.reductions]
polyadic.step_substitutive [lemma, in Chapter6.reductions]
POPLMark1 [library]
POPLMark21 [library]
POPLMark22 [library]
pred [constructor, in Chapter6.fol]
preservation [lemma, in Chapter10.POPLMark22]
preservation [lemma, in Chapter9.preservation]
preservation [lemma, in Chapter4.termination]
preservation [lemma, in Chapter10.POPLMark21]
preservation [lemma, in Chapter10.POPLMark1]
preservation [library]
preservation_var [lemma, in Chapter9.sn_var]
proc [inductive, in Chapter6.picalculus]
proc [section, in Chapter6.picalculus]
prod_comp [definition, in axioms]
prod_ext [definition, in axioms]
prod_id [definition, in axioms]
prod_map [definition, in axioms]
proj [constructor, in Chapter10.sysf_pat]
pstep [inductive, in Chapter4.termination]
Q
quote_list [definition, in header_metacoq]R
rectm [constructor, in Chapter10.sysf_pat]recty [constructor, in Chapter6.recty]
recty [constructor, in Chapter10.sysf_pat]
recty [library]
Red [definition, in Chapter9.sn_raamsdonk]
RedS [definition, in Chapter9.sn_raamsdonk]
redsn [inductive, in Chapter9.sn_raamsdonk]
redsn_backwards [lemma, in Chapter9.sn_raamsdonk]
redsn_app [constructor, in Chapter9.sn_raamsdonk]
redsn_beta [constructor, in Chapter9.sn_raamsdonk]
redSN_ind_2 [definition, in Chapter9.sn_raamsdonk]
reduction [library]
reductions [library]
red_var [lemma, in Chapter9.sn_raamsdonk]
Rel [definition, in ARS]
remove_suffix [definition, in header_metacoq]
remove_injs [definition, in header_metacoq]
ren [definition, in fintype]
ren [definition, in fintype_variadic]
Ren [inductive, in Chapter4.termination]
rename [lemma, in Chapter9.sn_raamsdonk]
rename_red [lemma, in Chapter9.sn_raamsdonk]
renComp_tm [lemma, in Chapter3.utlc_scoped]
renComp_tm [lemma, in Chapter6.variadic_list]
renComp_exp [lemma, in Chapter7.expressions]
renComp_exp_var [lemma, in Chapter7.expressions]
renComp_exp_bool [lemma, in Chapter7.expressions]
renComp_exp_arith [lemma, in Chapter7.expressions]
renComp_exp_lam [lemma, in Chapter7.expressions]
renComp_tm [lemma, in Chapter6.variadic_fin]
renComp_vl [lemma, in Chapter6.sysf_cbv]
renComp_tm [lemma, in Chapter6.sysf_cbv]
renComp_ty [lemma, in Chapter6.sysf_cbv]
renComp_tm [lemma, in Chapter9.stlc]
renComp_tm [lemma, in Chapter6.utlc_pairs]
renComp_exp [lemma, in Chapter9.sn_lam]
renComp_tm [lemma, in Chapter3.utlc_pure]
renComp_tm [lemma, in Chapter10.sysf]
renComp_ty [lemma, in Chapter10.sysf]
renComp_ty [lemma, in Chapter6.recty]
renComp_tm [lemma, in Chapter10.sysf_pat]
renComp_pat [lemma, in Chapter10.sysf_pat]
renComp_ty [lemma, in Chapter10.sysf_pat]
renComp'_tm [lemma, in Chapter3.utlc_scoped]
renComp'_tm [lemma, in Chapter6.variadic_list]
renComp'_exp [lemma, in Chapter7.expressions]
renComp'_exp_var [lemma, in Chapter7.expressions]
renComp'_exp_bool [lemma, in Chapter7.expressions]
renComp'_exp_arith [lemma, in Chapter7.expressions]
renComp'_exp_lam [lemma, in Chapter7.expressions]
renComp'_tm [lemma, in Chapter6.variadic_fin]
renComp'_vl [lemma, in Chapter6.sysf_cbv]
renComp'_tm [lemma, in Chapter6.sysf_cbv]
renComp'_ty [lemma, in Chapter6.sysf_cbv]
renComp'_tm [lemma, in Chapter9.stlc]
renComp'_tm [lemma, in Chapter6.utlc_pairs]
renComp'_exp [lemma, in Chapter9.sn_lam]
renComp'_tm [lemma, in Chapter3.utlc_pure]
renComp'_tm [lemma, in Chapter10.sysf]
renComp'_ty [lemma, in Chapter10.sysf]
renComp'_ty [lemma, in Chapter6.recty]
renComp'_tm [lemma, in Chapter10.sysf_pat]
renComp'_pat [lemma, in Chapter10.sysf_pat]
renComp'_ty [lemma, in Chapter10.sysf_pat]
RenExp [inductive, in Chapter4.termination]
renRen_tm [lemma, in Chapter3.utlc_scoped]
renRen_tm [lemma, in Chapter6.variadic_list]
renRen_exp [lemma, in Chapter7.expressions]
renRen_exp_var [lemma, in Chapter7.expressions]
renRen_exp_bool [lemma, in Chapter7.expressions]
renRen_exp_arith [lemma, in Chapter7.expressions]
renRen_exp_lam [lemma, in Chapter7.expressions]
renRen_tm [lemma, in Chapter6.variadic_fin]
renRen_vl [lemma, in Chapter6.sysf_cbv]
renRen_tm [lemma, in Chapter6.sysf_cbv]
renRen_ty [lemma, in Chapter6.sysf_cbv]
renRen_tm [lemma, in Chapter9.stlc]
renRen_tm [lemma, in Chapter6.utlc_pairs]
renRen_exp [lemma, in Chapter9.sn_lam]
renRen_tm [lemma, in Chapter3.utlc_pure]
renRen_tm [lemma, in Chapter10.sysf]
renRen_ty [lemma, in Chapter10.sysf]
renRen_proc [lemma, in Chapter6.picalculus]
renRen_chan [lemma, in Chapter6.picalculus]
renRen_ty [lemma, in Chapter6.recty]
renRen_tm [lemma, in Chapter10.sysf_pat]
renRen_pat [lemma, in Chapter10.sysf_pat]
renRen_ty [lemma, in Chapter10.sysf_pat]
renRen'_tm [lemma, in Chapter3.utlc_scoped]
renRen'_tm [lemma, in Chapter6.variadic_list]
renRen'_exp [lemma, in Chapter7.expressions]
renRen'_exp_var [lemma, in Chapter7.expressions]
renRen'_exp_bool [lemma, in Chapter7.expressions]
renRen'_exp_arith [lemma, in Chapter7.expressions]
renRen'_exp_lam [lemma, in Chapter7.expressions]
renRen'_tm [lemma, in Chapter6.variadic_fin]
renRen'_vl [lemma, in Chapter6.sysf_cbv]
renRen'_tm [lemma, in Chapter6.sysf_cbv]
renRen'_ty [lemma, in Chapter6.sysf_cbv]
renRen'_tm [lemma, in Chapter9.stlc]
renRen'_tm [lemma, in Chapter6.utlc_pairs]
renRen'_exp [lemma, in Chapter9.sn_lam]
renRen'_tm [lemma, in Chapter3.utlc_pure]
renRen'_tm [lemma, in Chapter10.sysf]
renRen'_ty [lemma, in Chapter10.sysf]
renRen'_proc [lemma, in Chapter6.picalculus]
renRen'_chan [lemma, in Chapter6.picalculus]
renRen'_ty [lemma, in Chapter6.recty]
renRen'_tm [lemma, in Chapter10.sysf_pat]
renRen'_pat [lemma, in Chapter10.sysf_pat]
renRen'_ty [lemma, in Chapter10.sysf_pat]
RenTerm [constructor, in Chapter4.termination]
Ren_tm [instance, in Chapter3.utlc_scoped]
ren_tm [definition, in Chapter3.utlc_scoped]
Ren_tm [instance, in Chapter6.variadic_list]
ren_tm [definition, in Chapter6.variadic_list]
Ren_exp [instance, in Chapter7.expressions]
ren_exp [definition, in Chapter7.expressions]
ren_exp_var [definition, in Chapter7.expressions]
ren_exp_bool [definition, in Chapter7.expressions]
ren_exp_arith [definition, in Chapter7.expressions]
ren_exp_lam [definition, in Chapter7.expressions]
Ren_tm [instance, in Chapter6.variadic_fin]
ren_tm [definition, in Chapter6.variadic_fin]
Ren_vl [instance, in Chapter6.sysf_cbv]
Ren_tm [instance, in Chapter6.sysf_cbv]
Ren_ty [instance, in Chapter6.sysf_cbv]
ren_vl [definition, in Chapter6.sysf_cbv]
ren_tm [definition, in Chapter6.sysf_cbv]
ren_ty [definition, in Chapter6.sysf_cbv]
Ren_tm [instance, in Chapter9.stlc]
ren_tm [definition, in Chapter9.stlc]
ren_preserves_var [lemma, in Chapter9.sn_var]
Ren_tm [instance, in Chapter6.utlc_pairs]
ren_tm [definition, in Chapter6.utlc_pairs]
ren_preserves_app [lemma, in Chapter9.sn_lam]
ren_preserves_ab [lemma, in Chapter9.sn_lam]
ren_preserves_arith [lemma, in Chapter9.sn_mod]
ren_preserves_bool [lemma, in Chapter9.sn_mod]
ren_preserves_lam [lemma, in Chapter9.sn_mod]
ren_preserves [lemma, in Chapter9.sn_mod]
ren_preserves_constBool [lemma, in Chapter9.sn_bool]
ren_preserves_If [lemma, in Chapter9.sn_bool]
Ren_tm [instance, in Chapter3.utlc_pure]
ren_tm [definition, in Chapter3.utlc_pure]
Ren_tm [instance, in Chapter10.sysf]
Ren_ty [instance, in Chapter10.sysf]
ren_tm [definition, in Chapter10.sysf]
ren_ty [definition, in Chapter10.sysf]
Ren_proc [instance, in Chapter6.picalculus]
Ren_chan [instance, in Chapter6.picalculus]
ren_proc [definition, in Chapter6.picalculus]
ren_chan [definition, in Chapter6.picalculus]
ren_sn [lemma, in Chapter4.termination]
ren_preserve [lemma, in Chapter4.termination]
Ren_ty [instance, in Chapter6.recty]
ren_ty [definition, in Chapter6.recty]
ren_preserves_constNat [lemma, in Chapter9.sn_arith]
ren_preserves_Plus [lemma, in Chapter9.sn_arith]
Ren_tm [instance, in Chapter10.sysf_pat]
Ren_pat [instance, in Chapter10.sysf_pat]
Ren_ty [instance, in Chapter10.sysf_pat]
ren_tm [definition, in Chapter10.sysf_pat]
ren_pat [definition, in Chapter10.sysf_pat]
ren_ty [definition, in Chapter10.sysf_pat]
ren1 [projection, in unscoped]
Ren1 [record, in unscoped]
ren1 [constructor, in unscoped]
Ren1 [inductive, in unscoped]
ren1 [projection, in fintype]
Ren1 [record, in fintype]
ren1 [constructor, in fintype]
Ren1 [inductive, in fintype]
ren1 [projection, in fintype_variadic]
Ren1 [record, in fintype_variadic]
ren1 [constructor, in fintype_variadic]
Ren1 [inductive, in fintype_variadic]
ren2 [projection, in unscoped]
Ren2 [record, in unscoped]
ren2 [constructor, in unscoped]
Ren2 [inductive, in unscoped]
ren2 [projection, in fintype]
Ren2 [record, in fintype]
ren2 [constructor, in fintype]
Ren2 [inductive, in fintype]
ren2 [projection, in fintype_variadic]
Ren2 [record, in fintype_variadic]
ren2 [constructor, in fintype_variadic]
Ren2 [inductive, in fintype_variadic]
ren3 [projection, in unscoped]
Ren3 [record, in unscoped]
ren3 [constructor, in unscoped]
Ren3 [inductive, in unscoped]
ren3 [projection, in fintype]
Ren3 [record, in fintype]
ren3 [constructor, in fintype]
Ren3 [inductive, in fintype]
ren3 [projection, in fintype_variadic]
Ren3 [record, in fintype_variadic]
ren3 [constructor, in fintype_variadic]
Ren3 [inductive, in fintype_variadic]
ren4 [projection, in unscoped]
Ren4 [record, in unscoped]
ren4 [constructor, in unscoped]
Ren4 [inductive, in unscoped]
ren4 [projection, in fintype]
Ren4 [record, in fintype]
ren4 [constructor, in fintype]
Ren4 [inductive, in fintype]
ren4 [projection, in fintype_variadic]
Ren4 [record, in fintype_variadic]
ren4 [constructor, in fintype_variadic]
Ren4 [inductive, in fintype_variadic]
ren5 [projection, in unscoped]
Ren5 [record, in unscoped]
ren5 [constructor, in unscoped]
Ren5 [inductive, in unscoped]
ren5 [projection, in fintype]
Ren5 [record, in fintype]
ren5 [constructor, in fintype]
Ren5 [inductive, in fintype]
ren5 [projection, in fintype_variadic]
Ren5 [record, in fintype_variadic]
ren5 [constructor, in fintype_variadic]
Ren5 [inductive, in fintype_variadic]
replace_ext [definition, in header_metacoq]
replace_consts [definition, in header_metacoq]
replace_terms [definition, in header_metacoq]
replace_const [definition, in header_metacoq]
replace_term [definition, in header_metacoq]
Res [constructor, in Chapter6.picalculus]
retr [abbreviation, in header_extensible]
retract [record, in header_extensible]
retract_exp_var_exp [instance, in Chapter7.expressions]
retract_exp_bool_exp [instance, in Chapter7.expressions]
retract_exp_arith_exp [instance, in Chapter7.expressions]
retract_exp_lam_exp [instance, in Chapter7.expressions]
retract_ty_arith_ty [instance, in Chapter7.expressions]
retract_ty_bool_ty [instance, in Chapter7.expressions]
retract_ty_lam_ty [instance, in Chapter7.expressions]
retract_has_ty_rev_instance [instance, in Chapter9.sn_var]
retract_has_ty_instance [instance, in Chapter9.sn_var]
retract_step_rev_instance [instance, in Chapter9.sn_lam]
retract_step_instance [instance, in Chapter9.sn_lam]
retract_has_ty_rev_instance [instance, in Chapter9.sn_lam]
retract_has_ty_instance [instance, in Chapter9.sn_lam]
retract_step_arith [lemma, in Chapter9.sn_mod]
retract_step_bool [lemma, in Chapter9.sn_mod]
retract_step_lam [lemma, in Chapter9.sn_mod]
retract_step_rev_instance [instance, in Chapter9.sn_bool]
retract_step_instance [instance, in Chapter9.sn_bool]
retract_has_ty_rev_instance [instance, in Chapter9.sn_bool]
retract_has_ty_instance [instance, in Chapter9.sn_bool]
retract_step_rev_instance [instance, in Chapter9.sn_arith]
retract_step_instance [instance, in Chapter9.sn_arith]
retract_has_ty_rev_instance [instance, in Chapter9.sn_arith]
retract_has_ty_instance [instance, in Chapter9.sn_arith]
retract_option [instance, in header_extensible]
retract_inj [lemma, in header_extensible]
retract_tight [projection, in header_extensible]
retract_works [projection, in header_extensible]
retract_R [projection, in header_extensible]
retract_I [projection, in header_extensible]
rinstId_tm [lemma, in Chapter3.utlc_scoped]
rinstId_tm [lemma, in Chapter6.variadic_list]
rinstId_exp [lemma, in Chapter7.expressions]
rinstId_exp_var [lemma, in Chapter7.expressions]
rinstId_exp_bool [lemma, in Chapter7.expressions]
rinstId_exp_arith [lemma, in Chapter7.expressions]
rinstId_exp_lam [lemma, in Chapter7.expressions]
rinstId_tm [lemma, in Chapter6.variadic_fin]
rinstId_vl [lemma, in Chapter6.sysf_cbv]
rinstId_tm [lemma, in Chapter6.sysf_cbv]
rinstId_ty [lemma, in Chapter6.sysf_cbv]
rinstId_tm [lemma, in Chapter9.stlc]
rinstId_tm [lemma, in Chapter6.utlc_pairs]
rinstId_exp [lemma, in Chapter9.sn_lam]
rinstId_tm [lemma, in Chapter3.utlc_pure]
rinstId_tm [lemma, in Chapter10.sysf]
rinstId_ty [lemma, in Chapter10.sysf]
rinstId_ty [lemma, in Chapter6.recty]
rinstId_tm [lemma, in Chapter10.sysf_pat]
rinstId_pat [lemma, in Chapter10.sysf_pat]
rinstId_ty [lemma, in Chapter10.sysf_pat]
rinstInst_tm [lemma, in Chapter3.utlc_scoped]
rinstInst_up_list_tm_tm [definition, in Chapter3.utlc_scoped]
rinstInst_up_tm_tm [definition, in Chapter3.utlc_scoped]
rinstInst_tm [lemma, in Chapter6.variadic_list]
rinstInst_up_list_tm_tm [definition, in Chapter6.variadic_list]
rinstInst_up_tm_tm [definition, in Chapter6.variadic_list]
rinstInst_exp [lemma, in Chapter7.expressions]
rinstInst_up_exp_exp [definition, in Chapter7.expressions]
rinstInst_exp_var [lemma, in Chapter7.expressions]
rinstInst_exp_bool [lemma, in Chapter7.expressions]
rinstInst_exp_arith [lemma, in Chapter7.expressions]
rinstInst_exp_lam [lemma, in Chapter7.expressions]
rinstInst_tm [lemma, in Chapter6.variadic_fin]
rinstInst_up_list_tm_tm [definition, in Chapter6.variadic_fin]
rinstInst_up_tm_tm [definition, in Chapter6.variadic_fin]
rinstInst_vl [lemma, in Chapter6.sysf_cbv]
rinstInst_tm [lemma, in Chapter6.sysf_cbv]
rinstInst_up_list_vl_vl [definition, in Chapter6.sysf_cbv]
rinstInst_up_list_vl_ty [definition, in Chapter6.sysf_cbv]
rinstInst_up_list_ty_vl [definition, in Chapter6.sysf_cbv]
rinstInst_up_vl_vl [definition, in Chapter6.sysf_cbv]
rinstInst_up_vl_ty [definition, in Chapter6.sysf_cbv]
rinstInst_up_ty_vl [definition, in Chapter6.sysf_cbv]
rinstInst_ty [lemma, in Chapter6.sysf_cbv]
rinstInst_up_list_ty_ty [definition, in Chapter6.sysf_cbv]
rinstInst_up_ty_ty [definition, in Chapter6.sysf_cbv]
rinstInst_tm [lemma, in Chapter9.stlc]
rinstInst_up_list_tm_tm [definition, in Chapter9.stlc]
rinstInst_up_tm_tm [definition, in Chapter9.stlc]
rinstInst_tm [lemma, in Chapter6.utlc_pairs]
rinstInst_up_list_tm_tm [definition, in Chapter6.utlc_pairs]
rinstInst_up_tm_tm [definition, in Chapter6.utlc_pairs]
rinstInst_exp [lemma, in Chapter9.sn_lam]
rinstInst_tm [lemma, in Chapter3.utlc_pure]
rinstInst_up_tm_tm [definition, in Chapter3.utlc_pure]
rinstInst_tm [lemma, in Chapter10.sysf]
rinstInst_up_list_tm_tm [definition, in Chapter10.sysf]
rinstInst_up_list_tm_ty [definition, in Chapter10.sysf]
rinstInst_up_list_ty_tm [definition, in Chapter10.sysf]
rinstInst_up_tm_tm [definition, in Chapter10.sysf]
rinstInst_up_tm_ty [definition, in Chapter10.sysf]
rinstInst_up_ty_tm [definition, in Chapter10.sysf]
rinstInst_ty [lemma, in Chapter10.sysf]
rinstInst_up_list_ty_ty [definition, in Chapter10.sysf]
rinstInst_up_ty_ty [definition, in Chapter10.sysf]
rinstInst_ty [lemma, in Chapter6.recty]
rinstInst_up_list_ty_ty [definition, in Chapter6.recty]
rinstInst_up_ty_ty [definition, in Chapter6.recty]
rinstInst_tm [lemma, in Chapter10.sysf_pat]
rinstInst_up_list_tm_tm [definition, in Chapter10.sysf_pat]
rinstInst_up_list_tm_ty [definition, in Chapter10.sysf_pat]
rinstInst_up_list_ty_tm [definition, in Chapter10.sysf_pat]
rinstInst_up_tm_tm [definition, in Chapter10.sysf_pat]
rinstInst_up_tm_ty [definition, in Chapter10.sysf_pat]
rinstInst_up_ty_tm [definition, in Chapter10.sysf_pat]
rinstInst_pat [lemma, in Chapter10.sysf_pat]
rinstInst_ty [lemma, in Chapter10.sysf_pat]
rinstInst_up_list_ty_ty [definition, in Chapter10.sysf_pat]
rinstInst_up_ty_ty [definition, in Chapter10.sysf_pat]
rinst_inst_tm [definition, in Chapter3.utlc_scoped]
rinst_inst_tm [definition, in Chapter6.variadic_list]
rinst_inst_exp [definition, in Chapter7.expressions]
rinst_inst_exp_var [definition, in Chapter7.expressions]
rinst_inst_exp_bool [definition, in Chapter7.expressions]
rinst_inst_exp_arith [definition, in Chapter7.expressions]
rinst_inst_exp_lam [definition, in Chapter7.expressions]
rinst_inst_tm [definition, in Chapter6.variadic_fin]
rinst_inst_vl [definition, in Chapter6.sysf_cbv]
rinst_inst_tm [definition, in Chapter6.sysf_cbv]
rinst_inst_ty [definition, in Chapter6.sysf_cbv]
rinst_inst_tm [definition, in Chapter9.stlc]
rinst_inst_tm [definition, in Chapter6.utlc_pairs]
rinst_inst_tm [definition, in Chapter3.utlc_pure]
rinst_inst_tm [definition, in Chapter10.sysf]
rinst_inst_ty [definition, in Chapter10.sysf]
rinst_inst_ty [definition, in Chapter6.recty]
rinst_inst_tm [definition, in Chapter10.sysf_pat]
rinst_inst_pat [definition, in Chapter10.sysf_pat]
rinst_inst_ty [definition, in Chapter10.sysf_pat]
S
SAbs [constructor, in Chapter9.sn_raamsdonk]SApp [constructor, in Chapter9.sn_raamsdonk]
SAppl [constructor, in Chapter9.sn_raamsdonk]
SA_rec [constructor, in Chapter10.POPLMark22]
SA_all [constructor, in Chapter10.POPLMark22]
SA_arrow [constructor, in Chapter10.POPLMark22]
SA_Trans [constructor, in Chapter10.POPLMark22]
SA_Refl [constructor, in Chapter10.POPLMark22]
SA_top [constructor, in Chapter10.POPLMark22]
SA_rec [constructor, in Chapter10.POPLMark21]
SA_all [constructor, in Chapter10.POPLMark21]
SA_arrow [constructor, in Chapter10.POPLMark21]
SA_Trans [constructor, in Chapter10.POPLMark21]
SA_Refl [constructor, in Chapter10.POPLMark21]
SA_top [constructor, in Chapter10.POPLMark21]
SA_all [constructor, in Chapter10.POPLMark1]
SA_arrow [constructor, in Chapter10.POPLMark1]
SA_Trans [constructor, in Chapter10.POPLMark1]
SA_Refl [constructor, in Chapter10.POPLMark1]
SA_top [constructor, in Chapter10.POPLMark1]
SBeta [constructor, in Chapter9.sn_raamsdonk]
scons [definition, in unscoped]
scons [definition, in fintype]
scons [definition, in fintype_variadic]
scons_comp [lemma, in unscoped]
scons_eta [lemma, in unscoped]
scons_eta_id [lemma, in unscoped]
scons_p_eta [lemma, in fintype]
scons_p_congr [lemma, in fintype]
scons_p_comp [lemma, in fintype]
scons_p_comp' [lemma, in fintype]
scons_p_tail [lemma, in fintype]
scons_p_tail' [lemma, in fintype]
scons_p_head [lemma, in fintype]
scons_p_head' [lemma, in fintype]
scons_p [definition, in fintype]
scons_comp [lemma, in fintype]
scons_eta_id [lemma, in fintype]
scons_eta [lemma, in fintype]
scons_p_eta [lemma, in fintype_variadic]
scons_p_congr [lemma, in fintype_variadic]
scons_p_comp [lemma, in fintype_variadic]
scons_p_comp' [lemma, in fintype_variadic]
scons_p_tail [lemma, in fintype_variadic]
scons_p_tail' [lemma, in fintype_variadic]
scons_p_head [lemma, in fintype_variadic]
scons_p_head' [lemma, in fintype_variadic]
scons_p [definition, in fintype_variadic]
scons_comp [lemma, in fintype_variadic]
scons_eta_id [lemma, in fintype_variadic]
scons_eta [lemma, in fintype_variadic]
setoid_crutch [lemma, in Chapter4.soundness]
shift [definition, in unscoped]
shift [definition, in fintype]
shift [definition, in fintype_variadic]
shift_p [definition, in fintype]
shift_p [definition, in fintype_variadic]
sigmacalculus [library]
Singleton [constructor, in Chapter4.termination]
SingletonRen [constructor, in Chapter4.termination]
size_ind [lemma, in header_extensible]
SN [inductive, in Chapter9.sn_raamsdonk]
sn [inductive, in Chapter9.defs]
sn [lemma, in Chapter9.sn]
SN [module, in Chapter9.girard]
sn [abbreviation, in Chapter9.girard]
sn [inductive, in ARS]
sn [library]
SNe [inductive, in Chapter9.sn_raamsdonk]
SNeu [constructor, in Chapter9.sn_raamsdonk]
SNe_ind_2 [definition, in Chapter9.sn_raamsdonk]
SNI [constructor, in Chapter9.defs]
SNI [constructor, in ARS]
SNRed [inductive, in Chapter9.sn_raamsdonk]
SN_sn [lemma, in Chapter9.sn_raamsdonk]
sn_app_neutral [lemma, in Chapter9.sn_raamsdonk]
sn_confluence [lemma, in Chapter9.sn_raamsdonk]
sn_subst_tm [lemma, in Chapter9.sn_raamsdonk]
sn_appL [lemma, in Chapter9.sn_raamsdonk]
SN_multind [definition, in Chapter9.sn_raamsdonk]
SN_ind_2 [definition, in Chapter9.sn_raamsdonk]
sn_mstep [lemma, in Chapter9.sn_raamsdonk]
sn_fundamental_var [lemma, in Chapter9.sn_var]
sn_fundamental [lemma, in Chapter9.sn]
sn_lam [lemma, in Chapter9.sn_mod]
sn_subst [lemma, in Chapter4.termination]
sn_exp [lemma, in Chapter4.termination]
sn_uexp [lemma, in Chapter4.termination]
sn_uexp_comp [lemma, in Chapter4.termination]
sn_uexp_shift [lemma, in Chapter4.termination]
sn_pstep_shift [lemma, in Chapter4.termination]
sn_leaf_Ren [lemma, in Chapter4.termination]
sn_leaf_pair [lemma, in Chapter4.termination]
sn_leaf_Singleton [lemma, in Chapter4.termination]
sn_leaf_Term [lemma, in Chapter4.termination]
sn_split [lemma, in Chapter4.termination]
sn_split_term [lemma, in Chapter4.termination]
sn_split_pair [lemma, in Chapter4.termination]
sn_split_singleton [lemma, in Chapter4.termination]
sn_pair' [lemma, in Chapter4.termination]
sn_CCompR' [lemma, in Chapter4.termination]
sn_CCompL' [lemma, in Chapter4.termination]
sn_pairR' [lemma, in Chapter4.termination]
sn_pairL' [lemma, in Chapter4.termination]
sn_CLam [lemma, in Chapter4.termination]
sn_zero' [lemma, in Chapter4.termination]
sn_pair [lemma, in Chapter4.termination]
sn_lam [lemma, in Chapter4.termination]
sn_zero [lemma, in Chapter4.termination]
sn_uquiv_red_eq [lemma, in Chapter4.termination]
sn_uquiv_red [lemma, in Chapter4.termination]
sn_sub [lemma, in Chapter4.termination]
sn_sub_comp [lemma, in Chapter4.termination]
sn_sub_pair [lemma, in Chapter4.termination]
sn_sub_lam [lemma, in Chapter4.termination]
sn_uquiv_equiv_subst [lemma, in Chapter4.termination]
sn_uquiv_equiv [lemma, in Chapter4.termination]
sn_plus [lemma, in ARS]
sn_forward_star [lemma, in ARS]
sn_orR [lemma, in ARS]
sn_orL [lemma, in ARS]
sn_morphism [lemma, in ARS]
sn_lam [library]
sn_var [library]
sn_raamsdonk [library]
sn_arith [library]
sn_bool [library]
sn_mod [library]
SN.weak [lemma, in Chapter9.girard]
Some [definition, in unscoped]
some_none_explosion [lemma, in header_extensible]
Some_inj [lemma, in header_extensible]
soundness [definition, in Chapter4.soundness]
soundness [library]
soundness_subst [definition, in Chapter4.soundness]
split [inductive, in Chapter4.termination]
split_forall_impl [definition, in header_metacoq]
SRed [constructor, in Chapter9.sn_raamsdonk]
srefl [constructor, in Chapter9.defs]
star [inductive, in Chapter9.defs]
star [inductive, in ARS]
starR [constructor, in ARS]
starSE [constructor, in ARS]
star_trans [lemma, in Chapter9.defs]
star_appR [lemma, in Chapter9.sn_lam]
star_appL [lemma, in Chapter9.sn_lam]
star_If1 [lemma, in Chapter9.sn_bool]
star_plus2 [lemma, in Chapter9.sn_arith]
star_plus1 [lemma, in Chapter9.sn_arith]
star_CompR [lemma, in Chapter4.sigmacalculus]
star_CompL [lemma, in Chapter4.sigmacalculus]
star_ConsR [lemma, in Chapter4.sigmacalculus]
star_ConsL [lemma, in Chapter4.sigmacalculus]
star_InstR [lemma, in Chapter4.sigmacalculus]
star_InstL [lemma, in Chapter4.sigmacalculus]
star_Lam [lemma, in Chapter4.sigmacalculus]
star_AppR [lemma, in Chapter4.sigmacalculus]
star_AppL [lemma, in Chapter4.sigmacalculus]
star_plus [lemma, in ARS]
star_hom [lemma, in ARS]
star_img [lemma, in ARS]
star_trans [lemma, in ARS]
star1 [lemma, in ARS]
step [inductive, in Chapter9.sn_mod]
step [inductive, in Chapter9.reduction]
step [inductive, in Chapter9.variadic_preservation]
stepAppL [constructor, in Chapter9.sn_lam]
stepAppR [constructor, in Chapter9.sn_lam]
stepBeta [constructor, in Chapter9.sn_lam]
stepBeta' [lemma, in Chapter9.sn_lam]
stepIfBeta [constructor, in Chapter9.sn_bool]
stepIf1 [constructor, in Chapter9.sn_bool]
stepIf2 [constructor, in Chapter9.sn_bool]
stepIf3 [constructor, in Chapter9.sn_bool]
stepLam [constructor, in Chapter9.sn_lam]
stepPlus [constructor, in Chapter9.sn_arith]
stepPlus1 [constructor, in Chapter9.sn_arith]
stepPlus2 [constructor, in Chapter9.sn_arith]
step_inst_var [lemma, in Chapter9.sn_var]
step_anti_renaming_var [lemma, in Chapter9.sn_var]
step_var [inductive, in Chapter9.sn_var]
step_lam [inductive, in Chapter9.sn_lam]
step_features [instance, in Chapter9.sn_mod]
step_bool [inductive, in Chapter9.sn_bool]
step_naturality [lemma, in Chapter9.reduction]
step_inst [lemma, in Chapter9.reduction]
step_beta' [lemma, in Chapter9.reduction]
step_appR [constructor, in Chapter9.reduction]
step_appL [constructor, in Chapter9.reduction]
step_abs [constructor, in Chapter9.reduction]
step_beta [constructor, in Chapter9.reduction]
step_arith [inductive, in Chapter9.sn_arith]
step_typing [lemma, in Chapter9.variadic_preservation]
step_inst [lemma, in Chapter9.variadic_preservation]
step_beta' [lemma, in Chapter9.variadic_preservation]
step_appL [constructor, in Chapter9.variadic_preservation]
step_abs [constructor, in Chapter9.variadic_preservation]
step_beta [constructor, in Chapter9.variadic_preservation]
stlc [library]
strans [constructor, in Chapter9.defs]
strong_normalisation [lemma, in Chapter9.girard]
sub [inductive, in Chapter10.POPLMark22]
sub [inductive, in Chapter4.termination]
sub [inductive, in Chapter10.POPLMark21]
sub [inductive, in Chapter10.POPLMark1]
Subst_tm [instance, in Chapter3.utlc_scoped]
subst_tm [definition, in Chapter3.utlc_scoped]
Subst_tm [instance, in Chapter6.variadic_list]
subst_tm [definition, in Chapter6.variadic_list]
Subst_exp [instance, in Chapter7.expressions]
subst_exp [definition, in Chapter7.expressions]
subst_exp_var [definition, in Chapter7.expressions]
subst_exp_bool [definition, in Chapter7.expressions]
subst_exp_arith [definition, in Chapter7.expressions]
subst_exp_lam [definition, in Chapter7.expressions]
Subst_tm [instance, in Chapter6.variadic_fin]
subst_tm [definition, in Chapter6.variadic_fin]
Subst_vl [instance, in Chapter6.sysf_cbv]
Subst_tm [instance, in Chapter6.sysf_cbv]
Subst_ty [instance, in Chapter6.sysf_cbv]
subst_vl [definition, in Chapter6.sysf_cbv]
subst_tm [definition, in Chapter6.sysf_cbv]
subst_ty [definition, in Chapter6.sysf_cbv]
Subst_tm [instance, in Chapter9.stlc]
subst_tm [definition, in Chapter9.stlc]
Subst_tm [instance, in Chapter6.utlc_pairs]
subst_tm [definition, in Chapter6.utlc_pairs]
Subst_form [instance, in Chapter6.fol]
Subst_tm [instance, in Chapter6.fol]
subst_form [definition, in Chapter6.fol]
subst_tm [definition, in Chapter6.fol]
Subst_tm [instance, in Chapter3.utlc_pure]
subst_tm [definition, in Chapter3.utlc_pure]
Subst_tm [instance, in Chapter10.sysf]
Subst_ty [instance, in Chapter10.sysf]
subst_tm [definition, in Chapter10.sysf]
subst_ty [definition, in Chapter10.sysf]
subst_exp_uexp [definition, in Chapter4.termination]
Subst_ty [instance, in Chapter6.recty]
subst_ty [definition, in Chapter6.recty]
subst_exp [inductive, in Chapter4.sigmacalculus]
Subst_tm [instance, in Chapter10.sysf_pat]
Subst_pat [instance, in Chapter10.sysf_pat]
Subst_ty [instance, in Chapter10.sysf_pat]
subst_tm [definition, in Chapter10.sysf_pat]
subst_pat [definition, in Chapter10.sysf_pat]
subst_ty [definition, in Chapter10.sysf_pat]
subst1 [projection, in unscoped]
Subst1 [record, in unscoped]
subst1 [constructor, in unscoped]
Subst1 [inductive, in unscoped]
subst1 [projection, in fintype]
Subst1 [record, in fintype]
subst1 [constructor, in fintype]
Subst1 [inductive, in fintype]
subst1 [projection, in fintype_variadic]
Subst1 [record, in fintype_variadic]
subst1 [constructor, in fintype_variadic]
Subst1 [inductive, in fintype_variadic]
subst2 [projection, in unscoped]
Subst2 [record, in unscoped]
subst2 [constructor, in unscoped]
Subst2 [inductive, in unscoped]
subst2 [projection, in fintype]
Subst2 [record, in fintype]
subst2 [constructor, in fintype]
Subst2 [inductive, in fintype]
subst2 [projection, in fintype_variadic]
Subst2 [record, in fintype_variadic]
subst2 [constructor, in fintype_variadic]
Subst2 [inductive, in fintype_variadic]
subst3 [projection, in unscoped]
Subst3 [record, in unscoped]
subst3 [constructor, in unscoped]
Subst3 [inductive, in unscoped]
subst3 [projection, in fintype]
Subst3 [record, in fintype]
subst3 [constructor, in fintype]
Subst3 [inductive, in fintype]
subst3 [projection, in fintype_variadic]
Subst3 [record, in fintype_variadic]
subst3 [constructor, in fintype_variadic]
Subst3 [inductive, in fintype_variadic]
subst4 [projection, in unscoped]
Subst4 [record, in unscoped]
subst4 [constructor, in unscoped]
Subst4 [inductive, in unscoped]
subst4 [projection, in fintype]
Subst4 [record, in fintype]
subst4 [constructor, in fintype]
Subst4 [inductive, in fintype]
subst4 [projection, in fintype_variadic]
Subst4 [record, in fintype_variadic]
subst4 [constructor, in fintype_variadic]
Subst4 [inductive, in fintype_variadic]
subst5 [projection, in unscoped]
Subst5 [record, in unscoped]
subst5 [constructor, in unscoped]
Subst5 [inductive, in unscoped]
subst5 [projection, in fintype]
Subst5 [record, in fintype]
subst5 [constructor, in fintype]
Subst5 [inductive, in fintype]
subst5 [projection, in fintype_variadic]
Subst5 [record, in fintype_variadic]
subst5 [constructor, in fintype_variadic]
Subst5 [inductive, in fintype_variadic]
subtermC [record, in header_metacoq]
subtermC [inductive, in header_metacoq]
subterm_rel [projection, in header_metacoq]
subterm_rel [constructor, in header_metacoq]
sub_substitution [lemma, in Chapter10.POPLMark22]
sub_trans [lemma, in Chapter10.POPLMark22]
sub_trans' [lemma, in Chapter10.POPLMark22]
sub_narrow [lemma, in Chapter10.POPLMark22]
sub_weak1 [lemma, in Chapter10.POPLMark22]
sub_weak [lemma, in Chapter10.POPLMark22]
sub_rec [lemma, in Chapter10.POPLMark22]
sub_substitution [lemma, in Chapter10.POPLMark21]
sub_trans [lemma, in Chapter10.POPLMark21]
sub_trans' [lemma, in Chapter10.POPLMark21]
sub_narrow [lemma, in Chapter10.POPLMark21]
sub_weak1 [lemma, in Chapter10.POPLMark21]
sub_weak [lemma, in Chapter10.POPLMark21]
sub_rec [lemma, in Chapter10.POPLMark21]
sub_substitution [lemma, in Chapter10.POPLMark1]
sub_trans [lemma, in Chapter10.POPLMark1]
sub_trans' [lemma, in Chapter10.POPLMark1]
sub_narrow [lemma, in Chapter10.POPLMark1]
sub_weak1 [lemma, in Chapter10.POPLMark1]
sub_weak [lemma, in Chapter10.POPLMark1]
sub_refl [lemma, in Chapter10.POPLMark1]
Succ [constructor, in Chapter4.sigmacalculus]
SVar [constructor, in Chapter9.sn_raamsdonk]
sysf [library]
sysf_cbv.step_substitutive [lemma, in Chapter6.reductions]
sysf_cbv.Beta [constructor, in Chapter6.reductions]
sysf_cbv.beta [constructor, in Chapter6.reductions]
sysf_cbv.step [inductive, in Chapter6.reductions]
sysf_cbv.sysf_cbv [section, in Chapter6.reductions]
sysf_cbv [module, in Chapter6.reductions]
sysf_cbv [library]
sysf_pat [library]
T
tabs [constructor, in Chapter10.sysf]tabs [constructor, in Chapter10.sysf_pat]
tactics [library]
tapp [constructor, in Chapter6.sysf_cbv]
tapp [constructor, in Chapter10.sysf]
tapp [constructor, in Chapter10.sysf_pat]
Term [constructor, in Chapter4.termination]
terminating [definition, in ARS]
termination [library]
tlam [constructor, in Chapter6.sysf_cbv]
tm [inductive, in Chapter3.utlc_scoped]
tm [section, in Chapter3.utlc_scoped]
tm [inductive, in Chapter6.variadic_list]
tm [section, in Chapter6.variadic_list]
tm [inductive, in Chapter6.variadic_fin]
tm [section, in Chapter6.variadic_fin]
tm [inductive, in Chapter6.sysf_cbv]
tm [inductive, in Chapter9.stlc]
tm [section, in Chapter9.stlc]
tm [inductive, in Chapter6.utlc_pairs]
tm [section, in Chapter6.utlc_pairs]
tm [inductive, in Chapter6.fol]
tm [section, in Chapter6.fol]
tm [inductive, in Chapter3.utlc_pure]
tm [section, in Chapter3.utlc_pure]
tm [inductive, in Chapter10.sysf]
tm [inductive, in Chapter10.sysf_pat]
tm [section, in Chapter10.sysf_pat]
tmMkDefinition [definition, in header_metacoq]
tmTryInferInstance [definition, in header_metacoq]
tmvl [section, in Chapter6.sysf_cbv]
top [constructor, in Chapter10.sysf]
top [constructor, in Chapter6.recty]
top [constructor, in Chapter10.sysf_pat]
transitivity_ren [lemma, in Chapter10.POPLMark22]
transitivity_proj [lemma, in Chapter10.POPLMark22]
transitivity_at [definition, in Chapter10.POPLMark22]
transitivity_ren [lemma, in Chapter10.POPLMark21]
transitivity_proj [lemma, in Chapter10.POPLMark21]
transitivity_at [definition, in Chapter10.POPLMark21]
transitivity_ren [lemma, in Chapter10.POPLMark1]
transitivity_proj [lemma, in Chapter10.POPLMark1]
transitivity_at [definition, in Chapter10.POPLMark1]
ty [inductive, in Chapter7.expressions]
ty [section, in Chapter7.expressions]
ty [inductive, in Chapter6.sysf_cbv]
ty [section, in Chapter6.sysf_cbv]
ty [inductive, in Chapter9.stlc]
ty [section, in Chapter9.stlc]
ty [inductive, in Chapter9.equivalence]
ty [inductive, in Chapter10.sysf]
ty [inductive, in Chapter6.recty]
ty [section, in Chapter6.recty]
ty [inductive, in Chapter9.variadic_preservation]
ty [inductive, in Chapter10.sysf_pat]
ty [section, in Chapter10.sysf_pat]
type_unique [lemma, in Chapter9.equivalence]
typing_inst [lemma, in Chapter9.preservation]
typing_ren [lemma, in Chapter9.preservation]
typing_inst [lemma, in Chapter9.variadic_preservation]
typing_ren [lemma, in Chapter9.variadic_preservation]
ty_arith.retract_ty_arith [variable, in Chapter7.expressions]
ty_arith [inductive, in Chapter7.expressions]
ty_arith.ty [variable, in Chapter7.expressions]
ty_arith [section, in Chapter7.expressions]
ty_bool.retract_ty_bool [variable, in Chapter7.expressions]
ty_bool [inductive, in Chapter7.expressions]
ty_bool.ty [variable, in Chapter7.expressions]
ty_bool [section, in Chapter7.expressions]
ty_lam.retract_ty_lam [variable, in Chapter7.expressions]
ty_lam [inductive, in Chapter7.expressions]
ty_lam.ty [variable, in Chapter7.expressions]
ty_lam [section, in Chapter7.expressions]
ty_inv_tabs [lemma, in Chapter10.POPLMark22]
ty_subst [lemma, in Chapter10.POPLMark22]
ty_inv_rec [lemma, in Chapter10.POPLMark22]
ty_inv_abs [lemma, in Chapter10.POPLMark22]
ty_rec [lemma, in Chapter10.POPLMark22]
ty_app [constructor, in Chapter9.preservation]
ty_abs [constructor, in Chapter9.preservation]
ty_var_tm [constructor, in Chapter9.preservation]
ty_features [instance, in Chapter9.sn_mod]
ty_var' [lemma, in Chapter9.variadic_preservation]
ty_app [constructor, in Chapter9.variadic_preservation]
ty_abs [constructor, in Chapter9.variadic_preservation]
ty_var [constructor, in Chapter9.variadic_preservation]
ty_inv_tabs [lemma, in Chapter10.POPLMark21]
ty_subst [lemma, in Chapter10.POPLMark21]
ty_inv_rec [lemma, in Chapter10.POPLMark21]
ty_inv_abs [lemma, in Chapter10.POPLMark21]
ty_rec [lemma, in Chapter10.POPLMark21]
ty_inv_tabs [lemma, in Chapter10.POPLMark1]
ty_subst [lemma, in Chapter10.POPLMark1]
ty_inv_abs [lemma, in Chapter10.POPLMark1]
T_Var' [lemma, in Chapter10.POPLMark22]
T_Sub [constructor, in Chapter10.POPLMark22]
T_Proj [constructor, in Chapter10.POPLMark22]
T_Rcd [constructor, in Chapter10.POPLMark22]
T_Tapp [constructor, in Chapter10.POPLMark22]
T_tabs [constructor, in Chapter10.POPLMark22]
T_app [constructor, in Chapter10.POPLMark22]
T_abs [constructor, in Chapter10.POPLMark22]
T_Var [constructor, in Chapter10.POPLMark22]
T_Var' [lemma, in Chapter10.POPLMark21]
T_Sub [constructor, in Chapter10.POPLMark21]
T_Proj [constructor, in Chapter10.POPLMark21]
T_Rcd [constructor, in Chapter10.POPLMark21]
T_Tapp [constructor, in Chapter10.POPLMark21]
T_tabs [constructor, in Chapter10.POPLMark21]
T_app [constructor, in Chapter10.POPLMark21]
T_abs [constructor, in Chapter10.POPLMark21]
T_Var [constructor, in Chapter10.POPLMark21]
T_Sub [constructor, in Chapter10.POPLMark1]
T_Tapp [constructor, in Chapter10.POPLMark1]
T_tabs [constructor, in Chapter10.POPLMark1]
T_app [constructor, in Chapter10.POPLMark1]
T_abs [constructor, in Chapter10.POPLMark1]
T_Var [constructor, in Chapter10.POPLMark1]
U
ucons [constructor, in Chapter10.POPLMark22]ucons [constructor, in Chapter10.POPLMark21]
uexp [inductive, in Chapter4.termination]
unil [constructor, in Chapter10.POPLMark22]
unil [constructor, in Chapter10.POPLMark21]
unique [inductive, in Chapter10.POPLMark22]
unique [inductive, in Chapter10.POPLMark21]
unique_update [lemma, in Chapter10.POPLMark22]
unique_spec [lemma, in Chapter10.POPLMark22]
unique_map [lemma, in Chapter10.POPLMark22]
unique_update [lemma, in Chapter10.POPLMark21]
unique_spec [lemma, in Chapter10.POPLMark21]
unique_map [lemma, in Chapter10.POPLMark21]
unscoped [library]
update [definition, in Chapter10.POPLMark22]
update [definition, in Chapter10.POPLMark21]
update_char [lemma, in Chapter10.POPLMark22]
update_char [lemma, in Chapter10.POPLMark21]
upExtRen_list_tm_tm [definition, in Chapter3.utlc_scoped]
upExtRen_tm_tm [definition, in Chapter3.utlc_scoped]
upExtRen_list_tm_tm [definition, in Chapter6.variadic_list]
upExtRen_tm_tm [definition, in Chapter6.variadic_list]
upExtRen_exp_exp [definition, in Chapter7.expressions]
upExtRen_list_tm_tm [definition, in Chapter6.variadic_fin]
upExtRen_tm_tm [definition, in Chapter6.variadic_fin]
upExtRen_list_vl_vl [definition, in Chapter6.sysf_cbv]
upExtRen_list_vl_ty [definition, in Chapter6.sysf_cbv]
upExtRen_list_ty_vl [definition, in Chapter6.sysf_cbv]
upExtRen_vl_vl [definition, in Chapter6.sysf_cbv]
upExtRen_vl_ty [definition, in Chapter6.sysf_cbv]
upExtRen_ty_vl [definition, in Chapter6.sysf_cbv]
upExtRen_list_ty_ty [definition, in Chapter6.sysf_cbv]
upExtRen_ty_ty [definition, in Chapter6.sysf_cbv]
upExtRen_list_tm_tm [definition, in Chapter9.stlc]
upExtRen_tm_tm [definition, in Chapter9.stlc]
upExtRen_list_tm_tm [definition, in Chapter6.utlc_pairs]
upExtRen_tm_tm [definition, in Chapter6.utlc_pairs]
upExtRen_tm_tm [definition, in Chapter3.utlc_pure]
upExtRen_list_tm_tm [definition, in Chapter10.sysf]
upExtRen_list_tm_ty [definition, in Chapter10.sysf]
upExtRen_list_ty_tm [definition, in Chapter10.sysf]
upExtRen_tm_tm [definition, in Chapter10.sysf]
upExtRen_tm_ty [definition, in Chapter10.sysf]
upExtRen_ty_tm [definition, in Chapter10.sysf]
upExtRen_list_ty_ty [definition, in Chapter10.sysf]
upExtRen_ty_ty [definition, in Chapter10.sysf]
upExtRen_chan_chan [definition, in Chapter6.picalculus]
upExtRen_list_ty_ty [definition, in Chapter6.recty]
upExtRen_ty_ty [definition, in Chapter6.recty]
upExtRen_list_tm_tm [definition, in Chapter10.sysf_pat]
upExtRen_list_tm_ty [definition, in Chapter10.sysf_pat]
upExtRen_list_ty_tm [definition, in Chapter10.sysf_pat]
upExtRen_tm_tm [definition, in Chapter10.sysf_pat]
upExtRen_tm_ty [definition, in Chapter10.sysf_pat]
upExtRen_ty_tm [definition, in Chapter10.sysf_pat]
upExtRen_list_ty_ty [definition, in Chapter10.sysf_pat]
upExtRen_ty_ty [definition, in Chapter10.sysf_pat]
upExt_list_tm_tm [definition, in Chapter3.utlc_scoped]
upExt_tm_tm [definition, in Chapter3.utlc_scoped]
upExt_list_tm_tm [definition, in Chapter6.variadic_list]
upExt_tm_tm [definition, in Chapter6.variadic_list]
upExt_exp_exp [definition, in Chapter7.expressions]
upExt_list_tm_tm [definition, in Chapter6.variadic_fin]
upExt_tm_tm [definition, in Chapter6.variadic_fin]
upExt_list_vl_vl [definition, in Chapter6.sysf_cbv]
upExt_list_vl_ty [definition, in Chapter6.sysf_cbv]
upExt_list_ty_vl [definition, in Chapter6.sysf_cbv]
upExt_vl_vl [definition, in Chapter6.sysf_cbv]
upExt_vl_ty [definition, in Chapter6.sysf_cbv]
upExt_ty_vl [definition, in Chapter6.sysf_cbv]
upExt_list_ty_ty [definition, in Chapter6.sysf_cbv]
upExt_ty_ty [definition, in Chapter6.sysf_cbv]
upExt_list_tm_tm [definition, in Chapter9.stlc]
upExt_tm_tm [definition, in Chapter9.stlc]
upExt_list_tm_tm [definition, in Chapter6.utlc_pairs]
upExt_tm_tm [definition, in Chapter6.utlc_pairs]
upExt_list_tm_tm [definition, in Chapter6.fol]
upExt_tm_tm [definition, in Chapter6.fol]
upExt_tm_tm [definition, in Chapter3.utlc_pure]
upExt_list_tm_tm [definition, in Chapter10.sysf]
upExt_list_tm_ty [definition, in Chapter10.sysf]
upExt_list_ty_tm [definition, in Chapter10.sysf]
upExt_tm_tm [definition, in Chapter10.sysf]
upExt_tm_ty [definition, in Chapter10.sysf]
upExt_ty_tm [definition, in Chapter10.sysf]
upExt_list_ty_ty [definition, in Chapter10.sysf]
upExt_ty_ty [definition, in Chapter10.sysf]
upExt_list_ty_ty [definition, in Chapter6.recty]
upExt_ty_ty [definition, in Chapter6.recty]
upExt_list_tm_tm [definition, in Chapter10.sysf_pat]
upExt_list_tm_ty [definition, in Chapter10.sysf_pat]
upExt_list_ty_tm [definition, in Chapter10.sysf_pat]
upExt_tm_tm [definition, in Chapter10.sysf_pat]
upExt_tm_ty [definition, in Chapter10.sysf_pat]
upExt_ty_tm [definition, in Chapter10.sysf_pat]
upExt_list_ty_ty [definition, in Chapter10.sysf_pat]
upExt_ty_ty [definition, in Chapter10.sysf_pat]
upIdList_tm_tm [definition, in Chapter3.utlc_scoped]
upIdList_tm_tm [definition, in Chapter6.variadic_list]
upIdList_tm_tm [definition, in Chapter6.variadic_fin]
upIdList_vl_vl [definition, in Chapter6.sysf_cbv]
upIdList_vl_ty [definition, in Chapter6.sysf_cbv]
upIdList_ty_vl [definition, in Chapter6.sysf_cbv]
upIdList_ty_ty [definition, in Chapter6.sysf_cbv]
upIdList_tm_tm [definition, in Chapter9.stlc]
upIdList_tm_tm [definition, in Chapter6.utlc_pairs]
upIdList_tm_tm [definition, in Chapter6.fol]
upIdList_tm_tm [definition, in Chapter10.sysf]
upIdList_tm_ty [definition, in Chapter10.sysf]
upIdList_ty_tm [definition, in Chapter10.sysf]
upIdList_ty_ty [definition, in Chapter10.sysf]
upIdList_ty_ty [definition, in Chapter6.recty]
upIdList_tm_tm [definition, in Chapter10.sysf_pat]
upIdList_tm_ty [definition, in Chapter10.sysf_pat]
upIdList_ty_tm [definition, in Chapter10.sysf_pat]
upIdList_ty_ty [definition, in Chapter10.sysf_pat]
upId_tm_tm [definition, in Chapter3.utlc_scoped]
upId_tm_tm [definition, in Chapter6.variadic_list]
upId_exp_exp [definition, in Chapter7.expressions]
upId_tm_tm [definition, in Chapter6.variadic_fin]
upId_vl_vl [definition, in Chapter6.sysf_cbv]
upId_vl_ty [definition, in Chapter6.sysf_cbv]
upId_ty_vl [definition, in Chapter6.sysf_cbv]
upId_ty_ty [definition, in Chapter6.sysf_cbv]
upId_tm_tm [definition, in Chapter9.stlc]
upId_tm_tm [definition, in Chapter6.utlc_pairs]
upId_tm_tm [definition, in Chapter6.fol]
upId_tm_tm [definition, in Chapter3.utlc_pure]
upId_tm_tm [definition, in Chapter10.sysf]
upId_tm_ty [definition, in Chapter10.sysf]
upId_ty_tm [definition, in Chapter10.sysf]
upId_ty_ty [definition, in Chapter10.sysf]
upId_ty_ty [definition, in Chapter6.recty]
upId_tm_tm [definition, in Chapter10.sysf_pat]
upId_tm_ty [definition, in Chapter10.sysf_pat]
upId_ty_tm [definition, in Chapter10.sysf_pat]
upId_ty_ty [definition, in Chapter10.sysf_pat]
upList_tm_tm [definition, in Chapter3.utlc_scoped]
upList_tm_tm [definition, in Chapter6.variadic_list]
upList_tm_tm [definition, in Chapter6.variadic_fin]
upList_vl_vl [definition, in Chapter6.sysf_cbv]
upList_vl_ty [definition, in Chapter6.sysf_cbv]
upList_ty_vl [definition, in Chapter6.sysf_cbv]
upList_ty_ty [definition, in Chapter6.sysf_cbv]
upList_tm_tm [definition, in Chapter9.stlc]
upList_tm_tm [definition, in Chapter6.utlc_pairs]
upList_tm_tm [definition, in Chapter6.fol]
upList_tm_tm [definition, in Chapter10.sysf]
upList_tm_ty [definition, in Chapter10.sysf]
upList_ty_tm [definition, in Chapter10.sysf]
upList_ty_ty [definition, in Chapter10.sysf]
upList_ty_ty [definition, in Chapter6.recty]
upList_tm_tm [definition, in Chapter10.sysf_pat]
upList_tm_ty [definition, in Chapter10.sysf_pat]
upList_ty_tm [definition, in Chapter10.sysf_pat]
upList_ty_ty [definition, in Chapter10.sysf_pat]
upRenList_tm_tm [definition, in Chapter3.utlc_scoped]
upRenList_tm_tm [definition, in Chapter6.variadic_list]
upRenList_tm_tm [definition, in Chapter6.variadic_fin]
upRenList_vl_vl [definition, in Chapter6.sysf_cbv]
upRenList_vl_ty [definition, in Chapter6.sysf_cbv]
upRenList_ty_vl [definition, in Chapter6.sysf_cbv]
upRenList_ty_ty [definition, in Chapter6.sysf_cbv]
upRenList_tm_tm [definition, in Chapter9.stlc]
upRenList_tm_tm [definition, in Chapter6.utlc_pairs]
upRenList_tm_tm [definition, in Chapter10.sysf]
upRenList_tm_ty [definition, in Chapter10.sysf]
upRenList_ty_tm [definition, in Chapter10.sysf]
upRenList_ty_ty [definition, in Chapter10.sysf]
upRenList_ty_ty [definition, in Chapter6.recty]
upRenList_tm_tm [definition, in Chapter10.sysf_pat]
upRenList_tm_ty [definition, in Chapter10.sysf_pat]
upRenList_ty_tm [definition, in Chapter10.sysf_pat]
upRenList_ty_ty [definition, in Chapter10.sysf_pat]
upRen_tm_tm [definition, in Chapter3.utlc_scoped]
upRen_tm_tm [definition, in Chapter6.variadic_list]
upRen_exp_exp [definition, in Chapter7.expressions]
upRen_tm_tm [definition, in Chapter6.variadic_fin]
upRen_vl_vl [definition, in Chapter6.sysf_cbv]
upRen_vl_ty [definition, in Chapter6.sysf_cbv]
upRen_ty_vl [definition, in Chapter6.sysf_cbv]
upRen_ty_ty [definition, in Chapter6.sysf_cbv]
upRen_tm_tm [definition, in Chapter9.stlc]
upRen_p [definition, in fintype]
upRen_p [definition, in fintype_variadic]
upRen_tm_tm [definition, in Chapter6.utlc_pairs]
upRen_tm_tm [definition, in Chapter3.utlc_pure]
upRen_tm_tm [definition, in Chapter10.sysf]
upRen_tm_ty [definition, in Chapter10.sysf]
upRen_ty_tm [definition, in Chapter10.sysf]
upRen_ty_ty [definition, in Chapter10.sysf]
upRen_chan_chan [definition, in Chapter6.picalculus]
upRen_ty_ty [definition, in Chapter6.recty]
upRen_tm_tm [definition, in Chapter10.sysf_pat]
upRen_tm_ty [definition, in Chapter10.sysf_pat]
upRen_ty_tm [definition, in Chapter10.sysf_pat]
upRen_ty_ty [definition, in Chapter10.sysf_pat]
up_ren_ren [lemma, in unscoped]
up_ren [definition, in unscoped]
Up_tm_tm [instance, in Chapter3.utlc_scoped]
up_tm [projection, in Chapter3.utlc_scoped]
Up_tm [record, in Chapter3.utlc_scoped]
up_tm [constructor, in Chapter3.utlc_scoped]
Up_tm [inductive, in Chapter3.utlc_scoped]
up_subst_subst_list_tm_tm [definition, in Chapter3.utlc_scoped]
up_subst_subst_tm_tm [definition, in Chapter3.utlc_scoped]
up_subst_ren_list_tm_tm [definition, in Chapter3.utlc_scoped]
up_subst_ren_tm_tm [definition, in Chapter3.utlc_scoped]
up_ren_subst_list_tm_tm [definition, in Chapter3.utlc_scoped]
up_ren_subst_tm_tm [definition, in Chapter3.utlc_scoped]
up_ren_ren_list_tm_tm [definition, in Chapter3.utlc_scoped]
up_ren_ren_tm_tm [definition, in Chapter3.utlc_scoped]
up_tm_tm [definition, in Chapter3.utlc_scoped]
Up_tm_tm [instance, in Chapter6.variadic_list]
up_tm [projection, in Chapter6.variadic_list]
Up_tm [record, in Chapter6.variadic_list]
up_tm [constructor, in Chapter6.variadic_list]
Up_tm [inductive, in Chapter6.variadic_list]
up_subst_subst_list_tm_tm [definition, in Chapter6.variadic_list]
up_subst_subst_tm_tm [definition, in Chapter6.variadic_list]
up_subst_ren_list_tm_tm [definition, in Chapter6.variadic_list]
up_subst_ren_tm_tm [definition, in Chapter6.variadic_list]
up_ren_subst_list_tm_tm [definition, in Chapter6.variadic_list]
up_ren_subst_tm_tm [definition, in Chapter6.variadic_list]
up_ren_ren_list_tm_tm [definition, in Chapter6.variadic_list]
up_ren_ren_tm_tm [definition, in Chapter6.variadic_list]
up_tm_tm [definition, in Chapter6.variadic_list]
Up_exp_exp [instance, in Chapter7.expressions]
up_exp [projection, in Chapter7.expressions]
Up_exp [record, in Chapter7.expressions]
up_exp [constructor, in Chapter7.expressions]
Up_exp [inductive, in Chapter7.expressions]
up_subst_subst_exp_exp [definition, in Chapter7.expressions]
up_subst_ren_exp_exp [definition, in Chapter7.expressions]
up_ren_subst_exp_exp [definition, in Chapter7.expressions]
up_ren_ren_exp_exp [definition, in Chapter7.expressions]
up_exp_exp [definition, in Chapter7.expressions]
Up_tm_tm [instance, in Chapter6.variadic_fin]
up_tm [projection, in Chapter6.variadic_fin]
Up_tm [record, in Chapter6.variadic_fin]
up_tm [constructor, in Chapter6.variadic_fin]
Up_tm [inductive, in Chapter6.variadic_fin]
up_subst_subst_list_tm_tm [definition, in Chapter6.variadic_fin]
up_subst_subst_tm_tm [definition, in Chapter6.variadic_fin]
up_subst_ren_list_tm_tm [definition, in Chapter6.variadic_fin]
up_subst_ren_tm_tm [definition, in Chapter6.variadic_fin]
up_ren_subst_list_tm_tm [definition, in Chapter6.variadic_fin]
up_ren_subst_tm_tm [definition, in Chapter6.variadic_fin]
up_ren_ren_list_tm_tm [definition, in Chapter6.variadic_fin]
up_ren_ren_tm_tm [definition, in Chapter6.variadic_fin]
up_tm_tm [definition, in Chapter6.variadic_fin]
Up_vl_vl [instance, in Chapter6.sysf_cbv]
Up_vl_ty [instance, in Chapter6.sysf_cbv]
Up_ty_vl [instance, in Chapter6.sysf_cbv]
Up_ty_ty [instance, in Chapter6.sysf_cbv]
up_vl [projection, in Chapter6.sysf_cbv]
Up_vl [record, in Chapter6.sysf_cbv]
up_vl [constructor, in Chapter6.sysf_cbv]
Up_vl [inductive, in Chapter6.sysf_cbv]
up_ty [projection, in Chapter6.sysf_cbv]
Up_ty [record, in Chapter6.sysf_cbv]
up_ty [constructor, in Chapter6.sysf_cbv]
Up_ty [inductive, in Chapter6.sysf_cbv]
up_subst_subst_list_vl_vl [definition, in Chapter6.sysf_cbv]
up_subst_subst_list_vl_ty [definition, in Chapter6.sysf_cbv]
up_subst_subst_list_ty_vl [definition, in Chapter6.sysf_cbv]
up_subst_subst_vl_vl [definition, in Chapter6.sysf_cbv]
up_subst_subst_vl_ty [definition, in Chapter6.sysf_cbv]
up_subst_subst_ty_vl [definition, in Chapter6.sysf_cbv]
up_subst_ren_list_vl_vl [definition, in Chapter6.sysf_cbv]
up_subst_ren_list_vl_ty [definition, in Chapter6.sysf_cbv]
up_subst_ren_list_ty_vl [definition, in Chapter6.sysf_cbv]
up_subst_ren_vl_vl [definition, in Chapter6.sysf_cbv]
up_subst_ren_vl_ty [definition, in Chapter6.sysf_cbv]
up_subst_ren_ty_vl [definition, in Chapter6.sysf_cbv]
up_ren_subst_list_vl_vl [definition, in Chapter6.sysf_cbv]
up_ren_subst_list_vl_ty [definition, in Chapter6.sysf_cbv]
up_ren_subst_list_ty_vl [definition, in Chapter6.sysf_cbv]
up_ren_subst_vl_vl [definition, in Chapter6.sysf_cbv]
up_ren_subst_vl_ty [definition, in Chapter6.sysf_cbv]
up_ren_subst_ty_vl [definition, in Chapter6.sysf_cbv]
up_ren_ren_list_vl_vl [definition, in Chapter6.sysf_cbv]
up_ren_ren_list_vl_ty [definition, in Chapter6.sysf_cbv]
up_ren_ren_list_ty_vl [definition, in Chapter6.sysf_cbv]
up_ren_ren_vl_vl [definition, in Chapter6.sysf_cbv]
up_ren_ren_vl_ty [definition, in Chapter6.sysf_cbv]
up_ren_ren_ty_vl [definition, in Chapter6.sysf_cbv]
up_vl_vl [definition, in Chapter6.sysf_cbv]
up_vl_ty [definition, in Chapter6.sysf_cbv]
up_ty_vl [definition, in Chapter6.sysf_cbv]
up_subst_subst_list_ty_ty [definition, in Chapter6.sysf_cbv]
up_subst_subst_ty_ty [definition, in Chapter6.sysf_cbv]
up_subst_ren_list_ty_ty [definition, in Chapter6.sysf_cbv]
up_subst_ren_ty_ty [definition, in Chapter6.sysf_cbv]
up_ren_subst_list_ty_ty [definition, in Chapter6.sysf_cbv]
up_ren_subst_ty_ty [definition, in Chapter6.sysf_cbv]
up_ren_ren_list_ty_ty [definition, in Chapter6.sysf_cbv]
up_ren_ren_ty_ty [definition, in Chapter6.sysf_cbv]
up_ty_ty [definition, in Chapter6.sysf_cbv]
Up_tm_tm [instance, in Chapter9.stlc]
up_tm [projection, in Chapter9.stlc]
Up_tm [record, in Chapter9.stlc]
up_tm [constructor, in Chapter9.stlc]
Up_tm [inductive, in Chapter9.stlc]
up_subst_subst_list_tm_tm [definition, in Chapter9.stlc]
up_subst_subst_tm_tm [definition, in Chapter9.stlc]
up_subst_ren_list_tm_tm [definition, in Chapter9.stlc]
up_subst_ren_tm_tm [definition, in Chapter9.stlc]
up_ren_subst_list_tm_tm [definition, in Chapter9.stlc]
up_ren_subst_tm_tm [definition, in Chapter9.stlc]
up_ren_ren_list_tm_tm [definition, in Chapter9.stlc]
up_ren_ren_tm_tm [definition, in Chapter9.stlc]
up_tm_tm [definition, in Chapter9.stlc]
up_ren_ren_p [lemma, in fintype]
up_ren_ren [lemma, in fintype]
up_ren [definition, in fintype]
up_ren_ren_p [lemma, in fintype_variadic]
up_ren_ren [lemma, in fintype_variadic]
up_ren [definition, in fintype_variadic]
Up_tm_tm [instance, in Chapter6.utlc_pairs]
up_tm [projection, in Chapter6.utlc_pairs]
Up_tm [record, in Chapter6.utlc_pairs]
up_tm [constructor, in Chapter6.utlc_pairs]
Up_tm [inductive, in Chapter6.utlc_pairs]
up_subst_subst_list_tm_tm [definition, in Chapter6.utlc_pairs]
up_subst_subst_tm_tm [definition, in Chapter6.utlc_pairs]
up_subst_ren_list_tm_tm [definition, in Chapter6.utlc_pairs]
up_subst_ren_tm_tm [definition, in Chapter6.utlc_pairs]
up_ren_subst_list_tm_tm [definition, in Chapter6.utlc_pairs]
up_ren_subst_tm_tm [definition, in Chapter6.utlc_pairs]
up_ren_ren_list_tm_tm [definition, in Chapter6.utlc_pairs]
up_ren_ren_tm_tm [definition, in Chapter6.utlc_pairs]
up_tm_tm [definition, in Chapter6.utlc_pairs]
Up_tm_tm [instance, in Chapter6.fol]
up_tm [projection, in Chapter6.fol]
Up_tm [record, in Chapter6.fol]
up_tm [constructor, in Chapter6.fol]
Up_tm [inductive, in Chapter6.fol]
up_subst_subst_list_tm_tm [definition, in Chapter6.fol]
up_subst_subst_tm_tm [definition, in Chapter6.fol]
up_tm_tm [definition, in Chapter6.fol]
up_ren_ext [lemma, in Chapter9.sn_mod]
Up_tm_tm [instance, in Chapter3.utlc_pure]
up_tm [projection, in Chapter3.utlc_pure]
Up_tm [record, in Chapter3.utlc_pure]
up_tm [constructor, in Chapter3.utlc_pure]
Up_tm [inductive, in Chapter3.utlc_pure]
up_subst_subst_tm_tm [definition, in Chapter3.utlc_pure]
up_subst_ren_tm_tm [definition, in Chapter3.utlc_pure]
up_ren_subst_tm_tm [definition, in Chapter3.utlc_pure]
up_ren_ren_tm_tm [definition, in Chapter3.utlc_pure]
up_tm_tm [definition, in Chapter3.utlc_pure]
Up_tm_tm [instance, in Chapter10.sysf]
Up_tm_ty [instance, in Chapter10.sysf]
Up_ty_tm [instance, in Chapter10.sysf]
Up_ty_ty [instance, in Chapter10.sysf]
up_tm [projection, in Chapter10.sysf]
Up_tm [record, in Chapter10.sysf]
up_tm [constructor, in Chapter10.sysf]
Up_tm [inductive, in Chapter10.sysf]
up_ty [projection, in Chapter10.sysf]
Up_ty [record, in Chapter10.sysf]
up_ty [constructor, in Chapter10.sysf]
Up_ty [inductive, in Chapter10.sysf]
up_subst_subst_list_tm_tm [definition, in Chapter10.sysf]
up_subst_subst_list_tm_ty [definition, in Chapter10.sysf]
up_subst_subst_list_ty_tm [definition, in Chapter10.sysf]
up_subst_subst_tm_tm [definition, in Chapter10.sysf]
up_subst_subst_tm_ty [definition, in Chapter10.sysf]
up_subst_subst_ty_tm [definition, in Chapter10.sysf]
up_subst_ren_list_tm_tm [definition, in Chapter10.sysf]
up_subst_ren_list_tm_ty [definition, in Chapter10.sysf]
up_subst_ren_list_ty_tm [definition, in Chapter10.sysf]
up_subst_ren_tm_tm [definition, in Chapter10.sysf]
up_subst_ren_tm_ty [definition, in Chapter10.sysf]
up_subst_ren_ty_tm [definition, in Chapter10.sysf]
up_ren_subst_list_tm_tm [definition, in Chapter10.sysf]
up_ren_subst_list_tm_ty [definition, in Chapter10.sysf]
up_ren_subst_list_ty_tm [definition, in Chapter10.sysf]
up_ren_subst_tm_tm [definition, in Chapter10.sysf]
up_ren_subst_tm_ty [definition, in Chapter10.sysf]
up_ren_subst_ty_tm [definition, in Chapter10.sysf]
up_tm_tm [definition, in Chapter10.sysf]
up_tm_ty [definition, in Chapter10.sysf]
up_ty_tm [definition, in Chapter10.sysf]
up_subst_subst_list_ty_ty [definition, in Chapter10.sysf]
up_subst_subst_ty_ty [definition, in Chapter10.sysf]
up_subst_ren_list_ty_ty [definition, in Chapter10.sysf]
up_subst_ren_ty_ty [definition, in Chapter10.sysf]
up_ren_subst_list_ty_ty [definition, in Chapter10.sysf]
up_ren_subst_ty_ty [definition, in Chapter10.sysf]
up_ty_ty [definition, in Chapter10.sysf]
up_chan [projection, in Chapter6.picalculus]
Up_chan [record, in Chapter6.picalculus]
up_chan [constructor, in Chapter6.picalculus]
Up_chan [inductive, in Chapter6.picalculus]
up_ren_ren_chan_chan [definition, in Chapter6.picalculus]
Up_ty_ty [instance, in Chapter6.recty]
up_ty [projection, in Chapter6.recty]
Up_ty [record, in Chapter6.recty]
up_ty [constructor, in Chapter6.recty]
Up_ty [inductive, in Chapter6.recty]
up_subst_subst_list_ty_ty [definition, in Chapter6.recty]
up_subst_subst_ty_ty [definition, in Chapter6.recty]
up_subst_ren_list_ty_ty [definition, in Chapter6.recty]
up_subst_ren_ty_ty [definition, in Chapter6.recty]
up_ren_subst_list_ty_ty [definition, in Chapter6.recty]
up_ren_subst_ty_ty [definition, in Chapter6.recty]
up_ren_ren_list_ty_ty [definition, in Chapter6.recty]
up_ren_ren_ty_ty [definition, in Chapter6.recty]
up_ty_ty [definition, in Chapter6.recty]
Up_tm_tm [instance, in Chapter10.sysf_pat]
Up_tm_ty [instance, in Chapter10.sysf_pat]
Up_ty_tm [instance, in Chapter10.sysf_pat]
Up_ty_ty [instance, in Chapter10.sysf_pat]
up_tm [projection, in Chapter10.sysf_pat]
Up_tm [record, in Chapter10.sysf_pat]
up_tm [constructor, in Chapter10.sysf_pat]
Up_tm [inductive, in Chapter10.sysf_pat]
up_ty [projection, in Chapter10.sysf_pat]
Up_ty [record, in Chapter10.sysf_pat]
up_ty [constructor, in Chapter10.sysf_pat]
Up_ty [inductive, in Chapter10.sysf_pat]
up_subst_subst_list_tm_tm [definition, in Chapter10.sysf_pat]
up_subst_subst_list_tm_ty [definition, in Chapter10.sysf_pat]
up_subst_subst_list_ty_tm [definition, in Chapter10.sysf_pat]
up_subst_subst_tm_tm [definition, in Chapter10.sysf_pat]
up_subst_subst_tm_ty [definition, in Chapter10.sysf_pat]
up_subst_subst_ty_tm [definition, in Chapter10.sysf_pat]
up_subst_ren_list_tm_tm [definition, in Chapter10.sysf_pat]
up_subst_ren_list_tm_ty [definition, in Chapter10.sysf_pat]
up_subst_ren_list_ty_tm [definition, in Chapter10.sysf_pat]
up_subst_ren_tm_tm [definition, in Chapter10.sysf_pat]
up_subst_ren_tm_ty [definition, in Chapter10.sysf_pat]
up_subst_ren_ty_tm [definition, in Chapter10.sysf_pat]
up_ren_subst_list_tm_tm [definition, in Chapter10.sysf_pat]
up_ren_subst_list_tm_ty [definition, in Chapter10.sysf_pat]
up_ren_subst_list_ty_tm [definition, in Chapter10.sysf_pat]
up_ren_subst_tm_tm [definition, in Chapter10.sysf_pat]
up_ren_subst_tm_ty [definition, in Chapter10.sysf_pat]
up_ren_subst_ty_tm [definition, in Chapter10.sysf_pat]
up_ren_ren_list_tm_tm [definition, in Chapter10.sysf_pat]
up_ren_ren_list_tm_ty [definition, in Chapter10.sysf_pat]
up_ren_ren_list_ty_tm [definition, in Chapter10.sysf_pat]
up_ren_ren_tm_tm [definition, in Chapter10.sysf_pat]
up_ren_ren_tm_ty [definition, in Chapter10.sysf_pat]
up_ren_ren_ty_tm [definition, in Chapter10.sysf_pat]
up_tm_tm [definition, in Chapter10.sysf_pat]
up_tm_ty [definition, in Chapter10.sysf_pat]
up_ty_tm [definition, in Chapter10.sysf_pat]
up_subst_subst_list_ty_ty [definition, in Chapter10.sysf_pat]
up_subst_subst_ty_ty [definition, in Chapter10.sysf_pat]
up_subst_ren_list_ty_ty [definition, in Chapter10.sysf_pat]
up_subst_ren_ty_ty [definition, in Chapter10.sysf_pat]
up_ren_subst_list_ty_ty [definition, in Chapter10.sysf_pat]
up_ren_subst_ty_ty [definition, in Chapter10.sysf_pat]
up_ren_ren_list_ty_ty [definition, in Chapter10.sysf_pat]
up_ren_ren_ty_ty [definition, in Chapter10.sysf_pat]
up_ty_ty [definition, in Chapter10.sysf_pat]
uquivAssoc [constructor, in Chapter4.termination]
uquivCompL [constructor, in Chapter4.termination]
uquivCompPair [constructor, in Chapter4.termination]
uquivCompR [constructor, in Chapter4.termination]
uquivLambda [constructor, in Chapter4.termination]
uquivLamC [constructor, in Chapter4.termination]
uquivPairL [constructor, in Chapter4.termination]
uquivPairR [constructor, in Chapter4.termination]
uquivSubCompL [constructor, in Chapter4.termination]
uquivSubCompR [constructor, in Chapter4.termination]
uquivSubLam [constructor, in Chapter4.termination]
uquivSubPairL [constructor, in Chapter4.termination]
uquivSubPairR [constructor, in Chapter4.termination]
uquiv_plus_compR [lemma, in Chapter4.termination]
uquiv_plus_compL [lemma, in Chapter4.termination]
uquiv_plus_pairR [lemma, in Chapter4.termination]
uquiv_plus_pairL [lemma, in Chapter4.termination]
uquiv_plus_lam [lemma, in Chapter4.termination]
uquiv_star_compR [lemma, in Chapter4.termination]
uquiv_star_compL [lemma, in Chapter4.termination]
uquiv_star_pairR [lemma, in Chapter4.termination]
uquiv_star_pairL [lemma, in Chapter4.termination]
uquiv_star_lam [lemma, in Chapter4.termination]
utlc_pairs [library]
utlc_scoped [library]
utlc_pure [library]
V
value [inductive, in Chapter10.POPLMark22]value [definition, in Chapter9.reduction]
value [inductive, in Chapter10.POPLMark21]
value [inductive, in Chapter10.POPLMark1]
Value_rec [constructor, in Chapter10.POPLMark22]
Value_tabs [constructor, in Chapter10.POPLMark22]
Value_abs [constructor, in Chapter10.POPLMark22]
value_anti_renaming_lam [lemma, in Chapter9.sn]
value_anti [lemma, in Chapter9.reduction]
Value_rec [constructor, in Chapter10.POPLMark21]
Value_tabs [constructor, in Chapter10.POPLMark21]
Value_abs [constructor, in Chapter10.POPLMark21]
Value_tabs [constructor, in Chapter10.POPLMark1]
Value_abs [constructor, in Chapter10.POPLMark1]
val_inclusion [lemma, in Chapter9.sn_var]
val_inclusion [lemma, in Chapter9.wn]
Var [record, in unscoped]
Var [inductive, in unscoped]
Var [record, in fintype]
Var [inductive, in fintype]
Var [record, in fintype_variadic]
Var [inductive, in fintype_variadic]
variadic_preservation [library]
variadic_fin [library]
variadic_list [library]
VarInstance_tm [instance, in Chapter3.utlc_scoped]
VarInstance_tm [instance, in Chapter6.variadic_list]
VarInstance_exp_var [instance, in Chapter7.expressions]
VarInstance_tm [instance, in Chapter6.variadic_fin]
VarInstance_vl [instance, in Chapter6.sysf_cbv]
VarInstance_ty [instance, in Chapter6.sysf_cbv]
VarInstance_tm [instance, in Chapter9.stlc]
VarInstance_tm [instance, in Chapter6.utlc_pairs]
VarInstance_tm [instance, in Chapter6.fol]
VarInstance_tm [instance, in Chapter3.utlc_pure]
VarInstance_tm [instance, in Chapter10.sysf]
VarInstance_ty [instance, in Chapter10.sysf]
VarInstance_chan [instance, in Chapter6.picalculus]
VarInstance_ty [instance, in Chapter6.recty]
VarInstance_tm [instance, in Chapter10.sysf_pat]
VarInstance_ty [instance, in Chapter10.sysf_pat]
varLRen_tm [lemma, in Chapter3.utlc_scoped]
varLRen_tm [lemma, in Chapter6.variadic_list]
varLRen_exp_var [lemma, in Chapter7.expressions]
varLRen_tm [lemma, in Chapter6.variadic_fin]
varLRen_vl [lemma, in Chapter6.sysf_cbv]
varLRen_ty [lemma, in Chapter6.sysf_cbv]
varLRen_tm [lemma, in Chapter9.stlc]
varLRen_tm [lemma, in Chapter6.utlc_pairs]
varLRen_tm [lemma, in Chapter3.utlc_pure]
varLRen_tm [lemma, in Chapter10.sysf]
varLRen_ty [lemma, in Chapter10.sysf]
varLRen_chan [lemma, in Chapter6.picalculus]
varLRen_ty [lemma, in Chapter6.recty]
varLRen_tm [lemma, in Chapter10.sysf_pat]
varLRen_ty [lemma, in Chapter10.sysf_pat]
varL_tm [lemma, in Chapter3.utlc_scoped]
varL_tm [lemma, in Chapter6.variadic_list]
varL_exp_var [lemma, in Chapter7.expressions]
varL_tm [lemma, in Chapter6.variadic_fin]
varL_vl [lemma, in Chapter6.sysf_cbv]
varL_ty [lemma, in Chapter6.sysf_cbv]
varL_tm [lemma, in Chapter9.stlc]
varL_tm [lemma, in Chapter6.utlc_pairs]
varL_tm [lemma, in Chapter6.fol]
varL_exp [lemma, in Chapter9.sn_lam]
varL_tm [lemma, in Chapter3.utlc_pure]
varL_tm [lemma, in Chapter10.sysf]
varL_ty [lemma, in Chapter10.sysf]
varL_ty [lemma, in Chapter6.recty]
varL_tm [lemma, in Chapter10.sysf_pat]
varL_ty [lemma, in Chapter10.sysf_pat]
var_zero [definition, in unscoped]
var_tm [constructor, in Chapter3.utlc_scoped]
var_tm [constructor, in Chapter6.variadic_list]
var_exp [definition, in Chapter7.expressions]
var_exp_var [constructor, in Chapter7.expressions]
var_tm [constructor, in Chapter6.variadic_fin]
var_vl [constructor, in Chapter6.sysf_cbv]
var_ty [constructor, in Chapter6.sysf_cbv]
var_tm [constructor, in Chapter9.stlc]
var_has_ty [constructor, in Chapter9.sn_var]
var_zero [definition, in fintype]
var_zero [definition, in fintype_variadic]
var_tm [constructor, in Chapter6.utlc_pairs]
var_tm [constructor, in Chapter6.fol]
var_tm [constructor, in Chapter3.utlc_pure]
var_tm [constructor, in Chapter10.sysf]
var_ty [constructor, in Chapter10.sysf]
var_chan [constructor, in Chapter6.picalculus]
var_ty [constructor, in Chapter6.recty]
var_subst [constructor, in Chapter4.sigmacalculus]
var_exp [constructor, in Chapter4.sigmacalculus]
var_tm [constructor, in Chapter10.sysf_pat]
var_ty [constructor, in Chapter10.sysf_pat]
vl [inductive, in Chapter6.sysf_cbv]
vt [constructor, in Chapter6.sysf_cbv]
vt [constructor, in Chapter10.sysf]
W
whnf [definition, in Chapter9.sn_mod]whnf_anti_renaming_var [lemma, in Chapter9.sn_var]
whnf_anti_renaming_lam [lemma, in Chapter9.sn_lam]
whnf_anti_renaming_bool [lemma, in Chapter9.sn_bool]
whnf_anti_renaming_arith [lemma, in Chapter9.sn_arith]
whr [inductive, in Chapter9.equivalence]
whrapp [constructor, in Chapter9.equivalence]
whr_ren [lemma, in Chapter9.equivalence]
wn [lemma, in Chapter9.sn_mod]
wn [library]
wn_fundamental_var [lemma, in Chapter9.sn_var]
wn_fundamental_lam [lemma, in Chapter9.wn]
Z
zero [constructor, in Chapter4.termination]Zero [constructor, in Chapter4.sigmacalculus]
ZeroRen [constructor, in Chapter4.termination]
zero_p [definition, in fintype]
zero_p [definition, in fintype_variadic]
other
[ _ ] (fscope) [notation, in Chapter3.utlc_scoped][ _ ] (fscope) [notation, in Chapter6.variadic_list]
[ _ ] (fscope) [notation, in Chapter7.expressions]
[ _ ] (fscope) [notation, in Chapter7.expressions]
[ _ ] (fscope) [notation, in Chapter7.expressions]
[ _ ] (fscope) [notation, in Chapter7.expressions]
[ _ ] (fscope) [notation, in Chapter7.expressions]
[ _ ] (fscope) [notation, in Chapter6.variadic_fin]
[ _ ; _ ] (fscope) [notation, in Chapter6.sysf_cbv]
[ _ ; _ ] (fscope) [notation, in Chapter6.sysf_cbv]
[ _ ] (fscope) [notation, in Chapter6.sysf_cbv]
[ _ ] (fscope) [notation, in Chapter9.stlc]
[ _ ] (fscope) [notation, in Chapter6.utlc_pairs]
[ _ ] (fscope) [notation, in Chapter6.fol]
[ _ ] (fscope) [notation, in Chapter6.fol]
[ _ ] (fscope) [notation, in Chapter3.utlc_pure]
[ _ ; _ ] (fscope) [notation, in Chapter10.sysf]
[ _ ] (fscope) [notation, in Chapter10.sysf]
[ _ ] (fscope) [notation, in Chapter6.recty]
[ _ ; _ ] (fscope) [notation, in Chapter10.sysf_pat]
[ _ ] (fscope) [notation, in Chapter10.sysf_pat]
[ _ ] (fscope) [notation, in Chapter10.sysf_pat]
⟨ _ ; _ ⟩ (fscope) [notation, in unscoped]
⟨ _ ⟩ (fscope) [notation, in unscoped]
⟨ _ ⟩ (fscope) [notation, in Chapter3.utlc_scoped]
⟨ _ ⟩ (fscope) [notation, in Chapter6.variadic_list]
⟨ _ ⟩ (fscope) [notation, in Chapter7.expressions]
⟨ _ ⟩ (fscope) [notation, in Chapter7.expressions]
⟨ _ ⟩ (fscope) [notation, in Chapter7.expressions]
⟨ _ ⟩ (fscope) [notation, in Chapter7.expressions]
⟨ _ ⟩ (fscope) [notation, in Chapter7.expressions]
⟨ _ ⟩ (fscope) [notation, in Chapter6.variadic_fin]
⟨ _ ; _ ⟩ (fscope) [notation, in Chapter6.sysf_cbv]
⟨ _ ; _ ⟩ (fscope) [notation, in Chapter6.sysf_cbv]
⟨ _ ⟩ (fscope) [notation, in Chapter6.sysf_cbv]
⟨ _ ⟩ (fscope) [notation, in Chapter9.stlc]
⟨ _ ; _ ⟩ (fscope) [notation, in fintype]
⟨ _ ⟩ (fscope) [notation, in fintype]
⟨ _ ; _ ⟩ (fscope) [notation, in fintype_variadic]
⟨ _ ⟩ (fscope) [notation, in fintype_variadic]
⟨ _ ⟩ (fscope) [notation, in Chapter6.utlc_pairs]
⟨ _ ⟩ (fscope) [notation, in Chapter3.utlc_pure]
⟨ _ ; _ ⟩ (fscope) [notation, in Chapter10.sysf]
⟨ _ ⟩ (fscope) [notation, in Chapter10.sysf]
⟨ _ ⟩ (fscope) [notation, in Chapter6.picalculus]
⟨ _ ⟩ (fscope) [notation, in Chapter6.picalculus]
⟨ _ ⟩ (fscope) [notation, in Chapter6.recty]
⟨ _ ; _ ⟩ (fscope) [notation, in Chapter10.sysf_pat]
⟨ _ ⟩ (fscope) [notation, in Chapter10.sysf_pat]
⟨ _ ⟩ (fscope) [notation, in Chapter10.sysf_pat]
[~ _ ; _ ; .. ; _ ~] (list_scope) [notation, in header_metacoq]
[~ _ ~] (list_scope) [notation, in header_metacoq]
_ .. (subst_scope) [notation, in unscoped]
_ , _ (subst_scope) [notation, in unscoped]
_ >> _ (subst_scope) [notation, in unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in unscoped]
_ [ _ ] (subst_scope) [notation, in unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter3.utlc_scoped]
_ [ _ ] (subst_scope) [notation, in Chapter3.utlc_scoped]
↑__tm (subst_scope) [notation, in Chapter3.utlc_scoped]
↑__tm (subst_scope) [notation, in Chapter3.utlc_scoped]
var (subst_scope) [notation, in Chapter3.utlc_scoped]
_ __tm (subst_scope) [notation, in Chapter3.utlc_scoped]
_ __tm (subst_scope) [notation, in Chapter3.utlc_scoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter6.variadic_list]
_ [ _ ] (subst_scope) [notation, in Chapter6.variadic_list]
↑__tm (subst_scope) [notation, in Chapter6.variadic_list]
↑__tm (subst_scope) [notation, in Chapter6.variadic_list]
var (subst_scope) [notation, in Chapter6.variadic_list]
_ __tm (subst_scope) [notation, in Chapter6.variadic_list]
_ __tm (subst_scope) [notation, in Chapter6.variadic_list]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter7.expressions]
_ [ _ ] (subst_scope) [notation, in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter7.expressions]
_ [ _ ] (subst_scope) [notation, in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter7.expressions]
_ [ _ ] (subst_scope) [notation, in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter7.expressions]
_ [ _ ] (subst_scope) [notation, in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter7.expressions]
_ [ _ ] (subst_scope) [notation, in Chapter7.expressions]
↑__exp (subst_scope) [notation, in Chapter7.expressions]
↑__exp (subst_scope) [notation, in Chapter7.expressions]
var (subst_scope) [notation, in Chapter7.expressions]
_ __exp_var (subst_scope) [notation, in Chapter7.expressions]
_ __exp_var (subst_scope) [notation, in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter6.variadic_fin]
_ [ _ ] (subst_scope) [notation, in Chapter6.variadic_fin]
↑__tm (subst_scope) [notation, in Chapter6.variadic_fin]
↑__tm (subst_scope) [notation, in Chapter6.variadic_fin]
var (subst_scope) [notation, in Chapter6.variadic_fin]
_ __tm (subst_scope) [notation, in Chapter6.variadic_fin]
_ __tm (subst_scope) [notation, in Chapter6.variadic_fin]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Chapter6.sysf_cbv]
_ [ _ ; _ ] (subst_scope) [notation, in Chapter6.sysf_cbv]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Chapter6.sysf_cbv]
_ [ _ ; _ ] (subst_scope) [notation, in Chapter6.sysf_cbv]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter6.sysf_cbv]
_ [ _ ] (subst_scope) [notation, in Chapter6.sysf_cbv]
↑__vl (subst_scope) [notation, in Chapter6.sysf_cbv]
↑__vl (subst_scope) [notation, in Chapter6.sysf_cbv]
↑__ty (subst_scope) [notation, in Chapter6.sysf_cbv]
↑__ty (subst_scope) [notation, in Chapter6.sysf_cbv]
↑__vl (subst_scope) [notation, in Chapter6.sysf_cbv]
↑__ty (subst_scope) [notation, in Chapter6.sysf_cbv]
var (subst_scope) [notation, in Chapter6.sysf_cbv]
_ __vl (subst_scope) [notation, in Chapter6.sysf_cbv]
_ __vl (subst_scope) [notation, in Chapter6.sysf_cbv]
var (subst_scope) [notation, in Chapter6.sysf_cbv]
_ __ty (subst_scope) [notation, in Chapter6.sysf_cbv]
_ __ty (subst_scope) [notation, in Chapter6.sysf_cbv]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter9.stlc]
_ [ _ ] (subst_scope) [notation, in Chapter9.stlc]
↑__tm (subst_scope) [notation, in Chapter9.stlc]
↑__tm (subst_scope) [notation, in Chapter9.stlc]
var (subst_scope) [notation, in Chapter9.stlc]
_ __tm (subst_scope) [notation, in Chapter9.stlc]
_ __tm (subst_scope) [notation, in Chapter9.stlc]
↑ (subst_scope) [notation, in fintype]
_ .. (subst_scope) [notation, in fintype]
_ .: _ (subst_scope) [notation, in fintype]
_ [ _ ; _ ] (subst_scope) [notation, in fintype]
_ [ _ ] (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in fintype]
↑ (subst_scope) [notation, in fintype_variadic]
_ .. (subst_scope) [notation, in fintype_variadic]
_ .: _ (subst_scope) [notation, in fintype_variadic]
_ [ _ ; _ ] (subst_scope) [notation, in fintype_variadic]
_ [ _ ] (subst_scope) [notation, in fintype_variadic]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype_variadic]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype_variadic]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in fintype_variadic]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in fintype_variadic]
_ ⟨ _ ⟩ (subst_scope) [notation, in fintype_variadic]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter6.utlc_pairs]
_ [ _ ] (subst_scope) [notation, in Chapter6.utlc_pairs]
↑__tm (subst_scope) [notation, in Chapter6.utlc_pairs]
↑__tm (subst_scope) [notation, in Chapter6.utlc_pairs]
var (subst_scope) [notation, in Chapter6.utlc_pairs]
_ __tm (subst_scope) [notation, in Chapter6.utlc_pairs]
_ __tm (subst_scope) [notation, in Chapter6.utlc_pairs]
_ [ _ ] (subst_scope) [notation, in Chapter6.fol]
_ [ _ ] (subst_scope) [notation, in Chapter6.fol]
↑__tm (subst_scope) [notation, in Chapter6.fol]
↑__tm (subst_scope) [notation, in Chapter6.fol]
var (subst_scope) [notation, in Chapter6.fol]
_ __tm (subst_scope) [notation, in Chapter6.fol]
_ __tm (subst_scope) [notation, in Chapter6.fol]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter3.utlc_pure]
_ [ _ ] (subst_scope) [notation, in Chapter3.utlc_pure]
↑__tm (subst_scope) [notation, in Chapter3.utlc_pure]
↑__tm (subst_scope) [notation, in Chapter3.utlc_pure]
var (subst_scope) [notation, in Chapter3.utlc_pure]
_ __tm (subst_scope) [notation, in Chapter3.utlc_pure]
_ __tm (subst_scope) [notation, in Chapter3.utlc_pure]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Chapter10.sysf]
_ [ _ ; _ ] (subst_scope) [notation, in Chapter10.sysf]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter10.sysf]
_ [ _ ] (subst_scope) [notation, in Chapter10.sysf]
↑__tm (subst_scope) [notation, in Chapter10.sysf]
↑__tm (subst_scope) [notation, in Chapter10.sysf]
↑__ty (subst_scope) [notation, in Chapter10.sysf]
↑__ty (subst_scope) [notation, in Chapter10.sysf]
↑__tm (subst_scope) [notation, in Chapter10.sysf]
↑__ty (subst_scope) [notation, in Chapter10.sysf]
var (subst_scope) [notation, in Chapter10.sysf]
_ __tm (subst_scope) [notation, in Chapter10.sysf]
_ __tm (subst_scope) [notation, in Chapter10.sysf]
var (subst_scope) [notation, in Chapter10.sysf]
_ __ty (subst_scope) [notation, in Chapter10.sysf]
_ __ty (subst_scope) [notation, in Chapter10.sysf]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter6.picalculus]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter6.picalculus]
↑__chan (subst_scope) [notation, in Chapter6.picalculus]
var (subst_scope) [notation, in Chapter6.picalculus]
_ __chan (subst_scope) [notation, in Chapter6.picalculus]
_ __chan (subst_scope) [notation, in Chapter6.picalculus]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter6.recty]
_ [ _ ] (subst_scope) [notation, in Chapter6.recty]
↑__ty (subst_scope) [notation, in Chapter6.recty]
↑__ty (subst_scope) [notation, in Chapter6.recty]
var (subst_scope) [notation, in Chapter6.recty]
_ __ty (subst_scope) [notation, in Chapter6.recty]
_ __ty (subst_scope) [notation, in Chapter6.recty]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Chapter10.sysf_pat]
_ [ _ ; _ ] (subst_scope) [notation, in Chapter10.sysf_pat]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter10.sysf_pat]
_ [ _ ] (subst_scope) [notation, in Chapter10.sysf_pat]
_ ⟨ _ ⟩ (subst_scope) [notation, in Chapter10.sysf_pat]
_ [ _ ] (subst_scope) [notation, in Chapter10.sysf_pat]
↑__tm (subst_scope) [notation, in Chapter10.sysf_pat]
↑__tm (subst_scope) [notation, in Chapter10.sysf_pat]
↑__ty (subst_scope) [notation, in Chapter10.sysf_pat]
↑__ty (subst_scope) [notation, in Chapter10.sysf_pat]
↑__tm (subst_scope) [notation, in Chapter10.sysf_pat]
↑__ty (subst_scope) [notation, in Chapter10.sysf_pat]
var (subst_scope) [notation, in Chapter10.sysf_pat]
_ __tm (subst_scope) [notation, in Chapter10.sysf_pat]
_ __tm (subst_scope) [notation, in Chapter10.sysf_pat]
var (subst_scope) [notation, in Chapter10.sysf_pat]
_ __ty (subst_scope) [notation, in Chapter10.sysf_pat]
_ __ty (subst_scope) [notation, in Chapter10.sysf_pat]
_ .: _ [notation, in unscoped]
_ >> _ [notation, in fintype]
_ >> _ [notation, in fintype_variadic]
_ `_ _ [notation, in Chapter9.equivalence]
_ |- _ : _ [notation, in Chapter9.preservation]
_ ≡* _ [notation, in Chapter4.termination]
_ ≡+ _ [notation, in Chapter4.termination]
_ ≡ _ [notation, in Chapter4.termination]
_ ≻ _ [notation, in Chapter4.termination]
_ ⊃ _ [notation, in Chapter4.termination]
_ ⇝__s _ [notation, in Chapter4.termination]
_ ⇝__p _ [notation, in Chapter4.termination]
_ ∘ _ [notation, in Chapter4.termination]
_ |- _ : _ [notation, in Chapter9.variadic_preservation]
_ ~> _ [notation, in header_metacoq]
Compose Lemma _ on _ using _ : _ [notation, in header_metacoq]
Compose Lemma _ on _ by inversion : _ [notation, in header_metacoq]
Compose Lemma _ on _ : _ [notation, in header_metacoq]
Compose Fixpoint _ on _ : _ [notation, in header_metacoq]
EV _ => _ [notation, in Chapter10.POPLMark1]
list_map [notation, in axioms]
Modular Fixpoint _ where _ extends _ := _ [notation, in header_metacoq]
Modular Fixpoint _ where _ extends _ with _ := _ [notation, in header_metacoq]
Modular Lemma _ where _ extends _ with _ : _ [notation, in header_metacoq]
Modular Lemma _ where _ extends _ at _ with _ : _ [notation, in header_metacoq]
sn__leaf [notation, in Chapter4.termination]
sn__split [notation, in Chapter4.termination]
sn≡ [notation, in Chapter4.termination]
sn≻ [notation, in Chapter4.termination]
sn⊃ [notation, in Chapter4.termination]
SUB _ |- _ <: _ [notation, in Chapter10.POPLMark22]
SUB _ |- _ <: _ [notation, in Chapter10.POPLMark21]
SUB _ |- _ <: _ [notation, in Chapter10.POPLMark1]
TY _ ; _ |- _ : _ [notation, in Chapter10.POPLMark1]
0 [notation, in Chapter4.termination]
↑ [notation, in unscoped]
⟨ _ , _ ⟩ [notation, in Chapter4.termination]
λ _ [notation, in Chapter4.termination]
Notation Index
C
_ , _ (subst_scope) [in fintype]_ , _ (subst_scope) [in fintype_variadic]
P
EV _ => _ [in Chapter10.POPLMark22]EV _ => _ [in Chapter10.POPLMark21]
TY _ ; _ |- _ : _ [in Chapter10.POPLMark22]
TY _ ; _ |- _ : _ [in Chapter10.POPLMark21]
other
[ _ ] (fscope) [in Chapter3.utlc_scoped][ _ ] (fscope) [in Chapter6.variadic_list]
[ _ ] (fscope) [in Chapter7.expressions]
[ _ ] (fscope) [in Chapter7.expressions]
[ _ ] (fscope) [in Chapter7.expressions]
[ _ ] (fscope) [in Chapter7.expressions]
[ _ ] (fscope) [in Chapter7.expressions]
[ _ ] (fscope) [in Chapter6.variadic_fin]
[ _ ; _ ] (fscope) [in Chapter6.sysf_cbv]
[ _ ; _ ] (fscope) [in Chapter6.sysf_cbv]
[ _ ] (fscope) [in Chapter6.sysf_cbv]
[ _ ] (fscope) [in Chapter9.stlc]
[ _ ] (fscope) [in Chapter6.utlc_pairs]
[ _ ] (fscope) [in Chapter6.fol]
[ _ ] (fscope) [in Chapter6.fol]
[ _ ] (fscope) [in Chapter3.utlc_pure]
[ _ ; _ ] (fscope) [in Chapter10.sysf]
[ _ ] (fscope) [in Chapter10.sysf]
[ _ ] (fscope) [in Chapter6.recty]
[ _ ; _ ] (fscope) [in Chapter10.sysf_pat]
[ _ ] (fscope) [in Chapter10.sysf_pat]
[ _ ] (fscope) [in Chapter10.sysf_pat]
⟨ _ ; _ ⟩ (fscope) [in unscoped]
⟨ _ ⟩ (fscope) [in unscoped]
⟨ _ ⟩ (fscope) [in Chapter3.utlc_scoped]
⟨ _ ⟩ (fscope) [in Chapter6.variadic_list]
⟨ _ ⟩ (fscope) [in Chapter7.expressions]
⟨ _ ⟩ (fscope) [in Chapter7.expressions]
⟨ _ ⟩ (fscope) [in Chapter7.expressions]
⟨ _ ⟩ (fscope) [in Chapter7.expressions]
⟨ _ ⟩ (fscope) [in Chapter7.expressions]
⟨ _ ⟩ (fscope) [in Chapter6.variadic_fin]
⟨ _ ; _ ⟩ (fscope) [in Chapter6.sysf_cbv]
⟨ _ ; _ ⟩ (fscope) [in Chapter6.sysf_cbv]
⟨ _ ⟩ (fscope) [in Chapter6.sysf_cbv]
⟨ _ ⟩ (fscope) [in Chapter9.stlc]
⟨ _ ; _ ⟩ (fscope) [in fintype]
⟨ _ ⟩ (fscope) [in fintype]
⟨ _ ; _ ⟩ (fscope) [in fintype_variadic]
⟨ _ ⟩ (fscope) [in fintype_variadic]
⟨ _ ⟩ (fscope) [in Chapter6.utlc_pairs]
⟨ _ ⟩ (fscope) [in Chapter3.utlc_pure]
⟨ _ ; _ ⟩ (fscope) [in Chapter10.sysf]
⟨ _ ⟩ (fscope) [in Chapter10.sysf]
⟨ _ ⟩ (fscope) [in Chapter6.picalculus]
⟨ _ ⟩ (fscope) [in Chapter6.picalculus]
⟨ _ ⟩ (fscope) [in Chapter6.recty]
⟨ _ ; _ ⟩ (fscope) [in Chapter10.sysf_pat]
⟨ _ ⟩ (fscope) [in Chapter10.sysf_pat]
⟨ _ ⟩ (fscope) [in Chapter10.sysf_pat]
[~ _ ; _ ; .. ; _ ~] (list_scope) [in header_metacoq]
[~ _ ~] (list_scope) [in header_metacoq]
_ .. (subst_scope) [in unscoped]
_ , _ (subst_scope) [in unscoped]
_ >> _ (subst_scope) [in unscoped]
_ [ _ ; _ ] (subst_scope) [in unscoped]
_ [ _ ] (subst_scope) [in unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ⟩ (subst_scope) [in unscoped]
_ ⟨ _ ⟩ (subst_scope) [in Chapter3.utlc_scoped]
_ [ _ ] (subst_scope) [in Chapter3.utlc_scoped]
↑__tm (subst_scope) [in Chapter3.utlc_scoped]
↑__tm (subst_scope) [in Chapter3.utlc_scoped]
var (subst_scope) [in Chapter3.utlc_scoped]
_ __tm (subst_scope) [in Chapter3.utlc_scoped]
_ __tm (subst_scope) [in Chapter3.utlc_scoped]
_ ⟨ _ ⟩ (subst_scope) [in Chapter6.variadic_list]
_ [ _ ] (subst_scope) [in Chapter6.variadic_list]
↑__tm (subst_scope) [in Chapter6.variadic_list]
↑__tm (subst_scope) [in Chapter6.variadic_list]
var (subst_scope) [in Chapter6.variadic_list]
_ __tm (subst_scope) [in Chapter6.variadic_list]
_ __tm (subst_scope) [in Chapter6.variadic_list]
_ ⟨ _ ⟩ (subst_scope) [in Chapter7.expressions]
_ [ _ ] (subst_scope) [in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [in Chapter7.expressions]
_ [ _ ] (subst_scope) [in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [in Chapter7.expressions]
_ [ _ ] (subst_scope) [in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [in Chapter7.expressions]
_ [ _ ] (subst_scope) [in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [in Chapter7.expressions]
_ [ _ ] (subst_scope) [in Chapter7.expressions]
↑__exp (subst_scope) [in Chapter7.expressions]
↑__exp (subst_scope) [in Chapter7.expressions]
var (subst_scope) [in Chapter7.expressions]
_ __exp_var (subst_scope) [in Chapter7.expressions]
_ __exp_var (subst_scope) [in Chapter7.expressions]
_ ⟨ _ ⟩ (subst_scope) [in Chapter6.variadic_fin]
_ [ _ ] (subst_scope) [in Chapter6.variadic_fin]
↑__tm (subst_scope) [in Chapter6.variadic_fin]
↑__tm (subst_scope) [in Chapter6.variadic_fin]
var (subst_scope) [in Chapter6.variadic_fin]
_ __tm (subst_scope) [in Chapter6.variadic_fin]
_ __tm (subst_scope) [in Chapter6.variadic_fin]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Chapter6.sysf_cbv]
_ [ _ ; _ ] (subst_scope) [in Chapter6.sysf_cbv]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Chapter6.sysf_cbv]
_ [ _ ; _ ] (subst_scope) [in Chapter6.sysf_cbv]
_ ⟨ _ ⟩ (subst_scope) [in Chapter6.sysf_cbv]
_ [ _ ] (subst_scope) [in Chapter6.sysf_cbv]
↑__vl (subst_scope) [in Chapter6.sysf_cbv]
↑__vl (subst_scope) [in Chapter6.sysf_cbv]
↑__ty (subst_scope) [in Chapter6.sysf_cbv]
↑__ty (subst_scope) [in Chapter6.sysf_cbv]
↑__vl (subst_scope) [in Chapter6.sysf_cbv]
↑__ty (subst_scope) [in Chapter6.sysf_cbv]
var (subst_scope) [in Chapter6.sysf_cbv]
_ __vl (subst_scope) [in Chapter6.sysf_cbv]
_ __vl (subst_scope) [in Chapter6.sysf_cbv]
var (subst_scope) [in Chapter6.sysf_cbv]
_ __ty (subst_scope) [in Chapter6.sysf_cbv]
_ __ty (subst_scope) [in Chapter6.sysf_cbv]
_ ⟨ _ ⟩ (subst_scope) [in Chapter9.stlc]
_ [ _ ] (subst_scope) [in Chapter9.stlc]
↑__tm (subst_scope) [in Chapter9.stlc]
↑__tm (subst_scope) [in Chapter9.stlc]
var (subst_scope) [in Chapter9.stlc]
_ __tm (subst_scope) [in Chapter9.stlc]
_ __tm (subst_scope) [in Chapter9.stlc]
↑ (subst_scope) [in fintype]
_ .. (subst_scope) [in fintype]
_ .: _ (subst_scope) [in fintype]
_ [ _ ; _ ] (subst_scope) [in fintype]
_ [ _ ] (subst_scope) [in fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [in fintype]
_ ⟨ _ ⟩ (subst_scope) [in fintype]
↑ (subst_scope) [in fintype_variadic]
_ .. (subst_scope) [in fintype_variadic]
_ .: _ (subst_scope) [in fintype_variadic]
_ [ _ ; _ ] (subst_scope) [in fintype_variadic]
_ [ _ ] (subst_scope) [in fintype_variadic]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in fintype_variadic]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in fintype_variadic]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in fintype_variadic]
_ ⟨ _ ; _ ⟩ (subst_scope) [in fintype_variadic]
_ ⟨ _ ⟩ (subst_scope) [in fintype_variadic]
_ ⟨ _ ⟩ (subst_scope) [in Chapter6.utlc_pairs]
_ [ _ ] (subst_scope) [in Chapter6.utlc_pairs]
↑__tm (subst_scope) [in Chapter6.utlc_pairs]
↑__tm (subst_scope) [in Chapter6.utlc_pairs]
var (subst_scope) [in Chapter6.utlc_pairs]
_ __tm (subst_scope) [in Chapter6.utlc_pairs]
_ __tm (subst_scope) [in Chapter6.utlc_pairs]
_ [ _ ] (subst_scope) [in Chapter6.fol]
_ [ _ ] (subst_scope) [in Chapter6.fol]
↑__tm (subst_scope) [in Chapter6.fol]
↑__tm (subst_scope) [in Chapter6.fol]
var (subst_scope) [in Chapter6.fol]
_ __tm (subst_scope) [in Chapter6.fol]
_ __tm (subst_scope) [in Chapter6.fol]
_ ⟨ _ ⟩ (subst_scope) [in Chapter3.utlc_pure]
_ [ _ ] (subst_scope) [in Chapter3.utlc_pure]
↑__tm (subst_scope) [in Chapter3.utlc_pure]
↑__tm (subst_scope) [in Chapter3.utlc_pure]
var (subst_scope) [in Chapter3.utlc_pure]
_ __tm (subst_scope) [in Chapter3.utlc_pure]
_ __tm (subst_scope) [in Chapter3.utlc_pure]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Chapter10.sysf]
_ [ _ ; _ ] (subst_scope) [in Chapter10.sysf]
_ ⟨ _ ⟩ (subst_scope) [in Chapter10.sysf]
_ [ _ ] (subst_scope) [in Chapter10.sysf]
↑__tm (subst_scope) [in Chapter10.sysf]
↑__tm (subst_scope) [in Chapter10.sysf]
↑__ty (subst_scope) [in Chapter10.sysf]
↑__ty (subst_scope) [in Chapter10.sysf]
↑__tm (subst_scope) [in Chapter10.sysf]
↑__ty (subst_scope) [in Chapter10.sysf]
var (subst_scope) [in Chapter10.sysf]
_ __tm (subst_scope) [in Chapter10.sysf]
_ __tm (subst_scope) [in Chapter10.sysf]
var (subst_scope) [in Chapter10.sysf]
_ __ty (subst_scope) [in Chapter10.sysf]
_ __ty (subst_scope) [in Chapter10.sysf]
_ ⟨ _ ⟩ (subst_scope) [in Chapter6.picalculus]
_ ⟨ _ ⟩ (subst_scope) [in Chapter6.picalculus]
↑__chan (subst_scope) [in Chapter6.picalculus]
var (subst_scope) [in Chapter6.picalculus]
_ __chan (subst_scope) [in Chapter6.picalculus]
_ __chan (subst_scope) [in Chapter6.picalculus]
_ ⟨ _ ⟩ (subst_scope) [in Chapter6.recty]
_ [ _ ] (subst_scope) [in Chapter6.recty]
↑__ty (subst_scope) [in Chapter6.recty]
↑__ty (subst_scope) [in Chapter6.recty]
var (subst_scope) [in Chapter6.recty]
_ __ty (subst_scope) [in Chapter6.recty]
_ __ty (subst_scope) [in Chapter6.recty]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Chapter10.sysf_pat]
_ [ _ ; _ ] (subst_scope) [in Chapter10.sysf_pat]
_ ⟨ _ ⟩ (subst_scope) [in Chapter10.sysf_pat]
_ [ _ ] (subst_scope) [in Chapter10.sysf_pat]
_ ⟨ _ ⟩ (subst_scope) [in Chapter10.sysf_pat]
_ [ _ ] (subst_scope) [in Chapter10.sysf_pat]
↑__tm (subst_scope) [in Chapter10.sysf_pat]
↑__tm (subst_scope) [in Chapter10.sysf_pat]
↑__ty (subst_scope) [in Chapter10.sysf_pat]
↑__ty (subst_scope) [in Chapter10.sysf_pat]
↑__tm (subst_scope) [in Chapter10.sysf_pat]
↑__ty (subst_scope) [in Chapter10.sysf_pat]
var (subst_scope) [in Chapter10.sysf_pat]
_ __tm (subst_scope) [in Chapter10.sysf_pat]
_ __tm (subst_scope) [in Chapter10.sysf_pat]
var (subst_scope) [in Chapter10.sysf_pat]
_ __ty (subst_scope) [in Chapter10.sysf_pat]
_ __ty (subst_scope) [in Chapter10.sysf_pat]
_ .: _ [in unscoped]
_ >> _ [in fintype]
_ >> _ [in fintype_variadic]
_ `_ _ [in Chapter9.equivalence]
_ |- _ : _ [in Chapter9.preservation]
_ ≡* _ [in Chapter4.termination]
_ ≡+ _ [in Chapter4.termination]
_ ≡ _ [in Chapter4.termination]
_ ≻ _ [in Chapter4.termination]
_ ⊃ _ [in Chapter4.termination]
_ ⇝__s _ [in Chapter4.termination]
_ ⇝__p _ [in Chapter4.termination]
_ ∘ _ [in Chapter4.termination]
_ |- _ : _ [in Chapter9.variadic_preservation]
_ ~> _ [in header_metacoq]
Compose Lemma _ on _ using _ : _ [in header_metacoq]
Compose Lemma _ on _ by inversion : _ [in header_metacoq]
Compose Lemma _ on _ : _ [in header_metacoq]
Compose Fixpoint _ on _ : _ [in header_metacoq]
EV _ => _ [in Chapter10.POPLMark1]
list_map [in axioms]
Modular Fixpoint _ where _ extends _ := _ [in header_metacoq]
Modular Fixpoint _ where _ extends _ with _ := _ [in header_metacoq]
Modular Lemma _ where _ extends _ with _ : _ [in header_metacoq]
Modular Lemma _ where _ extends _ at _ with _ : _ [in header_metacoq]
sn__leaf [in Chapter4.termination]
sn__split [in Chapter4.termination]
sn≡ [in Chapter4.termination]
sn≻ [in Chapter4.termination]
sn⊃ [in Chapter4.termination]
SUB _ |- _ <: _ [in Chapter10.POPLMark22]
SUB _ |- _ <: _ [in Chapter10.POPLMark21]
SUB _ |- _ <: _ [in Chapter10.POPLMark1]
TY _ ; _ |- _ : _ [in Chapter10.POPLMark1]
0 [in Chapter4.termination]
↑ [in unscoped]
⟨ _ , _ ⟩ [in Chapter4.termination]
λ _ [in Chapter4.termination]
Module Index
C
CommaNotation [in fintype]CommaNotation [in fintype_variadic]
L
L [in Chapter9.girard]P
polyadic [in Chapter6.reductions]S
SN [in Chapter9.girard]sysf_cbv [in Chapter6.reductions]
Variable Index
D
Definitions.e [in ARS]Definitions.T [in ARS]
E
exp_var.retract_subst_exp [in Chapter7.expressions]exp_var.retract_ren_exp [in Chapter7.expressions]
exp_var.retract_exp_var [in Chapter7.expressions]
exp_var.subst_exp [in Chapter7.expressions]
exp_var.ren_exp [in Chapter7.expressions]
exp_var.exp [in Chapter7.expressions]
exp_bool.retract_subst_exp [in Chapter7.expressions]
exp_bool.retract_ren_exp [in Chapter7.expressions]
exp_bool.retract_exp_bool [in Chapter7.expressions]
exp_bool.rinst_inst_exp [in Chapter7.expressions]
exp_bool.rinstInst_up_exp_exp [in Chapter7.expressions]
exp_bool.compSubstSubst_exp [in Chapter7.expressions]
exp_bool.up_subst_subst_exp_exp [in Chapter7.expressions]
exp_bool.compSubstRen_exp [in Chapter7.expressions]
exp_bool.up_subst_ren_exp_exp [in Chapter7.expressions]
exp_bool.compRenSubst_exp [in Chapter7.expressions]
exp_bool.up_ren_subst_exp_exp [in Chapter7.expressions]
exp_bool.compRenRen_exp [in Chapter7.expressions]
exp_bool.up_ren_ren_exp_exp [in Chapter7.expressions]
exp_bool.ext_exp [in Chapter7.expressions]
exp_bool.upExt_exp_exp [in Chapter7.expressions]
exp_bool.extRen_exp [in Chapter7.expressions]
exp_bool.upExtRen_exp_exp [in Chapter7.expressions]
exp_bool.idSubst_exp [in Chapter7.expressions]
exp_bool.upId_exp_exp [in Chapter7.expressions]
exp_bool.subst_exp [in Chapter7.expressions]
exp_bool.up_exp_exp [in Chapter7.expressions]
exp_bool.ren_exp [in Chapter7.expressions]
exp_bool.upRen_exp_exp [in Chapter7.expressions]
exp_bool.var_exp [in Chapter7.expressions]
exp_bool.exp [in Chapter7.expressions]
exp_arith.retract_subst_exp [in Chapter7.expressions]
exp_arith.retract_ren_exp [in Chapter7.expressions]
exp_arith.retract_exp_arith [in Chapter7.expressions]
exp_arith.rinst_inst_exp [in Chapter7.expressions]
exp_arith.rinstInst_up_exp_exp [in Chapter7.expressions]
exp_arith.compSubstSubst_exp [in Chapter7.expressions]
exp_arith.up_subst_subst_exp_exp [in Chapter7.expressions]
exp_arith.compSubstRen_exp [in Chapter7.expressions]
exp_arith.up_subst_ren_exp_exp [in Chapter7.expressions]
exp_arith.compRenSubst_exp [in Chapter7.expressions]
exp_arith.up_ren_subst_exp_exp [in Chapter7.expressions]
exp_arith.compRenRen_exp [in Chapter7.expressions]
exp_arith.up_ren_ren_exp_exp [in Chapter7.expressions]
exp_arith.ext_exp [in Chapter7.expressions]
exp_arith.upExt_exp_exp [in Chapter7.expressions]
exp_arith.extRen_exp [in Chapter7.expressions]
exp_arith.upExtRen_exp_exp [in Chapter7.expressions]
exp_arith.idSubst_exp [in Chapter7.expressions]
exp_arith.upId_exp_exp [in Chapter7.expressions]
exp_arith.subst_exp [in Chapter7.expressions]
exp_arith.up_exp_exp [in Chapter7.expressions]
exp_arith.ren_exp [in Chapter7.expressions]
exp_arith.upRen_exp_exp [in Chapter7.expressions]
exp_arith.var_exp [in Chapter7.expressions]
exp_arith.exp [in Chapter7.expressions]
exp_lam.retract_subst_exp [in Chapter7.expressions]
exp_lam.retract_ren_exp [in Chapter7.expressions]
exp_lam.retract_exp_lam [in Chapter7.expressions]
exp_lam.rinst_inst_exp [in Chapter7.expressions]
exp_lam.rinstInst_up_exp_exp [in Chapter7.expressions]
exp_lam.compSubstSubst_exp [in Chapter7.expressions]
exp_lam.up_subst_subst_exp_exp [in Chapter7.expressions]
exp_lam.compSubstRen_exp [in Chapter7.expressions]
exp_lam.up_subst_ren_exp_exp [in Chapter7.expressions]
exp_lam.compRenSubst_exp [in Chapter7.expressions]
exp_lam.up_ren_subst_exp_exp [in Chapter7.expressions]
exp_lam.compRenRen_exp [in Chapter7.expressions]
exp_lam.up_ren_ren_exp_exp [in Chapter7.expressions]
exp_lam.ext_exp [in Chapter7.expressions]
exp_lam.upExt_exp_exp [in Chapter7.expressions]
exp_lam.extRen_exp [in Chapter7.expressions]
exp_lam.upExtRen_exp_exp [in Chapter7.expressions]
exp_lam.idSubst_exp [in Chapter7.expressions]
exp_lam.upId_exp_exp [in Chapter7.expressions]
exp_lam.subst_exp [in Chapter7.expressions]
exp_lam.up_exp_exp [in Chapter7.expressions]
exp_lam.ren_exp [in Chapter7.expressions]
exp_lam.upRen_exp_exp [in Chapter7.expressions]
exp_lam.var_exp [in Chapter7.expressions]
exp_lam.exp [in Chapter7.expressions]
M
MiniML_var.L_strong [in Chapter9.sn_var]MiniML_var.L [in Chapter9.sn_var]
MiniML_var.ren_preserves [in Chapter9.sn_var]
MiniML_var.whnf_whnf_var [in Chapter9.sn_var]
MiniML_var.step [in Chapter9.sn_var]
MiniML_var.retract_has_ty_rev [in Chapter9.sn_var]
MiniML_var.retract_has_ty [in Chapter9.sn_var]
MiniML_var.has_ty [in Chapter9.sn_var]
MiniML_var.subst_id_exp [in Chapter9.sn_var]
MiniML_var.retract_subst_exp [in Chapter9.sn_var]
MiniML_var.subst_exp [in Chapter9.sn_var]
MiniML_var.retract_ren_exp [in Chapter9.sn_var]
MiniML_var.ren_exp [in Chapter9.sn_var]
MiniML_var.ty [in Chapter9.sn_var]
MiniML_var.exp [in Chapter9.sn_var]
MiniML_Lambda.E_strong_var [in Chapter9.sn_lam]
MiniML_Lambda.retract_L_strong [in Chapter9.sn_lam]
MiniML_Lambda.ren_var [in Chapter9.sn_lam]
MiniML_Lambda.ren_preserves [in Chapter9.sn_lam]
MiniML_Lambda.whnf_anti_renaming [in Chapter9.sn_lam]
MiniML_Lambda.L_strong [in Chapter9.sn_lam]
MiniML_Lambda.retract_whnf_lam [in Chapter9.sn_lam]
MiniML_Lambda.retract_L [in Chapter9.sn_lam]
MiniML_Lambda.L [in Chapter9.sn_lam]
MiniML_Lambda.retract_step_rev [in Chapter9.sn_lam]
MiniML_Lambda.retract_step [in Chapter9.sn_lam]
MiniML_Lambda.step [in Chapter9.sn_lam]
MiniML_Lambda.retract_has_ty_rev [in Chapter9.sn_lam]
MiniML_Lambda.retract_has_ty [in Chapter9.sn_lam]
MiniML_Lambda.hasty_var [in Chapter9.sn_lam]
MiniML_Lambda.has_ty [in Chapter9.sn_lam]
MiniML_Lambda.subst_exp_var [in Chapter9.sn_lam]
MiniML_Lambda.up_exp_exp_def' [in Chapter9.sn_lam]
MiniML_Lambda.up_exp_exp_def [in Chapter9.sn_lam]
MiniML_Lambda.upRen_exp_exp_def [in Chapter9.sn_lam]
MiniML_Lambda.retract_subst_exp [in Chapter9.sn_lam]
MiniML_Lambda.retract_ren_exp [in Chapter9.sn_lam]
MiniML_Lambda.rinst_inst_exp [in Chapter9.sn_lam]
MiniML_Lambda.rinstInst_up_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.compSubstSubst_exp [in Chapter9.sn_lam]
MiniML_Lambda.up_subst_subst_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.compSubstRen_exp [in Chapter9.sn_lam]
MiniML_Lambda.up_subst_ren_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.compRenSubst_exp [in Chapter9.sn_lam]
MiniML_Lambda.up_ren_subst_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.compRenRen_exp [in Chapter9.sn_lam]
MiniML_Lambda.up_ren_ren_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.ext_exp [in Chapter9.sn_lam]
MiniML_Lambda.upExt_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.extRen_exp [in Chapter9.sn_lam]
MiniML_Lambda.upExtRen_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.idSubst_exp [in Chapter9.sn_lam]
MiniML_Lambda.upId_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.subst_exp [in Chapter9.sn_lam]
MiniML_Lambda.up_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.ren_exp [in Chapter9.sn_lam]
MiniML_Lambda.upRen_exp_exp [in Chapter9.sn_lam]
MiniML_Lambda.exp [in Chapter9.sn_lam]
MiniML_Bool.ren_preserves [in Chapter9.sn_bool]
MiniML_Bool.retract_L_strong [in Chapter9.sn_bool]
MiniML_Bool.whnf_whnf_bool [in Chapter9.sn_bool]
MiniML_Bool.retract_L [in Chapter9.sn_bool]
MiniML_Bool.retract_step_rev [in Chapter9.sn_bool]
MiniML_Bool.retract_step [in Chapter9.sn_bool]
MiniML_Bool.step [in Chapter9.sn_bool]
MiniML_Bool.retract_has_ty_rev [in Chapter9.sn_bool]
MiniML_Bool.retract_has_ty [in Chapter9.sn_bool]
MiniML_Bool.has_ty [in Chapter9.sn_bool]
MiniML_Bool.retract_subst_exp [in Chapter9.sn_bool]
MiniML_Bool.subst_exp [in Chapter9.sn_bool]
MiniML_Bool.retract_ren_exp [in Chapter9.sn_bool]
MiniML_Bool.ren_exp [in Chapter9.sn_bool]
MiniML_Bool.exp [in Chapter9.sn_bool]
MiniML_Bool.ty [in Chapter9.sn_bool]
MiniML_Arith.step_anti_renaming [in Chapter9.sn_arith]
MiniML_Arith.ren_preserves [in Chapter9.sn_arith]
MiniML_Arith.retract_L_strong [in Chapter9.sn_arith]
MiniML_Arith.whnf_whnf_arith [in Chapter9.sn_arith]
MiniML_Arith.retract_L [in Chapter9.sn_arith]
MiniML_Arith.retract_step_rev [in Chapter9.sn_arith]
MiniML_Arith.retract_step [in Chapter9.sn_arith]
MiniML_Arith.step [in Chapter9.sn_arith]
MiniML_Arith.retract_has_ty_rev [in Chapter9.sn_arith]
MiniML_Arith.retract_has_ty [in Chapter9.sn_arith]
MiniML_Arith.has_ty [in Chapter9.sn_arith]
MiniML_Arith.retract_subst_exp [in Chapter9.sn_arith]
MiniML_Arith.subst_exp [in Chapter9.sn_arith]
MiniML_Arith.retract_ren_exp [in Chapter9.sn_arith]
MiniML_Arith.ren_exp [in Chapter9.sn_arith]
MiniML_Arith.exp [in Chapter9.sn_arith]
MiniML_Arith.ty [in Chapter9.sn_arith]
P
Pattern.pat_ty_eval [in Chapter10.POPLMark22]Pattern.pat_progress [in Chapter10.POPLMark22]
Pattern.pat_ty_subst [in Chapter10.POPLMark22]
Pattern.pat_eval [in Chapter10.POPLMark22]
Pattern.pat_ty [in Chapter10.POPLMark22]
Pattern.pat_ty_eval [in Chapter10.POPLMark21]
Pattern.pat_progress [in Chapter10.POPLMark21]
Pattern.pat_ty_subst [in Chapter10.POPLMark21]
Pattern.pat_eval [in Chapter10.POPLMark21]
Pattern.pat_ty [in Chapter10.POPLMark21]
Pattern.sub_refl [in Chapter10.POPLMark22]
Pattern.sub_refl [in Chapter10.POPLMark21]
T
ty_arith.retract_ty_arith [in Chapter7.expressions]ty_arith.ty [in Chapter7.expressions]
ty_bool.retract_ty_bool [in Chapter7.expressions]
ty_bool.ty [in Chapter7.expressions]
ty_lam.retract_ty_lam [in Chapter7.expressions]
ty_lam.ty [in Chapter7.expressions]
Library Index
A
ARSaxioms
C
confluenceD
defsE
equivalenceexpressions
F
fintypefintype_variadic
fol
G
girardH
header_extensibleheader_metacoq
P
picalculusPOPLMark1
POPLMark21
POPLMark22
preservation
R
rectyreduction
reductions
S
sigmacalculussn
sn_lam
sn_var
sn_raamsdonk
sn_arith
sn_bool
sn_mod
soundness
stlc
sysf
sysf_cbv
sysf_pat
T
tacticstermination
U
unscopedutlc_pairs
utlc_scoped
utlc_pure
V
variadic_preservationvariadic_fin
variadic_list
W
wnLemma Index
A
algeq_trans [in Chapter9.equivalence]algeq_sym [in Chapter9.equivalence]
algeq_backward_closure [in Chapter9.equivalence]
algEq_monotone [in Chapter9.equivalence]
anti_rename [in Chapter9.sn_raamsdonk]
B
beta_closure [in Chapter9.girard]C
can_form_rectm [in Chapter10.POPLMark22]can_form_all [in Chapter10.POPLMark22]
can_form_arr [in Chapter10.POPLMark22]
can_form_rectm [in Chapter10.POPLMark21]
can_form_all [in Chapter10.POPLMark21]
can_form_arr [in Chapter10.POPLMark21]
can_form_all [in Chapter10.POPLMark1]
can_form_arr [in Chapter10.POPLMark1]
closed_appR [in Chapter9.sn_raamsdonk]
closed_lam [in Chapter9.sn_raamsdonk]
close_ren [in Chapter9.sn]
close_ren [in Chapter9.sn_lam]
compComp_tm [in Chapter3.utlc_scoped]
compComp_tm [in Chapter6.variadic_list]
compComp_exp [in Chapter7.expressions]
compComp_exp_var [in Chapter7.expressions]
compComp_exp_bool [in Chapter7.expressions]
compComp_exp_arith [in Chapter7.expressions]
compComp_exp_lam [in Chapter7.expressions]
compComp_tm [in Chapter6.variadic_fin]
compComp_vl [in Chapter6.sysf_cbv]
compComp_tm [in Chapter6.sysf_cbv]
compComp_ty [in Chapter6.sysf_cbv]
compComp_tm [in Chapter9.stlc]
compComp_tm [in Chapter6.utlc_pairs]
compComp_form [in Chapter6.fol]
compComp_tm [in Chapter6.fol]
compComp_exp [in Chapter9.sn_lam]
compComp_tm [in Chapter3.utlc_pure]
compComp_tm [in Chapter10.sysf]
compComp_ty [in Chapter10.sysf]
compComp_ty [in Chapter6.recty]
compComp_tm [in Chapter10.sysf_pat]
compComp_pat [in Chapter10.sysf_pat]
compComp_ty [in Chapter10.sysf_pat]
compComp'_tm [in Chapter3.utlc_scoped]
compComp'_tm [in Chapter6.variadic_list]
compComp'_exp [in Chapter7.expressions]
compComp'_exp_var [in Chapter7.expressions]
compComp'_exp_bool [in Chapter7.expressions]
compComp'_exp_arith [in Chapter7.expressions]
compComp'_exp_lam [in Chapter7.expressions]
compComp'_tm [in Chapter6.variadic_fin]
compComp'_vl [in Chapter6.sysf_cbv]
compComp'_tm [in Chapter6.sysf_cbv]
compComp'_ty [in Chapter6.sysf_cbv]
compComp'_tm [in Chapter9.stlc]
compComp'_tm [in Chapter6.utlc_pairs]
compComp'_form [in Chapter6.fol]
compComp'_tm [in Chapter6.fol]
compComp'_exp [in Chapter9.sn_lam]
compComp'_tm [in Chapter3.utlc_pure]
compComp'_tm [in Chapter10.sysf]
compComp'_ty [in Chapter10.sysf]
compComp'_ty [in Chapter6.recty]
compComp'_tm [in Chapter10.sysf_pat]
compComp'_pat [in Chapter10.sysf_pat]
compComp'_ty [in Chapter10.sysf_pat]
completeness [in Chapter9.equivalence]
compRen_tm [in Chapter3.utlc_scoped]
compRen_tm [in Chapter6.variadic_list]
compRen_exp [in Chapter7.expressions]
compRen_exp_var [in Chapter7.expressions]
compRen_exp_bool [in Chapter7.expressions]
compRen_exp_arith [in Chapter7.expressions]
compRen_exp_lam [in Chapter7.expressions]
compRen_tm [in Chapter6.variadic_fin]
compRen_vl [in Chapter6.sysf_cbv]
compRen_tm [in Chapter6.sysf_cbv]
compRen_ty [in Chapter6.sysf_cbv]
compRen_tm [in Chapter9.stlc]
compRen_tm [in Chapter6.utlc_pairs]
compRen_exp [in Chapter9.sn_lam]
compRen_tm [in Chapter3.utlc_pure]
compRen_tm [in Chapter10.sysf]
compRen_ty [in Chapter10.sysf]
compRen_ty [in Chapter6.recty]
compRen_tm [in Chapter10.sysf_pat]
compRen_pat [in Chapter10.sysf_pat]
compRen_ty [in Chapter10.sysf_pat]
compRen'_tm [in Chapter3.utlc_scoped]
compRen'_tm [in Chapter6.variadic_list]
compRen'_exp [in Chapter7.expressions]
compRen'_exp_var [in Chapter7.expressions]
compRen'_exp_bool [in Chapter7.expressions]
compRen'_exp_arith [in Chapter7.expressions]
compRen'_exp_lam [in Chapter7.expressions]
compRen'_tm [in Chapter6.variadic_fin]
compRen'_vl [in Chapter6.sysf_cbv]
compRen'_tm [in Chapter6.sysf_cbv]
compRen'_ty [in Chapter6.sysf_cbv]
compRen'_tm [in Chapter9.stlc]
compRen'_tm [in Chapter6.utlc_pairs]
compRen'_exp [in Chapter9.sn_lam]
compRen'_tm [in Chapter3.utlc_pure]
compRen'_tm [in Chapter10.sysf]
compRen'_ty [in Chapter10.sysf]
compRen'_ty [in Chapter6.recty]
compRen'_tm [in Chapter10.sysf_pat]
compRen'_pat [in Chapter10.sysf_pat]
compRen'_ty [in Chapter10.sysf_pat]
confluence [in Chapter9.equivalence]
congr_lam [in Chapter3.utlc_scoped]
congr_app [in Chapter3.utlc_scoped]
congr_lam [in Chapter6.variadic_list]
congr_app [in Chapter6.variadic_list]
congr_In_exp_arith [in Chapter7.expressions]
congr_In_exp_bool [in Chapter7.expressions]
congr_In_exp_lam [in Chapter7.expressions]
congr_In_exp_var [in Chapter7.expressions]
congr_If_ [in Chapter7.expressions]
congr_constBool_ [in Chapter7.expressions]
congr_constNat_ [in Chapter7.expressions]
congr_plus_ [in Chapter7.expressions]
congr_app_ [in Chapter7.expressions]
congr_ab_ [in Chapter7.expressions]
congr_In_ty_arith [in Chapter7.expressions]
congr_In_ty_bool [in Chapter7.expressions]
congr_In_ty_lam [in Chapter7.expressions]
congr_natTy_ [in Chapter7.expressions]
congr_boolTy_ [in Chapter7.expressions]
congr_arr_ [in Chapter7.expressions]
congr_lam [in Chapter6.variadic_fin]
congr_app [in Chapter6.variadic_fin]
congr_tlam [in Chapter6.sysf_cbv]
congr_lam [in Chapter6.sysf_cbv]
congr_vt [in Chapter6.sysf_cbv]
congr_tapp [in Chapter6.sysf_cbv]
congr_app [in Chapter6.sysf_cbv]
congr_all [in Chapter6.sysf_cbv]
congr_arr [in Chapter6.sysf_cbv]
congr_lam [in Chapter9.stlc]
congr_app [in Chapter9.stlc]
congr_Fun [in Chapter9.stlc]
congr_Base [in Chapter9.stlc]
congr_matchpair [in Chapter6.utlc_pairs]
congr_pair [in Chapter6.utlc_pairs]
congr_lam [in Chapter6.utlc_pairs]
congr_app [in Chapter6.utlc_pairs]
congr_all [in Chapter6.fol]
congr_pred [in Chapter6.fol]
congr_fal [in Chapter6.fol]
congr_plus [in Chapter6.fol]
congr_atom [in Chapter6.fol]
congr_lam [in Chapter3.utlc_pure]
congr_app [in Chapter3.utlc_pure]
congr_Out [in Chapter6.picalculus]
congr_In [in Chapter6.picalculus]
congr_Par [in Chapter6.picalculus]
congr_Res [in Chapter6.picalculus]
congr_Bang [in Chapter6.picalculus]
congr_Nil [in Chapter6.picalculus]
congr_pairR [in Chapter4.termination]
congr_pairL [in Chapter4.termination]
congr_compR [in Chapter4.termination]
congr_compL [in Chapter4.termination]
congr_lam [in Chapter4.termination]
congr_recty [in Chapter6.recty]
congr_all [in Chapter6.recty]
congr_arr [in Chapter6.recty]
congr_top [in Chapter6.recty]
congr_inj [in header_extensible]
congr_letpat [in Chapter10.sysf_pat]
congr_proj [in Chapter10.sysf_pat]
congr_rectm [in Chapter10.sysf_pat]
congr_tabs [in Chapter10.sysf_pat]
congr_abs [in Chapter10.sysf_pat]
congr_tapp [in Chapter10.sysf_pat]
congr_app [in Chapter10.sysf_pat]
congr_patlist [in Chapter10.sysf_pat]
congr_patvar [in Chapter10.sysf_pat]
congr_recty [in Chapter10.sysf_pat]
congr_all [in Chapter10.sysf_pat]
congr_arr [in Chapter10.sysf_pat]
congr_top [in Chapter10.sysf_pat]
context_morphism_lemma [in Chapter10.POPLMark22]
context_renaming_lemma' [in Chapter10.POPLMark22]
context_renaming_lemma [in Chapter10.POPLMark22]
context_morphism_lemma [in Chapter10.POPLMark21]
context_renaming_lemma' [in Chapter10.POPLMark21]
context_renaming_lemma [in Chapter10.POPLMark21]
context_morphism_lemma [in Chapter10.POPLMark1]
context_renaming_lemma [in Chapter10.POPLMark1]
cont_ext_id [in Chapter9.equivalence]
cont_ext_cons [in Chapter9.equivalence]
cont_ext_shift [in Chapter9.equivalence]
cr [in Chapter9.sn_raamsdonk]
D
destruct_fin [in fintype]destruct_fin [in fintype_variadic]
E
equiv_confluent [in Chapter4.confluence]equiv_locally_confluent [in Chapter4.confluence]
equiv_uquiv [in Chapter4.termination]
ev_progress [in Chapter10.POPLMark22]
ev_progress [in Chapter10.POPLMark21]
ev_progress [in Chapter10.POPLMark1]
exchangeability [in Chapter4.termination]
ext_SN [in Chapter9.sn_raamsdonk]
E_strong_base [in Chapter9.sn_var]
E_strong_step [in Chapter9.sn_var]
E_strong_sn [in Chapter9.sn_var]
E_strong_var [in Chapter9.sn]
E_strong_base [in Chapter9.sn]
E_strong_step [in Chapter9.sn]
E_strong_sn [in Chapter9.sn]
E_strong_var [in Chapter9.sn_mod]
F
fin_eta [in fintype]fin_eta [in fintype_variadic]
fundamental [in Chapter9.equivalence]
fundamental_backwards [in Chapter9.sn_raamsdonk]
fundamental_theorem [in Chapter9.girard]
H
has_ty_subst_var [in Chapter9.sn_var]has_ty_ren_var [in Chapter9.sn_var]
has_ty_rev_arith [in Chapter9.sn_mod]
has_ty_rev_bool [in Chapter9.sn_mod]
has_ty_rev_lam [in Chapter9.sn_mod]
has_ty_rev_var [in Chapter9.sn_mod]
I
id_red [in Chapter9.sn_raamsdonk]instId_tm [in Chapter3.utlc_scoped]
instId_tm [in Chapter6.variadic_list]
instId_exp [in Chapter7.expressions]
instId_exp_var [in Chapter7.expressions]
instId_exp_bool [in Chapter7.expressions]
instId_exp_arith [in Chapter7.expressions]
instId_exp_lam [in Chapter7.expressions]
instId_tm [in Chapter6.variadic_fin]
instId_vl [in Chapter6.sysf_cbv]
instId_tm [in Chapter6.sysf_cbv]
instId_ty [in Chapter6.sysf_cbv]
instId_tm [in Chapter9.stlc]
instId_tm [in Chapter6.utlc_pairs]
instId_form [in Chapter6.fol]
instId_tm [in Chapter6.fol]
instId_exp [in Chapter9.sn_lam]
instId_tm [in Chapter3.utlc_pure]
instId_tm [in Chapter10.sysf]
instId_ty [in Chapter10.sysf]
instId_ty [in Chapter6.recty]
instId_tm [in Chapter10.sysf_pat]
instId_pat [in Chapter10.sysf_pat]
instId_ty [in Chapter10.sysf_pat]
in_map [in Chapter10.POPLMark22]
in_map [in Chapter10.POPLMark21]
L
label_equiv_map [in Chapter10.POPLMark22]label_equiv_map [in Chapter10.POPLMark21]
list_dec [in Chapter10.POPLMark22]
list_dec [in Chapter10.POPLMark21]
logeq_id [in Chapter9.equivalence]
logeq_trans [in Chapter9.equivalence]
logeq_sym [in Chapter9.equivalence]
logeq_backward_closure [in Chapter9.equivalence]
logEq_monotone [in Chapter9.equivalence]
L_close_ren_lam [in Chapter9.sn]
L_val_lam [in Chapter9.sn_lam]
L_close_ren_bool [in Chapter9.sn_bool]
L_close_ren_arith [in Chapter9.sn_arith]
L_ren [in Chapter9.wn]
L.Girard [in Chapter9.girard]
L.L_typing [in Chapter9.girard]
L.preservation [in Chapter9.girard]
L.preservation_mstep [in Chapter9.girard]
L.ren [in Chapter9.girard]
L.sn [in Chapter9.girard]
L.var [in Chapter9.girard]
M
main [in Chapter9.equivalence]main_lemma [in Chapter9.sn_raamsdonk]
mstep_beta [in Chapter9.reduction]
mstep_subst [in Chapter9.reduction]
mstep_inst [in Chapter9.reduction]
mstep_app [in Chapter9.reduction]
mstep_lam [in Chapter9.reduction]
mstep_inst [in Chapter9.variadic_preservation]
mwhr_ren [in Chapter9.equivalence]
mwhr_trans [in Chapter9.equivalence]
mwhr_appL [in Chapter9.equivalence]
N
natequiv_update [in Chapter10.POPLMark22]natequiv_update [in Chapter10.POPLMark21]
neutral_preservation [in Chapter9.sn_raamsdonk]
neutral_mwhr [in Chapter9.equivalence]
neutral_whr [in Chapter9.equivalence]
newman [in ARS]
norm [in Chapter9.sn_raamsdonk]
P
polyadic.step_substitutive [in Chapter6.reductions]preservation [in Chapter10.POPLMark22]
preservation [in Chapter9.preservation]
preservation [in Chapter4.termination]
preservation [in Chapter10.POPLMark21]
preservation [in Chapter10.POPLMark1]
preservation_var [in Chapter9.sn_var]
R
redsn_backwards [in Chapter9.sn_raamsdonk]red_var [in Chapter9.sn_raamsdonk]
rename [in Chapter9.sn_raamsdonk]
rename_red [in Chapter9.sn_raamsdonk]
renComp_tm [in Chapter3.utlc_scoped]
renComp_tm [in Chapter6.variadic_list]
renComp_exp [in Chapter7.expressions]
renComp_exp_var [in Chapter7.expressions]
renComp_exp_bool [in Chapter7.expressions]
renComp_exp_arith [in Chapter7.expressions]
renComp_exp_lam [in Chapter7.expressions]
renComp_tm [in Chapter6.variadic_fin]
renComp_vl [in Chapter6.sysf_cbv]
renComp_tm [in Chapter6.sysf_cbv]
renComp_ty [in Chapter6.sysf_cbv]
renComp_tm [in Chapter9.stlc]
renComp_tm [in Chapter6.utlc_pairs]
renComp_exp [in Chapter9.sn_lam]
renComp_tm [in Chapter3.utlc_pure]
renComp_tm [in Chapter10.sysf]
renComp_ty [in Chapter10.sysf]
renComp_ty [in Chapter6.recty]
renComp_tm [in Chapter10.sysf_pat]
renComp_pat [in Chapter10.sysf_pat]
renComp_ty [in Chapter10.sysf_pat]
renComp'_tm [in Chapter3.utlc_scoped]
renComp'_tm [in Chapter6.variadic_list]
renComp'_exp [in Chapter7.expressions]
renComp'_exp_var [in Chapter7.expressions]
renComp'_exp_bool [in Chapter7.expressions]
renComp'_exp_arith [in Chapter7.expressions]
renComp'_exp_lam [in Chapter7.expressions]
renComp'_tm [in Chapter6.variadic_fin]
renComp'_vl [in Chapter6.sysf_cbv]
renComp'_tm [in Chapter6.sysf_cbv]
renComp'_ty [in Chapter6.sysf_cbv]
renComp'_tm [in Chapter9.stlc]
renComp'_tm [in Chapter6.utlc_pairs]
renComp'_exp [in Chapter9.sn_lam]
renComp'_tm [in Chapter3.utlc_pure]
renComp'_tm [in Chapter10.sysf]
renComp'_ty [in Chapter10.sysf]
renComp'_ty [in Chapter6.recty]
renComp'_tm [in Chapter10.sysf_pat]
renComp'_pat [in Chapter10.sysf_pat]
renComp'_ty [in Chapter10.sysf_pat]
renRen_tm [in Chapter3.utlc_scoped]
renRen_tm [in Chapter6.variadic_list]
renRen_exp [in Chapter7.expressions]
renRen_exp_var [in Chapter7.expressions]
renRen_exp_bool [in Chapter7.expressions]
renRen_exp_arith [in Chapter7.expressions]
renRen_exp_lam [in Chapter7.expressions]
renRen_tm [in Chapter6.variadic_fin]
renRen_vl [in Chapter6.sysf_cbv]
renRen_tm [in Chapter6.sysf_cbv]
renRen_ty [in Chapter6.sysf_cbv]
renRen_tm [in Chapter9.stlc]
renRen_tm [in Chapter6.utlc_pairs]
renRen_exp [in Chapter9.sn_lam]
renRen_tm [in Chapter3.utlc_pure]
renRen_tm [in Chapter10.sysf]
renRen_ty [in Chapter10.sysf]
renRen_proc [in Chapter6.picalculus]
renRen_chan [in Chapter6.picalculus]
renRen_ty [in Chapter6.recty]
renRen_tm [in Chapter10.sysf_pat]
renRen_pat [in Chapter10.sysf_pat]
renRen_ty [in Chapter10.sysf_pat]
renRen'_tm [in Chapter3.utlc_scoped]
renRen'_tm [in Chapter6.variadic_list]
renRen'_exp [in Chapter7.expressions]
renRen'_exp_var [in Chapter7.expressions]
renRen'_exp_bool [in Chapter7.expressions]
renRen'_exp_arith [in Chapter7.expressions]
renRen'_exp_lam [in Chapter7.expressions]
renRen'_tm [in Chapter6.variadic_fin]
renRen'_vl [in Chapter6.sysf_cbv]
renRen'_tm [in Chapter6.sysf_cbv]
renRen'_ty [in Chapter6.sysf_cbv]
renRen'_tm [in Chapter9.stlc]
renRen'_tm [in Chapter6.utlc_pairs]
renRen'_exp [in Chapter9.sn_lam]
renRen'_tm [in Chapter3.utlc_pure]
renRen'_tm [in Chapter10.sysf]
renRen'_ty [in Chapter10.sysf]
renRen'_proc [in Chapter6.picalculus]
renRen'_chan [in Chapter6.picalculus]
renRen'_ty [in Chapter6.recty]
renRen'_tm [in Chapter10.sysf_pat]
renRen'_pat [in Chapter10.sysf_pat]
renRen'_ty [in Chapter10.sysf_pat]
ren_preserves_var [in Chapter9.sn_var]
ren_preserves_app [in Chapter9.sn_lam]
ren_preserves_ab [in Chapter9.sn_lam]
ren_preserves_arith [in Chapter9.sn_mod]
ren_preserves_bool [in Chapter9.sn_mod]
ren_preserves_lam [in Chapter9.sn_mod]
ren_preserves [in Chapter9.sn_mod]
ren_preserves_constBool [in Chapter9.sn_bool]
ren_preserves_If [in Chapter9.sn_bool]
ren_sn [in Chapter4.termination]
ren_preserve [in Chapter4.termination]
ren_preserves_constNat [in Chapter9.sn_arith]
ren_preserves_Plus [in Chapter9.sn_arith]
retract_step_arith [in Chapter9.sn_mod]
retract_step_bool [in Chapter9.sn_mod]
retract_step_lam [in Chapter9.sn_mod]
retract_inj [in header_extensible]
rinstId_tm [in Chapter3.utlc_scoped]
rinstId_tm [in Chapter6.variadic_list]
rinstId_exp [in Chapter7.expressions]
rinstId_exp_var [in Chapter7.expressions]
rinstId_exp_bool [in Chapter7.expressions]
rinstId_exp_arith [in Chapter7.expressions]
rinstId_exp_lam [in Chapter7.expressions]
rinstId_tm [in Chapter6.variadic_fin]
rinstId_vl [in Chapter6.sysf_cbv]
rinstId_tm [in Chapter6.sysf_cbv]
rinstId_ty [in Chapter6.sysf_cbv]
rinstId_tm [in Chapter9.stlc]
rinstId_tm [in Chapter6.utlc_pairs]
rinstId_exp [in Chapter9.sn_lam]
rinstId_tm [in Chapter3.utlc_pure]
rinstId_tm [in Chapter10.sysf]
rinstId_ty [in Chapter10.sysf]
rinstId_ty [in Chapter6.recty]
rinstId_tm [in Chapter10.sysf_pat]
rinstId_pat [in Chapter10.sysf_pat]
rinstId_ty [in Chapter10.sysf_pat]
rinstInst_tm [in Chapter3.utlc_scoped]
rinstInst_tm [in Chapter6.variadic_list]
rinstInst_exp [in Chapter7.expressions]
rinstInst_exp_var [in Chapter7.expressions]
rinstInst_exp_bool [in Chapter7.expressions]
rinstInst_exp_arith [in Chapter7.expressions]
rinstInst_exp_lam [in Chapter7.expressions]
rinstInst_tm [in Chapter6.variadic_fin]
rinstInst_vl [in Chapter6.sysf_cbv]
rinstInst_tm [in Chapter6.sysf_cbv]
rinstInst_ty [in Chapter6.sysf_cbv]
rinstInst_tm [in Chapter9.stlc]
rinstInst_tm [in Chapter6.utlc_pairs]
rinstInst_exp [in Chapter9.sn_lam]
rinstInst_tm [in Chapter3.utlc_pure]
rinstInst_tm [in Chapter10.sysf]
rinstInst_ty [in Chapter10.sysf]
rinstInst_ty [in Chapter6.recty]
rinstInst_tm [in Chapter10.sysf_pat]
rinstInst_pat [in Chapter10.sysf_pat]
rinstInst_ty [in Chapter10.sysf_pat]
S
scons_comp [in unscoped]scons_eta [in unscoped]
scons_eta_id [in unscoped]
scons_p_eta [in fintype]
scons_p_congr [in fintype]
scons_p_comp [in fintype]
scons_p_comp' [in fintype]
scons_p_tail [in fintype]
scons_p_tail' [in fintype]
scons_p_head [in fintype]
scons_p_head' [in fintype]
scons_comp [in fintype]
scons_eta_id [in fintype]
scons_eta [in fintype]
scons_p_eta [in fintype_variadic]
scons_p_congr [in fintype_variadic]
scons_p_comp [in fintype_variadic]
scons_p_comp' [in fintype_variadic]
scons_p_tail [in fintype_variadic]
scons_p_tail' [in fintype_variadic]
scons_p_head [in fintype_variadic]
scons_p_head' [in fintype_variadic]
scons_comp [in fintype_variadic]
scons_eta_id [in fintype_variadic]
scons_eta [in fintype_variadic]
setoid_crutch [in Chapter4.soundness]
size_ind [in header_extensible]
sn [in Chapter9.sn]
SN_sn [in Chapter9.sn_raamsdonk]
sn_app_neutral [in Chapter9.sn_raamsdonk]
sn_confluence [in Chapter9.sn_raamsdonk]
sn_subst_tm [in Chapter9.sn_raamsdonk]
sn_appL [in Chapter9.sn_raamsdonk]
sn_mstep [in Chapter9.sn_raamsdonk]
sn_fundamental_var [in Chapter9.sn_var]
sn_fundamental [in Chapter9.sn]
sn_lam [in Chapter9.sn_mod]
sn_subst [in Chapter4.termination]
sn_exp [in Chapter4.termination]
sn_uexp [in Chapter4.termination]
sn_uexp_comp [in Chapter4.termination]
sn_uexp_shift [in Chapter4.termination]
sn_pstep_shift [in Chapter4.termination]
sn_leaf_Ren [in Chapter4.termination]
sn_leaf_pair [in Chapter4.termination]
sn_leaf_Singleton [in Chapter4.termination]
sn_leaf_Term [in Chapter4.termination]
sn_split [in Chapter4.termination]
sn_split_term [in Chapter4.termination]
sn_split_pair [in Chapter4.termination]
sn_split_singleton [in Chapter4.termination]
sn_pair' [in Chapter4.termination]
sn_CCompR' [in Chapter4.termination]
sn_CCompL' [in Chapter4.termination]
sn_pairR' [in Chapter4.termination]
sn_pairL' [in Chapter4.termination]
sn_CLam [in Chapter4.termination]
sn_zero' [in Chapter4.termination]
sn_pair [in Chapter4.termination]
sn_lam [in Chapter4.termination]
sn_zero [in Chapter4.termination]
sn_uquiv_red_eq [in Chapter4.termination]
sn_uquiv_red [in Chapter4.termination]
sn_sub [in Chapter4.termination]
sn_sub_comp [in Chapter4.termination]
sn_sub_pair [in Chapter4.termination]
sn_sub_lam [in Chapter4.termination]
sn_uquiv_equiv_subst [in Chapter4.termination]
sn_uquiv_equiv [in Chapter4.termination]
sn_plus [in ARS]
sn_forward_star [in ARS]
sn_orR [in ARS]
sn_orL [in ARS]
sn_morphism [in ARS]
SN.weak [in Chapter9.girard]
some_none_explosion [in header_extensible]
Some_inj [in header_extensible]
star_trans [in Chapter9.defs]
star_appR [in Chapter9.sn_lam]
star_appL [in Chapter9.sn_lam]
star_If1 [in Chapter9.sn_bool]
star_plus2 [in Chapter9.sn_arith]
star_plus1 [in Chapter9.sn_arith]
star_CompR [in Chapter4.sigmacalculus]
star_CompL [in Chapter4.sigmacalculus]
star_ConsR [in Chapter4.sigmacalculus]
star_ConsL [in Chapter4.sigmacalculus]
star_InstR [in Chapter4.sigmacalculus]
star_InstL [in Chapter4.sigmacalculus]
star_Lam [in Chapter4.sigmacalculus]
star_AppR [in Chapter4.sigmacalculus]
star_AppL [in Chapter4.sigmacalculus]
star_plus [in ARS]
star_hom [in ARS]
star_img [in ARS]
star_trans [in ARS]
star1 [in ARS]
stepBeta' [in Chapter9.sn_lam]
step_inst_var [in Chapter9.sn_var]
step_anti_renaming_var [in Chapter9.sn_var]
step_naturality [in Chapter9.reduction]
step_inst [in Chapter9.reduction]
step_beta' [in Chapter9.reduction]
step_typing [in Chapter9.variadic_preservation]
step_inst [in Chapter9.variadic_preservation]
step_beta' [in Chapter9.variadic_preservation]
strong_normalisation [in Chapter9.girard]
sub_substitution [in Chapter10.POPLMark22]
sub_trans [in Chapter10.POPLMark22]
sub_trans' [in Chapter10.POPLMark22]
sub_narrow [in Chapter10.POPLMark22]
sub_weak1 [in Chapter10.POPLMark22]
sub_weak [in Chapter10.POPLMark22]
sub_rec [in Chapter10.POPLMark22]
sub_substitution [in Chapter10.POPLMark21]
sub_trans [in Chapter10.POPLMark21]
sub_trans' [in Chapter10.POPLMark21]
sub_narrow [in Chapter10.POPLMark21]
sub_weak1 [in Chapter10.POPLMark21]
sub_weak [in Chapter10.POPLMark21]
sub_rec [in Chapter10.POPLMark21]
sub_substitution [in Chapter10.POPLMark1]
sub_trans [in Chapter10.POPLMark1]
sub_trans' [in Chapter10.POPLMark1]
sub_narrow [in Chapter10.POPLMark1]
sub_weak1 [in Chapter10.POPLMark1]
sub_weak [in Chapter10.POPLMark1]
sub_refl [in Chapter10.POPLMark1]
sysf_cbv.step_substitutive [in Chapter6.reductions]
T
transitivity_ren [in Chapter10.POPLMark22]transitivity_proj [in Chapter10.POPLMark22]
transitivity_ren [in Chapter10.POPLMark21]
transitivity_proj [in Chapter10.POPLMark21]
transitivity_ren [in Chapter10.POPLMark1]
transitivity_proj [in Chapter10.POPLMark1]
type_unique [in Chapter9.equivalence]
typing_inst [in Chapter9.preservation]
typing_ren [in Chapter9.preservation]
typing_inst [in Chapter9.variadic_preservation]
typing_ren [in Chapter9.variadic_preservation]
ty_inv_tabs [in Chapter10.POPLMark22]
ty_subst [in Chapter10.POPLMark22]
ty_inv_rec [in Chapter10.POPLMark22]
ty_inv_abs [in Chapter10.POPLMark22]
ty_rec [in Chapter10.POPLMark22]
ty_var' [in Chapter9.variadic_preservation]
ty_inv_tabs [in Chapter10.POPLMark21]
ty_subst [in Chapter10.POPLMark21]
ty_inv_rec [in Chapter10.POPLMark21]
ty_inv_abs [in Chapter10.POPLMark21]
ty_rec [in Chapter10.POPLMark21]
ty_inv_tabs [in Chapter10.POPLMark1]
ty_subst [in Chapter10.POPLMark1]
ty_inv_abs [in Chapter10.POPLMark1]
T_Var' [in Chapter10.POPLMark22]
T_Var' [in Chapter10.POPLMark21]
U
unique_update [in Chapter10.POPLMark22]unique_spec [in Chapter10.POPLMark22]
unique_map [in Chapter10.POPLMark22]
unique_update [in Chapter10.POPLMark21]
unique_spec [in Chapter10.POPLMark21]
unique_map [in Chapter10.POPLMark21]
update_char [in Chapter10.POPLMark22]
update_char [in Chapter10.POPLMark21]
up_ren_ren [in unscoped]
up_ren_ren_p [in fintype]
up_ren_ren [in fintype]
up_ren_ren_p [in fintype_variadic]
up_ren_ren [in fintype_variadic]
up_ren_ext [in Chapter9.sn_mod]
uquiv_plus_compR [in Chapter4.termination]
uquiv_plus_compL [in Chapter4.termination]
uquiv_plus_pairR [in Chapter4.termination]
uquiv_plus_pairL [in Chapter4.termination]
uquiv_plus_lam [in Chapter4.termination]
uquiv_star_compR [in Chapter4.termination]
uquiv_star_compL [in Chapter4.termination]
uquiv_star_pairR [in Chapter4.termination]
uquiv_star_pairL [in Chapter4.termination]
uquiv_star_lam [in Chapter4.termination]
V
value_anti_renaming_lam [in Chapter9.sn]value_anti [in Chapter9.reduction]
val_inclusion [in Chapter9.sn_var]
val_inclusion [in Chapter9.wn]
varLRen_tm [in Chapter3.utlc_scoped]
varLRen_tm [in Chapter6.variadic_list]
varLRen_exp_var [in Chapter7.expressions]
varLRen_tm [in Chapter6.variadic_fin]
varLRen_vl [in Chapter6.sysf_cbv]
varLRen_ty [in Chapter6.sysf_cbv]
varLRen_tm [in Chapter9.stlc]
varLRen_tm [in Chapter6.utlc_pairs]
varLRen_tm [in Chapter3.utlc_pure]
varLRen_tm [in Chapter10.sysf]
varLRen_ty [in Chapter10.sysf]
varLRen_chan [in Chapter6.picalculus]
varLRen_ty [in Chapter6.recty]
varLRen_tm [in Chapter10.sysf_pat]
varLRen_ty [in Chapter10.sysf_pat]
varL_tm [in Chapter3.utlc_scoped]
varL_tm [in Chapter6.variadic_list]
varL_exp_var [in Chapter7.expressions]
varL_tm [in Chapter6.variadic_fin]
varL_vl [in Chapter6.sysf_cbv]
varL_ty [in Chapter6.sysf_cbv]
varL_tm [in Chapter9.stlc]
varL_tm [in Chapter6.utlc_pairs]
varL_tm [in Chapter6.fol]
varL_exp [in Chapter9.sn_lam]
varL_tm [in Chapter3.utlc_pure]
varL_tm [in Chapter10.sysf]
varL_ty [in Chapter10.sysf]
varL_ty [in Chapter6.recty]
varL_tm [in Chapter10.sysf_pat]
varL_ty [in Chapter10.sysf_pat]
W
whnf_anti_renaming_var [in Chapter9.sn_var]whnf_anti_renaming_lam [in Chapter9.sn_lam]
whnf_anti_renaming_bool [in Chapter9.sn_bool]
whnf_anti_renaming_arith [in Chapter9.sn_arith]
whr_ren [in Chapter9.equivalence]
wn [in Chapter9.sn_mod]
wn_fundamental_var [in Chapter9.sn_var]
wn_fundamental_lam [in Chapter9.wn]
Constructor Index
A
ab [in Chapter7.expressions]abs [in Chapter10.sysf]
abs [in Chapter10.sysf_pat]
alg_app [in Chapter9.equivalence]
alg_var [in Chapter9.equivalence]
alg_arr [in Chapter9.equivalence]
alg_base [in Chapter9.equivalence]
all [in Chapter6.sysf_cbv]
all [in Chapter6.fol]
all [in Chapter10.sysf]
all [in Chapter6.recty]
all [in Chapter10.sysf_pat]
app [in Chapter3.utlc_scoped]
app [in Chapter6.variadic_list]
app [in Chapter7.expressions]
app [in Chapter6.variadic_fin]
app [in Chapter6.sysf_cbv]
app [in Chapter9.stlc]
app [in Chapter6.utlc_pairs]
app [in Chapter3.utlc_pure]
app [in Chapter10.sysf]
App [in Chapter4.sigmacalculus]
app [in Chapter10.sysf_pat]
arr [in Chapter7.expressions]
arr [in Chapter6.sysf_cbv]
arr [in Chapter9.equivalence]
arr [in Chapter10.sysf]
arr [in Chapter6.recty]
arr [in Chapter9.variadic_preservation]
arr [in Chapter10.sysf_pat]
atom [in Chapter6.fol]
B
Bang [in Chapter6.picalculus]Base [in Chapter9.stlc]
Base [in Chapter9.equivalence]
Base [in Chapter9.variadic_preservation]
BaseClosure [in Chapter4.termination]
beta [in Chapter9.equivalence]
boolTy [in Chapter7.expressions]
C
CCompL [in Chapter4.termination]CCompR [in Chapter4.termination]
CLam [in Chapter4.termination]
comp [in Chapter4.termination]
Comp [in Chapter4.sigmacalculus]
compRelPair [in Chapter4.termination]
compRelSingleton [in Chapter4.termination]
compRelTerm [in Chapter4.termination]
CompRen [in Chapter4.termination]
comp_I [in Chapter4.sigmacalculus]
comp_cons [in Chapter4.sigmacalculus]
comp_assoc [in Chapter4.sigmacalculus]
comp_right [in Chapter4.sigmacalculus]
comp_left [in Chapter4.sigmacalculus]
comp_S [in Chapter4.sigmacalculus]
Cons [in Chapter4.sigmacalculus]
constBool [in Chapter7.expressions]
constNat [in Chapter7.expressions]
cons_eta [in Chapter4.sigmacalculus]
CPair [in Chapter4.termination]
CZero [in Chapter4.termination]
D
DecApp [in Chapter9.equivalence]DecBeta [in Chapter9.equivalence]
DecExt [in Chapter9.equivalence]
DecLam [in Chapter9.equivalence]
DecSym [in Chapter9.equivalence]
DecTrans [in Chapter9.equivalence]
DecVar [in Chapter9.equivalence]
E
equiv_consR [in Chapter4.sigmacalculus]equiv_consL [in Chapter4.sigmacalculus]
equiv_compR [in Chapter4.sigmacalculus]
equiv_compL [in Chapter4.sigmacalculus]
equiv_instR [in Chapter4.sigmacalculus]
equiv_instL [in Chapter4.sigmacalculus]
equiv_lam [in Chapter4.sigmacalculus]
equiv_appR [in Chapter4.sigmacalculus]
equiv_appL [in Chapter4.sigmacalculus]
equiv_inst_inst [in Chapter4.sigmacalculus]
equiv_inst_I [in Chapter4.sigmacalculus]
equiv_Zero [in Chapter4.sigmacalculus]
equiv_Lam [in Chapter4.sigmacalculus]
equiv_App [in Chapter4.sigmacalculus]
E_LetL [in Chapter10.POPLMark22]
E_Rec [in Chapter10.POPLMark22]
E_Proj [in Chapter10.POPLMark22]
E_TyFun [in Chapter10.POPLMark22]
E_appArg [in Chapter10.POPLMark22]
E_appFun [in Chapter10.POPLMark22]
E_RecProj [in Chapter10.POPLMark22]
E_Tapptabs [in Chapter10.POPLMark22]
E_appabs [in Chapter10.POPLMark22]
E_strong_In [in Chapter9.sn_var]
E_strong_In [in Chapter9.sn]
E_LetL [in Chapter10.POPLMark21]
E_Rec [in Chapter10.POPLMark21]
E_Proj [in Chapter10.POPLMark21]
E_TyFun [in Chapter10.POPLMark21]
E_appArg [in Chapter10.POPLMark21]
E_appFun [in Chapter10.POPLMark21]
E_RecProj [in Chapter10.POPLMark21]
E_Tapptabs [in Chapter10.POPLMark21]
E_appabs [in Chapter10.POPLMark21]
E_TyFun [in Chapter10.POPLMark1]
E_appArg [in Chapter10.POPLMark1]
E_appFun [in Chapter10.POPLMark1]
E_Tapptabs [in Chapter10.POPLMark1]
E_appabs [in Chapter10.POPLMark1]
F
fal [in Chapter6.fol]features [in header_metacoq]
Fun [in Chapter9.stlc]
G
GenCons [in header_metacoq]genCons [in header_metacoq]
GenNil [in header_metacoq]
genNil [in header_metacoq]
H
hasty_lam [in Chapter9.sn_lam]hasty_app [in Chapter9.sn_lam]
hasty_If [in Chapter9.sn_bool]
hasty_ConstBool [in Chapter9.sn_bool]
hasty_plus [in Chapter9.sn_arith]
hasty_ConstNat [in Chapter9.sn_arith]
Hole [in Chapter4.termination]
I
I [in Chapter4.sigmacalculus]ids [in unscoped]
ids [in fintype]
ids [in fintype_variadic]
If [in Chapter7.expressions]
imp [in tactics]
imprev [in tactics]
In [in Chapter6.picalculus]
Inl [in ARS]
inl_step_arith [in Chapter9.sn_mod]
inl_step_bool [in Chapter9.sn_mod]
inl_step_lam [in Chapter9.sn_mod]
inl_step_var [in Chapter9.sn_mod]
inl_has_ty_arith [in Chapter9.sn_mod]
inl_has_ty_bool [in Chapter9.sn_mod]
inl_has_ty_lam [in Chapter9.sn_mod]
inl_has_ty_var [in Chapter9.sn_mod]
Inr [in ARS]
Inst [in Chapter4.sigmacalculus]
In_exp_arith [in Chapter7.expressions]
In_exp_bool [in Chapter7.expressions]
In_exp_lam [in Chapter7.expressions]
In_exp_var [in Chapter7.expressions]
In_ty_arith [in Chapter7.expressions]
In_ty_bool [in Chapter7.expressions]
In_ty_lam [in Chapter7.expressions]
L
lam [in Chapter3.utlc_scoped]lam [in Chapter6.variadic_list]
lam [in Chapter6.variadic_fin]
lam [in Chapter6.sysf_cbv]
lam [in Chapter9.stlc]
lam [in Chapter6.utlc_pairs]
lam [in Chapter3.utlc_pure]
lam [in Chapter4.termination]
Lam [in Chapter4.sigmacalculus]
leafPairL [in Chapter4.termination]
leafPairR [in Chapter4.termination]
leafSingleton [in Chapter4.termination]
leafTermStep [in Chapter4.termination]
letpat [in Chapter10.sysf_pat]
letpat_eval [in Chapter10.POPLMark22]
letpat_ty [in Chapter10.POPLMark22]
letpat_eval [in Chapter10.POPLMark21]
letpat_ty [in Chapter10.POPLMark21]
M
make_Bundle [in header_extensible]matchpair [in Chapter6.utlc_pairs]
mwhrR [in Chapter9.equivalence]
mwhrS [in Chapter9.equivalence]
N
natTy [in Chapter7.expressions]Nil [in Chapter6.picalculus]
O
Out [in Chapter6.picalculus]P
pair [in Chapter6.utlc_pairs]Pair [in Chapter4.termination]
pair [in Chapter4.termination]
PairRen [in Chapter4.termination]
PairRenaming [in Chapter4.termination]
Par [in Chapter6.picalculus]
patlist [in Chapter10.sysf_pat]
patPairL [in Chapter4.termination]
patPairR [in Chapter4.termination]
patSingleton [in Chapter4.termination]
patSplitApp [in Chapter4.termination]
patSplitComp [in Chapter4.termination]
patSplitLambda [in Chapter4.termination]
patvar [in Chapter10.sysf_pat]
plus [in Chapter7.expressions]
plus [in Chapter6.fol]
plusR [in ARS]
polyadic.beta [in Chapter6.reductions]
polyadic.beta_match [in Chapter6.reductions]
pred [in Chapter6.fol]
proj [in Chapter10.sysf_pat]
R
rectm [in Chapter10.sysf_pat]recty [in Chapter6.recty]
recty [in Chapter10.sysf_pat]
redsn_app [in Chapter9.sn_raamsdonk]
redsn_beta [in Chapter9.sn_raamsdonk]
RenTerm [in Chapter4.termination]
ren1 [in unscoped]
ren1 [in fintype]
ren1 [in fintype_variadic]
ren2 [in unscoped]
ren2 [in fintype]
ren2 [in fintype_variadic]
ren3 [in unscoped]
ren3 [in fintype]
ren3 [in fintype_variadic]
ren4 [in unscoped]
ren4 [in fintype]
ren4 [in fintype_variadic]
ren5 [in unscoped]
ren5 [in fintype]
ren5 [in fintype_variadic]
Res [in Chapter6.picalculus]
S
SAbs [in Chapter9.sn_raamsdonk]SApp [in Chapter9.sn_raamsdonk]
SAppl [in Chapter9.sn_raamsdonk]
SA_rec [in Chapter10.POPLMark22]
SA_all [in Chapter10.POPLMark22]
SA_arrow [in Chapter10.POPLMark22]
SA_Trans [in Chapter10.POPLMark22]
SA_Refl [in Chapter10.POPLMark22]
SA_top [in Chapter10.POPLMark22]
SA_rec [in Chapter10.POPLMark21]
SA_all [in Chapter10.POPLMark21]
SA_arrow [in Chapter10.POPLMark21]
SA_Trans [in Chapter10.POPLMark21]
SA_Refl [in Chapter10.POPLMark21]
SA_top [in Chapter10.POPLMark21]
SA_all [in Chapter10.POPLMark1]
SA_arrow [in Chapter10.POPLMark1]
SA_Trans [in Chapter10.POPLMark1]
SA_Refl [in Chapter10.POPLMark1]
SA_top [in Chapter10.POPLMark1]
SBeta [in Chapter9.sn_raamsdonk]
Singleton [in Chapter4.termination]
SingletonRen [in Chapter4.termination]
SNeu [in Chapter9.sn_raamsdonk]
SNI [in Chapter9.defs]
SNI [in ARS]
SRed [in Chapter9.sn_raamsdonk]
srefl [in Chapter9.defs]
starR [in ARS]
starSE [in ARS]
stepAppL [in Chapter9.sn_lam]
stepAppR [in Chapter9.sn_lam]
stepBeta [in Chapter9.sn_lam]
stepIfBeta [in Chapter9.sn_bool]
stepIf1 [in Chapter9.sn_bool]
stepIf2 [in Chapter9.sn_bool]
stepIf3 [in Chapter9.sn_bool]
stepLam [in Chapter9.sn_lam]
stepPlus [in Chapter9.sn_arith]
stepPlus1 [in Chapter9.sn_arith]
stepPlus2 [in Chapter9.sn_arith]
step_appR [in Chapter9.reduction]
step_appL [in Chapter9.reduction]
step_abs [in Chapter9.reduction]
step_beta [in Chapter9.reduction]
step_appL [in Chapter9.variadic_preservation]
step_abs [in Chapter9.variadic_preservation]
step_beta [in Chapter9.variadic_preservation]
strans [in Chapter9.defs]
subst1 [in unscoped]
subst1 [in fintype]
subst1 [in fintype_variadic]
subst2 [in unscoped]
subst2 [in fintype]
subst2 [in fintype_variadic]
subst3 [in unscoped]
subst3 [in fintype]
subst3 [in fintype_variadic]
subst4 [in unscoped]
subst4 [in fintype]
subst4 [in fintype_variadic]
subst5 [in unscoped]
subst5 [in fintype]
subst5 [in fintype_variadic]
subterm_rel [in header_metacoq]
Succ [in Chapter4.sigmacalculus]
SVar [in Chapter9.sn_raamsdonk]
sysf_cbv.Beta [in Chapter6.reductions]
sysf_cbv.beta [in Chapter6.reductions]
T
tabs [in Chapter10.sysf]tabs [in Chapter10.sysf_pat]
tapp [in Chapter6.sysf_cbv]
tapp [in Chapter10.sysf]
tapp [in Chapter10.sysf_pat]
Term [in Chapter4.termination]
tlam [in Chapter6.sysf_cbv]
top [in Chapter10.sysf]
top [in Chapter6.recty]
top [in Chapter10.sysf_pat]
ty_app [in Chapter9.preservation]
ty_abs [in Chapter9.preservation]
ty_var_tm [in Chapter9.preservation]
ty_app [in Chapter9.variadic_preservation]
ty_abs [in Chapter9.variadic_preservation]
ty_var [in Chapter9.variadic_preservation]
T_Sub [in Chapter10.POPLMark22]
T_Proj [in Chapter10.POPLMark22]
T_Rcd [in Chapter10.POPLMark22]
T_Tapp [in Chapter10.POPLMark22]
T_tabs [in Chapter10.POPLMark22]
T_app [in Chapter10.POPLMark22]
T_abs [in Chapter10.POPLMark22]
T_Var [in Chapter10.POPLMark22]
T_Sub [in Chapter10.POPLMark21]
T_Proj [in Chapter10.POPLMark21]
T_Rcd [in Chapter10.POPLMark21]
T_Tapp [in Chapter10.POPLMark21]
T_tabs [in Chapter10.POPLMark21]
T_app [in Chapter10.POPLMark21]
T_abs [in Chapter10.POPLMark21]
T_Var [in Chapter10.POPLMark21]
T_Sub [in Chapter10.POPLMark1]
T_Tapp [in Chapter10.POPLMark1]
T_tabs [in Chapter10.POPLMark1]
T_app [in Chapter10.POPLMark1]
T_abs [in Chapter10.POPLMark1]
T_Var [in Chapter10.POPLMark1]
U
ucons [in Chapter10.POPLMark22]ucons [in Chapter10.POPLMark21]
unil [in Chapter10.POPLMark22]
unil [in Chapter10.POPLMark21]
up_tm [in Chapter3.utlc_scoped]
up_tm [in Chapter6.variadic_list]
up_exp [in Chapter7.expressions]
up_tm [in Chapter6.variadic_fin]
up_vl [in Chapter6.sysf_cbv]
up_ty [in Chapter6.sysf_cbv]
up_tm [in Chapter9.stlc]
up_tm [in Chapter6.utlc_pairs]
up_tm [in Chapter6.fol]
up_tm [in Chapter3.utlc_pure]
up_tm [in Chapter10.sysf]
up_ty [in Chapter10.sysf]
up_chan [in Chapter6.picalculus]
up_ty [in Chapter6.recty]
up_tm [in Chapter10.sysf_pat]
up_ty [in Chapter10.sysf_pat]
uquivAssoc [in Chapter4.termination]
uquivCompL [in Chapter4.termination]
uquivCompPair [in Chapter4.termination]
uquivCompR [in Chapter4.termination]
uquivLambda [in Chapter4.termination]
uquivLamC [in Chapter4.termination]
uquivPairL [in Chapter4.termination]
uquivPairR [in Chapter4.termination]
uquivSubCompL [in Chapter4.termination]
uquivSubCompR [in Chapter4.termination]
uquivSubLam [in Chapter4.termination]
uquivSubPairL [in Chapter4.termination]
uquivSubPairR [in Chapter4.termination]
V
Value_rec [in Chapter10.POPLMark22]Value_tabs [in Chapter10.POPLMark22]
Value_abs [in Chapter10.POPLMark22]
Value_rec [in Chapter10.POPLMark21]
Value_tabs [in Chapter10.POPLMark21]
Value_abs [in Chapter10.POPLMark21]
Value_tabs [in Chapter10.POPLMark1]
Value_abs [in Chapter10.POPLMark1]
var_tm [in Chapter3.utlc_scoped]
var_tm [in Chapter6.variadic_list]
var_exp_var [in Chapter7.expressions]
var_tm [in Chapter6.variadic_fin]
var_vl [in Chapter6.sysf_cbv]
var_ty [in Chapter6.sysf_cbv]
var_tm [in Chapter9.stlc]
var_has_ty [in Chapter9.sn_var]
var_tm [in Chapter6.utlc_pairs]
var_tm [in Chapter6.fol]
var_tm [in Chapter3.utlc_pure]
var_tm [in Chapter10.sysf]
var_ty [in Chapter10.sysf]
var_chan [in Chapter6.picalculus]
var_ty [in Chapter6.recty]
var_subst [in Chapter4.sigmacalculus]
var_exp [in Chapter4.sigmacalculus]
var_tm [in Chapter10.sysf_pat]
var_ty [in Chapter10.sysf_pat]
vt [in Chapter6.sysf_cbv]
vt [in Chapter10.sysf]
W
whrapp [in Chapter9.equivalence]Z
zero [in Chapter4.termination]Zero [in Chapter4.sigmacalculus]
ZeroRen [in Chapter4.termination]
Projection Index
F
features [in header_metacoq]I
ids [in unscoped]ids [in fintype]
ids [in fintype_variadic]
imp [in tactics]
imprev [in tactics]
in_rel [in header_metacoq]
in_subtype [in header_metacoq]
R
ren1 [in unscoped]ren1 [in fintype]
ren1 [in fintype_variadic]
ren2 [in unscoped]
ren2 [in fintype]
ren2 [in fintype_variadic]
ren3 [in unscoped]
ren3 [in fintype]
ren3 [in fintype_variadic]
ren4 [in unscoped]
ren4 [in fintype]
ren4 [in fintype_variadic]
ren5 [in unscoped]
ren5 [in fintype]
ren5 [in fintype_variadic]
retract_tight [in header_extensible]
retract_works [in header_extensible]
retract_R [in header_extensible]
retract_I [in header_extensible]
S
subst1 [in unscoped]subst1 [in fintype]
subst1 [in fintype_variadic]
subst2 [in unscoped]
subst2 [in fintype]
subst2 [in fintype_variadic]
subst3 [in unscoped]
subst3 [in fintype]
subst3 [in fintype_variadic]
subst4 [in unscoped]
subst4 [in fintype]
subst4 [in fintype_variadic]
subst5 [in unscoped]
subst5 [in fintype]
subst5 [in fintype_variadic]
subterm_rel [in header_metacoq]
U
up_tm [in Chapter3.utlc_scoped]up_tm [in Chapter6.variadic_list]
up_exp [in Chapter7.expressions]
up_tm [in Chapter6.variadic_fin]
up_vl [in Chapter6.sysf_cbv]
up_ty [in Chapter6.sysf_cbv]
up_tm [in Chapter9.stlc]
up_tm [in Chapter6.utlc_pairs]
up_tm [in Chapter6.fol]
up_tm [in Chapter3.utlc_pure]
up_tm [in Chapter10.sysf]
up_ty [in Chapter10.sysf]
up_chan [in Chapter6.picalculus]
up_ty [in Chapter6.recty]
up_tm [in Chapter10.sysf_pat]
up_ty [in Chapter10.sysf_pat]
Inductive Index
A
algeq [in Chapter9.equivalence]algeqNeu [in Chapter9.equivalence]
C
chan [in Chapter6.picalculus]closure [in Chapter4.termination]
compRel [in Chapter4.termination]
ctx [in Chapter4.termination]
D
decleq [in Chapter9.equivalence]E
equiv_axiom_subst [in Chapter4.sigmacalculus]equiv_axiom [in Chapter4.sigmacalculus]
eval [in Chapter10.POPLMark22]
eval [in Chapter10.POPLMark21]
eval [in Chapter10.POPLMark1]
exp [in Chapter7.expressions]
exp [in Chapter4.sigmacalculus]
exp_var [in Chapter7.expressions]
exp_bool [in Chapter7.expressions]
exp_arith [in Chapter7.expressions]
exp_lam [in Chapter7.expressions]
E_strong' [in Chapter9.sn_var]
E_strong' [in Chapter9.sn]
F
form [in Chapter6.fol]G
GenList [in header_metacoq]genList [in header_metacoq]
H
has_ty [in Chapter10.POPLMark22]has_ty_var [in Chapter9.sn_var]
has_type [in Chapter9.preservation]
has_ty_lam [in Chapter9.sn_lam]
has_ty [in Chapter9.sn_mod]
has_ty_bool [in Chapter9.sn_bool]
has_ty_arith [in Chapter9.sn_arith]
has_type [in Chapter9.variadic_preservation]
has_ty [in Chapter10.POPLMark21]
has_features [in header_metacoq]
has_ty [in Chapter10.POPLMark1]
I
Imp [in tactics]ImpRev [in tactics]
L
leaf_step [in Chapter4.termination]M
mwhr [in Chapter9.equivalence]O
Or [in ARS]P
pat [in Chapter4.termination]pat [in Chapter10.sysf_pat]
plus [in ARS]
polyadic.step [in Chapter6.reductions]
proc [in Chapter6.picalculus]
pstep [in Chapter4.termination]
R
redsn [in Chapter9.sn_raamsdonk]Ren [in Chapter4.termination]
RenExp [in Chapter4.termination]
Ren1 [in unscoped]
Ren1 [in fintype]
Ren1 [in fintype_variadic]
Ren2 [in unscoped]
Ren2 [in fintype]
Ren2 [in fintype_variadic]
Ren3 [in unscoped]
Ren3 [in fintype]
Ren3 [in fintype_variadic]
Ren4 [in unscoped]
Ren4 [in fintype]
Ren4 [in fintype_variadic]
Ren5 [in unscoped]
Ren5 [in fintype]
Ren5 [in fintype_variadic]
S
SN [in Chapter9.sn_raamsdonk]sn [in Chapter9.defs]
sn [in ARS]
SNe [in Chapter9.sn_raamsdonk]
SNRed [in Chapter9.sn_raamsdonk]
split [in Chapter4.termination]
star [in Chapter9.defs]
star [in ARS]
step [in Chapter9.sn_mod]
step [in Chapter9.reduction]
step [in Chapter9.variadic_preservation]
step_var [in Chapter9.sn_var]
step_lam [in Chapter9.sn_lam]
step_bool [in Chapter9.sn_bool]
step_arith [in Chapter9.sn_arith]
sub [in Chapter10.POPLMark22]
sub [in Chapter4.termination]
sub [in Chapter10.POPLMark21]
sub [in Chapter10.POPLMark1]
subst_exp [in Chapter4.sigmacalculus]
Subst1 [in unscoped]
Subst1 [in fintype]
Subst1 [in fintype_variadic]
Subst2 [in unscoped]
Subst2 [in fintype]
Subst2 [in fintype_variadic]
Subst3 [in unscoped]
Subst3 [in fintype]
Subst3 [in fintype_variadic]
Subst4 [in unscoped]
Subst4 [in fintype]
Subst4 [in fintype_variadic]
Subst5 [in unscoped]
Subst5 [in fintype]
Subst5 [in fintype_variadic]
subtermC [in header_metacoq]
sysf_cbv.step [in Chapter6.reductions]
T
tm [in Chapter3.utlc_scoped]tm [in Chapter6.variadic_list]
tm [in Chapter6.variadic_fin]
tm [in Chapter6.sysf_cbv]
tm [in Chapter9.stlc]
tm [in Chapter6.utlc_pairs]
tm [in Chapter6.fol]
tm [in Chapter3.utlc_pure]
tm [in Chapter10.sysf]
tm [in Chapter10.sysf_pat]
ty [in Chapter7.expressions]
ty [in Chapter6.sysf_cbv]
ty [in Chapter9.stlc]
ty [in Chapter9.equivalence]
ty [in Chapter10.sysf]
ty [in Chapter6.recty]
ty [in Chapter9.variadic_preservation]
ty [in Chapter10.sysf_pat]
ty_arith [in Chapter7.expressions]
ty_bool [in Chapter7.expressions]
ty_lam [in Chapter7.expressions]
U
uexp [in Chapter4.termination]unique [in Chapter10.POPLMark22]
unique [in Chapter10.POPLMark21]
Up_tm [in Chapter3.utlc_scoped]
Up_tm [in Chapter6.variadic_list]
Up_exp [in Chapter7.expressions]
Up_tm [in Chapter6.variadic_fin]
Up_vl [in Chapter6.sysf_cbv]
Up_ty [in Chapter6.sysf_cbv]
Up_tm [in Chapter9.stlc]
Up_tm [in Chapter6.utlc_pairs]
Up_tm [in Chapter6.fol]
Up_tm [in Chapter3.utlc_pure]
Up_tm [in Chapter10.sysf]
Up_ty [in Chapter10.sysf]
Up_chan [in Chapter6.picalculus]
Up_ty [in Chapter6.recty]
Up_tm [in Chapter10.sysf_pat]
Up_ty [in Chapter10.sysf_pat]
V
value [in Chapter10.POPLMark22]value [in Chapter10.POPLMark21]
value [in Chapter10.POPLMark1]
Var [in unscoped]
Var [in fintype]
Var [in fintype_variadic]
vl [in Chapter6.sysf_cbv]
W
whr [in Chapter9.equivalence]Instance Index
E
exp_features [in Chapter9.sn_mod]H
has_ty_features [in Chapter9.sn_mod]I
idsRen [in unscoped]N
nat_subterm' [in header_metacoq]R
Ren_tm [in Chapter3.utlc_scoped]Ren_tm [in Chapter6.variadic_list]
Ren_exp [in Chapter7.expressions]
Ren_tm [in Chapter6.variadic_fin]
Ren_vl [in Chapter6.sysf_cbv]
Ren_tm [in Chapter6.sysf_cbv]
Ren_ty [in Chapter6.sysf_cbv]
Ren_tm [in Chapter9.stlc]
Ren_tm [in Chapter6.utlc_pairs]
Ren_tm [in Chapter3.utlc_pure]
Ren_tm [in Chapter10.sysf]
Ren_ty [in Chapter10.sysf]
Ren_proc [in Chapter6.picalculus]
Ren_chan [in Chapter6.picalculus]
Ren_ty [in Chapter6.recty]
Ren_tm [in Chapter10.sysf_pat]
Ren_pat [in Chapter10.sysf_pat]
Ren_ty [in Chapter10.sysf_pat]
retract_exp_var_exp [in Chapter7.expressions]
retract_exp_bool_exp [in Chapter7.expressions]
retract_exp_arith_exp [in Chapter7.expressions]
retract_exp_lam_exp [in Chapter7.expressions]
retract_ty_arith_ty [in Chapter7.expressions]
retract_ty_bool_ty [in Chapter7.expressions]
retract_ty_lam_ty [in Chapter7.expressions]
retract_has_ty_rev_instance [in Chapter9.sn_var]
retract_has_ty_instance [in Chapter9.sn_var]
retract_step_rev_instance [in Chapter9.sn_lam]
retract_step_instance [in Chapter9.sn_lam]
retract_has_ty_rev_instance [in Chapter9.sn_lam]
retract_has_ty_instance [in Chapter9.sn_lam]
retract_step_rev_instance [in Chapter9.sn_bool]
retract_step_instance [in Chapter9.sn_bool]
retract_has_ty_rev_instance [in Chapter9.sn_bool]
retract_has_ty_instance [in Chapter9.sn_bool]
retract_step_rev_instance [in Chapter9.sn_arith]
retract_step_instance [in Chapter9.sn_arith]
retract_has_ty_rev_instance [in Chapter9.sn_arith]
retract_has_ty_instance [in Chapter9.sn_arith]
retract_option [in header_extensible]
S
step_features [in Chapter9.sn_mod]Subst_tm [in Chapter3.utlc_scoped]
Subst_tm [in Chapter6.variadic_list]
Subst_exp [in Chapter7.expressions]
Subst_tm [in Chapter6.variadic_fin]
Subst_vl [in Chapter6.sysf_cbv]
Subst_tm [in Chapter6.sysf_cbv]
Subst_ty [in Chapter6.sysf_cbv]
Subst_tm [in Chapter9.stlc]
Subst_tm [in Chapter6.utlc_pairs]
Subst_form [in Chapter6.fol]
Subst_tm [in Chapter6.fol]
Subst_tm [in Chapter3.utlc_pure]
Subst_tm [in Chapter10.sysf]
Subst_ty [in Chapter10.sysf]
Subst_ty [in Chapter6.recty]
Subst_tm [in Chapter10.sysf_pat]
Subst_pat [in Chapter10.sysf_pat]
Subst_ty [in Chapter10.sysf_pat]
T
ty_features [in Chapter9.sn_mod]U
Up_tm_tm [in Chapter3.utlc_scoped]Up_tm_tm [in Chapter6.variadic_list]
Up_exp_exp [in Chapter7.expressions]
Up_tm_tm [in Chapter6.variadic_fin]
Up_vl_vl [in Chapter6.sysf_cbv]
Up_vl_ty [in Chapter6.sysf_cbv]
Up_ty_vl [in Chapter6.sysf_cbv]
Up_ty_ty [in Chapter6.sysf_cbv]
Up_tm_tm [in Chapter9.stlc]
Up_tm_tm [in Chapter6.utlc_pairs]
Up_tm_tm [in Chapter6.fol]
Up_tm_tm [in Chapter3.utlc_pure]
Up_tm_tm [in Chapter10.sysf]
Up_tm_ty [in Chapter10.sysf]
Up_ty_tm [in Chapter10.sysf]
Up_ty_ty [in Chapter10.sysf]
Up_ty_ty [in Chapter6.recty]
Up_tm_tm [in Chapter10.sysf_pat]
Up_tm_ty [in Chapter10.sysf_pat]
Up_ty_tm [in Chapter10.sysf_pat]
Up_ty_ty [in Chapter10.sysf_pat]
V
VarInstance_tm [in Chapter3.utlc_scoped]VarInstance_tm [in Chapter6.variadic_list]
VarInstance_exp_var [in Chapter7.expressions]
VarInstance_tm [in Chapter6.variadic_fin]
VarInstance_vl [in Chapter6.sysf_cbv]
VarInstance_ty [in Chapter6.sysf_cbv]
VarInstance_tm [in Chapter9.stlc]
VarInstance_tm [in Chapter6.utlc_pairs]
VarInstance_tm [in Chapter6.fol]
VarInstance_tm [in Chapter3.utlc_pure]
VarInstance_tm [in Chapter10.sysf]
VarInstance_ty [in Chapter10.sysf]
VarInstance_chan [in Chapter6.picalculus]
VarInstance_ty [in Chapter6.recty]
VarInstance_tm [in Chapter10.sysf_pat]
VarInstance_ty [in Chapter10.sysf_pat]
Section Index
C
chan [in Chapter6.picalculus]D
Definitions [in ARS]E
exp [in Chapter7.expressions]exp_var [in Chapter7.expressions]
exp_bool [in Chapter7.expressions]
exp_arith [in Chapter7.expressions]
exp_lam [in Chapter7.expressions]
F
form [in Chapter6.fol]M
MiniML_var [in Chapter9.sn_var]MiniML_Lambda [in Chapter9.sn_lam]
MiniML_Bool [in Chapter9.sn_bool]
MiniML_Arith [in Chapter9.sn_arith]
P
pat [in Chapter10.sysf_pat]Pattern [in Chapter10.POPLMark22]
Pattern [in Chapter10.POPLMark21]
polyadic.polyadic [in Chapter6.reductions]
proc [in Chapter6.picalculus]
S
sysf_cbv.sysf_cbv [in Chapter6.reductions]T
tm [in Chapter3.utlc_scoped]tm [in Chapter6.variadic_list]
tm [in Chapter6.variadic_fin]
tm [in Chapter9.stlc]
tm [in Chapter6.utlc_pairs]
tm [in Chapter6.fol]
tm [in Chapter3.utlc_pure]
tm [in Chapter10.sysf_pat]
tmvl [in Chapter6.sysf_cbv]
ty [in Chapter7.expressions]
ty [in Chapter6.sysf_cbv]
ty [in Chapter9.stlc]
ty [in Chapter6.recty]
ty [in Chapter10.sysf_pat]
ty_arith [in Chapter7.expressions]
ty_bool [in Chapter7.expressions]
ty_lam [in Chapter7.expressions]
Abbreviation Index
F
fin [in unscoped]I
included [in header_extensible]inj [in header_extensible]
R
retr [in header_extensible]S
sn [in Chapter9.girard]Definition Index
A
ab_ [in Chapter7.expressions]algeqNeu_ind_2 [in Chapter9.equivalence]
algeq_mut_ind [in Chapter9.equivalence]
algeq_ind_2 [in Chapter9.equivalence]
ap [in unscoped]
ap [in fintype]
ap [in fintype_variadic]
apc [in unscoped]
apc [in fintype]
apc [in fintype_variadic]
app_ [in Chapter7.expressions]
arr_ [in Chapter7.expressions]
B
boolTy_ [in Chapter7.expressions]buildImp [in header_metacoq]
C
cand [in Chapter9.girard]cns [in header_metacoq]
cod [in axioms]
cod_comp [in axioms]
cod_ext [in axioms]
cod_id [in axioms]
cod_map [in axioms]
comb_equiv_ind [in Chapter4.sigmacalculus]
comb_exp_ind [in Chapter4.sigmacalculus]
comp [in fintype]
comp [in fintype_variadic]
compose_fixpoint [in header_metacoq]
compRenRen_tm [in Chapter3.utlc_scoped]
compRenRen_tm [in Chapter6.variadic_list]
compRenRen_exp [in Chapter7.expressions]
compRenRen_exp_var [in Chapter7.expressions]
compRenRen_exp_bool [in Chapter7.expressions]
compRenRen_exp_arith [in Chapter7.expressions]
compRenRen_exp_lam [in Chapter7.expressions]
compRenRen_tm [in Chapter6.variadic_fin]
compRenRen_vl [in Chapter6.sysf_cbv]
compRenRen_tm [in Chapter6.sysf_cbv]
compRenRen_ty [in Chapter6.sysf_cbv]
compRenRen_tm [in Chapter9.stlc]
compRenRen_tm [in Chapter6.utlc_pairs]
compRenRen_tm [in Chapter3.utlc_pure]
compRenRen_tm [in Chapter10.sysf]
compRenRen_ty [in Chapter10.sysf]
compRenRen_proc [in Chapter6.picalculus]
compRenRen_chan [in Chapter6.picalculus]
compRenRen_ty [in Chapter6.recty]
compRenRen_tm [in Chapter10.sysf_pat]
compRenRen_pat [in Chapter10.sysf_pat]
compRenRen_ty [in Chapter10.sysf_pat]
compRenSubst_tm [in Chapter3.utlc_scoped]
compRenSubst_tm [in Chapter6.variadic_list]
compRenSubst_exp [in Chapter7.expressions]
compRenSubst_exp_var [in Chapter7.expressions]
compRenSubst_exp_bool [in Chapter7.expressions]
compRenSubst_exp_arith [in Chapter7.expressions]
compRenSubst_exp_lam [in Chapter7.expressions]
compRenSubst_tm [in Chapter6.variadic_fin]
compRenSubst_vl [in Chapter6.sysf_cbv]
compRenSubst_tm [in Chapter6.sysf_cbv]
compRenSubst_ty [in Chapter6.sysf_cbv]
compRenSubst_tm [in Chapter9.stlc]
compRenSubst_tm [in Chapter6.utlc_pairs]
compRenSubst_tm [in Chapter3.utlc_pure]
compRenSubst_tm [in Chapter10.sysf]
compRenSubst_ty [in Chapter10.sysf]
compRenSubst_ty [in Chapter6.recty]
compRenSubst_tm [in Chapter10.sysf_pat]
compRenSubst_pat [in Chapter10.sysf_pat]
compRenSubst_ty [in Chapter10.sysf_pat]
compSubstRen_tm [in Chapter3.utlc_scoped]
compSubstRen_tm [in Chapter6.variadic_list]
compSubstRen_exp [in Chapter7.expressions]
compSubstRen_exp_var [in Chapter7.expressions]
compSubstRen_exp_bool [in Chapter7.expressions]
compSubstRen_exp_arith [in Chapter7.expressions]
compSubstRen_exp_lam [in Chapter7.expressions]
compSubstRen_tm [in Chapter6.variadic_fin]
compSubstRen_vl [in Chapter6.sysf_cbv]
compSubstRen_tm [in Chapter6.sysf_cbv]
compSubstRen_ty [in Chapter6.sysf_cbv]
compSubstRen_tm [in Chapter9.stlc]
compSubstRen_tm [in Chapter6.utlc_pairs]
compSubstRen_tm [in Chapter3.utlc_pure]
compSubstRen_tm [in Chapter10.sysf]
compSubstRen_ty [in Chapter10.sysf]
compSubstRen_ty [in Chapter6.recty]
compSubstRen_tm [in Chapter10.sysf_pat]
compSubstRen_pat [in Chapter10.sysf_pat]
compSubstRen_ty [in Chapter10.sysf_pat]
compSubstSubst_tm [in Chapter3.utlc_scoped]
compSubstSubst_tm [in Chapter6.variadic_list]
compSubstSubst_exp [in Chapter7.expressions]
compSubstSubst_exp_var [in Chapter7.expressions]
compSubstSubst_exp_bool [in Chapter7.expressions]
compSubstSubst_exp_arith [in Chapter7.expressions]
compSubstSubst_exp_lam [in Chapter7.expressions]
compSubstSubst_tm [in Chapter6.variadic_fin]
compSubstSubst_vl [in Chapter6.sysf_cbv]
compSubstSubst_tm [in Chapter6.sysf_cbv]
compSubstSubst_ty [in Chapter6.sysf_cbv]
compSubstSubst_tm [in Chapter9.stlc]
compSubstSubst_tm [in Chapter6.utlc_pairs]
compSubstSubst_form [in Chapter6.fol]
compSubstSubst_tm [in Chapter6.fol]
compSubstSubst_tm [in Chapter3.utlc_pure]
compSubstSubst_tm [in Chapter10.sysf]
compSubstSubst_ty [in Chapter10.sysf]
compSubstSubst_ty [in Chapter6.recty]
compSubstSubst_tm [in Chapter10.sysf_pat]
compSubstSubst_pat [in Chapter10.sysf_pat]
compSubstSubst_ty [in Chapter10.sysf_pat]
confluent [in ARS]
congr_tabs [in Chapter10.sysf]
congr_abs [in Chapter10.sysf]
congr_vt [in Chapter10.sysf]
congr_tapp [in Chapter10.sysf]
congr_app [in Chapter10.sysf]
congr_all [in Chapter10.sysf]
congr_arr [in Chapter10.sysf]
congr_top [in Chapter10.sysf]
constBool_ [in Chapter7.expressions]
constNat_ [in Chapter7.expressions]
cont_ext [in Chapter9.equivalence]
ctx [in Chapter10.POPLMark22]
ctx [in Chapter9.equivalence]
ctx [in Chapter9.preservation]
ctx [in Chapter9.variadic_preservation]
ctx [in Chapter10.POPLMark21]
ctx [in Chapter10.POPLMark1]
D
dctx [in Chapter10.POPLMark22]dctx [in Chapter10.POPLMark21]
dctx [in Chapter10.POPLMark1]
den [in Chapter4.soundness]
den_subst [in Chapter4.soundness]
destArity [in header_metacoq]
E
E [in Chapter9.sn_mod]empty [in Chapter10.POPLMark22]
empty [in Chapter10.POPLMark21]
empty [in Chapter10.POPLMark1]
equiv_den_subst [in Chapter4.soundness]
equiv_den [in Chapter4.soundness]
equiv_s_ind' [in Chapter4.sigmacalculus]
equiv_ind' [in Chapter4.sigmacalculus]
exp_uexp [in Chapter4.termination]
exp_s_ind' [in Chapter4.sigmacalculus]
exp_ind' [in Chapter4.sigmacalculus]
extRen_tm [in Chapter3.utlc_scoped]
extRen_tm [in Chapter6.variadic_list]
extRen_exp [in Chapter7.expressions]
extRen_exp_var [in Chapter7.expressions]
extRen_exp_bool [in Chapter7.expressions]
extRen_exp_arith [in Chapter7.expressions]
extRen_exp_lam [in Chapter7.expressions]
extRen_tm [in Chapter6.variadic_fin]
extRen_vl [in Chapter6.sysf_cbv]
extRen_tm [in Chapter6.sysf_cbv]
extRen_ty [in Chapter6.sysf_cbv]
extRen_tm [in Chapter9.stlc]
extRen_tm [in Chapter6.utlc_pairs]
extRen_tm [in Chapter3.utlc_pure]
extRen_tm [in Chapter10.sysf]
extRen_ty [in Chapter10.sysf]
extRen_proc [in Chapter6.picalculus]
extRen_chan [in Chapter6.picalculus]
extRen_ty [in Chapter6.recty]
extRen_tm [in Chapter10.sysf_pat]
extRen_pat [in Chapter10.sysf_pat]
extRen_ty [in Chapter10.sysf_pat]
ext_tm [in Chapter3.utlc_scoped]
ext_tm [in Chapter6.variadic_list]
ext_exp [in Chapter7.expressions]
ext_exp_var [in Chapter7.expressions]
ext_exp_bool [in Chapter7.expressions]
ext_exp_arith [in Chapter7.expressions]
ext_exp_lam [in Chapter7.expressions]
ext_tm [in Chapter6.variadic_fin]
ext_vl [in Chapter6.sysf_cbv]
ext_tm [in Chapter6.sysf_cbv]
ext_ty [in Chapter6.sysf_cbv]
ext_tm [in Chapter9.stlc]
ext_tm [in Chapter6.utlc_pairs]
ext_form [in Chapter6.fol]
ext_tm [in Chapter6.fol]
ext_tm [in Chapter3.utlc_pure]
ext_tm [in Chapter10.sysf]
ext_ty [in Chapter10.sysf]
ext_ty [in Chapter6.recty]
ext_tm [in Chapter10.sysf_pat]
ext_pat [in Chapter10.sysf_pat]
ext_ty [in Chapter10.sysf_pat]
E_strong [in Chapter9.sn_var]
E_ [in Chapter9.sn_var]
E_strong [in Chapter9.sn]
E_ [in Chapter9.wn]
F
fill [in Chapter4.termination]fin [in fintype]
fin [in fintype_variadic]
fixNames [in header_metacoq]
Forall [in header_metacoq]
ForallN [in header_metacoq]
Forall' [in header_metacoq]
funcomp [in unscoped]
funcomp [in axioms]
G
G [in Chapter9.sn_var]G [in Chapter9.wn]
genIH [in header_metacoq]
genStatement [in header_metacoq]
genStatement_Fix [in header_metacoq]
genStatement_no_lt [in header_metacoq]
get [in Chapter9.equivalence]
getName [in header_metacoq]
get_In [in header_extensible]
get_lemmas_and_name [in header_metacoq]
get_lemmas [in header_metacoq]
get_name [in header_metacoq]
get_name_of [in header_metacoq]
get_features [in header_metacoq]
G_strong [in Chapter9.sn_var]
G_strong [in Chapter9.sn]
H
has_ty_sem_strong [in Chapter9.sn_var]has_ty_sem [in Chapter9.sn_var]
has_ty_sem_strong [in Chapter9.sn]
has_ty_sem [in Chapter9.wn]
I
id [in unscoped]id [in fintype]
id [in fintype_variadic]
idren [in fintype]
idren [in fintype_variadic]
idSubst_tm [in Chapter3.utlc_scoped]
idSubst_tm [in Chapter6.variadic_list]
idSubst_exp [in Chapter7.expressions]
idSubst_exp_var [in Chapter7.expressions]
idSubst_exp_bool [in Chapter7.expressions]
idSubst_exp_arith [in Chapter7.expressions]
idSubst_exp_lam [in Chapter7.expressions]
idSubst_tm [in Chapter6.variadic_fin]
idSubst_vl [in Chapter6.sysf_cbv]
idSubst_tm [in Chapter6.sysf_cbv]
idSubst_ty [in Chapter6.sysf_cbv]
idSubst_tm [in Chapter9.stlc]
idSubst_tm [in Chapter6.utlc_pairs]
idSubst_form [in Chapter6.fol]
idSubst_tm [in Chapter6.fol]
idSubst_tm [in Chapter3.utlc_pure]
idSubst_tm [in Chapter10.sysf]
idSubst_ty [in Chapter10.sysf]
idSubst_ty [in Chapter6.recty]
idSubst_tm [in Chapter10.sysf_pat]
idSubst_pat [in Chapter10.sysf_pat]
idSubst_ty [in Chapter10.sysf_pat]
If_ [in Chapter7.expressions]
isIn_exp_exp_var [in Chapter7.expressions]
isIn_exp_exp_bool [in Chapter7.expressions]
isIn_exp_exp_arith [in Chapter7.expressions]
isIn_exp_exp_lam [in Chapter7.expressions]
L
L [in Chapter9.girard]L [in Chapter9.sn_mod]
L [in Chapter9.wn]
label_equiv [in Chapter10.POPLMark22]
label_equiv [in Chapter10.POPLMark21]
lift [in header_extensible]
list_comp [in axioms]
list_id [in axioms]
list_ext [in axioms]
locally_confluent [in ARS]
logeq [in Chapter9.equivalence]
logeq_rel [in Chapter9.equivalence]
ltc [in Chapter9.preservation]
ltc [in Chapter9.variadic_preservation]
L_strong [in Chapter9.sn]
L_strong_lam [in Chapter9.sn_lam]
L_close_ren [in Chapter9.sn_mod]
L_strong [in Chapter9.sn_mod]
L_ren [in Chapter9.sn_mod]
L.neutral [in Chapter9.girard]
M
mkDefinitionType [in header_metacoq]mkLemma [in header_metacoq]
mkVariable [in header_metacoq]
ModularFixpointN [in header_metacoq]
ModularFixpoint2 [in header_metacoq]
morphism [in ARS]
N
name_after_dot [in header_metacoq]name_after_dot' [in header_metacoq]
natTy_ [in Chapter7.expressions]
neutral [in Chapter9.sn_raamsdonk]
None [in unscoped]
null [in fintype]
null [in fintype_variadic]
P
plus_ [in Chapter7.expressions]prod_comp [in axioms]
prod_ext [in axioms]
prod_id [in axioms]
prod_map [in axioms]
Q
quote_list [in header_metacoq]R
Red [in Chapter9.sn_raamsdonk]RedS [in Chapter9.sn_raamsdonk]
redSN_ind_2 [in Chapter9.sn_raamsdonk]
Rel [in ARS]
remove_suffix [in header_metacoq]
remove_injs [in header_metacoq]
ren [in fintype]
ren [in fintype_variadic]
ren_tm [in Chapter3.utlc_scoped]
ren_tm [in Chapter6.variadic_list]
ren_exp [in Chapter7.expressions]
ren_exp_var [in Chapter7.expressions]
ren_exp_bool [in Chapter7.expressions]
ren_exp_arith [in Chapter7.expressions]
ren_exp_lam [in Chapter7.expressions]
ren_tm [in Chapter6.variadic_fin]
ren_vl [in Chapter6.sysf_cbv]
ren_tm [in Chapter6.sysf_cbv]
ren_ty [in Chapter6.sysf_cbv]
ren_tm [in Chapter9.stlc]
ren_tm [in Chapter6.utlc_pairs]
ren_tm [in Chapter3.utlc_pure]
ren_tm [in Chapter10.sysf]
ren_ty [in Chapter10.sysf]
ren_proc [in Chapter6.picalculus]
ren_chan [in Chapter6.picalculus]
ren_ty [in Chapter6.recty]
ren_tm [in Chapter10.sysf_pat]
ren_pat [in Chapter10.sysf_pat]
ren_ty [in Chapter10.sysf_pat]
replace_ext [in header_metacoq]
replace_consts [in header_metacoq]
replace_terms [in header_metacoq]
replace_const [in header_metacoq]
replace_term [in header_metacoq]
rinstInst_up_list_tm_tm [in Chapter3.utlc_scoped]
rinstInst_up_tm_tm [in Chapter3.utlc_scoped]
rinstInst_up_list_tm_tm [in Chapter6.variadic_list]
rinstInst_up_tm_tm [in Chapter6.variadic_list]
rinstInst_up_exp_exp [in Chapter7.expressions]
rinstInst_up_list_tm_tm [in Chapter6.variadic_fin]
rinstInst_up_tm_tm [in Chapter6.variadic_fin]
rinstInst_up_list_vl_vl [in Chapter6.sysf_cbv]
rinstInst_up_list_vl_ty [in Chapter6.sysf_cbv]
rinstInst_up_list_ty_vl [in Chapter6.sysf_cbv]
rinstInst_up_vl_vl [in Chapter6.sysf_cbv]
rinstInst_up_vl_ty [in Chapter6.sysf_cbv]
rinstInst_up_ty_vl [in Chapter6.sysf_cbv]
rinstInst_up_list_ty_ty [in Chapter6.sysf_cbv]
rinstInst_up_ty_ty [in Chapter6.sysf_cbv]
rinstInst_up_list_tm_tm [in Chapter9.stlc]
rinstInst_up_tm_tm [in Chapter9.stlc]
rinstInst_up_list_tm_tm [in Chapter6.utlc_pairs]
rinstInst_up_tm_tm [in Chapter6.utlc_pairs]
rinstInst_up_tm_tm [in Chapter3.utlc_pure]
rinstInst_up_list_tm_tm [in Chapter10.sysf]
rinstInst_up_list_tm_ty [in Chapter10.sysf]
rinstInst_up_list_ty_tm [in Chapter10.sysf]
rinstInst_up_tm_tm [in Chapter10.sysf]
rinstInst_up_tm_ty [in Chapter10.sysf]
rinstInst_up_ty_tm [in Chapter10.sysf]
rinstInst_up_list_ty_ty [in Chapter10.sysf]
rinstInst_up_ty_ty [in Chapter10.sysf]
rinstInst_up_list_ty_ty [in Chapter6.recty]
rinstInst_up_ty_ty [in Chapter6.recty]
rinstInst_up_list_tm_tm [in Chapter10.sysf_pat]
rinstInst_up_list_tm_ty [in Chapter10.sysf_pat]
rinstInst_up_list_ty_tm [in Chapter10.sysf_pat]
rinstInst_up_tm_tm [in Chapter10.sysf_pat]
rinstInst_up_tm_ty [in Chapter10.sysf_pat]
rinstInst_up_ty_tm [in Chapter10.sysf_pat]
rinstInst_up_list_ty_ty [in Chapter10.sysf_pat]
rinstInst_up_ty_ty [in Chapter10.sysf_pat]
rinst_inst_tm [in Chapter3.utlc_scoped]
rinst_inst_tm [in Chapter6.variadic_list]
rinst_inst_exp [in Chapter7.expressions]
rinst_inst_exp_var [in Chapter7.expressions]
rinst_inst_exp_bool [in Chapter7.expressions]
rinst_inst_exp_arith [in Chapter7.expressions]
rinst_inst_exp_lam [in Chapter7.expressions]
rinst_inst_tm [in Chapter6.variadic_fin]
rinst_inst_vl [in Chapter6.sysf_cbv]
rinst_inst_tm [in Chapter6.sysf_cbv]
rinst_inst_ty [in Chapter6.sysf_cbv]
rinst_inst_tm [in Chapter9.stlc]
rinst_inst_tm [in Chapter6.utlc_pairs]
rinst_inst_tm [in Chapter3.utlc_pure]
rinst_inst_tm [in Chapter10.sysf]
rinst_inst_ty [in Chapter10.sysf]
rinst_inst_ty [in Chapter6.recty]
rinst_inst_tm [in Chapter10.sysf_pat]
rinst_inst_pat [in Chapter10.sysf_pat]
rinst_inst_ty [in Chapter10.sysf_pat]
S
scons [in unscoped]scons [in fintype]
scons [in fintype_variadic]
scons_p [in fintype]
scons_p [in fintype_variadic]
shift [in unscoped]
shift [in fintype]
shift [in fintype_variadic]
shift_p [in fintype]
shift_p [in fintype_variadic]
SNe_ind_2 [in Chapter9.sn_raamsdonk]
SN_multind [in Chapter9.sn_raamsdonk]
SN_ind_2 [in Chapter9.sn_raamsdonk]
Some [in unscoped]
soundness [in Chapter4.soundness]
soundness_subst [in Chapter4.soundness]
split_forall_impl [in header_metacoq]
subst_tm [in Chapter3.utlc_scoped]
subst_tm [in Chapter6.variadic_list]
subst_exp [in Chapter7.expressions]
subst_exp_var [in Chapter7.expressions]
subst_exp_bool [in Chapter7.expressions]
subst_exp_arith [in Chapter7.expressions]
subst_exp_lam [in Chapter7.expressions]
subst_tm [in Chapter6.variadic_fin]
subst_vl [in Chapter6.sysf_cbv]
subst_tm [in Chapter6.sysf_cbv]
subst_ty [in Chapter6.sysf_cbv]
subst_tm [in Chapter9.stlc]
subst_tm [in Chapter6.utlc_pairs]
subst_form [in Chapter6.fol]
subst_tm [in Chapter6.fol]
subst_tm [in Chapter3.utlc_pure]
subst_tm [in Chapter10.sysf]
subst_ty [in Chapter10.sysf]
subst_exp_uexp [in Chapter4.termination]
subst_ty [in Chapter6.recty]
subst_tm [in Chapter10.sysf_pat]
subst_pat [in Chapter10.sysf_pat]
subst_ty [in Chapter10.sysf_pat]
T
terminating [in ARS]tmMkDefinition [in header_metacoq]
tmTryInferInstance [in header_metacoq]
transitivity_at [in Chapter10.POPLMark22]
transitivity_at [in Chapter10.POPLMark21]
transitivity_at [in Chapter10.POPLMark1]
U
update [in Chapter10.POPLMark22]update [in Chapter10.POPLMark21]
upExtRen_list_tm_tm [in Chapter3.utlc_scoped]
upExtRen_tm_tm [in Chapter3.utlc_scoped]
upExtRen_list_tm_tm [in Chapter6.variadic_list]
upExtRen_tm_tm [in Chapter6.variadic_list]
upExtRen_exp_exp [in Chapter7.expressions]
upExtRen_list_tm_tm [in Chapter6.variadic_fin]
upExtRen_tm_tm [in Chapter6.variadic_fin]
upExtRen_list_vl_vl [in Chapter6.sysf_cbv]
upExtRen_list_vl_ty [in Chapter6.sysf_cbv]
upExtRen_list_ty_vl [in Chapter6.sysf_cbv]
upExtRen_vl_vl [in Chapter6.sysf_cbv]
upExtRen_vl_ty [in Chapter6.sysf_cbv]
upExtRen_ty_vl [in Chapter6.sysf_cbv]
upExtRen_list_ty_ty [in Chapter6.sysf_cbv]
upExtRen_ty_ty [in Chapter6.sysf_cbv]
upExtRen_list_tm_tm [in Chapter9.stlc]
upExtRen_tm_tm [in Chapter9.stlc]
upExtRen_list_tm_tm [in Chapter6.utlc_pairs]
upExtRen_tm_tm [in Chapter6.utlc_pairs]
upExtRen_tm_tm [in Chapter3.utlc_pure]
upExtRen_list_tm_tm [in Chapter10.sysf]
upExtRen_list_tm_ty [in Chapter10.sysf]
upExtRen_list_ty_tm [in Chapter10.sysf]
upExtRen_tm_tm [in Chapter10.sysf]
upExtRen_tm_ty [in Chapter10.sysf]
upExtRen_ty_tm [in Chapter10.sysf]
upExtRen_list_ty_ty [in Chapter10.sysf]
upExtRen_ty_ty [in Chapter10.sysf]
upExtRen_chan_chan [in Chapter6.picalculus]
upExtRen_list_ty_ty [in Chapter6.recty]
upExtRen_ty_ty [in Chapter6.recty]
upExtRen_list_tm_tm [in Chapter10.sysf_pat]
upExtRen_list_tm_ty [in Chapter10.sysf_pat]
upExtRen_list_ty_tm [in Chapter10.sysf_pat]
upExtRen_tm_tm [in Chapter10.sysf_pat]
upExtRen_tm_ty [in Chapter10.sysf_pat]
upExtRen_ty_tm [in Chapter10.sysf_pat]
upExtRen_list_ty_ty [in Chapter10.sysf_pat]
upExtRen_ty_ty [in Chapter10.sysf_pat]
upExt_list_tm_tm [in Chapter3.utlc_scoped]
upExt_tm_tm [in Chapter3.utlc_scoped]
upExt_list_tm_tm [in Chapter6.variadic_list]
upExt_tm_tm [in Chapter6.variadic_list]
upExt_exp_exp [in Chapter7.expressions]
upExt_list_tm_tm [in Chapter6.variadic_fin]
upExt_tm_tm [in Chapter6.variadic_fin]
upExt_list_vl_vl [in Chapter6.sysf_cbv]
upExt_list_vl_ty [in Chapter6.sysf_cbv]
upExt_list_ty_vl [in Chapter6.sysf_cbv]
upExt_vl_vl [in Chapter6.sysf_cbv]
upExt_vl_ty [in Chapter6.sysf_cbv]
upExt_ty_vl [in Chapter6.sysf_cbv]
upExt_list_ty_ty [in Chapter6.sysf_cbv]
upExt_ty_ty [in Chapter6.sysf_cbv]
upExt_list_tm_tm [in Chapter9.stlc]
upExt_tm_tm [in Chapter9.stlc]
upExt_list_tm_tm [in Chapter6.utlc_pairs]
upExt_tm_tm [in Chapter6.utlc_pairs]
upExt_list_tm_tm [in Chapter6.fol]
upExt_tm_tm [in Chapter6.fol]
upExt_tm_tm [in Chapter3.utlc_pure]
upExt_list_tm_tm [in Chapter10.sysf]
upExt_list_tm_ty [in Chapter10.sysf]
upExt_list_ty_tm [in Chapter10.sysf]
upExt_tm_tm [in Chapter10.sysf]
upExt_tm_ty [in Chapter10.sysf]
upExt_ty_tm [in Chapter10.sysf]
upExt_list_ty_ty [in Chapter10.sysf]
upExt_ty_ty [in Chapter10.sysf]
upExt_list_ty_ty [in Chapter6.recty]
upExt_ty_ty [in Chapter6.recty]
upExt_list_tm_tm [in Chapter10.sysf_pat]
upExt_list_tm_ty [in Chapter10.sysf_pat]
upExt_list_ty_tm [in Chapter10.sysf_pat]
upExt_tm_tm [in Chapter10.sysf_pat]
upExt_tm_ty [in Chapter10.sysf_pat]
upExt_ty_tm [in Chapter10.sysf_pat]
upExt_list_ty_ty [in Chapter10.sysf_pat]
upExt_ty_ty [in Chapter10.sysf_pat]
upIdList_tm_tm [in Chapter3.utlc_scoped]
upIdList_tm_tm [in Chapter6.variadic_list]
upIdList_tm_tm [in Chapter6.variadic_fin]
upIdList_vl_vl [in Chapter6.sysf_cbv]
upIdList_vl_ty [in Chapter6.sysf_cbv]
upIdList_ty_vl [in Chapter6.sysf_cbv]
upIdList_ty_ty [in Chapter6.sysf_cbv]
upIdList_tm_tm [in Chapter9.stlc]
upIdList_tm_tm [in Chapter6.utlc_pairs]
upIdList_tm_tm [in Chapter6.fol]
upIdList_tm_tm [in Chapter10.sysf]
upIdList_tm_ty [in Chapter10.sysf]
upIdList_ty_tm [in Chapter10.sysf]
upIdList_ty_ty [in Chapter10.sysf]
upIdList_ty_ty [in Chapter6.recty]
upIdList_tm_tm [in Chapter10.sysf_pat]
upIdList_tm_ty [in Chapter10.sysf_pat]
upIdList_ty_tm [in Chapter10.sysf_pat]
upIdList_ty_ty [in Chapter10.sysf_pat]
upId_tm_tm [in Chapter3.utlc_scoped]
upId_tm_tm [in Chapter6.variadic_list]
upId_exp_exp [in Chapter7.expressions]
upId_tm_tm [in Chapter6.variadic_fin]
upId_vl_vl [in Chapter6.sysf_cbv]
upId_vl_ty [in Chapter6.sysf_cbv]
upId_ty_vl [in Chapter6.sysf_cbv]
upId_ty_ty [in Chapter6.sysf_cbv]
upId_tm_tm [in Chapter9.stlc]
upId_tm_tm [in Chapter6.utlc_pairs]
upId_tm_tm [in Chapter6.fol]
upId_tm_tm [in Chapter3.utlc_pure]
upId_tm_tm [in Chapter10.sysf]
upId_tm_ty [in Chapter10.sysf]
upId_ty_tm [in Chapter10.sysf]
upId_ty_ty [in Chapter10.sysf]
upId_ty_ty [in Chapter6.recty]
upId_tm_tm [in Chapter10.sysf_pat]
upId_tm_ty [in Chapter10.sysf_pat]
upId_ty_tm [in Chapter10.sysf_pat]
upId_ty_ty [in Chapter10.sysf_pat]
upList_tm_tm [in Chapter3.utlc_scoped]
upList_tm_tm [in Chapter6.variadic_list]
upList_tm_tm [in Chapter6.variadic_fin]
upList_vl_vl [in Chapter6.sysf_cbv]
upList_vl_ty [in Chapter6.sysf_cbv]
upList_ty_vl [in Chapter6.sysf_cbv]
upList_ty_ty [in Chapter6.sysf_cbv]
upList_tm_tm [in Chapter9.stlc]
upList_tm_tm [in Chapter6.utlc_pairs]
upList_tm_tm [in Chapter6.fol]
upList_tm_tm [in Chapter10.sysf]
upList_tm_ty [in Chapter10.sysf]
upList_ty_tm [in Chapter10.sysf]
upList_ty_ty [in Chapter10.sysf]
upList_ty_ty [in Chapter6.recty]
upList_tm_tm [in Chapter10.sysf_pat]
upList_tm_ty [in Chapter10.sysf_pat]
upList_ty_tm [in Chapter10.sysf_pat]
upList_ty_ty [in Chapter10.sysf_pat]
upRenList_tm_tm [in Chapter3.utlc_scoped]
upRenList_tm_tm [in Chapter6.variadic_list]
upRenList_tm_tm [in Chapter6.variadic_fin]
upRenList_vl_vl [in Chapter6.sysf_cbv]
upRenList_vl_ty [in Chapter6.sysf_cbv]
upRenList_ty_vl [in Chapter6.sysf_cbv]
upRenList_ty_ty [in Chapter6.sysf_cbv]
upRenList_tm_tm [in Chapter9.stlc]
upRenList_tm_tm [in Chapter6.utlc_pairs]
upRenList_tm_tm [in Chapter10.sysf]
upRenList_tm_ty [in Chapter10.sysf]
upRenList_ty_tm [in Chapter10.sysf]
upRenList_ty_ty [in Chapter10.sysf]
upRenList_ty_ty [in Chapter6.recty]
upRenList_tm_tm [in Chapter10.sysf_pat]
upRenList_tm_ty [in Chapter10.sysf_pat]
upRenList_ty_tm [in Chapter10.sysf_pat]
upRenList_ty_ty [in Chapter10.sysf_pat]
upRen_tm_tm [in Chapter3.utlc_scoped]
upRen_tm_tm [in Chapter6.variadic_list]
upRen_exp_exp [in Chapter7.expressions]
upRen_tm_tm [in Chapter6.variadic_fin]
upRen_vl_vl [in Chapter6.sysf_cbv]
upRen_vl_ty [in Chapter6.sysf_cbv]
upRen_ty_vl [in Chapter6.sysf_cbv]
upRen_ty_ty [in Chapter6.sysf_cbv]
upRen_tm_tm [in Chapter9.stlc]
upRen_p [in fintype]
upRen_p [in fintype_variadic]
upRen_tm_tm [in Chapter6.utlc_pairs]
upRen_tm_tm [in Chapter3.utlc_pure]
upRen_tm_tm [in Chapter10.sysf]
upRen_tm_ty [in Chapter10.sysf]
upRen_ty_tm [in Chapter10.sysf]
upRen_ty_ty [in Chapter10.sysf]
upRen_chan_chan [in Chapter6.picalculus]
upRen_ty_ty [in Chapter6.recty]
upRen_tm_tm [in Chapter10.sysf_pat]
upRen_tm_ty [in Chapter10.sysf_pat]
upRen_ty_tm [in Chapter10.sysf_pat]
upRen_ty_ty [in Chapter10.sysf_pat]
up_ren [in unscoped]
up_subst_subst_list_tm_tm [in Chapter3.utlc_scoped]
up_subst_subst_tm_tm [in Chapter3.utlc_scoped]
up_subst_ren_list_tm_tm [in Chapter3.utlc_scoped]
up_subst_ren_tm_tm [in Chapter3.utlc_scoped]
up_ren_subst_list_tm_tm [in Chapter3.utlc_scoped]
up_ren_subst_tm_tm [in Chapter3.utlc_scoped]
up_ren_ren_list_tm_tm [in Chapter3.utlc_scoped]
up_ren_ren_tm_tm [in Chapter3.utlc_scoped]
up_tm_tm [in Chapter3.utlc_scoped]
up_subst_subst_list_tm_tm [in Chapter6.variadic_list]
up_subst_subst_tm_tm [in Chapter6.variadic_list]
up_subst_ren_list_tm_tm [in Chapter6.variadic_list]
up_subst_ren_tm_tm [in Chapter6.variadic_list]
up_ren_subst_list_tm_tm [in Chapter6.variadic_list]
up_ren_subst_tm_tm [in Chapter6.variadic_list]
up_ren_ren_list_tm_tm [in Chapter6.variadic_list]
up_ren_ren_tm_tm [in Chapter6.variadic_list]
up_tm_tm [in Chapter6.variadic_list]
up_subst_subst_exp_exp [in Chapter7.expressions]
up_subst_ren_exp_exp [in Chapter7.expressions]
up_ren_subst_exp_exp [in Chapter7.expressions]
up_ren_ren_exp_exp [in Chapter7.expressions]
up_exp_exp [in Chapter7.expressions]
up_subst_subst_list_tm_tm [in Chapter6.variadic_fin]
up_subst_subst_tm_tm [in Chapter6.variadic_fin]
up_subst_ren_list_tm_tm [in Chapter6.variadic_fin]
up_subst_ren_tm_tm [in Chapter6.variadic_fin]
up_ren_subst_list_tm_tm [in Chapter6.variadic_fin]
up_ren_subst_tm_tm [in Chapter6.variadic_fin]
up_ren_ren_list_tm_tm [in Chapter6.variadic_fin]
up_ren_ren_tm_tm [in Chapter6.variadic_fin]
up_tm_tm [in Chapter6.variadic_fin]
up_subst_subst_list_vl_vl [in Chapter6.sysf_cbv]
up_subst_subst_list_vl_ty [in Chapter6.sysf_cbv]
up_subst_subst_list_ty_vl [in Chapter6.sysf_cbv]
up_subst_subst_vl_vl [in Chapter6.sysf_cbv]
up_subst_subst_vl_ty [in Chapter6.sysf_cbv]
up_subst_subst_ty_vl [in Chapter6.sysf_cbv]
up_subst_ren_list_vl_vl [in Chapter6.sysf_cbv]
up_subst_ren_list_vl_ty [in Chapter6.sysf_cbv]
up_subst_ren_list_ty_vl [in Chapter6.sysf_cbv]
up_subst_ren_vl_vl [in Chapter6.sysf_cbv]
up_subst_ren_vl_ty [in Chapter6.sysf_cbv]
up_subst_ren_ty_vl [in Chapter6.sysf_cbv]
up_ren_subst_list_vl_vl [in Chapter6.sysf_cbv]
up_ren_subst_list_vl_ty [in Chapter6.sysf_cbv]
up_ren_subst_list_ty_vl [in Chapter6.sysf_cbv]
up_ren_subst_vl_vl [in Chapter6.sysf_cbv]
up_ren_subst_vl_ty [in Chapter6.sysf_cbv]
up_ren_subst_ty_vl [in Chapter6.sysf_cbv]
up_ren_ren_list_vl_vl [in Chapter6.sysf_cbv]
up_ren_ren_list_vl_ty [in Chapter6.sysf_cbv]
up_ren_ren_list_ty_vl [in Chapter6.sysf_cbv]
up_ren_ren_vl_vl [in Chapter6.sysf_cbv]
up_ren_ren_vl_ty [in Chapter6.sysf_cbv]
up_ren_ren_ty_vl [in Chapter6.sysf_cbv]
up_vl_vl [in Chapter6.sysf_cbv]
up_vl_ty [in Chapter6.sysf_cbv]
up_ty_vl [in Chapter6.sysf_cbv]
up_subst_subst_list_ty_ty [in Chapter6.sysf_cbv]
up_subst_subst_ty_ty [in Chapter6.sysf_cbv]
up_subst_ren_list_ty_ty [in Chapter6.sysf_cbv]
up_subst_ren_ty_ty [in Chapter6.sysf_cbv]
up_ren_subst_list_ty_ty [in Chapter6.sysf_cbv]
up_ren_subst_ty_ty [in Chapter6.sysf_cbv]
up_ren_ren_list_ty_ty [in Chapter6.sysf_cbv]
up_ren_ren_ty_ty [in Chapter6.sysf_cbv]
up_ty_ty [in Chapter6.sysf_cbv]
up_subst_subst_list_tm_tm [in Chapter9.stlc]
up_subst_subst_tm_tm [in Chapter9.stlc]
up_subst_ren_list_tm_tm [in Chapter9.stlc]
up_subst_ren_tm_tm [in Chapter9.stlc]
up_ren_subst_list_tm_tm [in Chapter9.stlc]
up_ren_subst_tm_tm [in Chapter9.stlc]
up_ren_ren_list_tm_tm [in Chapter9.stlc]
up_ren_ren_tm_tm [in Chapter9.stlc]
up_tm_tm [in Chapter9.stlc]
up_ren [in fintype]
up_ren [in fintype_variadic]
up_subst_subst_list_tm_tm [in Chapter6.utlc_pairs]
up_subst_subst_tm_tm [in Chapter6.utlc_pairs]
up_subst_ren_list_tm_tm [in Chapter6.utlc_pairs]
up_subst_ren_tm_tm [in Chapter6.utlc_pairs]
up_ren_subst_list_tm_tm [in Chapter6.utlc_pairs]
up_ren_subst_tm_tm [in Chapter6.utlc_pairs]
up_ren_ren_list_tm_tm [in Chapter6.utlc_pairs]
up_ren_ren_tm_tm [in Chapter6.utlc_pairs]
up_tm_tm [in Chapter6.utlc_pairs]
up_subst_subst_list_tm_tm [in Chapter6.fol]
up_subst_subst_tm_tm [in Chapter6.fol]
up_tm_tm [in Chapter6.fol]
up_subst_subst_tm_tm [in Chapter3.utlc_pure]
up_subst_ren_tm_tm [in Chapter3.utlc_pure]
up_ren_subst_tm_tm [in Chapter3.utlc_pure]
up_ren_ren_tm_tm [in Chapter3.utlc_pure]
up_tm_tm [in Chapter3.utlc_pure]
up_subst_subst_list_tm_tm [in Chapter10.sysf]
up_subst_subst_list_tm_ty [in Chapter10.sysf]
up_subst_subst_list_ty_tm [in Chapter10.sysf]
up_subst_subst_tm_tm [in Chapter10.sysf]
up_subst_subst_tm_ty [in Chapter10.sysf]
up_subst_subst_ty_tm [in Chapter10.sysf]
up_subst_ren_list_tm_tm [in Chapter10.sysf]
up_subst_ren_list_tm_ty [in Chapter10.sysf]
up_subst_ren_list_ty_tm [in Chapter10.sysf]
up_subst_ren_tm_tm [in Chapter10.sysf]
up_subst_ren_tm_ty [in Chapter10.sysf]
up_subst_ren_ty_tm [in Chapter10.sysf]
up_ren_subst_list_tm_tm [in Chapter10.sysf]
up_ren_subst_list_tm_ty [in Chapter10.sysf]
up_ren_subst_list_ty_tm [in Chapter10.sysf]
up_ren_subst_tm_tm [in Chapter10.sysf]
up_ren_subst_tm_ty [in Chapter10.sysf]
up_ren_subst_ty_tm [in Chapter10.sysf]
up_tm_tm [in Chapter10.sysf]
up_tm_ty [in Chapter10.sysf]
up_ty_tm [in Chapter10.sysf]
up_subst_subst_list_ty_ty [in Chapter10.sysf]
up_subst_subst_ty_ty [in Chapter10.sysf]
up_subst_ren_list_ty_ty [in Chapter10.sysf]
up_subst_ren_ty_ty [in Chapter10.sysf]
up_ren_subst_list_ty_ty [in Chapter10.sysf]
up_ren_subst_ty_ty [in Chapter10.sysf]
up_ty_ty [in Chapter10.sysf]
up_ren_ren_chan_chan [in Chapter6.picalculus]
up_subst_subst_list_ty_ty [in Chapter6.recty]
up_subst_subst_ty_ty [in Chapter6.recty]
up_subst_ren_list_ty_ty [in Chapter6.recty]
up_subst_ren_ty_ty [in Chapter6.recty]
up_ren_subst_list_ty_ty [in Chapter6.recty]
up_ren_subst_ty_ty [in Chapter6.recty]
up_ren_ren_list_ty_ty [in Chapter6.recty]
up_ren_ren_ty_ty [in Chapter6.recty]
up_ty_ty [in Chapter6.recty]
up_subst_subst_list_tm_tm [in Chapter10.sysf_pat]
up_subst_subst_list_tm_ty [in Chapter10.sysf_pat]
up_subst_subst_list_ty_tm [in Chapter10.sysf_pat]
up_subst_subst_tm_tm [in Chapter10.sysf_pat]
up_subst_subst_tm_ty [in Chapter10.sysf_pat]
up_subst_subst_ty_tm [in Chapter10.sysf_pat]
up_subst_ren_list_tm_tm [in Chapter10.sysf_pat]
up_subst_ren_list_tm_ty [in Chapter10.sysf_pat]
up_subst_ren_list_ty_tm [in Chapter10.sysf_pat]
up_subst_ren_tm_tm [in Chapter10.sysf_pat]
up_subst_ren_tm_ty [in Chapter10.sysf_pat]
up_subst_ren_ty_tm [in Chapter10.sysf_pat]
up_ren_subst_list_tm_tm [in Chapter10.sysf_pat]
up_ren_subst_list_tm_ty [in Chapter10.sysf_pat]
up_ren_subst_list_ty_tm [in Chapter10.sysf_pat]
up_ren_subst_tm_tm [in Chapter10.sysf_pat]
up_ren_subst_tm_ty [in Chapter10.sysf_pat]
up_ren_subst_ty_tm [in Chapter10.sysf_pat]
up_ren_ren_list_tm_tm [in Chapter10.sysf_pat]
up_ren_ren_list_tm_ty [in Chapter10.sysf_pat]
up_ren_ren_list_ty_tm [in Chapter10.sysf_pat]
up_ren_ren_tm_tm [in Chapter10.sysf_pat]
up_ren_ren_tm_ty [in Chapter10.sysf_pat]
up_ren_ren_ty_tm [in Chapter10.sysf_pat]
up_tm_tm [in Chapter10.sysf_pat]
up_tm_ty [in Chapter10.sysf_pat]
up_ty_tm [in Chapter10.sysf_pat]
up_subst_subst_list_ty_ty [in Chapter10.sysf_pat]
up_subst_subst_ty_ty [in Chapter10.sysf_pat]
up_subst_ren_list_ty_ty [in Chapter10.sysf_pat]
up_subst_ren_ty_ty [in Chapter10.sysf_pat]
up_ren_subst_list_ty_ty [in Chapter10.sysf_pat]
up_ren_subst_ty_ty [in Chapter10.sysf_pat]
up_ren_ren_list_ty_ty [in Chapter10.sysf_pat]
up_ren_ren_ty_ty [in Chapter10.sysf_pat]
up_ty_ty [in Chapter10.sysf_pat]
V
value [in Chapter9.reduction]var_zero [in unscoped]
var_exp [in Chapter7.expressions]
var_zero [in fintype]
var_zero [in fintype_variadic]
W
whnf [in Chapter9.sn_mod]Z
zero_p [in fintype]zero_p [in fintype_variadic]
Record Index
B
Bundle [in header_extensible]H
has_features [in header_metacoq]I
Imp [in tactics]ImpRev [in tactics]
InRelC [in header_metacoq]
R
Ren1 [in unscoped]Ren1 [in fintype]
Ren1 [in fintype_variadic]
Ren2 [in unscoped]
Ren2 [in fintype]
Ren2 [in fintype_variadic]
Ren3 [in unscoped]
Ren3 [in fintype]
Ren3 [in fintype_variadic]
Ren4 [in unscoped]
Ren4 [in fintype]
Ren4 [in fintype_variadic]
Ren5 [in unscoped]
Ren5 [in fintype]
Ren5 [in fintype_variadic]
retract [in header_extensible]
S
Subst1 [in unscoped]Subst1 [in fintype]
Subst1 [in fintype_variadic]
Subst2 [in unscoped]
Subst2 [in fintype]
Subst2 [in fintype_variadic]
Subst3 [in unscoped]
Subst3 [in fintype]
Subst3 [in fintype_variadic]
Subst4 [in unscoped]
Subst4 [in fintype]
Subst4 [in fintype_variadic]
Subst5 [in unscoped]
Subst5 [in fintype]
Subst5 [in fintype_variadic]
subtermC [in header_metacoq]
U
Up_tm [in Chapter3.utlc_scoped]Up_tm [in Chapter6.variadic_list]
Up_exp [in Chapter7.expressions]
Up_tm [in Chapter6.variadic_fin]
Up_vl [in Chapter6.sysf_cbv]
Up_ty [in Chapter6.sysf_cbv]
Up_tm [in Chapter9.stlc]
Up_tm [in Chapter6.utlc_pairs]
Up_tm [in Chapter6.fol]
Up_tm [in Chapter3.utlc_pure]
Up_tm [in Chapter10.sysf]
Up_ty [in Chapter10.sysf]
Up_chan [in Chapter6.picalculus]
Up_ty [in Chapter6.recty]
Up_tm [in Chapter10.sysf_pat]
Up_ty [in Chapter10.sysf_pat]
V
Var [in unscoped]Var [in fintype]
Var [in fintype_variadic]
| 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 | (2746 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 | (255 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 | (6 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 | (192 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 | (43 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 | (668 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 | (386 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 | (59 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 | (148 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 | (101 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 | (35 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (792 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 | (56 entries) |