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 _ (2486 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 _ (179 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 _ (17 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 _ (4 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1252 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 _ (56 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 _ (168 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 _ (48 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 _ (14 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 _ (460 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 _ (96 entries)
Moduleid 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 _ (48 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 _ (87 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 _ (57 entries)

Global Index

A

Abs [constructor, in Lambda]
Abs [constructor, in Term]
Abs [constructor, in TermECC]
abs_par_red [constructor, in Term]
abs_par_red [constructor, in TypeJudge]
abs_par_red [constructor, in TermECC]
abs_red [constructor, in Lambda]
abs_red_l [constructor, in TermECC]
abs_red_l [constructor, in Term]
abs_red_morph [instance, in Lambda]
abs_red_r [constructor, in Term]
abs_red_r [constructor, in TermECC]
Abs_sound_Arr [lemma, in Can]
Abs_sound_Pi [lemma, in Can]
App [constructor, in Lambda]
App [constructor, in Term]
App [constructor, in TermECC]
app [definition, in HFrelation]
app [definition, in ZFrelations]
App2 [definition, in Lambda]
app_def [lemma, in HFrelation]
app_defined [lemma, in ZFrelations]
app_elim [lemma, in ZFrelations]
app_hf [definition, in HF]
app_morph [instance, in ZFrelations]
app_morph [instance, in HFrelation]
app_par_red [constructor, in TermECC]
app_par_red [constructor, in Term]
app_par_red [constructor, in TypeJudge]
app_red_l [constructor, in Term]
app_red_l [constructor, in Lambda]
app_red_l [constructor, in TermECC]
app_red_morph [instance, in Lambda]
app_red_r [constructor, in Term]
app_red_r [constructor, in TermECC]
app_red_r [constructor, in Lambda]
app_typ [lemma, in ZFrelations]
app_typ1 [lemma, in ZFrelations]
app_typ2 [lemma, in ZFrelations]
Arr [definition, in Can]


B

B [moduleid, in ModelCIC]
B [moduleid, in EnsUniv]
basic [library]
Beq [moduleid, in ModelCIC]
Beq.eq [definition, in ModelCIC]
Beq.eq_equiv [instance, in ModelCIC]
Beq.eq_equiv [definition, in ModelCIC]
Beq.t [definition, in ModelCIC]
beta [constructor, in Lambda]
beta [constructor, in TermECC]
beta [constructor, in Term]
beta_eq [lemma, in HFrelation]
beta_eq [lemma, in ZFrelations]
beta_morph [lemma, in HFcoc]
Beta_Reduction [section, in Lambda]
Beta_Reduction [section, in Term]
Beta_Reduction [section, in TermECC]
beta_rel_eq [lemma, in ZFrelations]
BOOL [definition, in ZFindtypes]
bool_elim [lemma, in ZFindtypes]
BuildModel [moduleid, in ModelZF]


C

Can [library]
cancel_repeat [lemma, in HF]
cand_sat [lemma, in Can]
cand_sn [lemma, in Can]
canonical [definition, in HF]
canonical_correct [lemma, in HF]
cantor [lemma, in ZFcard]
cantor_le [lemma, in ZFcard]
CCLam [definition, in ZFlambda]
CCM [moduleid, in ModelZF]
CCM.app [definition, in ModelZF]
CCM.app_ext [lemma, in ModelZF]
CCM.beta_eq [lemma, in ModelZF]
CCM.eqX [definition, in ModelZF]
CCM.eqX_equiv [definition, in ModelZF]
CCM.eq_fun [definition, in ModelZF]
CCM.impredicative_prod [lemma, in ModelZF]
CCM.inX [definition, in ModelZF]
CCM.in_ext [lemma, in ModelZF]
CCM.lam [definition, in ModelZF]
CCM.lam_ext [lemma, in ModelZF]
CCM.prod [definition, in ModelZF]
CCM.prod_elim [lemma, in ModelZF]
CCM.prod_ext [lemma, in ModelZF]
CCM.prod_intro [lemma, in ModelZF]
CCM.props [definition, in ModelZF]
CCM.X [definition, in ModelZF]
CCSN [moduleid, in SN_CC]
CCSN.cc_impredicative_prod_non_empty [lemma, in SN_CC]
CCSN.El [definition, in SN_CC]
CCSN.mkTY [definition, in SN_CC]
CCSN.piSAT [definition, in SN_CC]
CCSN.prop_repl_morph [lemma, in SN_CC]
CCSN.Red [definition, in SN_CC]
CCSN.sn_impredicative_prod [lemma, in SN_CC]
CCSN.sn_lam [definition, in SN_CC]
CCSN.sn_prod [definition, in SN_CC]
CCSN.sn_prod_elim [lemma, in SN_CC]
CCSN.sn_prod_intro [lemma, in SN_CC]
CCSN.sn_proof_of_false [lemma, in SN_CC]
CCSN.sn_props [definition, in SN_CC]
cc_app [definition, in HFcoc]
cc_app [definition, in ZFcoc]
cc_app_morph [instance, in ZFcoc]
cc_app_morph [instance, in HFcoc]
cc_beta_eq [lemma, in ZFcoc]
cc_beta_eq [lemma, in HFcoc]
cc_consistency [lemma, in ModelHF]
cc_consistency [lemma, in ModelZF]
cc_eta_eq [lemma, in ZFcoc]
cc_impredicative_lam [lemma, in HFcoc]
cc_impredicative_lam [lemma, in ZFcoc]
cc_impredicative_prod [lemma, in ZFcoc]
cc_impredicative_prod [lemma, in HFcoc]
cc_lam [definition, in ZFcoc]
cc_lam [definition, in HFcoc]
cc_lam_ext [lemma, in HFcoc]
cc_lam_ext [lemma, in ZFcoc]
cc_lam_fun1 [lemma, in ZFcoc]
cc_lam_fun2 [lemma, in ZFcoc]
CC_Model [moduleid, in Models]
CC_Model.app [axiom, in Models]
CC_Model.app_ext [axiom, in Models]
CC_Model.app_ext [instance, in Models]
CC_Model.beta_eq [axiom, in Models]
CC_Model.eqX [axiom, in Models]
CC_Model.eqX_equiv [axiom, in Models]
CC_Model.eqX_equiv [instance, in Models]
CC_Model.eq_fun [definition, in Models]
CC_Model.impredicative_prod [axiom, in Models]
CC_Model.inX [axiom, in Models]
CC_Model.in_ext [axiom, in Models]
CC_Model.in_ext [instance, in Models]
CC_Model.lam [axiom, in Models]
CC_Model.lam_ext [axiom, in Models]
CC_Model.prod [axiom, in Models]
CC_Model.prod_elim [axiom, in Models]
CC_Model.prod_ext [axiom, in Models]
CC_Model.prod_intro [axiom, in Models]
CC_Model.props [axiom, in Models]
CC_Model.X [axiom, in Models]
cc_prod [definition, in ZFcoc]
cc_prod [definition, in HFcoc]
cc_prod_covariant [lemma, in ZFcoc]
cc_prod_elim [lemma, in ZFcoc]
cc_prod_elim [lemma, in HFcoc]
cc_prod_ext [lemma, in HFcoc]
cc_prod_ext [lemma, in ZFcoc]
cc_prod_fun1 [lemma, in ZFcoc]
cc_prod_intro [lemma, in HFcoc]
cc_prod_intro [lemma, in ZFcoc]
cc_prod_univ [lemma, in ZFecc]
choice [axiom, in Choice]
Choice [library]
choose_elt [lemma, in HF]
Church_Rosser [section, in Conv]
church_rosser [lemma, in Lambda]
church_rosser [lemma, in Conv]
Church_Rosser [section, in ConvECC]
church_rosser [lemma, in TypeJudge]
church_rosser [lemma, in ConvECC]
ClassicOrdinal [moduleid, in ZFordcl]
ClassicOrdinal.EM [axiom, in ZFordcl]
ClassicOrdinal.ord_incl_le [lemma, in ZFordcl]
ClassicOrdinal.ord_total [lemma, in ZFordcl]
clos_exp [projection, in Can]
clos_red [projection, in Can]
clos_trans_transp [lemma, in SN_CC]
commut_lift_subst [lemma, in Term]
commut_lift_subst [lemma, in TermECC]
commut_lift_subst [lemma, in Lambda]
commut_lift_subst_rec [lemma, in Lambda]
commut_lift_subst_rec [lemma, in Term]
commut_lift_subst_rec [lemma, in TermECC]
commut_red1_subterm [lemma, in TermECC]
commut_red1_subterm [lemma, in Term]
commut_red1_subterm [lemma, in Lambda]
compl [definition, in Can]
Completion [section, in Can]
Completion.P [variable, in Can]
complSAT [definition, in ZFlambda]
compl_elim [lemma, in Can]
compl_intro [lemma, in Can]
confluence [lemma, in Lambda]
confluence [lemma, in TypeJudge]
confluence_par_red [lemma, in ConvECC]
confluence_par_red [lemma, in Conv]
confluence_red [lemma, in Conv]
confluence_red [lemma, in ConvECC]
cons_hf [definition, in HF]
cons_hf_cons [lemma, in HF]
cons_map [definition, in IntMap]
cons_map_ext [lemma, in IntMap]
conv [inductive, in TermECC]
conv [inductive, in Lambda]
conv [inductive, in Term]
Conv [library]
ConvECC [library]
conv_conv_lift [lemma, in Lambda]
conv_conv_lift [lemma, in Term]
conv_conv_lift [lemma, in TermECC]
conv_conv_prod [lemma, in Term]
conv_conv_prod [lemma, in TermECC]
conv_conv_subst [lemma, in Lambda]
conv_conv_subst [lemma, in Term]
conv_conv_subst [lemma, in TermECC]
conv_kind_prop [lemma, in ConvECC]
conv_kind_prop [lemma, in Conv]
conv_refl [instance, in Lambda]
conv_sort [lemma, in ConvECC]
conv_sort [lemma, in Conv]
conv_sort_prod [lemma, in ConvECC]
conv_sort_prod [lemma, in Conv]
couple [definition, in HF]
couple [definition, in ZFpairs]
couple_injection [lemma, in ZFpairs]
couple_intro [lemma, in ZFpairs]
couple_intro_sigma [lemma, in ZFpairs]
couple_morph [instance, in ZFpairs]
couple_morph [instance, in HF]
CR [definition, in Can]
cst_cont [lemma, in ZFindtypes]
cst_is_ext [lemma, in ZFindtypes]
cumul_Prop [lemma, in ModelCIC]
cumul_Type [lemma, in ModelCIC]


D

del_cons_map [lemma, in IntMap]
del_cons_map2 [lemma, in IntMap]
del_map [definition, in IntMap]
dep_func [definition, in ZFrelations]
dep_func [definition, in HFrelation]
dep_func_elim [lemma, in ZFrelations]
dep_func_elim [lemma, in HFrelation]
dep_func_elim0 [lemma, in HFrelation]
dep_func_eta [lemma, in HFrelation]
dep_func_eta [lemma, in ZFrelations]
dep_func_ext [lemma, in ZFrelations]
dep_func_ext [lemma, in HFrelation]
dep_func_incl_func [lemma, in ZFrelations]
dep_func_intro [lemma, in HFrelation]
dep_func_intro [lemma, in ZFrelations]
dep_func_total [lemma, in HFrelation]
dep_image [definition, in ZFrelations]
dep_image_ext [lemma, in ZFrelations]
df_morph1 [lemma, in HFrelation]
df_morph2 [lemma, in HFrelation]
discr [lemma, in ZFnats]
discr_lim_succ [lemma, in ZFordcl]
discr_lim_succ [lemma, in ZFord]
discr_power [lemma, in ZFcard]
discr_sum [lemma, in ZFsum]
distr_lift_subst [lemma, in Term]
distr_lift_subst [lemma, in TermECC]
distr_lift_subst [lemma, in Lambda]
distr_lift_subst_rec [lemma, in TermECC]
distr_lift_subst_rec [lemma, in Lambda]
distr_lift_subst_rec [lemma, in Term]
distr_subst [lemma, in Term]
distr_subst [lemma, in Lambda]
distr_subst [lemma, in TermECC]
distr_subst_rec [lemma, in Term]
distr_subst_rec [lemma, in TermECC]
distr_subst_rec [lemma, in Lambda]
domain [definition, in HFrelation]
domain_morph [instance, in HFrelation]
down_eq [lemma, in EnsUniv]
down_in [lemma, in EnsUniv]


E

ecc [definition, in ZFecc]
ECC [moduleid, in ModelECC]
ECC.CC [moduleid, in ModelECC]
ECC.u_card [definition, in ModelECC]
ECC.u_card_incl [lemma, in ModelECC]
ECC.u_card_in1 [lemma, in ModelECC]
ECC.u_card_in2 [lemma, in ModelECC]
ECC.u_card_prod [lemma, in ModelECC]
ECC.u_card_prod2 [lemma, in ModelECC]
ecc_grot [lemma, in ZFecc]
ecc_incl [lemma, in ZFecc]
ecc_in1 [lemma, in ZFecc]
ecc_in2 [lemma, in ZFecc]
ECC_Model [moduleid, in Models]
ECC_Model.CC [moduleid, in Models]
ECC_Model.u_card [axiom, in Models]
ECC_Model.u_card_incl [axiom, in Models]
ECC_Model.u_card_in1 [axiom, in Models]
ECC_Model.u_card_in2 [axiom, in Models]
ECC_Model.u_card_prod [axiom, in Models]
ECC_Model.u_card_prod2 [axiom, in Models]
ecc_prod [definition, in TypeECC]
ecc_prod [lemma, in ZFecc]
ecc_prod2 [lemma, in ZFecc]
ecc_prod_fun [axiom, in TypeECC]
EM [definition, in ModelZF]
empty [definition, in HF]
EMPTY [abbreviation, in HF]
empty_elim [lemma, in HF]
empty_ext [lemma, in ZF]
empty_ext [lemma, in HF]
empty_in_power [lemma, in ZF]
Ens [library]
EnsUniv [library]
Ens0 [library]
env [definition, in EnvECC]
env [definition, in Env]
Env [library]
EnvECC [library]
epsilon0 [definition, in ZFordcl]
epsilon0 [definition, in ZFord]
EQ [definition, in ModelZF]
eqSAT_equiv [instance, in Sat]
eqterm [lemma, in Term]
eqterm [lemma, in Lambda]
eqterm_subst_App [lemma, in ModelCIC]
equi_card [definition, in ZFcard]
equi_card_le [lemma, in ZFcard]
equi_card_morph [instance, in ZFcard]
equi_card_refl [instance, in ZFcard]
equi_card_sym [instance, in ZFcard]
equi_card_trans [instance, in ZFcard]
Eqv [moduleid, in VarMap]
Eqv.eq [axiom, in VarMap]
Eqv.eq_equiv [axiom, in VarMap]
Eqv.eq_equiv [instance, in VarMap]
Eqv.t [axiom, in VarMap]
eq_cand [definition, in Can]
eq_cand_incl [lemma, in Can]
eq_can_Arr [lemma, in Can]
eq_can_compl [lemma, in Can]
eq_can_Inter [lemma, in Can]
eq_can_Pi [lemma, in Can]
eq_can_union [lemma, in Can]
eq_conv [definition, in TypeJudge]
eq_conv_abs [lemma, in TypeJudge]
eq_conv_abs_l [lemma, in TypeJudge]
eq_conv_abs_r [lemma, in TypeJudge]
eq_conv_app [lemma, in TypeJudge]
eq_conv_app_l [lemma, in TypeJudge]
eq_conv_app_m [lemma, in TypeJudge]
eq_conv_app_r [lemma, in TypeJudge]
eq_conv_conv [lemma, in TypeJudge]
eq_conv_exp [lemma, in TypeJudge]
eq_conv_inv [lemma, in TypeJudge]
eq_conv_inv2 [lemma, in TypeJudge]
eq_conv_lift [lemma, in TypeJudge]
eq_conv_prod [lemma, in TypeJudge]
eq_conv_prod_l [lemma, in TypeJudge]
eq_conv_prod_r [lemma, in TypeJudge]
eq_conv_red [lemma, in TypeJudge]
eq_conv_red_env [lemma, in TypeJudge]
eq_conv_refl [lemma, in TypeJudge]
eq_conv_sort_trans [lemma, in TypeJudge]
eq_conv_subst_r [lemma, in TypeJudge]
eq_conv_subst_ty_l [lemma, in TypeJudge]
eq_conv_sym [lemma, in TypeJudge]
eq_conv_trans [lemma, in TypeJudge]
eq_elim [lemma, in ZF]
eq_fun [definition, in ZF]
eq_fun_ext [lemma, in ZF]
eq_fun_sym [instance, in ZF]
eq_fun_trans [instance, in ZF]
Eq_hf [definition, in HF]
eq_hf [definition, in HF]
Eq_hf_cons [lemma, in HF]
Eq_hf_cons_hf [lemma, in HF]
eq_hf_elim1 [lemma, in HF]
eq_hf_elim2 [lemma, in HF]
eq_hf_equiv [instance, in HF]
eq_hf_fun [definition, in HF]
eq_hf_fun_left [lemma, in HF]
eq_hf_fun_sym [lemma, in HF]
eq_hf_fun_trans [lemma, in HF]
Eq_hf_intro [lemma, in HF]
eq_hf_intro [lemma, in HF]
eq_hf_morph [instance, in HF]
eq_hf_pred [definition, in HF]
eq_hf_refl [instance, in HF]
Eq_hf_split [lemma, in HF]
eq_hf_sym [instance, in HF]
eq_hf_trans [instance, in HF]
eq_index [definition, in ZF]
eq_index_eq [lemma, in ZF]
eq_index_sym [lemma, in ZF]
eq_intro [lemma, in ZF]
eq_map [definition, in IntMap]
eq_pred [definition, in ZF]
eq_pred_set [instance, in ZF]
eq_red [definition, in TypeJudge]
eq_red_conv [lemma, in TypeJudge]
eq_red_inv [lemma, in TypeJudge]
eq_red_inv2 [lemma, in TypeJudge]
eq_set_equiv [instance, in ZF]
eq_typ [inductive, in TypeJudge]
eq_typ [inductive, in TypeJudgeECC]
eq_typ_eq [definition, in TypeJudgeECC]
eq_typ_eq_exp [lemma, in TypeJudgeECC]
eq_typ_eq_red [lemma, in TypeJudgeECC]
eq_typ_not_kind [lemma, in TypeJudge]
eq_typ_par_red0 [lemma, in TypeJudge]
eq_typ_red_env_unmark [lemma, in TypeJudge]
eq_typ_typ [lemma, in TypeJudge]
eq_typ_uniqueness [lemma, in TypeJudge]
Example [section, in ModelCIC]
exists_elt [definition, in HF]
exists_elt_true_elim [lemma, in HF]
exists_elt_true_intro [lemma, in HF]
exp_sort_mem [lemma, in Term]
EXT [definition, in ModelZF]
extends_app [axiom, in ModelCIC]
ext_fun [definition, in ZF]
ext_fun [definition, in HFcoc]
ext_fun_ty [lemma, in ModelCIC]
ext_rel [definition, in ZF]
ex2_mono [instance, in basic]
ex2_morph [instance, in basic]
ex_mono [instance, in basic]
ex_morph [instance, in basic]


F

FALSE [definition, in ZFindtypes]
FALSE [definition, in ModelZF]
false_typ [lemma, in ZFindtypes]
fa_mono [lemma, in basic]
fa_morph [lemma, in basic]
fextends [axiom, in ModelCIC]
fext_intro [axiom, in ModelCIC]
fext_lam [lemma, in ModelCIC]
fext_morph [axiom, in ModelCIC]
fext_morph [instance, in ModelCIC]
fext_trans [lemma, in ModelCIC]
fincreasing_bounded [definition, in ModelCIC]
Fmono_morph [instance, in ZFfix]
fold_set [definition, in HF]
fold_set_ind [lemma, in HF]
fold_set_unfold [lemma, in HF]
forall_elt [definition, in HF]
forall_elt_case [lemma, in HF]
forall_elt_false_elim [lemma, in HF]
forall_elt_false_intro [lemma, in HF]
forall_elt_true_elim [lemma, in HF]
forall_elt_true_intro [lemma, in HF]
forall_int_env [definition, in ModelHF]
fst [definition, in HF]
fst [definition, in ZFpairs]
fst_def [lemma, in ZFpairs]
fst_def [lemma, in HF]
fst_morph [instance, in HF]
fst_morph [instance, in ZFpairs]
fst_typ [lemma, in ZFpairs]
fst_typ_sigma [lemma, in ZFpairs]
func [definition, in ZFrelations]
func [definition, in HFrelation]
func_cons [definition, in HFrelation]
func_cons_morph [instance, in HFrelation]
func_cont [lemma, in ZFindtypes]
func_eta [lemma, in ZFrelations]
func_is_ext [lemma, in ZFindtypes]
func_is_function [lemma, in ZFrelations]
func_map_image [definition, in HFrelation]
func_map_image_elim [lemma, in HFrelation]
func_map_image_intro [lemma, in HFrelation]
func_mono [instance, in ZFrelations]
func_morph [instance, in ZFrelations]
func_narrow [lemma, in ZFrelations]
func_rel_incl [lemma, in ZFrelations]
fun_domain_func [lemma, in ZFrelations]
fun_elt_is_ext [lemma, in ZFrelations]
fun_item [lemma, in MyList]
fx_abs [lemma, in ModelCIC]
fx_equals [definition, in ModelCIC]
fx_eq_app [lemma, in ModelCIC]
fx_eq_noc [lemma, in ModelCIC]
fx_eq_rec_call [lemma, in ModelCIC]
fx_extends [definition, in ModelCIC]
fx_sub [definition, in ModelCIC]


G

G [definition, in ZFord]
G [definition, in ZFfixfuntyp]
G [definition, in ZFordcl]
GenModel [library]
GenModelSN [library]
GenModelSyntax [library]
Gmorph [lemma, in ZFord]
Gmorph [lemma, in ZFfixfuntyp]
Gmorph [lemma, in ZFordcl]
gr [axiom, in ZFecc]
grothendieck [definition, in ZFgrothendieck]
GrothendieckUniverse [section, in ZFgrothendieck]
GrothendieckUniverse.grot [variable, in ZFgrothendieck]
GrothendieckUniverse.U [variable, in ZFgrothendieck]
grot_empty [lemma, in ZFgrothendieck]
grot_inter [lemma, in ZFgrothendieck]
grot_intersection [lemma, in ZFgrothendieck]
grot_inter_unique [lemma, in ZFgrothendieck]
grot_succ [definition, in ZFgrothendieck]
grot_succ_in [lemma, in ZFgrothendieck]
grot_succ_pred [definition, in ZFgrothendieck]
grot_succ_typ [lemma, in ZFgrothendieck]
grot_univ [record, in EnsUniv]
grot_univ [record, in ZFgrothendieck]
grot_univ_ext [lemma, in ZFgrothendieck]
G_couple [lemma, in ZFgrothendieck]
G_dep_func [lemma, in ZFgrothendieck]
G_func [lemma, in ZFgrothendieck]
G_pair [projection, in EnsUniv]
G_pair [projection, in ZFgrothendieck]
G_power [projection, in ZFgrothendieck]
G_power [projection, in EnsUniv]
G_prodcart [lemma, in ZFgrothendieck]
G_rel [lemma, in ZFgrothendieck]
G_repl [lemma, in ZFgrothendieck]
G_replf [lemma, in ZFgrothendieck]
G_singl [lemma, in ZFgrothendieck]
G_subset [lemma, in ZFgrothendieck]
G_trans [projection, in ZFgrothendieck]
G_trans [projection, in EnsUniv]
G_union [lemma, in ZFgrothendieck]
G_union2 [lemma, in ZFgrothendieck]
G_union_repl [projection, in ZFgrothendieck]
G_union_repl [projection, in EnsUniv]


H

has_fin_limit [lemma, in ZFindtypes]
hf [inductive, in HF]
HF [constructor, in HF]
HF [library]
HFcoc [library]
HFrelation [library]
hf_bool [definition, in HF]
HF_Coc_Model [moduleid, in ModelHF]
HF_Coc_Model.app [definition, in ModelHF]
HF_Coc_Model.app_ext [lemma, in ModelHF]
HF_Coc_Model.beta_eq [lemma, in ModelHF]
HF_Coc_Model.eqX [definition, in ModelHF]
HF_Coc_Model.eqX_equiv [definition, in ModelHF]
HF_Coc_Model.eq_fun [definition, in ModelHF]
HF_Coc_Model.impredicative_prod [lemma, in ModelHF]
HF_Coc_Model.inX [definition, in ModelHF]
HF_Coc_Model.in_ext [lemma, in ModelHF]
HF_Coc_Model.lam [definition, in ModelHF]
HF_Coc_Model.lam_ext [lemma, in ModelHF]
HF_Coc_Model.prod [definition, in ModelHF]
HF_Coc_Model.prod_elim [lemma, in ModelHF]
HF_Coc_Model.prod_ext [lemma, in ModelHF]
HF_Coc_Model.prod_intro [lemma, in ModelHF]
HF_Coc_Model.props [definition, in ModelHF]
HF_Coc_Model.X [definition, in ModelHF]
hf_elts [definition, in HF]
hf_elts_ext [lemma, in HF]
hf_false [definition, in HF]
hf_ind2 [lemma, in HF]
hf_pred_morph [definition, in HF]
hf_size_ind [lemma, in HF]
hf_true [definition, in HF]


I

iff_impl [lemma, in basic]
iff_morph [lemma, in basic]
iLAM [definition, in ZFlambda]
iLAM_inj [lemma, in ZFlambda]
iLAM_typ [lemma, in ZFlambda]
image [definition, in HFrelation]
image_morph [instance, in HFrelation]
Inaccessible [section, in ZFfix]
InaccessibleCard [section, in ZFfix]
InaccessibleCard.mu [variable, in ZFfix]
InaccessibleCard.mu_card [variable, in ZFfix]
InaccessibleCard.mu_lim [variable, in ZFfix]
InaccessibleCard.mu_regular [variable, in ZFfix]
Inaccessible.mu [variable, in ZFfix]
Inaccessible.mu_lim [variable, in ZFfix]
Inaccessible.mu_ord [variable, in ZFfix]
Inaccessible.mu_regular [variable, in ZFfix]
INAT [definition, in ModelZF]
incl_eq [lemma, in ZF]
Incl_hf [definition, in HF]
incl_hf [definition, in HF]
incl_hf_complete [lemma, in HF]
incl_hf_morph [instance, in HF]
incl_hf_sound [lemma, in HF]
incl_le_card [lemma, in ZFcard]
incl_set [definition, in ZF]
incl_set_morph [instance, in ZF]
incl_set_pre [instance, in ZF]
incl_sn [projection, in Can]
increasing [definition, in ZFord]
increasing [definition, in ZFordcl]
increasing_bounded [definition, in ZFord]
increasing_le [lemma, in ZFordcl]
indexed_relation [definition, in Sat]
inject_rel [definition, in ZFrelations]
inject_rel_elim [lemma, in ZFrelations]
inject_rel_intro [lemma, in ZFrelations]
inject_rel_is_rel [lemma, in ZFrelations]
injU [definition, in EnsUniv]
injU_elim [lemma, in EnsUniv]
inl [definition, in ZFsum]
inl_inj [lemma, in ZFsum]
inl_morph [instance, in ZFsum]
inl_typ [lemma, in ZFsum]
inr [definition, in ZFsum]
inr_inj [lemma, in ZFsum]
inr_morph [instance, in ZFsum]
inr_typ [lemma, in ZFsum]
insert [inductive, in MyList]
insert_hd [constructor, in MyList]
insert_tl [constructor, in MyList]
ins_cons_map [lemma, in IntMap]
ins_eq [lemma, in MyList]
ins_gt [lemma, in MyList]
ins_in_env [inductive, in Env]
ins_in_env [inductive, in EnvECC]
ins_item_ge [lemma, in Env]
ins_item_ge [lemma, in EnvECC]
ins_item_lift_ge [lemma, in EnvECC]
ins_item_lift_ge [lemma, in Env]
ins_item_lift_lt [lemma, in Env]
ins_item_lift_lt [lemma, in EnvECC]
ins_item_lt [lemma, in EnvECC]
ins_item_lt [lemma, in Env]
ins_le [lemma, in MyList]
ins_map [definition, in IntMap]
ins_O [constructor, in EnvECC]
ins_O [constructor, in Env]
ins_S [constructor, in EnvECC]
ins_S [constructor, in Env]
inter [definition, in ZF]
Inter [definition, in Can]
interp [definition, in SN_CC]
interp_sound [lemma, in SN_CC]
interp_wf [lemma, in SN_CC]
interSAT_ax [lemma, in ZFlambda]
interSAT_morph_subset [lemma, in Sat]
inter_elim [lemma, in ZF]
inter_empty_eq [lemma, in ZF]
inter_ext [lemma, in ZF]
inter_intro [lemma, in ZF]
inter_morph [instance, in ZF]
IntMap [library]
int_clos [definition, in ModelHF]
int_env [definition, in SN_CC]
int_lift [lemma, in SN_CC]
int_lift_rec [lemma, in SN_CC]
int_not_kind [lemma, in SN_CC]
int_sound [lemma, in SN_CC]
int_subst [lemma, in SN_CC]
int_subst_rec [lemma, in SN_CC]
int_trm [definition, in SN_CC]
inv_conv_prod_l [lemma, in Conv]
inv_conv_prod_l [lemma, in ConvECC]
inv_conv_prod_r [lemma, in ConvECC]
inv_conv_prod_r [lemma, in Conv]
inv_lift_sort [lemma, in Term]
inv_lift_sort [lemma, in TermECC]
inv_nth_cs [lemma, in MyList]
inv_nth_nl [lemma, in MyList]
inv_par_red_abs [lemma, in Term]
inv_par_red_abs [lemma, in TermECC]
inv_prod_l [lemma, in TypeJudge]
inv_prod_r [lemma, in TypeJudge]
inv_subst_sort [lemma, in TermECC]
inv_subst_sort [lemma, in Term]
inv_type [definition, in TypeECC]
inv_type [definition, in TypeJudgeECC]
inv_type [definition, in TypeJudge]
inv_type [definition, in Types]
inv_type_conv [lemma, in TypeJudge]
inv_type_conv [lemma, in Types]
inv_type_conv [lemma, in TypeJudgeECC]
inv_type_conv [lemma, in TypeECC]
inv_typ_abs [lemma, in Types]
inv_typ_abs [lemma, in TypeECC]
inv_typ_app [lemma, in Types]
inv_typ_app [lemma, in TypeECC]
inv_typ_conv_kind [lemma, in Types]
inv_typ_kind [lemma, in Types]
inv_typ_kind [lemma, in TypeECC]
inv_typ_prod [lemma, in TypeECC]
inv_typ_prod [lemma, in Types]
inv_typ_prop [lemma, in Types]
inv_typ_prop [lemma, in TypeECC]
inv_typ_ref [lemma, in Types]
inv_typ_ref [lemma, in TypeECC]
In_app_elim [lemma, in HF]
In_app_hf_elim [lemma, in HF]
In_app_hf_left [lemma, in HF]
In_app_hf_right [lemma, in HF]
In_app_left [lemma, in HF]
In_app_right [lemma, in HF]
in_hf [definition, in HF]
In_hf [definition, in HF]
in_hf_elim [lemma, in HF]
In_hf_elim [lemma, in HF]
In_hf_elim_hf [lemma, in HF]
In_hf_head [lemma, in HF]
In_hf_head_hf [lemma, in HF]
in_hf_intro [lemma, in HF]
In_hf_morph [instance, in HF]
in_hf_morph [instance, in HF]
in_hf_reg_l [lemma, in HF]
in_hf_reg_r [lemma, in HF]
In_hf_tail [lemma, in HF]
In_hf_tail_hf [lemma, in HF]
in_map_inv [lemma, in HF]
in_set_morph [instance, in ZF]
iSAT [definition, in ZFlambda]
iSAT_id [lemma, in ZFlambda]
iSAT_morph [instance, in ZFlambda]
isCard [definition, in ZFcard]
isOrd [definition, in ZFord]
isOrd [definition, in ZFord3]
isOrd [definition, in ZFordcl]
isOrd_elim [lemma, in ZFord3]
isOrd_elim [lemma, in ZFordcl]
isOrd_epsilon0 [lemma, in ZFord]
isOrd_epsilon0 [lemma, in ZFordcl]
isOrd_eq [lemma, in ZFord]
isOrd_eq [lemma, in ZFordcl]
isOrd_equiv [lemma, in ZFord_equiv]
isOrd_eqv1 [lemma, in ZFord_equiv]
isOrd_ext [lemma, in ZFord]
isOrd_ext [lemma, in ZFordcl]
isOrd_ext [lemma, in ZFord3]
isOrd_ind [lemma, in ZFordcl]
isOrd_ind [lemma, in ZFord3]
isOrd_ind [lemma, in ZFord]
isOrd_intro [lemma, in ZFordcl]
isOrd_intro [lemma, in ZFord]
isOrd_intro0 [lemma, in ZFord3]
isOrd_inv [lemma, in ZFord3]
isOrd_inv [lemma, in ZFordcl]
isOrd_inv [lemma, in ZFord]
isOrd_iter_w [lemma, in ZFord]
isOrd_iter_w [lemma, in ZFordcl]
isOrd_le [lemma, in ZFordcl]
isOrd_morph [instance, in ZFord]
isOrd_morph [instance, in ZFordcl]
isOrd_morph [instance, in ZFord3]
isOrd_N [lemma, in ZFordcl]
isOrd_omega [lemma, in ZFord]
isOrd_plump [lemma, in ZFord3]
isOrd_plump [lemma, in ZFord]
isOrd_succ [lemma, in ZFord]
isOrd_succ [lemma, in ZFordcl]
isOrd_sup [lemma, in ZFordcl]
isOrd_sup [lemma, in ZFord]
isOrd_supf [lemma, in ZFord]
isOrd_supf_elim [lemma, in ZFord]
isOrd_supf_intro [lemma, in ZFord]
isOrd_sup_elim [lemma, in ZFord]
isOrd_sup_elim [lemma, in ZFordcl]
isOrd_sup_intro [lemma, in ZFord]
isOrd_sup_intro [lemma, in ZFordcl]
isOrd_sup_rel [lemma, in ZFord]
isOrd_sup_rel [lemma, in ZFordcl]
isOrd_sup_rel_elim [lemma, in ZFordcl]
isOrd_sup_rel_elim [lemma, in ZFord]
isOrd_sup_rel_intro [lemma, in ZFord]
isOrd_sup_rel_intro [lemma, in ZFordcl]
isOrd_sup_rel_intro2 [lemma, in ZFordcl]
isOrd_sup_rel_intro2 [lemma, in ZFord]
isOrd_trans [lemma, in ZFordcl]
isOrd_trans [lemma, in ZFord3]
isOrd_trans [lemma, in ZFord]
isOrd_zero [lemma, in ZFord]
isOrd_zero [lemma, in ZFordcl]
isPOrd [definition, in ZFord2]
isPOrd_morph [instance, in ZFord2]
isPOrd_succ [lemma, in ZFord2]
isPOrd_zero [lemma, in ZFord2]
isWf [definition, in ZFwf]
isWf_antirefl [lemma, in ZFwf]
isWf_ext [lemma, in ZFwf]
isWf_ind [lemma, in ZFwf]
isWf_intro [lemma, in ZFwf]
isWf_inv [lemma, in ZFwf]
isWf_N [lemma, in ZFwf]
isWf_pair [lemma, in ZFwf]
isWf_power [lemma, in ZFwf]
isWf_repl [lemma, in ZFwf]
isWf_subset [lemma, in ZFwf]
isWf_succ [lemma, in ZFwf]
isWf_union [lemma, in ZFwf]
isWf_zero [lemma, in ZFwf]
is_cand [record, in Can]
is_cand_Arr [lemma, in Can]
is_cand_Pi [lemma, in Can]
is_cand_union [lemma, in Can]
is_cand_union1 [lemma, in Can]
is_cand_union2 [lemma, in Can]
is_can_compl [lemma, in Can]
is_can_Inter [lemma, in Can]
is_function [definition, in ZFrelations]
is_nat [definition, in ZFnats]
is_nat_succ [lemma, in ZFnats]
is_nat_zero [lemma, in ZFnats]
is_relation [definition, in ZFrelations]
item [inductive, in MyList]
item_hd [constructor, in MyList]
item_lift [definition, in Env]
item_lift [definition, in EnvECC]
item_lift_fun [lemma, in Env]
item_tl [constructor, in MyList]
item_trunc [lemma, in MyList]
IterMonotone [section, in ZFfix]
IterMonotone [section, in ZFfixfuntyp]
IterMonotone.F [variable, in ZFfix]
IterMonotone.F [variable, in ZFfixfuntyp]
IterMonotone.Fmono [variable, in ZFfix]
IterMonotone.Fmono [variable, in ZFfixfuntyp]
IterMonotone.Fmorph [variable, in ZFfixfuntyp]
iter_w [definition, in ZFordcl]
iter_w [definition, in ZFord]
IZF [moduleid, in Ens0]
IZF [moduleid, in Ens]
IZF [moduleid, in ZF]
IZF.choice' [lemma, in Ens]
IZF.choice' [lemma, in Ens0]
IZF.elts [definition, in Ens]
IZF.elts [definition, in Ens0]
IZF.elts' [definition, in Ens]
IZF.elts' [definition, in Ens0]
IZF.empty [definition, in Ens]
IZF.empty [definition, in Ens0]
IZF.empty_ax [lemma, in Ens0]
IZF.empty_ax [lemma, in Ens]
IZF.empty_ex [lemma, in Ens]
IZF.empty_ex [lemma, in Ens0]
IZF.eq_elim [lemma, in Ens]
IZF.eq_elim [lemma, in Ens0]
IZF.eq_elim0 [lemma, in Ens]
IZF.eq_elim0 [lemma, in Ens0]
IZF.eq_intro [lemma, in Ens0]
IZF.eq_intro [lemma, in Ens]
IZF.eq_set [definition, in Ens0]
IZF.eq_set [definition, in Ens]
IZF.eq_set_ax [lemma, in Ens]
IZF.eq_set_ax [lemma, in Ens0]
IZF.eq_set_def [lemma, in Ens]
IZF.eq_set_def [lemma, in Ens0]
IZF.eq_set_refl [lemma, in Ens]
IZF.eq_set_refl [lemma, in Ens0]
IZF.eq_set_sym [lemma, in Ens0]
IZF.eq_set_sym [lemma, in Ens]
IZF.eq_set_trans [lemma, in Ens]
IZF.eq_set_trans [lemma, in Ens0]
IZF.idx [definition, in Ens0]
IZF.idx [definition, in Ens]
IZF.infinity [definition, in Ens0]
IZF.infinity [definition, in Ens]
IZF.infinity_ex [lemma, in Ens0]
IZF.infinity_ex [lemma, in Ens]
IZF.infty_ax1 [lemma, in Ens0]
IZF.infty_ax1 [lemma, in Ens]
IZF.infty_ax2 [lemma, in Ens0]
IZF.infty_ax2 [lemma, in Ens]
IZF.in_reg [lemma, in Ens]
IZF.in_reg [lemma, in Ens0]
IZF.in_set [definition, in Ens]
IZF.in_set [definition, in Ens0]
IZF.num [definition, in Ens0]
IZF.num [definition, in Ens]
IZF.pair [definition, in Ens0]
IZF.pair [definition, in Ens]
IZF.pair_ax [lemma, in Ens]
IZF.pair_ax [lemma, in Ens0]
IZF.pair_ex [lemma, in Ens0]
IZF.pair_ex [lemma, in Ens]
IZF.pair_morph [lemma, in Ens]
IZF.pair_morph [lemma, in Ens0]
IZF.power [definition, in Ens0]
IZF.power [definition, in Ens]
IZF.power_ax [lemma, in Ens]
IZF.power_ax [lemma, in Ens0]
IZF.power_ex [lemma, in Ens0]
IZF.power_ex [lemma, in Ens]
IZF.power_morph [lemma, in Ens0]
IZF.power_morph [lemma, in Ens]
IZF.regularity_ax [lemma, in Ens]
IZF.regularity_ax [lemma, in Ens0]
IZF.repl0 [definition, in Ens]
IZF.repl0 [definition, in Ens0]
IZF.repl0_ax [lemma, in Ens0]
IZF.repl0_ax [lemma, in Ens]
IZF.repl1 [definition, in Ens0]
IZF.repl1 [definition, in Ens]
IZF.repl1_ax [lemma, in Ens]
IZF.repl1_ax [lemma, in Ens0]
IZF.repl1_morph [lemma, in Ens0]
IZF.repl1_morph [lemma, in Ens]
IZF.repl_ax [lemma, in Ens0]
IZF.repl_ax [lemma, in Ens]
IZF.repl_ex [lemma, in Ens0]
IZF.repl_ex [lemma, in Ens]
IZF.set [definition, in Ens0]
IZF.set [definition, in Ens]
IZF.set_ [inductive, in Ens0]
IZF.set_ [inductive, in Ens]
IZF.subset [definition, in Ens]
IZF.subset [definition, in Ens0]
IZF.subset_ax [lemma, in Ens0]
IZF.subset_ax [lemma, in Ens]
IZF.sup [constructor, in Ens0]
IZF.sup [constructor, in Ens]
IZF.union [definition, in Ens0]
IZF.union [definition, in Ens]
IZF.union_ax [lemma, in Ens]
IZF.union_ax [lemma, in Ens0]
IZF.union_ex [lemma, in Ens0]
IZF.union_ex [lemma, in Ens]
IZF.union_morph [lemma, in Ens0]
IZF.union_morph [lemma, in Ens]
IZF_Ex_sig [moduleid, in ZFdef]
IZF_Ex_sig.empty_ex [axiom, in ZFdef]
IZF_Ex_sig.eq_set [axiom, in ZFdef]
IZF_Ex_sig.eq_set_ax [axiom, in ZFdef]
IZF_Ex_sig.infinity_ex [axiom, in ZFdef]
IZF_Ex_sig.in_reg [axiom, in ZFdef]
IZF_Ex_sig.in_set [axiom, in ZFdef]
IZF_Ex_sig.pair_ex [axiom, in ZFdef]
IZF_Ex_sig.power_ex [axiom, in ZFdef]
IZF_Ex_sig.regularity_ax [axiom, in ZFdef]
IZF_Ex_sig.repl_ex [axiom, in ZFdef]
IZF_Ex_sig.set [axiom, in ZFdef]
IZF_Ex_sig.union_ex [axiom, in ZFdef]
IZF_sig [moduleid, in ZFdef]
IZF_sig.empty [axiom, in ZFdef]
IZF_sig.empty_ax [axiom, in ZFdef]
IZF_sig.eq_set [axiom, in ZFdef]
IZF_sig.eq_set_ax [axiom, in ZFdef]
IZF_sig.infinite [axiom, in ZFdef]
IZF_sig.infinity_ax1 [axiom, in ZFdef]
IZF_sig.infinity_ax2 [axiom, in ZFdef]
IZF_sig.in_reg [axiom, in ZFdef]
IZF_sig.in_set [axiom, in ZFdef]
IZF_sig.pair [axiom, in ZFdef]
IZF_sig.pair_ax [axiom, in ZFdef]
IZF_sig.power [axiom, in ZFdef]
IZF_sig.power_ax [axiom, in ZFdef]
IZF_sig.regularity_ax [axiom, in ZFdef]
IZF_sig.repl [axiom, in ZFdef]
IZF_sig.repl_ax [axiom, in ZFdef]
IZF_sig.repl_mono [axiom, in ZFdef]
IZF_sig.set [axiom, in ZFdef]
IZF_sig.union [axiom, in ZFdef]
IZF_sig.union_ax [axiom, in ZFdef]


K

K [definition, in Lambda]
kind [constructor, in TermECC]
kind [constructor, in Term]
KSAT_intro [lemma, in Sat]


L

lam [definition, in ZFrelations]
Lam [moduleid, in ZFlambda]
lam [definition, in HFrelation]
Lambda [library]
Lam.Abs [definition, in ZFlambda]
Lam.Abs_typ [lemma, in ZFlambda]
Lam.Abs_typ0 [lemma, in ZFlambda]
Lam.App [definition, in ZFlambda]
Lam.App_typ [lemma, in ZFlambda]
Lam.App_typ0 [lemma, in ZFlambda]
Lam.Cst [definition, in ZFlambda]
Lam.Cst_typ [lemma, in ZFlambda]
Lam.Cst_typ0 [lemma, in ZFlambda]
Lam.Lambda [definition, in ZFlambda]
Lam.LambdaTerms [section, in ZFlambda]
Lam.LambdaTerms.A [variable, in ZFlambda]
Lam.Lambda_elim [lemma, in ZFlambda]
Lam.Lambda_eqn [lemma, in ZFlambda]
Lam.Lambda_fix [lemma, in ZFlambda]
Lam.Lambda_ind [lemma, in ZFlambda]
Lam.Lambda_intro [lemma, in ZFlambda]
Lam.LAMf [definition, in ZFlambda]
Lam.LAMf_ind [lemma, in ZFlambda]
Lam.LAMf_mono [instance, in ZFlambda]
Lam.LAMf_morph [instance, in ZFlambda]
Lam.Lamn [definition, in ZFlambda]
Lam.Lamn_case [lemma, in ZFlambda]
Lam.Lamn_eq [lemma, in ZFlambda]
Lam.Lamn_incl [lemma, in ZFlambda]
Lam.Lamn_incl_succ [lemma, in ZFlambda]
Lam.Var [definition, in ZFlambda]
Lam.Var_typ [lemma, in ZFlambda]
Lam.Var_typ0 [lemma, in ZFlambda]
lam_domain [lemma, in HFrelation]
lam_elim [lemma, in HFrelation]
lam_ext [lemma, in HFrelation]
lam_intro [lemma, in HFrelation]
lam_is_func [lemma, in ZFrelations]
lam_is_function [lemma, in ZFrelations]
lam_rel [definition, in ZFrelations]
lam_rel_is_func [lemma, in ZFrelations]
Lc [moduleid, in GenModelSN]
Lc [moduleid, in SN_CC]
le [definition, in ZFnats]
least_ord [definition, in ZFordcl]
least_ord1 [lemma, in ZFordcl]
least_ord_morph [lemma, in ZFordcl]
le_card [definition, in ZFcard]
le_card_morph [instance, in ZFcard]
le_card_refl [instance, in ZFcard]
le_card_trans [instance, in ZFcard]
le_case [lemma, in ZFnats]
le_lt_trans [lemma, in ZFord]
le_lt_trans [lemma, in ZFordcl]
le_morph [instance, in ZFnats]
le_refl [lemma, in ZFnats]
le_total [lemma, in ZFnats]
Library [library]
lift [definition, in Lambda]
lift [definition, in TermECC]
lift [definition, in Term]
LiftAndSubstEquiv [section, in SN_CC]
lift0 [lemma, in Lambda]
lift0 [lemma, in Term]
lift0 [lemma, in TermECC]
lift0_term [lemma, in ModelCIC]
lift10 [lemma, in ModelCIC]
lift_eq [lemma, in EnsUniv]
lift_in [lemma, in EnsUniv]
lift_rec [definition, in Term]
lift_rec [definition, in TermECC]
lift_rec [definition, in Lambda]
lift_rec0 [lemma, in Term]
lift_rec0 [lemma, in TermECC]
lift_rec0 [lemma, in Lambda]
lift_ref_ge [lemma, in Term]
lift_ref_ge [lemma, in TermECC]
lift_ref_ge [lemma, in Lambda]
lift_ref_lt [lemma, in Lambda]
lift_ref_lt [lemma, in Term]
lift_ref_lt [lemma, in TermECC]
LIM [definition, in ZFindtypes]
limitOrd [definition, in ZFordcl]
limitOrd [definition, in ZFord]
limitOrd' [definition, in ZFordcl]
limit'_is_ord [lemma, in ZFordcl]
limit_equiv [lemma, in ZFordcl]
limit_is_ord [lemma, in ZFord]
limit_is_ord [lemma, in ZFordcl]
limit_union [lemma, in ZFord]
limit_union_intro [lemma, in ZFord]
LimOrd [section, in ZFord]
LimOrd [section, in ZFordcl]
LimOrdRel [section, in ZFordcl]
LimOrdRel [section, in ZFord]
LimOrdRel.R [variable, in ZFordcl]
LimOrdRel.R [variable, in ZFord]
LimOrdRel.Rfun [variable, in ZFordcl]
LimOrdRel.Rfun [variable, in ZFord]
LimOrdRel.Rmorph [variable, in ZFord]
LimOrdRel.Rmorph [variable, in ZFordcl]
LimOrdRel.Rord [variable, in ZFordcl]
LimOrdRel.Rord [variable, in ZFord]
LimOrdRel.Rtot [variable, in ZFord]
LimOrdRel.Rtot [variable, in ZFordcl]
LimOrd.f [variable, in ZFord]
LimOrd.f [variable, in ZFordcl]
LimOrd.ford [variable, in ZFord]
LimOrd.ford [variable, in ZFordcl]
LIM_typ_gen [lemma, in ZFindtypes]
List [definition, in MyList]
Listes [section, in MyList]
Listes.A [variable, in MyList]
list_item [lemma, in MyList]
lt [definition, in ZFnats]
lt_antirefl [lemma, in ZFordcl]
lt_antirefl [lemma, in ZFord]
lt_card [definition, in ZFcard]
lt_card_lt [lemma, in ZFfix]
lt_card_non_zero [lemma, in ZFcard]
lt_is_le [lemma, in ZFnats]
lt_le_trans [lemma, in ZFordcl]
lt_mono [lemma, in ZFnats]
lt_morph [instance, in ZFnats]
lt_osucc [lemma, in ZFord]
lt_osucc_compat [lemma, in ZFord]
lt_trans [lemma, in ZFnats]
lt_0_succ [lemma, in ZFnats]


M

Make [moduleid, in VarMap]
MakeModel [moduleid, in GenModel]
MakeModel [moduleid, in ModelECC]
MakeModel [moduleid, in GenModelSN]
MakeModel [moduleid, in GenModelSyntax]
MakeModel.Abs [definition, in GenModelSN]
MakeModel.Abs_morph [instance, in GenModelSN]
MakeModel.add_var_eq_fun [lemma, in GenModel]
MakeModel.add_var_eq_fun [lemma, in GenModelSN]
MakeModel.App [definition, in GenModelSN]
MakeModel.App_morph [instance, in GenModelSN]
MakeModel.cons_morph [instance, in GenModelSN]
MakeModel.cons_morph [instance, in GenModelSN]
MakeModel.cons_morph [instance, in GenModel]
MakeModel.cons_morph' [instance, in GenModel]
MakeModel.cons_morph' [instance, in GenModelSN]
MakeModel.cons_morph' [instance, in GenModelSN]
MakeModel.cst_fun [definition, in GenModelSN]
MakeModel.cst_morph [instance, in GenModelSN]
MakeModel.discr_ref_prod [lemma, in GenModelSN]
MakeModel.EM [definition, in GenModelSyntax]
MakeModel.env [definition, in GenModel]
MakeModel.env [definition, in GenModelSN]
MakeModel.EQ [definition, in GenModelSyntax]
MakeModel.eq_fun_sym [lemma, in ModelECC]
MakeModel.eq_fun_sym [lemma, in GenModel]
MakeModel.eq_fun_trans [lemma, in ModelECC]
MakeModel.eq_fun_trans [lemma, in GenModel]
MakeModel.eq_int [definition, in ModelECC]
MakeModel.eq_intt [abbreviation, in GenModelSN]
MakeModel.eq_intt_equiv [instance, in GenModelSN]
MakeModel.eq_int_equiv [instance, in ModelECC]
MakeModel.eq_judge [definition, in ModelECC]
MakeModel.eq_judge_beta [lemma, in ModelECC]
MakeModel.eq_judge_trans [lemma, in ModelECC]
MakeModel.eq_kind [lemma, in GenModelSN]
MakeModel.eq_trm [definition, in GenModelSN]
MakeModel.eq_trm_equiv [instance, in GenModelSN]
MakeModel.eq_trm_intro [lemma, in GenModelSN]
MakeModel.eq_trm_refl [instance, in GenModelSN]
MakeModel.eq_trm_sym [instance, in GenModelSN]
MakeModel.eq_trm_trans [instance, in GenModelSN]
MakeModel.eq_typ [definition, in GenModelSN]
MakeModel.eq_typ_abs [lemma, in GenModelSN]
MakeModel.eq_typ_app [lemma, in GenModelSN]
MakeModel.eq_typ_beta [lemma, in GenModelSN]
MakeModel.eq_typ_morph [instance, in GenModelSN]
MakeModel.eq_typ_prod [lemma, in GenModelSN]
MakeModel.eq_typ_setoid [instance, in GenModelSN]
MakeModel.eq_val [abbreviation, in GenModel]
MakeModel.eq_val [abbreviation, in GenModelSN]
MakeModel.eq_val_equiv [instance, in GenModel]
MakeModel.eq_val_equiv [instance, in GenModelSN]
MakeModel.EXT [definition, in GenModelSyntax]
MakeModel.FALSE [definition, in GenModelSyntax]
MakeModel.I [moduleid, in GenModelSN]
MakeModel.iint [projection, in GenModelSN]
MakeModel.iint_morph [projection, in GenModelSN]
MakeModel.iint_morph [instance, in GenModelSN]
MakeModel.ilift [definition, in GenModelSN]
MakeModel.ilift_binder [lemma, in GenModelSN]
MakeModel.ilift_binder_lift [lemma, in GenModelSN]
MakeModel.ilift_lams [lemma, in GenModelSN]
MakeModel.ilift_morph [instance, in GenModelSN]
MakeModel.INAT [definition, in GenModelSyntax]
MakeModel.inftrm [record, in GenModelSN]
MakeModel.int [definition, in GenModelSN]
MakeModel.int [definition, in ModelECC]
MakeModel.intt [abbreviation, in GenModelSN]
MakeModel.int_cons_lift_eq [lemma, in GenModelSN]
MakeModel.int_env [definition, in ModelECC]
MakeModel.int_env [definition, in GenModelSyntax]
MakeModel.int_env_cons [lemma, in ModelECC]
MakeModel.int_lift [lemma, in ModelECC]
MakeModel.int_lift [lemma, in GenModelSyntax]
MakeModel.int_lift_eq [lemma, in GenModelSN]
MakeModel.int_lift_rec_eq [lemma, in GenModelSN]
MakeModel.int_morph [instance, in GenModelSN]
MakeModel.int_morph [instance, in ModelECC]
MakeModel.int_not_kind [lemma, in GenModelSyntax]
MakeModel.int_sound [lemma, in ModelECC]
MakeModel.int_sound [lemma, in GenModelSyntax]
MakeModel.int_subst [lemma, in ModelECC]
MakeModel.int_subst [lemma, in GenModelSyntax]
MakeModel.int_subst0 [lemma, in ModelECC]
MakeModel.int_subst_eq [lemma, in GenModelSN]
MakeModel.int_subst_rec_eq [lemma, in GenModelSN]
MakeModel.int_trm [definition, in GenModelSyntax]
MakeModel.In_int [definition, in ModelECC]
MakeModel.in_int [definition, in GenModelSN]
MakeModel.in_int_intro [lemma, in GenModelSN]
MakeModel.in_int_morph [instance, in GenModelSN]
MakeModel.in_int_not_kind [lemma, in GenModelSN]
MakeModel.in_int_sn [lemma, in GenModelSN]
MakeModel.in_int_varS [lemma, in GenModelSN]
MakeModel.in_int_var0 [lemma, in GenModelSN]
MakeModel.in_reg_r [lemma, in ModelECC]
MakeModel.itm [projection, in GenModelSN]
MakeModel.itm_lift [projection, in GenModelSN]
MakeModel.itm_morph [projection, in GenModelSN]
MakeModel.itm_morph [instance, in GenModelSN]
MakeModel.itm_subst [projection, in GenModelSN]
MakeModel.J [moduleid, in GenModel]
MakeModel.judge [definition, in ModelECC]
MakeModel.judge_abs [lemma, in ModelECC]
MakeModel.judge_app [lemma, in ModelECC]
MakeModel.judge_beta [lemma, in ModelECC]
MakeModel.judge_conv [lemma, in ModelECC]
MakeModel.judge_kind [lemma, in ModelECC]
MakeModel.judge_prod [lemma, in ModelECC]
MakeModel.judge_prop [lemma, in ModelECC]
MakeModel.judge_var [lemma, in ModelECC]
MakeModel.J.eq_typ [definition, in GenModel]
MakeModel.J.eq_typ_morph [instance, in GenModel]
MakeModel.J.sub_typ [definition, in GenModel]
MakeModel.J.sub_typ_morph [instance, in GenModel]
MakeModel.J.typ [definition, in GenModel]
MakeModel.J.typ_morph [instance, in GenModel]
MakeModel.kind [definition, in GenModelSN]
MakeModel.lams_morph [instance, in GenModelSN]
MakeModel.lams_morph [instance, in GenModelSN]
MakeModel.LCeq [moduleid, in GenModelSN]
MakeModel.LCeq.eq [definition, in GenModelSN]
MakeModel.LCeq.eq_equiv [definition, in GenModelSN]
MakeModel.LCeq.eq_equiv [instance, in GenModelSN]
MakeModel.LCeq.t [definition, in GenModelSN]
MakeModel.lift [definition, in GenModelSN]
MakeModel.liftable [definition, in GenModelSN]
MakeModel.lift1var [lemma, in GenModelSN]
MakeModel.lift_morph [instance, in GenModelSN]
MakeModel.lift_rec [definition, in GenModelSN]
MakeModel.non_empty [definition, in GenModelSN]
MakeModel.non_empty_morph [instance, in GenModelSN]
MakeModel.non_empty_var_lift [lemma, in GenModelSN]
MakeModel.non_empty_witness [lemma, in GenModelSN]
MakeModel.non_provability [lemma, in GenModelSyntax]
MakeModel.PI [definition, in GenModelSyntax]
MakeModel.Prod [definition, in GenModelSN]
MakeModel.prod_list [definition, in GenModelSN]
MakeModel.Prod_morph [instance, in GenModelSN]
MakeModel.prod_non_empty [lemma, in GenModelSN]
MakeModel.prop [definition, in GenModelSN]
MakeModel.prop_non_empty [lemma, in GenModelSN]
MakeModel.R [moduleid, in GenModel]
MakeModel.Ref [definition, in GenModelSN]
MakeModel.refl [lemma, in GenModelSN]
MakeModel.R.eq_typ_abs [lemma, in GenModel]
MakeModel.R.eq_typ_app [lemma, in GenModel]
MakeModel.R.eq_typ_beta [lemma, in GenModel]
MakeModel.R.eq_typ_equiv [instance, in GenModel]
MakeModel.R.eq_typ_prod [lemma, in GenModel]
MakeModel.R.refl [lemma, in GenModel]
MakeModel.R.sub_refl [lemma, in GenModel]
MakeModel.R.sub_trans [lemma, in GenModel]
MakeModel.R.sym [lemma, in GenModel]
MakeModel.R.trans [lemma, in GenModel]
MakeModel.R.typ_abs [lemma, in GenModel]
MakeModel.R.typ_app [lemma, in GenModel]
MakeModel.R.typ_beta [lemma, in GenModel]
MakeModel.R.typ_conv [lemma, in GenModel]
MakeModel.R.typ_prod [lemma, in GenModel]
MakeModel.R.typ_prop [lemma, in GenModel]
MakeModel.R.typ_subsumption [lemma, in GenModel]
MakeModel.R.typ_var [lemma, in GenModel]
MakeModel.shift_morph [instance, in GenModelSN]
MakeModel.shift_morph [instance, in GenModelSN]
MakeModel.split_lift [lemma, in GenModelSN]
MakeModel.subst [definition, in GenModelSN]
MakeModel.substitutive [definition, in GenModelSN]
MakeModel.subst_rec [definition, in GenModelSN]
MakeModel.sym [lemma, in GenModelSN]
MakeModel.T [moduleid, in GenModel]
MakeModel.tm [definition, in GenModelSN]
MakeModel.tm_liftable [lemma, in GenModelSN]
MakeModel.tm_lift_rec_eq [lemma, in GenModelSN]
MakeModel.tm_morph [instance, in GenModelSN]
MakeModel.tm_substitutive [lemma, in GenModelSN]
MakeModel.tm_subst_cons [lemma, in GenModelSN]
MakeModel.tm_subst_eq [lemma, in GenModelSN]
MakeModel.tm_subst_rec_eq [lemma, in GenModelSN]
MakeModel.trans [lemma, in GenModelSN]
MakeModel.trm [definition, in GenModelSN]
MakeModel.TRUE [definition, in GenModelSyntax]
MakeModel.typ [definition, in GenModelSN]
MakeModel.typs [definition, in GenModelSN]
MakeModel.typs_non_empty [lemma, in GenModelSN]
MakeModel.typs_not_kind [lemma, in GenModelSN]
MakeModel.typ_abs [lemma, in GenModelSN]
MakeModel.typ_app [lemma, in GenModelSN]
MakeModel.typ_beta [lemma, in GenModelSN]
MakeModel.typ_conv [lemma, in GenModelSN]
MakeModel.typ_morph [instance, in GenModelSN]
MakeModel.typ_prod [lemma, in GenModelSN]
MakeModel.typ_prop [lemma, in GenModelSN]
MakeModel.typ_sn [lemma, in GenModelSN]
MakeModel.typ_var [lemma, in GenModelSN]
MakeModel.T.Abs [definition, in GenModel]
MakeModel.T.Abs_morph [instance, in GenModel]
MakeModel.T.App [definition, in GenModel]
MakeModel.T.App_morph [instance, in GenModel]
MakeModel.T.cst [definition, in GenModel]
MakeModel.T.el [definition, in GenModel]
MakeModel.T.el_morph [instance, in GenModel]
MakeModel.T.el_subst_eq [lemma, in GenModel]
MakeModel.T.eq_term [definition, in GenModel]
MakeModel.T.eq_term_refl [instance, in GenModel]
MakeModel.T.eq_term_sym [instance, in GenModel]
MakeModel.T.eq_term_trans [instance, in GenModel]
MakeModel.T.int [definition, in GenModel]
MakeModel.T.int_lift_rec_eq [lemma, in GenModel]
MakeModel.T.int_morph [instance, in GenModel]
MakeModel.T.int_subst_eq [lemma, in GenModel]
MakeModel.T.int_subst_rec_eq [lemma, in GenModel]
MakeModel.T.kind [definition, in GenModel]
MakeModel.T.lift [definition, in GenModel]
MakeModel.T.Lift [section, in GenModel]
MakeModel.T.lift0_term [lemma, in GenModel]
MakeModel.T.lift1 [definition, in GenModel]
MakeModel.T.lift10 [lemma, in GenModel]
MakeModel.T.lift_morph [instance, in GenModel]
MakeModel.T.lift_rec [definition, in GenModel]
MakeModel.T.Prod [definition, in GenModel]
MakeModel.T.Prod_morph [instance, in GenModel]
MakeModel.T.prop [definition, in GenModel]
MakeModel.T.Ref [definition, in GenModel]
MakeModel.T.simpl_int_lift [lemma, in GenModel]
MakeModel.T.simpl_int_lift1 [lemma, in GenModel]
MakeModel.T.simpl_lift1 [lemma, in GenModel]
MakeModel.T.subst [definition, in GenModel]
MakeModel.T.Substitution [section, in GenModel]
MakeModel.T.subst_morph [instance, in GenModel]
MakeModel.T.subst_rec [definition, in GenModel]
MakeModel.T.term [definition, in GenModel]
MakeModel.u_card_incl_le [lemma, in ModelECC]
MakeModel.V [moduleid, in GenModelSN]
MakeModel.V [moduleid, in GenModel]
MakeModel.val [abbreviation, in GenModel]
MakeModel.val [abbreviation, in GenModelSN]
MakeModel.val_ok [definition, in GenModelSN]
MakeModel.val_ok [definition, in GenModel]
MakeModel.vcons_add_var [lemma, in GenModelSN]
MakeModel.vcons_add_var [lemma, in GenModel]
MakeModel.vcons_add_var0 [lemma, in GenModelSN]
MakeModel.vcons_add_var0 [lemma, in GenModel]
MakeModel.vnil [definition, in GenModel]
MakeModel.vnil [definition, in GenModelSN]
MakeModel.wf [definition, in GenModelSN]
MakeModel.wf_cons [lemma, in GenModelSN]
MakeModel.wf_nil [lemma, in GenModelSN]
MakeModel.wit_prod [lemma, in GenModelSN]
MakeModel.Xeq [moduleid, in GenModelSN]
MakeModel.Xeq [moduleid, in GenModel]
MakeModel.Xeq.eq [definition, in GenModel]
MakeModel.Xeq.eq [definition, in GenModelSN]
MakeModel.Xeq.eq_equiv [instance, in GenModelSN]
MakeModel.Xeq.eq_equiv [definition, in GenModelSN]
MakeModel.Xeq.eq_equiv [definition, in GenModel]
MakeModel.Xeq.eq_equiv [instance, in GenModel]
MakeModel.Xeq.t [definition, in GenModelSN]
MakeModel.Xeq.t [definition, in GenModel]
Make.cons [definition, in VarMap]
Make.cons_ext [lemma, in VarMap]
Make.cons_lams [lemma, in VarMap]
Make.cons_morph [instance, in VarMap]
Make.cons_morph' [instance, in VarMap]
Make.eq_map [definition, in VarMap]
Make.lams [definition, in VarMap]
Make.lams0 [lemma, in VarMap]
Make.lams_bv [lemma, in VarMap]
Make.lams_morph [instance, in VarMap]
Make.lams_shift [lemma, in VarMap]
Make.map [definition, in VarMap]
Make.nil [definition, in VarMap]
Make.shift [definition, in VarMap]
Make.shift0 [lemma, in VarMap]
Make.shift_cons [lemma, in VarMap]
Make.shift_lams [lemma, in VarMap]
Make.shift_morph [instance, in VarMap]
Make.shift_split [lemma, in VarMap]
Map [section, in IntMap]
map [definition, in MyList]
Map.A [variable, in IntMap]
max [definition, in ZFnats]
max_eq [lemma, in ZFnats]
max_lt [lemma, in ZFnats]
max_morph [instance, in ZFnats]
max_sym [lemma, in ZFnats]
max_typ [lemma, in ZFnats]
mem_abs_l [constructor, in Term]
mem_abs_l [constructor, in TermECC]
mem_abs_r [constructor, in Term]
mem_abs_r [constructor, in TermECC]
mem_app_l [constructor, in TermECC]
mem_app_l [constructor, in Term]
mem_app_r [constructor, in TermECC]
mem_app_r [constructor, in Term]
mem_eq [constructor, in TermECC]
mem_eq [constructor, in Term]
mem_prod_l [constructor, in Term]
mem_prod_l [constructor, in TermECC]
mem_prod_r [constructor, in TermECC]
mem_prod_r [constructor, in Term]
mem_sort [inductive, in Term]
mem_sort [inductive, in TermECC]
mem_sort_lift [lemma, in Term]
mem_sort_lift [lemma, in TermECC]
mem_sort_subst [lemma, in Term]
mem_sort_subst [lemma, in TermECC]
minus2 [definition, in ZF]
ModelCIC [library]
ModelECC [library]
ModelHF [library]
Models [library]
ModelSyntax [library]
ModelZF [library]
morph1 [abbreviation, in HF]
morph1 [abbreviation, in ZF]
morph2 [abbreviation, in HF]
morph2 [abbreviation, in ZF]
morph3 [abbreviation, in HF]
morph_fix_body [lemma, in ModelCIC]
mpar_red1 [inductive, in TypeJudge]
mpar_red1_refl [lemma, in TypeJudge]
mult_w [definition, in ZFord]
mult_w [definition, in ZFordcl]
mu_lim [definition, in ZFindtypes]
mu_lt [definition, in ZFfix]
mu_ord [definition, in ZFfix]
mu_ord [definition, in ZFindtypes]
mu_ord [definition, in ZFindtypes]
mu_regular [definition, in ZFindtypes]
MyList [library]


N

N [definition, in ZFnats]
Nat [definition, in ModelCIC]
NAT [definition, in ZFindtypes]
Natcase [definition, in ModelCIC]
NATCASE [definition, in ZFindtypes]
NATCASE_choice_pred [lemma, in ZFindtypes]
NATCASE_def [lemma, in ZFindtypes]
NATCASE_morph [instance, in ZFindtypes]
Natcase_morph [instance, in ModelCIC]
NATCASE_rel [definition, in ZFindtypes]
NATCASE_SUCC [lemma, in ZFindtypes]
Natcase_succ [lemma, in ModelCIC]
NATCASE_typ [lemma, in ZFindtypes]
Natcase_zero [lemma, in ModelCIC]
NATCASE_ZERO [lemma, in ZFindtypes]
NATf [definition, in ZFindtypes]
NatFix [definition, in ModelCIC]
NatFixRules [section, in ModelCIC]
NatFixRules.e [variable, in ModelCIC]
NatFixRules.eps [variable, in ModelCIC]
NatFixRules.eps_ord [variable, in ModelCIC]
NatFixRules.M [variable, in ModelCIC]
NatFixRules.M_nk [variable, in ModelCIC]
NatFixRules.O [variable, in ModelCIC]
NatFixRules.stab [variable, in ModelCIC]
NatFixRules.ty_M [variable, in ModelCIC]
NatFixRules.ty_O [variable, in ModelCIC]
NatFixRules.U [variable, in ModelCIC]
NATfun_ext [lemma, in ZFindtypes]
NATf_case [lemma, in ZFindtypes]
NATf_discr [lemma, in ZFindtypes]
NATf_mono [instance, in ZFindtypes]
NATf_morph [instance, in ZFindtypes]
NatI [definition, in ModelCIC]
Nati [definition, in ModelCIC]
NATi [definition, in ZFindtypes]
NATi_case [lemma, in ZFindtypes]
NATi_fix [lemma, in ZFindtypes]
NATi_morph [instance, in ZFindtypes]
NATi_morph [instance, in ModelCIC]
NATi_morph [instance, in ZFindtypes]
NATi_NAT [lemma, in ZFindtypes]
NATi_pre_typ [lemma, in ZFindtypes]
NATi_sub [lemma, in ModelCIC]
natOrd [lemma, in ZFordcl]
NatOrd_theory [section, in ZFindtypes]
NatOrd_theory.IterationNat [section, in ZFindtypes]
NatOrd_theory.IterationOrd [section, in ZFindtypes]
NatOrd_theory.NatFixpoint [section, in ZFindtypes]
NatOrd_theory.NatUniverse [section, in ZFindtypes]
NatOrd_theory.NatUniverse.has_cstr [variable, in ZFindtypes]
NatOrd_theory.NatUniverse.has_empty [variable, in ZFindtypes]
NatOrd_theory.NatUniverse.has_limit [variable, in ZFindtypes]
NatOrd_theory.NatUniverse.U [variable, in ZFindtypes]
NatOrd_theory.OrdFixpoint [section, in ZFindtypes]
NatOrd_theory.OrdFixpoint.mu [variable, in ZFindtypes]
NatOrd_theory.OrdFixpoint.mu_strong [variable, in ZFindtypes]
NatOrd_theory.OrdFixpoint.NAT_in_mu [variable, in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse [section, in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.has_cstr [variable, in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.has_empty [variable, in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.mu_clos [variable, in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.U [variable, in ZFindtypes]
NATREC [definition, in ModelCIC]
NatRec [section, in ModelCIC]
NatRec.eps [variable, in ModelCIC]
NatRec.epsOrd [variable, in ModelCIC]
NatRec.F [variable, in ModelCIC]
NatRec.Fm [variable, in ModelCIC]
NatRec.Fstab [variable, in ModelCIC]
NatRec.Ftyp [variable, in ModelCIC]
NatRec.NATREC_Eqn [section, in ModelCIC]
NatRec.NATREC_Eqn.lt_eps [variable, in ModelCIC]
NatRec.NATREC_Eqn.o [variable, in ModelCIC]
NatRec.U [variable, in ModelCIC]
NatRec.Um [variable, in ModelCIC]
NATREC_eqn [lemma, in ModelCIC]
NATREC_expand [lemma, in ModelCIC]
NATREC_inv [lemma, in ModelCIC]
NATREC_morph [lemma, in ModelCIC]
NATREC_step [lemma, in ModelCIC]
NATREC_wt [lemma, in ModelCIC]
nat2NAT [definition, in ZFindtypes]
nat2NAT_reflect [lemma, in ZFindtypes]
nat2ordset [definition, in ZFord]
nat2ordset_typ [lemma, in ZFord]
nat2set [definition, in ZFnats]
nat2set_inj [lemma, in ZFnats]
nat2set_reflect [lemma, in ZFnats]
nat2set_typ [lemma, in ZFnats]
NAT_continuous [lemma, in ZFindtypes]
NAT_eq [lemma, in ZFindtypes]
NAT_fix [lemma, in ZFindtypes]
nat_fix_eq [lemma, in ModelCIC]
nat_ind [definition, in ModelCIC]
NAT_ind [lemma, in ZFindtypes]
nat_ind_def [lemma, in ModelCIC]
nat_ind_typ [definition, in ModelCIC]
NAT_typ [lemma, in ZFindtypes]
neutral [definition, in Can]
nf_uniqueness [lemma, in ConvECC]
nf_uniqueness [lemma, in Conv]
noccur [definition, in ModelCIC]
noc_app [lemma, in ModelCIC]
noc_kind [lemma, in ModelCIC]
noc_prop [lemma, in ModelCIC]
noc_var [lemma, in ModelCIC]
normal [definition, in Term]
normal [definition, in Lambda]
normal [definition, in TermECC]
Normalisation_Forte [section, in TermECC]
Normalisation_Forte [section, in Term]
no_universal_set [lemma, in ZF]
nth_def [definition, in MyList]
nth_sound [lemma, in MyList]
nth_sub_eq [lemma, in Env]
nth_sub_eq [lemma, in EnvECC]
nth_sub_inf [lemma, in Env]
nth_sub_inf [lemma, in EnvECC]
nth_sub_sup [lemma, in EnvECC]
nth_sub_sup [lemma, in Env]
N_ind [lemma, in ZFnats]
N_limit_ord [lemma, in ZFordcl]


O

OL [constructor, in ZFord]
OL [constructor, in ZFordcl]
ole_lts [lemma, in ZFord]
olts_le [lemma, in ZFord]
omega [definition, in ZF]
omega [definition, in ZFord]
omega_in_omega [lemma, in ZF]
omega_limit_ord [lemma, in ZFord]
omega_not_in_omega [lemma, in ZF]
ONE [abbreviation, in HF]
one_step_conv_exp [lemma, in TermECC]
one_step_conv_exp [lemma, in Term]
one_step_red [lemma, in Term]
one_step_red [lemma, in Lambda]
one_step_red [lemma, in TermECC]
OO [constructor, in ZFord]
OO [constructor, in ZFordcl]
ORD [definition, in ZFindtypes]
ord [inductive, in ZFordcl]
Ord [definition, in ModelCIC]
ord [inductive, in ZFord]
ORDf [definition, in ZFindtypes]
ORDfun_ext [lemma, in ZFindtypes]
ORDf_case [lemma, in ZFindtypes]
ORDf_mono [instance, in ZFindtypes]
ORDf_morph [instance, in ZFindtypes]
ORDi [definition, in ZFindtypes]
OrdinalUpperBound [section, in ZFord]
OrdinalUpperBound.f [variable, in ZFord]
OrdinalUpperBound.f_ext [variable, in ZFord]
OrdinalUpperBound.f_ord [variable, in ZFord]
OrdinalUpperBound.I [variable, in ZFord]
ORDi_case [lemma, in ZFindtypes]
ORDi_fix [lemma, in ZFindtypes]
ORDi_morph [instance, in ZFindtypes]
ORDi_ORD [lemma, in ZFindtypes]
ORDi_pre_typ [lemma, in ZFindtypes]
ord2set [definition, in ZFord]
ord2set [definition, in ZFordcl]
ord2set_typ [lemma, in ZFord]
ord2set_typ [lemma, in ZFordcl]
ORD_eq [lemma, in ZFindtypes]
ord_le_incl [lemma, in ZFordcl]
ord_sup [definition, in ZFordcl]
ord_sup [definition, in ZFord]
ORD_typ [lemma, in ZFindtypes]
OS [constructor, in ZFordcl]
OS [constructor, in ZFord]
osucc [definition, in ZFord2]
OSucc [definition, in ModelCIC]
osucc [definition, in ZFord]
osucc_morph [instance, in ZFord]
osucc_omega [lemma, in ZFord]
OSucc_sub [lemma, in ModelCIC]
o_ord [definition, in ModelCIC]


P

pair [definition, in HF]
pair_commut [lemma, in ZF]
pair_elim [lemma, in ZF]
pair_elim [lemma, in HF]
pair_equiv [lemma, in EnsUniv]
pair_ext [lemma, in ZF]
pair_intro1 [lemma, in ZF]
pair_intro1 [lemma, in HF]
pair_intro2 [lemma, in HF]
pair_intro2 [lemma, in ZF]
pair_inv [lemma, in ZF]
pair_morph [instance, in ZF]
pair_morph [instance, in HF]
par_beta [constructor, in TypeJudge]
par_beta [constructor, in Term]
par_beta [constructor, in TermECC]
par_red [definition, in TermECC]
par_red [definition, in Term]
par_red1 [inductive, in TermECC]
par_red1 [inductive, in Term]
par_red1_lift [lemma, in TermECC]
par_red1_lift [lemma, in Term]
par_red1_subst [lemma, in Term]
par_red1_subst [lemma, in TermECC]
par_red_red [lemma, in TermECC]
par_red_red [lemma, in Term]
permute_lift [lemma, in Lambda]
permute_lift [lemma, in Term]
permute_lift [lemma, in TermECC]
permute_lift_rec [lemma, in Lambda]
permute_lift_rec [lemma, in Term]
permute_lift_rec [lemma, in TermECC]
PI [definition, in ModelZF]
Pi [definition, in Can]
plump [definition, in ZFord3]
plump [definition, in ZFord]
plump_Acc [lemma, in ZFord]
plump_Acc [lemma, in ZFord3]
plump_bound [lemma, in ZFord3]
plump_bound [lemma, in ZFord]
plump_morph [lemma, in ZFord]
plump_morph [lemma, in ZFord3]
plus_w [definition, in ZFordcl]
plus_w [definition, in ZFord]
power [definition, in HF]
power_elim [lemma, in ZF]
power_elim [lemma, in HF]
power_equiv [lemma, in EnsUniv]
power_ext [lemma, in HF]
power_ext [lemma, in ZF]
power_intro [lemma, in ZF]
power_intro [lemma, in HF]
power_mono [lemma, in ZF]
power_morph [instance, in ZF]
power_morph [lemma, in HF]
pow_w [definition, in ZFordcl]
pow_w [definition, in ZFord]
prd_sup [axiom, in ModelCIC]
prd_sup_lub [axiom, in ModelCIC]
prd_union [axiom, in ModelCIC]
pred [definition, in ZFnats]
pred_morph [instance, in ZFnats]
pred_succ_eq [lemma, in ZFnats]
pred_typ [lemma, in ZFnats]
prf_trm [definition, in HFcoc]
prf_trm [definition, in ZFcoc]
Prod [constructor, in TermECC]
Prod [constructor, in Term]
prodcart [definition, in ZFpairs]
prodcart_mono [instance, in ZFpairs]
prodcart_morph [instance, in ZFpairs]
ProductContinuity [section, in ZFindtypes]
ProductContinuity.mu [variable, in ZFindtypes]
ProductContinuity.mu_strong [variable, in ZFindtypes]
prod_par_red [constructor, in TermECC]
prod_par_red [constructor, in Term]
prod_par_red [constructor, in TypeJudge]
prod_red_l [constructor, in TermECC]
prod_red_l [constructor, in Term]
prod_red_r [constructor, in TermECC]
prod_red_r [constructor, in Term]
prop [constructor, in TermECC]
prop [constructor, in Term]
props [definition, in HFcoc]
props [definition, in ZFcoc]


R

raw_choose_elt [lemma, in HF]
red [inductive, in Lambda]
red [inductive, in TermECC]
red [inductive, in Term]
redp [definition, in Lambda]
redp_abs [lemma, in Lambda]
redp_app_l [lemma, in Lambda]
redp_app_r [lemma, in Lambda]
redp_K [lemma, in Lambda]
redp_lift_rec [lemma, in Lambda]
Reduction [section, in EnvECC]
Reduction [section, in Env]
Reduction.R [variable, in EnvECC]
Reduction.R [variable, in Env]
Reduction.R_lift [variable, in EnvECC]
Reduction.R_lift [variable, in Env]
red1 [inductive, in Term]
red1 [inductive, in Lambda]
red1 [inductive, in TermECC]
red1_beta [lemma, in Lambda]
red1_env_hd [constructor, in Env]
red1_env_hd [constructor, in TypeJudgeECC]
red1_env_hd [constructor, in TypeJudge]
red1_env_hd [constructor, in EnvECC]
red1_env_tl [constructor, in Env]
red1_env_tl [constructor, in TypeJudge]
red1_env_tl [constructor, in EnvECC]
red1_env_tl [constructor, in TypeJudgeECC]
red1_in_env [inductive, in TypeJudgeECC]
red1_in_env [inductive, in EnvECC]
red1_in_env [inductive, in TypeJudge]
red1_in_env [inductive, in Env]
red1_lift [lemma, in Lambda]
red1_lift [lemma, in Term]
red1_lift [lemma, in TermECC]
red1_mpar_red1 [lemma, in TypeJudge]
red1_par_red1 [lemma, in Term]
red1_par_red1 [lemma, in TermECC]
red1_red_ind [lemma, in Term]
red1_red_ind [lemma, in TermECC]
red1_subst_l [lemma, in TermECC]
red1_subst_l [lemma, in Term]
red1_subst_l [lemma, in Lambda]
red1_subst_r [lemma, in TermECC]
red1_subst_r [lemma, in Lambda]
red1_subst_r [lemma, in Term]
red_conv [lemma, in Term]
red_conv [lemma, in TermECC]
red_conv [lemma, in Lambda]
red_env_unmark_conv [lemma, in TypeJudge]
red_item [lemma, in EnvECC]
red_item [lemma, in TypeJudge]
red_item [lemma, in Env]
red_item [lemma, in TypeJudgeECC]
red_normal [lemma, in Term]
red_normal [lemma, in TermECC]
red_par_red [lemma, in Term]
red_par_red [lemma, in TermECC]
red_prod_prod [lemma, in Term]
red_prod_prod [lemma, in TypeJudge]
red_prod_prod [lemma, in TermECC]
red_prod_prod_eq [lemma, in TypeJudge]
red_red_abs [lemma, in Lambda]
red_red_abs [lemma, in TermECC]
red_red_abs [lemma, in Term]
red_red_app [lemma, in TermECC]
red_red_app [lemma, in Lambda]
red_red_app [lemma, in Term]
red_red_prod [lemma, in TermECC]
red_red_prod [lemma, in Term]
red_refl [instance, in Lambda]
red_sort_mem [lemma, in TermECC]
red_sort_mem [lemma, in Term]
red_sort_sort [lemma, in Term]
red_sort_sort [lemma, in TermECC]
red_sym_conv [lemma, in Lambda]
red_trans [instance, in Lambda]
Ref [constructor, in Term]
Ref [constructor, in Lambda]
Ref [constructor, in TermECC]
refl_conv [constructor, in Lambda]
refl_conv [constructor, in TermECC]
refl_conv [constructor, in Term]
refl_eq_map [lemma, in IntMap]
refl_par_red1 [lemma, in Term]
refl_par_red1 [lemma, in TermECC]
refl_red [constructor, in Lambda]
refl_red [constructor, in TermECC]
refl_red [constructor, in Term]
ref_par_red [constructor, in TermECC]
ref_par_red [constructor, in Term]
ref_par_red [constructor, in TypeJudge]
regular [definition, in ZFcard]
regularity_ax [lemma, in HF]
regular' [definition, in ZFcard]
regular_card [definition, in ZFcard]
rel [definition, in ZFrelations]
relation_is_rel [lemma, in ZFrelations]
rel_app [definition, in ZFrelations]
rel_app_morph [instance, in ZFrelations]
rel_comp [definition, in ZFrelations]
rel_comp_intro [lemma, in ZFrelations]
rel_domain [definition, in ZFrelations]
rel_domain_incl [lemma, in ZFrelations]
rel_domain_intro [lemma, in ZFrelations]
rel_image [definition, in ZFrelations]
rel_image_ex [lemma, in ZFrelations]
rel_image_incl [lemma, in ZFrelations]
rel_image_intro [lemma, in ZFrelations]
rel_image_morph [instance, in ZFrelations]
rel_is_relation [lemma, in ZFrelations]
rel_mono [lemma, in ZFrelations]
rel_morph [instance, in ZFrelations]
repl [definition, in HF]
replf [definition, in ZF]
replf_ax [lemma, in ZF]
replf_elim [lemma, in ZF]
replf_empty [lemma, in ZF]
replf_ext [lemma, in ZF]
replf_intro [lemma, in ZF]
replf_mono2 [lemma, in ZF]
replf_mono_raw [instance, in ZF]
replf_morph [lemma, in ZF]
replf_morph_gen [lemma, in ZF]
replf_morph_raw [instance, in ZF]
replSAT [definition, in ZFlambda]
replSAT_ax [lemma, in ZFlambda]
repl1_equiv [lemma, in EnsUniv]
repl_elim [lemma, in ZFrepl]
repl_elim [lemma, in HF]
repl_empty [lemma, in ZFrepl]
repl_ext [lemma, in ZFrepl]
repl_ext [lemma, in HF]
repl_intro [lemma, in HF]
repl_intro [lemma, in ZFrepl]
repl_mono2 [lemma, in ZFrepl]
repl_mono_raw [instance, in ZFrepl]
repl_morph [lemma, in HF]
repl_morph_raw [instance, in ZFrepl]
repl_rel [definition, in ZFrepl]
repl_rel_compat_lemma [lemma, in ZFrepl]
repl_rel_fun [lemma, in ZFrepl]
repl_rel_incl [lemma, in ZFfix]
repl_sup [lemma, in ZFord]
repl_sup [lemma, in ZFordcl]
repl_sup_rel [lemma, in ZFord]
repl_sup_rel [lemma, in ZFordcl]
Russel [section, in ZF]
Russel.U [variable, in ZF]
Russel.universal [variable, in ZF]


S

S [moduleid, in EnsUniv]
SAT [moduleid, in Sat]
Sat [library]
SatSet [moduleid, in Sat]
SatSet.daimon [definition, in Sat]
SatSet.eqSAT [definition, in Sat]
SatSet.eqSAT_def [lemma, in Sat]
SatSet.inSAT [definition, in Sat]
SatSet.inSAT_morph [instance, in Sat]
SatSet.interSAT [definition, in Sat]
SatSet.interSAT_elim [lemma, in Sat]
SatSet.interSAT_intro [lemma, in Sat]
SatSet.interSAT_morph [lemma, in Sat]
SatSet.prodSAT [definition, in Sat]
SatSet.prodSAT_elim [lemma, in Sat]
SatSet.prodSAT_intro [lemma, in Sat]
SatSet.prodSAT_morph [instance, in Sat]
SatSet.SAT [definition, in Sat]
SatSet.sat_sn [lemma, in Sat]
SatSet.snSAT [definition, in Sat]
SatSet.snSAT_intro [lemma, in Sat]
SatSet.varSAT [lemma, in Sat]
SAT.daimon [axiom, in Sat]
SAT.eqSAT [axiom, in Sat]
SAT.eqSAT_def [axiom, in Sat]
SAT.inSAT [axiom, in Sat]
SAT.inSAT_morph [instance, in Sat]
SAT.inSAT_morph [axiom, in Sat]
SAT.interSAT [axiom, in Sat]
SAT.interSAT_elim [axiom, in Sat]
SAT.interSAT_intro [axiom, in Sat]
SAT.interSAT_morph [axiom, in Sat]
SAT.prodSAT [axiom, in Sat]
SAT.prodSAT_elim [axiom, in Sat]
SAT.prodSAT_intro [axiom, in Sat]
SAT.prodSAT_morph [axiom, in Sat]
SAT.prodSAT_morph [instance, in Sat]
SAT.SAT [axiom, in Sat]
SAT.sat_sn [axiom, in Sat]
SAT.snSAT [axiom, in Sat]
SAT.snSAT_intro [axiom, in Sat]
SAT.varSAT [axiom, in Sat]
sbtrm_abs [constructor, in Lambda]
sbtrm_abs_l [constructor, in Term]
sbtrm_abs_l [constructor, in TermECC]
sbtrm_abs_r [constructor, in TermECC]
sbtrm_abs_r [constructor, in Term]
sbtrm_app_l [constructor, in Lambda]
sbtrm_app_l [constructor, in TermECC]
sbtrm_app_l [constructor, in Term]
sbtrm_app_r [constructor, in TermECC]
sbtrm_app_r [constructor, in Term]
sbtrm_app_r [constructor, in Lambda]
sbtrm_prod_l [constructor, in Term]
sbtrm_prod_l [constructor, in TermECC]
sbtrm_prod_r [constructor, in TermECC]
sbtrm_prod_r [constructor, in Term]
sigma [definition, in ZFpairs]
sigma_morph [lemma, in ZFpairs]
simpl_int_lift [lemma, in ModelCIC]
simpl_int_lift1 [lemma, in ModelCIC]
simpl_lift [lemma, in Term]
simpl_lift [lemma, in TermECC]
simpl_lift [lemma, in Lambda]
simpl_lift1 [lemma, in ModelCIC]
simpl_lift_rec [lemma, in Lambda]
simpl_lift_rec [lemma, in TermECC]
simpl_lift_rec [lemma, in Term]
simpl_subst [lemma, in Lambda]
simpl_subst [lemma, in TermECC]
simpl_subst [lemma, in Term]
simpl_subst_rec [lemma, in TermECC]
simpl_subst_rec [lemma, in Term]
simpl_subst_rec [lemma, in Lambda]
singl [definition, in ZF]
singl [definition, in HF]
singl_elim [lemma, in HF]
singl_elim [lemma, in ZF]
singl_ext [lemma, in ZF]
singl_ext [lemma, in HF]
singl_inj [lemma, in ZF]
singl_intro [lemma, in HF]
singl_intro [lemma, in ZF]
singl_intro_eq [lemma, in ZF]
singl_morph [instance, in HF]
singl_morph [instance, in ZF]
Skolem [moduleid, in ZFskol]
Skolem.downR [definition, in ZFskol]
Skolem.downR_fun [lemma, in ZFskol]
Skolem.downR_morph [lemma, in ZFskol]
Skolem.empty [definition, in ZFskol]
Skolem.empty_ax [lemma, in ZFskol]
Skolem.empty_sig [lemma, in ZFskol]
Skolem.Eq_proj [lemma, in ZFskol]
Skolem.eq_set [definition, in ZFskol]
Skolem.eq_setoid [instance, in ZFskol]
Skolem.eq_set_ax [lemma, in ZFskol]
Skolem.eq_Zeq [lemma, in ZFskol]
Skolem.funDom [definition, in ZFskol]
Skolem.incl_set [definition, in ZFskol]
Skolem.infinite [definition, in ZFskol]
Skolem.infinite_sig [definition, in ZFskol]
Skolem.infinity_ax1 [lemma, in ZFskol]
Skolem.infinity_ax2 [lemma, in ZFskol]
Skolem.InSet [constructor, in ZFskol]
Skolem.inZ_in [lemma, in ZFskol]
Skolem.In_intro [lemma, in ZFskol]
Skolem.in_inZ [lemma, in ZFskol]
Skolem.in_morph [instance, in ZFskol]
Skolem.in_reg [lemma, in ZFskol]
Skolem.in_set [definition, in ZFskol]
Skolem.in_set_ [inductive, in ZFskol]
Skolem.in_set_elim [lemma, in ZFskol]
Skolem.Nat [definition, in ZFskol]
Skolem.Nat_morph [instance, in ZFskol]
Skolem.Nat_S [lemma, in ZFskol]
Skolem.pair [definition, in ZFskol]
Skolem.pair_ax [lemma, in ZFskol]
Skolem.pair_sig [lemma, in ZFskol]
Skolem.power [definition, in ZFskol]
Skolem.power_ax [lemma, in ZFskol]
Skolem.power_sig [lemma, in ZFskol]
Skolem.regularity_ax [lemma, in ZFskol]
Skolem.repl [definition, in ZFskol]
Skolem.repl0 [lemma, in ZFskol]
Skolem.repl0_mono [lemma, in ZFskol]
Skolem.repl_ax [lemma, in ZFskol]
Skolem.repl_mono [lemma, in ZFskol]
Skolem.repl_sig [lemma, in ZFskol]
Skolem.set [definition, in ZFskol]
Skolem.set_intro [lemma, in ZFskol]
Skolem.union [definition, in ZFskol]
Skolem.union_ax [lemma, in ZFskol]
Skolem.union_sig [lemma, in ZFskol]
Skolem.Zeq_eq [lemma, in ZFskol]
Skolem.Zin_morph [instance, in ZFskol]
Skolem.Zsetoid [instance, in ZFskol]
Skolem.Z2set [definition, in ZFskol]
Skolem.Z2set_morph [instance, in ZFskol]
Skolem.Z2set_surj [lemma, in ZFskol]
sn [definition, in Lambda]
SN [moduleid, in SN_CC]
sn [definition, in TermECC]
sn [definition, in Term]
snd [definition, in HF]
snd [definition, in ZFpairs]
snd_def [lemma, in ZFpairs]
snd_def [lemma, in HF]
snd_ext [lemma, in HF]
snd_morph [instance, in ZFpairs]
snd_morph [instance, in HF]
snd_typ [lemma, in ZFpairs]
snd_typ_sigma [lemma, in ZFpairs]
sn_abs [lemma, in Lambda]
SN_addon [moduleid, in GenModelSN]
SN_addon.daemon [axiom, in GenModelSN]
SN_addon.daemon_false [axiom, in GenModelSN]
SN_addon.Red [axiom, in GenModelSN]
SN_addon.Red_morph [axiom, in GenModelSN]
SN_addon.Red_morph [instance, in GenModelSN]
SN_addon.Red_prod [axiom, in GenModelSN]
SN_addon.Red_sort [axiom, in GenModelSN]
SN_CC [library]
SN_CC_addon [moduleid, in SN_CC]
SN_CC_addon.daemon [definition, in SN_CC]
SN_CC_addon.daemon_false [lemma, in SN_CC]
SN_CC_addon.Red [definition, in SN_CC]
SN_CC_addon.Red_morph [lemma, in SN_CC]
SN_CC_addon.Red_prod [lemma, in SN_CC]
SN_CC_addon.Red_sort [lemma, in SN_CC]
SN_CC_Model [moduleid, in SN_CC]
SN_CC_Model.app [definition, in SN_CC]
SN_CC_Model.app_ext [lemma, in SN_CC]
SN_CC_Model.beta_eq [lemma, in SN_CC]
SN_CC_Model.eqX [definition, in SN_CC]
SN_CC_Model.eqX_equiv [lemma, in SN_CC]
SN_CC_Model.eq_fun [definition, in SN_CC]
SN_CC_Model.impredicative_prod [lemma, in SN_CC]
SN_CC_Model.inX [definition, in SN_CC]
SN_CC_Model.in_ext [lemma, in SN_CC]
SN_CC_Model.lam [definition, in SN_CC]
SN_CC_Model.lam_ext [lemma, in SN_CC]
SN_CC_Model.prod [definition, in SN_CC]
SN_CC_Model.prod_elim [lemma, in SN_CC]
SN_CC_Model.prod_ext [lemma, in SN_CC]
SN_CC_Model.prod_intro [lemma, in SN_CC]
SN_CC_Model.props [definition, in SN_CC]
SN_CC_Model.X [definition, in SN_CC]
sn_K [lemma, in Lambda]
sn_prod [lemma, in TermECC]
sn_prod [lemma, in Term]
sn_red_sn [lemma, in Term]
sn_red_sn [lemma, in TermECC]
sn_red_sn [lemma, in Lambda]
sn_subst [lemma, in Term]
sn_subst [lemma, in Lambda]
sn_subst [lemma, in TermECC]
sn_tm [lemma, in SN_CC]
sort [inductive, in TermECC]
sort [inductive, in Term]
sort_par_red [constructor, in Term]
sort_par_red [constructor, in TypeJudge]
sort_par_red [constructor, in TermECC]
sort_uniqueness [lemma, in TypeJudge]
Soundness [moduleid, in ModelHF]
Srt [constructor, in TermECC]
Srt [constructor, in Term]
sSAT [definition, in ZFlambda]
sSAT_morph [instance, in ZFlambda]
stab_fix_body [lemma, in ModelCIC]
stab_fix_prop [definition, in ModelCIC]
strip_lemma [lemma, in ConvECC]
strip_lemma [lemma, in Conv]
strip_lemma [lemma, in TypeJudge]
stronglyInaccessibleCard [definition, in ZFcard]
StrongNormalisation [section, in Lambda]
strong_normalization [lemma, in SN_CC]
str_confl [lemma, in TypeJudge]
str_confluence_par_red1 [lemma, in ConvECC]
str_confluence_par_red1 [lemma, in Conv]
str_confluent [definition, in ConvECC]
str_confluent [definition, in Conv]
subject_reduction [lemma, in TypeECC]
subject_reduction [lemma, in TypeJudge]
subject_reduction [lemma, in Types]
subj_red [lemma, in TypeECC]
subj_red [lemma, in Types]
subset [definition, in HF]
subset [definition, in ZF]
subset_ax [lemma, in ZF]
subset_elim1 [lemma, in ZF]
subset_elim1 [lemma, in HF]
subset_elim2 [lemma, in ZF]
subset_elim2 [lemma, in HF]
subset_elim2_gen [lemma, in HF]
subset_empty1 [lemma, in HF]
subset_equiv [lemma, in EnsUniv]
subset_ext [lemma, in HF]
subset_ext [lemma, in ZF]
subset_intro [lemma, in HF]
subset_intro [lemma, in ZF]
subset_intro_gen [lemma, in HF]
subset_morph [lemma, in ZF]
subset_morph_ext [lemma, in HF]
subset_singl [lemma, in HF]
subst [definition, in Lambda]
subst [definition, in Term]
subst [definition, in TermECC]
substitution [lemma, in Types]
substitution [lemma, in TypeJudge]
substitution [lemma, in TypeJudgeECC]
substitution [lemma, in TypeECC]
subst_rec [definition, in TermECC]
subst_rec [definition, in Lambda]
subst_rec [definition, in Term]
subst_ref_eq [lemma, in Term]
subst_ref_eq [lemma, in TermECC]
subst_ref_eq [lemma, in Lambda]
subst_ref_gt [lemma, in Term]
subst_ref_gt [lemma, in Lambda]
subst_ref_gt [lemma, in TermECC]
subst_ref_lt [lemma, in TermECC]
subst_ref_lt [lemma, in Term]
subst_ref_lt [lemma, in Lambda]
subterm [inductive, in Term]
subterm [inductive, in Lambda]
subterm [inductive, in TermECC]
subterm_sn [lemma, in Lambda]
subterm_sn [lemma, in TermECC]
subterm_sn [lemma, in Term]
sub_in_env [inductive, in Env]
sub_in_env [inductive, in EnvECC]
sub_item_lift_eq [lemma, in Env]
sub_item_lift_eq [lemma, in EnvECC]
sub_item_lift_sup [lemma, in EnvECC]
sub_item_lift_sup [lemma, in Env]
sub_O [constructor, in EnvECC]
sub_O [constructor, in Env]
sub_S [constructor, in EnvECC]
sub_S [constructor, in Env]
sub_typ_covariant [definition, in ModelCIC]
succ [definition, in ZFnats]
SUCC [definition, in ZFindtypes]
SuccI [definition, in ModelCIC]
succOrd [definition, in ZFordcl]
succOrd [definition, in ZFord]
succ_equiv [lemma, in ZFord_equiv]
SUCC_inj [lemma, in ZFindtypes]
succ_inj [lemma, in ZFnats]
succ_intro1 [lemma, in ZFnats]
succ_intro2 [lemma, in ZFnats]
succ_morph [instance, in ZFnats]
SUCC_typ [lemma, in ZFindtypes]
succ_typ [lemma, in ZFnats]
SUCC_typ_gen [lemma, in ZFindtypes]
sum [definition, in ZFsum]
sum_cont [lemma, in ZFindtypes]
sum_ext_natf [lemma, in ZFindtypes]
sum_ext_ordf [lemma, in ZFindtypes]
sum_ind [lemma, in ZFsum]
sum_is_ext [lemma, in ZFindtypes]
sum_mono [lemma, in ZFsum]
sum_morph [instance, in ZFsum]
sup [definition, in ZF]
sup_ax [lemma, in ZF]
sup_ext [lemma, in ZF]
sup_incl [lemma, in ZF]
sup_morph [lemma, in ZF]
sup_morph_gen [lemma, in ZF]
sup_rel [definition, in ZFord]
sup_rel [definition, in ZFordcl]
surj_pair [lemma, in ZFpairs]
sym_conv [lemma, in Term]
sym_conv [lemma, in TermECC]
sym_eq_map [lemma, in IntMap]
SyntacticModel [moduleid, in ModelSyntax]
SyntacticModel.eqX [definition, in ModelSyntax]
SyntacticModel.eqX_equiv [instance, in ModelSyntax]
SyntacticModel.mem [inductive, in ModelSyntax]
SyntacticModel.MemProp [constructor, in ModelSyntax]
SyntacticModel.X [definition, in ModelSyntax]


T

TarskiGrothendieck [section, in ZFgrothendieck]
TarskiGrothendieck.gr [variable, in ZFgrothendieck]
term [inductive, in Term]
term [inductive, in Lambda]
term [inductive, in TermECC]
Term [library]
TermECC [library]
Termes [section, in TermECC]
Termes [section, in Term]
Terms [section, in Lambda]
thinning [lemma, in Types]
thinning [lemma, in TypeECC]
thinning_n [lemma, in TypeECC]
thinning_n [lemma, in Types]
TI [definition, in ZFord]
TI [definition, in ZFordcl]
TIO [definition, in ZFfixfuntyp]
TIO_elim [lemma, in ZFfixfuntyp]
TIO_eq [lemma, in ZFfixfuntyp]
TIO_fun_ext [lemma, in ZFfixfuntyp]
TIO_incl [lemma, in ZFfixfuntyp]
TIO_initial [lemma, in ZFfixfuntyp]
TIO_intro [lemma, in ZFfixfuntyp]
TIO_mono [lemma, in ZFfixfuntyp]
TIO_mono_succ [lemma, in ZFfixfuntyp]
TIO_morph [instance, in ZFfixfuntyp]
TIO_morph [instance, in ZFfixfuntyp]
TIO_typ [lemma, in ZFfixfuntyp]
TI_elim [lemma, in ZFord]
TI_elim [lemma, in ZFordcl]
TI_eq [lemma, in ZFordcl]
TI_eq [lemma, in ZFord]
TI_fun_ext [lemma, in ZFord]
TI_fun_ext [lemma, in ZFordcl]
TI_incl [lemma, in ZFfix]
TI_initial [lemma, in ZFord]
TI_initial [lemma, in ZFordcl]
TI_intro [lemma, in ZFordcl]
TI_intro [lemma, in ZFord]
TI_mono [lemma, in ZFfix]
TI_mono_succ [lemma, in ZFfix]
TI_morph [instance, in ZFordcl]
TI_morph [instance, in ZFord]
TI_pre_fix [lemma, in ZFfix]
TI_typ [lemma, in ZFord]
TI_typ [lemma, in ZFordcl]
Tm [moduleid, in SN_CC]
tm_red1 [lemma, in SN_CC]
toOrd [axiom, in ModelCIC]
toOrd [definition, in ZFord]
toOrd_isOrd [lemma, in ZFord]
toOrd_isOrd [axiom, in ModelCIC]
toOrd_morph [axiom, in ModelCIC]
toOrd_morph [instance, in ZFord]
toOrd_morph [instance, in ModelCIC]
toOrd_ord [lemma, in ZFord]
toOrd_ord [axiom, in ModelCIC]
TR [definition, in ZFord]
TR [definition, in ZFordcl]
TransfiniteIteration [section, in ZFordcl]
TransfiniteIteration [section, in ZFfixfuntyp]
TransfiniteIteration [section, in ZFord]
TransfiniteIteration.F [variable, in ZFord]
TransfiniteIteration.F [variable, in ZFfixfuntyp]
TransfiniteIteration.F [variable, in ZFordcl]
TransfiniteIteration.Fmorph [variable, in ZFordcl]
TransfiniteIteration.Fmorph [variable, in ZFord]
TransfiniteIteration.Fmorph [variable, in ZFfixfuntyp]
TransfiniteRecursion [section, in ZFordcl]
TransfiniteRecursion [section, in ZFord]
TransfiniteRecursion.F [variable, in ZFordcl]
TransfiniteRecursion.F [variable, in ZFord]
TransfiniteRecursion.Fmorph [variable, in ZFord]
TransfiniteRecursion.Fmorph [variable, in ZFordcl]
trans_conv_conv [lemma, in TermECC]
trans_conv_conv [lemma, in Lambda]
trans_conv_conv [lemma, in Term]
trans_conv_exp [constructor, in Term]
trans_conv_exp [constructor, in Lambda]
trans_conv_exp [constructor, in TermECC]
trans_conv_red [constructor, in TermECC]
trans_conv_red [constructor, in Lambda]
trans_conv_red [constructor, in Term]
trans_eq_map [lemma, in IntMap]
trans_red [constructor, in TermECC]
trans_red [constructor, in Lambda]
trans_red [constructor, in Term]
trans_red_red [lemma, in Term]
trans_red_red [lemma, in TermECC]
TRUE [definition, in ModelZF]
TRUE [definition, in ZFindtypes]
true_typ [lemma, in ZFindtypes]
trunc [inductive, in MyList]
trunc_O [constructor, in MyList]
trunc_S [constructor, in MyList]
TR_eqn [lemma, in ZFord]
TR_eqn [lemma, in ZFordcl]
TR_ind [lemma, in ZFordcl]
TR_ind [lemma, in ZFord]
TR_morph [instance, in ZFordcl]
TR_morph [instance, in ZFord]
TR_rel [definition, in ZFord]
TR_rel [definition, in ZFordcl]
TR_rel_choice_pred [lemma, in ZFord]
TR_rel_choice_pred [lemma, in ZFordcl]
TR_rel_def [lemma, in ZFord]
TR_rel_def [lemma, in ZFordcl]
TR_rel_fun [lemma, in ZFord]
TR_rel_fun [lemma, in ZFordcl]
TR_rel_intro [lemma, in ZFordcl]
TR_rel_intro [lemma, in ZFord]
TR_rel_inv [lemma, in ZFord]
TR_rel_inv [lemma, in ZFordcl]
TR_rel_morph [instance, in ZFord]
TR_rel_morph [instance, in ZFordcl]
TR_rel_repl_rel [lemma, in ZFord]
TR_rel_repl_rel [lemma, in ZFordcl]
TR_typ [lemma, in ZFordcl]
TR_typ [lemma, in ZFord]
TWO [abbreviation, in HF]
Ty [definition, in ModelCIC]
Ty [moduleid, in SN_CC]
typ [inductive, in Types]
typ [inductive, in TypeECC]
Typage [section, in Types]
Typage [section, in TypeJudge]
Typage [section, in TypeECC]
Typage [section, in TypeJudgeECC]
Typage.CC_Is_Functional [section, in TypeJudge]
Typage.Equivalence1 [section, in TypeJudge]
type [definition, in ModelCIC]
TypeECC [library]
TypeJudge [library]
TypeJudgeECC [library]
Types [library]
type_abs [constructor, in TypeECC]
type_abs [constructor, in Types]
type_abs [constructor, in TypeJudge]
type_abs [constructor, in TypeJudgeECC]
type_app [constructor, in TypeECC]
type_app [constructor, in TypeJudge]
type_app [constructor, in TypeJudgeECC]
type_app [constructor, in Types]
type_beta [constructor, in TypeJudgeECC]
type_beta [constructor, in TypeJudge]
type_case [lemma, in TypeECC]
type_case [lemma, in TypeJudge]
type_case [lemma, in Types]
type_case [lemma, in TypeJudgeECC]
type_conv [lemma, in TypeJudgeECC]
type_conv [constructor, in Types]
type_conv [constructor, in TypeECC]
type_conv_gen [lemma, in TypeJudgeECC]
type_eq_conv [lemma, in TypeJudge]
type_eq_conv_gen [lemma, in TypeJudge]
type_exp [constructor, in TypeJudge]
type_exp [constructor, in TypeJudgeECC]
type_kind [constructor, in TypeECC]
type_kind [constructor, in TypeJudgeECC]
type_kind_not_conv [lemma, in Types]
type_prod [constructor, in TypeECC]
type_prod [constructor, in TypeJudge]
type_prod [constructor, in TypeJudgeECC]
type_prod [constructor, in Types]
type_prop [constructor, in TypeJudgeECC]
type_prop [constructor, in Types]
type_prop [constructor, in TypeECC]
type_prop [constructor, in TypeJudge]
type_red [constructor, in TypeJudgeECC]
type_red [constructor, in TypeJudge]
type_reduction [lemma, in Types]
type_reduction [lemma, in TypeECC]
type_var [constructor, in TypeECC]
type_var [constructor, in TypeJudge]
type_var [constructor, in TypeJudgeECC]
type_var [constructor, in Types]
typ_app' [lemma, in ModelCIC]
typ_app0 [lemma, in ModelCIC]
typ_change [lemma, in TypeJudge]
typ_conv_conv [lemma, in Types]
typ_conv_conv [lemma, in TypeECC]
typ_eq_typ [lemma, in TypeJudge]
typ_inversion [lemma, in TypeJudge]
typ_inversion [lemma, in Types]
typ_inversion [lemma, in TypeJudgeECC]
typ_inversion [lemma, in TypeECC]
typ_mem_kind [lemma, in Types]
typ_natcase [lemma, in ModelCIC]
typ_natI [lemma, in ModelCIC]
typ_nati [lemma, in ModelCIC]
typ_nat_fix [lemma, in ModelCIC]
typ_ord_kind [definition, in ModelCIC]
typ_ord_ord [definition, in ModelCIC]
typ_prod2 [lemma, in ModelCIC]
typ_Prop [lemma, in ModelCIC]
typ_red_env [lemma, in Types]
typ_red_env [lemma, in TypeJudge]
typ_red_env [lemma, in TypeECC]
typ_red_env [lemma, in TypeJudgeECC]
typ_red_env_raw [lemma, in TypeJudge]
typ_red_env_trans [lemma, in TypeJudge]
typ_refl [lemma, in TypeJudge]
typ_refl [lemma, in TypeJudgeECC]
typ_refl2 [lemma, in TypeJudge]
typ_refl2 [lemma, in TypeJudgeECC]
typ_sub [lemma, in TypeJudgeECC]
typ_sub [lemma, in TypeJudge]
typ_sub_weak [lemma, in Types]
typ_sub_weak [lemma, in TypeECC]
typ_succi [lemma, in ModelCIC]
typ_thin [lemma, in TypeJudge]
typ_thin [lemma, in TypeJudgeECC]
typ_thinning [lemma, in TypeJudgeECC]
typ_thinning [lemma, in TypeJudge]
typ_thinning_n [lemma, in TypeJudge]
typ_thinning_n [lemma, in TypeJudgeECC]
typ_Type [lemma, in ModelCIC]
typ_unique [lemma, in Types]
typ_unique [lemma, in TypeECC]
typ_var' [lemma, in ModelCIC]
typ_weak_weak [lemma, in TypeECC]
typ_weak_weak [lemma, in Types]
typ_wf [lemma, in TypeJudge]
typ_wf [lemma, in TypeECC]
typ_wf [lemma, in Types]
typ_wf [lemma, in TypeJudgeECC]
typ_zero [lemma, in ModelCIC]
ty_fix_body [lemma, in ModelCIC]


U

U [definition, in EnsUniv]
uchoice [definition, in ZFrepl]
uchoice_ax [lemma, in ZFrepl]
uchoice_def [lemma, in ZFrepl]
uchoice_ext [lemma, in ZFrepl]
uchoice_morph [lemma, in ZFrepl]
uchoice_morph_raw [instance, in ZFrepl]
uchoice_pred [definition, in ZFrepl]
union [definition, in HF]
Union [definition, in Can]
union2 [definition, in ZF]
union2_commut [lemma, in ZF]
union2_elim [lemma, in ZF]
union2_intro1 [lemma, in ZF]
union2_intro2 [lemma, in ZF]
union2_mono [lemma, in ZF]
union2_morph [instance, in ZF]
union_couple_eq [lemma, in HF]
union_couple_eq [lemma, in ZFpairs]
union_elim [lemma, in ZF]
union_elim [lemma, in HF]
union_empty_eq [lemma, in ZF]
union_equiv [lemma, in EnsUniv]
union_ext [lemma, in ZF]
union_ext [lemma, in HF]
union_intro [lemma, in ZF]
union_intro [lemma, in HF]
union_in_power [lemma, in ZF]
union_morph [instance, in ZF]
union_morph [instance, in HF]
union_singl [lemma, in HF]
union_singl_eq [lemma, in ZF]
union_subset_singl [lemma, in ZF]
UNIT [definition, in ZFindtypes]
unit_elim [lemma, in ZFindtypes]
unit_typ [lemma, in ZFindtypes]
unmark_app [definition, in TypeJudge]
unmark_conv_sort [lemma, in TypeJudge]
unmark_env [definition, in TypeJudge]
unmark_env_cons_inv [lemma, in TypeJudge]
unmark_env_item [lemma, in TypeJudge]
unmark_eq_conv [lemma, in TypeJudge]
unmark_item_lift [lemma, in TypeJudge]
unmark_lift [lemma, in TypeJudge]
unmark_prod_inv [lemma, in TypeJudge]
unmark_sort_inv [lemma, in TypeJudge]
unmark_sr [lemma, in TypeJudge]
unmark_subst [lemma, in TypeJudge]
unmark_subst0 [lemma, in TypeJudge]
unmark_subst2 [lemma, in TypeJudge]
U_elim [lemma, in EnsUniv]
U_intro [lemma, in EnsUniv]
U_univ [lemma, in EnsUniv]


V

valid_context [definition, in ModelHF]
val_mono [definition, in ModelCIC]
val_M_ok [lemma, in ModelCIC]
VarMap [library]
var_in_cand [lemma, in Can]
var_sub [lemma, in ModelCIC]
VN [definition, in ZFfix]
VNcard [lemma, in ZFfix]
VNcard' [lemma, in ZFfix]
VNlim_clos_power [lemma, in ZFfix]
VNlim_clos_union_repl [lemma, in ZFfix]
VNreg_clos_sup [lemma, in ZFfix]
VNsucc_power [lemma, in ZFfix]
VN_clos_union [lemma, in ZFfix]
VN_incl [lemma, in ZFfix]
VN_trans [lemma, in ZFfix]


W

WellFoundedSets [section, in ZFwf]
wf [inductive, in TypeJudgeECC]
wf [inductive, in TypeJudge]
wf [inductive, in TypeECC]
wf [inductive, in Types]
wf_morph [instance, in ZFord]
wf_morph [instance, in ZFord3]
wf_nil [constructor, in Types]
wf_nil [constructor, in TypeJudge]
wf_nil [constructor, in TypeECC]
wf_nil [constructor, in TypeJudgeECC]
wf_red_env_trans [lemma, in TypeJudge]
wf_sort [lemma, in TypeECC]
wf_sort [lemma, in Types]
wf_sort_lift [lemma, in Types]
wf_sort_lift [lemma, in TypeJudgeECC]
wf_sort_lift [lemma, in TypeECC]
wf_sort_lift [lemma, in TypeJudge]
wf_var [constructor, in TypeJudgeECC]
wf_var [constructor, in TypeJudge]
wf_var [constructor, in Types]
wf_var [constructor, in TypeECC]


Z

Zero [definition, in ModelCIC]
zero [definition, in ZFnats]
ZERO [definition, in ZFindtypes]
zero_omega [lemma, in ZFord]
ZERO_typ [lemma, in ZFindtypes]
zero_typ [lemma, in ZFnats]
zero_typ_e0 [lemma, in ZFord]
zero_typ_e0 [lemma, in ZFordcl]
ZERO_typ_gen [lemma, in ZFindtypes]
ZF [library]
ZFcard [library]
ZFcoc [library]
ZFdef [library]
ZFecc [library]
ZFfix [library]
ZFfixfuntyp [library]
ZFgrothendieck [library]
ZFindtypes [library]
ZFlambda [library]
ZFnats [library]
ZFord [library]
ZFordcl [library]
ZFord2 [library]
ZFord3 [library]
ZFord_equiv [library]
ZFpairs [library]
ZFrelations [library]
ZFrepl [library]
ZFskol [library]
ZFsum [library]
ZFwf [library]



Instance Index

A

abs_red_morph [in Lambda]
app_morph [in ZFrelations]
app_morph [in HFrelation]
app_red_morph [in Lambda]


B

Beq.eq_equiv [in ModelCIC]


C

cc_app_morph [in ZFcoc]
cc_app_morph [in HFcoc]
CC_Model.app_ext [in Models]
CC_Model.eqX_equiv [in Models]
CC_Model.in_ext [in Models]
conv_refl [in Lambda]
couple_morph [in ZFpairs]
couple_morph [in HF]


D

domain_morph [in HFrelation]


E

eqSAT_equiv [in Sat]
equi_card_morph [in ZFcard]
equi_card_refl [in ZFcard]
equi_card_sym [in ZFcard]
equi_card_trans [in ZFcard]
Eqv.eq_equiv [in VarMap]
eq_fun_sym [in ZF]
eq_fun_trans [in ZF]
eq_hf_equiv [in HF]
eq_hf_morph [in HF]
eq_hf_refl [in HF]
eq_hf_sym [in HF]
eq_hf_trans [in HF]
eq_pred_set [in ZF]
eq_set_equiv [in ZF]
ex2_mono [in basic]
ex2_morph [in basic]
ex_mono [in basic]
ex_morph [in basic]


F

fext_morph [in ModelCIC]
Fmono_morph [in ZFfix]
fst_morph [in HF]
fst_morph [in ZFpairs]
func_cons_morph [in HFrelation]
func_mono [in ZFrelations]
func_morph [in ZFrelations]


I

image_morph [in HFrelation]
incl_hf_morph [in HF]
incl_set_morph [in ZF]
incl_set_pre [in ZF]
inl_morph [in ZFsum]
inr_morph [in ZFsum]
inter_morph [in ZF]
In_hf_morph [in HF]
in_hf_morph [in HF]
in_set_morph [in ZF]
iSAT_morph [in ZFlambda]
isOrd_morph [in ZFord]
isOrd_morph [in ZFordcl]
isOrd_morph [in ZFord3]
isPOrd_morph [in ZFord2]


L

Lam.LAMf_mono [in ZFlambda]
Lam.LAMf_morph [in ZFlambda]
le_card_morph [in ZFcard]
le_card_refl [in ZFcard]
le_card_trans [in ZFcard]
le_morph [in ZFnats]
lt_morph [in ZFnats]


M

MakeModel.Abs_morph [in GenModelSN]
MakeModel.App_morph [in GenModelSN]
MakeModel.cons_morph [in GenModelSN]
MakeModel.cons_morph [in GenModelSN]
MakeModel.cons_morph [in GenModel]
MakeModel.cons_morph' [in GenModel]
MakeModel.cons_morph' [in GenModelSN]
MakeModel.cons_morph' [in GenModelSN]
MakeModel.cst_morph [in GenModelSN]
MakeModel.eq_intt_equiv [in GenModelSN]
MakeModel.eq_int_equiv [in ModelECC]
MakeModel.eq_trm_equiv [in GenModelSN]
MakeModel.eq_trm_refl [in GenModelSN]
MakeModel.eq_trm_sym [in GenModelSN]
MakeModel.eq_trm_trans [in GenModelSN]
MakeModel.eq_typ_morph [in GenModelSN]
MakeModel.eq_typ_setoid [in GenModelSN]
MakeModel.eq_val_equiv [in GenModel]
MakeModel.eq_val_equiv [in GenModelSN]
MakeModel.iint_morph [in GenModelSN]
MakeModel.ilift_morph [in GenModelSN]
MakeModel.int_morph [in GenModelSN]
MakeModel.int_morph [in ModelECC]
MakeModel.in_int_morph [in GenModelSN]
MakeModel.itm_morph [in GenModelSN]
MakeModel.J.eq_typ_morph [in GenModel]
MakeModel.J.sub_typ_morph [in GenModel]
MakeModel.J.typ_morph [in GenModel]
MakeModel.lams_morph [in GenModelSN]
MakeModel.lams_morph [in GenModelSN]
MakeModel.LCeq.eq_equiv [in GenModelSN]
MakeModel.lift_morph [in GenModelSN]
MakeModel.non_empty_morph [in GenModelSN]
MakeModel.Prod_morph [in GenModelSN]
MakeModel.R.eq_typ_equiv [in GenModel]
MakeModel.shift_morph [in GenModelSN]
MakeModel.shift_morph [in GenModelSN]
MakeModel.tm_morph [in GenModelSN]
MakeModel.typ_morph [in GenModelSN]
MakeModel.T.Abs_morph [in GenModel]
MakeModel.T.App_morph [in GenModel]
MakeModel.T.el_morph [in GenModel]
MakeModel.T.eq_term_refl [in GenModel]
MakeModel.T.eq_term_sym [in GenModel]
MakeModel.T.eq_term_trans [in GenModel]
MakeModel.T.int_morph [in GenModel]
MakeModel.T.lift_morph [in GenModel]
MakeModel.T.Prod_morph [in GenModel]
MakeModel.T.subst_morph [in GenModel]
MakeModel.Xeq.eq_equiv [in GenModelSN]
MakeModel.Xeq.eq_equiv [in GenModel]
Make.cons_morph [in VarMap]
Make.cons_morph' [in VarMap]
Make.lams_morph [in VarMap]
Make.shift_morph [in VarMap]
max_morph [in ZFnats]


N

NATCASE_morph [in ZFindtypes]
Natcase_morph [in ModelCIC]
NATf_mono [in ZFindtypes]
NATf_morph [in ZFindtypes]
NATi_morph [in ZFindtypes]
NATi_morph [in ModelCIC]
NATi_morph [in ZFindtypes]


O

ORDf_mono [in ZFindtypes]
ORDf_morph [in ZFindtypes]
ORDi_morph [in ZFindtypes]
osucc_morph [in ZFord]


P

pair_morph [in ZF]
pair_morph [in HF]
power_morph [in ZF]
pred_morph [in ZFnats]
prodcart_mono [in ZFpairs]
prodcart_morph [in ZFpairs]


R

red_refl [in Lambda]
red_trans [in Lambda]
rel_app_morph [in ZFrelations]
rel_image_morph [in ZFrelations]
rel_morph [in ZFrelations]
replf_mono_raw [in ZF]
replf_morph_raw [in ZF]
repl_mono_raw [in ZFrepl]
repl_morph_raw [in ZFrepl]


S

SatSet.inSAT_morph [in Sat]
SatSet.prodSAT_morph [in Sat]
SAT.inSAT_morph [in Sat]
SAT.prodSAT_morph [in Sat]
singl_morph [in HF]
singl_morph [in ZF]
Skolem.eq_setoid [in ZFskol]
Skolem.in_morph [in ZFskol]
Skolem.Nat_morph [in ZFskol]
Skolem.Zin_morph [in ZFskol]
Skolem.Zsetoid [in ZFskol]
Skolem.Z2set_morph [in ZFskol]
snd_morph [in ZFpairs]
snd_morph [in HF]
SN_addon.Red_morph [in GenModelSN]
sSAT_morph [in ZFlambda]
succ_morph [in ZFnats]
sum_morph [in ZFsum]
SyntacticModel.eqX_equiv [in ModelSyntax]


T

TIO_morph [in ZFfixfuntyp]
TIO_morph [in ZFfixfuntyp]
TI_morph [in ZFordcl]
TI_morph [in ZFord]
toOrd_morph [in ZFord]
toOrd_morph [in ModelCIC]
TR_morph [in ZFordcl]
TR_morph [in ZFord]
TR_rel_morph [in ZFord]
TR_rel_morph [in ZFordcl]


U

uchoice_morph_raw [in ZFrepl]
union2_morph [in ZF]
union_morph [in ZF]
union_morph [in HF]


W

wf_morph [in ZFord]
wf_morph [in ZFord3]



Projection Index

C

clos_exp [in Can]
clos_red [in Can]


G

G_pair [in EnsUniv]
G_pair [in ZFgrothendieck]
G_power [in ZFgrothendieck]
G_power [in EnsUniv]
G_trans [in ZFgrothendieck]
G_trans [in EnsUniv]
G_union_repl [in ZFgrothendieck]
G_union_repl [in EnsUniv]


I

incl_sn [in Can]


M

MakeModel.iint [in GenModelSN]
MakeModel.iint_morph [in GenModelSN]
MakeModel.itm [in GenModelSN]
MakeModel.itm_lift [in GenModelSN]
MakeModel.itm_morph [in GenModelSN]
MakeModel.itm_subst [in GenModelSN]



Record Index

G

grot_univ [in EnsUniv]
grot_univ [in ZFgrothendieck]


I

is_cand [in Can]


M

MakeModel.inftrm [in GenModelSN]



Lemma Index

A

Abs_sound_Arr [in Can]
Abs_sound_Pi [in Can]
app_def [in HFrelation]
app_defined [in ZFrelations]
app_elim [in ZFrelations]
app_typ [in ZFrelations]
app_typ1 [in ZFrelations]
app_typ2 [in ZFrelations]


B

beta_eq [in HFrelation]
beta_eq [in ZFrelations]
beta_morph [in HFcoc]
beta_rel_eq [in ZFrelations]
bool_elim [in ZFindtypes]


C

cancel_repeat [in HF]
cand_sat [in Can]
cand_sn [in Can]
canonical_correct [in HF]
cantor [in ZFcard]
cantor_le [in ZFcard]
CCM.app_ext [in ModelZF]
CCM.beta_eq [in ModelZF]
CCM.impredicative_prod [in ModelZF]
CCM.in_ext [in ModelZF]
CCM.lam_ext [in ModelZF]
CCM.prod_elim [in ModelZF]
CCM.prod_ext [in ModelZF]
CCM.prod_intro [in ModelZF]
CCSN.cc_impredicative_prod_non_empty [in SN_CC]
CCSN.prop_repl_morph [in SN_CC]
CCSN.sn_impredicative_prod [in SN_CC]
CCSN.sn_prod_elim [in SN_CC]
CCSN.sn_prod_intro [in SN_CC]
CCSN.sn_proof_of_false [in SN_CC]
cc_beta_eq [in ZFcoc]
cc_beta_eq [in HFcoc]
cc_consistency [in ModelHF]
cc_consistency [in ModelZF]
cc_eta_eq [in ZFcoc]
cc_impredicative_lam [in HFcoc]
cc_impredicative_lam [in ZFcoc]
cc_impredicative_prod [in ZFcoc]
cc_impredicative_prod [in HFcoc]
cc_lam_ext [in HFcoc]
cc_lam_ext [in ZFcoc]
cc_lam_fun1 [in ZFcoc]
cc_lam_fun2 [in ZFcoc]
cc_prod_covariant [in ZFcoc]
cc_prod_elim [in ZFcoc]
cc_prod_elim [in HFcoc]
cc_prod_ext [in HFcoc]
cc_prod_ext [in ZFcoc]
cc_prod_fun1 [in ZFcoc]
cc_prod_intro [in HFcoc]
cc_prod_intro [in ZFcoc]
cc_prod_univ [in ZFecc]
choose_elt [in HF]
church_rosser [in Lambda]
church_rosser [in Conv]
church_rosser [in TypeJudge]
church_rosser [in ConvECC]
ClassicOrdinal.ord_incl_le [in ZFordcl]
ClassicOrdinal.ord_total [in ZFordcl]
clos_trans_transp [in SN_CC]
commut_lift_subst [in Term]
commut_lift_subst [in TermECC]
commut_lift_subst [in Lambda]
commut_lift_subst_rec [in Lambda]
commut_lift_subst_rec [in Term]
commut_lift_subst_rec [in TermECC]
commut_red1_subterm [in TermECC]
commut_red1_subterm [in Term]
commut_red1_subterm [in Lambda]
compl_elim [in Can]
compl_intro [in Can]
confluence [in Lambda]
confluence [in TypeJudge]
confluence_par_red [in ConvECC]
confluence_par_red [in Conv]
confluence_red [in Conv]
confluence_red [in ConvECC]
cons_hf_cons [in HF]
cons_map_ext [in IntMap]
conv_conv_lift [in Lambda]
conv_conv_lift [in Term]
conv_conv_lift [in TermECC]
conv_conv_prod [in Term]
conv_conv_prod [in TermECC]
conv_conv_subst [in Lambda]
conv_conv_subst [in Term]
conv_conv_subst [in TermECC]
conv_kind_prop [in ConvECC]
conv_kind_prop [in Conv]
conv_sort [in ConvECC]
conv_sort [in Conv]
conv_sort_prod [in ConvECC]
conv_sort_prod [in Conv]
couple_injection [in ZFpairs]
couple_intro [in ZFpairs]
couple_intro_sigma [in ZFpairs]
cst_cont [in ZFindtypes]
cst_is_ext [in ZFindtypes]
cumul_Prop [in ModelCIC]
cumul_Type [in ModelCIC]


D

del_cons_map [in IntMap]
del_cons_map2 [in IntMap]
dep_func_elim [in ZFrelations]
dep_func_elim [in HFrelation]
dep_func_elim0 [in HFrelation]
dep_func_eta [in HFrelation]
dep_func_eta [in ZFrelations]
dep_func_ext [in ZFrelations]
dep_func_ext [in HFrelation]
dep_func_incl_func [in ZFrelations]
dep_func_intro [in HFrelation]
dep_func_intro [in ZFrelations]
dep_func_total [in HFrelation]
dep_image_ext [in ZFrelations]
df_morph1 [in HFrelation]
df_morph2 [in HFrelation]
discr [in ZFnats]
discr_lim_succ [in ZFordcl]
discr_lim_succ [in ZFord]
discr_power [in ZFcard]
discr_sum [in ZFsum]
distr_lift_subst [in Term]
distr_lift_subst [in TermECC]
distr_lift_subst [in Lambda]
distr_lift_subst_rec [in TermECC]
distr_lift_subst_rec [in Lambda]
distr_lift_subst_rec [in Term]
distr_subst [in Term]
distr_subst [in Lambda]
distr_subst [in TermECC]
distr_subst_rec [in Term]
distr_subst_rec [in TermECC]
distr_subst_rec [in Lambda]
down_eq [in EnsUniv]
down_in [in EnsUniv]


E

ECC.u_card_incl [in ModelECC]
ECC.u_card_in1 [in ModelECC]
ECC.u_card_in2 [in ModelECC]
ECC.u_card_prod [in ModelECC]
ECC.u_card_prod2 [in ModelECC]
ecc_grot [in ZFecc]
ecc_incl [in ZFecc]
ecc_in1 [in ZFecc]
ecc_in2 [in ZFecc]
ecc_prod [in ZFecc]
ecc_prod2 [in ZFecc]
empty_elim [in HF]
empty_ext [in ZF]
empty_ext [in HF]
empty_in_power [in ZF]
eqterm [in Term]
eqterm [in Lambda]
eqterm_subst_App [in ModelCIC]
equi_card_le [in ZFcard]
eq_cand_incl [in Can]
eq_can_Arr [in Can]
eq_can_compl [in Can]
eq_can_Inter [in Can]
eq_can_Pi [in Can]
eq_can_union [in Can]
eq_conv_abs [in TypeJudge]
eq_conv_abs_l [in TypeJudge]
eq_conv_abs_r [in TypeJudge]
eq_conv_app [in TypeJudge]
eq_conv_app_l [in TypeJudge]
eq_conv_app_m [in TypeJudge]
eq_conv_app_r [in TypeJudge]
eq_conv_conv [in TypeJudge]
eq_conv_exp [in TypeJudge]
eq_conv_inv [in TypeJudge]
eq_conv_inv2 [in TypeJudge]
eq_conv_lift [in TypeJudge]
eq_conv_prod [in TypeJudge]
eq_conv_prod_l [in TypeJudge]
eq_conv_prod_r [in TypeJudge]
eq_conv_red [in TypeJudge]
eq_conv_red_env [in TypeJudge]
eq_conv_refl [in TypeJudge]
eq_conv_sort_trans [in TypeJudge]
eq_conv_subst_r [in TypeJudge]
eq_conv_subst_ty_l [in TypeJudge]
eq_conv_sym [in TypeJudge]
eq_conv_trans [in TypeJudge]
eq_elim [in ZF]
eq_fun_ext [in ZF]
Eq_hf_cons [in HF]
Eq_hf_cons_hf [in HF]
eq_hf_elim1 [in HF]
eq_hf_elim2 [in HF]
eq_hf_fun_left [in HF]
eq_hf_fun_sym [in HF]
eq_hf_fun_trans [in HF]
Eq_hf_intro [in HF]
eq_hf_intro [in HF]
Eq_hf_split [in HF]
eq_index_eq [in ZF]
eq_index_sym [in ZF]
eq_intro [in ZF]
eq_red_conv [in TypeJudge]
eq_red_inv [in TypeJudge]
eq_red_inv2 [in TypeJudge]
eq_typ_eq_exp [in TypeJudgeECC]
eq_typ_eq_red [in TypeJudgeECC]
eq_typ_not_kind [in TypeJudge]
eq_typ_par_red0 [in TypeJudge]
eq_typ_red_env_unmark [in TypeJudge]
eq_typ_typ [in TypeJudge]
eq_typ_uniqueness [in TypeJudge]
exists_elt_true_elim [in HF]
exists_elt_true_intro [in HF]
exp_sort_mem [in Term]
ext_fun_ty [in ModelCIC]


F

false_typ [in ZFindtypes]
fa_mono [in basic]
fa_morph [in basic]
fext_lam [in ModelCIC]
fext_trans [in ModelCIC]
fold_set_ind [in HF]
fold_set_unfold [in HF]
forall_elt_case [in HF]
forall_elt_false_elim [in HF]
forall_elt_false_intro [in HF]
forall_elt_true_elim [in HF]
forall_elt_true_intro [in HF]
fst_def [in ZFpairs]
fst_def [in HF]
fst_typ [in ZFpairs]
fst_typ_sigma [in ZFpairs]
func_cont [in ZFindtypes]
func_eta [in ZFrelations]
func_is_ext [in ZFindtypes]
func_is_function [in ZFrelations]
func_map_image_elim [in HFrelation]
func_map_image_intro [in HFrelation]
func_narrow [in ZFrelations]
func_rel_incl [in ZFrelations]
fun_domain_func [in ZFrelations]
fun_elt_is_ext [in ZFrelations]
fun_item [in MyList]
fx_abs [in ModelCIC]
fx_eq_app [in ModelCIC]
fx_eq_noc [in ModelCIC]
fx_eq_rec_call [in ModelCIC]


G

Gmorph [in ZFord]
Gmorph [in ZFfixfuntyp]
Gmorph [in ZFordcl]
grot_empty [in ZFgrothendieck]
grot_inter [in ZFgrothendieck]
grot_intersection [in ZFgrothendieck]
grot_inter_unique [in ZFgrothendieck]
grot_succ_in [in ZFgrothendieck]
grot_succ_typ [in ZFgrothendieck]
grot_univ_ext [in ZFgrothendieck]
G_couple [in ZFgrothendieck]
G_dep_func [in ZFgrothendieck]
G_func [in ZFgrothendieck]
G_prodcart [in ZFgrothendieck]
G_rel [in ZFgrothendieck]
G_repl [in ZFgrothendieck]
G_replf [in ZFgrothendieck]
G_singl [in ZFgrothendieck]
G_subset [in ZFgrothendieck]
G_union [in ZFgrothendieck]
G_union2 [in ZFgrothendieck]


H

has_fin_limit [in ZFindtypes]
HF_Coc_Model.app_ext [in ModelHF]
HF_Coc_Model.beta_eq [in ModelHF]
HF_Coc_Model.impredicative_prod [in ModelHF]
HF_Coc_Model.in_ext [in ModelHF]
HF_Coc_Model.lam_ext [in ModelHF]
HF_Coc_Model.prod_elim [in ModelHF]
HF_Coc_Model.prod_ext [in ModelHF]
HF_Coc_Model.prod_intro [in ModelHF]
hf_elts_ext [in HF]
hf_ind2 [in HF]
hf_size_ind [in HF]


I

iff_impl [in basic]
iff_morph [in basic]
iLAM_inj [in ZFlambda]
iLAM_typ [in ZFlambda]
incl_eq [in ZF]
incl_hf_complete [in HF]
incl_hf_sound [in HF]
incl_le_card [in ZFcard]
increasing_le [in ZFordcl]
inject_rel_elim [in ZFrelations]
inject_rel_intro [in ZFrelations]
inject_rel_is_rel [in ZFrelations]
injU_elim [in EnsUniv]
inl_inj [in ZFsum]
inl_typ [in ZFsum]
inr_inj [in ZFsum]
inr_typ [in ZFsum]
ins_cons_map [in IntMap]
ins_eq [in MyList]
ins_gt [in MyList]
ins_item_ge [in Env]
ins_item_ge [in EnvECC]
ins_item_lift_ge [in EnvECC]
ins_item_lift_ge [in Env]
ins_item_lift_lt [in Env]
ins_item_lift_lt [in EnvECC]
ins_item_lt [in EnvECC]
ins_item_lt [in Env]
ins_le [in MyList]
interp_sound [in SN_CC]
interp_wf [in SN_CC]
interSAT_ax [in ZFlambda]
interSAT_morph_subset [in Sat]
inter_elim [in ZF]
inter_empty_eq [in ZF]
inter_ext [in ZF]
inter_intro [in ZF]
int_lift [in SN_CC]
int_lift_rec [in SN_CC]
int_not_kind [in SN_CC]
int_sound [in SN_CC]
int_subst [in SN_CC]
int_subst_rec [in SN_CC]
inv_conv_prod_l [in Conv]
inv_conv_prod_l [in ConvECC]
inv_conv_prod_r [in ConvECC]
inv_conv_prod_r [in Conv]
inv_lift_sort [in Term]
inv_lift_sort [in TermECC]
inv_nth_cs [in MyList]
inv_nth_nl [in MyList]
inv_par_red_abs [in Term]
inv_par_red_abs [in TermECC]
inv_prod_l [in TypeJudge]
inv_prod_r [in TypeJudge]
inv_subst_sort [in TermECC]
inv_subst_sort [in Term]
inv_type_conv [in TypeJudge]
inv_type_conv [in Types]
inv_type_conv [in TypeJudgeECC]
inv_type_conv [in TypeECC]
inv_typ_abs [in Types]
inv_typ_abs [in TypeECC]
inv_typ_app [in Types]
inv_typ_app [in TypeECC]
inv_typ_conv_kind [in Types]
inv_typ_kind [in Types]
inv_typ_kind [in TypeECC]
inv_typ_prod [in TypeECC]
inv_typ_prod [in Types]
inv_typ_prop [in Types]
inv_typ_prop [in TypeECC]
inv_typ_ref [in Types]
inv_typ_ref [in TypeECC]
In_app_elim [in HF]
In_app_hf_elim [in HF]
In_app_hf_left [in HF]
In_app_hf_right [in HF]
In_app_left [in HF]
In_app_right [in HF]
in_hf_elim [in HF]
In_hf_elim [in HF]
In_hf_elim_hf [in HF]
In_hf_head [in HF]
In_hf_head_hf [in HF]
in_hf_intro [in HF]
in_hf_reg_l [in HF]
in_hf_reg_r [in HF]
In_hf_tail [in HF]
In_hf_tail_hf [in HF]
in_map_inv [in HF]
iSAT_id [in ZFlambda]
isOrd_elim [in ZFord3]
isOrd_elim [in ZFordcl]
isOrd_epsilon0 [in ZFord]
isOrd_epsilon0 [in ZFordcl]
isOrd_eq [in ZFord]
isOrd_eq [in ZFordcl]
isOrd_equiv [in ZFord_equiv]
isOrd_eqv1 [in ZFord_equiv]
isOrd_ext [in ZFord]
isOrd_ext [in ZFordcl]
isOrd_ext [in ZFord3]
isOrd_ind [in ZFordcl]
isOrd_ind [in ZFord3]
isOrd_ind [in ZFord]
isOrd_intro [in ZFordcl]
isOrd_intro [in ZFord]
isOrd_intro0 [in ZFord3]
isOrd_inv [in ZFord3]
isOrd_inv [in ZFordcl]
isOrd_inv [in ZFord]
isOrd_iter_w [in ZFord]
isOrd_iter_w [in ZFordcl]
isOrd_le [in ZFordcl]
isOrd_N [in ZFordcl]
isOrd_omega [in ZFord]
isOrd_plump [in ZFord3]
isOrd_plump [in ZFord]
isOrd_succ [in ZFord]
isOrd_succ [in ZFordcl]
isOrd_sup [in ZFordcl]
isOrd_sup [in ZFord]
isOrd_supf [in ZFord]
isOrd_supf_elim [in ZFord]
isOrd_supf_intro [in ZFord]
isOrd_sup_elim [in ZFord]
isOrd_sup_elim [in ZFordcl]
isOrd_sup_intro [in ZFord]
isOrd_sup_intro [in ZFordcl]
isOrd_sup_rel [in ZFord]
isOrd_sup_rel [in ZFordcl]
isOrd_sup_rel_elim [in ZFordcl]
isOrd_sup_rel_elim [in ZFord]
isOrd_sup_rel_intro [in ZFord]
isOrd_sup_rel_intro [in ZFordcl]
isOrd_sup_rel_intro2 [in ZFordcl]
isOrd_sup_rel_intro2 [in ZFord]
isOrd_trans [in ZFordcl]
isOrd_trans [in ZFord3]
isOrd_trans [in ZFord]
isOrd_zero [in ZFord]
isOrd_zero [in ZFordcl]
isPOrd_succ [in ZFord2]
isPOrd_zero [in ZFord2]
isWf_antirefl [in ZFwf]
isWf_ext [in ZFwf]
isWf_ind [in ZFwf]
isWf_intro [in ZFwf]
isWf_inv [in ZFwf]
isWf_N [in ZFwf]
isWf_pair [in ZFwf]
isWf_power [in ZFwf]
isWf_repl [in ZFwf]
isWf_subset [in ZFwf]
isWf_succ [in ZFwf]
isWf_union [in ZFwf]
isWf_zero [in ZFwf]
is_cand_Arr [in Can]
is_cand_Pi [in Can]
is_cand_union [in Can]
is_cand_union1 [in Can]
is_cand_union2 [in Can]
is_can_compl [in Can]
is_can_Inter [in Can]
is_nat_succ [in ZFnats]
is_nat_zero [in ZFnats]
item_lift_fun [in Env]
item_trunc [in MyList]
IZF.choice' [in Ens]
IZF.choice' [in Ens0]
IZF.empty_ax [in Ens0]
IZF.empty_ax [in Ens]
IZF.empty_ex [in Ens]
IZF.empty_ex [in Ens0]
IZF.eq_elim [in Ens]
IZF.eq_elim [in Ens0]
IZF.eq_elim0 [in Ens]
IZF.eq_elim0 [in Ens0]
IZF.eq_intro [in Ens0]
IZF.eq_intro [in Ens]
IZF.eq_set_ax [in Ens]
IZF.eq_set_ax [in Ens0]
IZF.eq_set_def [in Ens]
IZF.eq_set_def [in Ens0]
IZF.eq_set_refl [in Ens]
IZF.eq_set_refl [in Ens0]
IZF.eq_set_sym [in Ens0]
IZF.eq_set_sym [in Ens]
IZF.eq_set_trans [in Ens]
IZF.eq_set_trans [in Ens0]
IZF.infinity_ex [in Ens0]
IZF.infinity_ex [in Ens]
IZF.infty_ax1 [in Ens0]
IZF.infty_ax1 [in Ens]
IZF.infty_ax2 [in Ens0]
IZF.infty_ax2 [in Ens]
IZF.in_reg [in Ens]
IZF.in_reg [in Ens0]
IZF.pair_ax [in Ens]
IZF.pair_ax [in Ens0]
IZF.pair_ex [in Ens0]
IZF.pair_ex [in Ens]
IZF.pair_morph [in Ens]
IZF.pair_morph [in Ens0]
IZF.power_ax [in Ens]
IZF.power_ax [in Ens0]
IZF.power_ex [in Ens0]
IZF.power_ex [in Ens]
IZF.power_morph [in Ens0]
IZF.power_morph [in Ens]
IZF.regularity_ax [in Ens]
IZF.regularity_ax [in Ens0]
IZF.repl0_ax [in Ens0]
IZF.repl0_ax [in Ens]
IZF.repl1_ax [in Ens]
IZF.repl1_ax [in Ens0]
IZF.repl1_morph [in Ens0]
IZF.repl1_morph [in Ens]
IZF.repl_ax [in Ens0]
IZF.repl_ax [in Ens]
IZF.repl_ex [in Ens0]
IZF.repl_ex [in Ens]
IZF.subset_ax [in Ens0]
IZF.subset_ax [in Ens]
IZF.union_ax [in Ens]
IZF.union_ax [in Ens0]
IZF.union_ex [in Ens0]
IZF.union_ex [in Ens]
IZF.union_morph [in Ens0]
IZF.union_morph [in Ens]


K

KSAT_intro [in Sat]


L

Lam.Abs_typ [in ZFlambda]
Lam.Abs_typ0 [in ZFlambda]
Lam.App_typ [in ZFlambda]
Lam.App_typ0 [in ZFlambda]
Lam.Cst_typ [in ZFlambda]
Lam.Cst_typ0 [in ZFlambda]
Lam.Lambda_elim [in ZFlambda]
Lam.Lambda_eqn [in ZFlambda]
Lam.Lambda_fix [in ZFlambda]
Lam.Lambda_ind [in ZFlambda]
Lam.Lambda_intro [in ZFlambda]
Lam.LAMf_ind [in ZFlambda]
Lam.Lamn_case [in ZFlambda]
Lam.Lamn_eq [in ZFlambda]
Lam.Lamn_incl [in ZFlambda]
Lam.Lamn_incl_succ [in ZFlambda]
Lam.Var_typ [in ZFlambda]
Lam.Var_typ0 [in ZFlambda]
lam_domain [in HFrelation]
lam_elim [in HFrelation]
lam_ext [in HFrelation]
lam_intro [in HFrelation]
lam_is_func [in ZFrelations]
lam_is_function [in ZFrelations]
lam_rel_is_func [in ZFrelations]
least_ord1 [in ZFordcl]
least_ord_morph [in ZFordcl]
le_case [in ZFnats]
le_lt_trans [in ZFord]
le_lt_trans [in ZFordcl]
le_refl [in ZFnats]
le_total [in ZFnats]
lift0 [in Lambda]
lift0 [in Term]
lift0 [in TermECC]
lift0_term [in ModelCIC]
lift10 [in ModelCIC]
lift_eq [in EnsUniv]
lift_in [in EnsUniv]
lift_rec0 [in Term]
lift_rec0 [in TermECC]
lift_rec0 [in Lambda]
lift_ref_ge [in Term]
lift_ref_ge [in TermECC]
lift_ref_ge [in Lambda]
lift_ref_lt [in Lambda]
lift_ref_lt [in Term]
lift_ref_lt [in TermECC]
limit'_is_ord [in ZFordcl]
limit_equiv [in ZFordcl]
limit_is_ord [in ZFord]
limit_is_ord [in ZFordcl]
limit_union [in ZFord]
limit_union_intro [in ZFord]
LIM_typ_gen [in ZFindtypes]
list_item [in MyList]
lt_antirefl [in ZFordcl]
lt_antirefl [in ZFord]
lt_card_lt [in ZFfix]
lt_card_non_zero [in ZFcard]
lt_is_le [in ZFnats]
lt_le_trans [in ZFordcl]
lt_mono [in ZFnats]
lt_osucc [in ZFord]
lt_osucc_compat [in ZFord]
lt_trans [in ZFnats]
lt_0_succ [in ZFnats]


M

MakeModel.add_var_eq_fun [in GenModel]
MakeModel.add_var_eq_fun [in GenModelSN]
MakeModel.discr_ref_prod [in GenModelSN]
MakeModel.eq_fun_sym [in ModelECC]
MakeModel.eq_fun_sym [in GenModel]
MakeModel.eq_fun_trans [in ModelECC]
MakeModel.eq_fun_trans [in GenModel]
MakeModel.eq_judge_beta [in ModelECC]
MakeModel.eq_judge_trans [in ModelECC]
MakeModel.eq_kind [in GenModelSN]
MakeModel.eq_trm_intro [in GenModelSN]
MakeModel.eq_typ_abs [in GenModelSN]
MakeModel.eq_typ_app [in GenModelSN]
MakeModel.eq_typ_beta [in GenModelSN]
MakeModel.eq_typ_prod [in GenModelSN]
MakeModel.ilift_binder [in GenModelSN]
MakeModel.ilift_binder_lift [in GenModelSN]
MakeModel.ilift_lams [in GenModelSN]
MakeModel.int_cons_lift_eq [in GenModelSN]
MakeModel.int_env_cons [in ModelECC]
MakeModel.int_lift [in ModelECC]
MakeModel.int_lift [in GenModelSyntax]
MakeModel.int_lift_eq [in GenModelSN]
MakeModel.int_lift_rec_eq [in GenModelSN]
MakeModel.int_not_kind [in GenModelSyntax]
MakeModel.int_sound [in ModelECC]
MakeModel.int_sound [in GenModelSyntax]
MakeModel.int_subst [in ModelECC]
MakeModel.int_subst [in GenModelSyntax]
MakeModel.int_subst0 [in ModelECC]
MakeModel.int_subst_eq [in GenModelSN]
MakeModel.int_subst_rec_eq [in GenModelSN]
MakeModel.in_int_intro [in GenModelSN]
MakeModel.in_int_not_kind [in GenModelSN]
MakeModel.in_int_sn [in GenModelSN]
MakeModel.in_int_varS [in GenModelSN]
MakeModel.in_int_var0 [in GenModelSN]
MakeModel.in_reg_r [in ModelECC]
MakeModel.judge_abs [in ModelECC]
MakeModel.judge_app [in ModelECC]
MakeModel.judge_beta [in ModelECC]
MakeModel.judge_conv [in ModelECC]
MakeModel.judge_kind [in ModelECC]
MakeModel.judge_prod [in ModelECC]
MakeModel.judge_prop [in ModelECC]
MakeModel.judge_var [in ModelECC]
MakeModel.lift1var [in GenModelSN]
MakeModel.non_empty_var_lift [in GenModelSN]
MakeModel.non_empty_witness [in GenModelSN]
MakeModel.non_provability [in GenModelSyntax]
MakeModel.prod_non_empty [in GenModelSN]
MakeModel.prop_non_empty [in GenModelSN]
MakeModel.refl [in GenModelSN]
MakeModel.R.eq_typ_abs [in GenModel]
MakeModel.R.eq_typ_app [in GenModel]
MakeModel.R.eq_typ_beta [in GenModel]
MakeModel.R.eq_typ_prod [in GenModel]
MakeModel.R.refl [in GenModel]
MakeModel.R.sub_refl [in GenModel]
MakeModel.R.sub_trans [in GenModel]
MakeModel.R.sym [in GenModel]
MakeModel.R.trans [in GenModel]
MakeModel.R.typ_abs [in GenModel]
MakeModel.R.typ_app [in GenModel]
MakeModel.R.typ_beta [in GenModel]
MakeModel.R.typ_conv [in GenModel]
MakeModel.R.typ_prod [in GenModel]
MakeModel.R.typ_prop [in GenModel]
MakeModel.R.typ_subsumption [in GenModel]
MakeModel.R.typ_var [in GenModel]
MakeModel.split_lift [in GenModelSN]
MakeModel.sym [in GenModelSN]
MakeModel.tm_liftable [in GenModelSN]
MakeModel.tm_lift_rec_eq [in GenModelSN]
MakeModel.tm_substitutive [in GenModelSN]
MakeModel.tm_subst_cons [in GenModelSN]
MakeModel.tm_subst_eq [in GenModelSN]
MakeModel.tm_subst_rec_eq [in GenModelSN]
MakeModel.trans [in GenModelSN]
MakeModel.typs_non_empty [in GenModelSN]
MakeModel.typs_not_kind [in GenModelSN]
MakeModel.typ_abs [in GenModelSN]
MakeModel.typ_app [in GenModelSN]
MakeModel.typ_beta [in GenModelSN]
MakeModel.typ_conv [in GenModelSN]
MakeModel.typ_prod [in GenModelSN]
MakeModel.typ_prop [in GenModelSN]
MakeModel.typ_sn [in GenModelSN]
MakeModel.typ_var [in GenModelSN]
MakeModel.T.el_subst_eq [in GenModel]
MakeModel.T.int_lift_rec_eq [in GenModel]
MakeModel.T.int_subst_eq [in GenModel]
MakeModel.T.int_subst_rec_eq [in GenModel]
MakeModel.T.lift0_term [in GenModel]
MakeModel.T.lift10 [in GenModel]
MakeModel.T.simpl_int_lift [in GenModel]
MakeModel.T.simpl_int_lift1 [in GenModel]
MakeModel.T.simpl_lift1 [in GenModel]
MakeModel.u_card_incl_le [in ModelECC]
MakeModel.vcons_add_var [in GenModelSN]
MakeModel.vcons_add_var [in GenModel]
MakeModel.vcons_add_var0 [in GenModelSN]
MakeModel.vcons_add_var0 [in GenModel]
MakeModel.wf_cons [in GenModelSN]
MakeModel.wf_nil [in GenModelSN]
MakeModel.wit_prod [in GenModelSN]
Make.cons_ext [in VarMap]
Make.cons_lams [in VarMap]
Make.lams0 [in VarMap]
Make.lams_bv [in VarMap]
Make.lams_shift [in VarMap]
Make.shift0 [in VarMap]
Make.shift_cons [in VarMap]
Make.shift_lams [in VarMap]
Make.shift_split [in VarMap]
max_eq [in ZFnats]
max_lt [in ZFnats]
max_sym [in ZFnats]
max_typ [in ZFnats]
mem_sort_lift [in Term]
mem_sort_lift [in TermECC]
mem_sort_subst [in Term]
mem_sort_subst [in TermECC]
morph_fix_body [in ModelCIC]
mpar_red1_refl [in TypeJudge]


N

NATCASE_choice_pred [in ZFindtypes]
NATCASE_def [in ZFindtypes]
NATCASE_SUCC [in ZFindtypes]
Natcase_succ [in ModelCIC]
NATCASE_typ [in ZFindtypes]
Natcase_zero [in ModelCIC]
NATCASE_ZERO [in ZFindtypes]
NATfun_ext [in ZFindtypes]
NATf_case [in ZFindtypes]
NATf_discr [in ZFindtypes]
NATi_case [in ZFindtypes]
NATi_fix [in ZFindtypes]
NATi_NAT [in ZFindtypes]
NATi_pre_typ [in ZFindtypes]
NATi_sub [in ModelCIC]
natOrd [in ZFordcl]
NATREC_eqn [in ModelCIC]
NATREC_expand [in ModelCIC]
NATREC_inv [in ModelCIC]
NATREC_morph [in ModelCIC]
NATREC_step [in ModelCIC]
NATREC_wt [in ModelCIC]
nat2NAT_reflect [in ZFindtypes]
nat2ordset_typ [in ZFord]
nat2set_inj [in ZFnats]
nat2set_reflect [in ZFnats]
nat2set_typ [in ZFnats]
NAT_continuous [in ZFindtypes]
NAT_eq [in ZFindtypes]
NAT_fix [in ZFindtypes]
nat_fix_eq [in ModelCIC]
NAT_ind [in ZFindtypes]
nat_ind_def [in ModelCIC]
NAT_typ [in ZFindtypes]
nf_uniqueness [in ConvECC]
nf_uniqueness [in Conv]
noc_app [in ModelCIC]
noc_kind [in ModelCIC]
noc_prop [in ModelCIC]
noc_var [in ModelCIC]
no_universal_set [in ZF]
nth_sound [in MyList]
nth_sub_eq [in Env]
nth_sub_eq [in EnvECC]
nth_sub_inf [in Env]
nth_sub_inf [in EnvECC]
nth_sub_sup [in EnvECC]
nth_sub_sup [in Env]
N_ind [in ZFnats]
N_limit_ord [in ZFordcl]


O

ole_lts [in ZFord]
olts_le [in ZFord]
omega_in_omega [in ZF]
omega_limit_ord [in ZFord]
omega_not_in_omega [in ZF]
one_step_conv_exp [in TermECC]
one_step_conv_exp [in Term]
one_step_red [in Term]
one_step_red [in Lambda]
one_step_red [in TermECC]
ORDfun_ext [in ZFindtypes]
ORDf_case [in ZFindtypes]
ORDi_case [in ZFindtypes]
ORDi_fix [in ZFindtypes]
ORDi_ORD [in ZFindtypes]
ORDi_pre_typ [in ZFindtypes]
ord2set_typ [in ZFord]
ord2set_typ [in ZFordcl]
ORD_eq [in ZFindtypes]
ord_le_incl [in ZFordcl]
ORD_typ [in ZFindtypes]
osucc_omega [in ZFord]
OSucc_sub [in ModelCIC]


P

pair_commut [in ZF]
pair_elim [in ZF]
pair_elim [in HF]
pair_equiv [in EnsUniv]
pair_ext [in ZF]
pair_intro1 [in ZF]
pair_intro1 [in HF]
pair_intro2 [in HF]
pair_intro2 [in ZF]
pair_inv [in ZF]
par_red1_lift [in TermECC]
par_red1_lift [in Term]
par_red1_subst [in Term]
par_red1_subst [in TermECC]
par_red_red [in TermECC]
par_red_red [in Term]
permute_lift [in Lambda]
permute_lift [in Term]
permute_lift [in TermECC]
permute_lift_rec [in Lambda]
permute_lift_rec [in Term]
permute_lift_rec [in TermECC]
plump_Acc [in ZFord]
plump_Acc [in ZFord3]
plump_bound [in ZFord3]
plump_bound [in ZFord]
plump_morph [in ZFord]
plump_morph [in ZFord3]
power_elim [in ZF]
power_elim [in HF]
power_equiv [in EnsUniv]
power_ext [in HF]
power_ext [in ZF]
power_intro [in ZF]
power_intro [in HF]
power_mono [in ZF]
power_morph [in HF]
pred_succ_eq [in ZFnats]
pred_typ [in ZFnats]


R

raw_choose_elt [in HF]
redp_abs [in Lambda]
redp_app_l [in Lambda]
redp_app_r [in Lambda]
redp_K [in Lambda]
redp_lift_rec [in Lambda]
red1_beta [in Lambda]
red1_lift [in Lambda]
red1_lift [in Term]
red1_lift [in TermECC]
red1_mpar_red1 [in TypeJudge]
red1_par_red1 [in Term]
red1_par_red1 [in TermECC]
red1_red_ind [in Term]
red1_red_ind [in TermECC]
red1_subst_l [in TermECC]
red1_subst_l [in Term]
red1_subst_l [in Lambda]
red1_subst_r [in TermECC]
red1_subst_r [in Lambda]
red1_subst_r [in Term]
red_conv [in Term]
red_conv [in TermECC]
red_conv [in Lambda]
red_env_unmark_conv [in TypeJudge]
red_item [in EnvECC]
red_item [in TypeJudge]
red_item [in Env]
red_item [in TypeJudgeECC]
red_normal [in Term]
red_normal [in TermECC]
red_par_red [in Term]
red_par_red [in TermECC]
red_prod_prod [in Term]
red_prod_prod [in TypeJudge]
red_prod_prod [in TermECC]
red_prod_prod_eq [in TypeJudge]
red_red_abs [in Lambda]
red_red_abs [in TermECC]
red_red_abs [in Term]
red_red_app [in TermECC]
red_red_app [in Lambda]
red_red_app [in Term]
red_red_prod [in TermECC]
red_red_prod [in Term]
red_sort_mem [in TermECC]
red_sort_mem [in Term]
red_sort_sort [in Term]
red_sort_sort [in TermECC]
red_sym_conv [in Lambda]
refl_eq_map [in IntMap]
refl_par_red1 [in Term]
refl_par_red1 [in TermECC]
regularity_ax [in HF]
relation_is_rel [in ZFrelations]
rel_comp_intro [in ZFrelations]
rel_domain_incl [in ZFrelations]
rel_domain_intro [in ZFrelations]
rel_image_ex [in ZFrelations]
rel_image_incl [in ZFrelations]
rel_image_intro [in ZFrelations]
rel_is_relation [in ZFrelations]
rel_mono [in ZFrelations]
replf_ax [in ZF]
replf_elim [in ZF]
replf_empty [in ZF]
replf_ext [in ZF]
replf_intro [in ZF]
replf_mono2 [in ZF]
replf_morph [in ZF]
replf_morph_gen [in ZF]
replSAT_ax [in ZFlambda]
repl1_equiv [in EnsUniv]
repl_elim [in ZFrepl]
repl_elim [in HF]
repl_empty [in ZFrepl]
repl_ext [in ZFrepl]
repl_ext [in HF]
repl_intro [in HF]
repl_intro [in ZFrepl]
repl_mono2 [in ZFrepl]
repl_morph [in HF]
repl_rel_compat_lemma [in ZFrepl]
repl_rel_fun [in ZFrepl]
repl_rel_incl [in ZFfix]
repl_sup [in ZFord]
repl_sup [in ZFordcl]
repl_sup_rel [in ZFord]
repl_sup_rel [in ZFordcl]


S

SatSet.eqSAT_def [in Sat]
SatSet.interSAT_elim [in Sat]
SatSet.interSAT_intro [in Sat]
SatSet.interSAT_morph [in Sat]
SatSet.prodSAT_elim [in Sat]
SatSet.prodSAT_intro [in Sat]
SatSet.sat_sn [in Sat]
SatSet.snSAT_intro [in Sat]
SatSet.varSAT [in Sat]
sigma_morph [in ZFpairs]
simpl_int_lift [in ModelCIC]
simpl_int_lift1 [in ModelCIC]
simpl_lift [in Term]
simpl_lift [in TermECC]
simpl_lift [in Lambda]
simpl_lift1 [in ModelCIC]
simpl_lift_rec [in Lambda]
simpl_lift_rec [in TermECC]
simpl_lift_rec [in Term]
simpl_subst [in Lambda]
simpl_subst [in TermECC]
simpl_subst [in Term]
simpl_subst_rec [in TermECC]
simpl_subst_rec [in Term]
simpl_subst_rec [in Lambda]
singl_elim [in HF]
singl_elim [in ZF]
singl_ext [in ZF]
singl_ext [in HF]
singl_inj [in ZF]
singl_intro [in HF]
singl_intro [in ZF]
singl_intro_eq [in ZF]
Skolem.downR_fun [in ZFskol]
Skolem.downR_morph [in ZFskol]
Skolem.empty_ax [in ZFskol]
Skolem.empty_sig [in ZFskol]
Skolem.Eq_proj [in ZFskol]
Skolem.eq_set_ax [in ZFskol]
Skolem.eq_Zeq [in ZFskol]
Skolem.infinity_ax1 [in ZFskol]
Skolem.infinity_ax2 [in ZFskol]
Skolem.inZ_in [in ZFskol]
Skolem.In_intro [in ZFskol]
Skolem.in_inZ [in ZFskol]
Skolem.in_reg [in ZFskol]
Skolem.in_set_elim [in ZFskol]
Skolem.Nat_S [in ZFskol]
Skolem.pair_ax [in ZFskol]
Skolem.pair_sig [in ZFskol]
Skolem.power_ax [in ZFskol]
Skolem.power_sig [in ZFskol]
Skolem.regularity_ax [in ZFskol]
Skolem.repl0 [in ZFskol]
Skolem.repl0_mono [in ZFskol]
Skolem.repl_ax [in ZFskol]
Skolem.repl_mono [in ZFskol]
Skolem.repl_sig [in ZFskol]
Skolem.set_intro [in ZFskol]
Skolem.union_ax [in ZFskol]
Skolem.union_sig [in ZFskol]
Skolem.Zeq_eq [in ZFskol]
Skolem.Z2set_surj [in ZFskol]
snd_def [in ZFpairs]
snd_def [in HF]
snd_ext [in HF]
snd_typ [in ZFpairs]
snd_typ_sigma [in ZFpairs]
sn_abs [in Lambda]
SN_CC_addon.daemon_false [in SN_CC]
SN_CC_addon.Red_morph [in SN_CC]
SN_CC_addon.Red_prod [in SN_CC]
SN_CC_addon.Red_sort [in SN_CC]
SN_CC_Model.app_ext [in SN_CC]
SN_CC_Model.beta_eq [in SN_CC]
SN_CC_Model.eqX_equiv [in SN_CC]
SN_CC_Model.impredicative_prod [in SN_CC]
SN_CC_Model.in_ext [in SN_CC]
SN_CC_Model.lam_ext [in SN_CC]
SN_CC_Model.prod_elim [in SN_CC]
SN_CC_Model.prod_ext [in SN_CC]
SN_CC_Model.prod_intro [in SN_CC]
sn_K [in Lambda]
sn_prod [in TermECC]
sn_prod [in Term]
sn_red_sn [in Term]
sn_red_sn [in TermECC]
sn_red_sn [in Lambda]
sn_subst [in Term]
sn_subst [in Lambda]
sn_subst [in TermECC]
sn_tm [in SN_CC]
sort_uniqueness [in TypeJudge]
stab_fix_body [in ModelCIC]
strip_lemma [in ConvECC]
strip_lemma [in Conv]
strip_lemma [in TypeJudge]
strong_normalization [in SN_CC]
str_confl [in TypeJudge]
str_confluence_par_red1 [in ConvECC]
str_confluence_par_red1 [in Conv]
subject_reduction [in TypeECC]
subject_reduction [in TypeJudge]
subject_reduction [in Types]
subj_red [in TypeECC]
subj_red [in Types]
subset_ax [in ZF]
subset_elim1 [in ZF]
subset_elim1 [in HF]
subset_elim2 [in ZF]
subset_elim2 [in HF]
subset_elim2_gen [in HF]
subset_empty1 [in HF]
subset_equiv [in EnsUniv]
subset_ext [in HF]
subset_ext [in ZF]
subset_intro [in HF]
subset_intro [in ZF]
subset_intro_gen [in HF]
subset_morph [in ZF]
subset_morph_ext [in HF]
subset_singl [in HF]
substitution [in Types]
substitution [in TypeJudge]
substitution [in TypeJudgeECC]
substitution [in TypeECC]
subst_ref_eq [in Term]
subst_ref_eq [in TermECC]
subst_ref_eq [in Lambda]
subst_ref_gt [in Term]
subst_ref_gt [in Lambda]
subst_ref_gt [in TermECC]
subst_ref_lt [in TermECC]
subst_ref_lt [in Term]
subst_ref_lt [in Lambda]
subterm_sn [in Lambda]
subterm_sn [in TermECC]
subterm_sn [in Term]
sub_item_lift_eq [in Env]
sub_item_lift_eq [in EnvECC]
sub_item_lift_sup [in EnvECC]
sub_item_lift_sup [in Env]
succ_equiv [in ZFord_equiv]
SUCC_inj [in ZFindtypes]
succ_inj [in ZFnats]
succ_intro1 [in ZFnats]
succ_intro2 [in ZFnats]
SUCC_typ [in ZFindtypes]
succ_typ [in ZFnats]
SUCC_typ_gen [in ZFindtypes]
sum_cont [in ZFindtypes]
sum_ext_natf [in ZFindtypes]
sum_ext_ordf [in ZFindtypes]
sum_ind [in ZFsum]
sum_is_ext [in ZFindtypes]
sum_mono [in ZFsum]
sup_ax [in ZF]
sup_ext [in ZF]
sup_incl [in ZF]
sup_morph [in ZF]
sup_morph_gen [in ZF]
surj_pair [in ZFpairs]
sym_conv [in Term]
sym_conv [in TermECC]
sym_eq_map [in IntMap]


T

thinning [in Types]
thinning [in TypeECC]
thinning_n [in TypeECC]
thinning_n [in Types]
TIO_elim [in ZFfixfuntyp]
TIO_eq [in ZFfixfuntyp]
TIO_fun_ext [in ZFfixfuntyp]
TIO_incl [in ZFfixfuntyp]
TIO_initial [in ZFfixfuntyp]
TIO_intro [in ZFfixfuntyp]
TIO_mono [in ZFfixfuntyp]
TIO_mono_succ [in ZFfixfuntyp]
TIO_typ [in ZFfixfuntyp]
TI_elim [in ZFord]
TI_elim [in ZFordcl]
TI_eq [in ZFordcl]
TI_eq [in ZFord]
TI_fun_ext [in ZFord]
TI_fun_ext [in ZFordcl]
TI_incl [in ZFfix]
TI_initial [in ZFord]
TI_initial [in ZFordcl]
TI_intro [in ZFordcl]
TI_intro [in ZFord]
TI_mono [in ZFfix]
TI_mono_succ [in ZFfix]
TI_pre_fix [in ZFfix]
TI_typ [in ZFord]
TI_typ [in ZFordcl]
tm_red1 [in SN_CC]
toOrd_isOrd [in ZFord]
toOrd_ord [in ZFord]
trans_conv_conv [in TermECC]
trans_conv_conv [in Lambda]
trans_conv_conv [in Term]
trans_eq_map [in IntMap]
trans_red_red [in Term]
trans_red_red [in TermECC]
true_typ [in ZFindtypes]
TR_eqn [in ZFord]
TR_eqn [in ZFordcl]
TR_ind [in ZFordcl]
TR_ind [in ZFord]
TR_rel_choice_pred [in ZFord]
TR_rel_choice_pred [in ZFordcl]
TR_rel_def [in ZFord]
TR_rel_def [in ZFordcl]
TR_rel_fun [in ZFord]
TR_rel_fun [in ZFordcl]
TR_rel_intro [in ZFordcl]
TR_rel_intro [in ZFord]
TR_rel_inv [in ZFord]
TR_rel_inv [in ZFordcl]
TR_rel_repl_rel [in ZFord]
TR_rel_repl_rel [in ZFordcl]
TR_typ [in ZFordcl]
TR_typ [in ZFord]
type_case [in TypeECC]
type_case [in TypeJudge]
type_case [in Types]
type_case [in TypeJudgeECC]
type_conv [in TypeJudgeECC]
type_conv_gen [in TypeJudgeECC]
type_eq_conv [in TypeJudge]
type_eq_conv_gen [in TypeJudge]
type_kind_not_conv [in Types]
type_reduction [in Types]
type_reduction [in TypeECC]
typ_app' [in ModelCIC]
typ_app0 [in ModelCIC]
typ_change [in TypeJudge]
typ_conv_conv [in Types]
typ_conv_conv [in TypeECC]
typ_eq_typ [in TypeJudge]
typ_inversion [in TypeJudge]
typ_inversion [in Types]
typ_inversion [in TypeJudgeECC]
typ_inversion [in TypeECC]
typ_mem_kind [in Types]
typ_natcase [in ModelCIC]
typ_natI [in ModelCIC]
typ_nati [in ModelCIC]
typ_nat_fix [in ModelCIC]
typ_prod2 [in ModelCIC]
typ_Prop [in ModelCIC]
typ_red_env [in Types]
typ_red_env [in TypeJudge]
typ_red_env [in TypeECC]
typ_red_env [in TypeJudgeECC]
typ_red_env_raw [in TypeJudge]
typ_red_env_trans [in TypeJudge]
typ_refl [in TypeJudge]
typ_refl [in TypeJudgeECC]
typ_refl2 [in TypeJudge]
typ_refl2 [in TypeJudgeECC]
typ_sub [in TypeJudgeECC]
typ_sub [in TypeJudge]
typ_sub_weak [in Types]
typ_sub_weak [in TypeECC]
typ_succi [in ModelCIC]
typ_thin [in TypeJudge]
typ_thin [in TypeJudgeECC]
typ_thinning [in TypeJudgeECC]
typ_thinning [in TypeJudge]
typ_thinning_n [in TypeJudge]
typ_thinning_n [in TypeJudgeECC]
typ_Type [in ModelCIC]
typ_unique [in Types]
typ_unique [in TypeECC]
typ_var' [in ModelCIC]
typ_weak_weak [in TypeECC]
typ_weak_weak [in Types]
typ_wf [in TypeJudge]
typ_wf [in TypeECC]
typ_wf [in Types]
typ_wf [in TypeJudgeECC]
typ_zero [in ModelCIC]
ty_fix_body [in ModelCIC]


U

uchoice_ax [in ZFrepl]
uchoice_def [in ZFrepl]
uchoice_ext [in ZFrepl]
uchoice_morph [in ZFrepl]
union2_commut [in ZF]
union2_elim [in ZF]
union2_intro1 [in ZF]
union2_intro2 [in ZF]
union2_mono [in ZF]
union_couple_eq [in HF]
union_couple_eq [in ZFpairs]
union_elim [in ZF]
union_elim [in HF]
union_empty_eq [in ZF]
union_equiv [in EnsUniv]
union_ext [in ZF]
union_ext [in HF]
union_intro [in ZF]
union_intro [in HF]
union_in_power [in ZF]
union_singl [in HF]
union_singl_eq [in ZF]
union_subset_singl [in ZF]
unit_elim [in ZFindtypes]
unit_typ [in ZFindtypes]
unmark_conv_sort [in TypeJudge]
unmark_env_cons_inv [in TypeJudge]
unmark_env_item [in TypeJudge]
unmark_eq_conv [in TypeJudge]
unmark_item_lift [in TypeJudge]
unmark_lift [in TypeJudge]
unmark_prod_inv [in TypeJudge]
unmark_sort_inv [in TypeJudge]
unmark_sr [in TypeJudge]
unmark_subst [in TypeJudge]
unmark_subst0 [in TypeJudge]
unmark_subst2 [in TypeJudge]
U_elim [in EnsUniv]
U_intro [in EnsUniv]
U_univ [in EnsUniv]


V

val_M_ok [in ModelCIC]
var_in_cand [in Can]
var_sub [in ModelCIC]
VNcard [in ZFfix]
VNcard' [in ZFfix]
VNlim_clos_power [in ZFfix]
VNlim_clos_union_repl [in ZFfix]
VNreg_clos_sup [in ZFfix]
VNsucc_power [in ZFfix]
VN_clos_union [in ZFfix]
VN_incl [in ZFfix]
VN_trans [in ZFfix]


W

wf_red_env_trans [in TypeJudge]
wf_sort [in TypeECC]
wf_sort [in Types]
wf_sort_lift [in Types]
wf_sort_lift [in TypeJudgeECC]
wf_sort_lift [in TypeECC]
wf_sort_lift [in TypeJudge]


Z

zero_omega [in ZFord]
ZERO_typ [in ZFindtypes]
zero_typ [in ZFnats]
zero_typ_e0 [in ZFord]
zero_typ_e0 [in ZFordcl]
ZERO_typ_gen [in ZFindtypes]



Section Index

B

Beta_Reduction [in Lambda]
Beta_Reduction [in Term]
Beta_Reduction [in TermECC]


C

Church_Rosser [in Conv]
Church_Rosser [in ConvECC]
Completion [in Can]


E

Example [in ModelCIC]


G

GrothendieckUniverse [in ZFgrothendieck]


I

Inaccessible [in ZFfix]
InaccessibleCard [in ZFfix]
IterMonotone [in ZFfix]
IterMonotone [in ZFfixfuntyp]


L

Lam.LambdaTerms [in ZFlambda]
LiftAndSubstEquiv [in SN_CC]
LimOrd [in ZFord]
LimOrd [in ZFordcl]
LimOrdRel [in ZFordcl]
LimOrdRel [in ZFord]
Listes [in MyList]


M

MakeModel.T.Lift [in GenModel]
MakeModel.T.Substitution [in GenModel]
Map [in IntMap]


N

NatFixRules [in ModelCIC]
NatOrd_theory [in ZFindtypes]
NatOrd_theory.IterationNat [in ZFindtypes]
NatOrd_theory.IterationOrd [in ZFindtypes]
NatOrd_theory.NatFixpoint [in ZFindtypes]
NatOrd_theory.NatUniverse [in ZFindtypes]
NatOrd_theory.OrdFixpoint [in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse [in ZFindtypes]
NatRec [in ModelCIC]
NatRec.NATREC_Eqn [in ModelCIC]
Normalisation_Forte [in TermECC]
Normalisation_Forte [in Term]


O

OrdinalUpperBound [in ZFord]


P

ProductContinuity [in ZFindtypes]


R

Reduction [in EnvECC]
Reduction [in Env]
Russel [in ZF]


S

StrongNormalisation [in Lambda]


T

TarskiGrothendieck [in ZFgrothendieck]
Termes [in TermECC]
Termes [in Term]
Terms [in Lambda]
TransfiniteIteration [in ZFordcl]
TransfiniteIteration [in ZFfixfuntyp]
TransfiniteIteration [in ZFord]
TransfiniteRecursion [in ZFordcl]
TransfiniteRecursion [in ZFord]
Typage [in Types]
Typage [in TypeJudge]
Typage [in TypeECC]
Typage [in TypeJudgeECC]
Typage.CC_Is_Functional [in TypeJudge]
Typage.Equivalence1 [in TypeJudge]


W

WellFoundedSets [in ZFwf]



Constructor Index

A

Abs [in Lambda]
Abs [in Term]
Abs [in TermECC]
abs_par_red [in Term]
abs_par_red [in TypeJudge]
abs_par_red [in TermECC]
abs_red [in Lambda]
abs_red_l [in TermECC]
abs_red_l [in Term]
abs_red_r [in Term]
abs_red_r [in TermECC]
App [in Lambda]
App [in Term]
App [in TermECC]
app_par_red [in TermECC]
app_par_red [in Term]
app_par_red [in TypeJudge]
app_red_l [in Term]
app_red_l [in Lambda]
app_red_l [in TermECC]
app_red_r [in Term]
app_red_r [in TermECC]
app_red_r [in Lambda]


B

beta [in Lambda]
beta [in TermECC]
beta [in Term]


H

HF [in HF]


I

insert_hd [in MyList]
insert_tl [in MyList]
ins_O [in EnvECC]
ins_O [in Env]
ins_S [in EnvECC]
ins_S [in Env]
item_hd [in MyList]
item_tl [in MyList]
IZF.sup [in Ens0]
IZF.sup [in Ens]


K

kind [in TermECC]
kind [in Term]


M

mem_abs_l [in Term]
mem_abs_l [in TermECC]
mem_abs_r [in Term]
mem_abs_r [in TermECC]
mem_app_l [in TermECC]
mem_app_l [in Term]
mem_app_r [in TermECC]
mem_app_r [in Term]
mem_eq [in TermECC]
mem_eq [in Term]
mem_prod_l [in Term]
mem_prod_l [in TermECC]
mem_prod_r [in TermECC]
mem_prod_r [in Term]


O

OL [in ZFord]
OL [in ZFordcl]
OO [in ZFord]
OO [in ZFordcl]
OS [in ZFordcl]
OS [in ZFord]


P

par_beta [in TypeJudge]
par_beta [in Term]
par_beta [in TermECC]
Prod [in TermECC]
Prod [in Term]
prod_par_red [in TermECC]
prod_par_red [in Term]
prod_par_red [in TypeJudge]
prod_red_l [in TermECC]
prod_red_l [in Term]
prod_red_r [in TermECC]
prod_red_r [in Term]
prop [in TermECC]
prop [in Term]


R

red1_env_hd [in Env]
red1_env_hd [in TypeJudgeECC]
red1_env_hd [in TypeJudge]
red1_env_hd [in EnvECC]
red1_env_tl [in Env]
red1_env_tl [in TypeJudge]
red1_env_tl [in EnvECC]
red1_env_tl [in TypeJudgeECC]
Ref [in Term]
Ref [in Lambda]
Ref [in TermECC]
refl_conv [in Lambda]
refl_conv [in TermECC]
refl_conv [in Term]
refl_red [in Lambda]
refl_red [in TermECC]
refl_red [in Term]
ref_par_red [in TermECC]
ref_par_red [in Term]
ref_par_red [in TypeJudge]


S

sbtrm_abs [in Lambda]
sbtrm_abs_l [in Term]
sbtrm_abs_l [in TermECC]
sbtrm_abs_r [in TermECC]
sbtrm_abs_r [in Term]
sbtrm_app_l [in Lambda]
sbtrm_app_l [in TermECC]
sbtrm_app_l [in Term]
sbtrm_app_r [in TermECC]
sbtrm_app_r [in Term]
sbtrm_app_r [in Lambda]
sbtrm_prod_l [in Term]
sbtrm_prod_l [in TermECC]
sbtrm_prod_r [in TermECC]
sbtrm_prod_r [in Term]
Skolem.InSet [in ZFskol]
sort_par_red [in Term]
sort_par_red [in TypeJudge]
sort_par_red [in TermECC]
Srt [in TermECC]
Srt [in Term]
sub_O [in EnvECC]
sub_O [in Env]
sub_S [in EnvECC]
sub_S [in Env]
SyntacticModel.MemProp [in ModelSyntax]


T

trans_conv_exp [in Term]
trans_conv_exp [in Lambda]
trans_conv_exp [in TermECC]
trans_conv_red [in TermECC]
trans_conv_red [in Lambda]
trans_conv_red [in Term]
trans_red [in TermECC]
trans_red [in Lambda]
trans_red [in Term]
trunc_O [in MyList]
trunc_S [in MyList]
type_abs [in TypeECC]
type_abs [in Types]
type_abs [in TypeJudge]
type_abs [in TypeJudgeECC]
type_app [in TypeECC]
type_app [in TypeJudge]
type_app [in TypeJudgeECC]
type_app [in Types]
type_beta [in TypeJudgeECC]
type_beta [in TypeJudge]
type_conv [in Types]
type_conv [in TypeECC]
type_exp [in TypeJudge]
type_exp [in TypeJudgeECC]
type_kind [in TypeECC]
type_kind [in TypeJudgeECC]
type_prod [in TypeECC]
type_prod [in TypeJudge]
type_prod [in TypeJudgeECC]
type_prod [in Types]
type_prop [in TypeJudgeECC]
type_prop [in Types]
type_prop [in TypeECC]
type_prop [in TypeJudge]
type_red [in TypeJudgeECC]
type_red [in TypeJudge]
type_var [in TypeECC]
type_var [in TypeJudge]
type_var [in TypeJudgeECC]
type_var [in Types]


W

wf_nil [in Types]
wf_nil [in TypeJudge]
wf_nil [in TypeECC]
wf_nil [in TypeJudgeECC]
wf_var [in TypeJudgeECC]
wf_var [in TypeJudge]
wf_var [in Types]
wf_var [in TypeECC]



Inductive Index

C

conv [in TermECC]
conv [in Lambda]
conv [in Term]


E

eq_typ [in TypeJudge]
eq_typ [in TypeJudgeECC]


H

hf [in HF]


I

insert [in MyList]
ins_in_env [in Env]
ins_in_env [in EnvECC]
item [in MyList]
IZF.set_ [in Ens0]
IZF.set_ [in Ens]


M

mem_sort [in Term]
mem_sort [in TermECC]
mpar_red1 [in TypeJudge]


O

ord [in ZFordcl]
ord [in ZFord]


P

par_red1 [in TermECC]
par_red1 [in Term]


R

red [in Lambda]
red [in TermECC]
red [in Term]
red1 [in Term]
red1 [in Lambda]
red1 [in TermECC]
red1_in_env [in TypeJudgeECC]
red1_in_env [in EnvECC]
red1_in_env [in TypeJudge]
red1_in_env [in Env]


S

Skolem.in_set_ [in ZFskol]
sort [in TermECC]
sort [in Term]
subterm [in Term]
subterm [in Lambda]
subterm [in TermECC]
sub_in_env [in Env]
sub_in_env [in EnvECC]
SyntacticModel.mem [in ModelSyntax]


T

term [in Term]
term [in Lambda]
term [in TermECC]
trunc [in MyList]
typ [in Types]
typ [in TypeECC]


W

wf [in TypeJudgeECC]
wf [in TypeJudge]
wf [in TypeECC]
wf [in Types]



Abbreviation Index

E

EMPTY [in HF]


M

MakeModel.eq_intt [in GenModelSN]
MakeModel.eq_val [in GenModel]
MakeModel.eq_val [in GenModelSN]
MakeModel.intt [in GenModelSN]
MakeModel.val [in GenModel]
MakeModel.val [in GenModelSN]
morph1 [in HF]
morph1 [in ZF]
morph2 [in HF]
morph2 [in ZF]
morph3 [in HF]


O

ONE [in HF]


T

TWO [in HF]



Definition Index

A

app [in HFrelation]
app [in ZFrelations]
App2 [in Lambda]
app_hf [in HF]
Arr [in Can]


B

Beq.eq [in ModelCIC]
Beq.eq_equiv [in ModelCIC]
Beq.t [in ModelCIC]
BOOL [in ZFindtypes]


C

canonical [in HF]
CCLam [in ZFlambda]
CCM.app [in ModelZF]
CCM.eqX [in ModelZF]
CCM.eqX_equiv [in ModelZF]
CCM.eq_fun [in ModelZF]
CCM.inX [in ModelZF]
CCM.lam [in ModelZF]
CCM.prod [in ModelZF]
CCM.props [in ModelZF]
CCM.X [in ModelZF]
CCSN.El [in SN_CC]
CCSN.mkTY [in SN_CC]
CCSN.piSAT [in SN_CC]
CCSN.Red [in SN_CC]
CCSN.sn_lam [in SN_CC]
CCSN.sn_prod [in SN_CC]
CCSN.sn_props [in SN_CC]
cc_app [in HFcoc]
cc_app [in ZFcoc]
cc_lam [in ZFcoc]
cc_lam [in HFcoc]
CC_Model.eq_fun [in Models]
cc_prod [in ZFcoc]
cc_prod [in HFcoc]
compl [in Can]
complSAT [in ZFlambda]
cons_hf [in HF]
cons_map [in IntMap]
couple [in HF]
couple [in ZFpairs]
CR [in Can]


D

del_map [in IntMap]
dep_func [in ZFrelations]
dep_func [in HFrelation]
dep_image [in ZFrelations]
domain [in HFrelation]


E

ecc [in ZFecc]
ECC.u_card [in ModelECC]
ecc_prod [in TypeECC]
EM [in ModelZF]
empty [in HF]
env [in EnvECC]
env [in Env]
epsilon0 [in ZFordcl]
epsilon0 [in ZFord]
EQ [in ModelZF]
equi_card [in ZFcard]
eq_cand [in Can]
eq_conv [in TypeJudge]
eq_fun [in ZF]
Eq_hf [in HF]
eq_hf [in HF]
eq_hf_fun [in HF]
eq_hf_pred [in HF]
eq_index [in ZF]
eq_map [in IntMap]
eq_pred [in ZF]
eq_red [in TypeJudge]
eq_typ_eq [in TypeJudgeECC]
exists_elt [in HF]
EXT [in ModelZF]
ext_fun [in ZF]
ext_fun [in HFcoc]
ext_rel [in ZF]


F

FALSE [in ZFindtypes]
FALSE [in ModelZF]
fincreasing_bounded [in ModelCIC]
fold_set [in HF]
forall_elt [in HF]
forall_int_env [in ModelHF]
fst [in HF]
fst [in ZFpairs]
func [in ZFrelations]
func [in HFrelation]
func_cons [in HFrelation]
func_map_image [in HFrelation]
fx_equals [in ModelCIC]
fx_extends [in ModelCIC]
fx_sub [in ModelCIC]


G

G [in ZFord]
G [in ZFfixfuntyp]
G [in ZFordcl]
grothendieck [in ZFgrothendieck]
grot_succ [in ZFgrothendieck]
grot_succ_pred [in ZFgrothendieck]


H

hf_bool [in HF]
HF_Coc_Model.app [in ModelHF]
HF_Coc_Model.eqX [in ModelHF]
HF_Coc_Model.eqX_equiv [in ModelHF]
HF_Coc_Model.eq_fun [in ModelHF]
HF_Coc_Model.inX [in ModelHF]
HF_Coc_Model.lam [in ModelHF]
HF_Coc_Model.prod [in ModelHF]
HF_Coc_Model.props [in ModelHF]
HF_Coc_Model.X [in ModelHF]
hf_elts [in HF]
hf_false [in HF]
hf_pred_morph [in HF]
hf_true [in HF]


I

iLAM [in ZFlambda]
image [in HFrelation]
INAT [in ModelZF]
Incl_hf [in HF]
incl_hf [in HF]
incl_set [in ZF]
increasing [in ZFord]
increasing [in ZFordcl]
increasing_bounded [in ZFord]
indexed_relation [in Sat]
inject_rel [in ZFrelations]
injU [in EnsUniv]
inl [in ZFsum]
inr [in ZFsum]
ins_map [in IntMap]
inter [in ZF]
Inter [in Can]
interp [in SN_CC]
int_clos [in ModelHF]
int_env [in SN_CC]
int_trm [in SN_CC]
inv_type [in TypeECC]
inv_type [in TypeJudgeECC]
inv_type [in TypeJudge]
inv_type [in Types]
in_hf [in HF]
In_hf [in HF]
iSAT [in ZFlambda]
isCard [in ZFcard]
isOrd [in ZFord]
isOrd [in ZFord3]
isOrd [in ZFordcl]
isPOrd [in ZFord2]
isWf [in ZFwf]
is_function [in ZFrelations]
is_nat [in ZFnats]
is_relation [in ZFrelations]
item_lift [in Env]
item_lift [in EnvECC]
iter_w [in ZFordcl]
iter_w [in ZFord]
IZF.elts [in Ens]
IZF.elts [in Ens0]
IZF.elts' [in Ens]
IZF.elts' [in Ens0]
IZF.empty [in Ens]
IZF.empty [in Ens0]
IZF.eq_set [in Ens0]
IZF.eq_set [in Ens]
IZF.idx [in Ens0]
IZF.idx [in Ens]
IZF.infinity [in Ens0]
IZF.infinity [in Ens]
IZF.in_set [in Ens]
IZF.in_set [in Ens0]
IZF.num [in Ens0]
IZF.num [in Ens]
IZF.pair [in Ens0]
IZF.pair [in Ens]
IZF.power [in Ens0]
IZF.power [in Ens]
IZF.repl0 [in Ens]
IZF.repl0 [in Ens0]
IZF.repl1 [in Ens0]
IZF.repl1 [in Ens]
IZF.set [in Ens0]
IZF.set [in Ens]
IZF.subset [in Ens]
IZF.subset [in Ens0]
IZF.union [in Ens0]
IZF.union [in Ens]


K

K [in Lambda]


L

lam [in ZFrelations]
lam [in HFrelation]
Lam.Abs [in ZFlambda]
Lam.App [in ZFlambda]
Lam.Cst [in ZFlambda]
Lam.Lambda [in ZFlambda]
Lam.LAMf [in ZFlambda]
Lam.Lamn [in ZFlambda]
Lam.Var [in ZFlambda]
lam_rel [in ZFrelations]
le [in ZFnats]
least_ord [in ZFordcl]
le_card [in ZFcard]
lift [in Lambda]
lift [in TermECC]
lift [in Term]
lift_rec [in Term]
lift_rec [in TermECC]
lift_rec [in Lambda]
LIM [in ZFindtypes]
limitOrd [in ZFordcl]
limitOrd [in ZFord]
limitOrd' [in ZFordcl]
List [in MyList]
lt [in ZFnats]
lt_card [in ZFcard]


M

MakeModel.Abs [in GenModelSN]
MakeModel.App [in GenModelSN]
MakeModel.cst_fun [in GenModelSN]
MakeModel.EM [in GenModelSyntax]
MakeModel.env [in GenModel]
MakeModel.env [in GenModelSN]
MakeModel.EQ [in GenModelSyntax]
MakeModel.eq_int [in ModelECC]
MakeModel.eq_judge [in ModelECC]
MakeModel.eq_trm [in GenModelSN]
MakeModel.eq_typ [in GenModelSN]
MakeModel.EXT [in GenModelSyntax]
MakeModel.FALSE [in GenModelSyntax]
MakeModel.ilift [in GenModelSN]
MakeModel.INAT [in GenModelSyntax]
MakeModel.int [in GenModelSN]
MakeModel.int [in ModelECC]
MakeModel.int_env [in ModelECC]
MakeModel.int_env [in GenModelSyntax]
MakeModel.int_trm [in GenModelSyntax]
MakeModel.In_int [in ModelECC]
MakeModel.in_int [in GenModelSN]
MakeModel.judge [in ModelECC]
MakeModel.J.eq_typ [in GenModel]
MakeModel.J.sub_typ [in GenModel]
MakeModel.J.typ [in GenModel]
MakeModel.kind [in GenModelSN]
MakeModel.LCeq.eq [in GenModelSN]
MakeModel.LCeq.eq_equiv [in GenModelSN]
MakeModel.LCeq.t [in GenModelSN]
MakeModel.lift [in GenModelSN]
MakeModel.liftable [in GenModelSN]
MakeModel.lift_rec [in GenModelSN]
MakeModel.non_empty [in GenModelSN]
MakeModel.PI [in GenModelSyntax]
MakeModel.Prod [in GenModelSN]
MakeModel.prod_list [in GenModelSN]
MakeModel.prop [in GenModelSN]
MakeModel.Ref [in GenModelSN]
MakeModel.subst [in GenModelSN]
MakeModel.substitutive [in GenModelSN]
MakeModel.subst_rec [in GenModelSN]
MakeModel.tm [in GenModelSN]
MakeModel.trm [in GenModelSN]
MakeModel.TRUE [in GenModelSyntax]
MakeModel.typ [in GenModelSN]
MakeModel.typs [in GenModelSN]
MakeModel.T.Abs [in GenModel]
MakeModel.T.App [in GenModel]
MakeModel.T.cst [in GenModel]
MakeModel.T.el [in GenModel]
MakeModel.T.eq_term [in GenModel]
MakeModel.T.int [in GenModel]
MakeModel.T.kind [in GenModel]
MakeModel.T.lift [in GenModel]
MakeModel.T.lift1 [in GenModel]
MakeModel.T.lift_rec [in GenModel]
MakeModel.T.Prod [in GenModel]
MakeModel.T.prop [in GenModel]
MakeModel.T.Ref [in GenModel]
MakeModel.T.subst [in GenModel]
MakeModel.T.subst_rec [in GenModel]
MakeModel.T.term [in GenModel]
MakeModel.val_ok [in GenModelSN]
MakeModel.val_ok [in GenModel]
MakeModel.vnil [in GenModel]
MakeModel.vnil [in GenModelSN]
MakeModel.wf [in GenModelSN]
MakeModel.Xeq.eq [in GenModel]
MakeModel.Xeq.eq [in GenModelSN]
MakeModel.Xeq.eq_equiv [in GenModelSN]
MakeModel.Xeq.eq_equiv [in GenModel]
MakeModel.Xeq.t [in GenModelSN]
MakeModel.Xeq.t [in GenModel]
Make.cons [in VarMap]
Make.eq_map [in VarMap]
Make.lams [in VarMap]
Make.map [in VarMap]
Make.nil [in VarMap]
Make.shift [in VarMap]
map [in MyList]
max [in ZFnats]
minus2 [in ZF]
mult_w [in ZFord]
mult_w [in ZFordcl]
mu_lim [in ZFindtypes]
mu_lt [in ZFfix]
mu_ord [in ZFfix]
mu_ord [in ZFindtypes]
mu_ord [in ZFindtypes]
mu_regular [in ZFindtypes]


N

N [in ZFnats]
Nat [in ModelCIC]
NAT [in ZFindtypes]
Natcase [in ModelCIC]
NATCASE [in ZFindtypes]
NATCASE_rel [in ZFindtypes]
NATf [in ZFindtypes]
NatFix [in ModelCIC]
NatI [in ModelCIC]
Nati [in ModelCIC]
NATi [in ZFindtypes]
NATREC [in ModelCIC]
nat2NAT [in ZFindtypes]
nat2ordset [in ZFord]
nat2set [in ZFnats]
nat_ind [in ModelCIC]
nat_ind_typ [in ModelCIC]
neutral [in Can]
noccur [in ModelCIC]
normal [in Term]
normal [in Lambda]
normal [in TermECC]
nth_def [in MyList]


O

omega [in ZF]
omega [in ZFord]
ORD [in ZFindtypes]
Ord [in ModelCIC]
ORDf [in ZFindtypes]
ORDi [in ZFindtypes]
ord2set [in ZFord]
ord2set [in ZFordcl]
ord_sup [in ZFordcl]
ord_sup [in ZFord]
osucc [in ZFord2]
OSucc [in ModelCIC]
osucc [in ZFord]
o_ord [in ModelCIC]


P

pair [in HF]
par_red [in TermECC]
par_red [in Term]
PI [in ModelZF]
Pi [in Can]
plump [in ZFord3]
plump [in ZFord]
plus_w [in ZFordcl]
plus_w [in ZFord]
power [in HF]
pow_w [in ZFordcl]
pow_w [in ZFord]
pred [in ZFnats]
prf_trm [in HFcoc]
prf_trm [in ZFcoc]
prodcart [in ZFpairs]
props [in HFcoc]
props [in ZFcoc]


R

redp [in Lambda]
regular [in ZFcard]
regular' [in ZFcard]
regular_card [in ZFcard]
rel [in ZFrelations]
rel_app [in ZFrelations]
rel_comp [in ZFrelations]
rel_domain [in ZFrelations]
rel_image [in ZFrelations]
repl [in HF]
replf [in ZF]
replSAT [in ZFlambda]
repl_rel [in ZFrepl]


S

SatSet.daimon [in Sat]
SatSet.eqSAT [in Sat]
SatSet.inSAT [in Sat]
SatSet.interSAT [in Sat]
SatSet.prodSAT [in Sat]
SatSet.SAT [in Sat]
SatSet.snSAT [in Sat]
sigma [in ZFpairs]
singl [in ZF]
singl [in HF]
Skolem.downR [in ZFskol]
Skolem.empty [in ZFskol]
Skolem.eq_set [in ZFskol]
Skolem.funDom [in ZFskol]
Skolem.incl_set [in ZFskol]
Skolem.infinite [in ZFskol]
Skolem.infinite_sig [in ZFskol]
Skolem.in_set [in ZFskol]
Skolem.Nat [in ZFskol]
Skolem.pair [in ZFskol]
Skolem.power [in ZFskol]
Skolem.repl [in ZFskol]
Skolem.set [in ZFskol]
Skolem.union [in ZFskol]
Skolem.Z2set [in ZFskol]
sn [in Lambda]
sn [in TermECC]
sn [in Term]
snd [in HF]
snd [in ZFpairs]
SN_CC_addon.daemon [in SN_CC]
SN_CC_addon.Red [in SN_CC]
SN_CC_Model.app [in SN_CC]
SN_CC_Model.eqX [in SN_CC]
SN_CC_Model.eq_fun [in SN_CC]
SN_CC_Model.inX [in SN_CC]
SN_CC_Model.lam [in SN_CC]
SN_CC_Model.prod [in SN_CC]
SN_CC_Model.props [in SN_CC]
SN_CC_Model.X [in SN_CC]
sSAT [in ZFlambda]
stab_fix_prop [in ModelCIC]
stronglyInaccessibleCard [in ZFcard]
str_confluent [in ConvECC]
str_confluent [in Conv]
subset [in HF]
subset [in ZF]
subst [in Lambda]
subst [in Term]
subst [in TermECC]
subst_rec [in TermECC]
subst_rec [in Lambda]
subst_rec [in Term]
sub_typ_covariant [in ModelCIC]
succ [in ZFnats]
SUCC [in ZFindtypes]
SuccI [in ModelCIC]
succOrd [in ZFordcl]
succOrd [in ZFord]
sum [in ZFsum]
sup [in ZF]
sup_rel [in ZFord]
sup_rel [in ZFordcl]
SyntacticModel.eqX [in ModelSyntax]
SyntacticModel.X [in ModelSyntax]


T

TI [in ZFord]
TI [in ZFordcl]
TIO [in ZFfixfuntyp]
toOrd [in ZFord]
TR [in ZFord]
TR [in ZFordcl]
TRUE [in ModelZF]
TRUE [in ZFindtypes]
TR_rel [in ZFord]
TR_rel [in ZFordcl]
Ty [in ModelCIC]
type [in ModelCIC]
typ_ord_kind [in ModelCIC]
typ_ord_ord [in ModelCIC]


U

U [in EnsUniv]
uchoice [in ZFrepl]
uchoice_pred [in ZFrepl]
union [in HF]
Union [in Can]
union2 [in ZF]
UNIT [in ZFindtypes]
unmark_app [in TypeJudge]
unmark_env [in TypeJudge]


V

valid_context [in ModelHF]
val_mono [in ModelCIC]
VN [in ZFfix]


Z

Zero [in ModelCIC]
zero [in ZFnats]
ZERO [in ZFindtypes]



Axiom Index

C

CC_Model.app [in Models]
CC_Model.app_ext [in Models]
CC_Model.beta_eq [in Models]
CC_Model.eqX [in Models]
CC_Model.eqX_equiv [in Models]
CC_Model.impredicative_prod [in Models]
CC_Model.inX [in Models]
CC_Model.in_ext [in Models]
CC_Model.lam [in Models]
CC_Model.lam_ext [in Models]
CC_Model.prod [in Models]
CC_Model.prod_elim [in Models]
CC_Model.prod_ext [in Models]
CC_Model.prod_intro [in Models]
CC_Model.props [in Models]
CC_Model.X [in Models]
choice [in Choice]
ClassicOrdinal.EM [in ZFordcl]


E

ECC_Model.u_card [in Models]
ECC_Model.u_card_incl [in Models]
ECC_Model.u_card_in1 [in Models]
ECC_Model.u_card_in2 [in Models]
ECC_Model.u_card_prod [in Models]
ECC_Model.u_card_prod2 [in Models]
ecc_prod_fun [in TypeECC]
Eqv.eq [in VarMap]
Eqv.eq_equiv [in VarMap]
Eqv.t [in VarMap]
extends_app [in ModelCIC]


F

fextends [in ModelCIC]
fext_intro [in ModelCIC]
fext_morph [in ModelCIC]


G

gr [in ZFecc]


I

IZF_Ex_sig.empty_ex [in ZFdef]
IZF_Ex_sig.eq_set [in ZFdef]
IZF_Ex_sig.eq_set_ax [in ZFdef]
IZF_Ex_sig.infinity_ex [in ZFdef]
IZF_Ex_sig.in_reg [in ZFdef]
IZF_Ex_sig.in_set [in ZFdef]
IZF_Ex_sig.pair_ex [in ZFdef]
IZF_Ex_sig.power_ex [in ZFdef]
IZF_Ex_sig.regularity_ax [in ZFdef]
IZF_Ex_sig.repl_ex [in ZFdef]
IZF_Ex_sig.set [in ZFdef]
IZF_Ex_sig.union_ex [in ZFdef]
IZF_sig.empty [in ZFdef]
IZF_sig.empty_ax [in ZFdef]
IZF_sig.eq_set [in ZFdef]
IZF_sig.eq_set_ax [in ZFdef]
IZF_sig.infinite [in ZFdef]
IZF_sig.infinity_ax1 [in ZFdef]
IZF_sig.infinity_ax2 [in ZFdef]
IZF_sig.in_reg [in ZFdef]
IZF_sig.in_set [in ZFdef]
IZF_sig.pair [in ZFdef]
IZF_sig.pair_ax [in ZFdef]
IZF_sig.power [in ZFdef]
IZF_sig.power_ax [in ZFdef]
IZF_sig.regularity_ax [in ZFdef]
IZF_sig.repl [in ZFdef]
IZF_sig.repl_ax [in ZFdef]
IZF_sig.repl_mono [in ZFdef]
IZF_sig.set [in ZFdef]
IZF_sig.union [in ZFdef]
IZF_sig.union_ax [in ZFdef]


P

prd_sup [in ModelCIC]
prd_sup_lub [in ModelCIC]
prd_union [in ModelCIC]


S

SAT.daimon [in Sat]
SAT.eqSAT [in Sat]
SAT.eqSAT_def [in Sat]
SAT.inSAT [in Sat]
SAT.inSAT_morph [in Sat]
SAT.interSAT [in Sat]
SAT.interSAT_elim [in Sat]
SAT.interSAT_intro [in Sat]
SAT.interSAT_morph [in Sat]
SAT.prodSAT [in Sat]
SAT.prodSAT_elim [in Sat]
SAT.prodSAT_intro [in Sat]
SAT.prodSAT_morph [in Sat]
SAT.SAT [in Sat]
SAT.sat_sn [in Sat]
SAT.snSAT [in Sat]
SAT.snSAT_intro [in Sat]
SAT.varSAT [in Sat]
SN_addon.daemon [in GenModelSN]
SN_addon.daemon_false [in GenModelSN]
SN_addon.Red [in GenModelSN]
SN_addon.Red_morph [in GenModelSN]
SN_addon.Red_prod [in GenModelSN]
SN_addon.Red_sort [in GenModelSN]


T

toOrd [in ModelCIC]
toOrd_isOrd [in ModelCIC]
toOrd_morph [in ModelCIC]
toOrd_ord [in ModelCIC]



Moduleid Index

B

B [in ModelCIC]
B [in EnsUniv]
Beq [in ModelCIC]
BuildModel [in ModelZF]


C

CCM [in ModelZF]
CCSN [in SN_CC]
CC_Model [in Models]
ClassicOrdinal [in ZFordcl]


E

ECC [in ModelECC]
ECC.CC [in ModelECC]
ECC_Model [in Models]
ECC_Model.CC [in Models]
Eqv [in VarMap]


H

HF_Coc_Model [in ModelHF]


I

IZF [in Ens0]
IZF [in Ens]
IZF [in ZF]
IZF_Ex_sig [in ZFdef]
IZF_sig [in ZFdef]


L

Lam [in ZFlambda]
Lc [in GenModelSN]
Lc [in SN_CC]


M

Make [in VarMap]
MakeModel [in GenModel]
MakeModel [in ModelECC]
MakeModel [in GenModelSN]
MakeModel [in GenModelSyntax]
MakeModel.I [in GenModelSN]
MakeModel.J [in GenModel]
MakeModel.LCeq [in GenModelSN]
MakeModel.R [in GenModel]
MakeModel.T [in GenModel]
MakeModel.V [in GenModelSN]
MakeModel.V [in GenModel]
MakeModel.Xeq [in GenModelSN]
MakeModel.Xeq [in GenModel]


S

S [in EnsUniv]
SAT [in Sat]
SatSet [in Sat]
Skolem [in ZFskol]
SN [in SN_CC]
SN_addon [in GenModelSN]
SN_CC_addon [in SN_CC]
SN_CC_Model [in SN_CC]
Soundness [in ModelHF]
SyntacticModel [in ModelSyntax]


T

Tm [in SN_CC]
Ty [in SN_CC]



Variable Index

C

Completion.P [in Can]


G

GrothendieckUniverse.grot [in ZFgrothendieck]
GrothendieckUniverse.U [in ZFgrothendieck]


I

InaccessibleCard.mu [in ZFfix]
InaccessibleCard.mu_card [in ZFfix]
InaccessibleCard.mu_lim [in ZFfix]
InaccessibleCard.mu_regular [in ZFfix]
Inaccessible.mu [in ZFfix]
Inaccessible.mu_lim [in ZFfix]
Inaccessible.mu_ord [in ZFfix]
Inaccessible.mu_regular [in ZFfix]
IterMonotone.F [in ZFfix]
IterMonotone.F [in ZFfixfuntyp]
IterMonotone.Fmono [in ZFfix]
IterMonotone.Fmono [in ZFfixfuntyp]
IterMonotone.Fmorph [in ZFfixfuntyp]


L

Lam.LambdaTerms.A [in ZFlambda]
LimOrdRel.R [in ZFordcl]
LimOrdRel.R [in ZFord]
LimOrdRel.Rfun [in ZFordcl]
LimOrdRel.Rfun [in ZFord]
LimOrdRel.Rmorph [in ZFord]
LimOrdRel.Rmorph [in ZFordcl]
LimOrdRel.Rord [in ZFordcl]
LimOrdRel.Rord [in ZFord]
LimOrdRel.Rtot [in ZFord]
LimOrdRel.Rtot [in ZFordcl]
LimOrd.f [in ZFord]
LimOrd.f [in ZFordcl]
LimOrd.ford [in ZFord]
LimOrd.ford [in ZFordcl]
Listes.A [in MyList]


M

Map.A [in IntMap]


N

NatFixRules.e [in ModelCIC]
NatFixRules.eps [in ModelCIC]
NatFixRules.eps_ord [in ModelCIC]
NatFixRules.M [in ModelCIC]
NatFixRules.M_nk [in ModelCIC]
NatFixRules.O [in ModelCIC]
NatFixRules.stab [in ModelCIC]
NatFixRules.ty_M [in ModelCIC]
NatFixRules.ty_O [in ModelCIC]
NatFixRules.U [in ModelCIC]
NatOrd_theory.NatUniverse.has_cstr [in ZFindtypes]
NatOrd_theory.NatUniverse.has_empty [in ZFindtypes]
NatOrd_theory.NatUniverse.has_limit [in ZFindtypes]
NatOrd_theory.NatUniverse.U [in ZFindtypes]
NatOrd_theory.OrdFixpoint.mu [in ZFindtypes]
NatOrd_theory.OrdFixpoint.mu_strong [in ZFindtypes]
NatOrd_theory.OrdFixpoint.NAT_in_mu [in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.has_cstr [in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.has_empty [in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.mu_clos [in ZFindtypes]
NatOrd_theory.OrdFixpoint.OrdUniverse.U [in ZFindtypes]
NatRec.eps [in ModelCIC]
NatRec.epsOrd [in ModelCIC]
NatRec.F [in ModelCIC]
NatRec.Fm [in ModelCIC]
NatRec.Fstab [in ModelCIC]
NatRec.Ftyp [in ModelCIC]
NatRec.NATREC_Eqn.lt_eps [in ModelCIC]
NatRec.NATREC_Eqn.o [in ModelCIC]
NatRec.U [in ModelCIC]
NatRec.Um [in ModelCIC]


O

OrdinalUpperBound.f [in ZFord]
OrdinalUpperBound.f_ext [in ZFord]
OrdinalUpperBound.f_ord [in ZFord]
OrdinalUpperBound.I [in ZFord]


P

ProductContinuity.mu [in ZFindtypes]
ProductContinuity.mu_strong [in ZFindtypes]


R

Reduction.R [in EnvECC]
Reduction.R [in Env]
Reduction.R_lift [in EnvECC]
Reduction.R_lift [in Env]
Russel.U [in ZF]
Russel.universal [in ZF]


T

TarskiGrothendieck.gr [in ZFgrothendieck]
TransfiniteIteration.F [in ZFord]
TransfiniteIteration.F [in ZFfixfuntyp]
TransfiniteIteration.F [in ZFordcl]
TransfiniteIteration.Fmorph [in ZFordcl]
TransfiniteIteration.Fmorph [in ZFord]
TransfiniteIteration.Fmorph [in ZFfixfuntyp]
TransfiniteRecursion.F [in ZFordcl]
TransfiniteRecursion.F [in ZFord]
TransfiniteRecursion.Fmorph [in ZFord]
TransfiniteRecursion.Fmorph [in ZFordcl]



Library Index

B

basic


C

Can
Choice
Conv
ConvECC


E

Ens
EnsUniv
Ens0
Env
EnvECC


G

GenModel
GenModelSN
GenModelSyntax


H

HF
HFcoc
HFrelation


I

IntMap


L

Lambda
Library


M

ModelCIC
ModelECC
ModelHF
Models
ModelSyntax
ModelZF
MyList


S

Sat
SN_CC


T

Term
TermECC
TypeECC
TypeJudge
TypeJudgeECC
Types


V

VarMap


Z

ZF
ZFcard
ZFcoc
ZFdef
ZFecc
ZFfix
ZFfixfuntyp
ZFgrothendieck
ZFindtypes
ZFlambda
ZFnats
ZFord
ZFordcl
ZFord2
ZFord3
ZFord_equiv
ZFpairs
ZFrelations
ZFrepl
ZFskol
ZFsum
ZFwf



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 _ (2486 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 _ (179 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 _ (17 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 _ (4 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1252 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 _ (56 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 _ (168 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 _ (48 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 _ (14 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 _ (460 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 _ (96 entries)
Moduleid 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 _ (48 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 _ (87 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 _ (57 entries)

This page has been generated by coqdoc