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 (337 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 (6 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 (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 _ other (165 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 (57 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 (17 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 (9 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 (31 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 (5 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 (2 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 (35 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 (5 entries)

Global Index

A

AllF [constructor, in SysF_PTS.sysf]
AppF [constructor, in SysF_PTS.sysf]
AppL [constructor, in SysF_PTS.lambda2]
atn [inductive, in SysF_PTS.lib]
atnd [inductive, in SysF_PTS.lib]
AtndS [constructor, in SysF_PTS.lib]
atnd_type_eqPrp_f [lemma, in SysF_PTS.lambda2]
atnd_notPrp_eqPrp_f [lemma, in SysF_PTS.lambda2]
atnd_eqPrp_t [lemma, in SysF_PTS.lambda2]
atnd_getD [lemma, in SysF_PTS.lib]
Atnd0 [constructor, in SysF_PTS.lib]
AtnS [constructor, in SysF_PTS.lib]
atn_mmap [lemma, in SysF_PTS.lib]
atn_get [lemma, in SysF_PTS.lib]
Atn0 [constructor, in SysF_PTS.lib]


B

bfr [definition, in SysF_PTS.lib]
bfr_ushift [lemma, in SysF_PTS.lib]
bfr_shift [lemma, in SysF_PTS.lib]
bfr_up [lemma, in SysF_PTS.lib]
bind [projection, in SysF_PTS.lib]


C

cm_typingL_beta [lemma, in SysF_PTS.lambda2]
cm_typingL_id [lemma, in SysF_PTS.lambda2]
cm_typingL_up [lemma, in SysF_PTS.lambda2]
cm_typingL [definition, in SysF_PTS.lambda2]
cm_typingP_beta_type [lemma, in SysF_PTS.lambda2]
cm_typingP_beta_term [lemma, in SysF_PTS.lambda2]
cm_typingP_up [lemma, in SysF_PTS.lambda2]
cm_typingP [definition, in SysF_PTS.lambda2]
cm_istyP_beta_term [lemma, in SysF_PTS.lambda2]
cm_istyP_beta_type [lemma, in SysF_PTS.lambda2]
cm_istyP_up [lemma, in SysF_PTS.lambda2]
cm_istyP [definition, in SysF_PTS.lambda2]
cm_typingL_nat_beta [lemma, in SysF_PTS.lambda2]
cm_typingL_nat_id [lemma, in SysF_PTS.lambda2]
cm_typingL_nat_up [lemma, in SysF_PTS.lambda2]
cm_typingL_nat [definition, in SysF_PTS.lambda2]
cm_tyrel_beta [lemma, in SysF_PTS.RelEquiv]
cm_tyrel_ext [lemma, in SysF_PTS.RelEquiv]
cm_tyrel_rs [lemma, in SysF_PTS.RelEquiv]
cm_tyrel [definition, in SysF_PTS.RelEquiv]
cm_istyF_beta [lemma, in SysF_PTS.sysf]
cm_istyF_up [lemma, in SysF_PTS.sysf]
cm_istyF [definition, in SysF_PTS.sysf]
Coincidence [section, in SysF_PTS.lib]
CoincidenceHSubst [section, in SysF_PTS.lib]
comb [definition, in SysF_PTS.lib]
comb_comp [lemma, in SysF_PTS.lib]
comb_cons [lemma, in SysF_PTS.lib]
ContextRenamings [section, in SysF_PTS.lib]
Countable [record, in SysF_PTS.Decidable]
countableProp [projection, in SysF_PTS.Decidable]
cr [definition, in SysF_PTS.lib]
cr_typingP_shift [lemma, in SysF_PTS.lambda2]
cr_typingP_up [lemma, in SysF_PTS.lambda2]
cr_typingP [definition, in SysF_PTS.lambda2]
cr_cm_istyP [lemma, in SysF_PTS.lambda2]
cr_istyP_ushift [lemma, in SysF_PTS.lambda2]
cr_istyP_shift [lemma, in SysF_PTS.lambda2]
cr_istyP_up_id [lemma, in SysF_PTS.lambda2]
cr_istyP_up [lemma, in SysF_PTS.lambda2]
cr_istyP_id [lemma, in SysF_PTS.lambda2]
cr_cr_istyP [lemma, in SysF_PTS.lambda2]
cr_istyP [definition, in SysF_PTS.lambda2]
cr_typingL_shift [lemma, in SysF_PTS.lambda2]
cr_typingL_up [lemma, in SysF_PTS.lambda2]
cr_typingL [definition, in SysF_PTS.lambda2]
cr_shift [lemma, in SysF_PTS.lib]
cr_up [lemma, in SysF_PTS.lib]
cr_typingF_shift [lemma, in SysF_PTS.sysf]
cr_typingF_ren_ushift [lemma, in SysF_PTS.sysf]
cr_typingF_ren [lemma, in SysF_PTS.sysf]
cr_typingF_up [lemma, in SysF_PTS.sysf]
cr_typingF_id [lemma, in SysF_PTS.sysf]
cr_typingF [definition, in SysF_PTS.sysf]
cr_istyF_ushift [lemma, in SysF_PTS.sysf]
cr_istyF_shift [lemma, in SysF_PTS.sysf]
cr_istyF_up [lemma, in SysF_PTS.sysf]
cr_istyF_id [lemma, in SysF_PTS.sysf]
cr_istyF [definition, in SysF_PTS.sysf]
CtxBoolFun [section, in SysF_PTS.lib]


D

Dec [record, in SysF_PTS.Decidable]
Dec [inductive, in SysF_PTS.Decidable]
dec [abbreviation, in SysF_PTS.Decidable]
Decidable [library]
decidable_neg [instance, in SysF_PTS.Decidable]
decide [projection, in SysF_PTS.Decidable]
decide [constructor, in SysF_PTS.Decidable]
decide_eq_termL [instance, in SysF_PTS.lambda2]
decide_eq_level [instance, in SysF_PTS.lambda2]
decide_eq_fin_domain [lemma, in SysF_PTS.Decidable]
decide_refl [lemma, in SysF_PTS.lib]
decide_eq_termF [instance, in SysF_PTS.sysf]
decide_eq_typeF [instance, in SysF_PTS.sysf]
Dec_eq_fin_domain [instance, in SysF_PTS.Decidable]
Dec_fin_quant [instance, in SysF_PTS.Decidable]
Dec_fin_quant_T [instance, in SysF_PTS.Decidable]
Dec_impl [instance, in SysF_PTS.Decidable]
Dec_or [instance, in SysF_PTS.Decidable]
Dec_and [instance, in SysF_PTS.Decidable]
Dec_lt_nat [instance, in SysF_PTS.Decidable]
Dec_le_nat [instance, in SysF_PTS.Decidable]
Dec_eq_option [instance, in SysF_PTS.Decidable]
Dec_eq_nat [instance, in SysF_PTS.Decidable]


E

enum [projection, in SysF_PTS.Decidable]
eqPrp [definition, in SysF_PTS.lambda2]
eqPrp_t_subst_t [lemma, in SysF_PTS.lambda2]
eqPrp_ren [lemma, in SysF_PTS.lambda2]
eq_dec [abbreviation, in SysF_PTS.Decidable]


F

Finite [record, in SysF_PTS.Decidable]
finiteProp [projection, in SysF_PTS.Decidable]
fmap [projection, in SysF_PTS.lib]
Functor [record, in SysF_PTS.lib]
Functor_Monad [instance, in SysF_PTS.lib]


G

gentypingP [definition, in SysF_PTS.lambda2]
gentypingP_typingP [lemma, in SysF_PTS.lambda2]
get [definition, in SysF_PTS.lib]
getD [definition, in SysF_PTS.lib]
getD_cons [lemma, in SysF_PTS.lib]
getD_get [lemma, in SysF_PTS.lib]
getD_atnd [lemma, in SysF_PTS.lib]
get_mmap_None [lemma, in SysF_PTS.lib]
get_mmap [lemma, in SysF_PTS.lib]
get_atn [lemma, in SysF_PTS.lib]


H

HSubstLemmas_termF [instance, in SysF_PTS.sysf]
HSubst_termF [instance, in SysF_PTS.sysf]


I

Ids_termL [instance, in SysF_PTS.lambda2]
Ids_termF [instance, in SysF_PTS.sysf]
Ids_typeF [instance, in SysF_PTS.sysf]
ImpF [constructor, in SysF_PTS.sysf]
internF [definition, in SysF_PTS.sysf]
internF_correct [lemma, in SysF_PTS.sysf]
internF_ty [definition, in SysF_PTS.sysf]
internL [definition, in SysF_PTS.lambda2]
internLP_correct [lemma, in SysF_PTS.lambda2]
istyF [inductive, in SysF_PTS.sysf]
istyF_beta [lemma, in SysF_PTS.sysf]
istyF_subst [lemma, in SysF_PTS.sysf]
istyF_strengthen [lemma, in SysF_PTS.sysf]
istyF_weaken [lemma, in SysF_PTS.sysf]
istyF_ren [lemma, in SysF_PTS.sysf]
istyF_all [constructor, in SysF_PTS.sysf]
istyF_imp [constructor, in SysF_PTS.sysf]
istyF_var [constructor, in SysF_PTS.sysf]
istyP [inductive, in SysF_PTS.lambda2]
istyP_typingL [lemma, in SysF_PTS.lambda2]
istyP_subst [lemma, in SysF_PTS.lambda2]
istyP_strengthen [lemma, in SysF_PTS.lambda2]
istyP_weaken [lemma, in SysF_PTS.lambda2]
istyP_ren [lemma, in SysF_PTS.lambda2]
istyP_neqPrp [lemma, in SysF_PTS.lambda2]
istyP_notSort [lemma, in SysF_PTS.lambda2]
istyP_prod2 [constructor, in SysF_PTS.lambda2]
istyP_prod1 [constructor, in SysF_PTS.lambda2]
istyP_var [constructor, in SysF_PTS.lambda2]


L

lambda2 [library]
LamF [constructor, in SysF_PTS.sysf]
LamL [constructor, in SysF_PTS.lambda2]
level [inductive, in SysF_PTS.lambda2]
lib [library]


M

mmap_get_None [lemma, in SysF_PTS.lib]
mmap_get [lemma, in SysF_PTS.lib]
mmap_atn [lemma, in SysF_PTS.lib]
Monad [record, in SysF_PTS.lib]


N

numElems [projection, in SysF_PTS.Decidable]


P

ProdL [constructor, in SysF_PTS.lambda2]
Prp [constructor, in SysF_PTS.lambda2]


R

RelEquiv [library]
Rename_termL [instance, in SysF_PTS.lambda2]
Rename_termF [instance, in SysF_PTS.sysf]
Rename_typeF [instance, in SysF_PTS.sysf]
repr [projection, in SysF_PTS.Decidable]
ret [projection, in SysF_PTS.lib]


S

SortL [constructor, in SysF_PTS.lambda2]
sortL_add_subst [lemma, in SysF_PTS.lambda2]
sortL_p1 [lemma, in SysF_PTS.lambda2]
sortL_ren [lemma, in SysF_PTS.lambda2]
sortP_eqPrp_f [lemma, in SysF_PTS.lambda2]
sortP_neq_ren [lemma, in SysF_PTS.lambda2]
SubstHSubstComp_typeF_termF [instance, in SysF_PTS.sysf]
SubstInstance [section, in SysF_PTS.lib]
SubstLemmas_termL [instance, in SysF_PTS.lambda2]
SubstLemmas_termF [instance, in SysF_PTS.sysf]
SubstLemmas_typeF [instance, in SysF_PTS.sysf]
Subst_termL [instance, in SysF_PTS.lambda2]
subst_coinc_hcomp [lemma, in SysF_PTS.lib]
subst_coinc_hd_f [lemma, in SysF_PTS.lib]
subst_coinc_up [lemma, in SysF_PTS.lib]
subst_coinc_id [lemma, in SysF_PTS.lib]
subst_coinc [definition, in SysF_PTS.lib]
Subst_termF [instance, in SysF_PTS.sysf]
Subst_typeF [instance, in SysF_PTS.sysf]
sum2bool [definition, in SysF_PTS.lib]
sysf [library]


T

termF [inductive, in SysF_PTS.sysf]
termL [inductive, in SysF_PTS.lambda2]
tmrel [inductive, in SysF_PTS.RelEquiv]
tmrel_lf_total_preserving [lemma, in SysF_PTS.RelEquiv]
tmrel_fl_total_preserving [lemma, in SysF_PTS.RelEquiv]
tmrel_injective [lemma, in SysF_PTS.RelEquiv]
tmrel_functional [lemma, in SysF_PTS.RelEquiv]
tmrel_lf_tot_pres [lemma, in SysF_PTS.RelEquiv]
tmrel_fl_tot_pres [lemma, in SysF_PTS.RelEquiv]
tmrel_inj [lemma, in SysF_PTS.RelEquiv]
tmrel_func [lemma, in SysF_PTS.RelEquiv]
tmrel_tyabs [constructor, in SysF_PTS.RelEquiv]
tmrel_tyspec [constructor, in SysF_PTS.RelEquiv]
tmrel_lam [constructor, in SysF_PTS.RelEquiv]
tmrel_app [constructor, in SysF_PTS.RelEquiv]
tmrel_var [constructor, in SysF_PTS.RelEquiv]
TmVarF [constructor, in SysF_PTS.sysf]
TyAbsF [constructor, in SysF_PTS.sysf]
Typ [constructor, in SysF_PTS.lambda2]
typeF [inductive, in SysF_PTS.sysf]
typingF [inductive, in SysF_PTS.sysf]
typingF_weaken_ty [lemma, in SysF_PTS.sysf]
typingF_ren_ty [lemma, in SysF_PTS.sysf]
typingF_weaken [lemma, in SysF_PTS.sysf]
typingF_ren [lemma, in SysF_PTS.sysf]
typingF_tyabs [constructor, in SysF_PTS.sysf]
typingF_tyspec [constructor, in SysF_PTS.sysf]
typingF_lam [constructor, in SysF_PTS.sysf]
typingF_app [constructor, in SysF_PTS.sysf]
typingF_var [constructor, in SysF_PTS.sysf]
typingL [inductive, in SysF_PTS.lambda2]
typingL_typ_degenerate [lemma, in SysF_PTS.lambda2]
typingL_propagation [lemma, in SysF_PTS.lambda2]
typingL_beta [lemma, in SysF_PTS.lambda2]
typingL_subst [lemma, in SysF_PTS.lambda2]
typingL_sort_strengthen [lemma, in SysF_PTS.lambda2]
typingL_typingP [lemma, in SysF_PTS.lambda2]
typingL_typ_degenerate_nat [lemma, in SysF_PTS.lambda2]
typingL_propagation_nat [lemma, in SysF_PTS.lambda2]
typingL_beta_nat [lemma, in SysF_PTS.lambda2]
typingL_subst_nat [lemma, in SysF_PTS.lambda2]
typingL_weaken [lemma, in SysF_PTS.lambda2]
typingL_ren [lemma, in SysF_PTS.lambda2]
typingL_prp_prp_contra [lemma, in SysF_PTS.lambda2]
typingL_lam [constructor, in SysF_PTS.lambda2]
typingL_app [constructor, in SysF_PTS.lambda2]
typingL_prod [constructor, in SysF_PTS.lambda2]
typingL_var [constructor, in SysF_PTS.lambda2]
typingL_ax [constructor, in SysF_PTS.lambda2]
typingP [inductive, in SysF_PTS.lambda2]
typingPL_equiv [lemma, in SysF_PTS.lambda2]
typingP_typingL [lemma, in SysF_PTS.lambda2]
typingP_istyP [lemma, in SysF_PTS.lambda2]
typingP_beta_type [lemma, in SysF_PTS.lambda2]
typingP_beta_term [lemma, in SysF_PTS.lambda2]
typingP_subst [lemma, in SysF_PTS.lambda2]
typingP_weaken [lemma, in SysF_PTS.lambda2]
typingP_ren [lemma, in SysF_PTS.lambda2]
typingP_lam2 [constructor, in SysF_PTS.lambda2]
typingP_app2 [constructor, in SysF_PTS.lambda2]
typingP_lam1 [constructor, in SysF_PTS.lambda2]
typingP_app1 [constructor, in SysF_PTS.lambda2]
typingP_var [constructor, in SysF_PTS.lambda2]
tyrel [inductive, in SysF_PTS.RelEquiv]
tyrel_lf_total_preserving [lemma, in SysF_PTS.RelEquiv]
tyrel_fl_total_preserving [lemma, in SysF_PTS.RelEquiv]
tyrel_injective [lemma, in SysF_PTS.RelEquiv]
tyrel_functional [lemma, in SysF_PTS.RelEquiv]
tyrel_tmrel_disjoint [lemma, in SysF_PTS.RelEquiv]
tyrel_beta [lemma, in SysF_PTS.RelEquiv]
tyrel_subst [lemma, in SysF_PTS.RelEquiv]
tyrel_unmap [lemma, in SysF_PTS.RelEquiv]
tyrel_weaken_hd [lemma, in SysF_PTS.RelEquiv]
tyrel_weaken [lemma, in SysF_PTS.RelEquiv]
tyrel_ren [lemma, in SysF_PTS.RelEquiv]
tyrel_lf_tot_pres [lemma, in SysF_PTS.RelEquiv]
tyrel_fl_tot_pres [lemma, in SysF_PTS.RelEquiv]
tyrel_inj [lemma, in SysF_PTS.RelEquiv]
tyrel_func [lemma, in SysF_PTS.RelEquiv]
tyrel_all [constructor, in SysF_PTS.RelEquiv]
tyrel_imp [constructor, in SysF_PTS.RelEquiv]
tyrel_var [constructor, in SysF_PTS.RelEquiv]
TySpecF [constructor, in SysF_PTS.sysf]
TyVarF [constructor, in SysF_PTS.sysf]


U

upren_comb [lemma, in SysF_PTS.lib]


V

VarL [constructor, in SysF_PTS.lambda2]
vr [definition, in SysF_PTS.RelEquiv]
vrel [definition, in SysF_PTS.RelEquiv]
vrm [definition, in SysF_PTS.RelEquiv]
vrm_app [lemma, in SysF_PTS.RelEquiv]
vrm_comb [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf_ext_rs [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf_rs_ext [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf_nil [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_lf [definition, in SysF_PTS.RelEquiv]
vr_tmctx_fl_ext_rs [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_fl_rs_ext [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_fl_nil [lemma, in SysF_PTS.RelEquiv]
vr_tmctx_fl [definition, in SysF_PTS.RelEquiv]
vr_rdis_ext_rs [lemma, in SysF_PTS.RelEquiv]
vr_rdis_rs_ext [lemma, in SysF_PTS.RelEquiv]
vr_rdis_r_nil [lemma, in SysF_PTS.RelEquiv]
vr_rdis_l_nil [lemma, in SysF_PTS.RelEquiv]
vr_rdis_sym [lemma, in SysF_PTS.RelEquiv]
vr_rdis [definition, in SysF_PTS.RelEquiv]
vr_tyctx_lf_ext [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_lf_rs [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_lf_nil [definition, in SysF_PTS.RelEquiv]
vr_tyctx_lf [definition, in SysF_PTS.RelEquiv]
vr_tyctx_fl_ext [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_fl_rs [lemma, in SysF_PTS.RelEquiv]
vr_tyctx_fl_nil [definition, in SysF_PTS.RelEquiv]
vr_tyctx_fl [definition, in SysF_PTS.RelEquiv]
vr_inj_ext [lemma, in SysF_PTS.RelEquiv]
vr_inj_rs [lemma, in SysF_PTS.RelEquiv]
vr_inj_nil [lemma, in SysF_PTS.RelEquiv]
vr_inj [definition, in SysF_PTS.RelEquiv]
vr_func_ext [lemma, in SysF_PTS.RelEquiv]
vr_func_rs [lemma, in SysF_PTS.RelEquiv]
vr_func_nil [lemma, in SysF_PTS.RelEquiv]
vr_func [definition, in SysF_PTS.RelEquiv]
vr_right_app [lemma, in SysF_PTS.RelEquiv]
vr_left_app [lemma, in SysF_PTS.RelEquiv]
vr_app_or [lemma, in SysF_PTS.RelEquiv]
vr_unmap [lemma, in SysF_PTS.RelEquiv]
vr_map [lemma, in SysF_PTS.RelEquiv]


W

wfF [inductive, in SysF_PTS.sysf]
wfF_ext_tm [constructor, in SysF_PTS.sysf]
wfF_ext_ty [constructor, in SysF_PTS.sysf]
wfF_empty [constructor, in SysF_PTS.sysf]
wfL [inductive, in SysF_PTS.lambda2]
wfL_atnd_ok [lemma, in SysF_PTS.lambda2]
wfL_ext [constructor, in SysF_PTS.lambda2]
wfL_empty [constructor, in SysF_PTS.lambda2]
wfP [inductive, in SysF_PTS.lambda2]
wfP_ext_ty [constructor, in SysF_PTS.lambda2]
wfP_ext_prp [constructor, in SysF_PTS.lambda2]
wfP_empty [constructor, in SysF_PTS.lambda2]


other

_ <$> _ [notation, in SysF_PTS.lib]
do _ <- _ ; _ [notation, in SysF_PTS.lib]
GET _ <- _ ; _ [notation, in SysF_PTS.lib]
$$( _ ) [notation, in SysF_PTS.lib]
$? [notation, in SysF_PTS.lib]
(-1) [notation, in SysF_PTS.lib]



Notation Index

other

_ <$> _ [in SysF_PTS.lib]
do _ <- _ ; _ [in SysF_PTS.lib]
GET _ <- _ ; _ [in SysF_PTS.lib]
$$( _ ) [in SysF_PTS.lib]
$? [in SysF_PTS.lib]
(-1) [in SysF_PTS.lib]



Library Index

D

Decidable


L

lambda2
lib


R

RelEquiv


S

sysf



Lemma Index

A

atnd_type_eqPrp_f [in SysF_PTS.lambda2]
atnd_notPrp_eqPrp_f [in SysF_PTS.lambda2]
atnd_eqPrp_t [in SysF_PTS.lambda2]
atnd_getD [in SysF_PTS.lib]
atn_mmap [in SysF_PTS.lib]
atn_get [in SysF_PTS.lib]


B

bfr_ushift [in SysF_PTS.lib]
bfr_shift [in SysF_PTS.lib]
bfr_up [in SysF_PTS.lib]


C

cm_typingL_beta [in SysF_PTS.lambda2]
cm_typingL_id [in SysF_PTS.lambda2]
cm_typingL_up [in SysF_PTS.lambda2]
cm_typingP_beta_type [in SysF_PTS.lambda2]
cm_typingP_beta_term [in SysF_PTS.lambda2]
cm_typingP_up [in SysF_PTS.lambda2]
cm_istyP_beta_term [in SysF_PTS.lambda2]
cm_istyP_beta_type [in SysF_PTS.lambda2]
cm_istyP_up [in SysF_PTS.lambda2]
cm_typingL_nat_beta [in SysF_PTS.lambda2]
cm_typingL_nat_id [in SysF_PTS.lambda2]
cm_typingL_nat_up [in SysF_PTS.lambda2]
cm_tyrel_beta [in SysF_PTS.RelEquiv]
cm_tyrel_ext [in SysF_PTS.RelEquiv]
cm_tyrel_rs [in SysF_PTS.RelEquiv]
cm_istyF_beta [in SysF_PTS.sysf]
cm_istyF_up [in SysF_PTS.sysf]
comb_comp [in SysF_PTS.lib]
comb_cons [in SysF_PTS.lib]
cr_typingP_shift [in SysF_PTS.lambda2]
cr_typingP_up [in SysF_PTS.lambda2]
cr_cm_istyP [in SysF_PTS.lambda2]
cr_istyP_ushift [in SysF_PTS.lambda2]
cr_istyP_shift [in SysF_PTS.lambda2]
cr_istyP_up_id [in SysF_PTS.lambda2]
cr_istyP_up [in SysF_PTS.lambda2]
cr_istyP_id [in SysF_PTS.lambda2]
cr_cr_istyP [in SysF_PTS.lambda2]
cr_typingL_shift [in SysF_PTS.lambda2]
cr_typingL_up [in SysF_PTS.lambda2]
cr_shift [in SysF_PTS.lib]
cr_up [in SysF_PTS.lib]
cr_typingF_shift [in SysF_PTS.sysf]
cr_typingF_ren_ushift [in SysF_PTS.sysf]
cr_typingF_ren [in SysF_PTS.sysf]
cr_typingF_up [in SysF_PTS.sysf]
cr_typingF_id [in SysF_PTS.sysf]
cr_istyF_ushift [in SysF_PTS.sysf]
cr_istyF_shift [in SysF_PTS.sysf]
cr_istyF_up [in SysF_PTS.sysf]
cr_istyF_id [in SysF_PTS.sysf]


D

decide_eq_fin_domain [in SysF_PTS.Decidable]
decide_refl [in SysF_PTS.lib]


E

eqPrp_t_subst_t [in SysF_PTS.lambda2]
eqPrp_ren [in SysF_PTS.lambda2]


G

gentypingP_typingP [in SysF_PTS.lambda2]
getD_cons [in SysF_PTS.lib]
getD_get [in SysF_PTS.lib]
getD_atnd [in SysF_PTS.lib]
get_mmap_None [in SysF_PTS.lib]
get_mmap [in SysF_PTS.lib]
get_atn [in SysF_PTS.lib]


I

internF_correct [in SysF_PTS.sysf]
internLP_correct [in SysF_PTS.lambda2]
istyF_beta [in SysF_PTS.sysf]
istyF_subst [in SysF_PTS.sysf]
istyF_strengthen [in SysF_PTS.sysf]
istyF_weaken [in SysF_PTS.sysf]
istyF_ren [in SysF_PTS.sysf]
istyP_typingL [in SysF_PTS.lambda2]
istyP_subst [in SysF_PTS.lambda2]
istyP_strengthen [in SysF_PTS.lambda2]
istyP_weaken [in SysF_PTS.lambda2]
istyP_ren [in SysF_PTS.lambda2]
istyP_neqPrp [in SysF_PTS.lambda2]
istyP_notSort [in SysF_PTS.lambda2]


M

mmap_get_None [in SysF_PTS.lib]
mmap_get [in SysF_PTS.lib]
mmap_atn [in SysF_PTS.lib]


S

sortL_add_subst [in SysF_PTS.lambda2]
sortL_p1 [in SysF_PTS.lambda2]
sortL_ren [in SysF_PTS.lambda2]
sortP_eqPrp_f [in SysF_PTS.lambda2]
sortP_neq_ren [in SysF_PTS.lambda2]
subst_coinc_hcomp [in SysF_PTS.lib]
subst_coinc_hd_f [in SysF_PTS.lib]
subst_coinc_up [in SysF_PTS.lib]
subst_coinc_id [in SysF_PTS.lib]


T

tmrel_lf_total_preserving [in SysF_PTS.RelEquiv]
tmrel_fl_total_preserving [in SysF_PTS.RelEquiv]
tmrel_injective [in SysF_PTS.RelEquiv]
tmrel_functional [in SysF_PTS.RelEquiv]
tmrel_lf_tot_pres [in SysF_PTS.RelEquiv]
tmrel_fl_tot_pres [in SysF_PTS.RelEquiv]
tmrel_inj [in SysF_PTS.RelEquiv]
tmrel_func [in SysF_PTS.RelEquiv]
typingF_weaken_ty [in SysF_PTS.sysf]
typingF_ren_ty [in SysF_PTS.sysf]
typingF_weaken [in SysF_PTS.sysf]
typingF_ren [in SysF_PTS.sysf]
typingL_typ_degenerate [in SysF_PTS.lambda2]
typingL_propagation [in SysF_PTS.lambda2]
typingL_beta [in SysF_PTS.lambda2]
typingL_subst [in SysF_PTS.lambda2]
typingL_sort_strengthen [in SysF_PTS.lambda2]
typingL_typingP [in SysF_PTS.lambda2]
typingL_typ_degenerate_nat [in SysF_PTS.lambda2]
typingL_propagation_nat [in SysF_PTS.lambda2]
typingL_beta_nat [in SysF_PTS.lambda2]
typingL_subst_nat [in SysF_PTS.lambda2]
typingL_weaken [in SysF_PTS.lambda2]
typingL_ren [in SysF_PTS.lambda2]
typingL_prp_prp_contra [in SysF_PTS.lambda2]
typingPL_equiv [in SysF_PTS.lambda2]
typingP_typingL [in SysF_PTS.lambda2]
typingP_istyP [in SysF_PTS.lambda2]
typingP_beta_type [in SysF_PTS.lambda2]
typingP_beta_term [in SysF_PTS.lambda2]
typingP_subst [in SysF_PTS.lambda2]
typingP_weaken [in SysF_PTS.lambda2]
typingP_ren [in SysF_PTS.lambda2]
tyrel_lf_total_preserving [in SysF_PTS.RelEquiv]
tyrel_fl_total_preserving [in SysF_PTS.RelEquiv]
tyrel_injective [in SysF_PTS.RelEquiv]
tyrel_functional [in SysF_PTS.RelEquiv]
tyrel_tmrel_disjoint [in SysF_PTS.RelEquiv]
tyrel_beta [in SysF_PTS.RelEquiv]
tyrel_subst [in SysF_PTS.RelEquiv]
tyrel_unmap [in SysF_PTS.RelEquiv]
tyrel_weaken_hd [in SysF_PTS.RelEquiv]
tyrel_weaken [in SysF_PTS.RelEquiv]
tyrel_ren [in SysF_PTS.RelEquiv]
tyrel_lf_tot_pres [in SysF_PTS.RelEquiv]
tyrel_fl_tot_pres [in SysF_PTS.RelEquiv]
tyrel_inj [in SysF_PTS.RelEquiv]
tyrel_func [in SysF_PTS.RelEquiv]


U

upren_comb [in SysF_PTS.lib]


V

vrm_app [in SysF_PTS.RelEquiv]
vrm_comb [in SysF_PTS.RelEquiv]
vr_tmctx_lf_ext_rs [in SysF_PTS.RelEquiv]
vr_tmctx_lf_rs_ext [in SysF_PTS.RelEquiv]
vr_tmctx_lf_nil [in SysF_PTS.RelEquiv]
vr_tmctx_fl_ext_rs [in SysF_PTS.RelEquiv]
vr_tmctx_fl_rs_ext [in SysF_PTS.RelEquiv]
vr_tmctx_fl_nil [in SysF_PTS.RelEquiv]
vr_rdis_ext_rs [in SysF_PTS.RelEquiv]
vr_rdis_rs_ext [in SysF_PTS.RelEquiv]
vr_rdis_r_nil [in SysF_PTS.RelEquiv]
vr_rdis_l_nil [in SysF_PTS.RelEquiv]
vr_rdis_sym [in SysF_PTS.RelEquiv]
vr_tyctx_lf_ext [in SysF_PTS.RelEquiv]
vr_tyctx_lf_rs [in SysF_PTS.RelEquiv]
vr_tyctx_fl_ext [in SysF_PTS.RelEquiv]
vr_tyctx_fl_rs [in SysF_PTS.RelEquiv]
vr_inj_ext [in SysF_PTS.RelEquiv]
vr_inj_rs [in SysF_PTS.RelEquiv]
vr_inj_nil [in SysF_PTS.RelEquiv]
vr_func_ext [in SysF_PTS.RelEquiv]
vr_func_rs [in SysF_PTS.RelEquiv]
vr_func_nil [in SysF_PTS.RelEquiv]
vr_right_app [in SysF_PTS.RelEquiv]
vr_left_app [in SysF_PTS.RelEquiv]
vr_app_or [in SysF_PTS.RelEquiv]
vr_unmap [in SysF_PTS.RelEquiv]
vr_map [in SysF_PTS.RelEquiv]


W

wfL_atnd_ok [in SysF_PTS.lambda2]



Constructor Index

A

AllF [in SysF_PTS.sysf]
AppF [in SysF_PTS.sysf]
AppL [in SysF_PTS.lambda2]
AtndS [in SysF_PTS.lib]
Atnd0 [in SysF_PTS.lib]
AtnS [in SysF_PTS.lib]
Atn0 [in SysF_PTS.lib]


D

decide [in SysF_PTS.Decidable]


I

ImpF [in SysF_PTS.sysf]
istyF_all [in SysF_PTS.sysf]
istyF_imp [in SysF_PTS.sysf]
istyF_var [in SysF_PTS.sysf]
istyP_prod2 [in SysF_PTS.lambda2]
istyP_prod1 [in SysF_PTS.lambda2]
istyP_var [in SysF_PTS.lambda2]


L

LamF [in SysF_PTS.sysf]
LamL [in SysF_PTS.lambda2]


P

ProdL [in SysF_PTS.lambda2]
Prp [in SysF_PTS.lambda2]


S

SortL [in SysF_PTS.lambda2]


T

tmrel_tyabs [in SysF_PTS.RelEquiv]
tmrel_tyspec [in SysF_PTS.RelEquiv]
tmrel_lam [in SysF_PTS.RelEquiv]
tmrel_app [in SysF_PTS.RelEquiv]
tmrel_var [in SysF_PTS.RelEquiv]
TmVarF [in SysF_PTS.sysf]
TyAbsF [in SysF_PTS.sysf]
Typ [in SysF_PTS.lambda2]
typingF_tyabs [in SysF_PTS.sysf]
typingF_tyspec [in SysF_PTS.sysf]
typingF_lam [in SysF_PTS.sysf]
typingF_app [in SysF_PTS.sysf]
typingF_var [in SysF_PTS.sysf]
typingL_lam [in SysF_PTS.lambda2]
typingL_app [in SysF_PTS.lambda2]
typingL_prod [in SysF_PTS.lambda2]
typingL_var [in SysF_PTS.lambda2]
typingL_ax [in SysF_PTS.lambda2]
typingP_lam2 [in SysF_PTS.lambda2]
typingP_app2 [in SysF_PTS.lambda2]
typingP_lam1 [in SysF_PTS.lambda2]
typingP_app1 [in SysF_PTS.lambda2]
typingP_var [in SysF_PTS.lambda2]
tyrel_all [in SysF_PTS.RelEquiv]
tyrel_imp [in SysF_PTS.RelEquiv]
tyrel_var [in SysF_PTS.RelEquiv]
TySpecF [in SysF_PTS.sysf]
TyVarF [in SysF_PTS.sysf]


V

VarL [in SysF_PTS.lambda2]


W

wfF_ext_tm [in SysF_PTS.sysf]
wfF_ext_ty [in SysF_PTS.sysf]
wfF_empty [in SysF_PTS.sysf]
wfL_ext [in SysF_PTS.lambda2]
wfL_empty [in SysF_PTS.lambda2]
wfP_ext_ty [in SysF_PTS.lambda2]
wfP_ext_prp [in SysF_PTS.lambda2]
wfP_empty [in SysF_PTS.lambda2]



Inductive Index

A

atn [in SysF_PTS.lib]
atnd [in SysF_PTS.lib]


D

Dec [in SysF_PTS.Decidable]


I

istyF [in SysF_PTS.sysf]
istyP [in SysF_PTS.lambda2]


L

level [in SysF_PTS.lambda2]


T

termF [in SysF_PTS.sysf]
termL [in SysF_PTS.lambda2]
tmrel [in SysF_PTS.RelEquiv]
typeF [in SysF_PTS.sysf]
typingF [in SysF_PTS.sysf]
typingL [in SysF_PTS.lambda2]
typingP [in SysF_PTS.lambda2]
tyrel [in SysF_PTS.RelEquiv]


W

wfF [in SysF_PTS.sysf]
wfL [in SysF_PTS.lambda2]
wfP [in SysF_PTS.lambda2]



Projection Index

B

bind [in SysF_PTS.lib]


C

countableProp [in SysF_PTS.Decidable]


D

decide [in SysF_PTS.Decidable]


E

enum [in SysF_PTS.Decidable]


F

finiteProp [in SysF_PTS.Decidable]
fmap [in SysF_PTS.lib]


N

numElems [in SysF_PTS.Decidable]


R

repr [in SysF_PTS.Decidable]
ret [in SysF_PTS.lib]



Instance Index

D

decidable_neg [in SysF_PTS.Decidable]
decide_eq_termL [in SysF_PTS.lambda2]
decide_eq_level [in SysF_PTS.lambda2]
decide_eq_termF [in SysF_PTS.sysf]
decide_eq_typeF [in SysF_PTS.sysf]
Dec_eq_fin_domain [in SysF_PTS.Decidable]
Dec_fin_quant [in SysF_PTS.Decidable]
Dec_fin_quant_T [in SysF_PTS.Decidable]
Dec_impl [in SysF_PTS.Decidable]
Dec_or [in SysF_PTS.Decidable]
Dec_and [in SysF_PTS.Decidable]
Dec_lt_nat [in SysF_PTS.Decidable]
Dec_le_nat [in SysF_PTS.Decidable]
Dec_eq_option [in SysF_PTS.Decidable]
Dec_eq_nat [in SysF_PTS.Decidable]


F

Functor_Monad [in SysF_PTS.lib]


H

HSubstLemmas_termF [in SysF_PTS.sysf]
HSubst_termF [in SysF_PTS.sysf]


I

Ids_termL [in SysF_PTS.lambda2]
Ids_termF [in SysF_PTS.sysf]
Ids_typeF [in SysF_PTS.sysf]


R

Rename_termL [in SysF_PTS.lambda2]
Rename_termF [in SysF_PTS.sysf]
Rename_typeF [in SysF_PTS.sysf]


S

SubstHSubstComp_typeF_termF [in SysF_PTS.sysf]
SubstLemmas_termL [in SysF_PTS.lambda2]
SubstLemmas_termF [in SysF_PTS.sysf]
SubstLemmas_typeF [in SysF_PTS.sysf]
Subst_termL [in SysF_PTS.lambda2]
Subst_termF [in SysF_PTS.sysf]
Subst_typeF [in SysF_PTS.sysf]



Section Index

C

Coincidence [in SysF_PTS.lib]
CoincidenceHSubst [in SysF_PTS.lib]
ContextRenamings [in SysF_PTS.lib]
CtxBoolFun [in SysF_PTS.lib]


S

SubstInstance [in SysF_PTS.lib]



Abbreviation Index

D

dec [in SysF_PTS.Decidable]


E

eq_dec [in SysF_PTS.Decidable]



Definition Index

B

bfr [in SysF_PTS.lib]


C

cm_typingL [in SysF_PTS.lambda2]
cm_typingP [in SysF_PTS.lambda2]
cm_istyP [in SysF_PTS.lambda2]
cm_typingL_nat [in SysF_PTS.lambda2]
cm_tyrel [in SysF_PTS.RelEquiv]
cm_istyF [in SysF_PTS.sysf]
comb [in SysF_PTS.lib]
cr [in SysF_PTS.lib]
cr_typingP [in SysF_PTS.lambda2]
cr_istyP [in SysF_PTS.lambda2]
cr_typingL [in SysF_PTS.lambda2]
cr_typingF [in SysF_PTS.sysf]
cr_istyF [in SysF_PTS.sysf]


E

eqPrp [in SysF_PTS.lambda2]


G

gentypingP [in SysF_PTS.lambda2]
get [in SysF_PTS.lib]
getD [in SysF_PTS.lib]


I

internF [in SysF_PTS.sysf]
internF_ty [in SysF_PTS.sysf]
internL [in SysF_PTS.lambda2]


S

subst_coinc [in SysF_PTS.lib]
sum2bool [in SysF_PTS.lib]


V

vr [in SysF_PTS.RelEquiv]
vrel [in SysF_PTS.RelEquiv]
vrm [in SysF_PTS.RelEquiv]
vr_tmctx_lf [in SysF_PTS.RelEquiv]
vr_tmctx_fl [in SysF_PTS.RelEquiv]
vr_rdis [in SysF_PTS.RelEquiv]
vr_tyctx_lf_nil [in SysF_PTS.RelEquiv]
vr_tyctx_lf [in SysF_PTS.RelEquiv]
vr_tyctx_fl_nil [in SysF_PTS.RelEquiv]
vr_tyctx_fl [in SysF_PTS.RelEquiv]
vr_inj [in SysF_PTS.RelEquiv]
vr_func [in SysF_PTS.RelEquiv]



Record Index

C

Countable [in SysF_PTS.Decidable]


D

Dec [in SysF_PTS.Decidable]


F

Finite [in SysF_PTS.Decidable]
Functor [in SysF_PTS.lib]


M

Monad [in SysF_PTS.lib]



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 (337 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 (6 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 (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 _ other (165 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 (57 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 (17 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 (9 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 (31 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 (5 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 (2 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 (35 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 (5 entries)