Global Index

other

(713 entries)

Notation Index

other

(22 entries)

Module Index

other

(1 entry)

Variable Index

other

(38 entries)

Library Index

other

(31 entries)

Lemma Index

other

(396 entries)

Constructor Index

other

(27 entries)

Inductive Index

other

(10 entries)

Section Index

other

(19 entries)

Instance Index

other

(28 entries)

Definition Index

other

(141 entries)

Global Index

A

Acceptability [library]
acc_conj_correct [lemma, in Acceptability]
acc_conj [definition, in Acceptability]
Acc_RE [lemma, in RE]
AD [lemma, in AD]
AD [library]
Add [definition, in Nat]
Add_correct [lemma, in Nat]
Add_rec_S [lemma, in Nat]
Add_rec_0 [lemma, in Nat]
Andalso [definition, in Bool]
Andalso_rec_ff [lemma, in Bool]
Andalso_rec_ft [lemma, in Bool]
Andalso_rec_tf [lemma, in Bool]
Andalso_rec_tt [lemma, in Bool]
Andalso_correct [lemma, in Proc]
and_dec [instance, in Base]
app [constructor, in Lvw]
App [definition, in Encoding]
AppCross [definition, in EnumInt]
appCross [definition, in Enum]
AppCross_correct [lemma, in EnumInt]
AppCross_Cons [lemma, in EnumInt]
AppCross_Nil [lemma, in EnumInt]
appCross_dupfree [lemma, in Enum]
appCross_app [lemma, in Enum]
appCross_correct [lemma, in Enum]
Append [definition, in Lists]
Append_correct [lemma, in Lists]
Append_rec_Cons [lemma, in Lists]
Append_rec_Nil [lemma, in Lists]
app_converges [lemma, in Seval]
app_equi_proper [instance, in Base]
App_correct [lemma, in Encoding]
ARS [library]

B

bapp [constructor, in Lvw]
Base [library]
benc [definition, in Proc]
bijection [library]
bijections [section, in bijection]
bijections.A [variable, in bijection]
bijections.B [variable, in bijection]
bijective [inductive, in bijection]
blam [constructor, in Lvw]
Bool [library]
bool_eq_dec [instance, in Base]
bter [constructor, in Lvw]
bterm [inductive, in Lvw]
bvar [constructor, in Lvw]

C

c [definition, in Pairs]
C [definition, in Pairs]
card [definition, in Base]
Cardinality [section, in Base]
Cardinality.X [variable, in Base]
card_equi_proper [instance, in Base]
card_0 [lemma, in Base]
card_cons_rem [lemma, in Base]
card_cons [lemma, in Base]
card_ex [lemma, in Base]
card_or [lemma, in Base]
card_lt [lemma, in Base]
card_equi [lemma, in Base]
card_eq [lemma, in Base]
card_le [lemma, in Base]
CC [definition, in Pairs]
cChoice [definition, in Computability]
CC_correct [lemma, in Pairs]
CC_rec_S [lemma, in Pairs]
CC_rec_0 [lemma, in Pairs]
church_rosser [definition, in ARS]
church_rosser [lemma, in Lvw]
cLam [definition, in Eval]
closed [definition, in Lvw]
Closed [definition, in Proc]
closed_step [lemma, in Lvw]
closed_subst [lemma, in Lvw]
closed_app [lemma, in Lvw]
closed_dcl [lemma, in Lvw]
closed_k_dclosed [lemma, in Lvw]
Closed_correct [lemma, in Proc]
Cn [definition, in Pairs]
Cn_correct [lemma, in Pairs]
Cn_closed [lemma, in Pairs]
comb_proc_red [lemma, in Lvw]
complement [definition, in Decidability]
complete_induction [lemma, in Base]
Computability [library]
confluence [lemma, in Lvw]
confluent [definition, in ARS]
confluent_CR [lemma, in ARS]
conj [definition, in Decidability]
Cons [definition, in Lists]
Cons_correct [lemma, in Lists]
cons_equi_proper [instance, in Base]
converges [definition, in Lvw]
converges_proper [instance, in Lvw]
converges_equiv [lemma, in Lvw]
convert [definition, in Lvw]
convert' [definition, in Lvw]
c_surj [lemma, in Pairs]
c_c_inv [lemma, in Pairs]
c_inv [definition, in Pairs]
C_longenough [lemma, in Pairs]
C_exhaustive [lemma, in Pairs]
C_ge [lemma, in Pairs]
C_S [lemma, in Pairs]
C27 [lemma, in Scott]
C27_proc [lemma, in Scott]

D

DA [lemma, in DA]
DA [library]
database_dummy [lemma, in Tactics]
DA_nat [lemma, in DA]
dcl [definition, in Proc]
dclApp [constructor, in Lvw]
dcllam [constructor, in Lvw]
dclosed [inductive, in Lvw]
Dclosed [definition, in Proc]
dclosed_closed [lemma, in Lvw]
dclosed_gt [lemma, in Lvw]
dclosed_closed_k [lemma, in Lvw]
Dclosed_correct [lemma, in Proc]
Dclosed_rec_lam [lemma, in Proc]
Dclosed_rec_app [lemma, in Proc]
Dclosed_rec_var [lemma, in Proc]
dclosed_dcl [lemma, in Proc]
dclvar [constructor, in Lvw]
dcl_dclosed [lemma, in Proc]
dec [definition, in Base]
Decidability [library]
decision [definition, in Base]
dec_acc [lemma, in Acceptability]
dec_lacc [lemma, in Acceptability]
dec_dec [lemma, in Computability]
dec_pdec [lemma, in Computability]
dec_dclosed [lemma, in Lvw]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
dec_enc [lemma, in Encoding]
diamond [definition, in ARS]
diamond_to_confluent [lemma, in ARS]
diamond_to_semi_confluent [lemma, in ARS]
disj [definition, in Decidability]
disjoint [definition, in Base]
disjoint_cons [lemma, in Base]
disjoint_forall [lemma, in Base]
disjoint_symm [lemma, in Enum]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
DupfreeLength [section, in Base]
DupfreeLength.X [variable, in Base]
dupfreeN [constructor, in Base]
dupfree_elAt [lemma, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_equi [lemma, in Base]
dupfree_ex [lemma, in Base]
dupfree_lt [lemma, in Base]
dupfree_eq [lemma, in Base]
dupfree_le [lemma, in Base]
dupfree_reorder [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_inv [lemma, in Base]
dupfree_T [lemma, in Enum]
Dupfree.X [variable, in Base]

E

ecl [inductive, in ARS]
eclC [constructor, in ARS]
eclR [constructor, in ARS]
eclS [constructor, in ARS]
ecl_sym [lemma, in ARS]
ecl_trans [lemma, in ARS]
El [definition, in Lists]
elAt [definition, in Base]
elAt_el [lemma, in Base]
elAt_app [lemma, in Base]
El_correct [lemma, in Lists]
El_Cons [lemma, in Lists]
El_nil [lemma, in Lists]
el_elAt [lemma, in Base]
el_pos [lemma, in Base]
enc [definition, in Nat]
Encoding [library]
enc_proc [lemma, in Nat]
enc_cls [lemma, in Nat]
enc_lam [lemma, in Nat]
enc_inj [lemma, in Computability]
enc_injective [lemma, in Encoding]
Enum [library]
EnumInt [library]
eproc_equiv [lemma, in Seval]
Eq [definition, in Equality]
eqApp [lemma, in Lvw]
EqN [definition, in Equality]
EqN_correct [lemma, in Equality]
EqN_rec_SS [lemma, in Equality]
EqN_rec_S0 [lemma, in Equality]
EqN_rec_0S [lemma, in Equality]
EqN_rec_00 [lemma, in Equality]
eqRef [constructor, in Lvw]
eqStarT [lemma, in Lvw]
eqStep [constructor, in Lvw]
eqSym [constructor, in Lvw]
eqTrans [constructor, in Lvw]
Equality [library]
Equi [section, in Base]
equi [definition, in Base]
equiv [inductive, in Lvw]
equiv_trans_r [lemma, in Tactics]
equiv_eva [lemma, in Seval]
equiv_app_proper [instance, in Lvw]
equiv_lambda' [lemma, in Lvw]
equiv_lambda [lemma, in Lvw]
equiv_ecl [lemma, in Lvw]
equiv_Equivalence [instance, in Lvw]
equiv_lambda' [lemma, in Eval]
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]
Eq_correct [lemma, in Equality]
Eq_correct_f [lemma, in Equality]
Eq_correct_t [lemma, in Equality]
eq_term_dec [lemma, in Computability]
eq_ref [lemma, in ARS]
eq_lam [lemma, in Lvw]
eq_dec_string [instance, in Lvw]
Eq_ldec [lemma, in Scott]
eq_dec_pair [instance, in Pairs]
ESize [definition, in Pairs]
eSize [definition, in Pairs]
ESize_correct [lemma, in Pairs]
Eta [lemma, in Lvw]
eva [definition, in Seval]
Eva [definition, in Eval]
eval [definition, in Seval]
Eval [definition, in Eval]
Eval [library]
eval_seval [lemma, in Seval]
eval_step [lemma, in Seval]
Eval_converges [lemma, in Eval]
eval_converges [lemma, in Eval]
Eval_eval [lemma, in Eval]
eval_Eval [lemma, in Eval]
Eval_correct [lemma, in Eval]
eva_Sn_n [lemma, in Seval]
eva_n_Sn [lemma, in Seval]
eva_equiv [lemma, in Seval]
eva_seval [lemma, in Seval]
eva_lam [lemma, in Seval]
Eva_correct [lemma, in Eval]
Eva_rec_app_Sn_3 [lemma, in Eval]
Eva_rec_app_Sn_2 [lemma, in Eval]
Eva_rec_app_Sn_1 [lemma, in Eval]
Eva_rec_app_Sn [lemma, in Eval]
Eva_rec_app_0 [lemma, in Eval]
Eva_rec_lam [lemma, in Eval]
Eva_rec_var [lemma, in Eval]
Ex [definition, in DA]
Exh_size_correct [lemma, in EnumInt]
Exh_size_lam [lemma, in EnumInt]
Exh_size_app [lemma, in EnumInt]
Exh_size_var [lemma, in EnumInt]
Exh_size [definition, in EnumInt]
exh_size [definition, in Enum]
Ex_correct_2 [lemma, in DA]
Ex_correct_3 [lemma, in DA]
Ex_correct_3a [lemma, in DA]
Ex_correct_1 [lemma, in DA]
Ex_rec [lemma, in DA]

F

false [definition, in Bool]
false_2 [definition, in Bool]
false_1 [definition, in Bool]
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.step [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.X [variable, 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 Lists]
filter [definition, in Base]
FilterComm [section, in Base]
FilterComm.p [variable, in Base]
FilterComm.q [variable, in Base]
FilterComm.X [variable, in Base]
FilterLemmas [section, in Base]
FilterLemmas_pq.q [variable, in Base]
FilterLemmas_pq.p [variable, in Base]
FilterLemmas_pq.X [variable, in Base]
FilterLemmas_pq [section, in Base]
FilterLemmas.p [variable, in Base]
FilterLemmas.X [variable, in Base]
Filter_correct [lemma, in Lists]
Filter_Cons [lemma, in Lists]
Filter_Nil [lemma, in Lists]
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_app [lemma, in Base]
filter_fst [lemma, in Base]
filter_mono [lemma, in Base]
filter_incl [lemma, in Base]
FirstFixedPoint [lemma, in Fixpoints]
Fixpoints [library]
FixX [section, in ARS]
FixX.X [variable, in ARS]
Fix_X.Eq_cls [variable, in Lists]
Fix_X.Eq_correct [variable, in Lists]
Fix_X.Eq [variable, in Lists]
Fix_X.enc_cls [variable, in Lists]
Fix_X.enc_lam [variable, in Lists]
Fix_X.enc [variable, in Lists]
Fix_X.X [variable, in Lists]
Fix_X [section, in Lists]
Fix_f.total_f [variable, in RE]
Fix_f.cls_f [variable, in RE]
Fix_f.f [variable, in RE]
Fix_f [section, in RE]
FP [definition, in Base]
functional [definition, in ARS]

G

g [definition, in Enum]
g_T [lemma, in Enum]
g_g_inv [lemma, in Enum]
g_inv_g [lemma, in Enum]
g_inv [definition, in Enum]

I

I [definition, in Lvw]
iff_dec [instance, in Base]
impl_dec [instance, in Base]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_preorder [instance, in Base]
incl_equi_proper [instance, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [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]
injective [definition, in bijection]
inverse [definition, in bijection]
inv2bij [lemma, in bijection]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_sing [lemma, in Base]
is_bijective [constructor, in bijection]
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]
I_neq_Omega [lemma, in Scott]

J

joinable [definition, in ARS]

K

K [definition, in Lvw]

L

lacc [definition, in Acceptability]
lacc_disj [lemma, in Acceptability]
lacc_conj [lemma, in Acceptability]
lam [constructor, in Lvw]
Lam [definition, in Encoding]
lambda [definition, in Lvw]
Lambda [definition, in Proc]
lambda_lam [lemma, in Lvw]
Lambda_correct [lemma, in Proc]
lamOmega [lemma, in Rice]
Lam_correct [lemma, in Encoding]
ldec [definition, in Decidability]
ldec_disj [lemma, in Decidability]
ldec_conj [lemma, in Decidability]
ldec_complement [lemma, in Decidability]
ldec_proc [lemma, in Proc]
ldec_lambda [lemma, in Proc]
ldec_closed [lemma, in Proc]
Leb [definition, in Proc]
Leb_correct [lemma, in Proc]
Leb_rec_Sm_Sn [lemma, in Proc]
Leb_rec_Sm_0 [lemma, in Proc]
Leb_rec_0 [lemma, in Proc]
leb_lt [lemma, in Proc]
left_inv_inj [lemma, in bijection]
left_inverse [definition, in bijection]
lenc [definition, in Lists]
lenc_lam [lemma, in Lists]
lenc_cls [lemma, in Lists]
Lists [library]
list_cc [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_sigma_forall [lemma, in Base]
list_in_dec [instance, in Base]
list_eq_dec [instance, in Base]
list_cycle [lemma, in Base]
Lt [definition, in Proc]
Lt_correct [lemma, in Proc]
Lvw [library]

M

Map [definition, in Lists]
Map_correct [lemma, in Lists]
Map_rec_Cons [lemma, in Lists]
Map_rec_Nil [lemma, in Lists]
map_lam [lemma, in Enum]
MoreAcc [library]
Mul [definition, in Nat]
Mul_correct [lemma, in Nat]
Mul_rec_S [lemma, in Nat]
Mul_rec_0 [lemma, in Nat]

N

Nat [library]
nat_le_dec [instance, in Base]
nat_eq_dec [instance, in Base]
Nil [definition, in Lists]
none [definition, in Options]
none_equiv_some [lemma, in Options]
none_correct [lemma, in Options]
Not [definition, in Bool]
not_rec_false [lemma, in Bool]
not_rec_true [lemma, in Bool]
not_dec [instance, in Base]
Nth [definition, in Lists]
Nth_correct [lemma, in Lists]
Nth_Sn [lemma, in Lists]
Nth_0 [lemma, in Lists]
Nth_Nil [lemma, in Lists]
nth_error_none [lemma, in Base]
n_ldec [definition, in DA]
n_decider [definition, in DA]

O

oenc [definition, in Lists]
oenc [definition, in Options]
oenc_correct_some [lemma, in Options]
Omega [definition, in Lvw]
omega [definition, in Lvw]
Omega_diverges [lemma, in Seval]
Options [library]
Orelse [definition, in Bool]
Orelse_rec_ff [lemma, in Bool]
Orelse_rec_ft [lemma, in Bool]
Orelse_rec_tf [lemma, in Bool]
Orelse_rec_tt [lemma, in Bool]
or_dec [instance, in Base]

P

P [definition, in Encoding]
Pair [definition, in Pairs]
Pairs [library]
Pair_correct [lemma, in Pairs]
parametrized_confluence [lemma, in ARS]
parametrized_semi_confluence [lemma, in ARS]
Partial [library]
PartialFunctions [section, in Partial]
PartialFunctions.F [variable, in Partial]
PartialFunctions.mono_F [variable, in Partial]
PartialFunctions.proc_F [variable, in Partial]
PartialFunctions.total_F [variable, in Partial]
penc [definition, in Pairs]
penc_closed [lemma, in Pairs]
penc_lam [lemma, in Pairs]
PEq [definition, in Pairs]
PEq_correct [lemma, in Pairs]
PEq_rec [lemma, in Pairs]
pi [definition, in Acceptability]
pi_eval [lemma, in RE]
Por [definition, in Por]
Por [library]
Por_correct_false [lemma, in Por]
Por_correct_true [lemma, in Por]
Por_correct_2 [lemma, in Por]
Por_correct_2' [lemma, in Por]
Por_correct_1 [lemma, in Por]
Por_correct_1b [lemma, in Por]
Por_correct_1a [lemma, in Por]
Por' [definition, in Por]
Por'_n_conv [lemma, in Por]
Por'_n_Sn [lemma, in Por]
Por'_rec [lemma, in Por]
Por'2 [definition, in Por]
Pos [definition, in Lists]
pos [definition, in Base]
pos [section, in Base]
Pos_correct [lemma, in Lists]
Pos_rec_cons [lemma, in Lists]
Pos_rec_nil [lemma, in Lists]
pos_elAt [lemma, in Base]
_ .[ _ ] [notation, in Base]
pow [definition, in ARS]
power [definition, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
powSk [lemma, in Lvw]
pow_add [lemma, in ARS]
pow_trans_lam [lemma, in Lvw]
Pred [definition, in Nat]
Pred_correct [lemma, in Nat]
proc [definition, in Lvw]
Proc [library]
proc_lambda [lemma, in Lists]
proc_lambda [lemma, in Tactics]
proc_closed [lemma, in Tactics]
P_correct [lemma, in Encoding]

Q

Q [definition, in Encoding]
Q_correct [lemma, in Encoding]
Q_rec_lam [lemma, in Encoding]
Q_rec_app [lemma, in Encoding]
Q_rec_var [lemma, in Encoding]

R

R [definition, in Lvw]
rcomp [definition, in ARS]
rcomp_comm [lemma, in ARS]
rcomp_1 [lemma, in ARS]
rcomp_eq [lemma, in ARS]
Re [definition, in RE]
RE [definition, in RE]
RE [library]
reflexive [definition, in ARS]
rem [definition, in Base]
Removal [section, in Base]
Removal.X [variable, 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 [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]
RE_Acc [lemma, in RE]
Re_converges [lemma, in RE]
Re_ge [lemma, in RE]
Re_S [lemma, in RE]
Re_rec [lemma, in RE]
Re_rec_s [lemma, in RE]
Rice [lemma, in Rice]
Rice [library]
Rice_classical [lemma, in Rice]
Rice1 [lemma, in Rice]
Rice2 [lemma, in Rice]
right_inv_surj [lemma, in bijection]
right_inverse [definition, in bijection]

S

Scott [lemma, in Scott]
Scott [library]
Se [definition, in Partial]
SecondFixedPoint [lemma, in Fixpoints]
self_div_comb [lemma, in Rice]
self_div [lemma, in Rice]
self_diverging_comb [definition, in Rice]
self_diverging [definition, in Rice]
semi_confluent_confluent [lemma, in ARS]
semi_confluent [definition, in ARS]
seval [inductive, in Seval]
Seval [library]
sevalR [constructor, in Seval]
sevalS [constructor, in Seval]
seval_eva [lemma, in Seval]
seval_S [lemma, in Seval]
seval_eval [lemma, in Seval]
seval_Eval [lemma, in Eval]
Se_correct [lemma, in Partial]
Se_correct' [lemma, in Partial]
Se_converges [lemma, in Partial]
sim [definition, in Lists]
Size [definition, in Size]
size [definition, in Encoding]
Size [library]
size_surj [lemma, in Size]
Size_correct [lemma, in Size]
size_induction [lemma, in Base]
some [definition, in Options]
some_inj [lemma, in Options]
some_correct [lemma, in Options]
some_correct_enc [lemma, in Options]
star [inductive, in ARS]
starC [constructor, in ARS]
starR [constructor, in ARS]
star_ecl [lemma, in ARS]
star_pow [lemma, in ARS]
star_trans [lemma, in ARS]
star_simpl_ind [lemma, in ARS]
star_equiv [lemma, in Lvw]
star_trans_r [lemma, in Lvw]
star_trans_l [lemma, in Lvw]
star_PreOrder [instance, in Lvw]
step [inductive, in Lvw]
stepApp [constructor, in Lvw]
stepAppL [constructor, in Lvw]
stepAppR [constructor, in Lvw]
step_value [lemma, in Lvw]
sublist_T [lemma, in Enum]
sublist_C [lemma, in Pairs]
Subst [definition, in Subst]
subst [definition, in Lvw]
Subst [library]
Subst_correct [lemma, in Subst]
Succ [definition, in Nat]
Succ_correct [lemma, in Nat]
surjective [definition, in bijection]
symmetric [definition, in ARS]
S' [definition, in Partial]
S'_0_n [lemma, in Partial]
S'_n_Sn [lemma, in Partial]
S'_rec [lemma, in Partial]

T

T [definition, in Enum]
Tactics [library]
tcompl [definition, in Decidability]
tconj [definition, in Decidability]
tdisj [definition, in Decidability]
tenc [definition, in Encoding]
tenc_inj [lemma, in Encoding]
tenc_injective [lemma, in Encoding]
tenc_lam [lemma, in Encoding]
tenc_cls [lemma, in Encoding]
term [inductive, in Lvw]
term_eq_dec_proc [definition, in Lvw]
term_eq_dec [instance, in Lvw]
tlenc [definition, in EnumInt]
tlenc_cls [lemma, in EnumInt]
tlenc_lam [lemma, in EnumInt]
totality [lemma, in MoreAcc]
totality_compl [lemma, in MoreAcc]
totality_proc [lemma, in MoreAcc]
transitive [definition, in ARS]
true [definition, in Bool]
true_equiv_false [lemma, in Bool]
True_dec [instance, in Base]
TT [definition, in EnumInt]
TT_correct [lemma, in EnumInt]
TT_S [lemma, in EnumInt]
TT_0 [lemma, in EnumInt]
T_dup [lemma, in Enum]
T_var_not [lemma, in Enum]
T_longenough [lemma, in Enum]
T_exhaustive [lemma, in Enum]
T_lam [lemma, in Enum]
T_el_ge [lemma, in Enum]
T_app [lemma, in Enum]
T_var [lemma, in Enum]
T_ge [lemma, in Enum]
T_S [lemma, in Enum]

U

U [definition, in EnumInt]
undup [definition, in Base]
Undup [section, in Base]
undup_idempotent [lemma, in Base]
undup_eq [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_fp_equi [lemma, in Base]
Undup.X [variable, in Base]
unenc [definition, in Encoding]
unenc_correct2 [lemma, in Encoding]
unenc_correct [lemma, in Encoding]
uniform_confluent [definition, in ARS]
uniform_confluence [lemma, in Lvw]
unique_normal_forms [lemma, in Lvw]
U_correct [lemma, in EnumInt]

V

var [constructor, in Lvw]
Var [definition, in Encoding]
Var_correct [lemma, in Encoding]

Z

Zero [definition, in Nat]

other

_ ⇓ _ _ [notation, in Seval]
_ ⇓ _ [notation, in Seval]
_ =2 _ [notation, in ARS]
_ <=2 _ [notation, in ARS]
_ =1 _ [notation, in ARS]
_ <=1 _ [notation, in ARS]
_ == _ [notation, in Lvw]
_ >* _ [notation, in Lvw]
_ >^ _ _ [notation, in Lvw]
_ >> _ [notation, in Lvw]
_ === _ [notation, in Base]
_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
_ .[ _ ] [notation, in Enum]
eq_dec _ [notation, in Base]
! _ [notation, in Lvw]
# _ [notation, in Lvw]
(λ _ ) [notation, in Lvw]
.\ _ , .. , _ ; _ [notation, in Lvw]
| _ | [notation, in Base]
λ _ , .. , _ ; _ [notation, in Lvw]