| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (420 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (202 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Global Index
A
Ackermann [definition, in HFS.Ackermann]Ackermann [library]
adj [projection, in HFS.HF]
adj [definition, in HFS.Ackermann]
adj_incl [lemma, in HFS.HF]
adj_el [lemma, in HFS.HF]
adj_eld [lemma, in HFS.Model]
adj_diff [lemma, in HFS.Ackermann]
adj_mem [lemma, in HFS.Ackermann]
adj_el_strong [lemma, in HFS.Extensionality]
adj_nel [lemma, in HFS.Extensionality]
alpha [definition, in HFS.Model]
alpha_swap [lemma, in HFS.Model]
alpha_cancel [lemma, in HFS.Model]
alpha_ge [lemma, in HFS.Model]
alpha_le [lemma, in HFS.Model]
alpha_eq [lemma, in HFS.Model]
alpha_null [lemma, in HFS.Model]
alpha_equiv [lemma, in HFS.Model]
and_dec [instance, in HFS.Preliminaries]
B
BigIntersection [section, in HFS.Operations]BigIntersection.X [variable, in HFS.Operations]
BigUnion [section, in HFS.Operations]
BigUnion.X [variable, in HFS.Operations]
BinaryUnion [section, in HFS.Operations]
BinaryUnion.X [variable, in HFS.Operations]
bun [definition, in HFS.Operations]
bun_el [lemma, in HFS.Operations]
bun' [lemma, in HFS.Operations]
C
cancel [projection, in HFS.HF]cancel [lemma, in HFS.Ackermann]
card [inductive, in HFS.Cardinality]
cardA [constructor, in HFS.Cardinality]
Cardinality [library]
card_ord_normal [lemma, in HFS.Cardinality]
card_ord [lemma, in HFS.Cardinality]
card_invariance [lemma, in HFS.Cardinality]
card_fun [lemma, in HFS.Cardinality]
card_inv [lemma, in HFS.Cardinality]
card_wo_inv [lemma, in HFS.Cardinality]
card_inj [lemma, in HFS.Cardinality]
card_adj [lemma, in HFS.Cardinality]
card_empty' [lemma, in HFS.Cardinality]
card_empty [lemma, in HFS.Cardinality]
card_total [lemma, in HFS.Cardinality]
card_epot [lemma, in HFS.Cardinality]
card0 [constructor, in HFS.Cardinality]
categoricity [lemma, in HFS.Categoricity]
Categoricity [library]
chain [definition, in HFS.Operations]
Chain [section, in HFS.Operations]
chainA [lemma, in HFS.Operations]
chain_inter [lemma, in HFS.Operations]
chain_union [lemma, in HFS.Operations]
Chain.X [variable, in HFS.Operations]
choose_el [lemma, in HFS.HF]
complete_induction [lemma, in HFS.Ackermann]
D
dec [record, in HFS.Preliminaries]dec [inductive, in HFS.Preliminaries]
decision [projection, in HFS.Preliminaries]
decision [constructor, in HFS.Preliminaries]
decPred [record, in HFS.Preliminaries]
DecPred [constructor, in HFS.Preliminaries]
decPred_dec [projection, in HFS.Preliminaries]
decPred_p [projection, in HFS.Preliminaries]
dec_DM_or [lemma, in HFS.Preliminaries]
dec_eq_sym [lemma, in HFS.Preliminaries]
dec_trans [lemma, in HFS.Preliminaries]
dec_empty [lemma, in HFS.Ackermann]
dec_HF [instance, in HFS.Extensionality]
dec_ext [lemma, in HFS.Extensionality]
dec_part [lemma, in HFS.Extensionality]
dec_adj_el [lemma, in HFS.Extensionality]
dec_adj_incl [lemma, in HFS.Extensionality]
dec_0_incl [instance, in HFS.Extensionality]
dec_0_el [instance, in HFS.Extensionality]
dec_0_eq [instance, in HFS.Extensionality]
discrim [projection, in HFS.HF]
disjoint [lemma, in HFS.Ackermann]
div2 [definition, in HFS.Ackermann]
div2mul2add [lemma, in HFS.Ackermann]
div2Slt [lemma, in HFS.Ackermann]
div2SSlt [lemma, in HFS.Ackermann]
E
eld_elt [lemma, in HFS.Model]eltd [inductive, in HFS.Model]
eltdH [constructor, in HFS.Model]
eltdT [constructor, in HFS.Model]
el_asym [lemma, in HFS.Extensionality]
el_irrefl [lemma, in HFS.Extensionality]
emptyEq [lemma, in HFS.Ackermann]
epot [inductive, in HFS.Cardinality]
epotA [constructor, in HFS.Cardinality]
epot_dec [lemma, in HFS.Cardinality]
epot_Equivalence [instance, in HFS.Cardinality]
epot_empty [lemma, in HFS.Cardinality]
epot0 [constructor, in HFS.Cardinality]
eps_ind [lemma, in HFS.Extensionality]
eqType [record, in HFS.Preliminaries]
EqType [constructor, in HFS.Preliminaries]
eqType_dec [projection, in HFS.Preliminaries]
eqType_X [projection, in HFS.Preliminaries]
Equipotence [section, in HFS.Cardinality]
Equipotence.X [variable, in HFS.Cardinality]
_ == _ [notation, in HFS.Cardinality]
equiv [inductive, in HFS.Model]
equivCancel [constructor, in HFS.Model]
EquivCongruent [constructor, in HFS.Model]
EquivRefl [constructor, in HFS.Model]
equivSwap [constructor, in HFS.Model]
EquivSymm [constructor, in HFS.Model]
EquivTrans [constructor, in HFS.Model]
equiv_dec [lemma, in HFS.Model]
equiv_incl [lemma, in HFS.Model]
equiv_empty [lemma, in HFS.Model]
equiv_treeA_proper [instance, in HFS.Model]
equiv_Equivalence [instance, in HFS.Model]
eset [projection, in HFS.HF]
eset_incl [lemma, in HFS.HF]
eset_el [lemma, in HFS.HF]
Evaluation [section, in HFS.Tree]
Evaluation.adj [variable, in HFS.Tree]
Evaluation.eset [variable, in HFS.Tree]
Evaluation.sip [variable, in HFS.Tree]
Evaluation.X [variable, in HFS.Tree]
ExtDec [section, in HFS.Extensionality]
ExtDec.X [variable, in HFS.Extensionality]
extensionality [lemma, in HFS.Extensionality]
Extensionality [library]
F
F [section, in HFS.Categoricity]F [definition, in HFS.Categoricity]
False_dec [instance, in HFS.Preliminaries]
F_homo [lemma, in HFS.Categoricity]
F_cancel [lemma, in HFS.Categoricity]
F' [lemma, in HFS.Tree]
F.X [variable, in HFS.Categoricity]
F.Y [variable, in HFS.Categoricity]
G
Gamma [definition, in HFS.Cardinality]GammaS_eq [lemma, in HFS.Cardinality]
GammaS_eq' [lemma, in HFS.Cardinality]
Gamma_induction [lemma, in HFS.Cardinality]
Gamma_strict_incl [lemma, in HFS.Cardinality]
Gamma_ord_equiv [lemma, in HFS.Cardinality]
Gamma_range [lemma, in HFS.Cardinality]
Gamma_fixed_point [lemma, in HFS.Cardinality]
Gamma_equipotence [lemma, in HFS.Cardinality]
Gamma_idempotent [lemma, in HFS.Cardinality]
Gamma_coincidence [lemma, in HFS.Cardinality]
Gamma_ord [lemma, in HFS.Cardinality]
Gamma_card [lemma, in HFS.Cardinality]
Gamma0_eq' [lemma, in HFS.Cardinality]
Gamma0_eq [lemma, in HFS.Cardinality]
H
HF [section, in HFS.HF]HF [record, in HFS.HF]
HF [library]
HFS [module, in HFS.Tactics]
HFS [constructor, in HFS.HF]
HFS.forall_iff_R2L [lemma, in HFS.Tactics]
HFS.forall_iff_L2R [lemma, in HFS.Tactics]
hf_ind [projection, in HFS.HF]
hf_all_dec [instance, in HFS.Extensionality]
hf_ex_dec [instance, in HFS.Extensionality]
HF_Evaluation.X [variable, in HFS.Tree]
HF_Evaluation [section, in HFS.Tree]
HF.X [variable, in HFS.HF]
homo [definition, in HFS.Categoricity]
Homo [section, in HFS.Categoricity]
homo_unique [lemma, in HFS.Categoricity]
homo_R [lemma, in HFS.Categoricity]
Homo.X [variable, in HFS.Categoricity]
Homo.Y [variable, in HFS.Categoricity]
HT [definition, in HFS.Ordinals]
HT_trans [lemma, in HFS.Ordinals]
I
I [definition, in HFS.Tree]iff_dec [instance, in HFS.Preliminaries]
impl_dec [instance, in HFS.Preliminaries]
incl [definition, in HFS.Model]
incl_trans [lemma, in HFS.Model]
incl_antisym [lemma, in HFS.Extensionality]
incl_trans [lemma, in HFS.Extensionality]
incl_refl [lemma, in HFS.Extensionality]
incl_dec [instance, in HFS.Extensionality]
inter [definition, in HFS.Operations]
interA_incl_eq' [lemma, in HFS.Operations]
interA_incl_eq [lemma, in HFS.Operations]
inter_pair_eq [lemma, in HFS.Operations]
inter_sing_eq [lemma, in HFS.Operations]
inter_glb [lemma, in HFS.Operations]
inter_incl [lemma, in HFS.Operations]
inter_el_incl [lemma, in HFS.Operations]
inter_el [lemma, in HFS.Operations]
I' [definition, in HFS.Tree]
L
lto [inductive, in HFS.Model]ltoE [constructor, in HFS.Model]
ltoF [constructor, in HFS.Model]
ltoS [constructor, in HFS.Model]
lto_tricho [lemma, in HFS.Model]
lto_irrefl [lemma, in HFS.Model]
lto_irrefl' [lemma, in HFS.Model]
lto_trans [lemma, in HFS.Model]
M
mem [definition, in HFS.Ackermann]member [projection, in HFS.HF]
membership [lemma, in HFS.Ackermann]
membership_law_matters [definition, in HFS.HF]
membership_dec [lemma, in HFS.Extensionality]
mem_adj_iff [lemma, in HFS.Ackermann]
mem_add [lemma, in HFS.Ackermann]
mem_smaller [lemma, in HFS.Ackermann]
Model [library]
mod2 [definition, in HFS.Ackermann]
mod2_add_mul2 [lemma, in HFS.Ackermann]
muldiv_smaller [lemma, in HFS.Ackermann]
mul2 [definition, in HFS.Ackermann]
mul2div2_evenodd [lemma, in HFS.Ackermann]
mul2_larger_pres [lemma, in HFS.Ackermann]
mul2_larger_S [lemma, in HFS.Ackermann]
N
nat_eq_dec [instance, in HFS.Ackermann]nonempty [lemma, in HFS.HF]
not_dec [instance, in HFS.Preliminaries]
no_universal_set [lemma, in HFS.Extensionality]
O
Operations [library]ord [inductive, in HFS.Ordinals]
Ordinals [section, in HFS.Ordinals]
Ordinals [library]
Ordinals.X [variable, in HFS.Ordinals]
OrdS [constructor, in HFS.Ordinals]
ord_HT [lemma, in HFS.Ordinals]
ord_trans_ord [lemma, in HFS.Ordinals]
ord_chain' [lemma, in HFS.Ordinals]
ord_chain [lemma, in HFS.Ordinals]
ord_incl [lemma, in HFS.Ordinals]
ord_tricho [lemma, in HFS.Ordinals]
ord_mono [lemma, in HFS.Ordinals]
ord_sip [lemma, in HFS.Ordinals]
ord_inv [lemma, in HFS.Ordinals]
ord_pred' [lemma, in HFS.Ordinals]
ord_pred [lemma, in HFS.Ordinals]
ord_eset [lemma, in HFS.Ordinals]
ord_eset' [lemma, in HFS.Ordinals]
ord_ord [lemma, in HFS.Ordinals]
ord_trans [lemma, in HFS.Ordinals]
ord_dec [lemma, in HFS.Cardinality]
ord_canonical [lemma, in HFS.Cardinality]
Ord0 [constructor, in HFS.Ordinals]
or_dec [instance, in HFS.Preliminaries]
P
pair [definition, in HFS.Operations]Pairs [section, in HFS.Operations]
Pairs.X [variable, in HFS.Operations]
pair_injective [lemma, in HFS.Operations]
part [lemma, in HFS.Extensionality]
pi1 [definition, in HFS.Operations]
pi1_eq [lemma, in HFS.Operations]
pi2 [definition, in HFS.Operations]
pi2_eq [lemma, in HFS.Operations]
power [definition, in HFS.Operations]
Power [section, in HFS.Operations]
power_el [lemma, in HFS.Operations]
power' [lemma, in HFS.Operations]
Power.X [variable, in HFS.Operations]
pow2 [definition, in HFS.Ackermann]
pow2_larger [lemma, in HFS.Ackermann]
Preliminaries [library]
product [definition, in HFS.Operations]
product_el [lemma, in HFS.Operations]
pure [definition, in HFS.Preliminaries]
Pure [section, in HFS.Preliminaries]
pure_pir [lemma, in HFS.Preliminaries]
pure_equiv [lemma, in HFS.Preliminaries]
Pure.p [variable, in HFS.Preliminaries]
Pure.X [variable, in HFS.Preliminaries]
R
R [section, in HFS.Categoricity]R [inductive, in HFS.Categoricity]
rep [definition, in HFS.Operations]
Replacement [section, in HFS.Operations]
Replacement.f [variable, in HFS.Operations]
Replacement.X [variable, in HFS.Operations]
rep_el [lemma, in HFS.Operations]
rep' [lemma, in HFS.Operations]
right_inverse [lemma, in HFS.Preliminaries]
R_fun [lemma, in HFS.Categoricity]
R_functional.Y [variable, in HFS.Categoricity]
R_functional.X [variable, in HFS.Categoricity]
R_functional [section, in HFS.Categoricity]
R_sim [lemma, in HFS.Categoricity]
R_total [lemma, in HFS.Categoricity]
R_symm [lemma, in HFS.Categoricity]
R_adj [constructor, in HFS.Categoricity]
R_empty [constructor, in HFS.Categoricity]
R.X [variable, in HFS.Categoricity]
R.Y [variable, in HFS.Categoricity]
S
S [definition, in HFS.Tree]sep [definition, in HFS.Operations]
Separation [section, in HFS.Operations]
Separation.p [variable, in HFS.Operations]
Separation.X [variable, in HFS.Operations]
sep_el [lemma, in HFS.Operations]
sep' [lemma, in HFS.Operations]
set [projection, in HFS.HF]
SI [lemma, in HFS.Tree]
sigma [definition, in HFS.Model]
sigma_idem [lemma, in HFS.Model]
sigma_equiv_eq [lemma, in HFS.Model]
sigma_equiv [lemma, in HFS.Model]
SingUnorderedPair [section, in HFS.Operations]
SingUnorderedPair.X [variable, in HFS.Operations]
sing_injective [lemma, in HFS.Operations]
sing_el [lemma, in HFS.Operations]
sip [lemma, in HFS.Ackermann]
SIP [section, in HFS.Tree]
SIP.adj [variable, in HFS.Tree]
SIP.eset [variable, in HFS.Tree]
SIP.I [variable, in HFS.Tree]
SIP.S [variable, in HFS.Tree]
SIP.SI [variable, in HFS.Tree]
SIP.S_adj [variable, in HFS.Tree]
SIP.S_emp [variable, in HFS.Tree]
SIP.X [variable, in HFS.Tree]
SI' [lemma, in HFS.Tree]
SI2sip [lemma, in HFS.Tree]
subset_induction [lemma, in HFS.Cardinality]
Subtype [section, in HFS.Preliminaries]
Subtype.A [variable, in HFS.Preliminaries]
Subtype.f [variable, in HFS.Preliminaries]
Subtype.fp [variable, in HFS.Preliminaries]
Subtype.f_idem [variable, in HFS.Preliminaries]
Subtype.I [variable, in HFS.Preliminaries]
Subtype.I_injective [variable, in HFS.Preliminaries]
Subtype.S [variable, in HFS.Preliminaries]
Subtype.X [variable, in HFS.Preliminaries]
Subtype.X_eq_dec [variable, in HFS.Preliminaries]
sub_norm [lemma, in HFS.Preliminaries]
succ_inj [lemma, in HFS.Extensionality]
succ_inv [lemma, in HFS.Operations]
swap [projection, in HFS.HF]
swap [lemma, in HFS.Ackermann]
S' [definition, in HFS.Tree]
T
Tactics [library]tc [definition, in HFS.TC]
TC [definition, in HFS.TC]
TC [library]
tcA_eq [lemma, in HFS.TC]
tcE_eq [lemma, in HFS.TC]
tc_least [lemma, in HFS.TC]
tc_incl [lemma, in HFS.TC]
tc_trans [lemma, in HFS.TC]
tc_el [lemma, in HFS.TC]
TC_tc [lemma, in HFS.TC]
TC_adj [lemma, in HFS.TC]
TC_empty [lemma, in HFS.TC]
TC_fun [lemma, in HFS.TC]
TC_incl [lemma, in HFS.TC]
TC_trans [lemma, in HFS.TC]
tc' [lemma, in HFS.TC]
tdiscrim [lemma, in HFS.Model]
tel [inductive, in HFS.TC]
telI [constructor, in HFS.TC]
telT [constructor, in HFS.TC]
tel_dec [lemma, in HFS.TC]
tel_TC [lemma, in HFS.TC]
tel_adjR [lemma, in HFS.TC]
tel_adjL [lemma, in HFS.TC]
tel_inv [lemma, in HFS.TC]
tmember [lemma, in HFS.Model]
trans [definition, in HFS.HF]
TransitiveClosure [section, in HFS.TC]
TransitiveClosure.X [variable, in HFS.TC]
_ < _ [notation, in HFS.TC]
tree [inductive, in HFS.Tree]
Tree [library]
treeA [constructor, in HFS.Tree]
treeN [constructor, in HFS.Tree]
tree_extensionality [lemma, in HFS.Model]
tree_model [lemma, in HFS.Model]
tree_eq_dec [instance, in HFS.Tree]
True_dec [instance, in HFS.Preliminaries]
U
union [definition, in HFS.Operations]unionA_incl_eq' [lemma, in HFS.Operations]
unionA_incl_eq [lemma, in HFS.Operations]
unionE_eq [lemma, in HFS.Operations]
union_pair_eq [lemma, in HFS.Operations]
union_sing_eq [lemma, in HFS.Operations]
union_lub [lemma, in HFS.Operations]
union_incl [lemma, in HFS.Operations]
union_el_incl [lemma, in HFS.Operations]
union_el [lemma, in HFS.Operations]
union' [lemma, in HFS.Operations]
upair_sing [lemma, in HFS.Operations]
upair_injective [lemma, in HFS.Operations]
upair_el [lemma, in HFS.Operations]
W
WIP [section, in HFS.Tree]WIP.adj [variable, in HFS.Tree]
WIP.choice [variable, in HFS.Tree]
WIP.eset [variable, in HFS.Tree]
WIP.gamma [variable, in HFS.Tree]
WIP.wip [variable, in HFS.Tree]
WIP.X [variable, in HFS.Tree]
wip2sip [lemma, in HFS.Tree]
without [definition, in HFS.Ackermann]
Without [section, in HFS.Extensionality]
without [lemma, in HFS.Extensionality]
withoutA_neq [lemma, in HFS.Extensionality]
withoutA_eq [lemma, in HFS.Extensionality]
without_inverse [lemma, in HFS.Ackermann]
without_nin [lemma, in HFS.Extensionality]
without_el [lemma, in HFS.Extensionality]
Without.X [variable, in HFS.Extensionality]
other
Sigma _ .. _ , _ (type_scope) [notation, in HFS.Preliminaries]_ <<= _ [notation, in HFS.HF]
_ nel _ [notation, in HFS.HF]
_ el _ [notation, in HFS.HF]
_ @ _ [notation, in HFS.HF]
_ < _ [notation, in HFS.Model]
_ eld _ [notation, in HFS.Model]
_ elt _ [notation, in HFS.Model]
_ == _ [notation, in HFS.Model]
_ \\ _ [notation, in HFS.Extensionality]
_ @ _ [notation, in HFS.Tree]
eq_dec _ [notation, in HFS.Preliminaries]
inhab _ [notation, in HFS.HF]
0 [notation, in HFS.HF]
0 [notation, in HFS.Tree]
Notation Index
E
_ == _ [in HFS.Cardinality]T
_ < _ [in HFS.TC]other
Sigma _ .. _ , _ (type_scope) [in HFS.Preliminaries]_ <<= _ [in HFS.HF]
_ nel _ [in HFS.HF]
_ el _ [in HFS.HF]
_ @ _ [in HFS.HF]
_ < _ [in HFS.Model]
_ eld _ [in HFS.Model]
_ elt _ [in HFS.Model]
_ == _ [in HFS.Model]
_ \\ _ [in HFS.Extensionality]
_ @ _ [in HFS.Tree]
eq_dec _ [in HFS.Preliminaries]
inhab _ [in HFS.HF]
0 [in HFS.HF]
0 [in HFS.Tree]
Module Index
H
HFS [in HFS.Tactics]Variable Index
B
BigIntersection.X [in HFS.Operations]BigUnion.X [in HFS.Operations]
BinaryUnion.X [in HFS.Operations]
C
Chain.X [in HFS.Operations]E
Equipotence.X [in HFS.Cardinality]Evaluation.adj [in HFS.Tree]
Evaluation.eset [in HFS.Tree]
Evaluation.sip [in HFS.Tree]
Evaluation.X [in HFS.Tree]
ExtDec.X [in HFS.Extensionality]
F
F.X [in HFS.Categoricity]F.Y [in HFS.Categoricity]
H
HF_Evaluation.X [in HFS.Tree]HF.X [in HFS.HF]
Homo.X [in HFS.Categoricity]
Homo.Y [in HFS.Categoricity]
O
Ordinals.X [in HFS.Ordinals]P
Pairs.X [in HFS.Operations]Power.X [in HFS.Operations]
Pure.p [in HFS.Preliminaries]
Pure.X [in HFS.Preliminaries]
R
Replacement.f [in HFS.Operations]Replacement.X [in HFS.Operations]
R_functional.Y [in HFS.Categoricity]
R_functional.X [in HFS.Categoricity]
R.X [in HFS.Categoricity]
R.Y [in HFS.Categoricity]
S
Separation.p [in HFS.Operations]Separation.X [in HFS.Operations]
SingUnorderedPair.X [in HFS.Operations]
SIP.adj [in HFS.Tree]
SIP.eset [in HFS.Tree]
SIP.I [in HFS.Tree]
SIP.S [in HFS.Tree]
SIP.SI [in HFS.Tree]
SIP.S_adj [in HFS.Tree]
SIP.S_emp [in HFS.Tree]
SIP.X [in HFS.Tree]
Subtype.A [in HFS.Preliminaries]
Subtype.f [in HFS.Preliminaries]
Subtype.fp [in HFS.Preliminaries]
Subtype.f_idem [in HFS.Preliminaries]
Subtype.I [in HFS.Preliminaries]
Subtype.I_injective [in HFS.Preliminaries]
Subtype.S [in HFS.Preliminaries]
Subtype.X [in HFS.Preliminaries]
Subtype.X_eq_dec [in HFS.Preliminaries]
T
TransitiveClosure.X [in HFS.TC]W
WIP.adj [in HFS.Tree]WIP.choice [in HFS.Tree]
WIP.eset [in HFS.Tree]
WIP.gamma [in HFS.Tree]
WIP.wip [in HFS.Tree]
WIP.X [in HFS.Tree]
Without.X [in HFS.Extensionality]
Library Index
A
AckermannC
CardinalityCategoricity
E
ExtensionalityH
HFM
ModelO
OperationsOrdinals
P
PreliminariesT
TacticsTC
Tree
Lemma Index
A
adj_incl [in HFS.HF]adj_el [in HFS.HF]
adj_eld [in HFS.Model]
adj_diff [in HFS.Ackermann]
adj_mem [in HFS.Ackermann]
adj_el_strong [in HFS.Extensionality]
adj_nel [in HFS.Extensionality]
alpha_swap [in HFS.Model]
alpha_cancel [in HFS.Model]
alpha_ge [in HFS.Model]
alpha_le [in HFS.Model]
alpha_eq [in HFS.Model]
alpha_null [in HFS.Model]
alpha_equiv [in HFS.Model]
B
bun_el [in HFS.Operations]bun' [in HFS.Operations]
C
cancel [in HFS.Ackermann]card_ord_normal [in HFS.Cardinality]
card_ord [in HFS.Cardinality]
card_invariance [in HFS.Cardinality]
card_fun [in HFS.Cardinality]
card_inv [in HFS.Cardinality]
card_wo_inv [in HFS.Cardinality]
card_inj [in HFS.Cardinality]
card_adj [in HFS.Cardinality]
card_empty' [in HFS.Cardinality]
card_empty [in HFS.Cardinality]
card_total [in HFS.Cardinality]
card_epot [in HFS.Cardinality]
categoricity [in HFS.Categoricity]
chainA [in HFS.Operations]
chain_inter [in HFS.Operations]
chain_union [in HFS.Operations]
choose_el [in HFS.HF]
complete_induction [in HFS.Ackermann]
D
dec_DM_or [in HFS.Preliminaries]dec_eq_sym [in HFS.Preliminaries]
dec_trans [in HFS.Preliminaries]
dec_empty [in HFS.Ackermann]
dec_ext [in HFS.Extensionality]
dec_part [in HFS.Extensionality]
dec_adj_el [in HFS.Extensionality]
dec_adj_incl [in HFS.Extensionality]
disjoint [in HFS.Ackermann]
div2mul2add [in HFS.Ackermann]
div2Slt [in HFS.Ackermann]
div2SSlt [in HFS.Ackermann]
E
eld_elt [in HFS.Model]el_asym [in HFS.Extensionality]
el_irrefl [in HFS.Extensionality]
emptyEq [in HFS.Ackermann]
epot_dec [in HFS.Cardinality]
epot_empty [in HFS.Cardinality]
eps_ind [in HFS.Extensionality]
equiv_dec [in HFS.Model]
equiv_incl [in HFS.Model]
equiv_empty [in HFS.Model]
eset_incl [in HFS.HF]
eset_el [in HFS.HF]
extensionality [in HFS.Extensionality]
F
F_homo [in HFS.Categoricity]F_cancel [in HFS.Categoricity]
F' [in HFS.Tree]
G
GammaS_eq [in HFS.Cardinality]GammaS_eq' [in HFS.Cardinality]
Gamma_induction [in HFS.Cardinality]
Gamma_strict_incl [in HFS.Cardinality]
Gamma_ord_equiv [in HFS.Cardinality]
Gamma_range [in HFS.Cardinality]
Gamma_fixed_point [in HFS.Cardinality]
Gamma_equipotence [in HFS.Cardinality]
Gamma_idempotent [in HFS.Cardinality]
Gamma_coincidence [in HFS.Cardinality]
Gamma_ord [in HFS.Cardinality]
Gamma_card [in HFS.Cardinality]
Gamma0_eq' [in HFS.Cardinality]
Gamma0_eq [in HFS.Cardinality]
H
HFS.forall_iff_R2L [in HFS.Tactics]HFS.forall_iff_L2R [in HFS.Tactics]
homo_unique [in HFS.Categoricity]
homo_R [in HFS.Categoricity]
HT_trans [in HFS.Ordinals]
I
incl_trans [in HFS.Model]incl_antisym [in HFS.Extensionality]
incl_trans [in HFS.Extensionality]
incl_refl [in HFS.Extensionality]
interA_incl_eq' [in HFS.Operations]
interA_incl_eq [in HFS.Operations]
inter_pair_eq [in HFS.Operations]
inter_sing_eq [in HFS.Operations]
inter_glb [in HFS.Operations]
inter_incl [in HFS.Operations]
inter_el_incl [in HFS.Operations]
inter_el [in HFS.Operations]
L
lto_tricho [in HFS.Model]lto_irrefl [in HFS.Model]
lto_irrefl' [in HFS.Model]
lto_trans [in HFS.Model]
M
membership [in HFS.Ackermann]membership_dec [in HFS.Extensionality]
mem_adj_iff [in HFS.Ackermann]
mem_add [in HFS.Ackermann]
mem_smaller [in HFS.Ackermann]
mod2_add_mul2 [in HFS.Ackermann]
muldiv_smaller [in HFS.Ackermann]
mul2div2_evenodd [in HFS.Ackermann]
mul2_larger_pres [in HFS.Ackermann]
mul2_larger_S [in HFS.Ackermann]
N
nonempty [in HFS.HF]no_universal_set [in HFS.Extensionality]
O
ord_HT [in HFS.Ordinals]ord_trans_ord [in HFS.Ordinals]
ord_chain' [in HFS.Ordinals]
ord_chain [in HFS.Ordinals]
ord_incl [in HFS.Ordinals]
ord_tricho [in HFS.Ordinals]
ord_mono [in HFS.Ordinals]
ord_sip [in HFS.Ordinals]
ord_inv [in HFS.Ordinals]
ord_pred' [in HFS.Ordinals]
ord_pred [in HFS.Ordinals]
ord_eset [in HFS.Ordinals]
ord_eset' [in HFS.Ordinals]
ord_ord [in HFS.Ordinals]
ord_trans [in HFS.Ordinals]
ord_dec [in HFS.Cardinality]
ord_canonical [in HFS.Cardinality]
P
pair_injective [in HFS.Operations]part [in HFS.Extensionality]
pi1_eq [in HFS.Operations]
pi2_eq [in HFS.Operations]
power_el [in HFS.Operations]
power' [in HFS.Operations]
pow2_larger [in HFS.Ackermann]
product_el [in HFS.Operations]
pure_pir [in HFS.Preliminaries]
pure_equiv [in HFS.Preliminaries]
R
rep_el [in HFS.Operations]rep' [in HFS.Operations]
right_inverse [in HFS.Preliminaries]
R_fun [in HFS.Categoricity]
R_sim [in HFS.Categoricity]
R_total [in HFS.Categoricity]
R_symm [in HFS.Categoricity]
S
sep_el [in HFS.Operations]sep' [in HFS.Operations]
SI [in HFS.Tree]
sigma_idem [in HFS.Model]
sigma_equiv_eq [in HFS.Model]
sigma_equiv [in HFS.Model]
sing_injective [in HFS.Operations]
sing_el [in HFS.Operations]
sip [in HFS.Ackermann]
SI' [in HFS.Tree]
SI2sip [in HFS.Tree]
subset_induction [in HFS.Cardinality]
sub_norm [in HFS.Preliminaries]
succ_inj [in HFS.Extensionality]
succ_inv [in HFS.Operations]
swap [in HFS.Ackermann]
T
tcA_eq [in HFS.TC]tcE_eq [in HFS.TC]
tc_least [in HFS.TC]
tc_incl [in HFS.TC]
tc_trans [in HFS.TC]
tc_el [in HFS.TC]
TC_tc [in HFS.TC]
TC_adj [in HFS.TC]
TC_empty [in HFS.TC]
TC_fun [in HFS.TC]
TC_incl [in HFS.TC]
TC_trans [in HFS.TC]
tc' [in HFS.TC]
tdiscrim [in HFS.Model]
tel_dec [in HFS.TC]
tel_TC [in HFS.TC]
tel_adjR [in HFS.TC]
tel_adjL [in HFS.TC]
tel_inv [in HFS.TC]
tmember [in HFS.Model]
tree_extensionality [in HFS.Model]
tree_model [in HFS.Model]
U
unionA_incl_eq' [in HFS.Operations]unionA_incl_eq [in HFS.Operations]
unionE_eq [in HFS.Operations]
union_pair_eq [in HFS.Operations]
union_sing_eq [in HFS.Operations]
union_lub [in HFS.Operations]
union_incl [in HFS.Operations]
union_el_incl [in HFS.Operations]
union_el [in HFS.Operations]
union' [in HFS.Operations]
upair_sing [in HFS.Operations]
upair_injective [in HFS.Operations]
upair_el [in HFS.Operations]
W
wip2sip [in HFS.Tree]without [in HFS.Extensionality]
withoutA_neq [in HFS.Extensionality]
withoutA_eq [in HFS.Extensionality]
without_inverse [in HFS.Ackermann]
without_nin [in HFS.Extensionality]
without_el [in HFS.Extensionality]
Constructor Index
C
cardA [in HFS.Cardinality]card0 [in HFS.Cardinality]
D
decision [in HFS.Preliminaries]DecPred [in HFS.Preliminaries]
E
eltdH [in HFS.Model]eltdT [in HFS.Model]
epotA [in HFS.Cardinality]
epot0 [in HFS.Cardinality]
EqType [in HFS.Preliminaries]
equivCancel [in HFS.Model]
EquivCongruent [in HFS.Model]
EquivRefl [in HFS.Model]
equivSwap [in HFS.Model]
EquivSymm [in HFS.Model]
EquivTrans [in HFS.Model]
H
HFS [in HFS.HF]L
ltoE [in HFS.Model]ltoF [in HFS.Model]
ltoS [in HFS.Model]
O
OrdS [in HFS.Ordinals]Ord0 [in HFS.Ordinals]
R
R_adj [in HFS.Categoricity]R_empty [in HFS.Categoricity]
T
telI [in HFS.TC]telT [in HFS.TC]
treeA [in HFS.Tree]
treeN [in HFS.Tree]
Inductive Index
C
card [in HFS.Cardinality]D
dec [in HFS.Preliminaries]E
eltd [in HFS.Model]epot [in HFS.Cardinality]
equiv [in HFS.Model]
L
lto [in HFS.Model]O
ord [in HFS.Ordinals]R
R [in HFS.Categoricity]T
tel [in HFS.TC]tree [in HFS.Tree]
Projection Index
A
adj [in HFS.HF]C
cancel [in HFS.HF]D
decision [in HFS.Preliminaries]decPred_dec [in HFS.Preliminaries]
decPred_p [in HFS.Preliminaries]
discrim [in HFS.HF]
E
eqType_dec [in HFS.Preliminaries]eqType_X [in HFS.Preliminaries]
eset [in HFS.HF]
H
hf_ind [in HFS.HF]M
member [in HFS.HF]S
set [in HFS.HF]swap [in HFS.HF]
Section Index
B
BigIntersection [in HFS.Operations]BigUnion [in HFS.Operations]
BinaryUnion [in HFS.Operations]
C
Chain [in HFS.Operations]E
Equipotence [in HFS.Cardinality]Evaluation [in HFS.Tree]
ExtDec [in HFS.Extensionality]
F
F [in HFS.Categoricity]H
HF [in HFS.HF]HF_Evaluation [in HFS.Tree]
Homo [in HFS.Categoricity]
O
Ordinals [in HFS.Ordinals]P
Pairs [in HFS.Operations]Power [in HFS.Operations]
Pure [in HFS.Preliminaries]
R
R [in HFS.Categoricity]Replacement [in HFS.Operations]
R_functional [in HFS.Categoricity]
S
Separation [in HFS.Operations]SingUnorderedPair [in HFS.Operations]
SIP [in HFS.Tree]
Subtype [in HFS.Preliminaries]
T
TransitiveClosure [in HFS.TC]W
WIP [in HFS.Tree]Without [in HFS.Extensionality]
Instance Index
A
and_dec [in HFS.Preliminaries]D
dec_HF [in HFS.Extensionality]dec_0_incl [in HFS.Extensionality]
dec_0_el [in HFS.Extensionality]
dec_0_eq [in HFS.Extensionality]
E
epot_Equivalence [in HFS.Cardinality]equiv_treeA_proper [in HFS.Model]
equiv_Equivalence [in HFS.Model]
F
False_dec [in HFS.Preliminaries]H
hf_all_dec [in HFS.Extensionality]hf_ex_dec [in HFS.Extensionality]
I
iff_dec [in HFS.Preliminaries]impl_dec [in HFS.Preliminaries]
incl_dec [in HFS.Extensionality]
N
nat_eq_dec [in HFS.Ackermann]not_dec [in HFS.Preliminaries]
O
or_dec [in HFS.Preliminaries]T
tree_eq_dec [in HFS.Tree]True_dec [in HFS.Preliminaries]
Definition Index
A
Ackermann [in HFS.Ackermann]adj [in HFS.Ackermann]
alpha [in HFS.Model]
B
bun [in HFS.Operations]C
chain [in HFS.Operations]D
div2 [in HFS.Ackermann]F
F [in HFS.Categoricity]G
Gamma [in HFS.Cardinality]H
homo [in HFS.Categoricity]HT [in HFS.Ordinals]
I
I [in HFS.Tree]incl [in HFS.Model]
inter [in HFS.Operations]
I' [in HFS.Tree]
M
mem [in HFS.Ackermann]membership_law_matters [in HFS.HF]
mod2 [in HFS.Ackermann]
mul2 [in HFS.Ackermann]
P
pair [in HFS.Operations]pi1 [in HFS.Operations]
pi2 [in HFS.Operations]
power [in HFS.Operations]
pow2 [in HFS.Ackermann]
product [in HFS.Operations]
pure [in HFS.Preliminaries]
R
rep [in HFS.Operations]S
S [in HFS.Tree]sep [in HFS.Operations]
sigma [in HFS.Model]
S' [in HFS.Tree]
T
tc [in HFS.TC]TC [in HFS.TC]
trans [in HFS.HF]
U
union [in HFS.Operations]W
without [in HFS.Ackermann]Record Index
D
dec [in HFS.Preliminaries]decPred [in HFS.Preliminaries]
E
eqType [in HFS.Preliminaries]H
HF [in HFS.HF]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (420 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (202 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (27 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |