| 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 | (563 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 | (3 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 | (187 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 | (26 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 | (127 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 | (86 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 | (10 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 | (39 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 | (11 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 | (74 entries) |
Global Index
A
andb_intro [lemma, in Prfx.check_sound]B
Bot [abbreviation, in Prfx.objects]bot [constructor, in Prfx.objects]
bot_elim [constructor, in Prfx.objects]
bot_inv [lemma, in Prfx.inv_lems]
C
check [definition, in Prfx.check]check [library]
checksec [section, in Prfx.check]
checksec.F [variable, in Prfx.check]
checksec.l1 [variable, in Prfx.check]
checksec.l2 [variable, in Prfx.check]
checksec.P [variable, in Prfx.check]
checksec.T [variable, in Prfx.check]
checksec.Ts [variable, in Prfx.check]
check_sound [library]
check2ND [lemma, in Prfx.check_sound]
cnj [constructor, in Prfx.objects]
cnj_elim2 [constructor, in Prfx.objects]
cnj_elim1 [constructor, in Prfx.objects]
cnj_intro [constructor, in Prfx.objects]
cnj_elim2_inv [lemma, in Prfx.inv_lems]
cnj_elim1_inv [lemma, in Prfx.inv_lems]
cnj_intro_inv [lemma, in Prfx.inv_lems]
commute_lift_subst_cxt [lemma, in Prfx.subst_lems]
commute_lift_subst_frm [lemma, in Prfx.subst_lems]
commute_lift_subst_trms [lemma, in Prfx.subst_lems]
commute_lift_subst_trm [lemma, in Prfx.subst_lems]
commute_lift_subst_var [lemma, in Prfx.subst_lems]
Conj [abbreviation, in Prfx.list]
consn [constructor, in Prfx.list]
contr [definition, in Prfx.contr]
contr [library]
contr_hyp [definition, in Prfx.contr]
contr_prf.P [variable, in Prfx.contr]
contr_prf.l2 [variable, in Prfx.contr]
contr_prf.l1 [variable, in Prfx.contr]
contr_prf [section, in Prfx.contr]
D
distr_lift_substO_frm [lemma, in Prfx.lift_lems]distr_lift_subst_frm [lemma, in Prfx.lift_lems]
distr_lift_subst_trms [lemma, in Prfx.lift_lems]
distr_lift_subst_trm [lemma, in Prfx.lift_lems]
distr_lift_subst_var [lemma, in Prfx.lift_lems]
distr_subst_frm [lemma, in Prfx.subst_lems]
distr_subst_trms [lemma, in Prfx.subst_lems]
distr_subst_trm [lemma, in Prfx.subst_lems]
distr_subst_var [lemma, in Prfx.subst_lems]
dsj [constructor, in Prfx.objects]
dsj_elim [constructor, in Prfx.objects]
dsj_intro2 [constructor, in Prfx.objects]
dsj_intro1 [constructor, in Prfx.objects]
dsj_elim_inv [lemma, in Prfx.inv_lems]
dsj_intro2_inv [lemma, in Prfx.inv_lems]
dsj_intro1_inv [lemma, in Prfx.inv_lems]
E
emp [definition, in Prfx.objects]empty [inductive, in Prfx.indices]
empty_ind' [definition, in Prfx.indices]
eq_consn [lemma, in Prfx.list]
eq_dep_consn [lemma, in Prfx.list]
eq_niln [lemma, in Prfx.list]
eq_dep_niln [lemma, in Prfx.list]
Err [abbreviation, in Prfx.list]
err [constructor, in Prfx.list]
eval [library]
evaluation [section, in Prfx.eval]
evaluation.A [variable, in Prfx.eval]
evaluation.F [variable, in Prfx.eval]
evaluation.formula_evaluation.dflt [variable, in Prfx.eval]
evaluation.formula_evaluation.REL [variable, in Prfx.eval]
evaluation.formula_evaluation [section, in Prfx.eval]
evaluation.FUN [variable, in Prfx.eval]
evaluation.l1 [variable, in Prfx.eval]
evaluation.l2 [variable, in Prfx.eval]
evaluation.P [variable, in Prfx.eval]
evaluation.T [variable, in Prfx.eval]
evaluation.term_evaluation.VAR [variable, in Prfx.eval]
evaluation.term_evaluation [section, in Prfx.eval]
evaluation.Ts [variable, in Prfx.eval]
eval_lift_lemmas.Ecxt [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.Etrm [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.E [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.C [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.Ts [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.T [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.F [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.P [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.REL [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.FUN [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.l2 [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.l1 [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas.A [variable, in Prfx.eval_lift_lems]
eval_lift_lemmas [section, in Prfx.eval_lift_lems]
eval_subst_frm_ok2 [lemma, in Prfx.eval_subst_lems]
eval_subst_frm_ok1 [lemma, in Prfx.eval_subst_lems]
eval_subst_frm_ok [lemma, in Prfx.eval_subst_lems]
eval_subst_trms_ok [lemma, in Prfx.eval_subst_lems]
eval_subst_trm_ok [lemma, in Prfx.eval_subst_lems]
eval_subst_var_ok [lemma, in Prfx.eval_subst_lems]
eval_subst_lemmas.Ecxt [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.Etrm [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.E [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.C [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.Ts [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.T [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.F [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.P [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.REL [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.FUN [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.l2 [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.l1 [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas.A [variable, in Prfx.eval_subst_lems]
eval_subst_lemmas [section, in Prfx.eval_subst_lems]
eval_cxt [definition, in Prfx.eval]
eval_frm [definition, in Prfx.eval]
eval_cxt' [definition, in Prfx.eval]
eval_frm' [definition, in Prfx.eval]
eval_trms [definition, in Prfx.eval]
eval_trm [definition, in Prfx.eval]
eval_subst_lems [library]
eval_lift_lems [library]
exch [definition, in Prfx.exch]
exch [library]
exch_ok3 [lemma, in Prfx.exch]
exch_ok2 [lemma, in Prfx.exch]
exch_ok1 [lemma, in Prfx.exch]
exch_hyp [definition, in Prfx.exch]
exch_prf.P [variable, in Prfx.exch]
exch_prf.l2 [variable, in Prfx.exch]
exch_prf.l1 [variable, in Prfx.exch]
exch_prf [section, in Prfx.exch]
existTS [constructor, in Prfx.indices]
exq [constructor, in Prfx.objects]
exq_elim [constructor, in Prfx.objects]
exq_intro [constructor, in Prfx.objects]
exq_elim_inv [lemma, in Prfx.inv_lems]
exq_intro_inv [lemma, in Prfx.inv_lems]
F
free_inb_frm [definition, in Prfx.objects]free_inb_trms [definition, in Prfx.objects]
free_inb_trm [definition, in Prfx.objects]
frm [inductive, in Prfx.objects]
frm_eqb_dec [lemma, in Prfx.check_sound]
frm_eqb_refl [lemma, in Prfx.check_sound]
frm_eqb [definition, in Prfx.objects]
from_empty [definition, in Prfx.indices]
fun_ [constructor, in Prfx.objects]
fun_piT [definition, in Prfx.eval]
H
Hyp [abbreviation, in Prfx.objects]hyp [constructor, in Prfx.objects]
hypO_inv [lemma, in Prfx.inv_lems]
hypS_inv [lemma, in Prfx.inv_lems]
I
imm_red [inductive, in Prfx.red]imp [constructor, in Prfx.objects]
imp_elim [constructor, in Prfx.objects]
imp_intro [constructor, in Prfx.objects]
imp_elim_inv [lemma, in Prfx.inv_lems]
imp_intro_inv [lemma, in Prfx.inv_lems]
index [definition, in Prfx.indices]
index_inj [definition, in Prfx.indices]
index_eqb_dec [lemma, in Prfx.indices]
index_eqb_refl [lemma, in Prfx.indices]
index_eqb [definition, in Prfx.indices]
index2nat [definition, in Prfx.indices]
indices [section, in Prfx.indices]
indices [library]
indices.A [variable, in Prfx.indices]
indices.index_L.len [variable, in Prfx.indices]
indices.index_L.L [variable, in Prfx.indices]
indices.index_L [section, in Prfx.indices]
inn [definition, in Prfx.list]
insertVAR [definition, in Prfx.eval]
insertVAR_O [definition, in Prfx.eval]
insVARswap [lemma, in Prfx.eval_lift_lems]
insVAR_shift [lemma, in Prfx.eval_lift_lems]
Inversion_Lemmata.C [variable, in Prfx.inv_lems]
Inversion_Lemmata.Ts [variable, in Prfx.inv_lems]
Inversion_Lemmata.T [variable, in Prfx.inv_lems]
Inversion_Lemmata.F [variable, in Prfx.inv_lems]
Inversion_Lemmata.P [variable, in Prfx.inv_lems]
Inversion_Lemmata.l2 [variable, in Prfx.inv_lems]
Inversion_Lemmata.l1 [variable, in Prfx.inv_lems]
Inversion_Lemmata [section, in Prfx.inv_lems]
inv_lems [library]
L
length_map [lemma, in Prfx.list]lift [definition, in Prfx.lift]
lift [library]
lifting [section, in Prfx.lift]
lifting_lemmas.C [variable, in Prfx.lift_lems]
lifting_lemmas.Ts [variable, in Prfx.lift_lems]
lifting_lemmas.T [variable, in Prfx.lift_lems]
lifting_lemmas.F [variable, in Prfx.lift_lems]
lifting_lemmas.P [variable, in Prfx.lift_lems]
lifting_lemmas.l2 [variable, in Prfx.lift_lems]
lifting_lemmas.l1 [variable, in Prfx.lift_lems]
lifting_lemmas [section, in Prfx.lift_lems]
lifting.A [variable, in Prfx.lift]
lifting.F [variable, in Prfx.lift]
lifting.l1 [variable, in Prfx.lift]
lifting.l2 [variable, in Prfx.lift]
lifting.P [variable, in Prfx.lift]
lifting.T [variable, in Prfx.lift]
lifting.Ts [variable, in Prfx.lift]
lift_hyp_prf [definition, in Prfx.lift]
lift_var_prf [definition, in Prfx.lift]
lift_cxt [definition, in Prfx.lift]
lift_frm [definition, in Prfx.lift]
lift_trms [definition, in Prfx.lift]
lift_trm [definition, in Prfx.lift]
lift_proj_frm_simpl [lemma, in Prfx.lift_lems]
lift_proj_trms_simpl [lemma, in Prfx.lift_lems]
lift_proj_trm_simpl [lemma, in Prfx.lift_lems]
lift_proj_simpl [lemma, in Prfx.lift_lems]
lift_lems [library]
list [library]
listn [inductive, in Prfx.list]
listns [section, in Prfx.list]
listns.A [variable, in Prfx.list]
listns.A_eqb_dec [variable, in Prfx.list]
listns.A_eqb_refl [variable, in Prfx.list]
listns.A_eqb [variable, in Prfx.list]
listn_eqb_dec [lemma, in Prfx.list]
listn_eqb_refl [lemma, in Prfx.list]
listn_eqb [definition, in Prfx.list]
ltll [definition, in Prfx.indices]
ltll_dec [definition, in Prfx.indices]
ltll_dec_opaque [lemma, in Prfx.indices]
M
mapn [definition, in Prfx.list]mapnb [definition, in Prfx.list]
mapnb_orb_false [lemma, in Prfx.list]
mapns [section, in Prfx.list]
mapns.A [variable, in Prfx.list]
mapns.B [variable, in Prfx.list]
mapns.f [variable, in Prfx.list]
mapns.p [variable, in Prfx.list]
mapn_id [lemma, in Prfx.list]
mapn_mapn [lemma, in Prfx.list]
mapn_inn [lemma, in Prfx.list]
mapn_feeg [lemma, in Prfx.list]
mapn_andb [definition, in Prfx.list]
mapn_orb [definition, in Prfx.list]
map_prf_hyp [definition, in Prfx.objects]
map_prf_var [definition, in Prfx.objects]
map_frm_var [definition, in Prfx.objects]
map_trm [definition, in Prfx.objects]
map_map [lemma, in Prfx.list]
map_feeg [lemma, in Prfx.list]
map_app [lemma, in Prfx.list]
more_on_lists.f2 [variable, in Prfx.list]
more_on_lists.f1 [variable, in Prfx.list]
more_on_lists.C [variable, in Prfx.list]
more_on_lists.ee [variable, in Prfx.list]
more_on_lists.g [variable, in Prfx.list]
more_on_lists.f [variable, in Prfx.list]
more_on_lists.B [variable, in Prfx.list]
more_on_lists.A [variable, in Prfx.list]
more_on_lists [section, in Prfx.list]
N
Natural_Deduction.P [variable, in Prfx.ND]Natural_Deduction.C [variable, in Prfx.ND]
Natural_Deduction.F [variable, in Prfx.ND]
Natural_Deduction.T [variable, in Prfx.ND]
Natural_Deduction.l2 [variable, in Prfx.ND]
Natural_Deduction.l1 [variable, in Prfx.ND]
Natural_Deduction [section, in Prfx.ND]
nat_eqb_refl [lemma, in Prfx.nat_eqb]
nat_eqb_dec [lemma, in Prfx.nat_eqb]
nat_eqb [definition, in Prfx.nat_eqb]
nat_inj [definition, in Prfx.indices]
nat_eqb [library]
nat2index [definition, in Prfx.indices]
nat2index_sig [definition, in Prfx.indices]
ND [inductive, in Prfx.ND]
ND [library]
ND_hyp_nth [lemma, in Prfx.check_sound]
ND_exq_elim [constructor, in Prfx.ND]
ND_exq_intro [constructor, in Prfx.ND]
ND_uvq_elim [constructor, in Prfx.ND]
ND_uvq_intro [constructor, in Prfx.ND]
ND_dsj_elim [constructor, in Prfx.ND]
ND_dsj_intro2 [constructor, in Prfx.ND]
ND_dsj_intro1 [constructor, in Prfx.ND]
ND_cnj_elim2 [constructor, in Prfx.ND]
ND_cnj_elim1 [constructor, in Prfx.ND]
ND_cnj_intro [constructor, in Prfx.ND]
ND_imp_elim [constructor, in Prfx.ND]
ND_imp_intro [constructor, in Prfx.ND]
ND_bot_elim [constructor, in Prfx.ND]
ND_hypS [constructor, in Prfx.ND]
ND_hypO [constructor, in Prfx.ND]
ND_top_intro [constructor, in Prfx.ND]
ND_exch [lemma, in Prfx.ND_exch]
ND_exch_hyp [lemma, in Prfx.ND_exch]
ND_exchange_rule.P [variable, in Prfx.ND_exch]
ND_exchange_rule.X [variable, in Prfx.ND_exch]
ND_exchange_rule.F [variable, in Prfx.ND_exch]
ND_exchange_rule.T [variable, in Prfx.ND_exch]
ND_exchange_rule.l2 [variable, in Prfx.ND_exch]
ND_exchange_rule.l1 [variable, in Prfx.ND_exch]
ND_exchange_rule [section, in Prfx.ND_exch]
ND_contr [lemma, in Prfx.ND_contr]
ND_contr_hyp [lemma, in Prfx.ND_contr]
ND_contraction_rule.P [variable, in Prfx.ND_contr]
ND_contraction_rule.l2 [variable, in Prfx.ND_contr]
ND_contraction_rule.l1 [variable, in Prfx.ND_contr]
ND_contraction_rule [section, in Prfx.ND_contr]
ND_weakening [lemma, in Prfx.ND_lift_lems]
ND_weak_hyp [lemma, in Prfx.ND_lift_lems]
ND_lift_var [lemma, in Prfx.ND_lift_lems]
ND_lifting_lemmas.C [variable, in Prfx.ND_lift_lems]
ND_lifting_lemmas.Ts [variable, in Prfx.ND_lift_lems]
ND_lifting_lemmas.T [variable, in Prfx.ND_lift_lems]
ND_lifting_lemmas.F [variable, in Prfx.ND_lift_lems]
ND_lifting_lemmas.P [variable, in Prfx.ND_lift_lems]
ND_lifting_lemmas.l2 [variable, in Prfx.ND_lift_lems]
ND_lifting_lemmas.l1 [variable, in Prfx.ND_lift_lems]
ND_lifting_lemmas [section, in Prfx.ND_lift_lems]
ND_sound [lemma, in Prfx.ND_sound]
ND_substitution_lemmas.C [variable, in Prfx.ND_subst_lems]
ND_substitution_lemmas.Ts [variable, in Prfx.ND_subst_lems]
ND_substitution_lemmas.T [variable, in Prfx.ND_subst_lems]
ND_substitution_lemmas.F [variable, in Prfx.ND_subst_lems]
ND_substitution_lemmas.P [variable, in Prfx.ND_subst_lems]
ND_substitution_lemmas.l2 [variable, in Prfx.ND_subst_lems]
ND_substitution_lemmas.l1 [variable, in Prfx.ND_subst_lems]
ND_substitution_lemmas [section, in Prfx.ND_subst_lems]
ND_exch [library]
ND_lift_lems [library]
ND_subst_lems [library]
ND_unique_types [library]
ND_sound [library]
ND_contr [library]
ND2check [lemma, in Prfx.check_sound]
Nil [abbreviation, in Prfx.list]
niln [constructor, in Prfx.list]
nohyp_inv [lemma, in Prfx.inv_lems]
not_free_lift_frm [lemma, in Prfx.lift_lems]
not_free_lift_trms [lemma, in Prfx.lift_lems]
not_free_lift_trm [lemma, in Prfx.lift_lems]
not_free_lift [lemma, in Prfx.lift_lems]
O
objects [section, in Prfx.objects]objects [library]
objects.boolpreds [section, in Prfx.objects]
objects.ip1 [section, in Prfx.objects]
objects.ip1.h [variable, in Prfx.objects]
objects.ip1.h0 [variable, in Prfx.objects]
objects.ip1.h1 [variable, in Prfx.objects]
objects.ip1.h2 [variable, in Prfx.objects]
objects.ip1.P [variable, in Prfx.objects]
objects.ip1.P0 [variable, in Prfx.objects]
objects.ip2 [section, in Prfx.objects]
objects.ip2.h [variable, in Prfx.objects]
objects.ip2.h0 [variable, in Prfx.objects]
objects.ip2.h1 [variable, in Prfx.objects]
objects.ip2.h2 [variable, in Prfx.objects]
objects.ip2.P [variable, in Prfx.objects]
objects.ip2.P0 [variable, in Prfx.objects]
objects.l1 [variable, in Prfx.objects]
objects.l2 [variable, in Prfx.objects]
objects.map_hyp_sec.g [variable, in Prfx.objects]
objects.map_hyp_sec [section, in Prfx.objects]
objects.map_var_sec.g [variable, in Prfx.objects]
objects.map_var_sec [section, in Prfx.objects]
objects.map_trm_sec.g [variable, in Prfx.objects]
objects.map_trm_sec [section, in Prfx.objects]
opt [inductive, in Prfx.list]
opt_nth [definition, in Prfx.list]
P
pcd_exq [constructor, in Prfx.red]pcd_uvq [constructor, in Prfx.red]
pcd_dsj [constructor, in Prfx.red]
pcd_cnj2 [constructor, in Prfx.red]
pcd_cnj1 [constructor, in Prfx.red]
pcd_imp [constructor, in Prfx.red]
pcd_bot [constructor, in Prfx.red]
pce_exq [constructor, in Prfx.red]
pce_uvq [constructor, in Prfx.red]
pce_dsj [constructor, in Prfx.red]
pce_cnj2 [constructor, in Prfx.red]
pce_cnj1 [constructor, in Prfx.red]
pce_imp [constructor, in Prfx.red]
pce_bot [constructor, in Prfx.red]
permute_lift_cxt [lemma, in Prfx.lift_lems]
permute_lift_frm [lemma, in Prfx.lift_lems]
permute_lift_trms [lemma, in Prfx.lift_lems]
permute_lift_trm [lemma, in Prfx.lift_lems]
permute_lift_var [lemma, in Prfx.lift_lems]
piffp [definition, in Prfx.eval_lift_lems]
plusO [lemma, in Prfx.lift_lems]
preliminaries [section, in Prfx.list]
preliminaries.A [variable, in Prfx.list]
prf [inductive, in Prfx.objects]
prfx [library]
proj [definition, in Prfx.lift]
projTS1 [definition, in Prfx.indices]
projTS2 [definition, in Prfx.indices]
proj_frm [definition, in Prfx.lift]
proj_trms [definition, in Prfx.lift]
proj_trm [definition, in Prfx.lift]
proj_lift_frm_simpl [lemma, in Prfx.lift_lems]
proj_lift_trms_simpl [lemma, in Prfx.lift_lems]
proj_lift_trm_simpl [lemma, in Prfx.lift_lems]
proj_lift_simpl [lemma, in Prfx.lift_lems]
Proj1 [abbreviation, in Prfx.list]
Proj2 [abbreviation, in Prfx.list]
pr_exq [constructor, in Prfx.red]
pr_uvq [constructor, in Prfx.red]
pr_dsj2 [constructor, in Prfx.red]
pr_dsj1 [constructor, in Prfx.red]
pr_cnj2 [constructor, in Prfx.red]
pr_cnj1 [constructor, in Prfx.red]
pr_imp [constructor, in Prfx.red]
R
red [inductive, in Prfx.red]red [library]
reduction [section, in Prfx.red]
reduction.F [variable, in Prfx.red]
reduction.l1 [variable, in Prfx.red]
reduction.l2 [variable, in Prfx.red]
reduction.P [variable, in Prfx.red]
reduction.T [variable, in Prfx.red]
_ --> _ [notation, in Prfx.red]
_ |--> _ [notation, in Prfx.red]
red_exq_elim_2 [constructor, in Prfx.red]
red_exq_elim_1 [constructor, in Prfx.red]
red_exq_intro [constructor, in Prfx.red]
red_uvq_elim [constructor, in Prfx.red]
red_uvq_intro [constructor, in Prfx.red]
red_dsj_elim_3 [constructor, in Prfx.red]
red_dsj_elim_2 [constructor, in Prfx.red]
red_dsj_elim_1 [constructor, in Prfx.red]
red_dsj_intro2 [constructor, in Prfx.red]
red_dsj_intro1 [constructor, in Prfx.red]
red_cnj_elim2 [constructor, in Prfx.red]
red_cnj_elim1 [constructor, in Prfx.red]
red_cnj_intro_2 [constructor, in Prfx.red]
red_cnj_intro_1 [constructor, in Prfx.red]
red_imp_elim_2 [constructor, in Prfx.red]
red_imp_elim_1 [constructor, in Prfx.red]
red_imp_intro [constructor, in Prfx.red]
red_bot_elim [constructor, in Prfx.red]
red_imm_red [constructor, in Prfx.red]
rel [constructor, in Prfx.objects]
rel_piT [definition, in Prfx.eval]
rewr_cxt [definition, in Prfx.ND_lift_lems]
rewr_prf [definition, in Prfx.ND_lift_lems]
S
select [abbreviation, in Prfx.indices]select_expl [definition, in Prfx.indices]
shiftVAR [definition, in Prfx.lift]
shiftVAR_lift_trms_O [lemma, in Prfx.eval_lift_lems]
shiftVAR_lift_trm_O [lemma, in Prfx.eval_lift_lems]
Sigma_Type_Set.P [variable, in Prfx.indices]
Sigma_Type_Set.T [variable, in Prfx.indices]
Sigma_Type_Set [section, in Prfx.indices]
sigTS [inductive, in Prfx.indices]
simpl_subst_frm [lemma, in Prfx.subst_lems]
simpl_subst_trms [lemma, in Prfx.subst_lems]
simpl_subst_trm [lemma, in Prfx.subst_lems]
simpl_subst_var [lemma, in Prfx.subst_lems]
soundcheck [section, in Prfx.check_sound]
soundcheck.F [variable, in Prfx.check_sound]
soundcheck.l1 [variable, in Prfx.check_sound]
soundcheck.l2 [variable, in Prfx.check_sound]
soundcheck.P [variable, in Prfx.check_sound]
soundcheck.T [variable, in Prfx.check_sound]
soundcheck.Ts [variable, in Prfx.check_sound]
Soundness_of_ND.Ecxt [variable, in Prfx.ND_sound]
Soundness_of_ND.Etrm [variable, in Prfx.ND_sound]
Soundness_of_ND.E [variable, in Prfx.ND_sound]
Soundness_of_ND.Ts [variable, in Prfx.ND_sound]
Soundness_of_ND.T [variable, in Prfx.ND_sound]
Soundness_of_ND.F [variable, in Prfx.ND_sound]
Soundness_of_ND.P [variable, in Prfx.ND_sound]
Soundness_of_ND.REL [variable, in Prfx.ND_sound]
Soundness_of_ND.FUN [variable, in Prfx.ND_sound]
Soundness_of_ND.l2 [variable, in Prfx.ND_sound]
Soundness_of_ND.l1 [variable, in Prfx.ND_sound]
Soundness_of_ND.A [variable, in Prfx.ND_sound]
Soundness_of_ND [section, in Prfx.ND_sound]
SR [lemma, in Prfx.subj_red]
SR_imm_red [lemma, in Prfx.subj_red]
subject_reduction.T [variable, in Prfx.subj_red]
subject_reduction.C [variable, in Prfx.subj_red]
subject_reduction.F [variable, in Prfx.subj_red]
subject_reduction.P [variable, in Prfx.subj_red]
subject_reduction.l2 [variable, in Prfx.subj_red]
subject_reduction.l1 [variable, in Prfx.subj_red]
subject_reduction [section, in Prfx.subj_red]
subj_red [library]
subst [library]
substitution [section, in Prfx.subst]
substitution_lemmas.v [variable, in Prfx.subst_lems]
substitution_lemmas.C [variable, in Prfx.subst_lems]
substitution_lemmas.Ts [variable, in Prfx.subst_lems]
substitution_lemmas.T [variable, in Prfx.subst_lems]
substitution_lemmas.F [variable, in Prfx.subst_lems]
substitution_lemmas.P [variable, in Prfx.subst_lems]
substitution_lemmas.l2 [variable, in Prfx.subst_lems]
substitution_lemmas.l1 [variable, in Prfx.subst_lems]
substitution_lemmas [section, in Prfx.subst_lems]
substitution.C [variable, in Prfx.subst]
substitution.F [variable, in Prfx.subst]
substitution.hyp_substitution [section, in Prfx.subst]
substitution.l1 [variable, in Prfx.subst]
substitution.l2 [variable, in Prfx.subst]
substitution.P [variable, in Prfx.subst]
substitution.T [variable, in Prfx.subst]
substitution.Ts [variable, in Prfx.subst]
substitution.var_substitution [section, in Prfx.subst]
substO_hyp_prf_ok [lemma, in Prfx.ND_subst_lems]
substO_var_prf_ok [lemma, in Prfx.ND_subst_lems]
subst_frm_id [lemma, in Prfx.subst_lems]
subst_trms_id [lemma, in Prfx.subst_lems]
subst_trm_id [lemma, in Prfx.subst_lems]
subst_var_id [lemma, in Prfx.subst_lems]
subst_hyp_prf [definition, in Prfx.subst]
subst_hyp [definition, in Prfx.subst]
subst_var_prf [definition, in Prfx.subst]
subst_cxt [definition, in Prfx.subst]
subst_frm [definition, in Prfx.subst]
subst_trms [definition, in Prfx.subst]
subst_trm [definition, in Prfx.subst]
subst_var [definition, in Prfx.subst]
subst_hyp_prf_ok [lemma, in Prfx.ND_subst_lems]
subst_hyp_ok [lemma, in Prfx.ND_subst_lems]
subst_var_prf_ok [lemma, in Prfx.ND_subst_lems]
subst_var_hyp_ok [lemma, in Prfx.ND_subst_lems]
subst_lems [library]
T
thinning_eval_cxt_O [lemma, in Prfx.eval_lift_lems]thinning_eval_frm2 [lemma, in Prfx.eval_lift_lems]
thinning_eval_frm1 [lemma, in Prfx.eval_lift_lems]
thinning_eval_frm [lemma, in Prfx.eval_lift_lems]
thinning_eval_trms [lemma, in Prfx.eval_lift_lems]
thinning_eval_trm [lemma, in Prfx.eval_lift_lems]
thinning_eval_var [lemma, in Prfx.eval_lift_lems]
Top [abbreviation, in Prfx.objects]
top [constructor, in Prfx.objects]
Top_intro [abbreviation, in Prfx.objects]
top_intro [constructor, in Prfx.objects]
top_inv [lemma, in Prfx.inv_lems]
trm [inductive, in Prfx.objects]
trms [definition, in Prfx.objects]
trms_eqb_dec [lemma, in Prfx.check_sound]
trms_eqb_refl [lemma, in Prfx.check_sound]
trms_eqb [definition, in Prfx.objects]
trm_eqb_dec [lemma, in Prfx.check_sound]
trm_eqb_refl [lemma, in Prfx.check_sound]
trm_eqb [definition, in Prfx.objects]
trm_ind [definition, in Prfx.objects]
trm_ind' [definition, in Prfx.objects]
U
uniqueness_of_types.T [variable, in Prfx.ND_unique_types]uniqueness_of_types.F [variable, in Prfx.ND_unique_types]
uniqueness_of_types.P [variable, in Prfx.ND_unique_types]
uniqueness_of_types.l2 [variable, in Prfx.ND_unique_types]
uniqueness_of_types.l1 [variable, in Prfx.ND_unique_types]
uniqueness_of_types [section, in Prfx.ND_unique_types]
unique_types [lemma, in Prfx.ND_unique_types]
uvq [constructor, in Prfx.objects]
uvq_elim [constructor, in Prfx.objects]
uvq_intro [constructor, in Prfx.objects]
uvq_elim_inv [lemma, in Prfx.inv_lems]
uvq_intro_inv [lemma, in Prfx.inv_lems]
V
val [constructor, in Prfx.list]Var [abbreviation, in Prfx.objects]
var [constructor, in Prfx.objects]
VARexteq_eval_frm [lemma, in Prfx.eval_lift_lems]
VARexteq_eval_trms [lemma, in Prfx.eval_lift_lems]
VARexteq_eval_trm [lemma, in Prfx.eval_lift_lems]
other
_ }- _ [notation, in Prfx.indices]Notation Index
R
_ --> _ [in Prfx.red]_ |--> _ [in Prfx.red]
other
_ }- _ [in Prfx.indices]Variable Index
C
checksec.F [in Prfx.check]checksec.l1 [in Prfx.check]
checksec.l2 [in Prfx.check]
checksec.P [in Prfx.check]
checksec.T [in Prfx.check]
checksec.Ts [in Prfx.check]
contr_prf.P [in Prfx.contr]
contr_prf.l2 [in Prfx.contr]
contr_prf.l1 [in Prfx.contr]
E
evaluation.A [in Prfx.eval]evaluation.F [in Prfx.eval]
evaluation.formula_evaluation.dflt [in Prfx.eval]
evaluation.formula_evaluation.REL [in Prfx.eval]
evaluation.FUN [in Prfx.eval]
evaluation.l1 [in Prfx.eval]
evaluation.l2 [in Prfx.eval]
evaluation.P [in Prfx.eval]
evaluation.T [in Prfx.eval]
evaluation.term_evaluation.VAR [in Prfx.eval]
evaluation.Ts [in Prfx.eval]
eval_lift_lemmas.Ecxt [in Prfx.eval_lift_lems]
eval_lift_lemmas.Etrm [in Prfx.eval_lift_lems]
eval_lift_lemmas.E [in Prfx.eval_lift_lems]
eval_lift_lemmas.C [in Prfx.eval_lift_lems]
eval_lift_lemmas.Ts [in Prfx.eval_lift_lems]
eval_lift_lemmas.T [in Prfx.eval_lift_lems]
eval_lift_lemmas.F [in Prfx.eval_lift_lems]
eval_lift_lemmas.P [in Prfx.eval_lift_lems]
eval_lift_lemmas.REL [in Prfx.eval_lift_lems]
eval_lift_lemmas.FUN [in Prfx.eval_lift_lems]
eval_lift_lemmas.l2 [in Prfx.eval_lift_lems]
eval_lift_lemmas.l1 [in Prfx.eval_lift_lems]
eval_lift_lemmas.A [in Prfx.eval_lift_lems]
eval_subst_lemmas.Ecxt [in Prfx.eval_subst_lems]
eval_subst_lemmas.Etrm [in Prfx.eval_subst_lems]
eval_subst_lemmas.E [in Prfx.eval_subst_lems]
eval_subst_lemmas.C [in Prfx.eval_subst_lems]
eval_subst_lemmas.Ts [in Prfx.eval_subst_lems]
eval_subst_lemmas.T [in Prfx.eval_subst_lems]
eval_subst_lemmas.F [in Prfx.eval_subst_lems]
eval_subst_lemmas.P [in Prfx.eval_subst_lems]
eval_subst_lemmas.REL [in Prfx.eval_subst_lems]
eval_subst_lemmas.FUN [in Prfx.eval_subst_lems]
eval_subst_lemmas.l2 [in Prfx.eval_subst_lems]
eval_subst_lemmas.l1 [in Prfx.eval_subst_lems]
eval_subst_lemmas.A [in Prfx.eval_subst_lems]
exch_prf.P [in Prfx.exch]
exch_prf.l2 [in Prfx.exch]
exch_prf.l1 [in Prfx.exch]
I
indices.A [in Prfx.indices]indices.index_L.len [in Prfx.indices]
indices.index_L.L [in Prfx.indices]
Inversion_Lemmata.C [in Prfx.inv_lems]
Inversion_Lemmata.Ts [in Prfx.inv_lems]
Inversion_Lemmata.T [in Prfx.inv_lems]
Inversion_Lemmata.F [in Prfx.inv_lems]
Inversion_Lemmata.P [in Prfx.inv_lems]
Inversion_Lemmata.l2 [in Prfx.inv_lems]
Inversion_Lemmata.l1 [in Prfx.inv_lems]
L
lifting_lemmas.C [in Prfx.lift_lems]lifting_lemmas.Ts [in Prfx.lift_lems]
lifting_lemmas.T [in Prfx.lift_lems]
lifting_lemmas.F [in Prfx.lift_lems]
lifting_lemmas.P [in Prfx.lift_lems]
lifting_lemmas.l2 [in Prfx.lift_lems]
lifting_lemmas.l1 [in Prfx.lift_lems]
lifting.A [in Prfx.lift]
lifting.F [in Prfx.lift]
lifting.l1 [in Prfx.lift]
lifting.l2 [in Prfx.lift]
lifting.P [in Prfx.lift]
lifting.T [in Prfx.lift]
lifting.Ts [in Prfx.lift]
listns.A [in Prfx.list]
listns.A_eqb_dec [in Prfx.list]
listns.A_eqb_refl [in Prfx.list]
listns.A_eqb [in Prfx.list]
M
mapns.A [in Prfx.list]mapns.B [in Prfx.list]
mapns.f [in Prfx.list]
mapns.p [in Prfx.list]
more_on_lists.f2 [in Prfx.list]
more_on_lists.f1 [in Prfx.list]
more_on_lists.C [in Prfx.list]
more_on_lists.ee [in Prfx.list]
more_on_lists.g [in Prfx.list]
more_on_lists.f [in Prfx.list]
more_on_lists.B [in Prfx.list]
more_on_lists.A [in Prfx.list]
N
Natural_Deduction.P [in Prfx.ND]Natural_Deduction.C [in Prfx.ND]
Natural_Deduction.F [in Prfx.ND]
Natural_Deduction.T [in Prfx.ND]
Natural_Deduction.l2 [in Prfx.ND]
Natural_Deduction.l1 [in Prfx.ND]
ND_exchange_rule.P [in Prfx.ND_exch]
ND_exchange_rule.X [in Prfx.ND_exch]
ND_exchange_rule.F [in Prfx.ND_exch]
ND_exchange_rule.T [in Prfx.ND_exch]
ND_exchange_rule.l2 [in Prfx.ND_exch]
ND_exchange_rule.l1 [in Prfx.ND_exch]
ND_contraction_rule.P [in Prfx.ND_contr]
ND_contraction_rule.l2 [in Prfx.ND_contr]
ND_contraction_rule.l1 [in Prfx.ND_contr]
ND_lifting_lemmas.C [in Prfx.ND_lift_lems]
ND_lifting_lemmas.Ts [in Prfx.ND_lift_lems]
ND_lifting_lemmas.T [in Prfx.ND_lift_lems]
ND_lifting_lemmas.F [in Prfx.ND_lift_lems]
ND_lifting_lemmas.P [in Prfx.ND_lift_lems]
ND_lifting_lemmas.l2 [in Prfx.ND_lift_lems]
ND_lifting_lemmas.l1 [in Prfx.ND_lift_lems]
ND_substitution_lemmas.C [in Prfx.ND_subst_lems]
ND_substitution_lemmas.Ts [in Prfx.ND_subst_lems]
ND_substitution_lemmas.T [in Prfx.ND_subst_lems]
ND_substitution_lemmas.F [in Prfx.ND_subst_lems]
ND_substitution_lemmas.P [in Prfx.ND_subst_lems]
ND_substitution_lemmas.l2 [in Prfx.ND_subst_lems]
ND_substitution_lemmas.l1 [in Prfx.ND_subst_lems]
O
objects.ip1.h [in Prfx.objects]objects.ip1.h0 [in Prfx.objects]
objects.ip1.h1 [in Prfx.objects]
objects.ip1.h2 [in Prfx.objects]
objects.ip1.P [in Prfx.objects]
objects.ip1.P0 [in Prfx.objects]
objects.ip2.h [in Prfx.objects]
objects.ip2.h0 [in Prfx.objects]
objects.ip2.h1 [in Prfx.objects]
objects.ip2.h2 [in Prfx.objects]
objects.ip2.P [in Prfx.objects]
objects.ip2.P0 [in Prfx.objects]
objects.l1 [in Prfx.objects]
objects.l2 [in Prfx.objects]
objects.map_hyp_sec.g [in Prfx.objects]
objects.map_var_sec.g [in Prfx.objects]
objects.map_trm_sec.g [in Prfx.objects]
P
preliminaries.A [in Prfx.list]R
reduction.F [in Prfx.red]reduction.l1 [in Prfx.red]
reduction.l2 [in Prfx.red]
reduction.P [in Prfx.red]
reduction.T [in Prfx.red]
S
Sigma_Type_Set.P [in Prfx.indices]Sigma_Type_Set.T [in Prfx.indices]
soundcheck.F [in Prfx.check_sound]
soundcheck.l1 [in Prfx.check_sound]
soundcheck.l2 [in Prfx.check_sound]
soundcheck.P [in Prfx.check_sound]
soundcheck.T [in Prfx.check_sound]
soundcheck.Ts [in Prfx.check_sound]
Soundness_of_ND.Ecxt [in Prfx.ND_sound]
Soundness_of_ND.Etrm [in Prfx.ND_sound]
Soundness_of_ND.E [in Prfx.ND_sound]
Soundness_of_ND.Ts [in Prfx.ND_sound]
Soundness_of_ND.T [in Prfx.ND_sound]
Soundness_of_ND.F [in Prfx.ND_sound]
Soundness_of_ND.P [in Prfx.ND_sound]
Soundness_of_ND.REL [in Prfx.ND_sound]
Soundness_of_ND.FUN [in Prfx.ND_sound]
Soundness_of_ND.l2 [in Prfx.ND_sound]
Soundness_of_ND.l1 [in Prfx.ND_sound]
Soundness_of_ND.A [in Prfx.ND_sound]
subject_reduction.T [in Prfx.subj_red]
subject_reduction.C [in Prfx.subj_red]
subject_reduction.F [in Prfx.subj_red]
subject_reduction.P [in Prfx.subj_red]
subject_reduction.l2 [in Prfx.subj_red]
subject_reduction.l1 [in Prfx.subj_red]
substitution_lemmas.v [in Prfx.subst_lems]
substitution_lemmas.C [in Prfx.subst_lems]
substitution_lemmas.Ts [in Prfx.subst_lems]
substitution_lemmas.T [in Prfx.subst_lems]
substitution_lemmas.F [in Prfx.subst_lems]
substitution_lemmas.P [in Prfx.subst_lems]
substitution_lemmas.l2 [in Prfx.subst_lems]
substitution_lemmas.l1 [in Prfx.subst_lems]
substitution.C [in Prfx.subst]
substitution.F [in Prfx.subst]
substitution.l1 [in Prfx.subst]
substitution.l2 [in Prfx.subst]
substitution.P [in Prfx.subst]
substitution.T [in Prfx.subst]
substitution.Ts [in Prfx.subst]
U
uniqueness_of_types.T [in Prfx.ND_unique_types]uniqueness_of_types.F [in Prfx.ND_unique_types]
uniqueness_of_types.P [in Prfx.ND_unique_types]
uniqueness_of_types.l2 [in Prfx.ND_unique_types]
uniqueness_of_types.l1 [in Prfx.ND_unique_types]
Library Index
C
checkcheck_sound
contr
E
evaleval_subst_lems
eval_lift_lems
exch
I
indicesinv_lems
L
liftlift_lems
list
N
nat_eqbND
ND_exch
ND_lift_lems
ND_subst_lems
ND_unique_types
ND_sound
ND_contr
O
objectsP
prfxR
redS
subj_redsubst
subst_lems
Lemma Index
A
andb_intro [in Prfx.check_sound]B
bot_inv [in Prfx.inv_lems]C
check2ND [in Prfx.check_sound]cnj_elim2_inv [in Prfx.inv_lems]
cnj_elim1_inv [in Prfx.inv_lems]
cnj_intro_inv [in Prfx.inv_lems]
commute_lift_subst_cxt [in Prfx.subst_lems]
commute_lift_subst_frm [in Prfx.subst_lems]
commute_lift_subst_trms [in Prfx.subst_lems]
commute_lift_subst_trm [in Prfx.subst_lems]
commute_lift_subst_var [in Prfx.subst_lems]
D
distr_lift_substO_frm [in Prfx.lift_lems]distr_lift_subst_frm [in Prfx.lift_lems]
distr_lift_subst_trms [in Prfx.lift_lems]
distr_lift_subst_trm [in Prfx.lift_lems]
distr_lift_subst_var [in Prfx.lift_lems]
distr_subst_frm [in Prfx.subst_lems]
distr_subst_trms [in Prfx.subst_lems]
distr_subst_trm [in Prfx.subst_lems]
distr_subst_var [in Prfx.subst_lems]
dsj_elim_inv [in Prfx.inv_lems]
dsj_intro2_inv [in Prfx.inv_lems]
dsj_intro1_inv [in Prfx.inv_lems]
E
eq_consn [in Prfx.list]eq_dep_consn [in Prfx.list]
eq_niln [in Prfx.list]
eq_dep_niln [in Prfx.list]
eval_subst_frm_ok2 [in Prfx.eval_subst_lems]
eval_subst_frm_ok1 [in Prfx.eval_subst_lems]
eval_subst_frm_ok [in Prfx.eval_subst_lems]
eval_subst_trms_ok [in Prfx.eval_subst_lems]
eval_subst_trm_ok [in Prfx.eval_subst_lems]
eval_subst_var_ok [in Prfx.eval_subst_lems]
exch_ok3 [in Prfx.exch]
exch_ok2 [in Prfx.exch]
exch_ok1 [in Prfx.exch]
exq_elim_inv [in Prfx.inv_lems]
exq_intro_inv [in Prfx.inv_lems]
F
frm_eqb_dec [in Prfx.check_sound]frm_eqb_refl [in Prfx.check_sound]
H
hypO_inv [in Prfx.inv_lems]hypS_inv [in Prfx.inv_lems]
I
imp_elim_inv [in Prfx.inv_lems]imp_intro_inv [in Prfx.inv_lems]
index_eqb_dec [in Prfx.indices]
index_eqb_refl [in Prfx.indices]
insVARswap [in Prfx.eval_lift_lems]
insVAR_shift [in Prfx.eval_lift_lems]
L
length_map [in Prfx.list]lift_proj_frm_simpl [in Prfx.lift_lems]
lift_proj_trms_simpl [in Prfx.lift_lems]
lift_proj_trm_simpl [in Prfx.lift_lems]
lift_proj_simpl [in Prfx.lift_lems]
listn_eqb_dec [in Prfx.list]
listn_eqb_refl [in Prfx.list]
ltll_dec_opaque [in Prfx.indices]
M
mapnb_orb_false [in Prfx.list]mapn_id [in Prfx.list]
mapn_mapn [in Prfx.list]
mapn_inn [in Prfx.list]
mapn_feeg [in Prfx.list]
map_map [in Prfx.list]
map_feeg [in Prfx.list]
map_app [in Prfx.list]
N
nat_eqb_refl [in Prfx.nat_eqb]nat_eqb_dec [in Prfx.nat_eqb]
ND_hyp_nth [in Prfx.check_sound]
ND_exch [in Prfx.ND_exch]
ND_exch_hyp [in Prfx.ND_exch]
ND_contr [in Prfx.ND_contr]
ND_contr_hyp [in Prfx.ND_contr]
ND_weakening [in Prfx.ND_lift_lems]
ND_weak_hyp [in Prfx.ND_lift_lems]
ND_lift_var [in Prfx.ND_lift_lems]
ND_sound [in Prfx.ND_sound]
ND2check [in Prfx.check_sound]
nohyp_inv [in Prfx.inv_lems]
not_free_lift_frm [in Prfx.lift_lems]
not_free_lift_trms [in Prfx.lift_lems]
not_free_lift_trm [in Prfx.lift_lems]
not_free_lift [in Prfx.lift_lems]
P
permute_lift_cxt [in Prfx.lift_lems]permute_lift_frm [in Prfx.lift_lems]
permute_lift_trms [in Prfx.lift_lems]
permute_lift_trm [in Prfx.lift_lems]
permute_lift_var [in Prfx.lift_lems]
plusO [in Prfx.lift_lems]
proj_lift_frm_simpl [in Prfx.lift_lems]
proj_lift_trms_simpl [in Prfx.lift_lems]
proj_lift_trm_simpl [in Prfx.lift_lems]
proj_lift_simpl [in Prfx.lift_lems]
S
shiftVAR_lift_trms_O [in Prfx.eval_lift_lems]shiftVAR_lift_trm_O [in Prfx.eval_lift_lems]
simpl_subst_frm [in Prfx.subst_lems]
simpl_subst_trms [in Prfx.subst_lems]
simpl_subst_trm [in Prfx.subst_lems]
simpl_subst_var [in Prfx.subst_lems]
SR [in Prfx.subj_red]
SR_imm_red [in Prfx.subj_red]
substO_hyp_prf_ok [in Prfx.ND_subst_lems]
substO_var_prf_ok [in Prfx.ND_subst_lems]
subst_frm_id [in Prfx.subst_lems]
subst_trms_id [in Prfx.subst_lems]
subst_trm_id [in Prfx.subst_lems]
subst_var_id [in Prfx.subst_lems]
subst_hyp_prf_ok [in Prfx.ND_subst_lems]
subst_hyp_ok [in Prfx.ND_subst_lems]
subst_var_prf_ok [in Prfx.ND_subst_lems]
subst_var_hyp_ok [in Prfx.ND_subst_lems]
T
thinning_eval_cxt_O [in Prfx.eval_lift_lems]thinning_eval_frm2 [in Prfx.eval_lift_lems]
thinning_eval_frm1 [in Prfx.eval_lift_lems]
thinning_eval_frm [in Prfx.eval_lift_lems]
thinning_eval_trms [in Prfx.eval_lift_lems]
thinning_eval_trm [in Prfx.eval_lift_lems]
thinning_eval_var [in Prfx.eval_lift_lems]
top_inv [in Prfx.inv_lems]
trms_eqb_dec [in Prfx.check_sound]
trms_eqb_refl [in Prfx.check_sound]
trm_eqb_dec [in Prfx.check_sound]
trm_eqb_refl [in Prfx.check_sound]
U
unique_types [in Prfx.ND_unique_types]uvq_elim_inv [in Prfx.inv_lems]
uvq_intro_inv [in Prfx.inv_lems]
V
VARexteq_eval_frm [in Prfx.eval_lift_lems]VARexteq_eval_trms [in Prfx.eval_lift_lems]
VARexteq_eval_trm [in Prfx.eval_lift_lems]
Constructor Index
B
bot [in Prfx.objects]bot_elim [in Prfx.objects]
C
cnj [in Prfx.objects]cnj_elim2 [in Prfx.objects]
cnj_elim1 [in Prfx.objects]
cnj_intro [in Prfx.objects]
consn [in Prfx.list]
D
dsj [in Prfx.objects]dsj_elim [in Prfx.objects]
dsj_intro2 [in Prfx.objects]
dsj_intro1 [in Prfx.objects]
E
err [in Prfx.list]existTS [in Prfx.indices]
exq [in Prfx.objects]
exq_elim [in Prfx.objects]
exq_intro [in Prfx.objects]
F
fun_ [in Prfx.objects]H
hyp [in Prfx.objects]I
imp [in Prfx.objects]imp_elim [in Prfx.objects]
imp_intro [in Prfx.objects]
N
ND_exq_elim [in Prfx.ND]ND_exq_intro [in Prfx.ND]
ND_uvq_elim [in Prfx.ND]
ND_uvq_intro [in Prfx.ND]
ND_dsj_elim [in Prfx.ND]
ND_dsj_intro2 [in Prfx.ND]
ND_dsj_intro1 [in Prfx.ND]
ND_cnj_elim2 [in Prfx.ND]
ND_cnj_elim1 [in Prfx.ND]
ND_cnj_intro [in Prfx.ND]
ND_imp_elim [in Prfx.ND]
ND_imp_intro [in Prfx.ND]
ND_bot_elim [in Prfx.ND]
ND_hypS [in Prfx.ND]
ND_hypO [in Prfx.ND]
ND_top_intro [in Prfx.ND]
niln [in Prfx.list]
P
pcd_exq [in Prfx.red]pcd_uvq [in Prfx.red]
pcd_dsj [in Prfx.red]
pcd_cnj2 [in Prfx.red]
pcd_cnj1 [in Prfx.red]
pcd_imp [in Prfx.red]
pcd_bot [in Prfx.red]
pce_exq [in Prfx.red]
pce_uvq [in Prfx.red]
pce_dsj [in Prfx.red]
pce_cnj2 [in Prfx.red]
pce_cnj1 [in Prfx.red]
pce_imp [in Prfx.red]
pce_bot [in Prfx.red]
pr_exq [in Prfx.red]
pr_uvq [in Prfx.red]
pr_dsj2 [in Prfx.red]
pr_dsj1 [in Prfx.red]
pr_cnj2 [in Prfx.red]
pr_cnj1 [in Prfx.red]
pr_imp [in Prfx.red]
R
red_exq_elim_2 [in Prfx.red]red_exq_elim_1 [in Prfx.red]
red_exq_intro [in Prfx.red]
red_uvq_elim [in Prfx.red]
red_uvq_intro [in Prfx.red]
red_dsj_elim_3 [in Prfx.red]
red_dsj_elim_2 [in Prfx.red]
red_dsj_elim_1 [in Prfx.red]
red_dsj_intro2 [in Prfx.red]
red_dsj_intro1 [in Prfx.red]
red_cnj_elim2 [in Prfx.red]
red_cnj_elim1 [in Prfx.red]
red_cnj_intro_2 [in Prfx.red]
red_cnj_intro_1 [in Prfx.red]
red_imp_elim_2 [in Prfx.red]
red_imp_elim_1 [in Prfx.red]
red_imp_intro [in Prfx.red]
red_bot_elim [in Prfx.red]
red_imm_red [in Prfx.red]
rel [in Prfx.objects]
T
top [in Prfx.objects]top_intro [in Prfx.objects]
U
uvq [in Prfx.objects]uvq_elim [in Prfx.objects]
uvq_intro [in Prfx.objects]
V
val [in Prfx.list]var [in Prfx.objects]
Inductive Index
E
empty [in Prfx.indices]F
frm [in Prfx.objects]I
imm_red [in Prfx.red]L
listn [in Prfx.list]N
ND [in Prfx.ND]O
opt [in Prfx.list]P
prf [in Prfx.objects]R
red [in Prfx.red]S
sigTS [in Prfx.indices]T
trm [in Prfx.objects]Section Index
C
checksec [in Prfx.check]contr_prf [in Prfx.contr]
E
evaluation [in Prfx.eval]evaluation.formula_evaluation [in Prfx.eval]
evaluation.term_evaluation [in Prfx.eval]
eval_lift_lemmas [in Prfx.eval_lift_lems]
eval_subst_lemmas [in Prfx.eval_subst_lems]
exch_prf [in Prfx.exch]
I
indices [in Prfx.indices]indices.index_L [in Prfx.indices]
Inversion_Lemmata [in Prfx.inv_lems]
L
lifting [in Prfx.lift]lifting_lemmas [in Prfx.lift_lems]
listns [in Prfx.list]
M
mapns [in Prfx.list]more_on_lists [in Prfx.list]
N
Natural_Deduction [in Prfx.ND]ND_exchange_rule [in Prfx.ND_exch]
ND_contraction_rule [in Prfx.ND_contr]
ND_lifting_lemmas [in Prfx.ND_lift_lems]
ND_substitution_lemmas [in Prfx.ND_subst_lems]
O
objects [in Prfx.objects]objects.boolpreds [in Prfx.objects]
objects.ip1 [in Prfx.objects]
objects.ip2 [in Prfx.objects]
objects.map_hyp_sec [in Prfx.objects]
objects.map_var_sec [in Prfx.objects]
objects.map_trm_sec [in Prfx.objects]
P
preliminaries [in Prfx.list]R
reduction [in Prfx.red]S
Sigma_Type_Set [in Prfx.indices]soundcheck [in Prfx.check_sound]
Soundness_of_ND [in Prfx.ND_sound]
subject_reduction [in Prfx.subj_red]
substitution [in Prfx.subst]
substitution_lemmas [in Prfx.subst_lems]
substitution.hyp_substitution [in Prfx.subst]
substitution.var_substitution [in Prfx.subst]
U
uniqueness_of_types [in Prfx.ND_unique_types]Abbreviation Index
B
Bot [in Prfx.objects]C
Conj [in Prfx.list]E
Err [in Prfx.list]H
Hyp [in Prfx.objects]N
Nil [in Prfx.list]P
Proj1 [in Prfx.list]Proj2 [in Prfx.list]
S
select [in Prfx.indices]T
Top [in Prfx.objects]Top_intro [in Prfx.objects]
V
Var [in Prfx.objects]Definition Index
C
check [in Prfx.check]contr [in Prfx.contr]
contr_hyp [in Prfx.contr]
E
emp [in Prfx.objects]empty_ind' [in Prfx.indices]
eval_cxt [in Prfx.eval]
eval_frm [in Prfx.eval]
eval_cxt' [in Prfx.eval]
eval_frm' [in Prfx.eval]
eval_trms [in Prfx.eval]
eval_trm [in Prfx.eval]
exch [in Prfx.exch]
exch_hyp [in Prfx.exch]
F
free_inb_frm [in Prfx.objects]free_inb_trms [in Prfx.objects]
free_inb_trm [in Prfx.objects]
frm_eqb [in Prfx.objects]
from_empty [in Prfx.indices]
fun_piT [in Prfx.eval]
I
index [in Prfx.indices]index_inj [in Prfx.indices]
index_eqb [in Prfx.indices]
index2nat [in Prfx.indices]
inn [in Prfx.list]
insertVAR [in Prfx.eval]
insertVAR_O [in Prfx.eval]
L
lift [in Prfx.lift]lift_hyp_prf [in Prfx.lift]
lift_var_prf [in Prfx.lift]
lift_cxt [in Prfx.lift]
lift_frm [in Prfx.lift]
lift_trms [in Prfx.lift]
lift_trm [in Prfx.lift]
listn_eqb [in Prfx.list]
ltll [in Prfx.indices]
ltll_dec [in Prfx.indices]
M
mapn [in Prfx.list]mapnb [in Prfx.list]
mapn_andb [in Prfx.list]
mapn_orb [in Prfx.list]
map_prf_hyp [in Prfx.objects]
map_prf_var [in Prfx.objects]
map_frm_var [in Prfx.objects]
map_trm [in Prfx.objects]
N
nat_eqb [in Prfx.nat_eqb]nat_inj [in Prfx.indices]
nat2index [in Prfx.indices]
nat2index_sig [in Prfx.indices]
O
opt_nth [in Prfx.list]P
piffp [in Prfx.eval_lift_lems]proj [in Prfx.lift]
projTS1 [in Prfx.indices]
projTS2 [in Prfx.indices]
proj_frm [in Prfx.lift]
proj_trms [in Prfx.lift]
proj_trm [in Prfx.lift]
R
rel_piT [in Prfx.eval]rewr_cxt [in Prfx.ND_lift_lems]
rewr_prf [in Prfx.ND_lift_lems]
S
select_expl [in Prfx.indices]shiftVAR [in Prfx.lift]
subst_hyp_prf [in Prfx.subst]
subst_hyp [in Prfx.subst]
subst_var_prf [in Prfx.subst]
subst_cxt [in Prfx.subst]
subst_frm [in Prfx.subst]
subst_trms [in Prfx.subst]
subst_trm [in Prfx.subst]
subst_var [in Prfx.subst]
T
trms [in Prfx.objects]trms_eqb [in Prfx.objects]
trm_eqb [in Prfx.objects]
trm_ind [in Prfx.objects]
trm_ind' [in Prfx.objects]
| 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 | (563 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 | (3 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 | (187 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 | (26 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 | (127 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 | (86 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 | (10 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 | (39 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 | (11 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 | (74 entries) |