Global Index

(817 entries)

Notation Index

other

(26 entries)

Module Index

other

(2 entries)

Variable Index

other

(42 entries)

Library Index

other

(9 entries)

Lemma Index

other

(477 entries)

Constructor Index

other

(56 entries)

Axiom Index

other

(15 entries)

Inductive Index

other

(21 entries)

Projection Index

other

(2 entries)

Section Index

other

(21 entries)

Instance Index

other

(35 entries)

Abbreviation Index

other

(23 entries)

Definition Index

other

(87 entries)

Record Index

other

(1 entry)

Global Index

A

Absorp [lemma, in BAlg]
Absorp' [lemma, in BAlg]
Acc [inductive, in complete_ind_nat]
Acc [inductive, in wo]
Acc [inductive, in wfr]
AccI [constructor, in complete_ind_nat]
AccI [constructor, in wo]
AccI [constructor, in wfr]
acc_regular [lemma, in wo]
Adj [axiom, in ST]
adj [axiom, in ST]
adj_incl_xm_or [lemma, in ST]
adj_sub_xm [lemma, in ST]
adj_el_xm [lemma, in ST]
adj_el_eq [lemma, in ST]
adj_sub_eset [lemma, in ST]
adj_inj [lemma, in ST]
adj_inhab [lemma, in ST]
adj_eset [lemma, in ST]
adj_sub [lemma, in ST]
adj_sub' [lemma, in ST]
Adj' [lemma, in ST]
aeq [inductive, in BAlg]
aeq_dec_bot [lemma, in BAlg]
aeq_Equivalence [instance, in BAlg]
agree [definition, in ST]
Agreement [lemma, in BAlg]
agreement [lemma, in BAlg]
agree_HF [lemma, in ST]
agree_BS [lemma, in ST]
agree_unique [lemma, in ST]
all_Acc_all_inductive [lemma, in wfr]
all_Acc_all_regular [lemma, in wfr]
all_regular_not_ex_serial [lemma, in wfr]
and_dec [instance, in Base]
Annu [lemma, in BAlg]
Annu' [lemma, in BAlg]
apply [definition, in ST]
apply_toset [lemma, in ST]
app_equi_proper [instance, in Base]
app_incl_proper [instance, in Base]
Assn [definition, in BAlg]
Assn [definition, in Solver]
Asso [lemma, in BAlg]
Asso' [lemma, in BAlg]

B

BAlg [library]
Base [library]
beq [definition, in BAlg]
bool_eq_dec [instance, in Base]
bool_dec [instance, in Base]
bool_Prop_false [lemma, in Base]
bool_Prop_true [lemma, in Base]
bool2exp [definition, in Solver]
bool2Prop [definition, in Base]
bot [constructor, in BAlg]
bot [constructor, in Solver]
BS [abbreviation, in ST]
BS_HF [lemma, in ST]
BS_tight [lemma, in ST]
BS_inf [lemma, in ST]
BS_lin_succ [lemma, in ST]
BS_trans [lemma, in ST]
BS_Stage [lemma, in ST]
btow [inductive, in ST]
btowA [inductive, in ST]
btowAI [constructor, in ST]
btowD [inductive, in ST]
btowDO [constructor, in ST]
btowDS [constructor, in ST]
btowO [constructor, in ST]
btowS [constructor, in ST]
btow_inf [lemma, in ST]
btow_acc [lemma, in ST]
btow_lin_succ [lemma, in ST]
btow_di [lemma, in ST]
btow_tight [lemma, in ST]
btow_tow [lemma, in ST]
bun [abbreviation, in ST]
bun_adj_eq [lemma, in ST]
bun_0_eq [lemma, in ST]
bun_el [lemma, in ST]

C

Cantor [lemma, in ST]
card [definition, in Base]
Cardinality [section, in Base]
Cardinality.X [variable, in Base]
card_equi_proper [instance, in Base]
card_or [lemma, in Base]
card_lt [lemma, in Base]
card_equi [lemma, in Base]
card_ex [lemma, in Base]
card_0 [lemma, in Base]
card_cons_rem [lemma, in Base]
card_eq [lemma, in Base]
card_le [lemma, in Base]
card_not_in_rem [lemma, in Base]
card_in_rem [lemma, in Base]
card_cons' [lemma, in Base]
card_cons [lemma, in Base]
cfind [lemma, in Base]
chain [definition, in ST]
chain_adj [lemma, in ST]
closed [definition, in ST]
closed_ex [lemma, in ST]
closure [definition, in ST]
Closure [section, in ST]
ClosureExists [section, in ST]
ClosureExists.f [variable, in ST]
ClosureExists.o [variable, in ST]
closure_ind [lemma, in ST]
closure_f [lemma, in ST]
closure_o [lemma, in ST]
closure_least [lemma, in ST]
closure_ind' [lemma, in ST]
closure_f' [lemma, in ST]
closure_o' [lemma, in ST]
closure_least' [lemma, in ST]
closure_eq [lemma, in ST]
Closure.f [variable, in ST]
Closure.o [variable, in ST]
coincidence [lemma, in Solver]
Comm [constructor, in BAlg]
Comm' [constructor, in BAlg]
comp [abbreviation, in ST]
CompC [constructor, in BAlg]
CompD [constructor, in BAlg]
complete_ind_nat [library]
CompN [constructor, in BAlg]
comp_ind [lemma, in complete_ind_nat]
comp_dis [lemma, in BAlg]
comp_con [lemma, in BAlg]
con [constructor, in BAlg]
cond [abbreviation, in BAlg]
cond [constructor, in Solver]
cond_complete2 [lemma, in Solver]
cond_compatibility [lemma, in Solver]
cond_reduction [lemma, in Solver]
cond_expansion [lemma, in Solver]
consistency [lemma, in BAlg]
cons_equi_proper [instance, in Base]
cons_incl_proper [instance, in Base]
con_aeq_proper [instance, in BAlg]
cprod [definition, in ST]

D

Dec [definition, in Base]
dec [definition, in Base]
Decb [abbreviation, in Base]
decidability [lemma, in BAlg]
dec_transfer [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
Dec_auto_not [lemma, in Base]
Dec_auto [lemma, in Base]
Dec_reflect_eq [lemma, in Base]
Dec_reflect [lemma, in Base]
dec_contra [lemma, in Solver]
dec_contra_not [lemma, in Solver]
dec2bool [definition, in Base]
Deep_embedding.check_equiv [definition, in Solver]
Deep_embedding.check_sat [definition, in Solver]
Deep_embedding.i [abbreviation, in Solver]
Deep_embedding.f [abbreviation, in Solver]
Deep_embedding.b [abbreviation, in Solver]
Deep_embedding.imp [abbreviation, in Solver]
_ || _ [notation, in Solver]
_ && _ [notation, in Solver]
Deep_embedding [module, in Solver]
delta [definition, in ST]
delta_eq [lemma, in ST]
deMorgan [lemma, in BAlg]
deMorgan' [lemma, in BAlg]
Diaconescu [lemma, in ST]
Diaconescu [section, in ST]
Diaconescu.choice [variable, in ST]
Diaconescu.gamma [variable, in ST]
dis [constructor, in BAlg]
disjoint [definition, in Base]
disjoint_app [lemma, in Base]
disjoint_cons [lemma, in Base]
disjoint_nil' [lemma, in Base]
disjoint_nil [lemma, in Base]
disjoint_incl [lemma, in Base]
disjoint_symm [lemma, in Base]
disjoint_forall [lemma, in Base]
Dist [constructor, in BAlg]
Dist' [constructor, in BAlg]
dis_aeq_proper [instance, in BAlg]
DM_exists [lemma, in Base]
DM_or [lemma, in Base]
DN [lemma, in BAlg]
dual [definition, in BAlg]
dualize [lemma, in BAlg]
dualize' [lemma, in BAlg]
dual_involutive [lemma, in BAlg]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
dupfreeN [constructor, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_card [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_cons [lemma, in Base]
Dupfree.X [variable, in Base]

E

eeq_val [lemma, in Solver]
eeq_sep [lemma, in Solver]
eeq_dec [instance, in Solver]
eeq_sat [lemma, in Solver]
elem [axiom, in ST]
el_cprod [lemma, in ST]
eqType [record, in Base]
EqType [constructor, in Base]
eqType_CS [definition, in Base]
eqType_dec [projection, in Base]
eqType_X [projection, in Base]
Equi [section, in Base]
equi [definition, in Base]
equiv_sep [lemma, in ssort]
equi_rotate [lemma, in Base]
equi_shift [lemma, in Base]
equi_swap [lemma, in Base]
equi_dup [lemma, in Base]
equi_push [lemma, in Base]
equi_Equivalence [instance, in Base]
Equi.X [variable, in Base]
Eset [axiom, in ST]
eset [axiom, in ST]
eset_trans [lemma, in ST]
eset_unique [lemma, in ST]
eset_sub [lemma, in ST]
eva [definition, in BAlg]
eva [definition, in Solver]
Exp [inductive, in BAlg]
Exp [inductive, in Solver]
expa [lemma, in BAlg]
Expa [lemma, in BAlg]
expansion [lemma, in BAlg]
expansion [lemma, in Solver]
expansion_bot [lemma, in BAlg]
expansion_top [lemma, in BAlg]
Expa' [lemma, in BAlg]
Exp_eq_dec [instance, in BAlg]
Exp_eq_dec [instance, in Solver]
Ext [axiom, in ST]
ext_xm [lemma, in ST]
ex_least [lemma, in complete_ind_nat]
Ex1 [definition, in Solver]
Ex4 [definition, in Solver]
Ex5 [definition, in Solver]
Ex6 [definition, in Solver]

F

False_dec [instance, in Base]
FCI [module, in Base]
FCI.C [definition, in Base]
FCI.closure [lemma, in Base]
FCI.F [definition, in Base]
FCI.FCI [section, in Base]
FCI.FCI.R [variable, in Base]
FCI.FCI.sigma [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.fip_dec [lemma, in Base]
FCI.fp [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.pick [lemma, in Base]
filter [definition, in Base]
Filter [section, in Base]
filter_comm [lemma, in Base]
filter_and [lemma, in Base]
filter_pq_eq [lemma, in Base]
filter_pq_mono [lemma, in Base]
filter_fst' [lemma, in Base]
filter_fst [lemma, in Base]
filter_app [lemma, in Base]
filter_id [lemma, in Base]
filter_mono [lemma, in Base]
filter_incl [lemma, in Base]
Filter.X [variable, in Base]
Fin [inductive, in ST]
FinA [constructor, in ST]
FinE [constructor, in ST]
Fin_sub [lemma, in ST]
Fin_sigma0_xm [lemma, in ST]
Fin_trans_Num [lemma, in ST]
Fin_chain_gel [lemma, in ST]
Fin_eset_inhab [lemma, in ST]
fip [inductive, in Base]
Fip [section, in Base]
fip_dec [lemma, in Base]
fip_it_closed [lemma, in Base]
fip_it_sound [lemma, in Base]
fip_it [definition, in Base]
fip_least [lemma, in Base]
fip_closed [definition, in Base]
fip_monotone [definition, in Base]
fip_intro [constructor, in Base]
Fip.R [variable, in Base]
Fip.sigma [variable, in Base]
Fip.X [variable, in Base]
FP [definition, in Base]
frep [definition, in ST]
frep_adj_eq [lemma, in ST]
frep_0_eq [lemma, in ST]
frep_delta_sep [lemma, in ST]
frep_el [lemma, in ST]
functional [definition, in ST]

G

gel [definition, in ST]
ground [inductive, in BAlg]
ground [abbreviation, in Solver]
groundB [constructor, in BAlg]
groundC [constructor, in BAlg]
groundD [constructor, in BAlg]
groundN [constructor, in BAlg]
groundT [constructor, in BAlg]
ground_eval [lemma, in BAlg]
ground_equiv [lemma, in Solver]
ground_sat_dec [lemma, in Solver]

H

HF [inductive, in ST]
HFA [constructor, in ST]
HFE [constructor, in ST]
HFT [definition, in ST]
HFT_Num [lemma, in ST]
HFT_closed [lemma, in ST]
HF_inf [lemma, in ST]
HF_BS_agree [lemma, in ST]
HF_BS [lemma, in ST]
HF_closed_power [lemma, in ST]
HF_closed_frep [lemma, in ST]
HF_closed_bun [lemma, in ST]
HF_WF [lemma, in ST]
HF_list' [lemma, in ST]
HF_list [lemma, in ST]
HF_xm [lemma, in ST]
HF_xm_eset_el [lemma, in ST]
HF_closed [lemma, in ST]
HF_fin [lemma, in ST]

I

Idem [lemma, in BAlg]
Idem' [lemma, in BAlg]
Iden [constructor, in BAlg]
Iden' [constructor, in BAlg]
iff_dec [instance, in Base]
if_complete2 [lemma, in Solver]
impl_dec [instance, in Base]
inacc [lemma, in wo]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_equi_proper [instance, in Base]
incl_preorder [instance, in Base]
incl_app_left [lemma, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [lemma, in Base]
incl_sing [lemma, in Base]
incl_lcons [lemma, in Base]
incl_shift [lemma, in Base]
incl_nil_eq [lemma, in Base]
incl_map [lemma, in Base]
incl_nil [lemma, in Base]
inductive [definition, in wfr]
Inf [axiom, in ST]
inhab [abbreviation, in ST]
inhab_neq [lemma, in ST]
inhab_not [lemma, in ST]
insert [definition, in ssort]
insert_sorted [lemma, in ssort]
insert_equiv [lemma, in ssort]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_incl_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_sing [lemma, in Base]
it [definition, in Base]
Iteration [section, in Base]
Iteration.f [variable, in Base]
Iteration.X [variable, in Base]
it_fp [lemma, in Base]
it_ind [lemma, in Base]

L

least [definition, in ST]
least_closed_ex [lemma, in ST]
least_unique [lemma, in ST]
list_cc [lemma, in Base]
list_exists_not_incl [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_in_dec [instance, in Base]
list_cycle [lemma, in Base]
list_eq_dec [instance, in Base]

M

Membership [section, in Base]
Membership.X [variable, in Base]
minel [definition, in wfr]

N

nat_le_dec [instance, in Base]
nat_eq_dec [instance, in Base]
neg [constructor, in BAlg]
neg [abbreviation, in Solver]
Nega [constructor, in BAlg]
Nega' [constructor, in BAlg]
neg_bot [lemma, in BAlg]
neg_top [lemma, in BAlg]
neg_aeq_proper [instance, in BAlg]
neg_cond [lemma, in Solver]
neg_neg [lemma, in Solver]
not_in_cons [lemma, in Base]
not_dec [instance, in Base]
not_ex_serial_all_Acc [lemma, in wfr]
num [definition, in ST]
Num [inductive, in ST]
NumO [constructor, in ST]
NumS [constructor, in ST]
Num_tight [lemma, in ST]
Num_inf [lemma, in ST]
Num_Ord [lemma, in ST]
Num_either [lemma, in ST]
Num_pred [lemma, in ST]
Num_trans_gel [lemma, in ST]
Num_HF [lemma, in ST]
num_sub_num [lemma, in ST]
num_el_num [lemma, in ST]
num_inj [lemma, in ST]
num_el [lemma, in ST]
num_le [lemma, in ST]
Num_num [lemma, in ST]
num_Num [lemma, in ST]
Num_eq_xm [lemma, in ST]
Num_sub_xm [lemma, in ST]
Num_el_xm [lemma, in ST]
Num_no_loop2 [lemma, in ST]
Num_closed [lemma, in ST]
Num_mono [lemma, in ST]
Num_cum [lemma, in ST]
Num_strict [lemma, in ST]
Num_lin [lemma, in ST]
Num_lin_el [lemma, in ST]
Num_lin_sigma [lemma, in ST]
Num_tricho [lemma, in ST]
Num_mono_el [lemma, in ST]
Num_eset [lemma, in ST]
Num_trans [lemma, in ST]

O

omega [abbreviation, in ST]
omega_sigma [lemma, in ST]
omega_O [lemma, in ST]
omega_inf [lemma, in ST]
omega_Num [lemma, in ST]
omega_no_num [lemma, in ST]
opair [definition, in ST]
opair_inj [lemma, in ST]
Ord [abbreviation, in ST]
Ord_Num [lemma, in ST]
Ord_WFT [lemma, in ST]
Ord_trans_Ord [lemma, in ST]
Ord_least [lemma, in ST]
Ord_succ_limit [lemma, in ST]
Ord_union [lemma, in ST]
Ord_cum [lemma, in ST]
Ord_tricho [lemma, in ST]
Ord_lin [lemma, in ST]
Ord_lin_el [lemma, in ST]
Ord_lin_succ [lemma, in ST]
Ord_omega [lemma, in ST]
Ord_omega.omega_Num [variable, in ST]
Ord_omega.omega [variable, in ST]
Ord_omega [section, in ST]
Ord_large [lemma, in ST]
Ord_new [lemma, in ST]
Ord_strict [lemma, in ST]
Ord_trans [lemma, in ST]
Ord_WF [lemma, in ST]
Ord_closed [lemma, in ST]
Ord_eset [lemma, in ST]
or_dec [instance, in Base]

P

pi [definition, in ST]
pi1 [definition, in ST]
pi1_eq [lemma, in ST]
pi2 [definition, in ST]
pi2_eq [lemma, in ST]
Power [axiom, in ST]
power [axiom, in ST]
power [definition, in Base]
Power [section, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
power_adj_eq [lemma, in ST]
power_0_eq [lemma, in ST]
power_above [lemma, in ST]
power_inj [lemma, in ST]
power_mono [lemma, in ST]
power_WF [lemma, in ST]
power_trans [lemma, in ST]
power_eager [lemma, in ST]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
Power.X [variable, in Base]
Prelude [library]
prod_eq_dec [instance, in Base]
propagate_con [lemma, in BAlg]
propagate_neg [lemma, in BAlg]

R

rank [definition, in ST]
rank_WF [lemma, in ST]
rank_fun [lemma, in ST]
rank_least [lemma, in ST]
reachable [definition, in ST]
reachable_reachable [lemma, in ST]
reachable_rank [lemma, in ST]
Rec [inductive, in ST]
RecO [constructor, in ST]
RecS [constructor, in ST]
Rec_fun [lemma, in ST]
Rec_Num [lemma, in ST]
reduce [lemma, in BAlg]
reduce_aeq [lemma, in BAlg]
Refl [lemma, in BAlg]
regular [definition, in ST]
regular [definition, in wo]
regular [definition, in wfr]
regularity_all_WF [lemma, in ST]
rem [definition, in Base]
Removal [section, in Base]
Removal.X [variable, in Base]
rem_inclr [lemma, in Base]
rem_reorder [lemma, in Base]
rem_id [lemma, in Base]
rem_fst' [lemma, in Base]
rem_fst [lemma, in Base]
rem_comm [lemma, in Base]
rem_equi [lemma, in Base]
rem_app' [lemma, in Base]
rem_app [lemma, in Base]
rem_neq [lemma, in Base]
rem_in [lemma, in Base]
rem_cons' [lemma, in Base]
rem_cons [lemma, in Base]
rem_mono [lemma, in Base]
rem_incl [lemma, in Base]
rem_not_in [lemma, in Base]
Rep [axiom, in ST]
rep [axiom, in ST]
rep [definition, in Base]
rep_dupfree [lemma, in Base]
rep_idempotent [lemma, in Base]
rep_injective [lemma, in Base]
rep_eq [lemma, in Base]
rep_eq' [lemma, in Base]
rep_mono [lemma, in Base]
rep_equi [lemma, in Base]
rep_in [lemma, in Base]
rep_incl [lemma, in Base]
rep_power [lemma, in Base]
rep_cons_eq [lemma, in Base]
rep_cons' [lemma, in Base]
rep_cons [lemma, in Base]
Russell [lemma, in ST]

S

sat [definition, in BAlg]
sat [abbreviation, in Solver]
sat_val [lemma, in Solver]
sat_eeq [lemma, in Solver]
sat_compatibility [lemma, in Solver]
sat_var_elim [lemma, in Solver]
sat_dec [instance, in Solver]
sat_solver [lemma, in Solver]
sep [definition, in ST]
sep [definition, in ssort]
sep [abbreviation, in Solver]
sep_sub [lemma, in ST]
sep_el [lemma, in ST]
sep_eeq [lemma, in Solver]
sep_dec [instance, in Solver]
sep_sat [lemma, in Solver]
serial [definition, in ST]
serial [definition, in wfr]
serial_ex [lemma, in ST]
serial_ex_trans [lemma, in ST]
serial_not_regular [lemma, in ST]
serial_not_has_min [lemma, in wfr]
set [axiom, in ST]
shallow_embedding [lemma, in Solver]
shift [lemma, in BAlg]
shift [lemma, in Solver]
sigma [definition, in ST]
sigma_eager [lemma, in ST]
sigma_WF [lemma, in ST]
sigma_inj [lemma, in ST]
sigma_inj_sub [lemma, in ST]
sigma_trans [lemma, in ST]
sigma_auto [lemma, in ST]
sing [abbreviation, in ST]
sing_eq [lemma, in ST]
sing_inj [lemma, in ST]
sing_el [lemma, in ST]
size_recursion [lemma, in Base]
small [definition, in ST]
small_HF_delta_Num [lemma, in ST]
small_HF_Num [lemma, in ST]
small_red [lemma, in ST]
Solve [lemma, in BAlg]
solve [definition, in BAlg]
solve [definition, in Solver]
Solver [library]
solve_correct [lemma, in BAlg]
solve_correct [lemma, in Solver]
sort [definition, in ssort]
sorted [inductive, in ssort]
sortedC [constructor, in ssort]
sortedN [constructor, in ssort]
sorted_dec [lemma, in ssort]
sorted_sort_fp [lemma, in ssort]
sorted_cons [lemma, in ssort]
sorted_unique [lemma, in ssort]
sorted_sep [lemma, in ssort]
sort_idempotent [lemma, in ssort]
sort_normalizer [lemma, in ssort]
sort_sorted [lemma, in ssort]
sort_equiv [lemma, in ssort]
soundness [lemma, in BAlg]
ssort [library]
ST [library]
sta [definition, in ST]
Stage [abbreviation, in ST]
Stage_BS [lemma, in ST]
Stage_least [lemma, in ST]
Stage_lin [lemma, in ST]
Stage_lin_el [lemma, in ST]
Stage_lin_succ [lemma, in ST]
Stage_inc [lemma, in ST]
Stage_large [lemma, in ST]
Stage_strict [lemma, in ST]
Stage_trans [lemma, in ST]
Stage_WF [lemma, in ST]
Stage_eset [lemma, in ST]
sta_inv [lemma, in ST]
sta_Zer [lemma, in ST]
sub [definition, in ST]
subset_outside [lemma, in ST]
subst [definition, in BAlg]
subst [definition, in Solver]
substitutivity [lemma, in BAlg]
subst_vars_ground [lemma, in BAlg]
subst_vars [lemma, in Solver]
subst_vars_ground [lemma, in Solver]
sub_eset [lemma, in ST]
sub_trans [lemma, in ST]
sub_refl [lemma, in ST]
Symm [constructor, in BAlg]

T

tau [definition, in ST]
tau [definition, in BAlg]
tau [definition, in Solver]
tau_inhab [lemma, in ST]
tc [definition, in ST]
top [constructor, in BAlg]
top [constructor, in Solver]
toset [definition, in ST]
tow [inductive, in ST]
towA [inductive, in ST]
towAI [constructor, in ST]
towD [inductive, in ST]
towDS [constructor, in ST]
towDU [constructor, in ST]
Tower [section, in ST]
Tower.g [variable, in ST]
Tower.g_trans [variable, in ST]
Tower.g_eager [variable, in ST]
Tower.g_WF [variable, in ST]
Tower.g_inc [variable, in ST]
towS [constructor, in ST]
towU [constructor, in ST]
tow_cum [lemma, in ST]
tow_trans [lemma, in ST]
tow_btow [lemma, in ST]
tow_large [lemma, in ST]
tow_new [lemma, in ST]
tow_mono_el [lemma, in ST]
tow_lt_el [lemma, in ST]
tow_tricho [lemma, in ST]
tow_lin_el [lemma, in ST]
tow_inj [lemma, in ST]
tow_inj_sub [lemma, in ST]
tow_strict [lemma, in ST]
tow_WF [lemma, in ST]
tow_least [lemma, in ST]
tow_acc [lemma, in ST]
tow_mono [lemma, in ST]
tow_not_sub [lemma, in ST]
tow_lin [lemma, in ST]
tow_lin_succ [lemma, in ST]
tow_di [lemma, in ST]
tow_eset [lemma, in ST]
Tran [constructor, in BAlg]
trans [definition, in ST]
trans_closure [lemma, in ST]
trans_power_eq [lemma, in ST]
trans_power [lemma, in ST]
True_dec [instance, in Base]

U

undup [definition, in Base]
Undup [section, in Base]
undup_idempotent [lemma, in Base]
undup_id [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_id_equi [lemma, in Base]
Undup.X [variable, in Base]
Union [axiom, in ST]
union [axiom, in ST]
union_omega [lemma, in ST]
union_power_eq [lemma, in ST]
union_abs' [lemma, in ST]
union_abs [lemma, in ST]
union_HF [lemma, in ST]
union_adj_adj [lemma, in ST]
union_adj_eset [lemma, in ST]
union_WFc [lemma, in ST]
union_WF [lemma, in ST]
union_trans [lemma, in ST]
union_sigma [lemma, in ST]
union_sing [lemma, in ST]
union_eset [lemma, in ST]
union_gel_eq [lemma, in ST]
union_gel [lemma, in ST]
union_lub [lemma, in ST]
union_mono [lemma, in ST]
union_trans_sub [lemma, in ST]
union_sub [lemma, in ST]
union_el_sub [lemma, in ST]
unique [definition, in ST]
UoC [lemma, in BAlg]
upair [abbreviation, in ST]
upair_inj [lemma, in ST]
upair_el [lemma, in ST]
upair_sing [lemma, in ST]
upbnd [abbreviation, in ST]
update [definition, in BAlg]
update [definition, in Solver]
update_id [lemma, in Solver]

V

val [abbreviation, in Solver]
val_sat [lemma, in Solver]
var [constructor, in BAlg]
Var [definition, in BAlg]
var [constructor, in Solver]
Var [definition, in Solver]
vars [definition, in BAlg]
vars [definition, in Solver]
vars_ground [lemma, in BAlg]

W

Wellordering [section, in ST]
Wellordering.choice [variable, in ST]
Wellordering.gamma [variable, in ST]
Wellordering.u [variable, in ST]
_ <= _ [notation, in ST]
WF [inductive, in ST]
WFI [constructor, in ST]
WFR [section, in wfr]
wfr [library]
WFR.R [variable, in wfr]
WFR.X [variable, in wfr]
WFR.XM [variable, in wfr]
WFT [definition, in ST]
WFT_closed [lemma, in ST]
WF_not [lemma, in ST]
WF_regular [lemma, in ST]
WF_reachable [lemma, in ST]
WF_min [lemma, in ST]
WF_sigma_neq [lemma, in ST]
WF_sigma_notin [lemma, in ST]
WF_sigma_inj [lemma, in ST]
WF_unrealizable [lemma, in ST]
WF_no_loop3 [lemma, in ST]
WF_no_loop2 [lemma, in ST]
WF_no_loop [lemma, in ST]
WF_adj [lemma, in ST]
WF_eset [lemma, in ST]
WF_sub_closed [lemma, in ST]
WF_closed [lemma, in ST]
WO [section, in wo]
wo [library]
wo_anti [lemma, in ST]
wo_least [lemma, in ST]
wo_lin [lemma, in ST]
wo_trans [lemma, in ST]
WO.anti [variable, in wo]
WO.linear [variable, in wo]
WO.R [variable, in wo]
WO.X [variable, in wo]
WO.XM [variable, in wo]
_ < _ [notation, in wo]
_ <= _ [notation, in wo]

X

XM [axiom, in ST]
xm [abbreviation, in ST]
xm_upbnd [lemma, in ST]

Z

Zer [abbreviation, in ST]
Zer_least [lemma, in ST]
Zer_not_sub [lemma, in ST]
Zer_lin_succ [lemma, in ST]
Zer_inc [lemma, in ST]
Zer_u [lemma, in ST]

other

_ ! _ [notation, in ST]
_ <=c _ [notation, in ST]
_ @ _ [notation, in ST]
_ << _ [notation, in ST]
_ <<= _ [notation, in ST]
_ nel _ [notation, in ST]
_ el _ [notation, in ST]
_ <=p _ [notation, in ST]
_ === _ [notation, in Base]
_ <<= _ [notation, in Base]
_ nel _ [notation, in Base]
_ el _ [notation, in Base]
_ == _ [notation, in BAlg]
_ =~= _ [notation, in BAlg]
_ || _ [notation, in BAlg]
_ && _ [notation, in BAlg]
_ == _ [notation, in Solver]
eq_dec _ [notation, in Base]
-- _ [notation, in BAlg]
0 [notation, in ST]
| _ | [notation, in Base]