| 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 |
_ |
(673 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 |
_ |
(5 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 |
_ |
(478 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 |
_ |
(78 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 |
_ |
(18 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 |
_ |
(74 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 |
_ |
(20 entries) |
Global Index
A
abstraction [constructor, in PTS]
antivar [definition, in Terms]
app [constructor, in Terms]
appl [constructor, in PTSeq]
application [constructor, in PTS]
appright [definition, in Terms]
app_eq [constructor, in PTSeq]
app_injl [lemma, in Terms]
app_injr [lemma, in Terms]
app_wd [lemma, in Terms]
app_wdl [lemma, in Terms]
app_wdr [lemma, in Terms]
ax [constructor, in PTSeq]
axiom [axiom, in PTS]
axioms [constructor, in PTS]
B
beta [constructor, in PTSeq]
bot [definition, in Finite]
botsub [definition, in Subst]
botsub_liftsub [lemma, in Subst]
botsub_Sfun [lemma, in Subst]
botsub_up [lemma, in Subst]
C
CComp [definition, in Subst]
CComp_is_Comp [lemma, in Subst]
Church_Rosser [lemma, in CR]
Comp [definition, in Subvar]
comp [definition, in Finite]
Comp_is_comp [lemma, in Subvar]
concat [definition, in String]
cons [constructor, in String]
context [definition, in PTS]
Context_Conversion [lemma, in Meta]
Context_Strength [lemma, in Meta]
Context_Validity [lemma, in PTSeq]
Context_Validity [lemma, in PTS]
conv [inductive, in Conv]
conv [constructor, in PTSeq]
Conv [library]
conversion [constructor, in PTS]
conversion' [lemma, in SR]
conv_app [lemma, in Conv]
conv_appl [lemma, in Conv]
conv_appr [lemma, in Conv]
conv_botsub [lemma, in Conv]
conv_ctxt [definition, in PTS]
conv_ctxt_build [lemma, in PTS]
conv_ctxt_injl [lemma, in PTS]
conv_ctxt_injr [lemma, in PTS]
conv_ctxt_ref [lemma, in PTS]
conv_eq [constructor, in PTSeq]
conv_lda [lemma, in Conv]
conv_ldal [lemma, in Conv]
conv_ldar [lemma, in Conv]
conv_lda_injl [lemma, in CR]
conv_lda_injr [lemma, in CR]
conv_liftsub [lemma, in Conv]
conv_liftterm [lemma, in Conv]
conv_liftterm_inj [lemma, in CR]
conv_par_red1 [constructor, in Conv]
conv_pi [lemma, in Conv]
conv_pil [lemma, in Conv]
conv_pir [lemma, in Conv]
conv_pi_injl [lemma, in CR]
conv_pi_injr [lemma, in CR]
conv_Pi_srt [lemma, in String]
conv_Pi_srt' [lemma, in String]
conv_red [lemma, in Conv]
conv_red' [lemma, in Conv]
conv_ref [lemma, in Conv]
conv_srt_inj [lemma, in CR]
conv_sub [definition, in Conv]
conv_subbot [lemma, in Conv]
conv_subbotl [lemma, in Conv]
conv_subbotr [lemma, in Conv]
conv_subst [lemma, in Conv]
conv_substl [lemma, in Conv]
conv_substr [lemma, in Conv]
conv_subvar [lemma, in Conv]
conv_subvar_inj [lemma, in CR]
conv_sub_ref [lemma, in Conv]
conv_sym [constructor, in Conv]
conv_trans [constructor, in Conv]
conv_var_inj [lemma, in CR]
CR [library]
ctxt_eq [definition, in PTSeq]
ctxt_eq_ref [lemma, in PTSeq]
ctxt_eq_validl [lemma, in PTSeq]
ctxt_eq_validr [lemma, in PTSeq]
ctxt_strng [lemma, in String]
E
emp [constructor, in String]
Equation_Validity_l [lemma, in PTSeq]
Equation_Validity_r [lemma, in PTSeq]
equiv [inductive, in PTSeq]
equiv_cons [constructor, in PTSeq]
equiv_consl [lemma, in PTSeq]
equiv_ref [constructor, in PTSeq]
equiv_sym [lemma, in PTSeq]
equiv_trans [lemma, in PTSeq]
equiv_weak [lemma, in PTSeq]
F
fin [definition, in Finite]
Finite [library]
funceq [definition, in Finite]
funceq_ref [lemma, in Finite]
funceq_sym [lemma, in Finite]
funceq_trans [lemma, in Finite]
Functionality [lemma, in PTSeq]
Functionality_bot [lemma, in PTSeq]
func_ax [axiom, in UT]
func_rule [axiom, in UT]
G
Gen_abs [lemma, in PTSeq]
Gen_app [lemma, in PTSeq]
Gen_app [lemma, in Meta]
Gen_conv_lda [lemma, in CR]
Gen_conv_pi [lemma, in CR]
Gen_conv_srt [lemma, in CR]
Gen_conv_var [lemma, in CR]
Gen_lda [lemma, in Meta]
Gen_lda' [lemma, in Meta]
Gen_par_red1_app [lemma, in Conv]
Gen_par_red1_lda [lemma, in Conv]
Gen_par_red1_pi [lemma, in Conv]
Gen_par_red1_srt [lemma, in Conv]
Gen_par_red1_var [lemma, in Conv]
Gen_pi [lemma, in Meta]
Gen_pi' [lemma, in Meta]
Gen_product [lemma, in PTSeq]
Gen_red_lda [lemma, in Conv]
Gen_red_pi [lemma, in Conv]
Gen_red_srt [lemma, in Conv]
Gen_red_var [lemma, in Conv]
Gen_sort [lemma, in PTSeq]
Gen_srt [lemma, in Meta]
Gen_srt' [lemma, in Meta]
Gen_var [lemma, in PTSeq]
Gen_var [lemma, in Meta]
H
head [definition, in String]
head_wd [lemma, in String]
I
id [definition, in Finite]
injective [definition, in Finite]
L
l [constructor, in Labconv]
l [constructor, in Labconv]
labCComp [definition, in Labsubst]
labComp [definition, in Labsubvar]
labComp_is_comp [lemma, in Labsubvar]
Labconv [library]
Labctxt [library]
Labsubst [library]
Labsubvar [library]
Labterms [library]
lab_antivar [definition, in Labterms]
lab_app [constructor, in Labterms]
lab_appright [definition, in Labterms]
lab_app_injcod [lemma, in Labterms]
lab_app_injl [lemma, in Labterms]
lab_app_injr [lemma, in Labterms]
lab_app_wd [lemma, in Labterms]
lab_app_wdcod [lemma, in Labterms]
lab_app_wdl [lemma, in Labterms]
lab_app_wdr [lemma, in Labterms]
lab_botsub [definition, in Labsubst]
lab_botsub_liftsub [lemma, in Labsubst]
lab_botsub_liftterm [lemma, in Labsubst]
lab_botsub_Sfun [lemma, in Labsubst]
lab_botsub_up [lemma, in Labsubst]
lab_CComp_is_Comp [lemma, in Labsubst]
lab_conv [inductive, in Labconv]
lab_conv_par_red1 [constructor, in Labconv]
lab_conv_sym [constructor, in Labconv]
lab_conv_trans [constructor, in Labconv]
lab_ctxt [definition, in Labctxt]
lab_lda [constructor, in Labterms]
lab_lda_injl [lemma, in Labterms]
lab_lda_injr [lemma, in Labterms]
lab_lda_wd [lemma, in Labterms]
lab_lda_wdl [lemma, in Labterms]
lab_lda_wdr [lemma, in Labterms]
lab_left [definition, in Labterms]
lab_liftsub_CComp [lemma, in Labsubst]
lab_liftterm_subbot [lemma, in Labsubst]
lab_liftterm_subst [lemma, in Labsubst]
lab_liftterm_subst' [lemma, in Labsubst]
lab_par_red1 [inductive, in Labconv]
lab_par_red1_app [constructor, in Labconv]
lab_par_red1_beta [constructor, in Labconv]
lab_par_red1_lda [constructor, in Labconv]
lab_par_red1_pi [constructor, in Labconv]
lab_par_red1_ref [lemma, in Labconv]
lab_par_red1_srt [constructor, in Labconv]
lab_par_red1_var [constructor, in Labconv]
lab_pi [constructor, in Labterms]
lab_pi_injl [lemma, in Labterms]
lab_pi_injr [lemma, in Labterms]
lab_pi_wd [lemma, in Labterms]
lab_pi_wdl [lemma, in Labterms]
lab_pi_wdr [lemma, in Labterms]
lab_red [inductive, in Labconv]
lab_red_par_red1 [constructor, in Labconv]
lab_red_trans [constructor, in Labconv]
lab_right [definition, in Labterms]
lab_srt [constructor, in Labterms]
lab_srt_inj [lemma, in Labterms]
lab_srt_wd [lemma, in Labterms]
lab_subbot [definition, in Labsubst]
lab_subbot_liftterm [lemma, in Labsubst]
lab_subbot_subvar [lemma, in Labsubst]
lab_subctxt [definition, in Labctxt]
lab_subctxt_up [lemma, in Labctxt]
lab_subctxt_Weak [lemma, in Labctxt]
lab_subst [definition, in Labsubst]
lab_subst_ext [lemma, in Labsubst]
lab_subst_is_subvar [lemma, in Labsubst]
lab_subst_liftterm [lemma, in Labsubst]
lab_subst_liftterm_botsub [lemma, in Labsubst]
lab_subst_lm [lemma, in Labsubst]
lab_subst_subbot [lemma, in Labsubst]
lab_subst_subvar [lemma, in Labsubst]
lab_subvar [definition, in Labsubvar]
lab_subvar_app [lemma, in Labsubvar]
lab_subvar_ext [lemma, in Labsubvar]
lab_subvar_inj [lemma, in Labsubvar]
lab_subvar_lda [lemma, in Labsubvar]
lab_subvar_liftlabterm [lemma, in Labsubvar]
lab_subvar_lm [lemma, in Labsubvar]
lab_subvar_pi [lemma, in Labsubvar]
lab_subvar_srt [lemma, in Labsubvar]
lab_subvar_subbot [lemma, in Labsubst]
lab_subvar_subst [lemma, in Labsubst]
lab_subvar_var [lemma, in Labsubvar]
lab_term [inductive, in Labterms]
lab_triv_subst [lemma, in Labsubst]
lab_triv_subvar [lemma, in Labsubvar]
lab_typeof [definition, in Labctxt]
lab_var [constructor, in Labterms]
lab_var_inj [lemma, in Labterms]
lab_var_wd [lemma, in Labterms]
lambda [constructor, in PTSeq]
lambda_eq [constructor, in PTSeq]
Lda [definition, in String]
lda [constructor, in Terms]
lda_injl [lemma, in Terms]
lda_injr [lemma, in Terms]
Lda_subst [lemma, in String]
Lda_subvar [lemma, in String]
lda_wd [lemma, in Terms]
lda_wdl [lemma, in Terms]
lda_wdr [lemma, in Terms]
left [definition, in Terms]
Left_Hand_Reflexivity [lemma, in TPOSR]
liftlabsub [definition, in Labsubvar]
liftlabsub_comp [lemma, in Labsubvar]
liftlabsub_Comp [lemma, in Labsubvar]
liftlabsub_ext [lemma, in Labsubvar]
liftlabsub_id [lemma, in Labsubvar]
liftlabterm [definition, in Labsubvar]
liftlabterm_app [lemma, in Labsubvar]
liftlabterm_inj [lemma, in Labsubvar]
liftlabterm_lab_subvar [lemma, in Labsubvar]
liftlabterm_lab_subvar' [lemma, in Labsubvar]
liftlabterm_lda [lemma, in Labsubvar]
liftlabterm_liftlabterm [lemma, in Labsubvar]
liftlabterm_liftlabterm' [lemma, in Labsubvar]
liftlabterm_pi [lemma, in Labsubvar]
liftlabterm_srt [lemma, in Labsubvar]
liftlabterm_var [lemma, in Labsubvar]
liftstring [definition, in String]
liftsub [definition, in Subvar]
liftsub_CComp [lemma, in Subst]
liftsub_Comp [lemma, in Subvar]
liftsub_comp [lemma, in Subvar]
liftsub_ext [lemma, in Subvar]
liftsub_id [lemma, in Subvar]
liftterm [definition, in Subvar]
liftterm_app [lemma, in Subvar]
liftterm_inj [lemma, in Subvar]
liftterm_lda [lemma, in Subvar]
liftterm_liftterm [lemma, in Subvar]
liftterm_liftterm' [lemma, in Subvar]
liftterm_pi [lemma, in Subvar]
liftterm_srt [lemma, in Subvar]
liftterm_subbot [lemma, in Subst]
liftterm_subst [lemma, in Subst]
liftterm_subst' [lemma, in Subst]
liftterm_subvar [lemma, in Subvar]
liftterm_subvar' [lemma, in Subvar]
liftterm_var [lemma, in Subvar]
lt_eq_lt_lm [lemma, in String]
M
Meta [library]
mtch [inductive, in String]
mtchO [constructor, in String]
mtchS [constructor, in String]
mtch_leql [lemma, in String]
mtch_leqr [lemma, in String]
mtch_Sm_Sn [lemma, in String]
mtch_Sm_Sn' [lemma, in String]
mtch_Sm_Sn_inv [lemma, in String]
N
not_conv_pi_srt [lemma, in CR]
not_red_pi_srt [lemma, in Conv]
not_red_srt_pi [lemma, in Conv]
O
O [definition, in Labctxt]
option_disc [lemma, in Finite]
P
par_red1 [inductive, in Conv]
par_red1_app [constructor, in Conv]
par_red1_beta [constructor, in Conv]
par_red1_botsub [lemma, in Conv]
par_red1_ctxt [definition, in PTS]
par_red1_ctxt_build [lemma, in PTS]
par_red1_ctxt_injl [lemma, in PTS]
par_red1_ctxt_injr [lemma, in PTS]
par_red1_ctxt_ref [lemma, in PTS]
par_red1_dmnd [lemma, in CR]
par_red1_lda [constructor, in Conv]
par_red1_lda_injl [lemma, in Conv]
par_red1_lda_injr [lemma, in Conv]
par_red1_liftsub [lemma, in Conv]
par_red1_liftterm [lemma, in Conv]
par_red1_liftterm_inj [lemma, in Conv]
par_red1_liftterm_inv [lemma, in Conv]
par_red1_pi [constructor, in Conv]
par_red1_pi_injl [lemma, in Conv]
par_red1_pi_injr [lemma, in Conv]
par_red1_ref [lemma, in Conv]
par_red1_srt [constructor, in Conv]
par_red1_srt_inj [lemma, in Conv]
par_red1_sub [definition, in Conv]
par_red1_subbot [lemma, in Conv]
par_red1_subst [lemma, in Conv]
par_red1_subvar [lemma, in Conv]
par_red1_subvar_inj [lemma, in Conv]
par_red1_subvar_inv [lemma, in Conv]
par_red1_sub_ref [lemma, in Conv]
par_red1_var [constructor, in Conv]
par_red1_var_inj [lemma, in Conv]
pi [constructor, in Terms]
Pi [definition, in String]
pi_injl [lemma, in Terms]
pi_injr [lemma, in Terms]
Pi_subbot_srt [lemma, in String]
Pi_subst [lemma, in String]
Pi_subvar [lemma, in String]
Pi_subvar_inv [lemma, in String]
pi_wd [lemma, in Terms]
pi_wdl [lemma, in Terms]
pi_wdr [lemma, in Terms]
Predicate_Reduction [lemma, in SR]
pre_Context_Conversion [lemma, in PTSeq]
pre_Context_Reduction [lemma, in TPOSR]
pre_Context_Reduction' [lemma, in TPOSR]
pre_Functionality [lemma, in PTSeq]
pre_Functionality_bot [lemma, in PTSeq]
pre_Gen_abs [lemma, in PTSeq]
pre_Gen_app [lemma, in Meta]
pre_Gen_app [lemma, in PTSeq]
pre_Gen_lda [lemma, in Meta]
pre_Gen_par_red1_app [lemma, in Conv]
pre_Gen_par_red1_lda [lemma, in Conv]
pre_Gen_par_red1_pi [lemma, in Conv]
pre_Gen_par_red1_srt [lemma, in Conv]
pre_Gen_par_red1_var [lemma, in Conv]
pre_Gen_pi [lemma, in Meta]
pre_Gen_product [lemma, in PTSeq]
pre_Gen_red_lda [lemma, in Conv]
pre_Gen_red_pi [lemma, in Conv]
pre_Gen_red_srt [lemma, in Conv]
pre_Gen_red_var [lemma, in Conv]
pre_Gen_sort [lemma, in PTSeq]
pre_Gen_srt [lemma, in Meta]
pre_Gen_var [lemma, in PTSeq]
pre_Gen_var [lemma, in Meta]
pre_mtch_Sm_Sn' [lemma, in String]
pre_mtch_Sm_Sn_inv [lemma, in String]
pre_par_red1_subvar_inv [lemma, in Conv]
pre_PTSeq_Context_Conversion [lemma, in PTSeq]
pre_PTSeq_to_PTS [lemma, in PTSeq]
pre_PTS'_Context_Conversion [lemma, in PTSeq]
pre_red_subvar_inv [lemma, in Conv]
pre_Sigma_gen [lemma, in Strength]
pre_Sigma_typing [lemma, in Strength]
pre_Strengthening [lemma, in Strength]
pre_TPOSR_Context_Conversion [lemma, in TPOSR]
pre_TPOSR_conv [lemma, in TPOSR]
pre_TPOSR_red_ctxt [definition, in TPOSR]
pre_TPOSR_red_ctxt_ref [lemma, in TPOSR]
pre_TPOSR_red_ctxt_TPOSR_ref [lemma, in TPOSR]
pre_TPOSR_red_ctxt_valid_r [lemma, in TPOSR]
pre_TPOSR_red_ctxt_valid_ref [lemma, in TPOSR]
pre_TPOSR_red_ctxt_xr [lemma, in TPOSR]
pre_TPOSR_to_PTSeq [lemma, in TPOSR]
pre_unlab_par_red1' [lemma, in Labconv]
pre_unlab_red' [lemma, in Labconv]
pre_Weak_satisfy_eq [lemma, in PTSeq]
prod [constructor, in PTSeq]
product [constructor, in PTS]
prod_eq [constructor, in PTSeq]
PTS [inductive, in PTS]
PTS [library]
PTSeq [inductive, in PTSeq]
PTSeq [library]
PTSeq_Context_Conversion [lemma, in PTSeq]
PTSeq_Context_Validity [lemma, in PTSeq]
PTSeq_conv [lemma, in PTSeq]
PTSeq_induction [lemma, in PTSeq]
PTSeq_Substitution [lemma, in PTSeq]
PTSeq_Substitution_bot [lemma, in PTSeq]
PTSeq_to_PTS_l [lemma, in PTSeq]
PTSeq_to_PTS_r [lemma, in PTSeq]
PTSeq_Type_Validity [lemma, in PTSeq]
PTS' [inductive, in PTSeq]
PTS'_Context_Conversion [lemma, in PTSeq]
PTS'_Context_Validity [lemma, in PTSeq]
PTS'_Substitution [lemma, in PTSeq]
PTS'_Substitution_bot [lemma, in PTSeq]
PTS'_to_PTS [lemma, in PTSeq]
PTS'_Type_Validity [lemma, in PTSeq]
PTS'_Weakening [lemma, in PTSeq]
PTS'_Weakening1 [lemma, in PTSeq]
Q
quantright [definition, in Terms]
R
red [inductive, in Conv]
red_app [lemma, in Conv]
red_appl [lemma, in Conv]
red_appr [lemma, in Conv]
red_beta [lemma, in Conv]
red_botsub [lemma, in Conv]
red_dmnd [lemma, in CR]
red_lda [lemma, in Conv]
red_ldal [lemma, in Conv]
red_ldar [lemma, in Conv]
red_lda_injl [lemma, in Conv]
red_lda_injr [lemma, in Conv]
red_liftsub [lemma, in Conv]
red_liftterm [lemma, in Conv]
red_liftterm_inv [lemma, in Conv]
red_par_red1 [constructor, in Conv]
red_par_red1_comm [lemma, in CR]
red_pi [lemma, in Conv]
red_pil [lemma, in Conv]
red_pir [lemma, in Conv]
red_pi_injl [lemma, in Conv]
red_pi_injr [lemma, in Conv]
red_Pi_inv [lemma, in String]
red_ref [lemma, in Conv]
red_srt_inj [lemma, in Conv]
red_string [definition, in String]
red_string_ref [lemma, in String]
red_sub [definition, in Conv]
red_subbot [lemma, in Conv]
red_subbotl [lemma, in Conv]
red_subbotr [lemma, in Conv]
red_subst [lemma, in Conv]
red_substl [lemma, in Conv]
red_substr [lemma, in Conv]
red_subvar [lemma, in Conv]
red_subvar_inj [lemma, in Conv]
red_subvar_inv [lemma, in Conv]
red_subvar_Pi [lemma, in String]
red_sub_ref [lemma, in Conv]
red_trans [constructor, in Conv]
red_var_inj [lemma, in Conv]
ref [constructor, in PTSeq]
Right_Hand_Reflexivity [lemma, in TPOSR]
rule [axiom, in PTS]
S
satisfy [definition, in PTS]
satisfy' [definition, in PTSeq]
satisfy'_botsub [lemma, in PTSeq]
satisfy_botsub [lemma, in PTS]
satisfy_concat [lemma, in String]
satisfy_eq [definition, in PTSeq]
satisfy_eq_ref [lemma, in PTSeq]
satisfy_eq_validl [lemma, in PTSeq]
satisfy_eq_validr [lemma, in PTSeq]
Sfun [definition, in Finite]
Sfun_comp [lemma, in Finite]
Sfun_ext [lemma, in Finite]
Sfun_id [lemma, in Finite]
Sfun_inj [lemma, in Finite]
Sfun_is_liftlabsub [lemma, in Labsubvar]
Sfun_is_liftsub [lemma, in Subvar]
Sigma [definition, in Strength]
Sigma_ctxt_irrel [lemma, in Strength]
Sigma_gen [lemma, in Strength]
Sigma_typing [lemma, in Strength]
Some_inj [lemma, in Finite]
sort [axiom, in Terms]
sortlike [definition, in Strength]
sortlike_liftterm [lemma, in Strength]
sortlike_liftterm' [lemma, in Strength]
sortlike_subvar [lemma, in Strength]
sortlike_subvar' [lemma, in Strength]
SR [library]
srt [constructor, in Terms]
srt_inj [lemma, in Terms]
srt_wd [lemma, in Terms]
start [constructor, in PTS]
Start_ax [lemma, in PTS]
Start_Ax [lemma, in PTSeq]
Start_Var [lemma, in PTSeq]
Start_var [lemma, in PTS]
Strength [library]
Strengthening [lemma, in Strength]
Strength_satisfy [lemma, in PTS]
Strength_satisfy' [lemma, in PTSeq]
Strength_satisfy_eq [lemma, in PTSeq]
Strength_subctxt [lemma, in PTS]
string [inductive, in String]
String [library]
string_id [definition, in String]
string_id_is_id [lemma, in String]
string_leq [lemma, in String]
string_m_n [lemma, in String]
string_n_n [lemma, in String]
strsubst [definition, in String]
strsubvar [definition, in String]
subbot [definition, in Subst]
subbot_liftterm [lemma, in Subst]
subbot_string [definition, in String]
subbot_subvar [lemma, in Subst]
subctxt [definition, in PTS]
subctxt_concat [lemma, in String]
subctxt_ext [lemma, in PTS]
subctxt_satisfy [lemma, in PTSeq]
subctxt_up [lemma, in PTS]
Subject_par_Reduction [lemma, in SR]
Subject_Reduction [lemma, in SR]
subst [definition, in Subst]
Subst [library]
Substitution [lemma, in Meta]
Substitution [lemma, in PTSeq]
Substitution_bot [lemma, in Meta]
subst_ext [lemma, in Subst]
subst_is_subvar [lemma, in Subst]
subst_lift [definition, in String]
subst_liftterm [lemma, in Subst]
subst_liftterm_botsub [lemma, in Subst]
subst_lm [lemma, in Subst]
subst_subbot [lemma, in Subst]
subst_subvar [lemma, in Subst]
subvar [definition, in Subvar]
Subvar [library]
subvar_app [lemma, in Subvar]
subvar_ext [lemma, in Subvar]
subvar_inj [lemma, in Subvar]
subvar_lda [lemma, in Subvar]
subvar_lift [definition, in String]
subvar_liftterm [lemma, in Subvar]
subvar_lm [lemma, in Subvar]
subvar_pi [lemma, in Subvar]
subvar_srt [lemma, in Subvar]
subvar_subbot [lemma, in Subst]
subvar_subst [lemma, in Subst]
subvar_var [lemma, in Subvar]
sym [constructor, in PTSeq]
T
tail [definition, in String]
tail_wd [lemma, in String]
term [inductive, in Terms]
Terms [library]
Test [library]
TPOSR [inductive, in TPOSR]
TPOSR [library]
TPOSRapp [constructor, in TPOSR]
TPOSRax [constructor, in TPOSR]
TPOSRbeta [constructor, in TPOSR]
TPOSRconv [inductive, in TPOSR]
TPOSRconv_Context_Validity [lemma, in TPOSR]
TPOSRconv_conv [lemma, in TPOSR]
TPOSRconv_Reflexivity [lemma, in TPOSR]
TPOSRconv_Reflexivityl [lemma, in TPOSR]
TPOSRconv_sym [constructor, in TPOSR]
TPOSRconv_to_PTS' [lemma, in TPOSR]
TPOSRconv_to_PTS'_l [lemma, in TPOSR]
TPOSRconv_to_PTS'_r [lemma, in TPOSR]
TPOSRconv_to_PTS_l [lemma, in TPOSR]
TPOSRconv_to_PTS_r [lemma, in TPOSR]
TPOSRconv_TPOSR [constructor, in TPOSR]
TPOSRconv_trans [constructor, in TPOSR]
TPOSRconv_Unique_Sorts [lemma, in TPOSR]
TPOSRconv_Weakening' [lemma, in TPOSR]
TPOSRctxt [constructor, in TPOSR]
TPOSRemp [constructor, in TPOSR]
TPOSRexp [constructor, in TPOSR]
TPOSRlambda [constructor, in TPOSR]
TPOSRplus [inductive, in TPOSR]
TPOSRplus_TPOSR [constructor, in TPOSR]
TPOSRplus_trans [constructor, in TPOSR]
TPOSRprod [constructor, in TPOSR]
TPOSRred [constructor, in TPOSR]
TPOSRsatisfy [definition, in TPOSR]
TPOSRsatisfy_last [lemma, in TPOSR]
TPOSRsatisfy_LHR [lemma, in TPOSR]
TPOSRvar [constructor, in TPOSR]
TPOSR_Context_Expansion [lemma, in TPOSR]
TPOSR_Context_Reduction [lemma, in TPOSR]
TPOSR_Context_Validity [lemma, in TPOSR]
TPOSR_conv [lemma, in TPOSR]
TPOSR_conv_ctxt [definition, in TPOSR]
TPOSR_conv_ctxt_x [lemma, in TPOSR]
TPOSR_induction [lemma, in TPOSR]
TPOSR_red [lemma, in TPOSR]
TPOSR_red_ctxt [definition, in TPOSR]
TPOSR_red_ctxt_pre_TPOSR_red_ctxt [lemma, in TPOSR]
TPOSR_red_ctxt_validl [lemma, in TPOSR]
TPOSR_red_ctxt_x [lemma, in TPOSR]
TPOSR_Substitution [lemma, in TPOSR]
TPOSR_Substitution' [lemma, in TPOSR]
TPOSR_to_PTSeq [lemma, in TPOSR]
TPOSR_to_PTS'_l [lemma, in TPOSR]
TPOSR_to_PTS'_r [lemma, in TPOSR]
TPOSR_to_PTS_l [lemma, in TPOSR]
TPOSR_to_PTS_r [lemma, in TPOSR]
TPOSR_Unique_Sorts [lemma, in TPOSR]
TPOSR_valid [inductive, in TPOSR]
TPOSR_Weakening [lemma, in TPOSR]
TPOSR_Weakening' [lemma, in TPOSR]
trans [constructor, in PTSeq]
Triv_satisfy [lemma, in PTS]
Triv_satisfy' [lemma, in PTSeq]
Triv_subctxt [lemma, in PTS]
triv_subst [lemma, in Subst]
triv_subst' [lemma, in Subst]
triv_subvar [lemma, in Subvar]
typeof [definition, in PTS]
Type_Eq_Valid [lemma, in PTSeq]
Type_Validity [lemma, in Meta]
Typing_Lemma_sortlike [lemma, in Strength]
U
Unique_Types [lemma, in UT]
Unique_Type_varlike [lemma, in Strength]
unlab [definition, in Labterms]
unlab_app [lemma, in Labterms]
unlab_conv [lemma, in Labconv]
unlab_ctxt [definition, in Labctxt]
unlab_lda [lemma, in Labterms]
unlab_liftlabterm [lemma, in Labsubvar]
unlab_liftsub [lemma, in Labsubvar]
unlab_par_red1 [lemma, in Labconv]
unlab_par_red1' [lemma, in Labconv]
unlab_pi [lemma, in Labterms]
unlab_red [lemma, in Labconv]
unlab_red' [lemma, in Labconv]
unlab_srt [lemma, in Labterms]
unlab_subbot [lemma, in Labsubst]
unlab_subst [lemma, in Labsubst]
unlab_subvar [lemma, in Labsubvar]
unlab_typeof [lemma, in Labctxt]
unlab_var [lemma, in Labterms]
up [definition, in Finite]
up_inj [lemma, in Finite]
up_wd [lemma, in Finite]
UT [library]
V
valid [definition, in PTS]
valid' [definition, in PTSeq]
valid'_Weakening1 [lemma, in PTSeq]
valid_concat [lemma, in String]
valid_concat' [lemma, in String]
var [constructor, in PTSeq]
var [definition, in Strength]
var [constructor, in Terms]
var [definition, in Strength]
varlike [definition, in Strength]
varlike_subvar [lemma, in Strength]
varlike_subvar' [lemma, in Strength]
var_inj [lemma, in Terms]
var_not_sort [lemma, in Strength]
var_or_sort [lemma, in Strength]
var_wd [lemma, in Terms]
W
weak [constructor, in PTSeq]
weakening [constructor, in PTS]
Weakening [lemma, in Meta]
weak_eq [constructor, in PTSeq]
Weak_satisfy [lemma, in Meta]
Weak_satisfyl [lemma, in PTS]
Weak_satisfy' [lemma, in PTSeq]
Weak_satisfy'l [lemma, in PTSeq]
Weak_satisfy_eql [lemma, in PTSeq]
Weak_subctxt [lemma, in PTS]
Weak_subctxtr [lemma, in PTS]
Weak_valid [lemma, in PTS]
Axiom Index
A
axiom [in PTS]
F
func_ax [in UT]
func_rule [in UT]
R
rule [in PTS]
S
sort [in Terms]
Lemma Index
A
app_injl [in Terms]
app_injr [in Terms]
app_wd [in Terms]
app_wdl [in Terms]
app_wdr [in Terms]
B
botsub_liftsub [in Subst]
botsub_Sfun [in Subst]
botsub_up [in Subst]
C
CComp_is_Comp [in Subst]
Church_Rosser [in CR]
Comp_is_comp [in Subvar]
Context_Conversion [in Meta]
Context_Strength [in Meta]
Context_Validity [in PTSeq]
Context_Validity [in PTS]
conversion' [in SR]
conv_app [in Conv]
conv_appl [in Conv]
conv_appr [in Conv]
conv_botsub [in Conv]
conv_ctxt_build [in PTS]
conv_ctxt_injl [in PTS]
conv_ctxt_injr [in PTS]
conv_ctxt_ref [in PTS]
conv_lda [in Conv]
conv_ldal [in Conv]
conv_ldar [in Conv]
conv_lda_injl [in CR]
conv_lda_injr [in CR]
conv_liftsub [in Conv]
conv_liftterm [in Conv]
conv_liftterm_inj [in CR]
conv_pi [in Conv]
conv_pil [in Conv]
conv_pir [in Conv]
conv_pi_injl [in CR]
conv_pi_injr [in CR]
conv_Pi_srt [in String]
conv_Pi_srt' [in String]
conv_red [in Conv]
conv_red' [in Conv]
conv_ref [in Conv]
conv_srt_inj [in CR]
conv_subbot [in Conv]
conv_subbotl [in Conv]
conv_subbotr [in Conv]
conv_subst [in Conv]
conv_substl [in Conv]
conv_substr [in Conv]
conv_subvar [in Conv]
conv_subvar_inj [in CR]
conv_sub_ref [in Conv]
conv_var_inj [in CR]
ctxt_eq_ref [in PTSeq]
ctxt_eq_validl [in PTSeq]
ctxt_eq_validr [in PTSeq]
ctxt_strng [in String]
E
Equation_Validity_l [in PTSeq]
Equation_Validity_r [in PTSeq]
equiv_consl [in PTSeq]
equiv_sym [in PTSeq]
equiv_trans [in PTSeq]
equiv_weak [in PTSeq]
F
funceq_ref [in Finite]
funceq_sym [in Finite]
funceq_trans [in Finite]
Functionality [in PTSeq]
Functionality_bot [in PTSeq]
G
Gen_abs [in PTSeq]
Gen_app [in PTSeq]
Gen_app [in Meta]
Gen_conv_lda [in CR]
Gen_conv_pi [in CR]
Gen_conv_srt [in CR]
Gen_conv_var [in CR]
Gen_lda [in Meta]
Gen_lda' [in Meta]
Gen_par_red1_app [in Conv]
Gen_par_red1_lda [in Conv]
Gen_par_red1_pi [in Conv]
Gen_par_red1_srt [in Conv]
Gen_par_red1_var [in Conv]
Gen_pi [in Meta]
Gen_pi' [in Meta]
Gen_product [in PTSeq]
Gen_red_lda [in Conv]
Gen_red_pi [in Conv]
Gen_red_srt [in Conv]
Gen_red_var [in Conv]
Gen_sort [in PTSeq]
Gen_srt [in Meta]
Gen_srt' [in Meta]
Gen_var [in PTSeq]
Gen_var [in Meta]
H
head_wd [in String]
L
labComp_is_comp [in Labsubvar]
lab_app_injcod [in Labterms]
lab_app_injl [in Labterms]
lab_app_injr [in Labterms]
lab_app_wd [in Labterms]
lab_app_wdcod [in Labterms]
lab_app_wdl [in Labterms]
lab_app_wdr [in Labterms]
lab_botsub_liftsub [in Labsubst]
lab_botsub_liftterm [in Labsubst]
lab_botsub_Sfun [in Labsubst]
lab_botsub_up [in Labsubst]
lab_CComp_is_Comp [in Labsubst]
lab_lda_injl [in Labterms]
lab_lda_injr [in Labterms]
lab_lda_wd [in Labterms]
lab_lda_wdl [in Labterms]
lab_lda_wdr [in Labterms]
lab_liftsub_CComp [in Labsubst]
lab_liftterm_subbot [in Labsubst]
lab_liftterm_subst [in Labsubst]
lab_liftterm_subst' [in Labsubst]
lab_par_red1_ref [in Labconv]
lab_pi_injl [in Labterms]
lab_pi_injr [in Labterms]
lab_pi_wd [in Labterms]
lab_pi_wdl [in Labterms]
lab_pi_wdr [in Labterms]
lab_srt_inj [in Labterms]
lab_srt_wd [in Labterms]
lab_subbot_liftterm [in Labsubst]
lab_subbot_subvar [in Labsubst]
lab_subctxt_up [in Labctxt]
lab_subctxt_Weak [in Labctxt]
lab_subst_ext [in Labsubst]
lab_subst_is_subvar [in Labsubst]
lab_subst_liftterm [in Labsubst]
lab_subst_liftterm_botsub [in Labsubst]
lab_subst_lm [in Labsubst]
lab_subst_subbot [in Labsubst]
lab_subst_subvar [in Labsubst]
lab_subvar_app [in Labsubvar]
lab_subvar_ext [in Labsubvar]
lab_subvar_inj [in Labsubvar]
lab_subvar_lda [in Labsubvar]
lab_subvar_liftlabterm [in Labsubvar]
lab_subvar_lm [in Labsubvar]
lab_subvar_pi [in Labsubvar]
lab_subvar_srt [in Labsubvar]
lab_subvar_subbot [in Labsubst]
lab_subvar_subst [in Labsubst]
lab_subvar_var [in Labsubvar]
lab_triv_subst [in Labsubst]
lab_triv_subvar [in Labsubvar]
lab_var_inj [in Labterms]
lab_var_wd [in Labterms]
lda_injl [in Terms]
lda_injr [in Terms]
Lda_subst [in String]
Lda_subvar [in String]
lda_wd [in Terms]
lda_wdl [in Terms]
lda_wdr [in Terms]
Left_Hand_Reflexivity [in TPOSR]
liftlabsub_comp [in Labsubvar]
liftlabsub_Comp [in Labsubvar]
liftlabsub_ext [in Labsubvar]
liftlabsub_id [in Labsubvar]
liftlabterm_app [in Labsubvar]
liftlabterm_inj [in Labsubvar]
liftlabterm_lab_subvar [in Labsubvar]
liftlabterm_lab_subvar' [in Labsubvar]
liftlabterm_lda [in Labsubvar]
liftlabterm_liftlabterm [in Labsubvar]
liftlabterm_liftlabterm' [in Labsubvar]
liftlabterm_pi [in Labsubvar]
liftlabterm_srt [in Labsubvar]
liftlabterm_var [in Labsubvar]
liftsub_CComp [in Subst]
liftsub_Comp [in Subvar]
liftsub_comp [in Subvar]
liftsub_ext [in Subvar]
liftsub_id [in Subvar]
liftterm_app [in Subvar]
liftterm_inj [in Subvar]
liftterm_lda [in Subvar]
liftterm_liftterm [in Subvar]
liftterm_liftterm' [in Subvar]
liftterm_pi [in Subvar]
liftterm_srt [in Subvar]
liftterm_subbot [in Subst]
liftterm_subst [in Subst]
liftterm_subst' [in Subst]
liftterm_subvar [in Subvar]
liftterm_subvar' [in Subvar]
liftterm_var [in Subvar]
lt_eq_lt_lm [in String]
M
mtch_leql [in String]
mtch_leqr [in String]
mtch_Sm_Sn [in String]
mtch_Sm_Sn' [in String]
mtch_Sm_Sn_inv [in String]
N
not_conv_pi_srt [in CR]
not_red_pi_srt [in Conv]
not_red_srt_pi [in Conv]
O
option_disc [in Finite]
P
par_red1_botsub [in Conv]
par_red1_ctxt_build [in PTS]
par_red1_ctxt_injl [in PTS]
par_red1_ctxt_injr [in PTS]
par_red1_ctxt_ref [in PTS]
par_red1_dmnd [in CR]
par_red1_lda_injl [in Conv]
par_red1_lda_injr [in Conv]
par_red1_liftsub [in Conv]
par_red1_liftterm [in Conv]
par_red1_liftterm_inj [in Conv]
par_red1_liftterm_inv [in Conv]
par_red1_pi_injl [in Conv]
par_red1_pi_injr [in Conv]
par_red1_ref [in Conv]
par_red1_srt_inj [in Conv]
par_red1_subbot [in Conv]
par_red1_subst [in Conv]
par_red1_subvar [in Conv]
par_red1_subvar_inj [in Conv]
par_red1_subvar_inv [in Conv]
par_red1_sub_ref [in Conv]
par_red1_var_inj [in Conv]
pi_injl [in Terms]
pi_injr [in Terms]
Pi_subbot_srt [in String]
Pi_subst [in String]
Pi_subvar [in String]
Pi_subvar_inv [in String]
pi_wd [in Terms]
pi_wdl [in Terms]
pi_wdr [in Terms]
Predicate_Reduction [in SR]
pre_Context_Conversion [in PTSeq]
pre_Context_Reduction [in TPOSR]
pre_Context_Reduction' [in TPOSR]
pre_Functionality [in PTSeq]
pre_Functionality_bot [in PTSeq]
pre_Gen_abs [in PTSeq]
pre_Gen_app [in Meta]
pre_Gen_app [in PTSeq]
pre_Gen_lda [in Meta]
pre_Gen_par_red1_app [in Conv]
pre_Gen_par_red1_lda [in Conv]
pre_Gen_par_red1_pi [in Conv]
pre_Gen_par_red1_srt [in Conv]
pre_Gen_par_red1_var [in Conv]
pre_Gen_pi [in Meta]
pre_Gen_product [in PTSeq]
pre_Gen_red_lda [in Conv]
pre_Gen_red_pi [in Conv]
pre_Gen_red_srt [in Conv]
pre_Gen_red_var [in Conv]
pre_Gen_sort [in PTSeq]
pre_Gen_srt [in Meta]
pre_Gen_var [in PTSeq]
pre_Gen_var [in Meta]
pre_mtch_Sm_Sn' [in String]
pre_mtch_Sm_Sn_inv [in String]
pre_par_red1_subvar_inv [in Conv]
pre_PTSeq_Context_Conversion [in PTSeq]
pre_PTSeq_to_PTS [in PTSeq]
pre_PTS'_Context_Conversion [in PTSeq]
pre_red_subvar_inv [in Conv]
pre_Sigma_gen [in Strength]
pre_Sigma_typing [in Strength]
pre_Strengthening [in Strength]
pre_TPOSR_Context_Conversion [in TPOSR]
pre_TPOSR_conv [in TPOSR]
pre_TPOSR_red_ctxt_ref [in TPOSR]
pre_TPOSR_red_ctxt_TPOSR_ref [in TPOSR]
pre_TPOSR_red_ctxt_valid_r [in TPOSR]
pre_TPOSR_red_ctxt_valid_ref [in TPOSR]
pre_TPOSR_red_ctxt_xr [in TPOSR]
pre_TPOSR_to_PTSeq [in TPOSR]
pre_unlab_par_red1' [in Labconv]
pre_unlab_red' [in Labconv]
pre_Weak_satisfy_eq [in PTSeq]
PTSeq_Context_Conversion [in PTSeq]
PTSeq_Context_Validity [in PTSeq]
PTSeq_conv [in PTSeq]
PTSeq_induction [in PTSeq]
PTSeq_Substitution [in PTSeq]
PTSeq_Substitution_bot [in PTSeq]
PTSeq_to_PTS_l [in PTSeq]
PTSeq_to_PTS_r [in PTSeq]
PTSeq_Type_Validity [in PTSeq]
PTS'_Context_Conversion [in PTSeq]
PTS'_Context_Validity [in PTSeq]
PTS'_Substitution [in PTSeq]
PTS'_Substitution_bot [in PTSeq]
PTS'_to_PTS [in PTSeq]
PTS'_Type_Validity [in PTSeq]
PTS'_Weakening [in PTSeq]
PTS'_Weakening1 [in PTSeq]
R
red_app [in Conv]
red_appl [in Conv]
red_appr [in Conv]
red_beta [in Conv]
red_botsub [in Conv]
red_dmnd [in CR]
red_lda [in Conv]
red_ldal [in Conv]
red_ldar [in Conv]
red_lda_injl [in Conv]
red_lda_injr [in Conv]
red_liftsub [in Conv]
red_liftterm [in Conv]
red_liftterm_inv [in Conv]
red_par_red1_comm [in CR]
red_pi [in Conv]
red_pil [in Conv]
red_pir [in Conv]
red_pi_injl [in Conv]
red_pi_injr [in Conv]
red_Pi_inv [in String]
red_ref [in Conv]
red_srt_inj [in Conv]
red_string_ref [in String]
red_subbot [in Conv]
red_subbotl [in Conv]
red_subbotr [in Conv]
red_subst [in Conv]
red_substl [in Conv]
red_substr [in Conv]
red_subvar [in Conv]
red_subvar_inj [in Conv]
red_subvar_inv [in Conv]
red_subvar_Pi [in String]
red_sub_ref [in Conv]
red_var_inj [in Conv]
Right_Hand_Reflexivity [in TPOSR]
S
satisfy'_botsub [in PTSeq]
satisfy_botsub [in PTS]
satisfy_concat [in String]
satisfy_eq_ref [in PTSeq]
satisfy_eq_validl [in PTSeq]
satisfy_eq_validr [in PTSeq]
Sfun_comp [in Finite]
Sfun_ext [in Finite]
Sfun_id [in Finite]
Sfun_inj [in Finite]
Sfun_is_liftlabsub [in Labsubvar]
Sfun_is_liftsub [in Subvar]
Sigma_ctxt_irrel [in Strength]
Sigma_gen [in Strength]
Sigma_typing [in Strength]
Some_inj [in Finite]
sortlike_liftterm [in Strength]
sortlike_liftterm' [in Strength]
sortlike_subvar [in Strength]
sortlike_subvar' [in Strength]
srt_inj [in Terms]
srt_wd [in Terms]
Start_ax [in PTS]
Start_Ax [in PTSeq]
Start_Var [in PTSeq]
Start_var [in PTS]
Strengthening [in Strength]
Strength_satisfy [in PTS]
Strength_satisfy' [in PTSeq]
Strength_satisfy_eq [in PTSeq]
Strength_subctxt [in PTS]
string_id_is_id [in String]
string_leq [in String]
string_m_n [in String]
string_n_n [in String]
subbot_liftterm [in Subst]
subbot_subvar [in Subst]
subctxt_concat [in String]
subctxt_ext [in PTS]
subctxt_satisfy [in PTSeq]
subctxt_up [in PTS]
Subject_par_Reduction [in SR]
Subject_Reduction [in SR]
Substitution [in Meta]
Substitution [in PTSeq]
Substitution_bot [in Meta]
subst_ext [in Subst]
subst_is_subvar [in Subst]
subst_liftterm [in Subst]
subst_liftterm_botsub [in Subst]
subst_lm [in Subst]
subst_subbot [in Subst]
subst_subvar [in Subst]
subvar_app [in Subvar]
subvar_ext [in Subvar]
subvar_inj [in Subvar]
subvar_lda [in Subvar]
subvar_liftterm [in Subvar]
subvar_lm [in Subvar]
subvar_pi [in Subvar]
subvar_srt [in Subvar]
subvar_subbot [in Subst]
subvar_subst [in Subst]
subvar_var [in Subvar]
T
tail_wd [in String]
TPOSRconv_Context_Validity [in TPOSR]
TPOSRconv_conv [in TPOSR]
TPOSRconv_Reflexivity [in TPOSR]
TPOSRconv_Reflexivityl [in TPOSR]
TPOSRconv_to_PTS' [in TPOSR]
TPOSRconv_to_PTS'_l [in TPOSR]
TPOSRconv_to_PTS'_r [in TPOSR]
TPOSRconv_to_PTS_l [in TPOSR]
TPOSRconv_to_PTS_r [in TPOSR]
TPOSRconv_Unique_Sorts [in TPOSR]
TPOSRconv_Weakening' [in TPOSR]
TPOSRsatisfy_last [in TPOSR]
TPOSRsatisfy_LHR [in TPOSR]
TPOSR_Context_Expansion [in TPOSR]
TPOSR_Context_Reduction [in TPOSR]
TPOSR_Context_Validity [in TPOSR]
TPOSR_conv [in TPOSR]
TPOSR_conv_ctxt_x [in TPOSR]
TPOSR_induction [in TPOSR]
TPOSR_red [in TPOSR]
TPOSR_red_ctxt_pre_TPOSR_red_ctxt [in TPOSR]
TPOSR_red_ctxt_validl [in TPOSR]
TPOSR_red_ctxt_x [in TPOSR]
TPOSR_Substitution [in TPOSR]
TPOSR_Substitution' [in TPOSR]
TPOSR_to_PTSeq [in TPOSR]
TPOSR_to_PTS'_l [in TPOSR]
TPOSR_to_PTS'_r [in TPOSR]
TPOSR_to_PTS_l [in TPOSR]
TPOSR_to_PTS_r [in TPOSR]
TPOSR_Unique_Sorts [in TPOSR]
TPOSR_Weakening [in TPOSR]
TPOSR_Weakening' [in TPOSR]
Triv_satisfy [in PTS]
Triv_satisfy' [in PTSeq]
Triv_subctxt [in PTS]
triv_subst [in Subst]
triv_subst' [in Subst]
triv_subvar [in Subvar]
Type_Eq_Valid [in PTSeq]
Type_Validity [in Meta]
Typing_Lemma_sortlike [in Strength]
U
Unique_Types [in UT]
Unique_Type_varlike [in Strength]
unlab_app [in Labterms]
unlab_conv [in Labconv]
unlab_lda [in Labterms]
unlab_liftlabterm [in Labsubvar]
unlab_liftsub [in Labsubvar]
unlab_par_red1 [in Labconv]
unlab_par_red1' [in Labconv]
unlab_pi [in Labterms]
unlab_red [in Labconv]
unlab_red' [in Labconv]
unlab_srt [in Labterms]
unlab_subbot [in Labsubst]
unlab_subst [in Labsubst]
unlab_subvar [in Labsubvar]
unlab_typeof [in Labctxt]
unlab_var [in Labterms]
up_inj [in Finite]
up_wd [in Finite]
V
valid'_Weakening1 [in PTSeq]
valid_concat [in String]
valid_concat' [in String]
varlike_subvar [in Strength]
varlike_subvar' [in Strength]
var_inj [in Terms]
var_not_sort [in Strength]
var_or_sort [in Strength]
var_wd [in Terms]
W
Weakening [in Meta]
Weak_satisfy [in Meta]
Weak_satisfyl [in PTS]
Weak_satisfy' [in PTSeq]
Weak_satisfy'l [in PTSeq]
Weak_satisfy_eql [in PTSeq]
Weak_subctxt [in PTS]
Weak_subctxtr [in PTS]
Weak_valid [in PTS]
Constructor Index
A
abstraction [in PTS]
app [in Terms]
appl [in PTSeq]
application [in PTS]
app_eq [in PTSeq]
ax [in PTSeq]
axioms [in PTS]
B
beta [in PTSeq]
C
cons [in String]
conv [in PTSeq]
conversion [in PTS]
conv_eq [in PTSeq]
conv_par_red1 [in Conv]
conv_sym [in Conv]
conv_trans [in Conv]
E
emp [in String]
equiv_cons [in PTSeq]
equiv_ref [in PTSeq]
L
l [in Labconv]
l [in Labconv]
lab_app [in Labterms]
lab_conv_par_red1 [in Labconv]
lab_conv_sym [in Labconv]
lab_conv_trans [in Labconv]
lab_lda [in Labterms]
lab_par_red1_app [in Labconv]
lab_par_red1_beta [in Labconv]
lab_par_red1_lda [in Labconv]
lab_par_red1_pi [in Labconv]
lab_par_red1_srt [in Labconv]
lab_par_red1_var [in Labconv]
lab_pi [in Labterms]
lab_red_par_red1 [in Labconv]
lab_red_trans [in Labconv]
lab_srt [in Labterms]
lab_var [in Labterms]
lambda [in PTSeq]
lambda_eq [in PTSeq]
lda [in Terms]
M
mtchO [in String]
mtchS [in String]
P
par_red1_app [in Conv]
par_red1_beta [in Conv]
par_red1_lda [in Conv]
par_red1_pi [in Conv]
par_red1_srt [in Conv]
par_red1_var [in Conv]
pi [in Terms]
prod [in PTSeq]
product [in PTS]
prod_eq [in PTSeq]
R
red_par_red1 [in Conv]
red_trans [in Conv]
ref [in PTSeq]
S
srt [in Terms]
start [in PTS]
sym [in PTSeq]
T
TPOSRapp [in TPOSR]
TPOSRax [in TPOSR]
TPOSRbeta [in TPOSR]
TPOSRconv_sym [in TPOSR]
TPOSRconv_TPOSR [in TPOSR]
TPOSRconv_trans [in TPOSR]
TPOSRctxt [in TPOSR]
TPOSRemp [in TPOSR]
TPOSRexp [in TPOSR]
TPOSRlambda [in TPOSR]
TPOSRplus_TPOSR [in TPOSR]
TPOSRplus_trans [in TPOSR]
TPOSRprod [in TPOSR]
TPOSRred [in TPOSR]
TPOSRvar [in TPOSR]
trans [in PTSeq]
V
var [in PTSeq]
var [in Terms]
W
weak [in PTSeq]
weakening [in PTS]
weak_eq [in PTSeq]
Inductive Index
C
conv [in Conv]
E
equiv [in PTSeq]
L
lab_conv [in Labconv]
lab_par_red1 [in Labconv]
lab_red [in Labconv]
lab_term [in Labterms]
M
mtch [in String]
P
par_red1 [in Conv]
PTS [in PTS]
PTSeq [in PTSeq]
PTS' [in PTSeq]
R
red [in Conv]
S
string [in String]
T
term [in Terms]
TPOSR [in TPOSR]
TPOSRconv [in TPOSR]
TPOSRplus [in TPOSR]
TPOSR_valid [in TPOSR]
Definition Index
A
antivar [in Terms]
appright [in Terms]
B
bot [in Finite]
botsub [in Subst]
C
CComp [in Subst]
Comp [in Subvar]
comp [in Finite]
concat [in String]
context [in PTS]
conv_ctxt [in PTS]
conv_sub [in Conv]
ctxt_eq [in PTSeq]
F
fin [in Finite]
funceq [in Finite]
H
head [in String]
I
id [in Finite]
injective [in Finite]
L
labCComp [in Labsubst]
labComp [in Labsubvar]
lab_antivar [in Labterms]
lab_appright [in Labterms]
lab_botsub [in Labsubst]
lab_ctxt [in Labctxt]
lab_left [in Labterms]
lab_right [in Labterms]
lab_subbot [in Labsubst]
lab_subctxt [in Labctxt]
lab_subst [in Labsubst]
lab_subvar [in Labsubvar]
lab_typeof [in Labctxt]
Lda [in String]
left [in Terms]
liftlabsub [in Labsubvar]
liftlabterm [in Labsubvar]
liftstring [in String]
liftsub [in Subvar]
liftterm [in Subvar]
O
O [in Labctxt]
P
par_red1_ctxt [in PTS]
par_red1_sub [in Conv]
Pi [in String]
pre_TPOSR_red_ctxt [in TPOSR]
Q
quantright [in Terms]
R
red_string [in String]
red_sub [in Conv]
S
satisfy [in PTS]
satisfy' [in PTSeq]
satisfy_eq [in PTSeq]
Sfun [in Finite]
Sigma [in Strength]
sortlike [in Strength]
string_id [in String]
strsubst [in String]
strsubvar [in String]
subbot [in Subst]
subbot_string [in String]
subctxt [in PTS]
subst [in Subst]
subst_lift [in String]
subvar [in Subvar]
subvar_lift [in String]
T
tail [in String]
TPOSRsatisfy [in TPOSR]
TPOSR_conv_ctxt [in TPOSR]
TPOSR_red_ctxt [in TPOSR]
typeof [in PTS]
U
unlab [in Labterms]
unlab_ctxt [in Labctxt]
up [in Finite]
V
valid [in PTS]
valid' [in PTSeq]
var [in Strength]
var [in Strength]
varlike [in Strength]
Library Index
C
Conv
CR
F
Finite
L
Labconv
Labctxt
Labsubst
Labsubvar
Labterms
M
Meta
P
PTS
PTSeq
S
SR
Strength
String
Subst
Subvar
T
Terms
Test
TPOSR
U
UT
| 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 |
_ |
(673 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 |
_ |
(5 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 |
_ |
(478 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 |
_ |
(78 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 |
_ |
(18 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 |
_ |
(74 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 |
_ |
(20 entries) |
This page has been generated by coqdoc