| 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 | (185 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 | (23 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 | (4 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 | (44 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) |
| 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 | (31 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 | (11 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 | (18 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) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 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 | (11 entries) |
Global Index
A
algeq [inductive, in LOG.logrel]algeqNeu [inductive, in LOG.logrel]
algeqNeu_ind_2 [definition, in LOG.logrel]
algeq_trans [lemma, in LOG.logrel]
algeq_sym [lemma, in LOG.logrel]
algeq_backward_closure [lemma, in LOG.logrel]
algEq_monotone [lemma, in LOG.logrel]
algeq_mut_ind [definition, in LOG.logrel]
algeq_ind_2 [definition, in LOG.logrel]
alg_app [constructor, in LOG.logrel]
alg_var [constructor, in LOG.logrel]
alg_arr [constructor, in LOG.logrel]
alg_base [constructor, in LOG.logrel]
ap [definition, in LOG.unscoped]
apc [definition, in LOG.unscoped]
app [constructor, in LOG.Syntax]
arr [constructor, in LOG.Syntax]
axioms [library]
B
Base [constructor, in LOG.Syntax]beta [constructor, in LOG.logrel]
C
compComp_tm [lemma, in LOG.Syntax]compComp'_tm [lemma, in LOG.Syntax]
completeness [lemma, in LOG.logrel]
compRenRen_tm [definition, in LOG.Syntax]
compRenSubst_tm [definition, in LOG.Syntax]
compRen_tm [lemma, in LOG.Syntax]
compRen'_tm [lemma, in LOG.Syntax]
compSubstRen__tm [definition, in LOG.Syntax]
compSubstSubst_tm [definition, in LOG.Syntax]
confluence [lemma, in LOG.logrel]
congr_lam [lemma, in LOG.Syntax]
congr_app [lemma, in LOG.Syntax]
congr_arr [lemma, in LOG.Syntax]
congr_Base [lemma, in LOG.Syntax]
cont_ext_id [lemma, in LOG.logrel]
cont_ext_cons [lemma, in LOG.logrel]
cont_ext_shift [lemma, in LOG.logrel]
cont_ext [definition, in LOG.logrel]
ctx [definition, in LOG.logrel]
D
DecApp [constructor, in LOG.logrel]DecBeta [constructor, in LOG.logrel]
DecExt [constructor, in LOG.logrel]
DecLam [constructor, in LOG.logrel]
decleq [inductive, in LOG.logrel]
DecSym [constructor, in LOG.logrel]
DecTrans [constructor, in LOG.logrel]
DecVar [constructor, in LOG.logrel]
E
extRen_tm [definition, in LOG.Syntax]ext_tm [definition, in LOG.Syntax]
F
fin [abbreviation, in LOG.unscoped]funcomp [definition, in LOG.unscoped]
fundamental [lemma, in LOG.logrel]
G
get [definition, in LOG.logrel]I
id [definition, in LOG.unscoped]ids [projection, in LOG.unscoped]
ids [constructor, in LOG.unscoped]
idsRen [instance, in LOG.unscoped]
idSubst_tm [definition, in LOG.Syntax]
instId_tm [lemma, in LOG.Syntax]
L
lam [constructor, in LOG.Syntax]logeq [definition, in LOG.logrel]
logeq_rel [definition, in LOG.logrel]
logeq_trans [lemma, in LOG.logrel]
logeq_sym [lemma, in LOG.logrel]
logeq_backward_closure [lemma, in LOG.logrel]
logEq_monotone [lemma, in LOG.logrel]
logrel [library]
M
main [lemma, in LOG.logrel]mstep [inductive, in LOG.logrel]
mstepR [constructor, in LOG.logrel]
mstepS [constructor, in LOG.logrel]
mstep_ren [lemma, in LOG.logrel]
mstep_trans [lemma, in LOG.logrel]
mstep_appL [lemma, in LOG.logrel]
N
neutral_mstep [lemma, in LOG.logrel]neutral_step [lemma, in LOG.logrel]
None [definition, in LOG.unscoped]
P
pext [axiom, in LOG.axioms]pi [lemma, in LOG.axioms]
R
renComp_tm [lemma, in LOG.Syntax]renComp'_tm [lemma, in LOG.Syntax]
renRen_tm [lemma, in LOG.Syntax]
renRen'_tm [lemma, in LOG.Syntax]
Ren_tm [instance, in LOG.Syntax]
ren_tm [definition, in LOG.Syntax]
ren1 [projection, in LOG.unscoped]
Ren1 [record, in LOG.unscoped]
ren1 [constructor, in LOG.unscoped]
Ren1 [inductive, in LOG.unscoped]
ren2 [projection, in LOG.unscoped]
Ren2 [record, in LOG.unscoped]
ren2 [constructor, in LOG.unscoped]
Ren2 [inductive, in LOG.unscoped]
ren3 [projection, in LOG.unscoped]
Ren3 [record, in LOG.unscoped]
ren3 [constructor, in LOG.unscoped]
Ren3 [inductive, in LOG.unscoped]
ren4 [projection, in LOG.unscoped]
Ren4 [record, in LOG.unscoped]
ren4 [constructor, in LOG.unscoped]
Ren4 [inductive, in LOG.unscoped]
ren5 [projection, in LOG.unscoped]
Ren5 [record, in LOG.unscoped]
ren5 [constructor, in LOG.unscoped]
Ren5 [inductive, in LOG.unscoped]
rinstId_tm [lemma, in LOG.Syntax]
rinstInst_tm [lemma, in LOG.Syntax]
rinstInst_up_tm_tm [definition, in LOG.Syntax]
rinst_inst_tm [definition, in LOG.Syntax]
S
scons [definition, in LOG.unscoped]scons_comp [lemma, in LOG.unscoped]
scons_eta_id [lemma, in LOG.unscoped]
scons_eta [lemma, in LOG.unscoped]
shift [definition, in LOG.unscoped]
Some [definition, in LOG.unscoped]
step [inductive, in LOG.logrel]
stepapp [constructor, in LOG.logrel]
step_ren [lemma, in LOG.logrel]
Subst_tm [instance, in LOG.Syntax]
subst_tm [definition, in LOG.Syntax]
subst1 [projection, in LOG.unscoped]
Subst1 [record, in LOG.unscoped]
subst1 [constructor, in LOG.unscoped]
Subst1 [inductive, in LOG.unscoped]
subst2 [projection, in LOG.unscoped]
Subst2 [record, in LOG.unscoped]
subst2 [constructor, in LOG.unscoped]
Subst2 [inductive, in LOG.unscoped]
subst3 [projection, in LOG.unscoped]
Subst3 [record, in LOG.unscoped]
subst3 [constructor, in LOG.unscoped]
Subst3 [inductive, in LOG.unscoped]
subst4 [projection, in LOG.unscoped]
Subst4 [record, in LOG.unscoped]
subst4 [constructor, in LOG.unscoped]
Subst4 [inductive, in LOG.unscoped]
subst5 [projection, in LOG.unscoped]
Subst5 [record, in LOG.unscoped]
subst5 [constructor, in LOG.unscoped]
Subst5 [inductive, in LOG.unscoped]
Syntax [library]
T
tm [inductive, in LOG.Syntax]ty [inductive, in LOG.Syntax]
type_unique [lemma, in LOG.logrel]
U
unscoped [library]upExtRen_tm_tm [definition, in LOG.Syntax]
upExt_tm_tm [definition, in LOG.Syntax]
upId_tm_tm [definition, in LOG.Syntax]
upRen_tm_tm [definition, in LOG.Syntax]
up_ren_ren [lemma, in LOG.unscoped]
up_ren [definition, in LOG.unscoped]
up_subst_subst_tm_tm [definition, in LOG.Syntax]
up_subst_ren_tm_tm [definition, in LOG.Syntax]
up_ren_subst_tm_tm [definition, in LOG.Syntax]
up_tm_tm [definition, in LOG.Syntax]
V
Var [record, in LOG.unscoped]Var [inductive, in LOG.unscoped]
VarInstance_tm [instance, in LOG.Syntax]
varLRen_tm [lemma, in LOG.Syntax]
varL_tm [lemma, in LOG.Syntax]
var_zero [definition, in LOG.unscoped]
var_tm [constructor, in LOG.Syntax]
other
[ _ ] (fscope) [notation, in LOG.Syntax]⟨ _ ; _ ⟩ (fscope) [notation, in LOG.unscoped]
⟨ _ ⟩ (fscope) [notation, in LOG.unscoped]
⟨ _ ⟩ (fscope) [notation, in LOG.Syntax]
_ .. (subst_scope) [notation, in LOG.unscoped]
_ , _ (subst_scope) [notation, in LOG.unscoped]
_ >> _ (subst_scope) [notation, in LOG.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in LOG.unscoped]
_ [ _ ] (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in LOG.Syntax]
_ [ _ ] (subst_scope) [notation, in LOG.Syntax]
⇑__tm (subst_scope) [notation, in LOG.Syntax]
var (subst_scope) [notation, in LOG.Syntax]
_ __tm (subst_scope) [notation, in LOG.Syntax]
_ __tm (subst_scope) [notation, in LOG.Syntax]
_ .: _ [notation, in LOG.unscoped]
_ `_ _ [notation, in LOG.logrel]
↑ [notation, in LOG.unscoped]
Notation Index
other
[ _ ] (fscope) [in LOG.Syntax]⟨ _ ; _ ⟩ (fscope) [in LOG.unscoped]
⟨ _ ⟩ (fscope) [in LOG.unscoped]
⟨ _ ⟩ (fscope) [in LOG.Syntax]
_ .. (subst_scope) [in LOG.unscoped]
_ , _ (subst_scope) [in LOG.unscoped]
_ >> _ (subst_scope) [in LOG.unscoped]
_ [ _ ; _ ] (subst_scope) [in LOG.unscoped]
_ [ _ ] (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in LOG.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in LOG.Syntax]
_ [ _ ] (subst_scope) [in LOG.Syntax]
⇑__tm (subst_scope) [in LOG.Syntax]
var (subst_scope) [in LOG.Syntax]
_ __tm (subst_scope) [in LOG.Syntax]
_ __tm (subst_scope) [in LOG.Syntax]
_ .: _ [in LOG.unscoped]
_ `_ _ [in LOG.logrel]
↑ [in LOG.unscoped]
Library Index
A
axiomsL
logrelS
SyntaxU
unscopedLemma Index
A
algeq_trans [in LOG.logrel]algeq_sym [in LOG.logrel]
algeq_backward_closure [in LOG.logrel]
algEq_monotone [in LOG.logrel]
C
compComp_tm [in LOG.Syntax]compComp'_tm [in LOG.Syntax]
completeness [in LOG.logrel]
compRen_tm [in LOG.Syntax]
compRen'_tm [in LOG.Syntax]
confluence [in LOG.logrel]
congr_lam [in LOG.Syntax]
congr_app [in LOG.Syntax]
congr_arr [in LOG.Syntax]
congr_Base [in LOG.Syntax]
cont_ext_id [in LOG.logrel]
cont_ext_cons [in LOG.logrel]
cont_ext_shift [in LOG.logrel]
F
fundamental [in LOG.logrel]I
instId_tm [in LOG.Syntax]L
logeq_trans [in LOG.logrel]logeq_sym [in LOG.logrel]
logeq_backward_closure [in LOG.logrel]
logEq_monotone [in LOG.logrel]
M
main [in LOG.logrel]mstep_ren [in LOG.logrel]
mstep_trans [in LOG.logrel]
mstep_appL [in LOG.logrel]
N
neutral_mstep [in LOG.logrel]neutral_step [in LOG.logrel]
P
pi [in LOG.axioms]R
renComp_tm [in LOG.Syntax]renComp'_tm [in LOG.Syntax]
renRen_tm [in LOG.Syntax]
renRen'_tm [in LOG.Syntax]
rinstId_tm [in LOG.Syntax]
rinstInst_tm [in LOG.Syntax]
S
scons_comp [in LOG.unscoped]scons_eta_id [in LOG.unscoped]
scons_eta [in LOG.unscoped]
step_ren [in LOG.logrel]
T
type_unique [in LOG.logrel]U
up_ren_ren [in LOG.unscoped]V
varLRen_tm [in LOG.Syntax]varL_tm [in LOG.Syntax]
Axiom Index
P
pext [in LOG.axioms]Constructor Index
A
alg_app [in LOG.logrel]alg_var [in LOG.logrel]
alg_arr [in LOG.logrel]
alg_base [in LOG.logrel]
app [in LOG.Syntax]
arr [in LOG.Syntax]
B
Base [in LOG.Syntax]beta [in LOG.logrel]
D
DecApp [in LOG.logrel]DecBeta [in LOG.logrel]
DecExt [in LOG.logrel]
DecLam [in LOG.logrel]
DecSym [in LOG.logrel]
DecTrans [in LOG.logrel]
DecVar [in LOG.logrel]
I
ids [in LOG.unscoped]L
lam [in LOG.Syntax]M
mstepR [in LOG.logrel]mstepS [in LOG.logrel]
R
ren1 [in LOG.unscoped]ren2 [in LOG.unscoped]
ren3 [in LOG.unscoped]
ren4 [in LOG.unscoped]
ren5 [in LOG.unscoped]
S
stepapp [in LOG.logrel]subst1 [in LOG.unscoped]
subst2 [in LOG.unscoped]
subst3 [in LOG.unscoped]
subst4 [in LOG.unscoped]
subst5 [in LOG.unscoped]
V
var_tm [in LOG.Syntax]Projection Index
I
ids [in LOG.unscoped]R
ren1 [in LOG.unscoped]ren2 [in LOG.unscoped]
ren3 [in LOG.unscoped]
ren4 [in LOG.unscoped]
ren5 [in LOG.unscoped]
S
subst1 [in LOG.unscoped]subst2 [in LOG.unscoped]
subst3 [in LOG.unscoped]
subst4 [in LOG.unscoped]
subst5 [in LOG.unscoped]
Inductive Index
A
algeq [in LOG.logrel]algeqNeu [in LOG.logrel]
D
decleq [in LOG.logrel]M
mstep [in LOG.logrel]R
Ren1 [in LOG.unscoped]Ren2 [in LOG.unscoped]
Ren3 [in LOG.unscoped]
Ren4 [in LOG.unscoped]
Ren5 [in LOG.unscoped]
S
step [in LOG.logrel]Subst1 [in LOG.unscoped]
Subst2 [in LOG.unscoped]
Subst3 [in LOG.unscoped]
Subst4 [in LOG.unscoped]
Subst5 [in LOG.unscoped]
T
tm [in LOG.Syntax]ty [in LOG.Syntax]
V
Var [in LOG.unscoped]Instance Index
I
idsRen [in LOG.unscoped]R
Ren_tm [in LOG.Syntax]S
Subst_tm [in LOG.Syntax]V
VarInstance_tm [in LOG.Syntax]Abbreviation Index
F
fin [in LOG.unscoped]Definition Index
A
algeqNeu_ind_2 [in LOG.logrel]algeq_mut_ind [in LOG.logrel]
algeq_ind_2 [in LOG.logrel]
ap [in LOG.unscoped]
apc [in LOG.unscoped]
C
compRenRen_tm [in LOG.Syntax]compRenSubst_tm [in LOG.Syntax]
compSubstRen__tm [in LOG.Syntax]
compSubstSubst_tm [in LOG.Syntax]
cont_ext [in LOG.logrel]
ctx [in LOG.logrel]
E
extRen_tm [in LOG.Syntax]ext_tm [in LOG.Syntax]
F
funcomp [in LOG.unscoped]G
get [in LOG.logrel]I
id [in LOG.unscoped]idSubst_tm [in LOG.Syntax]
L
logeq [in LOG.logrel]logeq_rel [in LOG.logrel]
N
None [in LOG.unscoped]R
ren_tm [in LOG.Syntax]rinstInst_up_tm_tm [in LOG.Syntax]
rinst_inst_tm [in LOG.Syntax]
S
scons [in LOG.unscoped]shift [in LOG.unscoped]
Some [in LOG.unscoped]
subst_tm [in LOG.Syntax]
U
upExtRen_tm_tm [in LOG.Syntax]upExt_tm_tm [in LOG.Syntax]
upId_tm_tm [in LOG.Syntax]
upRen_tm_tm [in LOG.Syntax]
up_ren [in LOG.unscoped]
up_subst_subst_tm_tm [in LOG.Syntax]
up_subst_ren_tm_tm [in LOG.Syntax]
up_ren_subst_tm_tm [in LOG.Syntax]
up_tm_tm [in LOG.Syntax]
V
var_zero [in LOG.unscoped]Record Index
R
Ren1 [in LOG.unscoped]Ren2 [in LOG.unscoped]
Ren3 [in LOG.unscoped]
Ren4 [in LOG.unscoped]
Ren5 [in LOG.unscoped]
S
Subst1 [in LOG.unscoped]Subst2 [in LOG.unscoped]
Subst3 [in LOG.unscoped]
Subst4 [in LOG.unscoped]
Subst5 [in LOG.unscoped]
V
Var [in LOG.unscoped]| 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 | (185 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 | (23 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 | (4 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 | (44 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) |
| 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 | (31 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 | (11 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 | (18 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) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 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 | (11 entries) |