| 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 | (260 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 | (26 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 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 | (62 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 | (69 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (23 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 | (12 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 | (4 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 | (41 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 | (12 entries) |
Global Index
A
anti_rename [lemma, in PR.sn_inductive_2a]ap [definition, in PR.fintype]
apc [definition, in PR.fintype]
app [constructor, in PR.stlc]
axioms [library]
B
Base [constructor, in PR.stlc]C
closed_orelim [lemma, in PR.sn_inductive_soundness_1a]closed_inr [lemma, in PR.sn_inductive_soundness_1a]
closed_inl [lemma, in PR.sn_inductive_soundness_1a]
closed_appR [lemma, in PR.sn_inductive_soundness_1a]
closed_lam [lemma, in PR.sn_inductive_soundness_1a]
closure [inductive, in PR.sn_inductive_2b]
CNeutral [constructor, in PR.sn_inductive_2b]
CommaNotation [module, in PR.fintype]
_ , _ (subst_scope) [notation, in PR.fintype]
comp [definition, in PR.fintype]
compComp_tm [lemma, in PR.stlc]
compComp'_tm [lemma, in PR.stlc]
compRenRen_tm [definition, in PR.stlc]
compRenSubst_tm [definition, in PR.stlc]
compRen_tm [lemma, in PR.stlc]
compRen'_tm [lemma, in PR.stlc]
compSubstRen__tm [definition, in PR.stlc]
compSubstSubst_tm [definition, in PR.stlc]
congr_orelim [lemma, in PR.stlc]
congr_inr [lemma, in PR.stlc]
congr_inl [lemma, in PR.stlc]
congr_lam [lemma, in PR.stlc]
congr_app [lemma, in PR.stlc]
congr_Plus [lemma, in PR.stlc]
congr_Fun [lemma, in PR.stlc]
congr_Base [lemma, in PR.stlc]
cr [lemma, in PR.sn_inductive_2b]
CRefl [constructor, in PR.sn_inductive_2b]
CStep [constructor, in PR.sn_inductive_2b]
ctx [definition, in PR.sn_inductive_2b]
E
extRen_tm [definition, in PR.stlc]ext_SN [lemma, in PR.sn_inductive_2a]
ext_tm [definition, in PR.stlc]
F
fin [definition, in PR.fintype]fintype [library]
Fun [constructor, in PR.stlc]
funcomp [definition, in PR.fintype]
fundamental_backwards_orr [lemma, in PR.sn_inductive_soundness_1a]
fundamental_backwards_orl [lemma, in PR.sn_inductive_soundness_1a]
fundamental_backwards [lemma, in PR.sn_inductive_soundness_1a]
H
has_type [inductive, in PR.sn_inductive_2b]I
id [definition, in PR.fintype]idren [definition, in PR.fintype]
ids [projection, in PR.fintype]
ids [constructor, in PR.fintype]
idSubst_tm [definition, in PR.stlc]
id_red [lemma, in PR.sn_inductive_2b]
ImPred [definition, in PR.reduction]
im_predI [lemma, in PR.reduction]
inl [constructor, in PR.stlc]
inr [constructor, in PR.stlc]
instId_tm [lemma, in PR.stlc]
L
lam [constructor, in PR.stlc]M
main_lemma [lemma, in PR.sn_inductive_2b]mstep [inductive, in PR.reduction]
mstep_beta [lemma, in PR.reduction]
mstep_subst [lemma, in PR.reduction]
mstep_inst [lemma, in PR.reduction]
mstep_orelim [lemma, in PR.reduction]
mstep_inr [lemma, in PR.reduction]
mstep_inl [lemma, in PR.reduction]
mstep_app [lemma, in PR.reduction]
mstep_lam [lemma, in PR.reduction]
mstep_trans [lemma, in PR.reduction]
mstep_step [constructor, in PR.reduction]
mstep_refl [constructor, in PR.reduction]
N
neutral [definition, in PR.sn_inductive_soundness_1a]neutral_preservation [lemma, in PR.sn_inductive_soundness_1a]
norm [lemma, in PR.sn_inductive_2b]
null [definition, in PR.fintype]
O
orelim [constructor, in PR.stlc]P
pext [axiom, in PR.axioms]pi [lemma, in PR.axioms]
Plus [constructor, in PR.stlc]
R
Red [definition, in PR.sn_inductive_2b]RedS [definition, in PR.sn_inductive_2b]
redsn [inductive, in PR.sn_inductive_soundness_1a]
redSN_ind_2 [definition, in PR.sn_defs]
redsn_backwards [lemma, in PR.sn_inductive_soundness_1a]
redsn_caseR [constructor, in PR.sn_inductive_soundness_1a]
redsn_caseL [constructor, in PR.sn_inductive_soundness_1a]
redsn_or [constructor, in PR.sn_inductive_soundness_1a]
redsn_app [constructor, in PR.sn_inductive_soundness_1a]
redsn_beta [constructor, in PR.sn_inductive_soundness_1a]
reduction [library]
RedUp [lemma, in PR.sn_inductive_2b]
red_var [lemma, in PR.sn_inductive_2b]
ren [definition, in PR.fintype]
rename [lemma, in PR.sn_inductive_2a]
rename_red [lemma, in PR.sn_inductive_2b]
renComp_tm [lemma, in PR.stlc]
renComp'_tm [lemma, in PR.stlc]
renRen_tm [lemma, in PR.stlc]
renRen'_tm [lemma, in PR.stlc]
Ren_tm [instance, in PR.stlc]
ren_tm [definition, in PR.stlc]
ren1 [projection, in PR.fintype]
Ren1 [record, in PR.fintype]
ren1 [constructor, in PR.fintype]
Ren1 [inductive, in PR.fintype]
ren2 [projection, in PR.fintype]
Ren2 [record, in PR.fintype]
ren2 [constructor, in PR.fintype]
Ren2 [inductive, in PR.fintype]
ren3 [projection, in PR.fintype]
Ren3 [record, in PR.fintype]
ren3 [constructor, in PR.fintype]
Ren3 [inductive, in PR.fintype]
ren4 [projection, in PR.fintype]
Ren4 [record, in PR.fintype]
ren4 [constructor, in PR.fintype]
Ren4 [inductive, in PR.fintype]
ren5 [projection, in PR.fintype]
Ren5 [record, in PR.fintype]
ren5 [constructor, in PR.fintype]
Ren5 [inductive, in PR.fintype]
rinstId_tm [lemma, in PR.stlc]
rinstInst_tm [lemma, in PR.stlc]
rinstInst_up_tm_tm [definition, in PR.stlc]
rinst_inst_tm [definition, in PR.stlc]
S
SAbs [constructor, in PR.sn_defs]SApp [constructor, in PR.sn_defs]
SAppl [constructor, in PR.sn_defs]
SBeta [constructor, in PR.sn_defs]
SCaseL [constructor, in PR.sn_defs]
SCaseR [constructor, in PR.sn_defs]
scons [definition, in PR.fintype]
scons_comp [lemma, in PR.fintype]
scons_eta_id [lemma, in PR.fintype]
scons_eta [lemma, in PR.fintype]
shift [definition, in PR.fintype]
SInl [constructor, in PR.sn_defs]
SInr [constructor, in PR.sn_defs]
SN [inductive, in PR.sn_defs]
sn [inductive, in PR.sn_defs]
SNe [inductive, in PR.sn_defs]
SNeu [constructor, in PR.sn_defs]
SNeuOr [constructor, in PR.sn_defs]
SNe_ind_2 [definition, in PR.sn_defs]
snI [constructor, in PR.sn_defs]
SNRed [inductive, in PR.sn_defs]
SN_multind [definition, in PR.sn_defs]
SN_ind_2 [definition, in PR.sn_defs]
sn_mstep [lemma, in PR.sn_defs]
SN_sn [lemma, in PR.sn_inductive_soundness_1b]
sn_confluence [lemma, in PR.sn_inductive_soundness_1a]
sn_case_neutral [lemma, in PR.sn_inductive_soundness_1a]
sn_app_neutral [lemma, in PR.sn_inductive_soundness_1a]
sn_subst_tm [lemma, in PR.sn_inductive_soundness_1a]
sn_appL [lemma, in PR.sn_inductive_soundness_1a]
sn_preimage [lemma, in PR.sn_inductive_soundness_1a]
sn_inductive_soundness_1a [library]
sn_inductive_2a [library]
sn_inductive_soundness_1b [library]
sn_inductive_2b [library]
sn_defs [library]
SOr [constructor, in PR.sn_defs]
SRed [constructor, in PR.sn_defs]
step [inductive, in PR.reduction]
step_inst [lemma, in PR.reduction]
step_weak [lemma, in PR.reduction]
step_caseR' [lemma, in PR.reduction]
step_caseL' [lemma, in PR.reduction]
step_beta' [lemma, in PR.reduction]
step_caseR [constructor, in PR.reduction]
step_caseL [constructor, in PR.reduction]
step_orelimR [constructor, in PR.reduction]
step_orelimL [constructor, in PR.reduction]
step_orelim [constructor, in PR.reduction]
step_inr [constructor, in PR.reduction]
step_inl [constructor, in PR.reduction]
step_appR [constructor, in PR.reduction]
step_appL [constructor, in PR.reduction]
step_abs [constructor, in PR.reduction]
step_beta [constructor, in PR.reduction]
stlc [library]
Subst_tm [instance, in PR.stlc]
subst_tm [definition, in PR.stlc]
subst1 [projection, in PR.fintype]
Subst1 [record, in PR.fintype]
subst1 [constructor, in PR.fintype]
Subst1 [inductive, in PR.fintype]
subst2 [projection, in PR.fintype]
Subst2 [record, in PR.fintype]
subst2 [constructor, in PR.fintype]
Subst2 [inductive, in PR.fintype]
subst3 [projection, in PR.fintype]
Subst3 [record, in PR.fintype]
subst3 [constructor, in PR.fintype]
Subst3 [inductive, in PR.fintype]
subst4 [projection, in PR.fintype]
Subst4 [record, in PR.fintype]
subst4 [constructor, in PR.fintype]
Subst4 [inductive, in PR.fintype]
subst5 [projection, in PR.fintype]
Subst5 [record, in PR.fintype]
subst5 [constructor, in PR.fintype]
Subst5 [inductive, in PR.fintype]
SVar [constructor, in PR.sn_defs]
T
tm [inductive, in PR.stlc]ty [inductive, in PR.stlc]
ty_or [constructor, in PR.sn_inductive_2b]
ty_inr [constructor, in PR.sn_inductive_2b]
ty_inl [constructor, in PR.sn_inductive_2b]
ty_app [constructor, in PR.sn_inductive_2b]
ty_abs [constructor, in PR.sn_inductive_2b]
ty_var_tm [constructor, in PR.sn_inductive_2b]
U
upExtRen_tm_tm [definition, in PR.stlc]upExt_tm_tm [definition, in PR.stlc]
upId_tm_tm [definition, in PR.stlc]
upRen_tm_tm [definition, in PR.stlc]
Up_tm_tm [instance, in PR.stlc]
up_tm [projection, in PR.stlc]
Up_tm [record, in PR.stlc]
up_tm [constructor, in PR.stlc]
Up_tm [inductive, in PR.stlc]
up_subst_subst_tm_tm [definition, in PR.stlc]
up_subst_ren_tm_tm [definition, in PR.stlc]
up_ren_subst_tm_tm [definition, in PR.stlc]
up_tm_tm [definition, in PR.stlc]
up_ren_ren [lemma, in PR.fintype]
up_ren [definition, in PR.fintype]
V
Var [record, in PR.fintype]Var [inductive, in PR.fintype]
VarInstance_tm [instance, in PR.stlc]
varLRen_tm [lemma, in PR.stlc]
varL_tm [lemma, in PR.stlc]
var_tm [constructor, in PR.stlc]
var_zero [definition, in PR.fintype]
other
[ _ ] (fscope) [notation, in PR.stlc]⟨ _ ⟩ (fscope) [notation, in PR.stlc]
⟨ _ ; _ ⟩ (fscope) [notation, in PR.fintype]
⟨ _ ⟩ (fscope) [notation, in PR.fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in PR.stlc]
_ [ _ ] (subst_scope) [notation, in PR.stlc]
↑__tm (subst_scope) [notation, in PR.stlc]
↑__tm (subst_scope) [notation, in PR.stlc]
var (subst_scope) [notation, in PR.stlc]
_ __tm (subst_scope) [notation, in PR.stlc]
_ __tm (subst_scope) [notation, in PR.stlc]
↑ (subst_scope) [notation, in PR.fintype]
_ .. (subst_scope) [notation, in PR.fintype]
_ .: _ (subst_scope) [notation, in PR.fintype]
_ [ _ ; _ ] (subst_scope) [notation, in PR.fintype]
_ [ _ ] (subst_scope) [notation, in PR.fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in PR.fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in PR.fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in PR.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in PR.fintype]
_ ⟨ _ ⟩ (subst_scope) [notation, in PR.fintype]
_ ∈ _ [notation, in PR.reduction]
_ |- _ : _ [notation, in PR.sn_inductive_2b]
_ >> _ [notation, in PR.fintype]
[ Pred _ | _ in _ ] [notation, in PR.reduction]
Notation Index
C
_ , _ (subst_scope) [in PR.fintype]other
[ _ ] (fscope) [in PR.stlc]⟨ _ ⟩ (fscope) [in PR.stlc]
⟨ _ ; _ ⟩ (fscope) [in PR.fintype]
⟨ _ ⟩ (fscope) [in PR.fintype]
_ ⟨ _ ⟩ (subst_scope) [in PR.stlc]
_ [ _ ] (subst_scope) [in PR.stlc]
↑__tm (subst_scope) [in PR.stlc]
↑__tm (subst_scope) [in PR.stlc]
var (subst_scope) [in PR.stlc]
_ __tm (subst_scope) [in PR.stlc]
_ __tm (subst_scope) [in PR.stlc]
↑ (subst_scope) [in PR.fintype]
_ .. (subst_scope) [in PR.fintype]
_ .: _ (subst_scope) [in PR.fintype]
_ [ _ ; _ ] (subst_scope) [in PR.fintype]
_ [ _ ] (subst_scope) [in PR.fintype]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in PR.fintype]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in PR.fintype]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in PR.fintype]
_ ⟨ _ ; _ ⟩ (subst_scope) [in PR.fintype]
_ ⟨ _ ⟩ (subst_scope) [in PR.fintype]
_ ∈ _ [in PR.reduction]
_ |- _ : _ [in PR.sn_inductive_2b]
_ >> _ [in PR.fintype]
[ Pred _ | _ in _ ] [in PR.reduction]
Module Index
C
CommaNotation [in PR.fintype]Library Index
A
axiomsF
fintypeR
reductionS
sn_inductive_soundness_1asn_inductive_2a
sn_inductive_soundness_1b
sn_inductive_2b
sn_defs
stlc
Constructor Index
A
app [in PR.stlc]B
Base [in PR.stlc]C
CNeutral [in PR.sn_inductive_2b]CRefl [in PR.sn_inductive_2b]
CStep [in PR.sn_inductive_2b]
F
Fun [in PR.stlc]I
ids [in PR.fintype]inl [in PR.stlc]
inr [in PR.stlc]
L
lam [in PR.stlc]M
mstep_step [in PR.reduction]mstep_refl [in PR.reduction]
O
orelim [in PR.stlc]P
Plus [in PR.stlc]R
redsn_caseR [in PR.sn_inductive_soundness_1a]redsn_caseL [in PR.sn_inductive_soundness_1a]
redsn_or [in PR.sn_inductive_soundness_1a]
redsn_app [in PR.sn_inductive_soundness_1a]
redsn_beta [in PR.sn_inductive_soundness_1a]
ren1 [in PR.fintype]
ren2 [in PR.fintype]
ren3 [in PR.fintype]
ren4 [in PR.fintype]
ren5 [in PR.fintype]
S
SAbs [in PR.sn_defs]SApp [in PR.sn_defs]
SAppl [in PR.sn_defs]
SBeta [in PR.sn_defs]
SCaseL [in PR.sn_defs]
SCaseR [in PR.sn_defs]
SInl [in PR.sn_defs]
SInr [in PR.sn_defs]
SNeu [in PR.sn_defs]
SNeuOr [in PR.sn_defs]
snI [in PR.sn_defs]
SOr [in PR.sn_defs]
SRed [in PR.sn_defs]
step_caseR [in PR.reduction]
step_caseL [in PR.reduction]
step_orelimR [in PR.reduction]
step_orelimL [in PR.reduction]
step_orelim [in PR.reduction]
step_inr [in PR.reduction]
step_inl [in PR.reduction]
step_appR [in PR.reduction]
step_appL [in PR.reduction]
step_abs [in PR.reduction]
step_beta [in PR.reduction]
subst1 [in PR.fintype]
subst2 [in PR.fintype]
subst3 [in PR.fintype]
subst4 [in PR.fintype]
subst5 [in PR.fintype]
SVar [in PR.sn_defs]
T
ty_or [in PR.sn_inductive_2b]ty_inr [in PR.sn_inductive_2b]
ty_inl [in PR.sn_inductive_2b]
ty_app [in PR.sn_inductive_2b]
ty_abs [in PR.sn_inductive_2b]
ty_var_tm [in PR.sn_inductive_2b]
U
up_tm [in PR.stlc]V
var_tm [in PR.stlc]Lemma Index
A
anti_rename [in PR.sn_inductive_2a]C
closed_orelim [in PR.sn_inductive_soundness_1a]closed_inr [in PR.sn_inductive_soundness_1a]
closed_inl [in PR.sn_inductive_soundness_1a]
closed_appR [in PR.sn_inductive_soundness_1a]
closed_lam [in PR.sn_inductive_soundness_1a]
compComp_tm [in PR.stlc]
compComp'_tm [in PR.stlc]
compRen_tm [in PR.stlc]
compRen'_tm [in PR.stlc]
congr_orelim [in PR.stlc]
congr_inr [in PR.stlc]
congr_inl [in PR.stlc]
congr_lam [in PR.stlc]
congr_app [in PR.stlc]
congr_Plus [in PR.stlc]
congr_Fun [in PR.stlc]
congr_Base [in PR.stlc]
cr [in PR.sn_inductive_2b]
E
ext_SN [in PR.sn_inductive_2a]F
fundamental_backwards_orr [in PR.sn_inductive_soundness_1a]fundamental_backwards_orl [in PR.sn_inductive_soundness_1a]
fundamental_backwards [in PR.sn_inductive_soundness_1a]
I
id_red [in PR.sn_inductive_2b]im_predI [in PR.reduction]
instId_tm [in PR.stlc]
M
main_lemma [in PR.sn_inductive_2b]mstep_beta [in PR.reduction]
mstep_subst [in PR.reduction]
mstep_inst [in PR.reduction]
mstep_orelim [in PR.reduction]
mstep_inr [in PR.reduction]
mstep_inl [in PR.reduction]
mstep_app [in PR.reduction]
mstep_lam [in PR.reduction]
mstep_trans [in PR.reduction]
N
neutral_preservation [in PR.sn_inductive_soundness_1a]norm [in PR.sn_inductive_2b]
P
pi [in PR.axioms]R
redsn_backwards [in PR.sn_inductive_soundness_1a]RedUp [in PR.sn_inductive_2b]
red_var [in PR.sn_inductive_2b]
rename [in PR.sn_inductive_2a]
rename_red [in PR.sn_inductive_2b]
renComp_tm [in PR.stlc]
renComp'_tm [in PR.stlc]
renRen_tm [in PR.stlc]
renRen'_tm [in PR.stlc]
rinstId_tm [in PR.stlc]
rinstInst_tm [in PR.stlc]
S
scons_comp [in PR.fintype]scons_eta_id [in PR.fintype]
scons_eta [in PR.fintype]
sn_mstep [in PR.sn_defs]
SN_sn [in PR.sn_inductive_soundness_1b]
sn_confluence [in PR.sn_inductive_soundness_1a]
sn_case_neutral [in PR.sn_inductive_soundness_1a]
sn_app_neutral [in PR.sn_inductive_soundness_1a]
sn_subst_tm [in PR.sn_inductive_soundness_1a]
sn_appL [in PR.sn_inductive_soundness_1a]
sn_preimage [in PR.sn_inductive_soundness_1a]
step_inst [in PR.reduction]
step_weak [in PR.reduction]
step_caseR' [in PR.reduction]
step_caseL' [in PR.reduction]
step_beta' [in PR.reduction]
U
up_ren_ren [in PR.fintype]V
varLRen_tm [in PR.stlc]varL_tm [in PR.stlc]
Axiom Index
P
pext [in PR.axioms]Inductive Index
C
closure [in PR.sn_inductive_2b]H
has_type [in PR.sn_inductive_2b]M
mstep [in PR.reduction]R
redsn [in PR.sn_inductive_soundness_1a]Ren1 [in PR.fintype]
Ren2 [in PR.fintype]
Ren3 [in PR.fintype]
Ren4 [in PR.fintype]
Ren5 [in PR.fintype]
S
SN [in PR.sn_defs]sn [in PR.sn_defs]
SNe [in PR.sn_defs]
SNRed [in PR.sn_defs]
step [in PR.reduction]
Subst1 [in PR.fintype]
Subst2 [in PR.fintype]
Subst3 [in PR.fintype]
Subst4 [in PR.fintype]
Subst5 [in PR.fintype]
T
tm [in PR.stlc]ty [in PR.stlc]
U
Up_tm [in PR.stlc]V
Var [in PR.fintype]Projection Index
I
ids [in PR.fintype]R
ren1 [in PR.fintype]ren2 [in PR.fintype]
ren3 [in PR.fintype]
ren4 [in PR.fintype]
ren5 [in PR.fintype]
S
subst1 [in PR.fintype]subst2 [in PR.fintype]
subst3 [in PR.fintype]
subst4 [in PR.fintype]
subst5 [in PR.fintype]
U
up_tm [in PR.stlc]Instance Index
R
Ren_tm [in PR.stlc]S
Subst_tm [in PR.stlc]U
Up_tm_tm [in PR.stlc]V
VarInstance_tm [in PR.stlc]Definition Index
A
ap [in PR.fintype]apc [in PR.fintype]
C
comp [in PR.fintype]compRenRen_tm [in PR.stlc]
compRenSubst_tm [in PR.stlc]
compSubstRen__tm [in PR.stlc]
compSubstSubst_tm [in PR.stlc]
ctx [in PR.sn_inductive_2b]
E
extRen_tm [in PR.stlc]ext_tm [in PR.stlc]
F
fin [in PR.fintype]funcomp [in PR.fintype]
I
id [in PR.fintype]idren [in PR.fintype]
idSubst_tm [in PR.stlc]
ImPred [in PR.reduction]
N
neutral [in PR.sn_inductive_soundness_1a]null [in PR.fintype]
R
Red [in PR.sn_inductive_2b]RedS [in PR.sn_inductive_2b]
redSN_ind_2 [in PR.sn_defs]
ren [in PR.fintype]
ren_tm [in PR.stlc]
rinstInst_up_tm_tm [in PR.stlc]
rinst_inst_tm [in PR.stlc]
S
scons [in PR.fintype]shift [in PR.fintype]
SNe_ind_2 [in PR.sn_defs]
SN_multind [in PR.sn_defs]
SN_ind_2 [in PR.sn_defs]
subst_tm [in PR.stlc]
U
upExtRen_tm_tm [in PR.stlc]upExt_tm_tm [in PR.stlc]
upId_tm_tm [in PR.stlc]
upRen_tm_tm [in PR.stlc]
up_subst_subst_tm_tm [in PR.stlc]
up_subst_ren_tm_tm [in PR.stlc]
up_ren_subst_tm_tm [in PR.stlc]
up_tm_tm [in PR.stlc]
up_ren [in PR.fintype]
V
var_zero [in PR.fintype]Record Index
R
Ren1 [in PR.fintype]Ren2 [in PR.fintype]
Ren3 [in PR.fintype]
Ren4 [in PR.fintype]
Ren5 [in PR.fintype]
S
Subst1 [in PR.fintype]Subst2 [in PR.fintype]
Subst3 [in PR.fintype]
Subst4 [in PR.fintype]
Subst5 [in PR.fintype]
U
Up_tm [in PR.stlc]V
Var [in PR.fintype]| 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 | (260 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 | (26 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 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 | (62 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 | (69 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (23 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 | (12 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 | (4 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 | (41 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 | (12 entries) |