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 | (837 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 | (28 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 | (38 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 | (41 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 | (352 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 | (59 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 | (20 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 | (6 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 | (21 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 | (126 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 | (142 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 | (3 entries) |

# Global Index

## A

Acceptability [library]acc_conj_correct [lemma, in Acceptability]

acc_conj [definition, in Acceptability]

AD [lemma, in AD]

AD [library]

and_dec [instance, in Base]

app [constructor, in Lvw]

App [definition, in Encoding]

app_converges [lemma, in Seval]

app_closed [lemma, in Lvw]

app_equi_proper [instance, in Base]

app_eq_proper [lemma, in crush_no_refl_ideas]

ARS [library]

## B

bapp [constructor, in Lvw]Base [library]

BaseLists [library]

benchTerm [definition, in Reflection]

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_enc_correct [lemma, in LBool]

bool_enc_inj [instance, in LBool]

bool_enc [definition, in LBool]

bool_enc_inv_correct [lemma, in Computability]

bool_enc_inv [definition, in Computability]

bool_eq_dec [instance, in Base]

bter [constructor, in Lvw]

bterm [inductive, in Lvw]

bvar [constructor, in Lvw]

## C

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]

cChoice [definition, in Computability]

church_rosser [definition, in ARS]

church_rosser [lemma, in Lvw]

closed [definition, in Lvw]

closed_star [lemma, in Lvw]

closed_step [lemma, in Lvw]

closed_subst [lemma, in Lvw]

closed_dec [instance, in Lvw]

closed_app [lemma, in Lvw]

closed_dcl [lemma, in Lvw]

closed_k_dclosed [lemma, in Lvw]

closed_dcl_x [lemma, in LTactics]

clR [lemma, in crush_no_refl_ideas]

clR' [lemma, in crush_no_refl_ideas]

comb_proc_red [lemma, in Lvw]

Comp [inductive, in LvwClos]

CompApp [constructor, in LvwClos]

CompBeta [definition, in LvwClos_Eval]

CompBeta_sound [lemma, in LvwClos_Eval]

CompBeta_validComp [lemma, in LvwClos_Eval]

CompClos [constructor, in LvwClos]

complement [definition, in Decidability]

complete_induction [lemma, in Base]

CompSeval [definition, in LvwClos_Eval]

CompSeval_sound [lemma, in LvwClos_Eval]

CompSeval_validComp [lemma, in LvwClos_Eval]

CompStep_correct2 [lemma, in LvwClos]

CompStep_correct2' [lemma, in LvwClos]

Computability [library]

CompVar [constructor, in LvwClos]

Comp_ind_deep [definition, in LvwClos]

Comp_ind_deep' [definition, in LvwClos]

confluence [lemma, in Lvw]

confluent [definition, in ARS]

confluent_CR [lemma, in ARS]

conj [definition, in Decidability]

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]

convI [definition, in LTactics]

correct [definition, in internalize_def]

correct_t [projection, in internalize_def]

crush_no_refl_ideas [library]

CStep [inductive, in LvwClos]

CStepApp [constructor, in LvwClos]

CStepAppL [constructor, in LvwClos]

CStepAppR [constructor, in LvwClos]

CStepVal [constructor, in LvwClos]

CStepVar [constructor, in LvwClos]

CStep_equivC [lemma, in LvwClos]

CStep_reduceC [lemma, in LvwClos]

CStep_star_subrelation [instance, in LvwClos]

C27 [lemma, in Scott]

C27_proc [lemma, in Scott]

## D

database_dummy [lemma, in Tactics_old]dclApp [constructor, in Lvw]

dcllam [constructor, in Lvw]

dclosed [inductive, in Lvw]

dclosedb [definition, in Proc]

dclosedb_spec [lemma, in Proc]

dclosed_dec [instance, in Lvw]

dclosed_closed [lemma, in Lvw]

dclosed_gt [lemma, in Lvw]

dclosed_ge [lemma, in Lvw]

dclosed_closed_k [lemma, in Lvw]

dclvar [constructor, in Lvw]

dec [definition, in Base]

Decidability [library]

decides [definition, in Decidability]

decision [definition, in Base]

deClos [definition, in LvwClos]

deClos_lam [lemma, in LvwClos]

deClos_correct_star [lemma, in LvwClos]

deClos_correct' [lemma, in LvwClos]

deClos_correct'' [lemma, in LvwClos]

deClos_validEnv [lemma, in LvwClos]

deClos_valComp [lemma, in LvwClos]

dec_acc [lemma, in Acceptability]

dec_lacc [lemma, in Acceptability]

dec_P [lemma, in MuRec]

dec_pdec [lemma, in Computability]

dec_ldec [lemma, in Decidability]

dec_enc [lemma, in LNat]

dec_prop_iff [lemma, in Base]

dec_DM_impl [lemma, in Base]

dec_DM_and [lemma, in Base]

dec_DN [lemma, in Base]

denoteComp [definition, in Reflection]

denoteTerm [definition, in Reflection]

denoteTerm_correct [lemma, in Reflection]

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]

doesHaltIn [definition, in Eval]

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.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]

elAt [definition, in Base]

elAt_el [lemma, in Base]

elAt_app [lemma, in Base]

elAt' [definition, in internalize_tac]

el_elAt [lemma, in Base]

el_pos [lemma, in Base]

enc [definition, in internalize_def]

Encoding [library]

enc_extinj [lemma, in Computability]

enc_f [projection, in internalize_def]

eproc_equiv [lemma, in Seval]

eqApp [lemma, in Lvw]

eqC [constructor, in LvwClos]

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]

equivC [inductive, in LvwClos]

equivC_deClos [lemma, in LvwClos]

equivC_App_proper [instance, in LvwClos]

equivC_Equivalence [instance, in LvwClos]

equivC_if [lemma, in LvwClos]

equiv_eva [lemma, in Seval]

equiv_app_proper [instance, in Lvw]

equiv_lambda [lemma, in Lvw]

equiv_ecl [lemma, in Lvw]

equiv_Equivalence [instance, in Lvw]

equiv_trans_r [lemma, in Tactics_old]

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_term_dec [lemma, in Computability]

eq_ref [lemma, in ARS]

eq_dec_string [instance, in Lvw]

Eq_ldec [lemma, in Scott]

Eta [lemma, in Lvw]

eva [definition, in Seval]

eval [definition, in Seval]

Eval [definition, in Eval]

Eval [library]

eval_seval [lemma, in Seval]

eval_step [lemma, in Seval]

eval_converges [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]

expandDenote [lemma, in Reflection]

## 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.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 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_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.intX [variable, in Lists]

Fix_X.X [variable, in Lists]

Fix_X [section, in Lists]

Fix_X.intX [variable, in LOptions]

Fix_X.X [variable, in LOptions]

Fix_X [section, in LOptions]

Fix_X.eq_dec_X [variable, in BaseLists]

Fix_X.X [variable, in BaseLists]

Fix_X [section, in BaseLists]

Fix_XY.intY [variable, in LProd]

Fix_XY.Y [variable, in LProd]

Fix_XY.intX [variable, in LProd]

Fix_XY.X [variable, in LProd]

Fix_XY [section, in LProd]

FP [definition, in Base]

from_sumbool_elim [lemma, in SumBool]

from_sumbool [definition, in SumBool]

functional [definition, in ARS]

## H

helper [definition, in intermediate]## I

I [definition, in Lvw]iApp [constructor, in intermediate]

iConst [constructor, in intermediate]

iff_dec [instance, in Base]

iFix [constructor, in intermediate]

iLam [constructor, in intermediate]

iMatch [constructor, in intermediate]

impl_dec [instance, in Base]

inb [definition, in Lists]

inb_spec [lemma, in Lists]

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]

inj_enc [projection, in internalize_def]

inj_reg [record, in internalize_def]

int [definition, in internalize_def]

intApp [lemma, in LTactics]

intAppTest [lemma, in LTactics]

intApp' [instance, in LTactics]

intermediate [library]

internalizedClass [record, in internalize_def]

internalizer [projection, in internalize_def]

internalizesF [definition, in internalize_def]

internalize_tac [library]

internalize_demo [library]

internalize_def [library]

intFApp [lemma, in LTactics]

intFEquiv [lemma, in LTactics]

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]

iTerm [inductive, in intermediate]

iType [constructor, in intermediate]

it_fp [lemma, in Base]

it_ind [lemma, in Base]

iVar [constructor, in intermediate]

I_neq_Omega [lemma, in Scott]

I_proc [lemma, in LTactics]

## J

joinable [definition, in ARS]## K

K [definition, in Lvw]K_proc [lemma, in LTactics]

## 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]

lambdaComp [constructor, in LvwClos]

lambda_dec [instance, in Lvw]

lambda_lam [lemma, in Lvw]

lamComp [inductive, in LvwClos]

lamComp_star [lemma, in LvwClos]

lamComp_noStep [lemma, in LvwClos]

lamOmega [lemma, in Rice]

lam_app_proper [lemma, in crush_no_refl_ideas]

LBool [library]

lcomp_comp [lemma, in Computability]

ldec [definition, in Decidability]

ldec_dec [lemma, in Computability]

ldec_disj [lemma, in Decidability]

ldec_conj [lemma, in Decidability]

ldec_complement [lemma, in Decidability]

ldec_proc [lemma, in Proc]

ldec_closed [lemma, in Proc]

ldec_lambda [lemma, in Proc]

left_inv_inj [lemma, in bijection]

left_inverse [definition, in bijection]

liftPhi [definition, in Reflection]

liftPhi_correct [lemma, in Reflection]

Lists [library]

lists_cons [definition, in Lists]

list_enc_correct [lemma, in Lists]

list_enc_inj [instance, in Lists]

list_enc [definition, in Lists]

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]

LNat [library]

LOptions [library]

LProd [library]

LProp [library]

lStep [lemma, in crush_no_refl_ideas]

LTactics [library]

Lvw [library]

LvwClos [library]

LvwClos_Eval [library]

## M

map_ext' [lemma, in Reflection]mk_inj_reg [constructor, in internalize_def]

mk_registered [constructor, in internalize_def]

MoreAcc [library]

mu [definition, in MuRec]

MuRec [library]

MuRecursor [section, in MuRec]

MuRecursor.dec'_P [variable, in MuRec]

MuRecursor.P [variable, in MuRec]

MuRecursor.P_proc [variable, in MuRec]

mu_complete [lemma, in MuRec]

mu_sound [lemma, in MuRec]

mu_proc [lemma, in MuRec]

mu' [definition, in MuRec]

mu'_complete [lemma, in MuRec]

mu'_sound [lemma, in MuRec]

mu'_n_true [lemma, in MuRec]

mu'_0_false [lemma, in MuRec]

mu'_n_false [lemma, in MuRec]

mu'_proc [lemma, in MuRec]

## N

name_after_dot [definition, in StringBase]name_after_dot' [definition, in StringBase]

nat_enc_proc [lemma, in LNat]

nat_enc_correct [lemma, in LNat]

nat_enc_inj [instance, in LNat]

nat_S [definition, in LNat]

nat_enc [definition, in LNat]

nat_le_dec [instance, in Base]

nat_eq_dec [instance, in Base]

normComp [definition, in LvwClos]

normComp_valid [lemma, in LvwClos]

normComp_idem [lemma, in LvwClos]

normComp_star [lemma, in LvwClos]

normComp_deClos [lemma, in LvwClos]

normComp' [definition, in LvwClos]

normComp'_valid [lemma, in LvwClos]

normComp'_idem [lemma, in LvwClos]

normComp'_star [lemma, in LvwClos]

normComp'_deClos [lemma, in LvwClos]

not_dec [instance, in Base]

nth_error_none [lemma, in Base]

## O

oenc_correct_some [lemma, in LOptions]Omega [definition, in Lvw]

omega [definition, in Lvw]

Omega_diverges [lemma, in Seval]

Omega_closed [lemma, in LTactics]

omega_proc [lemma, in LTactics]

on0 [definition, in internalize_demo]

option_enc_correct [lemma, in LOptions]

option_enc_inj [instance, in LOptions]

option_some [definition, in LOptions]

option_none [definition, in LOptions]

option_enc [definition, in LOptions]

option_enc_inj [instance, in LProd]

or_dec [instance, in Base]

## P

parametrized_confluence [lemma, in ARS]parametrized_semi_confluence [lemma, in ARS]

pi [definition, in Acceptability]

Por [definition, in Por]

Por [library]

Por_correct' [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_proc [lemma, in Por]

pos [definition, in Base]

pos [section, in Base]

pos_length [lemma, in BaseLists]

pos_second_S [lemma, in BaseLists]

pos_first_S [lemma, in BaseLists]

pos_None [lemma, in BaseLists]

pos_elAt [lemma, in Base]

pos.X [variable, 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_star [lemma, in ARS]

pow_trans_lam [lemma, in Lvw]

pow_trans_lam' [lemma, in Lvw]

Proc [definition, in Reflection]

proc [definition, in Lvw]

Proc [library]

proc_t [projection, in internalize_def]

proc_enc [projection, in internalize_def]

proc_dec [lemma, in Lvw]

proc_lambda [lemma, in Tactics_old]

proc_closed [lemma, in Tactics_old]

prod_eq_dec [instance, in Base]

prod_enc_correct [lemma, in LProd]

prod_enc [definition, in LProd]

prop_term [instance, in LProp]

prop_enc [definition, in LProp]

## R

R [definition, in Lvw]r [definition, in Lvw]

rApp [constructor, in Reflection]

rClosed [definition, in Reflection]

rClosed_decb_correct [lemma, in Reflection]

rClosed_decb [definition, in Reflection]

rClosed_decb'_correct [lemma, in Reflection]

rClosed_decb' [definition, in Reflection]

rClosed_valid [lemma, in Reflection]

rComp [inductive, in Reflection]

rcomp [definition, in ARS]

rCompApp [constructor, in Reflection]

rCompBeta [definition, in Reflection]

rCompBeta_rValidComp [lemma, in Reflection]

rCompBeta_sound [lemma, in Reflection]

rCompClos [constructor, in Reflection]

rCompSeval [definition, in Reflection]

rCompSeval_rValidComp [lemma, in Reflection]

rCompSeval_sound [lemma, in Reflection]

rCompSeval' [definition, in Reflection]

rCompVar [constructor, in Reflection]

rComp_ind_deep [definition, in Reflection]

rComp_ind_deep' [definition, in Reflection]

rcomp_comm [lemma, in ARS]

rcomp_1 [lemma, in ARS]

rcomp_eq [lemma, in ARS]

rConst [constructor, in Reflection]

rDeClos [definition, in Reflection]

rDeClos_rValidComp [lemma, in Reflection]

rDeClos_reduce [lemma, in Reflection]

redC [constructor, in LvwClos]

reduceC [inductive, in LvwClos]

reduceC_App_proper [instance, in LvwClos]

reduceC_PreOrder [instance, in LvwClos]

reduceC_if [lemma, in LvwClos]

Reflection [library]

reflection_1 [definition, in SumBool]

reflection_2 [definition, in SumBool]

reflect_dec [lemma, in SumBool]

reflexive [definition, in ARS]

registered [record, in internalize_def]

register_list [instance, in Lists]

register_Prop_el [instance, in LProp]

register_bool [instance, in LBool]

register_option [instance, in LOptions]

register_nat [instance, in LNat]

register_unit [instance, in internalize_demo]

register_unit [instance, in internalize_demo]

register_prod [instance, in LProd]

register_term [instance, in Encoding]

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]

replace [definition, in BaseLists]

replace_pos [lemma, in BaseLists]

replace_diff [lemma, in BaseLists]

replace_same [lemma, in BaseLists]

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]

rEquiv [definition, in Reflection]

rEquivIntro [lemma, in Reflection]

rEquiv_rApp_proper [instance, in Reflection]

rEquiv_Equivalence [instance, in Reflection]

rev_string [definition, in StringBase]

rho [definition, in Lvw]

rho_cls [lemma, in LTactics]

rho_lambda [lemma, in LTactics]

rho_inj [lemma, in LTactics]

rho_correct [lemma, in LTactics]

rho_dcls [lemma, in LTactics]

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]

rLam [constructor, in Reflection]

rReduce [definition, in Reflection]

rReduceIntro [lemma, in Reflection]

rReduce_rEquiv_subrelation [instance, in Reflection]

rReduce_rApp_proper [instance, in Reflection]

rReduce_PreOrder [instance, in Reflection]

rStandardize [lemma, in Reflection]

rStandardizeGoal [lemma, in Reflection]

rStandardizeGoalLeft [lemma, in Reflection]

rStandardizeGoalLeft' [lemma, in Reflection]

rStandardizeHypo [lemma, in Reflection]

rStandardizeUse [lemma, in Reflection]

rStar'_App_proper [instance, in LvwClos]

rStar'_trans_r [lemma, in LvwClos]

rStar'_trans_l [lemma, in LvwClos]

rStar'_PreOrder [instance, in LvwClos]

rSubstList [definition, in Reflection]

rSubstList_correct [lemma, in Reflection]

rTerm [inductive, in Reflection]

rValidComp [definition, in Reflection]

rVar [constructor, in Reflection]

## S

Scott [lemma, in Scott]Scott [library]

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]

size [definition, in Lvw]

Size [library]

size_surj [lemma, in Size]

size_induction [lemma, in Base]

star [inductive, in ARS]

starC [constructor, in ARS]

starC_equivC [lemma, in LvwClos]

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_subrelation [instance, in Lvw]

star_equiv [lemma, in Lvw]

star_closed_proper [instance, in Lvw]

star_step_app_proper [instance, 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_equiv_subrelation [instance, in Lvw]

step_star_subrelation [instance, in Lvw]

step_star [lemma, in Lvw]

step_value [lemma, in Lvw]

stHypo [lemma, in LTactics]

String [definition, in internalize_tac]

StringBase [library]

subst [definition, in Lvw]

Subst [library]

substList [definition, in LvwClos]

substList_nil [lemma, in LvwClos]

substList_closed' [lemma, in LvwClos]

substList_is_dclosed [lemma, in LvwClos]

substList_var [lemma, in LvwClos]

substList_var' [lemma, in LvwClos]

substList_closed [lemma, in LvwClos]

substList_dclosed [lemma, in LvwClos]

subst_substList [lemma, in LvwClos]

subst' [definition, in crush_no_refl_ideas]

subst'_rho [lemma, in crush_no_refl_ideas]

subst'_eq_proper [lemma, in crush_no_refl_ideas]

subst'_enc [lemma, in crush_no_refl_ideas]

subst'_int [lemma, in crush_no_refl_ideas]

subst'_cls [lemma, in crush_no_refl_ideas]

subst'_eq [lemma, in crush_no_refl_ideas]

SumBool [library]

sumbool_enc_correct [lemma, in SumBool]

sumbool_term [instance, in SumBool]

sumbool_enc [definition, in SumBool]

surjective [definition, in bijection]

symmetric [definition, in ARS]

## T

Tactics_old [library]tcompl [definition, in Decidability]

tconj [definition, in Decidability]

tdisj [definition, in Decidability]

term [inductive, in Lvw]

term_term_eq_dec [instance, in Equality]

term_term_eqb [instance, in Equality]

term_eqb [definition, in Equality]

term_nat_eq_dec [instance, in Equality]

term_nat_eqb [instance, in Equality]

term_elAt [instance, in Lists]

term_nth_error [instance, in Lists]

term_map [instance, in Lists]

term_pos [instance, in Lists]

term_list_in_dec [instance, in Lists]

term_inb [instance, in Lists]

term_nth [instance, in Lists]

term_filter [instance, in Lists]

term_append [instance, in Lists]

term_cons [instance, in Lists]

term_nil [instance, in Lists]

term_size [instance, in Size]

term_subst [instance, in Subst]

term_orb [instance, in LBool]

term_andb [instance, in LBool]

term_negb [instance, in LBool]

term_false [instance, in LBool]

term_true [instance, in LBool]

term_option_map [instance, in LOptions]

term_Some [instance, in LOptions]

term_None [instance, in LOptions]

term_nat_le_dec [instance, in LNat]

term_leb [instance, in LNat]

term_mult [instance, in LNat]

term_plus [instance, in LNat]

term_pred [instance, in LNat]

term_S [instance, in LNat]

term_O [instance, in LNat]

term_not_dec [instance, in SumBool]

term_impl_dec [instance, in SumBool]

term_from_sumbool [instance, in SumBool]

term_to_sumbool [instance, in SumBool]

term_right [instance, in SumBool]

term_left [instance, in SumBool]

term_False_dec [instance, in SumBool]

term_True_dec [instance, in SumBool]

term_eq_dec_proc [definition, in Lvw]

term_eq_dec [instance, in Lvw]

term_nat_eqb [instance, in internalize_demo]

term_option_map [instance, in internalize_demo]

term_on0 [instance, in internalize_demo]

term_prod_eq_dec [instance, in LProd]

term_snd [instance, in LProd]

term_fst [instance, in LProd]

term_pair [instance, in LProd]

term_doesHaltIn [instance, in Eval]

term_eva [instance, in Eval]

term_term_enc [instance, in Encoding]

term_nat_enc [instance, in Encoding]

term_lam [instance, in Encoding]

term_app [instance, in Encoding]

term_var [instance, in Encoding]

term_enc_correct [lemma, in Encoding]

term_enc_inj [instance, in Encoding]

term_enc [definition, in Encoding]

term_lambda_dec [instance, in Proc]

term_closed_dec [instance, in Proc]

term_dclosed_dec [instance, in Proc]

term_dclosedb [instance, in Proc]

term_unenc [instance, in Unenc]

test [instance, in internalize_demo]

testT [definition, in internalize_demo]

test_Some_nat [lemma, in internalize_demo]

totality [lemma, in MoreAcc]

totality_compl [lemma, in MoreAcc]

totality_proc [lemma, in MoreAcc]

to_list [definition, in StringBase]

to_string [definition, in StringBase]

to_sumbool [definition, in SumBool]

transform [definition, in internalize_tac]

transitive [definition, in ARS]

True_dec [instance, in Base]

TT [inductive, in internalize_def]

TyAll [constructor, in internalize_def]

TyB [constructor, in internalize_def]

TyElim [constructor, in internalize_def]

## U

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 LNat]

Unenc [library]

unenc_correct2 [lemma, in LNat]

unenc_correct [lemma, in LNat]

uniform_confluent [definition, in ARS]

uniform_confluence [lemma, in Lvw]

unique_normal_forms [lemma, in Lvw]

unit_enc [definition, in internalize_demo]

## V

validComp [inductive, in LvwClos]validCompApp [constructor, in LvwClos]

validCompClos [constructor, in LvwClos]

validComp_star [lemma, in LvwClos]

validComp_closed [lemma, in LvwClos]

validComp_step [lemma, in LvwClos]

validEnv [definition, in LvwClos]

validEnv_cons [lemma, in LvwClos]

validEnv' [definition, in LvwClos]

validEnv'_cons [lemma, in LvwClos]

var [constructor, in Lvw]

Var [definition, in Encoding]

## other

_ >[]* _ (LvwClos) [notation, in LvwClos]_ >[]> _ (LvwClos) [notation, in LvwClos]

_ â‡“ _ _ [notation, in Seval]

_ â‡“ _ [notation, in Seval]

_ =[]= _ [notation, in LvwClos]

_ =[]> _ [notation, in LvwClos]

_ ~> _ [notation, in internalize_def]

_ =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]

eq_dec _ [notation, in Base]

internalized _ [notation, in internalize_tac]

!! _ [notation, in Lvw]

! _ [notation, in internalize_def]

# _ [notation, in Lvw]

(Î» _ ) [notation, in Lvw]

.\ _ , .. , _ ; _ [notation, in Lvw]

| _ | [notation, in Base]

Î» _ , .. , _ ; _ [notation, in Lvw]

# Notation Index

## P

_ .[ _ ] [in Base]## other

_ >[]* _ (LvwClos) [in LvwClos]_ >[]> _ (LvwClos) [in LvwClos]

_ â‡“ _ _ [in Seval]

_ â‡“ _ [in Seval]

_ =[]= _ [in LvwClos]

_ =[]> _ [in LvwClos]

_ ~> _ [in internalize_def]

_ =2 _ [in ARS]

_ <=2 _ [in ARS]

_ =1 _ [in ARS]

_ <=1 _ [in ARS]

_ == _ [in Lvw]

_ >* _ [in Lvw]

_ >^ _ _ [in Lvw]

_ >> _ [in Lvw]

_ === _ [in Base]

_ <<= _ [in Base]

_ el _ [in Base]

eq_dec _ [in Base]

internalized _ [in internalize_tac]

!! _ [in Lvw]

! _ [in internalize_def]

# _ [in Lvw]

(Î» _ ) [in Lvw]

.\ _ , .. , _ ; _ [in Lvw]

| _ | [in Base]

Î» _ , .. , _ ; _ [in Lvw]

# Module Index

## F

FCI [in Base]# Variable Index

## B

bijections.A [in bijection]bijections.B [in bijection]

## C

Cardinality.X [in Base]## D

DupfreeLength.X [in Base]Dupfree.X [in Base]

## E

Equi.X [in Base]## F

FCI.FCI.step [in Base]FCI.FCI.V [in Base]

FCI.FCI.X [in Base]

FilterComm.p [in Base]

FilterComm.q [in Base]

FilterComm.X [in Base]

FilterLemmas_pq.q [in Base]

FilterLemmas_pq.p [in Base]

FilterLemmas_pq.X [in Base]

FilterLemmas.p [in Base]

FilterLemmas.X [in Base]

FixX.X [in ARS]

Fix_X.intX [in Lists]

Fix_X.X [in Lists]

Fix_X.intX [in LOptions]

Fix_X.X [in LOptions]

Fix_X.eq_dec_X [in BaseLists]

Fix_X.X [in BaseLists]

Fix_XY.intY [in LProd]

Fix_XY.Y [in LProd]

Fix_XY.intX [in LProd]

Fix_XY.X [in LProd]

## I

Inclusion.X [in Base]Iteration.f [in Base]

Iteration.X [in Base]

## M

MuRecursor.dec'_P [in MuRec]MuRecursor.P [in MuRec]

MuRecursor.P_proc [in MuRec]

## P

pos.X [in Base]PowerRep.X [in Base]

## R

Removal.X [in Base]## U

Undup.X [in Base]# Library Index

## A

AcceptabilityAD

ARS

## B

BaseBaseLists

bijection

## C

Computabilitycrush_no_refl_ideas

## D

Decidability## E

EncodingEquality

Eval

## F

Fixpoints## I

intermediateinternalize_tac

internalize_demo

internalize_def

## L

LBoolLists

LNat

LOptions

LProd

LProp

LTactics

Lvw

LvwClos

LvwClos_Eval

## M

MoreAccMuRec

## P

PorProc

## R

ReflectionRice

## S

ScottSeval

Size

StringBase

Subst

SumBool

## T

Tactics_old## U

Unenc# Lemma Index

## A

acc_conj_correct [in Acceptability]AD [in AD]

app_converges [in Seval]

app_closed [in Lvw]

app_eq_proper [in crush_no_refl_ideas]

## B

bool_enc_correct [in LBool]bool_enc_inv_correct [in Computability]

## C

card_0 [in Base]card_cons_rem [in Base]

card_cons [in Base]

card_ex [in Base]

card_or [in Base]

card_lt [in Base]

card_equi [in Base]

card_eq [in Base]

card_le [in Base]

church_rosser [in Lvw]

closed_star [in Lvw]

closed_step [in Lvw]

closed_subst [in Lvw]

closed_app [in Lvw]

closed_dcl [in Lvw]

closed_k_dclosed [in Lvw]

closed_dcl_x [in LTactics]

clR [in crush_no_refl_ideas]

clR' [in crush_no_refl_ideas]

comb_proc_red [in Lvw]

CompBeta_sound [in LvwClos_Eval]

CompBeta_validComp [in LvwClos_Eval]

complete_induction [in Base]

CompSeval_sound [in LvwClos_Eval]

CompSeval_validComp [in LvwClos_Eval]

CompStep_correct2 [in LvwClos]

CompStep_correct2' [in LvwClos]

confluence [in Lvw]

confluent_CR [in ARS]

converges_equiv [in Lvw]

CStep_equivC [in LvwClos]

CStep_reduceC [in LvwClos]

C27 [in Scott]

C27_proc [in Scott]

## D

database_dummy [in Tactics_old]dclosedb_spec [in Proc]

dclosed_closed [in Lvw]

dclosed_gt [in Lvw]

dclosed_ge [in Lvw]

dclosed_closed_k [in Lvw]

deClos_lam [in LvwClos]

deClos_correct_star [in LvwClos]

deClos_correct' [in LvwClos]

deClos_correct'' [in LvwClos]

deClos_validEnv [in LvwClos]

deClos_valComp [in LvwClos]

dec_acc [in Acceptability]

dec_lacc [in Acceptability]

dec_P [in MuRec]

dec_pdec [in Computability]

dec_ldec [in Decidability]

dec_enc [in LNat]

dec_prop_iff [in Base]

dec_DM_impl [in Base]

dec_DM_and [in Base]

dec_DN [in Base]

denoteTerm_correct [in Reflection]

diamond_to_confluent [in ARS]

diamond_to_semi_confluent [in ARS]

disjoint_cons [in Base]

disjoint_forall [in Base]

dupfree_elAt [in Base]

dupfree_in_power [in Base]

dupfree_power [in Base]

dupfree_equi [in Base]

dupfree_ex [in Base]

dupfree_lt [in Base]

dupfree_eq [in Base]

dupfree_le [in Base]

dupfree_reorder [in Base]

dupfree_undup [in Base]

dupfree_dec [in Base]

dupfree_filter [in Base]

dupfree_map [in Base]

dupfree_app [in Base]

dupfree_inv [in Base]

## E

ecl_sym [in ARS]ecl_trans [in ARS]

elAt_el [in Base]

elAt_app [in Base]

el_elAt [in Base]

el_pos [in Base]

enc_extinj [in Computability]

eproc_equiv [in Seval]

eqApp [in Lvw]

eqStarT [in Lvw]

equivC_deClos [in LvwClos]

equivC_if [in LvwClos]

equiv_eva [in Seval]

equiv_lambda [in Lvw]

equiv_ecl [in Lvw]

equiv_trans_r [in Tactics_old]

equi_rotate [in Base]

equi_shift [in Base]

equi_swap [in Base]

equi_dup [in Base]

equi_push [in Base]

eq_term_dec [in Computability]

eq_ref [in ARS]

Eq_ldec [in Scott]

Eta [in Lvw]

eval_seval [in Seval]

eval_step [in Seval]

eval_converges [in Seval]

Eval_converges [in Eval]

eval_converges [in Eval]

Eval_eval [in Eval]

eval_Eval [in Eval]

Eval_correct [in Eval]

eva_Sn_n [in Seval]

eva_n_Sn [in Seval]

eva_equiv [in Seval]

eva_seval [in Seval]

eva_lam [in Seval]

expandDenote [in Reflection]

## F

FCI.closure [in Base]FCI.fp [in Base]

FCI.incl [in Base]

FCI.ind [in Base]

FCI.it_incl [in Base]

FCI.pick [in Base]

filter_comm [in Base]

filter_and [in Base]

filter_pq_eq [in Base]

filter_pq_mono [in Base]

filter_fst' [in Base]

filter_app [in Base]

filter_fst [in Base]

filter_mono [in Base]

filter_incl [in Base]

FirstFixedPoint [in Fixpoints]

from_sumbool_elim [in SumBool]

## I

inb_spec [in Lists]incl_lrcons [in Base]

incl_rcons [in Base]

incl_lcons [in Base]

incl_shift [in Base]

incl_nil_eq [in Base]

incl_map [in Base]

incl_nil [in Base]

intApp [in LTactics]

intAppTest [in LTactics]

intFApp [in LTactics]

intFEquiv [in LTactics]

inv2bij [in bijection]

in_rem_iff [in Base]

in_filter_iff [in Base]

in_cons_neq [in Base]

in_sing [in Base]

it_fp [in Base]

it_ind [in Base]

I_neq_Omega [in Scott]

I_proc [in LTactics]

## K

K_proc [in LTactics]## L

lacc_disj [in Acceptability]lacc_conj [in Acceptability]

lambda_lam [in Lvw]

lamComp_star [in LvwClos]

lamComp_noStep [in LvwClos]

lamOmega [in Rice]

lam_app_proper [in crush_no_refl_ideas]

lcomp_comp [in Computability]

ldec_dec [in Computability]

ldec_disj [in Decidability]

ldec_conj [in Decidability]

ldec_complement [in Decidability]

ldec_proc [in Proc]

ldec_closed [in Proc]

ldec_lambda [in Proc]

left_inv_inj [in bijection]

liftPhi_correct [in Reflection]

list_enc_correct [in Lists]

list_cc [in Base]

list_exists_DM [in Base]

list_sigma_forall [in Base]

list_cycle [in Base]

lStep [in crush_no_refl_ideas]

## M

map_ext' [in Reflection]mu_complete [in MuRec]

mu_sound [in MuRec]

mu_proc [in MuRec]

mu'_complete [in MuRec]

mu'_sound [in MuRec]

mu'_n_true [in MuRec]

mu'_0_false [in MuRec]

mu'_n_false [in MuRec]

mu'_proc [in MuRec]

## N

nat_enc_proc [in LNat]nat_enc_correct [in LNat]

normComp_valid [in LvwClos]

normComp_idem [in LvwClos]

normComp_star [in LvwClos]

normComp_deClos [in LvwClos]

normComp'_valid [in LvwClos]

normComp'_idem [in LvwClos]

normComp'_star [in LvwClos]

normComp'_deClos [in LvwClos]

nth_error_none [in Base]

## O

oenc_correct_some [in LOptions]Omega_diverges [in Seval]

Omega_closed [in LTactics]

omega_proc [in LTactics]

option_enc_correct [in LOptions]

## P

parametrized_confluence [in ARS]parametrized_semi_confluence [in ARS]

Por_correct' [in Por]

Por_correct_2 [in Por]

Por_correct_1 [in Por]

Por_correct_1b [in Por]

Por_correct_1a [in Por]

Por_proc [in Por]

pos_length [in BaseLists]

pos_second_S [in BaseLists]

pos_first_S [in BaseLists]

pos_None [in BaseLists]

pos_elAt [in Base]

power_extensional [in Base]

power_nil [in Base]

power_incl [in Base]

powSk [in Lvw]

pow_add [in ARS]

pow_star [in ARS]

pow_trans_lam [in Lvw]

pow_trans_lam' [in Lvw]

proc_dec [in Lvw]

proc_lambda [in Tactics_old]

proc_closed [in Tactics_old]

prod_enc_correct [in LProd]

## R

rClosed_decb_correct [in Reflection]rClosed_decb'_correct [in Reflection]

rClosed_valid [in Reflection]

rCompBeta_rValidComp [in Reflection]

rCompBeta_sound [in Reflection]

rCompSeval_rValidComp [in Reflection]

rCompSeval_sound [in Reflection]

rcomp_comm [in ARS]

rcomp_1 [in ARS]

rcomp_eq [in ARS]

rDeClos_rValidComp [in Reflection]

rDeClos_reduce [in Reflection]

reduceC_if [in LvwClos]

reflect_dec [in SumBool]

rem_fst' [in Base]

rem_fst [in Base]

rem_comm [in Base]

rem_equi [in Base]

rem_app' [in Base]

rem_app [in Base]

rem_neq [in Base]

rem_in [in Base]

rem_cons' [in Base]

rem_cons [in Base]

rem_mono [in Base]

rem_incl [in Base]

rem_not_in [in Base]

replace_pos [in BaseLists]

replace_diff [in BaseLists]

replace_same [in BaseLists]

rep_dupfree [in Base]

rep_idempotent [in Base]

rep_injective [in Base]

rep_eq [in Base]

rep_eq' [in Base]

rep_mono [in Base]

rep_equi [in Base]

rep_in [in Base]

rep_incl [in Base]

rep_power [in Base]

rEquivIntro [in Reflection]

rho_cls [in LTactics]

rho_lambda [in LTactics]

rho_inj [in LTactics]

rho_correct [in LTactics]

rho_dcls [in LTactics]

Rice [in Rice]

Rice_classical [in Rice]

Rice1 [in Rice]

Rice2 [in Rice]

right_inv_surj [in bijection]

rReduceIntro [in Reflection]

rStandardize [in Reflection]

rStandardizeGoal [in Reflection]

rStandardizeGoalLeft [in Reflection]

rStandardizeGoalLeft' [in Reflection]

rStandardizeHypo [in Reflection]

rStandardizeUse [in Reflection]

rStar'_trans_r [in LvwClos]

rStar'_trans_l [in LvwClos]

rSubstList_correct [in Reflection]

## S

Scott [in Scott]SecondFixedPoint [in Fixpoints]

self_div_comb [in Rice]

self_div [in Rice]

semi_confluent_confluent [in ARS]

seval_eva [in Seval]

seval_S [in Seval]

seval_eval [in Seval]

seval_Eval [in Eval]

size_surj [in Size]

size_induction [in Base]

starC_equivC [in LvwClos]

star_ecl [in ARS]

star_pow [in ARS]

star_trans [in ARS]

star_simpl_ind [in ARS]

star_equiv [in Lvw]

star_trans_r [in Lvw]

star_trans_l [in Lvw]

step_star [in Lvw]

step_value [in Lvw]

stHypo [in LTactics]

substList_nil [in LvwClos]

substList_closed' [in LvwClos]

substList_is_dclosed [in LvwClos]

substList_var [in LvwClos]

substList_var' [in LvwClos]

substList_closed [in LvwClos]

substList_dclosed [in LvwClos]

subst_substList [in LvwClos]

subst'_rho [in crush_no_refl_ideas]

subst'_eq_proper [in crush_no_refl_ideas]

subst'_enc [in crush_no_refl_ideas]

subst'_int [in crush_no_refl_ideas]

subst'_cls [in crush_no_refl_ideas]

subst'_eq [in crush_no_refl_ideas]

sumbool_enc_correct [in SumBool]

## T

term_enc_correct [in Encoding]test_Some_nat [in internalize_demo]

totality [in MoreAcc]

totality_compl [in MoreAcc]

totality_proc [in MoreAcc]

## U

undup_idempotent [in Base]undup_eq [in Base]

undup_equi [in Base]

undup_incl [in Base]

undup_fp_equi [in Base]

unenc_correct2 [in LNat]

unenc_correct [in LNat]

uniform_confluence [in Lvw]

unique_normal_forms [in Lvw]

## V

validComp_star [in LvwClos]validComp_closed [in LvwClos]

validComp_step [in LvwClos]

validEnv_cons [in LvwClos]

validEnv'_cons [in LvwClos]

# Constructor Index

## A

app [in Lvw]## B

bapp [in Lvw]blam [in Lvw]

bter [in Lvw]

bvar [in Lvw]

## C

CompApp [in LvwClos]CompClos [in LvwClos]

CompVar [in LvwClos]

CStepApp [in LvwClos]

CStepAppL [in LvwClos]

CStepAppR [in LvwClos]

CStepVal [in LvwClos]

CStepVar [in LvwClos]

## D

dclApp [in Lvw]dcllam [in Lvw]

dclvar [in Lvw]

dupfreeC [in Base]

dupfreeN [in Base]

## E

eclC [in ARS]eclR [in ARS]

eclS [in ARS]

eqC [in LvwClos]

eqRef [in Lvw]

eqStep [in Lvw]

eqSym [in Lvw]

eqTrans [in Lvw]

## I

iApp [in intermediate]iConst [in intermediate]

iFix [in intermediate]

iLam [in intermediate]

iMatch [in intermediate]

is_bijective [in bijection]

iType [in intermediate]

iVar [in intermediate]

## L

lam [in Lvw]lambdaComp [in LvwClos]

## M

mk_inj_reg [in internalize_def]mk_registered [in internalize_def]

## R

rApp [in Reflection]rCompApp [in Reflection]

rCompClos [in Reflection]

rCompVar [in Reflection]

rConst [in Reflection]

redC [in LvwClos]

rLam [in Reflection]

rVar [in Reflection]

## S

sevalR [in Seval]sevalS [in Seval]

starC [in ARS]

starR [in ARS]

stepApp [in Lvw]

stepAppL [in Lvw]

stepAppR [in Lvw]

## T

TyAll [in internalize_def]TyB [in internalize_def]

TyElim [in internalize_def]

## V

validCompApp [in LvwClos]validCompClos [in LvwClos]

var [in Lvw]

# Inductive Index

## B

bijective [in bijection]bterm [in Lvw]

## C

Comp [in LvwClos]CStep [in LvwClos]

## D

dclosed [in Lvw]dupfree [in Base]

## E

ecl [in ARS]equiv [in Lvw]

equivC [in LvwClos]

## I

iTerm [in intermediate]## L

lamComp [in LvwClos]## R

rComp [in Reflection]reduceC [in LvwClos]

rTerm [in Reflection]

## S

seval [in Seval]star [in ARS]

step [in Lvw]

## T

term [in Lvw]TT [in internalize_def]

## V

validComp [in LvwClos]# Projection Index

## C

correct_t [in internalize_def]## E

enc_f [in internalize_def]## I

inj_enc [in internalize_def]internalizer [in internalize_def]

## P

proc_t [in internalize_def]proc_enc [in internalize_def]

# Section Index

## B

bijections [in bijection]## C

Cardinality [in Base]## D

Dupfree [in Base]DupfreeLength [in Base]

## E

Equi [in Base]## F

FCI.FCI [in Base]FilterComm [in Base]

FilterLemmas [in Base]

FilterLemmas_pq [in Base]

FixX [in ARS]

Fix_X [in Lists]

Fix_X [in LOptions]

Fix_X [in BaseLists]

Fix_XY [in LProd]

## I

Inclusion [in Base]Iteration [in Base]

## M

MuRecursor [in MuRec]## P

pos [in Base]PowerRep [in Base]

## R

Removal [in Base]## U

Undup [in Base]# Instance Index

## A

and_dec [in Base]app_equi_proper [in Base]

## B

bool_enc_inj [in LBool]bool_eq_dec [in Base]

## C

card_equi_proper [in Base]closed_dec [in Lvw]

cons_equi_proper [in Base]

converges_proper [in Lvw]

CStep_star_subrelation [in LvwClos]

## D

dclosed_dec [in Lvw]## E

equivC_App_proper [in LvwClos]equivC_Equivalence [in LvwClos]

equiv_app_proper [in Lvw]

equiv_Equivalence [in Lvw]

equi_Equivalence [in Base]

eq_dec_string [in Lvw]

## F

False_dec [in Base]## I

iff_dec [in Base]impl_dec [in Base]

incl_preorder [in Base]

incl_equi_proper [in Base]

intApp' [in LTactics]

in_equi_proper [in Base]

## L

lambda_dec [in Lvw]list_enc_inj [in Lists]

list_exists_dec [in Base]

list_forall_dec [in Base]

list_in_dec [in Base]

list_eq_dec [in Base]

## N

nat_enc_inj [in LNat]nat_le_dec [in Base]

nat_eq_dec [in Base]

not_dec [in Base]

## O

option_enc_inj [in LOptions]option_enc_inj [in LProd]

or_dec [in Base]

## P

prod_eq_dec [in Base]prop_term [in LProp]

## R

reduceC_App_proper [in LvwClos]reduceC_PreOrder [in LvwClos]

register_list [in Lists]

register_Prop_el [in LProp]

register_bool [in LBool]

register_option [in LOptions]

register_nat [in LNat]

register_unit [in internalize_demo]

register_unit [in internalize_demo]

register_prod [in LProd]

register_term [in Encoding]

rEquiv_rApp_proper [in Reflection]

rEquiv_Equivalence [in Reflection]

rReduce_rEquiv_subrelation [in Reflection]

rReduce_rApp_proper [in Reflection]

rReduce_PreOrder [in Reflection]

rStar'_App_proper [in LvwClos]

rStar'_PreOrder [in LvwClos]

## S

star_equiv_subrelation [in Lvw]star_closed_proper [in Lvw]

star_step_app_proper [in Lvw]

star_PreOrder [in Lvw]

step_equiv_subrelation [in Lvw]

step_star_subrelation [in Lvw]

sumbool_term [in SumBool]

## T

term_term_eq_dec [in Equality]term_term_eqb [in Equality]

term_nat_eq_dec [in Equality]

term_nat_eqb [in Equality]

term_elAt [in Lists]

term_nth_error [in Lists]

term_map [in Lists]

term_pos [in Lists]

term_list_in_dec [in Lists]

term_inb [in Lists]

term_nth [in Lists]

term_filter [in Lists]

term_append [in Lists]

term_cons [in Lists]

term_nil [in Lists]

term_size [in Size]

term_subst [in Subst]

term_orb [in LBool]

term_andb [in LBool]

term_negb [in LBool]

term_false [in LBool]

term_true [in LBool]

term_option_map [in LOptions]

term_Some [in LOptions]

term_None [in LOptions]

term_nat_le_dec [in LNat]

term_leb [in LNat]

term_mult [in LNat]

term_plus [in LNat]

term_pred [in LNat]

term_S [in LNat]

term_O [in LNat]

term_not_dec [in SumBool]

term_impl_dec [in SumBool]

term_from_sumbool [in SumBool]

term_to_sumbool [in SumBool]

term_right [in SumBool]

term_left [in SumBool]

term_False_dec [in SumBool]

term_True_dec [in SumBool]

term_eq_dec [in Lvw]

term_nat_eqb [in internalize_demo]

term_option_map [in internalize_demo]

term_on0 [in internalize_demo]

term_prod_eq_dec [in LProd]

term_snd [in LProd]

term_fst [in LProd]

term_pair [in LProd]

term_doesHaltIn [in Eval]

term_eva [in Eval]

term_term_enc [in Encoding]

term_nat_enc [in Encoding]

term_lam [in Encoding]

term_app [in Encoding]

term_var [in Encoding]

term_enc_inj [in Encoding]

term_lambda_dec [in Proc]

term_closed_dec [in Proc]

term_dclosed_dec [in Proc]

term_dclosedb [in Proc]

term_unenc [in Unenc]

test [in internalize_demo]

True_dec [in Base]

# Definition Index

## A

acc_conj [in Acceptability]App [in Encoding]

## B

benchTerm [in Reflection]bool_enc [in LBool]

bool_enc_inv [in Computability]

## C

card [in Base]cChoice [in Computability]

church_rosser [in ARS]

closed [in Lvw]

CompBeta [in LvwClos_Eval]

complement [in Decidability]

CompSeval [in LvwClos_Eval]

Comp_ind_deep [in LvwClos]

Comp_ind_deep' [in LvwClos]

confluent [in ARS]

conj [in Decidability]

converges [in Lvw]

convert [in Lvw]

convert' [in Lvw]

convI [in LTactics]

correct [in internalize_def]

## D

dclosedb [in Proc]dec [in Base]

decides [in Decidability]

decision [in Base]

deClos [in LvwClos]

denoteComp [in Reflection]

denoteTerm [in Reflection]

diamond [in ARS]

disj [in Decidability]

disjoint [in Base]

doesHaltIn [in Eval]

## E

elAt [in Base]elAt' [in internalize_tac]

enc [in internalize_def]

equi [in Base]

eva [in Seval]

eval [in Seval]

Eval [in Eval]

## F

FCI.C [in Base]FCI.F [in Base]

filter [in Base]

FP [in Base]

from_sumbool [in SumBool]

functional [in ARS]

## H

helper [in intermediate]## I

I [in Lvw]inb [in Lists]

inclp [in Base]

injective [in bijection]

int [in internalize_def]

internalizesF [in internalize_def]

inverse [in bijection]

it [in Base]

## J

joinable [in ARS]## K

K [in Lvw]## L

lacc [in Acceptability]Lam [in Encoding]

lambda [in Lvw]

ldec [in Decidability]

left_inverse [in bijection]

liftPhi [in Reflection]

lists_cons [in Lists]

list_enc [in Lists]

## M

mu [in MuRec]mu' [in MuRec]

## N

name_after_dot [in StringBase]name_after_dot' [in StringBase]

nat_S [in LNat]

nat_enc [in LNat]

normComp [in LvwClos]

normComp' [in LvwClos]

## O

Omega [in Lvw]omega [in Lvw]

on0 [in internalize_demo]

option_some [in LOptions]

option_none [in LOptions]

option_enc [in LOptions]

## P

pi [in Acceptability]Por [in Por]

pos [in Base]

pow [in ARS]

power [in Base]

Proc [in Reflection]

proc [in Lvw]

prod_enc [in LProd]

prop_enc [in LProp]

## R

R [in Lvw]r [in Lvw]

rClosed [in Reflection]

rClosed_decb [in Reflection]

rClosed_decb' [in Reflection]

rcomp [in ARS]

rCompBeta [in Reflection]

rCompSeval [in Reflection]

rCompSeval' [in Reflection]

rComp_ind_deep [in Reflection]

rComp_ind_deep' [in Reflection]

rDeClos [in Reflection]

reflection_1 [in SumBool]

reflection_2 [in SumBool]

reflexive [in ARS]

rem [in Base]

rep [in Base]

replace [in BaseLists]

rEquiv [in Reflection]

rev_string [in StringBase]

rho [in Lvw]

right_inverse [in bijection]

rReduce [in Reflection]

rSubstList [in Reflection]

rValidComp [in Reflection]

## S

self_diverging_comb [in Rice]self_diverging [in Rice]

semi_confluent [in ARS]

size [in Lvw]

String [in internalize_tac]

subst [in Lvw]

substList [in LvwClos]

subst' [in crush_no_refl_ideas]

sumbool_enc [in SumBool]

surjective [in bijection]

symmetric [in ARS]

## T

tcompl [in Decidability]tconj [in Decidability]

tdisj [in Decidability]

term_eqb [in Equality]

term_eq_dec_proc [in Lvw]

term_enc [in Encoding]

testT [in internalize_demo]

to_list [in StringBase]

to_string [in StringBase]

to_sumbool [in SumBool]

transform [in internalize_tac]

transitive [in ARS]

## U

undup [in Base]unenc [in LNat]

uniform_confluent [in ARS]

unit_enc [in internalize_demo]

## V

validEnv [in LvwClos]validEnv' [in LvwClos]

Var [in Encoding]

# Record Index

## I

inj_reg [in internalize_def]internalizedClass [in internalize_def]

## R

registered [in internalize_def]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 | (837 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 | (28 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 | (38 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 | (41 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 | (352 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 | (59 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 | (20 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 | (6 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 | (21 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 | (126 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 | (142 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 | (3 entries) |