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

(1398 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

(35 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

(16 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(20 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

(22 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

(342 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

(120 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 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

(66 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

(56 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

(12 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

(15 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 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

(660 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

(19 entries)

---

Global Index

A

Acc [inductive, in PRFA.review6]
Acc [inductive, in PRFA.live_coding5]
acc [abbreviation, in PRFA.tp5c]
Acc_sind [definition, in PRFA.review6]
Acc_ind [definition, in PRFA.review6]
Acc_intro [constructor, in PRFA.review6]
Acc_iff [lemma, in PRFA.live_coding5]
Acc_sind [definition, in PRFA.live_coding5]
Acc_rec [definition, in PRFA.live_coding5]
Acc_ind [definition, in PRFA.live_coding5]
Acc_rect [definition, in PRFA.live_coding5]
Acc_intro [constructor, in PRFA.live_coding5]
Acc_rect_dep [lemma, in PRFA.tp5c]
acc_implies_P_eventually [lemma, in PRFA.tp5c]
aConst [constructor, in PRFA.tp6c]
add [definition, in PRFA.tp2c]
add [definition, in PRFA.live_coding3]
add_from_nat [lemma, in PRFA.tp2c]
add_sub [lemma, in PRFA.review2]
add' [definition, in PRFA.review7]
add'_correct [lemma, in PRFA.review7]
Advanced [section, in PRFA.tp1c]
All [inductive, in PRFA.tp3c]
all_equal [definition, in PRFA.live_coding7]
all_equal [definition, in PRFA.tp7c]
All_sind [definition, in PRFA.tp3c]
All_rec [definition, in PRFA.tp3c]
All_ind [definition, in PRFA.tp3c]
All_rect [definition, in PRFA.tp3c]
All_cons [constructor, in PRFA.tp3c]
All_nil [constructor, in PRFA.tp3c]
andb_orb_distr [lemma, in PRFA.tp1c]
andb_comm' [lemma, in PRFA.live_coding1]
andb_comm [lemma, in PRFA.live_coding1]
and_comm [lemma, in PRFA.tp1c]
and_assoc [lemma, in PRFA.tp4c]
and_com [lemma, in PRFA.tp4c]
and_AA [lemma, in PRFA.tp4c]
and_comm [lemma, in PRFA.live_coding1]
anything_goes [lemma, in PRFA.tp1c]
anything_goes [lemma, in PRFA.live_coding1]
aPlus [constructor, in PRFA.tp6c]
app [definition, in PRFA.live_coding8]
app_assoc [lemma, in PRFA.tp2c]
app_nil_r [lemma, in PRFA.tp2c]
app_nil_r [lemma, in PRFA.live_coding2]
app_nil_r [lemma, in PRFA.live_coding8]
app_assoc [lemma, in PRFA.live_coding8]
app_ind [lemma, in PRFA.live_coding8]
arith [inductive, in PRFA.tp6c]
arith_sind [definition, in PRFA.tp6c]
arith_rec [definition, in PRFA.tp6c]
arith_ind [definition, in PRFA.tp6c]
arith_rect [definition, in PRFA.tp6c]
assms [definition, in PRFA.tp6c]
assumptions [definition, in PRFA.tp6c]
assumptions_alt [definition, in PRFA.tp6c]
assums [section, in PRFA.tp6c]
assum_fold [definition, in PRFA.tp6c]
aTimes [constructor, in PRFA.tp6c]

B

bad [inductive, in PRFA.live_coding3]
bad [inductive, in PRFA.tp3c]
bad_rational2 [record, in PRFA.live_coding4]
bad_rational1 [record, in PRFA.live_coding4]
bad_not_bad [lemma, in PRFA.tp3c]
bar [definition, in PRFA.live_coding3]
bar [definition, in PRFA.tp6c]
baz [definition, in PRFA.live_coding3]
below [definition, in PRFA.tp3c]
bintree [inductive, in PRFA.live_coding5]
bintree [inductive, in PRFA.tp5c]
bintree_sind [definition, in PRFA.live_coding5]
bintree_rec [definition, in PRFA.live_coding5]
bintree_ind [definition, in PRFA.live_coding5]
bintree_rect [definition, in PRFA.live_coding5]
bintree_sind [definition, in PRFA.tp5c]
bintree_rec [definition, in PRFA.tp5c]
bintree_ind [definition, in PRFA.tp5c]
bintree_rect [definition, in PRFA.tp5c]
box [constructor, in PRFA.live_coding5]
Box [inductive, in PRFA.live_coding5]
Box_sind [definition, in PRFA.live_coding5]
Box_rec [definition, in PRFA.live_coding5]
Box_ind [definition, in PRFA.live_coding5]
Box_rect [definition, in PRFA.live_coding5]
brec [definition, in PRFA.tp3c]
brec' [definition, in PRFA.tp3c]
bt_to_tree [definition, in PRFA.live_coding5]
bt_map_id [lemma, in PRFA.live_coding5]
bt_map [definition, in PRFA.live_coding5]
bt_node [constructor, in PRFA.live_coding5]
bt_leaf [constructor, in PRFA.live_coding5]
bt_to_tree [definition, in PRFA.tp5c]
bt_map_id [lemma, in PRFA.tp5c]
bt_map [definition, in PRFA.tp5c]
bt_node [constructor, in PRFA.tp5c]
bt_leaf [constructor, in PRFA.tp5c]

C

C [constructor, in PRFA.live_coding3]
C [constructor, in PRFA.tp3c]
calc_12_3 [lemma, in PRFA.tp1c]
calc_12_3 [lemma, in PRFA.live_coding1]
cancel_to_of [lemma, in PRFA.tp2c]
cancel_of_to [lemma, in PRFA.tp2c]
Cantor_bool' [lemma, in PRFA.tp7c]
car [definition, in PRFA.tp2c]
car [definition, in PRFA.live_coding2]
car_cur [lemma, in PRFA.tp2c]
car_cur [lemma, in PRFA.live_coding2]
car' [definition, in PRFA.tp2c]
car'' [definition, in PRFA.tp2c]
classical_impl [lemma, in PRFA.tp1c]
classical_or_contra_r [lemma, in PRFA.tp1c]
cons [constructor, in PRFA.review6]
ConstructiveIndefiniteGroundDescription_Acc.R [variable, in PRFA.tp5c]
ConstructiveIndefiniteGroundDescription_Acc.P_decidable [variable, in PRFA.tp5c]
ConstructiveIndefiniteGroundDescription_Acc.P [variable, in PRFA.tp5c]
ConstructiveIndefiniteGroundDescription_Acc [section, in PRFA.tp5c]
constructive_indefinite_ground_description_nat_Acc [lemma, in PRFA.tp5c]
contrad [lemma, in PRFA.tp1c]
contrapositive [lemma, in PRFA.tp1c]
count [definition, in PRFA.live_coding3]
count [definition, in PRFA.tp3c]
count_list [definition, in PRFA.live_coding3]
count_list [definition, in PRFA.tp3c]
cur [definition, in PRFA.tp2c]
cur [definition, in PRFA.live_coding2]
cur_car [lemma, in PRFA.tp2c]
cur_car [lemma, in PRFA.live_coding2]

D

debug_derive_updates [definition, in PRFA.tp6c]
debug_def_list [definition, in PRFA.tp6c]
define_nat.add_sub_alt [lemma, in PRFA.tp2c]
define_nat.sub_O [lemma, in PRFA.tp2c]
define_nat.add_sub [lemma, in PRFA.tp2c]
_ - _ [notation, in PRFA.tp2c]
_ + _ [notation, in PRFA.tp2c]
define_nat.add_S [lemma, in PRFA.tp2c]
define_nat.add_0 [lemma, in PRFA.tp2c]
define_nat.sub [definition, in PRFA.tp2c]
define_nat.add [definition, in PRFA.tp2c]
define_nat.nat_sind [definition, in PRFA.tp2c]
define_nat.nat_rec [definition, in PRFA.tp2c]
define_nat.nat_ind [definition, in PRFA.tp2c]
define_nat.nat_rect [definition, in PRFA.tp2c]
define_nat.S [constructor, in PRFA.tp2c]
define_nat.O [constructor, in PRFA.tp2c]
define_nat.nat [inductive, in PRFA.tp2c]
define_nat [module, in PRFA.tp2c]
define_sigma.pair2 [definition, in PRFA.live_coding2]
define_sigma.pair1 [definition, in PRFA.live_coding2]
define_sigma.T [definition, in PRFA.live_coding2]
define_sigma.sigT_sind [definition, in PRFA.live_coding2]
define_sigma.sigT_rec [definition, in PRFA.live_coding2]
define_sigma.sigT_ind [definition, in PRFA.live_coding2]
define_sigma.sigT_rect [definition, in PRFA.live_coding2]
define_sigma.existT [constructor, in PRFA.live_coding2]
define_sigma.sigT [inductive, in PRFA.live_coding2]
define_sigma [module, in PRFA.live_coding2]
define_list.list_sind [definition, in PRFA.live_coding2]
define_list.list_rec [definition, in PRFA.live_coding2]
define_list.list_ind [definition, in PRFA.live_coding2]
define_list.list_rect [definition, in PRFA.live_coding2]
define_list.cons [constructor, in PRFA.live_coding2]
define_list.nil [constructor, in PRFA.live_coding2]
define_list.list [inductive, in PRFA.live_coding2]
define_list [module, in PRFA.live_coding2]
define_prod.snd [definition, in PRFA.live_coding2]
define_prod.fst [definition, in PRFA.live_coding2]
define_prod.pair' [definition, in PRFA.live_coding2]
define_prod.prod_sind [definition, in PRFA.live_coding2]
define_prod.prod_rec [definition, in PRFA.live_coding2]
define_prod.prod_ind [definition, in PRFA.live_coding2]
define_prod.prod_rect [definition, in PRFA.live_coding2]
define_prod.pair [constructor, in PRFA.live_coding2]
define_prod.prod [inductive, in PRFA.live_coding2]
define_prod [module, in PRFA.live_coding2]
define_bool.true_false [lemma, in PRFA.live_coding2]
define_bool.bool_sind [definition, in PRFA.live_coding2]
define_bool.bool_rec [definition, in PRFA.live_coding2]
define_bool.bool_ind [definition, in PRFA.live_coding2]
define_bool.bool_rect [definition, in PRFA.live_coding2]
define_bool.false [constructor, in PRFA.live_coding2]
define_bool.true [constructor, in PRFA.live_coding2]
define_bool.bool [inductive, in PRFA.live_coding2]
define_bool [module, in PRFA.live_coding2]
define_nat.eq_nat_spec [lemma, in PRFA.live_coding2]
define_nat.eq_nat_spec [lemma, in PRFA.live_coding2]
define_nat.eq_nat [definition, in PRFA.live_coding2]
define_nat.S_inj_4 [lemma, in PRFA.live_coding2]
define_nat.S_inj_3 [lemma, in PRFA.live_coding2]
define_nat.S_inj_2 [lemma, in PRFA.live_coding2]
define_nat.S_inj [lemma, in PRFA.live_coding2]
define_nat.pred [definition, in PRFA.live_coding2]
define_nat.S_0' [lemma, in PRFA.live_coding2]
define_nat.S_O [lemma, in PRFA.live_coding2]
define_nat.is_zero [definition, in PRFA.live_coding2]
define_nat.is_zerob [definition, in PRFA.live_coding2]
define_nat.add_sub [lemma, in PRFA.live_coding2]
_ - _ [notation, in PRFA.live_coding2]
define_nat.sub [definition, in PRFA.live_coding2]
define_nat.add_S [lemma, in PRFA.live_coding2]
_ + _ [notation, in PRFA.live_coding2]
define_nat.add_0 [lemma, in PRFA.live_coding2]
define_nat.add [definition, in PRFA.live_coding2]
define_nat.variant2.nat_sind [definition, in PRFA.live_coding2]
define_nat.variant2.nat_rec [definition, in PRFA.live_coding2]
define_nat.variant2.nat_ind [definition, in PRFA.live_coding2]
define_nat.variant2.nat_rect [definition, in PRFA.live_coding2]
define_nat.variant2.S [constructor, in PRFA.live_coding2]
define_nat.variant2.O [constructor, in PRFA.live_coding2]
define_nat.variant2.nat [inductive, in PRFA.live_coding2]
define_nat.variant2 [module, in PRFA.live_coding2]
define_nat.variant1.nat_sind [definition, in PRFA.live_coding2]
define_nat.variant1.nat_rec [definition, in PRFA.live_coding2]
define_nat.variant1.nat_ind [definition, in PRFA.live_coding2]
define_nat.variant1.nat_rect [definition, in PRFA.live_coding2]
define_nat.variant1.S [constructor, in PRFA.live_coding2]
define_nat.variant1.O [constructor, in PRFA.live_coding2]
define_nat.variant1.nat [inductive, in PRFA.live_coding2]
define_nat.variant1 [module, in PRFA.live_coding2]
define_nat.nat_sind [definition, in PRFA.live_coding2]
define_nat.nat_rec [definition, in PRFA.live_coding2]
define_nat.nat_ind [definition, in PRFA.live_coding2]
define_nat.nat_rect [definition, in PRFA.live_coding2]
define_nat.S [constructor, in PRFA.live_coding2]
define_nat.O [constructor, in PRFA.live_coding2]
define_nat.nat [inductive, in PRFA.live_coding2]
define_nat [module, in PRFA.live_coding2]
def_list [definition, in PRFA.tp6c]
Demo [section, in PRFA.live_coding3]
Demo.X [variable, in PRFA.live_coding3]
Demo.Y [variable, in PRFA.live_coding3]
Demo.Z [variable, in PRFA.live_coding3]
denominator [projection, in PRFA.live_coding4]
denominator' [projection, in PRFA.live_coding4]
denominator'' [projection, in PRFA.live_coding4]
den_not_zero [projection, in PRFA.live_coding4]
dependent [definition, in PRFA.live_coding3]
dep_f_equal [lemma, in PRFA.live_coding7]
dep_f_equal [lemma, in PRFA.live_coding7]
dep_f_equal [lemma, in PRFA.tp7c]
derive_updates [definition, in PRFA.tp6c]
de_morgan [lemma, in PRFA.tp1c]
distr [lemma, in PRFA.tp1c]
div2 [definition, in PRFA.tp7c]
div2_double [lemma, in PRFA.tp7c]
DNE [axiom, in PRFA.live_coding4]
DNS [definition, in PRFA.tp1c]
dns_lem [lemma, in PRFA.tp1c]
dn_functorial [lemma, in PRFA.tp1c]
double [definition, in PRFA.live_coding1]
double_S [definition, in PRFA.live_coding6]
double_eq [lemma, in PRFA.tp1c]
double_div2 [lemma, in PRFA.tp7c]
double_eq2 [lemma, in PRFA.live_coding1]
double_eq [lemma, in PRFA.live_coding1]

E

elim_or [definition, in PRFA.live_coding3]
elim_and [definition, in PRFA.live_coding3]
elim_False [definition, in PRFA.live_coding3]
empty_tree [definition, in PRFA.live_coding3]
env [definition, in PRFA.tp8c]
env [definition, in PRFA.live_coding8]
epsilon_LEM [lemma, in PRFA.tp5c]
Eq [record, in PRFA.live_coding4]
Eq [record, in PRFA.tp4c]
eqb [projection, in PRFA.live_coding4]
eqb [projection, in PRFA.tp4c]
eqb_iff [projection, in PRFA.live_coding4]
eqb_iff [projection, in PRFA.tp4c]
equal [definition, in PRFA.live_coding8]
equiv [record, in PRFA.tp8c]
equivalence [definition, in PRFA.tp7c]
equivalence_eq_eq [lemma, in PRFA.tp7c]
equivalence_neg_bool [definition, in PRFA.tp7c]
equivalence_nat_even [lemma, in PRFA.tp7c]
equivalence_trans [lemma, in PRFA.tp7c]
equivalence_sym [lemma, in PRFA.tp7c]
equivalence_refl [lemma, in PRFA.tp7c]
equiv_ilist [lemma, in PRFA.tp8c]
eq_nat_spec [lemma, in PRFA.tp2c]
eq_nat [definition, in PRFA.tp2c]
eq_dec_term [definition, in PRFA.tp8c]
eq_dec [lemma, in PRFA.tp8c]
eq_nat_eq [lemma, in PRFA.tp8c]
eq_nat [definition, in PRFA.tp8c]
Eq_nat [instance, in PRFA.live_coding4]
eq_nat_spec [lemma, in PRFA.review2]
eq_nat [definition, in PRFA.review2]
Eq_nat [instance, in PRFA.tp4c]
eq_dec [lemma, in PRFA.live_coding7]
eq_eq_nat [lemma, in PRFA.live_coding7]
eq_nat_eq [lemma, in PRFA.live_coding7]
eq_nat [definition, in PRFA.live_coding7]
eq_trans' [definition, in PRFA.live_coding7]
eq_trans' [definition, in PRFA.live_coding7]
eq_sym' [definition, in PRFA.live_coding7]
eq_trans [definition, in PRFA.live_coding7]
eq_sym [definition, in PRFA.live_coding7]
eq_dec_term [definition, in PRFA.tp7c]
eq_nat_false [lemma, in PRFA.tp7c]
eq_dec [lemma, in PRFA.tp7c]
eq_eq_nat [lemma, in PRFA.tp7c]
eq_nat_eq [lemma, in PRFA.tp7c]
eq_nat [definition, in PRFA.tp7c]
eq_from_ts [lemma, in PRFA.tp7c]
eq_to_ts [lemma, in PRFA.tp7c]
eq_ts_sind [definition, in PRFA.tp7c]
eq_ts_ind [definition, in PRFA.tp7c]
eq_ts [inductive, in PRFA.tp7c]
eq_trans' [definition, in PRFA.tp7c]
eq_sym' [definition, in PRFA.tp7c]
eq_trans [definition, in PRFA.tp7c]
eq_sym [definition, in PRFA.tp7c]
eval [definition, in PRFA.tp8c]
even [inductive, in PRFA.live_coding2]
even [inductive, in PRFA.live_coding3]
even [inductive, in PRFA.review3]
even [inductive, in PRFA.live_coding7]
even [inductive, in PRFA.tp7c]
evenb [definition, in PRFA.live_coding2]
evenb_to_even [lemma, in PRFA.live_coding2]
evenb_to_even [lemma, in PRFA.live_coding2]
evenO [constructor, in PRFA.tp2c]
evenO [constructor, in PRFA.live_coding2]
evenO [constructor, in PRFA.live_coding3]
evenO [constructor, in PRFA.review3]
evenS [constructor, in PRFA.tp2c]
evenS [constructor, in PRFA.live_coding2]
evenS [constructor, in PRFA.live_coding3]
evenS [constructor, in PRFA.review3]
evenS [constructor, in PRFA.live_coding7]
evenS [constructor, in PRFA.tp7c]
evenSS_inv_alt [definition, in PRFA.live_coding7]
evenSS_inv [lemma, in PRFA.live_coding7]
evenSS_inv_alt [definition, in PRFA.tp7c]
evenSS_inv [lemma, in PRFA.tp7c]
even_to_evenb [lemma, in PRFA.live_coding2]
even_sind [definition, in PRFA.live_coding2]
even_ind [definition, in PRFA.live_coding2]
even_plus_four_term [definition, in PRFA.live_coding3]
even_plus_four_refine [lemma, in PRFA.live_coding3]
even_plus_four [lemma, in PRFA.live_coding3]
even_four' [definition, in PRFA.live_coding3]
even_four [lemma, in PRFA.live_coding3]
even_sind [definition, in PRFA.live_coding3]
even_ind [definition, in PRFA.live_coding3]
even_sind [definition, in PRFA.review3]
even_ind [definition, in PRFA.review3]
even_sind [definition, in PRFA.live_coding7]
even_ind [definition, in PRFA.live_coding7]
even_double [lemma, in PRFA.tp7c]
even_and_S_False [lemma, in PRFA.tp7c]
even_sind [definition, in PRFA.tp7c]
even_ind [definition, in PRFA.tp7c]
even0 [constructor, in PRFA.live_coding7]
even0 [constructor, in PRFA.tp7c]
even1 [definition, in PRFA.tp2c]
even1_to_even2 [lemma, in PRFA.tp2c]
even2 [definition, in PRFA.tp2c]
even2 [definition, in PRFA.review2]
even2_iff_even3 [lemma, in PRFA.tp2c]
even2_iff_even3 [lemma, in PRFA.review2]
even3 [definition, in PRFA.tp2c]
even3 [definition, in PRFA.review2]
even3_to_even4 [lemma, in PRFA.tp2c]
even4 [inductive, in PRFA.tp2c]
even4_to_even1 [lemma, in PRFA.tp2c]
even4_sind [definition, in PRFA.tp2c]
even4_ind [definition, in PRFA.tp2c]
exercise_chain [lemma, in PRFA.live_coding5]
exercise_loop [lemma, in PRFA.live_coding5]
exfalso' [definition, in PRFA.live_coding5]
exfalso' [definition, in PRFA.tp5c]
exists_unique [definition, in PRFA.tp7c]
exp [definition, in PRFA.tp2c]
exp_from_nat [lemma, in PRFA.tp2c]
extend [definition, in PRFA.tp8c]
extend [definition, in PRFA.live_coding8]
ex1 [definition, in PRFA.tp3c]
ex2 [definition, in PRFA.tp3c]
ex3 [definition, in PRFA.tp3c]
ex3_alt [definition, in PRFA.tp3c]
ex4 [definition, in PRFA.tp3c]

F

f [definition, in PRFA.live_coding3]
f [definition, in PRFA.tp3c]
fact_equiv [lemma, in PRFA.tp2c]
fact_iter [definition, in PRFA.tp2c]
fact_iter_f [definition, in PRFA.tp2c]
fact_fix [definition, in PRFA.tp2c]
falsefalse [lemma, in PRFA.live_coding1]
False_forall [lemma, in PRFA.tp1c]
fast_rev_eq_alt [lemma, in PRFA.tp2c]
fast_rev_eq [lemma, in PRFA.tp2c]
fast_rev [definition, in PRFA.tp2c]
fast_rev_eq_alt [lemma, in PRFA.live_coding2]
fast_rev_eq [lemma, in PRFA.live_coding2]
fast_rev_eq [lemma, in PRFA.live_coding2]
fast_rev [definition, in PRFA.live_coding2]
FE_test_eq_stable [lemma, in PRFA.tp7c]
FE_stable_HF [lemma, in PRFA.tp7c]
fib [definition, in PRFA.tp5c]
fib [definition, in PRFA.tp3c]
Fib_Iter.fib_eq3 [lemma, in PRFA.tp2c]
Fib_Iter.fib_eq1 [lemma, in PRFA.tp2c]
Fib_Iter.fib_eq0 [lemma, in PRFA.tp2c]
Fib_Iter.fib [definition, in PRFA.tp2c]
Fib_Iter.sigma [definition, in PRFA.tp2c]
Fib_Iter [module, in PRFA.tp2c]
fib_superlinear [lemma, in PRFA.tp5c]
fib_brec [definition, in PRFA.tp3c]
fib_natrec [definition, in PRFA.tp3c]
filter [definition, in PRFA.live_coding8]
filter_true [lemma, in PRFA.live_coding8]
fin [inductive, in PRFA.tp8c]
fin [inductive, in PRFA.live_coding8]
finS [constructor, in PRFA.tp8c]
finS [constructor, in PRFA.live_coding8]
fin_sind [definition, in PRFA.tp8c]
fin_rec [definition, in PRFA.tp8c]
fin_ind [definition, in PRFA.tp8c]
fin_rect [definition, in PRFA.tp8c]
fin_sind [definition, in PRFA.live_coding8]
fin_rec [definition, in PRFA.live_coding8]
fin_ind [definition, in PRFA.live_coding8]
fin_rect [definition, in PRFA.live_coding8]
fin0 [constructor, in PRFA.tp8c]
fin0 [constructor, in PRFA.live_coding8]
fold_def [definition, in PRFA.MetaCoqPrelude]
fold_branches [definition, in PRFA.MetaCoqPrelude]
fold_branch [definition, in PRFA.MetaCoqPrelude]
fold_predicate [definition, in PRFA.MetaCoqPrelude]
fold_handler [definition, in PRFA.MetaCoqPrelude]
fold_muladd_alt [definition, in PRFA.tp6c]
fold_muladd [definition, in PRFA.tp6c]
foo [definition, in PRFA.live_coding3]
foo [definition, in PRFA.live_coding4]
foo [definition, in PRFA.tp4c]
foo [lemma, in PRFA.tp6c]
foo_env [definition, in PRFA.tp6c]
forall_or [lemma, in PRFA.tp1c]
forall_False' [lemma, in PRFA.tp1c]
forall_False [lemma, in PRFA.tp1c]
Forall_wpermut [lemma, in PRFA.tp5c]
Forall_set_eq [lemma, in PRFA.tp4c]
Forall_In [lemma, in PRFA.tp4c]
from_nat [definition, in PRFA.tp2c]
from_prop_bool_neg_PI [lemma, in PRFA.tp5c]
from_mind [definition, in PRFA.tp6c]
from_ctor [definition, in PRFA.tp6c]
from_arg [definition, in PRFA.tp6c]
from_to_tree_alt [lemma, in PRFA.tp3c]
from_to_tree_list [definition, in PRFA.tp3c]
from_to_tree [definition, in PRFA.tp3c]
from_tree_list [definition, in PRFA.tp3c]
from_tree [definition, in PRFA.tp3c]
fst' [projection, in PRFA.review4]
fst' [projection, in PRFA.live_coding4]
fst' [projection, in PRFA.tp4c]
FunctionExtensionality [definition, in PRFA.tp7c]
FunExt [definition, in PRFA.tp5c]
funext [axiom, in PRFA.live_coding7]
FunExt [definition, in PRFA.live_coding7]
funext [axiom, in PRFA.tp6c]
funext [axiom, in PRFA.tp7c]
FunExt [definition, in PRFA.tp7c]
fun_choice_LEM [lemma, in PRFA.tp5c]
fun_choice [definition, in PRFA.tp5c]
f_equal'' [definition, in PRFA.live_coding7]
f_equal' [lemma, in PRFA.live_coding7]
f_equal_term' [definition, in PRFA.tp7c]
f_equal_term [definition, in PRFA.tp7c]
f_equal' [lemma, in PRFA.tp7c]
f_equal [definition, in PRFA.review7]

G

G [inductive, in PRFA.live_coding5]
get_kername [definition, in PRFA.MetaCoqPrelude]
get_inductive' [definition, in PRFA.tp6c]
get_name [definition, in PRFA.tp6c]
get_inductive [definition, in PRFA.tp6c]
GI [constructor, in PRFA.live_coding5]
good_tree_ind [lemma, in PRFA.live_coding5]
good_tree_ind' [lemma, in PRFA.live_coding5]
good_tree_ind [lemma, in PRFA.tp5c]
Group [record, in PRFA.tp4c]
group [record, in PRFA.tp4c]
Group_Z [instance, in PRFA.tp4c]
group_inverse_unique [lemma, in PRFA.tp4c]
group_neutral_unique [lemma, in PRFA.tp4c]
group_inv [projection, in PRFA.tp4c]
group_assoc [projection, in PRFA.tp4c]
group_right_neutral [projection, in PRFA.tp4c]
group_left_neutral [projection, in PRFA.tp4c]
group_fact [lemma, in PRFA.tp4c]
G_zero [lemma, in PRFA.live_coding5]
G_sig [lemma, in PRFA.live_coding5]
G_sind [definition, in PRFA.live_coding5]
G_rec [definition, in PRFA.live_coding5]
G_ind [definition, in PRFA.live_coding5]
G_rect [definition, in PRFA.live_coding5]
g_inv [projection, in PRFA.tp4c]
g_mon [projection, in PRFA.tp4c]

H

half [definition, in PRFA.live_coding4]
half' [definition, in PRFA.live_coding4]
has_body [definition, in PRFA.tp6c]
hd [definition, in PRFA.tp8c]
head [definition, in PRFA.tp8c]
head [definition, in PRFA.live_coding8]
head' [definition, in PRFA.live_coding8]
Hedberg [lemma, in PRFA.tp7c]
Hedberg' [lemma, in PRFA.tp7c]
Heq [inductive, in PRFA.tp7c]
heq [definition, in PRFA.tp7c]
Heq_heq [lemma, in PRFA.tp7c]
heq_Heq [lemma, in PRFA.tp7c]
Heq_sind [definition, in PRFA.tp7c]
Heq_rec [definition, in PRFA.tp7c]
Heq_ind [definition, in PRFA.tp7c]
Heq_rect [definition, in PRFA.tp7c]
heq_refl [constructor, in PRFA.tp7c]
HF [definition, in PRFA.tp7c]
Hierarchy [module, in PRFA.tp3c]
Hierarchy.embeds [definition, in PRFA.tp3c]
Hierarchy.embeds_refl [lemma, in PRFA.tp3c]
Hierarchy.hier [lemma, in PRFA.tp3c]
Hierarchy.hierarchy [lemma, in PRFA.tp3c]
Hierarchy.inconsistent [lemma, in PRFA.tp3c]
Hierarchy.sub [definition, in PRFA.tp3c]
Hierarchy.sub_irrefl [lemma, in PRFA.tp3c]
Hierarchy.T [constructor, in PRFA.tp3c]
Hierarchy.tree [inductive, in PRFA.tp3c]
Hierarchy.tree_sind [definition, in PRFA.tp3c]
Hierarchy.tree_rec [definition, in PRFA.tp3c]
Hierarchy.tree_ind [definition, in PRFA.tp3c]
Hierarchy.tree_rect [definition, in PRFA.tp3c]
Hierarchy.Tyi [definition, in PRFA.tp3c]
Hilbert [section, in PRFA.tp5c]

I

iAnd [definition, in PRFA.review3]
iAnd [definition, in PRFA.tp3c]
iAnd_and [lemma, in PRFA.review3]
iAnd_iff [lemma, in PRFA.tp3c]
identity [definition, in PRFA.tp6c]
idNat [definition, in PRFA.live_coding6]
idnat [definition, in PRFA.tp3c]
idren [definition, in PRFA.tp8c]
idval [definition, in PRFA.tp8c]
iEx [definition, in PRFA.review3]
iEx [definition, in PRFA.tp3c]
iEx_ex [lemma, in PRFA.review3]
iEx_iff [lemma, in PRFA.tp3c]
iFalse [definition, in PRFA.review3]
iFalse [definition, in PRFA.tp3c]
iFalse_iff [lemma, in PRFA.tp3c]
ilist [definition, in PRFA.tp8c]
ilist_eq [lemma, in PRFA.tp8c]
imp_trans [lemma, in PRFA.tp1c]
In [definition, in PRFA.tp2c]
incl [constructor, in PRFA.tp2c]
incl [constructor, in PRFA.live_coding2]
inhabited_is_True [lemma, in PRFA.live_coding7]
inhabited_is_True [lemma, in PRFA.tp7c]
instantiate_axiom [definition, in PRFA.tp6c]
interp [definition, in PRFA.live_coding8]
interp_type [definition, in PRFA.live_coding8]
in_cons [lemma, in PRFA.review4]
in_add_left [lemma, in PRFA.review4]
in_add_right [lemma, in PRFA.review4]
In_iff [lemma, in PRFA.tp2c]
In_i_sind [definition, in PRFA.tp2c]
In_i_ind [definition, in PRFA.tp2c]
in_tl [constructor, in PRFA.tp2c]
in_hd [constructor, in PRFA.tp2c]
In_i [inductive, in PRFA.tp2c]
In_hd' [lemma, in PRFA.live_coding4]
In_4 [lemma, in PRFA.live_coding4]
In_tl [lemma, in PRFA.live_coding4]
In_hd [lemma, in PRFA.live_coding4]
In_app_inv [lemma, in PRFA.tp4c]
In_hd_eq [lemma, in PRFA.tp4c]
In_app_r [lemma, in PRFA.tp4c]
In_app_l [lemma, in PRFA.tp4c]
In_hd' [lemma, in PRFA.tp4c]
In_4 [lemma, in PRFA.tp4c]
In_tl [lemma, in PRFA.tp4c]
In_hd [lemma, in PRFA.tp4c]
iOr [definition, in PRFA.tp3c]
iOr_iff [lemma, in PRFA.tp3c]
isEquiv [definition, in PRFA.tp7c]
isnil [definition, in PRFA.tp8c]
iter [definition, in PRFA.tp2c]
iter [definition, in PRFA.live_coding2]
iter_shift [lemma, in PRFA.tp2c]
iter_pow [lemma, in PRFA.tp2c]
iter_mul [lemma, in PRFA.live_coding2]
iter_add [lemma, in PRFA.live_coding2]
iTrue [definition, in PRFA.tp3c]
iTrue_iff [lemma, in PRFA.tp3c]

J

J [definition, in PRFA.tp7c]

K

K [axiom, in PRFA.tp8c]
K [definition, in PRFA.tp7c]
K_UIP [definition, in PRFA.tp7c]

L

lam_inv [lemma, in PRFA.tp8c]
Lawvere [lemma, in PRFA.tp7c]
le [inductive, in PRFA.live_coding2]
least [definition, in PRFA.live_coding5]
leb [definition, in PRFA.tp2c]
leb_spec_alt [lemma, in PRFA.tp2c]
leb_spec [lemma, in PRFA.tp2c]
Leibniz [module, in PRFA.live_coding7]
Leibniz [module, in PRFA.tp7c]
leibniz_sym [definition, in PRFA.review7]
Leibniz.EqDef [module, in PRFA.live_coding7]
Leibniz.EqDef.eq [inductive, in PRFA.live_coding7]
Leibniz.EqDef.eq_to_Leibniz [lemma, in PRFA.live_coding7]
Leibniz.EqDef.eq_sind [definition, in PRFA.live_coding7]
Leibniz.EqDef.eq_rec [definition, in PRFA.live_coding7]
Leibniz.EqDef.eq_ind [definition, in PRFA.live_coding7]
Leibniz.EqDef.eq_rect [definition, in PRFA.live_coding7]
Leibniz.EqDef.eq_refl [constructor, in PRFA.live_coding7]
Leibniz.EqDef.Leibniz_to_eq [lemma, in PRFA.live_coding7]
Leibniz.eq_to_leib [definition, in PRFA.tp7c]
Leibniz.f_equal [lemma, in PRFA.live_coding7]
Leibniz.f_equal [definition, in PRFA.tp7c]
Leibniz.leib_eq [definition, in PRFA.live_coding7]
Leibniz.leib_to_eq [definition, in PRFA.tp7c]
Leibniz.leib_eq [definition, in PRFA.tp7c]
Leibniz.nat_discr [lemma, in PRFA.live_coding7]
Leibniz.nat_discr [lemma, in PRFA.tp7c]
Leibniz.n_plus_0 [lemma, in PRFA.live_coding7]
Leibniz.n_plus_0 [lemma, in PRFA.tp7c]
Leibniz.refl [definition, in PRFA.live_coding7]
Leibniz.refl [definition, in PRFA.tp7c]
Leibniz.sym [definition, in PRFA.live_coding7]
Leibniz.sym [definition, in PRFA.tp7c]
Leibniz.trans [lemma, in PRFA.live_coding7]
Leibniz.trans [definition, in PRFA.tp7c]
_ == _ [notation, in PRFA.live_coding7]
_ == _ [notation, in PRFA.tp7c]
Leibniz2 [module, in PRFA.tp7c]
Leibniz2.all_equal_incl [lemma, in PRFA.tp7c]
Leibniz2.all_equal_implies_J [lemma, in PRFA.tp7c]
Leibniz2.all_equal [definition, in PRFA.tp7c]
Leibniz2.incl [definition, in PRFA.tp7c]
Leibniz2.J_implies_all_equal [lemma, in PRFA.tp7c]
Leibniz2.J_prop [definition, in PRFA.tp7c]
Leibniz2.leib_eq [definition, in PRFA.tp7c]
Leibniz2.refl [definition, in PRFA.tp7c]
Leibniz2.singleton [definition, in PRFA.tp7c]
Leibniz2.sym [definition, in PRFA.tp7c]
Leibniz2.trans [lemma, in PRFA.tp7c]
_ == _ [notation, in PRFA.tp7c]
LEM [definition, in PRFA.tp1c]
LEM [axiom, in PRFA.tp6c]
lem_dns [lemma, in PRFA.tp1c]
lem_pl [lemma, in PRFA.tp1c]
length_to_list [lemma, in PRFA.tp8c]
leO [constructor, in PRFA.live_coding2]
leO' [constructor, in PRFA.tp2c]
leS [constructor, in PRFA.live_coding2]
leS' [constructor, in PRFA.tp2c]
le_equiv [lemma, in PRFA.tp2c]
le_n_S [lemma, in PRFA.tp2c]
le_0_n [lemma, in PRFA.tp2c]
le_rtclos [lemma, in PRFA.live_coding2]
le_trans [lemma, in PRFA.live_coding2]
le_iff [lemma, in PRFA.live_coding2]
le_sind [definition, in PRFA.live_coding2]
le_ind [definition, in PRFA.live_coding2]
le_n_S [lemma, in PRFA.review3]
le_dec [definition, in PRFA.tp5c]
le_alt [definition, in PRFA.tp5c]
le_intro [constructor, in PRFA.tp5c]
le' [inductive, in PRFA.tp2c]
le' [inductive, in PRFA.tp5c]
le'_n_S [lemma, in PRFA.tp2c]
le'_refl [lemma, in PRFA.tp2c]
le'_sind [definition, in PRFA.tp2c]
le'_ind [definition, in PRFA.tp2c]
le'_sind [definition, in PRFA.tp5c]
le'_rec [definition, in PRFA.tp5c]
le'_ind [definition, in PRFA.tp5c]
le'_rect [definition, in PRFA.tp5c]
linear_search [lemma, in PRFA.live_coding5]
list [inductive, in PRFA.review6]
list_sind [definition, in PRFA.review6]
list_rec [definition, in PRFA.review6]
list_ind [definition, in PRFA.review6]
list_rect [definition, in PRFA.review6]
list_rect [definition, in PRFA.live_coding3]
list_seq_eq_app [lemma, in PRFA.tp4c]
list_set_eq_trans [instance, in PRFA.tp4c]
list_set_eq_sym [instance, in PRFA.tp4c]
list_set_eq_refl [instance, in PRFA.tp4c]
list_set_eq [definition, in PRFA.tp4c]
list_fact [lemma, in PRFA.tp4c]
list_monoid [definition, in PRFA.tp4c]
Live [section, in PRFA.live_coding1]
live_coding6 [library]
live_coding5 [library]
live_coding8 [library]
live_coding2 [library]
live_coding1 [library]
live_coding4 [library]
live_coding3 [library]
live_coding7 [library]
lt [inductive, in PRFA.review3]
lt [inductive, in PRFA.tp3c]
lt_plus_4' [definition, in PRFA.review3]
lt_plus_4 [definition, in PRFA.review3]
lt_sind [definition, in PRFA.review3]
lt_ind [definition, in PRFA.review3]
lt_S [constructor, in PRFA.review3]
lt_B [constructor, in PRFA.review3]
lt_plus_4' [definition, in PRFA.tp3c]
lt_plus_4 [lemma, in PRFA.tp3c]
lt_sind [definition, in PRFA.tp3c]
lt_ind [definition, in PRFA.tp3c]
lt_S [constructor, in PRFA.tp3c]
lt_B [constructor, in PRFA.tp3c]
l_to_l [projection, in PRFA.tp8c]
l_to_r [projection, in PRFA.tp8c]

M

map [definition, in PRFA.live_coding7]
map [definition, in PRFA.tp7c]
map_id' [lemma, in PRFA.live_coding7]
map_id' [lemma, in PRFA.live_coding7]
map_id [lemma, in PRFA.live_coding7]
map_id' [lemma, in PRFA.tp7c]
map_id' [lemma, in PRFA.tp7c]
map_id [lemma, in PRFA.tp7c]
memb [definition, in PRFA.live_coding4]
memb [definition, in PRFA.tp4c]
memb_spec [lemma, in PRFA.tp4c]
merge [definition, in PRFA.live_coding8]
merge [definition, in PRFA.live_coding8]
merge [definition, in PRFA.tp5c]
Merge [section, in PRFA.tp5c]
merge [definition, in PRFA.tp5c]
merge_In [lemma, in PRFA.live_coding8]
merge_spec [lemma, in PRFA.tp5c]
merge_acc [lemma, in PRFA.tp5c]
Merge.m [variable, in PRFA.tp5c]
Merge.R [variable, in PRFA.tp5c]
Merge.T [variable, in PRFA.tp5c]
MetaCoqPrelude [library]
min [definition, in PRFA.tp1c]
min_comm [lemma, in PRFA.tp1c]
mkargs [definition, in PRFA.tp6c]
mkargs_aux [definition, in PRFA.tp6c]
mkr [definition, in PRFA.tp6c]
Monoid [record, in PRFA.live_coding4]
monoid [record, in PRFA.live_coding4]
Monoid [record, in PRFA.tp4c]
monoid [record, in PRFA.tp4c]
MonoidList [instance, in PRFA.tp4c]
MonoidNat [instance, in PRFA.live_coding4]
MonoidNat [instance, in PRFA.tp4c]
MonoidProd [instance, in PRFA.live_coding4]
MonoidProd [instance, in PRFA.tp4c]
monoid_fact [lemma, in PRFA.live_coding4]
Monoid_Group [instance, in PRFA.tp4c]
monoid_fact [lemma, in PRFA.tp4c]
mon_assoc [projection, in PRFA.live_coding4]
mon_right_neutral [projection, in PRFA.live_coding4]
mon_left_neutral [projection, in PRFA.live_coding4]
mon_assoc [projection, in PRFA.tp4c]
mon_right_neutral [projection, in PRFA.tp4c]
mon_left_neutral [projection, in PRFA.tp4c]
more_deps [definition, in PRFA.tp6c]
mpow [definition, in PRFA.live_coding6]
mpow' [definition, in PRFA.live_coding6]
mul [definition, in PRFA.tp2c]
muladd [definition, in PRFA.tp6c]
muladd_handler [definition, in PRFA.tp6c]
mult_distr_lia [lemma, in PRFA.tp1c]
mult_distr [lemma, in PRFA.tp1c]
mult_comm [lemma, in PRFA.tp1c]
mult_S [lemma, in PRFA.tp1c]
mult_0 [lemma, in PRFA.tp1c]
mult4 [inductive, in PRFA.live_coding6]
mult4_sind [definition, in PRFA.live_coding6]
mult4_ind [definition, in PRFA.live_coding6]
mult4_plus [constructor, in PRFA.live_coding6]
mult4_0 [constructor, in PRFA.live_coding6]
mul_from_nat [lemma, in PRFA.tp2c]
mystery [axiom, in PRFA.tp6c]
m_assoc [projection, in PRFA.live_coding4]
m_r_ne [projection, in PRFA.live_coding4]
m_l_ne [projection, in PRFA.live_coding4]
m_op [projection, in PRFA.live_coding4]
m_ne [projection, in PRFA.live_coding4]
m_ty [projection, in PRFA.live_coding4]
m_assoc [projection, in PRFA.tp4c]
m_r_ne [projection, in PRFA.tp4c]
m_l_ne [projection, in PRFA.tp4c]
m_op [projection, in PRFA.tp4c]
m_ne [projection, in PRFA.tp4c]
m_ty [projection, in PRFA.tp4c]

N

N [constructor, in PRFA.live_coding3]
N [constructor, in PRFA.tp3c]
nat_rect [definition, in PRFA.live_coding3]
nat_nat_fact [lemma, in PRFA.live_coding4]
nat_nat_fact [lemma, in PRFA.live_coding4]
nat_fact [lemma, in PRFA.live_coding4]
nat_monoid [definition, in PRFA.live_coding4]
nat_ind_2 [lemma, in PRFA.tp5c]
nat_fact [lemma, in PRFA.tp4c]
nat_monoid [definition, in PRFA.tp4c]
nat_eqdec_eq [lemma, in PRFA.tp7c]
nat_bool [lemma, in PRFA.tp7c]
nbe [definition, in PRFA.tp8c]
ncons [constructor, in PRFA.live_coding3]
ncons [constructor, in PRFA.tp3c]
neg [definition, in PRFA.live_coding8]
negb_invol [lemma, in PRFA.live_coding1]
negb_true [lemma, in PRFA.live_coding1]
neg_inv [lemma, in PRFA.live_coding8]
neg_inv [lemma, in PRFA.live_coding8]
neg_inv [lemma, in PRFA.live_coding8]
neg_inv [lemma, in PRFA.live_coding8]
neg_eq_False [lemma, in PRFA.tp7c]
neq_nat_neq [lemma, in PRFA.tp8c]
nforest [inductive, in PRFA.live_coding3]
nforest [inductive, in PRFA.tp3c]
nforest_sind [definition, in PRFA.live_coding3]
nforest_rec [definition, in PRFA.live_coding3]
nforest_ind [definition, in PRFA.live_coding3]
nforest_rect [definition, in PRFA.live_coding3]
nforest_ntree_rec [definition, in PRFA.tp3c]
nforest_map [definition, in PRFA.tp3c]
nforest_sind [definition, in PRFA.tp3c]
nforest_rec [definition, in PRFA.tp3c]
nforest_ind [definition, in PRFA.tp3c]
nforest_rect [definition, in PRFA.tp3c]
nil [constructor, in PRFA.review6]
nlam [constructor, in PRFA.tp8c]
nnil [constructor, in PRFA.live_coding3]
nnil [constructor, in PRFA.tp3c]
nnode [constructor, in PRFA.live_coding3]
nnode [constructor, in PRFA.tp3c]
node [constructor, in PRFA.live_coding5]
node [constructor, in PRFA.tp5c]
nofalse [lemma, in PRFA.tp1c]
nofalse [lemma, in PRFA.live_coding1]
normal [inductive, in PRFA.tp8c]
normal_sind [definition, in PRFA.tp8c]
normal_rec [definition, in PRFA.tp8c]
normal_ind [definition, in PRFA.tp8c]
normal_rect [definition, in PRFA.tp8c]
not_mult4_sind [definition, in PRFA.live_coding6]
not_mult4_ind [definition, in PRFA.live_coding6]
not_mult4_plus [constructor, in PRFA.live_coding6]
not_mult4_3 [constructor, in PRFA.live_coding6]
not_mult4_2 [constructor, in PRFA.live_coding6]
not_mult4_1 [constructor, in PRFA.live_coding6]
not_mult4 [inductive, in PRFA.live_coding6]
not_even1_term [definition, in PRFA.tp7c]
not_even1 [lemma, in PRFA.tp7c]
nren [definition, in PRFA.tp8c]
nstar [constructor, in PRFA.tp8c]
nstuck [constructor, in PRFA.tp8c]
ntree [inductive, in PRFA.live_coding3]
ntree [inductive, in PRFA.tp3c]
ntree_sind [definition, in PRFA.live_coding3]
ntree_rec [definition, in PRFA.live_coding3]
ntree_ind [definition, in PRFA.live_coding3]
ntree_rect [definition, in PRFA.live_coding3]
ntree_nforest_rec [definition, in PRFA.tp3c]
ntree_map [definition, in PRFA.tp3c]
ntree_sind [definition, in PRFA.tp3c]
ntree_rec [definition, in PRFA.tp3c]
ntree_ind [definition, in PRFA.tp3c]
ntree_rect [definition, in PRFA.tp3c]
num [definition, in PRFA.tp2c]
num [projection, in PRFA.tp6c]
numerator [projection, in PRFA.live_coding4]
numerator' [projection, in PRFA.live_coding4]
numerator'' [projection, in PRFA.live_coding4]
Nx [constructor, in PRFA.tp3c]
n_plus_0 [lemma, in PRFA.tp1c]

O

of_nat_inj [lemma, in PRFA.tp2c]
of_nat [definition, in PRFA.tp2c]
one_zero_Z [lemma, in PRFA.tp4c]
or_imp [lemma, in PRFA.tp1c]
or_comm [lemma, in PRFA.tp1c]
or_imp [definition, in PRFA.review3]
or_com [lemma, in PRFA.tp4c]
or_AA [lemma, in PRFA.tp4c]
or_comm [definition, in PRFA.tp3c]
or_comm [lemma, in PRFA.live_coding1]

P

pfalse [constructor, in PRFA.live_coding5]
pfalse [constructor, in PRFA.tp5c]
PI [definition, in PRFA.live_coding5]
PI_UIP [definition, in PRFA.live_coding7]
PI_UIP [definition, in PRFA.tp7c]
PL [definition, in PRFA.tp1c]
plus_assoc [lemma, in PRFA.tp1c]
plus_comm [lemma, in PRFA.tp1c]
plus_S [lemma, in PRFA.tp1c]
pl_lem [lemma, in PRFA.tp1c]
pneg [definition, in PRFA.live_coding5]
pneg_invol [lemma, in PRFA.live_coding5]
point3D [record, in PRFA.tp6c]
positive [projection, in PRFA.tp6c]
pow13 [definition, in PRFA.live_coding6]
pow3 [definition, in PRFA.live_coding6]
pow5 [definition, in PRFA.live_coding6]
pred [definition, in PRFA.tp2c]
predext [lemma, in PRFA.tp7c]
pred_from_nat [lemma, in PRFA.tp2c]
pred' [definition, in PRFA.tp2c]
pred'_from_nat [lemma, in PRFA.tp2c]
prod_monoid [definition, in PRFA.live_coding4]
prod_monoid [definition, in PRFA.tp4c]
prod' [record, in PRFA.review4]
prod' [record, in PRFA.live_coding4]
prod' [record, in PRFA.tp4c]
prod'_ind [definition, in PRFA.review4]
ProofIrrelevance [definition, in PRFA.live_coding7]
ProofIrrelevance [definition, in PRFA.tp7c]
proof_irrelevance [lemma, in PRFA.live_coding7]
proof_irrelevance [lemma, in PRFA.tp7c]
PropExt [definition, in PRFA.tp5c]
propext [axiom, in PRFA.live_coding7]
PropExt [definition, in PRFA.live_coding7]
propext [axiom, in PRFA.tp7c]
PropExt [definition, in PRFA.tp7c]
prop_bool_sind [definition, in PRFA.live_coding5]
prop_bool_ind [definition, in PRFA.live_coding5]
prop_bool [inductive, in PRFA.live_coding5]
prop_bool_sind [definition, in PRFA.tp5c]
prop_bool_ind [definition, in PRFA.tp5c]
prop_bool [inductive, in PRFA.tp5c]
ptrue [constructor, in PRFA.live_coding5]
ptrue [constructor, in PRFA.tp5c]
px [projection, in PRFA.tp6c]
py [projection, in PRFA.tp6c]
pz [projection, in PRFA.tp6c]
P_iff_P [lemma, in PRFA.tp1c]
P_imp_P [lemma, in PRFA.tp1c]
P_eventually_implies_acc_ex [lemma, in PRFA.tp5c]
P_eventually_implies_acc [lemma, in PRFA.tp5c]
P_implies_acc [lemma, in PRFA.tp5c]
P_imp_P [lemma, in PRFA.live_coding1]
p1 [projection, in PRFA.tp6c]
p2 [projection, in PRFA.tp6c]
p3 [projection, in PRFA.tp6c]

Q

quarter [definition, in PRFA.live_coding4]
quarter'' [definition, in PRFA.live_coding4]
q_upd_num [definition, in PRFA.tp6c]
q_foo [definition, in PRFA.tp6c]

R

random [axiom, in PRFA.tp6c]
rational [record, in PRFA.live_coding4]
refl [constructor, in PRFA.tp2c]
refl [constructor, in PRFA.live_coding2]
reflect [definition, in PRFA.tp8c]
refl_eq [constructor, in PRFA.tp7c]
refl' [constructor, in PRFA.tp2c]
reify [definition, in PRFA.tp8c]
reify [definition, in PRFA.tp6c]
ren [definition, in PRFA.tp8c]
rencomp [definition, in PRFA.tp8c]
renval [definition, in PRFA.tp8c]
repeat [definition, in PRFA.tp8c]
repeat_ind [lemma, in PRFA.tp8c]
REPLACE_ME [definition, in PRFA.tp1c]
REPLACE_ME [axiom, in PRFA.tp8c]
replace_const_lift [definition, in PRFA.tp6c]
review2 [library]
review3 [library]
review4 [library]
review6 [library]
review7 [library]
rev_rev [lemma, in PRFA.tp2c]
rev_app_distr [lemma, in PRFA.tp2c]
rev_rev [lemma, in PRFA.live_coding2]
rev_app_distr [lemma, in PRFA.live_coding2]
rev_acc [definition, in PRFA.tp8c]
rho0 [definition, in PRFA.live_coding8]
rtclos [inductive, in PRFA.tp2c]
rtclos [inductive, in PRFA.live_coding2]
rtclos_iff [lemma, in PRFA.tp2c]
rtclos_sind [definition, in PRFA.tp2c]
rtclos_ind [definition, in PRFA.tp2c]
rtclos_sind [definition, in PRFA.live_coding2]
rtclos_ind [definition, in PRFA.live_coding2]
rtclos' [inductive, in PRFA.tp2c]
rtclos'_trans [lemma, in PRFA.tp2c]
rtclos'_sind [definition, in PRFA.tp2c]
rtclos'_ind [definition, in PRFA.tp2c]
Russel [lemma, in PRFA.tp1c]
Russel [definition, in PRFA.review3]
Russel [definition, in PRFA.review3]
Russel [definition, in PRFA.tp3c]
Russell [lemma, in PRFA.live_coding3]
r_to_r [projection, in PRFA.tp8c]
r_to_l [projection, in PRFA.tp8c]
R_step2 [lemma, in PRFA.tp5c]

S

sapp [constructor, in PRFA.tp8c]
sem [definition, in PRFA.tp8c]
semren [definition, in PRFA.tp8c]
Show_Definitions.or_sind [definition, in PRFA.live_coding3]
Show_Definitions.or_ind [definition, in PRFA.live_coding3]
Show_Definitions.or_intror [constructor, in PRFA.live_coding3]
Show_Definitions.or_introl [constructor, in PRFA.live_coding3]
Show_Definitions.or [inductive, in PRFA.live_coding3]
Show_Definitions.and_sind [definition, in PRFA.live_coding3]
Show_Definitions.and_rec [definition, in PRFA.live_coding3]
Show_Definitions.and_ind [definition, in PRFA.live_coding3]
Show_Definitions.and_rect [definition, in PRFA.live_coding3]
Show_Definitions.conj [constructor, in PRFA.live_coding3]
Show_Definitions.and [inductive, in PRFA.live_coding3]
~ _ [notation, in PRFA.live_coding3]
Show_Definitions.True_sind [definition, in PRFA.live_coding3]
Show_Definitions.True_rec [definition, in PRFA.live_coding3]
Show_Definitions.True_ind [definition, in PRFA.live_coding3]
Show_Definitions.True_rect [definition, in PRFA.live_coding3]
Show_Definitions.I [constructor, in PRFA.live_coding3]
Show_Definitions.True [inductive, in PRFA.live_coding3]
Show_Definitions.False_sind [definition, in PRFA.live_coding3]
Show_Definitions.False_rec [definition, in PRFA.live_coding3]
Show_Definitions.False_ind [definition, in PRFA.live_coding3]
Show_Definitions.False_rect [definition, in PRFA.live_coding3]
Show_Definitions.False [inductive, in PRFA.live_coding3]
Show_Definitions [module, in PRFA.live_coding3]
sig_ext [lemma, in PRFA.tp7c]
SIP_UIP [lemma, in PRFA.tp7c]
size_recursion [lemma, in PRFA.live_coding5]
snd' [projection, in PRFA.review4]
snd' [projection, in PRFA.live_coding4]
snd' [projection, in PRFA.tp4c]
some_tree [definition, in PRFA.live_coding3]
some_other_pair [definition, in PRFA.live_coding4]
some_pair [definition, in PRFA.live_coding4]
some_other_pair [definition, in PRFA.tp4c]
some_pair [definition, in PRFA.tp4c]
sorted [inductive, in PRFA.tp5c]
sorted_cons_inv [lemma, in PRFA.tp5c]
sorted_sind [definition, in PRFA.tp5c]
sorted_ind [definition, in PRFA.tp5c]
sorted_cons [constructor, in PRFA.tp5c]
sorted_nil [constructor, in PRFA.tp5c]
split_two [definition, in PRFA.live_coding8]
sren [definition, in PRFA.tp8c]
stable [definition, in PRFA.tp7c]
strong_nat_ind [lemma, in PRFA.tp2c]
strong_nat_ind [lemma, in PRFA.live_coding2]
strong_nat_ind [lemma, in PRFA.review2]
strong_nat_ind [lemma, in PRFA.tp5c]
stuck [inductive, in PRFA.tp8c]
stuck_vnil_inv [lemma, in PRFA.tp8c]
stuck_sind [definition, in PRFA.tp8c]
stuck_rec [definition, in PRFA.tp8c]
stuck_ind [definition, in PRFA.tp8c]
stuck_rect [definition, in PRFA.tp8c]
succ [definition, in PRFA.tp2c]
sval [definition, in PRFA.tp8c]
svar [constructor, in PRFA.tp8c]
swap [definition, in PRFA.tp2c]
swap_invol [lemma, in PRFA.tp2c]
sym_eq [constructor, in PRFA.tp7c]
S_neq [lemma, in PRFA.tp3c]

T

T [definition, in PRFA.live_coding3]
tail [definition, in PRFA.tp8c]
tail [definition, in PRFA.live_coding8]
tail' [definition, in PRFA.live_coding8]
tapp [constructor, in PRFA.tp8c]
tapp [constructor, in PRFA.live_coding8]
tarrow [constructor, in PRFA.tp8c]
tarrow [constructor, in PRFA.live_coding8]
Tauto [section, in PRFA.tp6c]
Tauto.P [variable, in PRFA.tp6c]
Tauto.Q [variable, in PRFA.tp6c]
Tauto.R [variable, in PRFA.tp6c]
term [inductive, in PRFA.tp8c]
term [inductive, in PRFA.live_coding8]
term_eqb [definition, in PRFA.MetaCoqPrelude]
term_sind [definition, in PRFA.tp8c]
term_rec [definition, in PRFA.tp8c]
term_ind [definition, in PRFA.tp8c]
term_rect [definition, in PRFA.tp8c]
term_sind [definition, in PRFA.live_coding8]
term_rec [definition, in PRFA.live_coding8]
term_ind [definition, in PRFA.live_coding8]
term_rect [definition, in PRFA.live_coding8]
test [lemma, in PRFA.live_coding6]
test [definition, in PRFA.tp8c]
test [definition, in PRFA.live_coding8]
test [definition, in PRFA.tp6c]
test [module, in PRFA.tp6c]
test_nat' [lemma, in PRFA.live_coding4]
test_monoid [lemma, in PRFA.live_coding4]
test_nat [lemma, in PRFA.live_coding4]
test_list [lemma, in PRFA.tp4c]
test_nat' [lemma, in PRFA.tp4c]
test_monoid [lemma, in PRFA.tp4c]
test_nat [lemma, in PRFA.tp4c]
test' [definition, in PRFA.live_coding8]
test.DNE [lemma, in PRFA.tp6c]
theDNS [definition, in PRFA.tp1c]
theLEM [definition, in PRFA.tp1c]
thePL [definition, in PRFA.tp1c]
tid [definition, in PRFA.tp8c]
tl [definition, in PRFA.tp8c]
tLam [abbreviation, in PRFA.MetaCoqPrelude]
tlam [constructor, in PRFA.tp8c]
tlam [constructor, in PRFA.live_coding8]
tLet [abbreviation, in PRFA.MetaCoqPrelude]
tmDebugDefinition [definition, in PRFA.tp6c]
tm_fold [definition, in PRFA.MetaCoqPrelude]
tm_nb_handler [definition, in PRFA.MetaCoqPrelude]
tm_handler [definition, in PRFA.MetaCoqPrelude]
tNat [definition, in PRFA.live_coding6]
to_nat_inj [lemma, in PRFA.tp2c]
to_nat [definition, in PRFA.tp2c]
to_nat' [definition, in PRFA.tp2c]
to_not_not [lemma, in PRFA.tp1c]
to_vec [definition, in PRFA.tp8c]
to_list [definition, in PRFA.tp8c]
to_ilist [definition, in PRFA.tp8c]
to_tree_map [lemma, in PRFA.live_coding5]
to_bool_function_not_PI [lemma, in PRFA.live_coding5]
to_bool [lemma, in PRFA.live_coding5]
to_bool [lemma, in PRFA.live_coding5]
to_bool [definition, in PRFA.live_coding5]
to_prop_bool [definition, in PRFA.live_coding5]
to_prod_alt3 [definition, in PRFA.live_coding4]
to_prod_alt2 [definition, in PRFA.live_coding4]
to_prod_alt [definition, in PRFA.live_coding4]
to_prod [definition, in PRFA.live_coding4]
to_tree_map [lemma, in PRFA.tp5c]
to_sig_bool [lemma, in PRFA.tp5c]
to_disj [definition, in PRFA.tp5c]
to_exists [lemma, in PRFA.tp5c]
to_bool [lemma, in PRFA.tp5c]
to_prop_bool [definition, in PRFA.tp5c]
to_prod_eq [lemma, in PRFA.tp4c]
to_prod_alt3 [definition, in PRFA.tp4c]
to_prod_alt2 [definition, in PRFA.tp4c]
to_prod_alt [definition, in PRFA.tp4c]
to_prod [definition, in PRFA.tp4c]
to_equiv [definition, in PRFA.tp7c]
to_from_tree [lemma, in PRFA.tp3c]
to_tree_list [definition, in PRFA.tp3c]
to_tree [definition, in PRFA.tp3c]
TP1 [section, in PRFA.tp1c]
tp1c [library]
tp2c [library]
tp3c [library]
tp4c [library]
tp5c [library]
tp6c [library]
tp7c [library]
tp8c [library]
trans [constructor, in PRFA.tp2c]
trans [constructor, in PRFA.live_coding2]
transform [definition, in PRFA.MetaCoqPrelude]
transform_nb [definition, in PRFA.MetaCoqPrelude]
transport [definition, in PRFA.tp8c]
transport [definition, in PRFA.tp5c]
transport [definition, in PRFA.live_coding7]
transport [definition, in PRFA.tp7c]
transportK [lemma, in PRFA.tp8c]
transport_vcons [lemma, in PRFA.tp8c]
trans_eq [constructor, in PRFA.tp7c]
trans' [constructor, in PRFA.tp2c]
trap [record, in PRFA.tp6c]
tree [inductive, in PRFA.live_coding5]
tree [inductive, in PRFA.live_coding3]
tree [inductive, in PRFA.tp5c]
tree [inductive, in PRFA.tp3c]
tree_map_id_again' [lemma, in PRFA.live_coding5]
tree_map_id_again [lemma, in PRFA.live_coding5]
tree_map_id [definition, in PRFA.live_coding5]
tree_map_id [lemma, in PRFA.live_coding5]
tree_map [definition, in PRFA.live_coding5]
tree_sind [definition, in PRFA.live_coding5]
tree_rec [definition, in PRFA.live_coding5]
tree_ind [definition, in PRFA.live_coding5]
tree_rect [definition, in PRFA.live_coding5]
tree_sind [definition, in PRFA.live_coding3]
tree_rec [definition, in PRFA.live_coding3]
tree_ind [definition, in PRFA.live_coding3]
tree_rect [definition, in PRFA.live_coding3]
tree_map_id [lemma, in PRFA.tp5c]
tree_map [definition, in PRFA.tp5c]
tree_sind [definition, in PRFA.tp5c]
tree_rec [definition, in PRFA.tp5c]
tree_ind [definition, in PRFA.tp5c]
tree_rect [definition, in PRFA.tp5c]
tree_rect_strong [definition, in PRFA.tp3c]
tree_sind [definition, in PRFA.tp3c]
tree_rec [definition, in PRFA.tp3c]
tree_ind [definition, in PRFA.tp3c]
tree_rect [definition, in PRFA.tp3c]
triple [record, in PRFA.tp6c]
truetrue [lemma, in PRFA.tp1c]
truetrue [lemma, in PRFA.live_coding1]
true_false [lemma, in PRFA.tp2c]
true_false [lemma, in PRFA.review3]
tstar [constructor, in PRFA.tp8c]
tstar [constructor, in PRFA.live_coding8]
tunit [constructor, in PRFA.tp8c]
tunit [constructor, in PRFA.live_coding8]
tvar [constructor, in PRFA.tp8c]
tvar [constructor, in PRFA.live_coding8]
twice [lemma, in PRFA.tp1c]
type [inductive, in PRFA.tp8c]
type [inductive, in PRFA.live_coding8]
type_sind [definition, in PRFA.tp8c]
type_rec [definition, in PRFA.tp8c]
type_ind [definition, in PRFA.tp8c]
type_rect [definition, in PRFA.tp8c]
type_sind [definition, in PRFA.live_coding8]
type_rec [definition, in PRFA.live_coding8]
type_ind [definition, in PRFA.live_coding8]
type_rect [definition, in PRFA.live_coding8]

U

UIP [definition, in PRFA.live_coding7]
UIP [definition, in PRFA.tp7c]
UIP_for_nat [lemma, in PRFA.tp7c]
UIP_refl_nat [lemma, in PRFA.tp7c]
UIP_nat' [lemma, in PRFA.tp7c]
UIP_for [definition, in PRFA.tp7c]
UIP_K [definition, in PRFA.tp7c]
unaxiom [definition, in PRFA.tp6c]
unfold_toplevel [definition, in PRFA.MetaCoqPrelude]
unit_neq_bool [lemma, in PRFA.live_coding7]
unit_bool [definition, in PRFA.tp7c]
unit_neq_bool [lemma, in PRFA.tp7c]
Univalence [definition, in PRFA.tp7c]
Univalence_neg_UIP [lemma, in PRFA.tp7c]
univalence_equiv_equal [lemma, in PRFA.tp7c]
Universes [section, in PRFA.live_coding5]
Universes.A [variable, in PRFA.live_coding5]
Universes.B [variable, in PRFA.live_coding5]
Universes.C [variable, in PRFA.live_coding5]
Universes.P [variable, in PRFA.live_coding5]
Universes.Q [variable, in PRFA.live_coding5]
unkown [axiom, in PRFA.tp6c]
Unnamed_thm2 [definition, in PRFA.live_coding6]
Unnamed_thm1 [definition, in PRFA.live_coding6]
Unnamed_thm1 [definition, in PRFA.live_coding6]
Unnamed_thm0 [definition, in PRFA.live_coding6]
Unnamed_thm [definition, in PRFA.live_coding6]
Unnamed_thm1 [definition, in PRFA.review4]
Unnamed_thm0 [definition, in PRFA.review4]
Unnamed_thm [definition, in PRFA.review4]
Unnamed_thm [definition, in PRFA.review6]
Unnamed_thm [definition, in PRFA.review6]
Unnamed_thm [definition, in PRFA.review6]
Unnamed_thm4 [definition, in PRFA.live_coding2]
Unnamed_thm3 [definition, in PRFA.live_coding2]
Unnamed_thm2 [definition, in PRFA.live_coding2]
Unnamed_thm1 [definition, in PRFA.live_coding2]
Unnamed_thm1 [definition, in PRFA.live_coding2]
Unnamed_thm0 [definition, in PRFA.live_coding2]
Unnamed_thm [definition, in PRFA.live_coding2]
Unnamed_thm2 [definition, in PRFA.live_coding5]
Unnamed_thm2 [definition, in PRFA.live_coding5]
Unnamed_thm1 [definition, in PRFA.live_coding5]
Unnamed_thm0 [definition, in PRFA.live_coding5]
Unnamed_thm [definition, in PRFA.live_coding5]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm6 [definition, in PRFA.live_coding3]
Unnamed_thm5 [definition, in PRFA.live_coding3]
Unnamed_thm4 [definition, in PRFA.live_coding3]
Unnamed_thm3 [definition, in PRFA.live_coding3]
Unnamed_thm2 [definition, in PRFA.live_coding3]
Unnamed_thm1 [definition, in PRFA.live_coding3]
Unnamed_thm0 [definition, in PRFA.live_coding3]
Unnamed_thm [definition, in PRFA.live_coding3]
Unnamed_thm2 [definition, in PRFA.live_coding4]
Unnamed_thm1 [definition, in PRFA.live_coding4]
Unnamed_thm0 [definition, in PRFA.live_coding4]
Unnamed_thm [definition, in PRFA.live_coding4]
Unnamed_thm [definition, in PRFA.review2]
Unnamed_thm0 [definition, in PRFA.tp5c]
Unnamed_thm0 [definition, in PRFA.tp5c]
Unnamed_thm [definition, in PRFA.tp5c]
Unnamed_thm18 [definition, in PRFA.tp4c]
Unnamed_thm17 [definition, in PRFA.tp4c]
Unnamed_thm16 [definition, in PRFA.tp4c]
Unnamed_thm15 [definition, in PRFA.tp4c]
Unnamed_thm14 [definition, in PRFA.tp4c]
Unnamed_thm13 [definition, in PRFA.tp4c]
Unnamed_thm12 [definition, in PRFA.tp4c]
Unnamed_thm11 [definition, in PRFA.tp4c]
Unnamed_thm10 [definition, in PRFA.tp4c]
Unnamed_thm9 [definition, in PRFA.tp4c]
Unnamed_thm8 [definition, in PRFA.tp4c]
Unnamed_thm7 [definition, in PRFA.tp4c]
Unnamed_thm6 [definition, in PRFA.tp4c]
Unnamed_thm5 [definition, in PRFA.tp4c]
Unnamed_thm4 [definition, in PRFA.tp4c]
Unnamed_thm3 [definition, in PRFA.tp4c]
Unnamed_thm2 [definition, in PRFA.tp4c]
Unnamed_thm1 [definition, in PRFA.tp4c]
Unnamed_thm0 [definition, in PRFA.tp4c]
Unnamed_thm [definition, in PRFA.tp4c]
Unnamed_thm1 [definition, in PRFA.live_coding7]
Unnamed_thm0 [definition, in PRFA.live_coding7]
Unnamed_thm0 [definition, in PRFA.live_coding7]
Unnamed_thm [definition, in PRFA.live_coding7]
Unnamed_thm8 [definition, in PRFA.tp6c]
Unnamed_thm7 [definition, in PRFA.tp6c]
Unnamed_thm6 [definition, in PRFA.tp6c]
Unnamed_thm5 [definition, in PRFA.tp6c]
Unnamed_thm4 [definition, in PRFA.tp6c]
Unnamed_thm3 [definition, in PRFA.tp6c]
Unnamed_thm2 [definition, in PRFA.tp6c]
Unnamed_thm1 [definition, in PRFA.tp6c]
Unnamed_thm1 [definition, in PRFA.tp6c]
Unnamed_thm1 [definition, in PRFA.tp6c]
Unnamed_thm0 [definition, in PRFA.tp6c]
Unnamed_thm0 [definition, in PRFA.tp6c]
Unnamed_thm0 [definition, in PRFA.tp6c]
Unnamed_thm0 [definition, in PRFA.tp6c]
Unnamed_thm [definition, in PRFA.tp6c]
Unnamed_thm0 [definition, in PRFA.tp3c]
Unnamed_thm [definition, in PRFA.tp3c]
upd_num [definition, in PRFA.tp6c]

V

valuation [definition, in PRFA.live_coding8]
vcons [constructor, in PRFA.tp8c]
vcons [constructor, in PRFA.live_coding8]
vec [inductive, in PRFA.tp8c]
vec [inductive, in PRFA.live_coding8]
vec_sind [definition, in PRFA.tp8c]
vec_rec [definition, in PRFA.tp8c]
vec_ind [definition, in PRFA.tp8c]
vec_rect [definition, in PRFA.tp8c]
vec_expand [lemma, in PRFA.live_coding8]
vec_sind [definition, in PRFA.live_coding8]
vec_rec [definition, in PRFA.live_coding8]
vec_ind [definition, in PRFA.live_coding8]
vec_rect [definition, in PRFA.live_coding8]
vmap [definition, in PRFA.tp8c]
vmap_ind [lemma, in PRFA.tp8c]
vnil [constructor, in PRFA.tp8c]
vnil [constructor, in PRFA.live_coding8]
vnth [definition, in PRFA.tp8c]
vnth [definition, in PRFA.live_coding8]
vnth_vmap [lemma, in PRFA.tp8c]
vnth_repeat [lemma, in PRFA.tp8c]
vnth_repeat [lemma, in PRFA.tp8c]
v1 [projection, in PRFA.tp6c]
v2 [projection, in PRFA.tp6c]
v3 [projection, in PRFA.tp6c]

W

weak [definition, in PRFA.tp8c]
Well_founded.R [variable, in PRFA.live_coding5]
Well_founded.A [variable, in PRFA.live_coding5]
Well_founded [section, in PRFA.live_coding5]
what [definition, in PRFA.tp6c]
WO [section, in PRFA.live_coding5]
WO.f [variable, in PRFA.live_coding5]
wpermut [definition, in PRFA.tp5c]
wpermut_app [lemma, in PRFA.tp5c]
wpermut_cons [lemma, in PRFA.tp5c]
wpermut_trans [instance, in PRFA.tp5c]
wpermut_sym [instance, in PRFA.tp5c]
wpermut_refl [instance, in PRFA.tp5c]

X

xren [definition, in PRFA.tp8c]
xtree [inductive, in PRFA.tp3c]
xtree_rect_strong [definition, in PRFA.tp3c]
xtree_sind [definition, in PRFA.tp3c]
xtree_rec [definition, in PRFA.tp3c]
xtree_ind [definition, in PRFA.tp3c]
xtree_rect [definition, in PRFA.tp3c]

Z

Zalt [record, in PRFA.tp6c]
zero [definition, in PRFA.tp2c]
zip [definition, in PRFA.tp8c]
zip [definition, in PRFA.live_coding8]
zip [definition, in PRFA.live_coding8]
zip_vnth [lemma, in PRFA.live_coding8]

other

_ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
' _ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
mlet ' _ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
mlet _ <- _ ;; _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ =<< _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ >>= _ (tm_scope) [notation, in PRFA.MetaCoqPrelude]
_ == _ [notation, in PRFA.MetaCoqPrelude]
_ ~> _ [notation, in PRFA.tp8c]
_ ** _ [notation, in PRFA.live_coding4]
_ ~> _ [notation, in PRFA.live_coding8]
_ +++ _ [notation, in PRFA.live_coding8]
_ ~ _ [notation, in PRFA.tp4c]
_ ** _ [notation, in PRFA.tp4c]
_ ** _ [notation, in PRFA.tp4c]
_ # _ [notation, in PRFA.tp6c]
__ [notation, in PRFA.MetaCoqPrelude]
$name _ [notation, in PRFA.MetaCoqPrelude]
$Quote_rec _ [notation, in PRFA.MetaCoqPrelude]
$quote_rec _ [notation, in PRFA.MetaCoqPrelude]
$Quote _ [notation, in PRFA.MetaCoqPrelude]
$quote _ [notation, in PRFA.MetaCoqPrelude]
$run _ [notation, in PRFA.MetaCoqPrelude]
$unquote _ : _ [notation, in PRFA.MetaCoqPrelude]
$unquote _ [notation, in PRFA.MetaCoqPrelude]
⟨ _ ⟩ [notation, in PRFA.tp8c]
⟨ _ | _ ⟩ [notation, in PRFA.tp8c]

---

Notation Index

D

_ - _ [in PRFA.tp2c]
_ + _ [in PRFA.tp2c]
_ - _ [in PRFA.live_coding2]
_ + _ [in PRFA.live_coding2]

L

_ == _ [in PRFA.live_coding7]
_ == _ [in PRFA.tp7c]
_ == _ [in PRFA.tp7c]

S

~ _ [in PRFA.live_coding3]

other

_ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
' _ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
mlet ' _ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
mlet _ <- _ ;; _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ =<< _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ >>= _ (tm_scope) [in PRFA.MetaCoqPrelude]
_ == _ [in PRFA.MetaCoqPrelude]
_ ~> _ [in PRFA.tp8c]
_ ** _ [in PRFA.live_coding4]
_ ~> _ [in PRFA.live_coding8]
_ +++ _ [in PRFA.live_coding8]
_ ~ _ [in PRFA.tp4c]
_ ** _ [in PRFA.tp4c]
_ ** _ [in PRFA.tp4c]
_ # _ [in PRFA.tp6c]
__ [in PRFA.MetaCoqPrelude]
$name _ [in PRFA.MetaCoqPrelude]
$Quote_rec _ [in PRFA.MetaCoqPrelude]
$quote_rec _ [in PRFA.MetaCoqPrelude]
$Quote _ [in PRFA.MetaCoqPrelude]
$quote _ [in PRFA.MetaCoqPrelude]
$run _ [in PRFA.MetaCoqPrelude]
$unquote _ : _ [in PRFA.MetaCoqPrelude]
$unquote _ [in PRFA.MetaCoqPrelude]
⟨ _ ⟩ [in PRFA.tp8c]
⟨ _ | _ ⟩ [in PRFA.tp8c]

---

Module Index

D

define_nat [in PRFA.tp2c]
define_sigma [in PRFA.live_coding2]
define_list [in PRFA.live_coding2]
define_prod [in PRFA.live_coding2]
define_bool [in PRFA.live_coding2]
define_nat.variant2 [in PRFA.live_coding2]
define_nat.variant1 [in PRFA.live_coding2]
define_nat [in PRFA.live_coding2]

F

Fib_Iter [in PRFA.tp2c]

H

Hierarchy [in PRFA.tp3c]

L

Leibniz [in PRFA.live_coding7]
Leibniz [in PRFA.tp7c]
Leibniz.EqDef [in PRFA.live_coding7]
Leibniz2 [in PRFA.tp7c]

S

Show_Definitions [in PRFA.live_coding3]

T

test [in PRFA.tp6c]

---

Variable Index

C

ConstructiveIndefiniteGroundDescription_Acc.R [in PRFA.tp5c]
ConstructiveIndefiniteGroundDescription_Acc.P_decidable [in PRFA.tp5c]
ConstructiveIndefiniteGroundDescription_Acc.P [in PRFA.tp5c]

D

Demo.X [in PRFA.live_coding3]
Demo.Y [in PRFA.live_coding3]
Demo.Z [in PRFA.live_coding3]

M

Merge.m [in PRFA.tp5c]
Merge.R [in PRFA.tp5c]
Merge.T [in PRFA.tp5c]

T

Tauto.P [in PRFA.tp6c]
Tauto.Q [in PRFA.tp6c]
Tauto.R [in PRFA.tp6c]

U

Universes.A [in PRFA.live_coding5]
Universes.B [in PRFA.live_coding5]
Universes.C [in PRFA.live_coding5]
Universes.P [in PRFA.live_coding5]
Universes.Q [in PRFA.live_coding5]

W

Well_founded.R [in PRFA.live_coding5]
Well_founded.A [in PRFA.live_coding5]
WO.f [in PRFA.live_coding5]

---

Library Index

L

live_coding6
live_coding5
live_coding8
live_coding2
live_coding1
live_coding4
live_coding3
live_coding7

M

MetaCoqPrelude

R

review2
review3
review4
review6
review7

T

tp1c
tp2c
tp3c
tp4c
tp5c
tp6c
tp7c
tp8c

---

Lemma Index

A

Acc_iff [in PRFA.live_coding5]
Acc_rect_dep [in PRFA.tp5c]
acc_implies_P_eventually [in PRFA.tp5c]
add_from_nat [in PRFA.tp2c]
add_sub [in PRFA.review2]
add'_correct [in PRFA.review7]
andb_orb_distr [in PRFA.tp1c]
andb_comm' [in PRFA.live_coding1]
andb_comm [in PRFA.live_coding1]
and_comm [in PRFA.tp1c]
and_assoc [in PRFA.tp4c]
and_com [in PRFA.tp4c]
and_AA [in PRFA.tp4c]
and_comm [in PRFA.live_coding1]
anything_goes [in PRFA.tp1c]
anything_goes [in PRFA.live_coding1]
app_assoc [in PRFA.tp2c]
app_nil_r [in PRFA.tp2c]
app_nil_r [in PRFA.live_coding2]
app_nil_r [in PRFA.live_coding8]
app_assoc [in PRFA.live_coding8]
app_ind [in PRFA.live_coding8]

B

bad_not_bad [in PRFA.tp3c]
bt_map_id [in PRFA.live_coding5]
bt_map_id [in PRFA.tp5c]

C

calc_12_3 [in PRFA.tp1c]
calc_12_3 [in PRFA.live_coding1]
cancel_to_of [in PRFA.tp2c]
cancel_of_to [in PRFA.tp2c]
Cantor_bool' [in PRFA.tp7c]
car_cur [in PRFA.tp2c]
car_cur [in PRFA.live_coding2]
classical_impl [in PRFA.tp1c]
classical_or_contra_r [in PRFA.tp1c]
constructive_indefinite_ground_description_nat_Acc [in PRFA.tp5c]
contrad [in PRFA.tp1c]
contrapositive [in PRFA.tp1c]
cur_car [in PRFA.tp2c]
cur_car [in PRFA.live_coding2]

D

define_nat.add_sub_alt [in PRFA.tp2c]
define_nat.sub_O [in PRFA.tp2c]
define_nat.add_sub [in PRFA.tp2c]
define_nat.add_S [in PRFA.tp2c]
define_nat.add_0 [in PRFA.tp2c]
define_bool.true_false [in PRFA.live_coding2]
define_nat.eq_nat_spec [in PRFA.live_coding2]
define_nat.eq_nat_spec [in PRFA.live_coding2]
define_nat.S_inj_4 [in PRFA.live_coding2]
define_nat.S_inj_3 [in PRFA.live_coding2]
define_nat.S_inj_2 [in PRFA.live_coding2]
define_nat.S_inj [in PRFA.live_coding2]
define_nat.S_0' [in PRFA.live_coding2]
define_nat.S_O [in PRFA.live_coding2]
define_nat.add_sub [in PRFA.live_coding2]
define_nat.add_S [in PRFA.live_coding2]
define_nat.add_0 [in PRFA.live_coding2]
dep_f_equal [in PRFA.live_coding7]
dep_f_equal [in PRFA.live_coding7]
dep_f_equal [in PRFA.tp7c]
de_morgan [in PRFA.tp1c]
distr [in PRFA.tp1c]
div2_double [in PRFA.tp7c]
dns_lem [in PRFA.tp1c]
dn_functorial [in PRFA.tp1c]
double_eq [in PRFA.tp1c]
double_div2 [in PRFA.tp7c]
double_eq2 [in PRFA.live_coding1]
double_eq [in PRFA.live_coding1]

E

epsilon_LEM [in PRFA.tp5c]
equivalence_eq_eq [in PRFA.tp7c]
equivalence_nat_even [in PRFA.tp7c]
equivalence_trans [in PRFA.tp7c]
equivalence_sym [in PRFA.tp7c]
equivalence_refl [in PRFA.tp7c]
equiv_ilist [in PRFA.tp8c]
eq_nat_spec [in PRFA.tp2c]
eq_dec [in PRFA.tp8c]
eq_nat_eq [in PRFA.tp8c]
eq_nat_spec [in PRFA.review2]
eq_dec [in PRFA.live_coding7]
eq_eq_nat [in PRFA.live_coding7]
eq_nat_eq [in PRFA.live_coding7]
eq_nat_false [in PRFA.tp7c]
eq_dec [in PRFA.tp7c]
eq_eq_nat [in PRFA.tp7c]
eq_nat_eq [in PRFA.tp7c]
eq_from_ts [in PRFA.tp7c]
eq_to_ts [in PRFA.tp7c]
evenb_to_even [in PRFA.live_coding2]
evenb_to_even [in PRFA.live_coding2]
evenSS_inv [in PRFA.live_coding7]
evenSS_inv [in PRFA.tp7c]
even_to_evenb [in PRFA.live_coding2]
even_plus_four_refine [in PRFA.live_coding3]
even_plus_four [in PRFA.live_coding3]
even_four [in PRFA.live_coding3]
even_double [in PRFA.tp7c]
even_and_S_False [in PRFA.tp7c]
even1_to_even2 [in PRFA.tp2c]
even2_iff_even3 [in PRFA.tp2c]
even2_iff_even3 [in PRFA.review2]
even3_to_even4 [in PRFA.tp2c]
even4_to_even1 [in PRFA.tp2c]
exercise_chain [in PRFA.live_coding5]
exercise_loop [in PRFA.live_coding5]
exp_from_nat [in PRFA.tp2c]

F

fact_equiv [in PRFA.tp2c]
falsefalse [in PRFA.live_coding1]
False_forall [in PRFA.tp1c]
fast_rev_eq_alt [in PRFA.tp2c]
fast_rev_eq [in PRFA.tp2c]
fast_rev_eq_alt [in PRFA.live_coding2]
fast_rev_eq [in PRFA.live_coding2]
fast_rev_eq [in PRFA.live_coding2]
FE_test_eq_stable [in PRFA.tp7c]
FE_stable_HF [in PRFA.tp7c]
Fib_Iter.fib_eq3 [in PRFA.tp2c]
Fib_Iter.fib_eq1 [in PRFA.tp2c]
Fib_Iter.fib_eq0 [in PRFA.tp2c]
fib_superlinear [in PRFA.tp5c]
filter_true [in PRFA.live_coding8]
foo [in PRFA.tp6c]
forall_or [in PRFA.tp1c]
forall_False' [in PRFA.tp1c]
forall_False [in PRFA.tp1c]
Forall_wpermut [in PRFA.tp5c]
Forall_set_eq [in PRFA.tp4c]
Forall_In [in PRFA.tp4c]
from_prop_bool_neg_PI [in PRFA.tp5c]
from_to_tree_alt [in PRFA.tp3c]
fun_choice_LEM [in PRFA.tp5c]
f_equal' [in PRFA.live_coding7]
f_equal' [in PRFA.tp7c]

G

good_tree_ind [in PRFA.live_coding5]
good_tree_ind' [in PRFA.live_coding5]
good_tree_ind [in PRFA.tp5c]
group_inverse_unique [in PRFA.tp4c]
group_neutral_unique [in PRFA.tp4c]
group_fact [in PRFA.tp4c]
G_zero [in PRFA.live_coding5]
G_sig [in PRFA.live_coding5]

H

Hedberg [in PRFA.tp7c]
Hedberg' [in PRFA.tp7c]
Heq_heq [in PRFA.tp7c]
heq_Heq [in PRFA.tp7c]
Hierarchy.embeds_refl [in PRFA.tp3c]
Hierarchy.hier [in PRFA.tp3c]
Hierarchy.hierarchy [in PRFA.tp3c]
Hierarchy.inconsistent [in PRFA.tp3c]
Hierarchy.sub_irrefl [in PRFA.tp3c]

I

iAnd_and [in PRFA.review3]
iAnd_iff [in PRFA.tp3c]
iEx_ex [in PRFA.review3]
iEx_iff [in PRFA.tp3c]
iFalse_iff [in PRFA.tp3c]
ilist_eq [in PRFA.tp8c]
imp_trans [in PRFA.tp1c]
inhabited_is_True [in PRFA.live_coding7]
inhabited_is_True [in PRFA.tp7c]
in_cons [in PRFA.review4]
in_add_left [in PRFA.review4]
in_add_right [in PRFA.review4]
In_iff [in PRFA.tp2c]
In_hd' [in PRFA.live_coding4]
In_4 [in PRFA.live_coding4]
In_tl [in PRFA.live_coding4]
In_hd [in PRFA.live_coding4]
In_app_inv [in PRFA.tp4c]
In_hd_eq [in PRFA.tp4c]
In_app_r [in PRFA.tp4c]
In_app_l [in PRFA.tp4c]
In_hd' [in PRFA.tp4c]
In_4 [in PRFA.tp4c]
In_tl [in PRFA.tp4c]
In_hd [in PRFA.tp4c]
iOr_iff [in PRFA.tp3c]
iter_shift [in PRFA.tp2c]
iter_pow [in PRFA.tp2c]
iter_mul [in PRFA.live_coding2]
iter_add [in PRFA.live_coding2]
iTrue_iff [in PRFA.tp3c]

L

lam_inv [in PRFA.tp8c]
Lawvere [in PRFA.tp7c]
leb_spec_alt [in PRFA.tp2c]
leb_spec [in PRFA.tp2c]
Leibniz.EqDef.eq_to_Leibniz [in PRFA.live_coding7]
Leibniz.EqDef.Leibniz_to_eq [in PRFA.live_coding7]
Leibniz.f_equal [in PRFA.live_coding7]
Leibniz.nat_discr [in PRFA.live_coding7]
Leibniz.nat_discr [in PRFA.tp7c]
Leibniz.n_plus_0 [in PRFA.live_coding7]
Leibniz.n_plus_0 [in PRFA.tp7c]
Leibniz.trans [in PRFA.live_coding7]
Leibniz2.all_equal_incl [in PRFA.tp7c]
Leibniz2.all_equal_implies_J [in PRFA.tp7c]
Leibniz2.J_implies_all_equal [in PRFA.tp7c]
Leibniz2.trans [in PRFA.tp7c]
lem_dns [in PRFA.tp1c]
lem_pl [in PRFA.tp1c]
length_to_list [in PRFA.tp8c]
le_equiv [in PRFA.tp2c]
le_n_S [in PRFA.tp2c]
le_0_n [in PRFA.tp2c]
le_rtclos [in PRFA.live_coding2]
le_trans [in PRFA.live_coding2]
le_iff [in PRFA.live_coding2]
le_n_S [in PRFA.review3]
le'_n_S [in PRFA.tp2c]
le'_refl [in PRFA.tp2c]
linear_search [in PRFA.live_coding5]
list_seq_eq_app [in PRFA.tp4c]
list_fact [in PRFA.tp4c]
lt_plus_4 [in PRFA.tp3c]

M

map_id' [in PRFA.live_coding7]
map_id' [in PRFA.live_coding7]
map_id [in PRFA.live_coding7]
map_id' [in PRFA.tp7c]
map_id' [in PRFA.tp7c]
map_id [in PRFA.tp7c]
memb_spec [in PRFA.tp4c]
merge_In [in PRFA.live_coding8]
merge_spec [in PRFA.tp5c]
merge_acc [in PRFA.tp5c]
min_comm [in PRFA.tp1c]
monoid_fact [in PRFA.live_coding4]
monoid_fact [in PRFA.tp4c]
mult_distr_lia [in PRFA.tp1c]
mult_distr [in PRFA.tp1c]
mult_comm [in PRFA.tp1c]
mult_S [in PRFA.tp1c]
mult_0 [in PRFA.tp1c]
mul_from_nat [in PRFA.tp2c]

N

nat_nat_fact [in PRFA.live_coding4]
nat_nat_fact [in PRFA.live_coding4]
nat_fact [in PRFA.live_coding4]
nat_ind_2 [in PRFA.tp5c]
nat_fact [in PRFA.tp4c]
nat_eqdec_eq [in PRFA.tp7c]
nat_bool [in PRFA.tp7c]
negb_invol [in PRFA.live_coding1]
negb_true [in PRFA.live_coding1]
neg_inv [in PRFA.live_coding8]
neg_inv [in PRFA.live_coding8]
neg_inv [in PRFA.live_coding8]
neg_inv [in PRFA.live_coding8]
neg_eq_False [in PRFA.tp7c]
neq_nat_neq [in PRFA.tp8c]
nofalse [in PRFA.tp1c]
nofalse [in PRFA.live_coding1]
not_even1 [in PRFA.tp7c]
n_plus_0 [in PRFA.tp1c]

O

of_nat_inj [in PRFA.tp2c]
one_zero_Z [in PRFA.tp4c]
or_imp [in PRFA.tp1c]
or_comm [in PRFA.tp1c]
or_com [in PRFA.tp4c]
or_AA [in PRFA.tp4c]
or_comm [in PRFA.live_coding1]

P

plus_assoc [in PRFA.tp1c]
plus_comm [in PRFA.tp1c]
plus_S [in PRFA.tp1c]
pl_lem [in PRFA.tp1c]
pneg_invol [in PRFA.live_coding5]
predext [in PRFA.tp7c]
pred_from_nat [in PRFA.tp2c]
pred'_from_nat [in PRFA.tp2c]
proof_irrelevance [in PRFA.live_coding7]
proof_irrelevance [in PRFA.tp7c]
P_iff_P [in PRFA.tp1c]
P_imp_P [in PRFA.tp1c]
P_eventually_implies_acc_ex [in PRFA.tp5c]
P_eventually_implies_acc [in PRFA.tp5c]
P_implies_acc [in PRFA.tp5c]
P_imp_P [in PRFA.live_coding1]

R

repeat_ind [in PRFA.tp8c]
rev_rev [in PRFA.tp2c]
rev_app_distr [in PRFA.tp2c]
rev_rev [in PRFA.live_coding2]
rev_app_distr [in PRFA.live_coding2]
rtclos_iff [in PRFA.tp2c]
rtclos'_trans [in PRFA.tp2c]
Russel [in PRFA.tp1c]
Russell [in PRFA.live_coding3]
R_step2 [in PRFA.tp5c]

S

sig_ext [in PRFA.tp7c]
SIP_UIP [in PRFA.tp7c]
size_recursion [in PRFA.live_coding5]
sorted_cons_inv [in PRFA.tp5c]
strong_nat_ind [in PRFA.tp2c]
strong_nat_ind [in PRFA.live_coding2]
strong_nat_ind [in PRFA.review2]
strong_nat_ind [in PRFA.tp5c]
stuck_vnil_inv [in PRFA.tp8c]
swap_invol [in PRFA.tp2c]
S_neq [in PRFA.tp3c]

T

test [in PRFA.live_coding6]
test_nat' [in PRFA.live_coding4]
test_monoid [in PRFA.live_coding4]
test_nat [in PRFA.live_coding4]
test_list [in PRFA.tp4c]
test_nat' [in PRFA.tp4c]
test_monoid [in PRFA.tp4c]
test_nat [in PRFA.tp4c]
test.DNE [in PRFA.tp6c]
to_nat_inj [in PRFA.tp2c]
to_not_not [in PRFA.tp1c]
to_tree_map [in PRFA.live_coding5]
to_bool_function_not_PI [in PRFA.live_coding5]
to_bool [in PRFA.live_coding5]
to_bool [in PRFA.live_coding5]
to_tree_map [in PRFA.tp5c]
to_sig_bool [in PRFA.tp5c]
to_exists [in PRFA.tp5c]
to_bool [in PRFA.tp5c]
to_prod_eq [in PRFA.tp4c]
to_from_tree [in PRFA.tp3c]
transportK [in PRFA.tp8c]
transport_vcons [in PRFA.tp8c]
tree_map_id_again' [in PRFA.live_coding5]
tree_map_id_again [in PRFA.live_coding5]
tree_map_id [in PRFA.live_coding5]
tree_map_id [in PRFA.tp5c]
truetrue [in PRFA.tp1c]
truetrue [in PRFA.live_coding1]
true_false [in PRFA.tp2c]
true_false [in PRFA.review3]
twice [in PRFA.tp1c]

U

UIP_for_nat [in PRFA.tp7c]
UIP_refl_nat [in PRFA.tp7c]
UIP_nat' [in PRFA.tp7c]
unit_neq_bool [in PRFA.live_coding7]
unit_neq_bool [in PRFA.tp7c]
Univalence_neg_UIP [in PRFA.tp7c]
univalence_equiv_equal [in PRFA.tp7c]

V

vec_expand [in PRFA.live_coding8]
vmap_ind [in PRFA.tp8c]
vnth_vmap [in PRFA.tp8c]
vnth_repeat [in PRFA.tp8c]
vnth_repeat [in PRFA.tp8c]

W

wpermut_app [in PRFA.tp5c]
wpermut_cons [in PRFA.tp5c]

Z

zip_vnth [in PRFA.live_coding8]

---

Constructor Index

A

Acc_intro [in PRFA.review6]
Acc_intro [in PRFA.live_coding5]
aConst [in PRFA.tp6c]
All_cons [in PRFA.tp3c]
All_nil [in PRFA.tp3c]
aPlus [in PRFA.tp6c]
aTimes [in PRFA.tp6c]

B

box [in PRFA.live_coding5]
bt_node [in PRFA.live_coding5]
bt_leaf [in PRFA.live_coding5]
bt_node [in PRFA.tp5c]
bt_leaf [in PRFA.tp5c]

C

C [in PRFA.live_coding3]
C [in PRFA.tp3c]
cons [in PRFA.review6]

D

define_nat.S [in PRFA.tp2c]
define_nat.O [in PRFA.tp2c]
define_sigma.existT [in PRFA.live_coding2]
define_list.cons [in PRFA.live_coding2]
define_list.nil [in PRFA.live_coding2]
define_prod.pair [in PRFA.live_coding2]
define_bool.false [in PRFA.live_coding2]
define_bool.true [in PRFA.live_coding2]
define_nat.variant2.S [in PRFA.live_coding2]
define_nat.variant2.O [in PRFA.live_coding2]
define_nat.variant1.S [in PRFA.live_coding2]
define_nat.variant1.O [in PRFA.live_coding2]
define_nat.S [in PRFA.live_coding2]
define_nat.O [in PRFA.live_coding2]

E

evenO [in PRFA.tp2c]
evenO [in PRFA.live_coding2]
evenO [in PRFA.live_coding3]
evenO [in PRFA.review3]
evenS [in PRFA.tp2c]
evenS [in PRFA.live_coding2]
evenS [in PRFA.live_coding3]
evenS [in PRFA.review3]
evenS [in PRFA.live_coding7]
evenS [in PRFA.tp7c]
even0 [in PRFA.live_coding7]
even0 [in PRFA.tp7c]

F

finS [in PRFA.tp8c]
finS [in PRFA.live_coding8]
fin0 [in PRFA.tp8c]
fin0 [in PRFA.live_coding8]

G

GI [in PRFA.live_coding5]

H

heq_refl [in PRFA.tp7c]
Hierarchy.T [in PRFA.tp3c]

I

incl [in PRFA.tp2c]
incl [in PRFA.live_coding2]
in_tl [in PRFA.tp2c]
in_hd [in PRFA.tp2c]

L

Leibniz.EqDef.eq_refl [in PRFA.live_coding7]
leO [in PRFA.live_coding2]
leO' [in PRFA.tp2c]
leS [in PRFA.live_coding2]
leS' [in PRFA.tp2c]
le_intro [in PRFA.tp5c]
lt_S [in PRFA.review3]
lt_B [in PRFA.review3]
lt_S [in PRFA.tp3c]
lt_B [in PRFA.tp3c]

M

mult4_plus [in PRFA.live_coding6]
mult4_0 [in PRFA.live_coding6]

N

N [in PRFA.live_coding3]
N [in PRFA.tp3c]
ncons [in PRFA.live_coding3]
ncons [in PRFA.tp3c]
nil [in PRFA.review6]
nlam [in PRFA.tp8c]
nnil [in PRFA.live_coding3]
nnil [in PRFA.tp3c]
nnode [in PRFA.live_coding3]
nnode [in PRFA.tp3c]
node [in PRFA.live_coding5]
node [in PRFA.tp5c]
not_mult4_plus [in PRFA.live_coding6]
not_mult4_3 [in PRFA.live_coding6]
not_mult4_2 [in PRFA.live_coding6]
not_mult4_1 [in PRFA.live_coding6]
nstar [in PRFA.tp8c]
nstuck [in PRFA.tp8c]
Nx [in PRFA.tp3c]

P

pfalse [in PRFA.live_coding5]
pfalse [in PRFA.tp5c]
ptrue [in PRFA.live_coding5]
ptrue [in PRFA.tp5c]

R

refl [in PRFA.tp2c]
refl [in PRFA.live_coding2]
refl_eq [in PRFA.tp7c]
refl' [in PRFA.tp2c]

S

sapp [in PRFA.tp8c]
Show_Definitions.or_intror [in PRFA.live_coding3]
Show_Definitions.or_introl [in PRFA.live_coding3]
Show_Definitions.conj [in PRFA.live_coding3]
Show_Definitions.I [in PRFA.live_coding3]
sorted_cons [in PRFA.tp5c]
sorted_nil [in PRFA.tp5c]
svar [in PRFA.tp8c]
sym_eq [in PRFA.tp7c]

T

tapp [in PRFA.tp8c]
tapp [in PRFA.live_coding8]
tarrow [in PRFA.tp8c]
tarrow [in PRFA.live_coding8]
tlam [in PRFA.tp8c]
tlam [in PRFA.live_coding8]
trans [in PRFA.tp2c]
trans [in PRFA.live_coding2]
trans_eq [in PRFA.tp7c]
trans' [in PRFA.tp2c]
tstar [in PRFA.tp8c]
tstar [in PRFA.live_coding8]
tunit [in PRFA.tp8c]
tunit [in PRFA.live_coding8]
tvar [in PRFA.tp8c]
tvar [in PRFA.live_coding8]

V

vcons [in PRFA.tp8c]
vcons [in PRFA.live_coding8]
vnil [in PRFA.tp8c]
vnil [in PRFA.live_coding8]

---

Axiom Index

D

DNE [in PRFA.live_coding4]

F

funext [in PRFA.live_coding7]
funext [in PRFA.tp6c]
funext [in PRFA.tp7c]

K

K [in PRFA.tp8c]

L

LEM [in PRFA.tp6c]

M

mystery [in PRFA.tp6c]

P

propext [in PRFA.live_coding7]
propext [in PRFA.tp7c]

R

random [in PRFA.tp6c]
REPLACE_ME [in PRFA.tp8c]

U

unkown [in PRFA.tp6c]

---

Inductive Index

A

Acc [in PRFA.review6]
Acc [in PRFA.live_coding5]
All [in PRFA.tp3c]
arith [in PRFA.tp6c]

B

bad [in PRFA.live_coding3]
bad [in PRFA.tp3c]
bintree [in PRFA.live_coding5]
bintree [in PRFA.tp5c]
Box [in PRFA.live_coding5]

D

define_nat.nat [in PRFA.tp2c]
define_sigma.sigT [in PRFA.live_coding2]
define_list.list [in PRFA.live_coding2]
define_prod.prod [in PRFA.live_coding2]
define_bool.bool [in PRFA.live_coding2]
define_nat.variant2.nat [in PRFA.live_coding2]
define_nat.variant1.nat [in PRFA.live_coding2]
define_nat.nat [in PRFA.live_coding2]

E

eq_ts [in PRFA.tp7c]
even [in PRFA.live_coding2]
even [in PRFA.live_coding3]
even [in PRFA.review3]
even [in PRFA.live_coding7]
even [in PRFA.tp7c]
even4 [in PRFA.tp2c]

F

fin [in PRFA.tp8c]
fin [in PRFA.live_coding8]

G

G [in PRFA.live_coding5]

H

Heq [in PRFA.tp7c]
Hierarchy.tree [in PRFA.tp3c]

I

In_i [in PRFA.tp2c]

L

le [in PRFA.live_coding2]
Leibniz.EqDef.eq [in PRFA.live_coding7]
le' [in PRFA.tp2c]
le' [in PRFA.tp5c]
list [in PRFA.review6]
lt [in PRFA.review3]
lt [in PRFA.tp3c]

M

mult4 [in PRFA.live_coding6]

N

nforest [in PRFA.live_coding3]
nforest [in PRFA.tp3c]
normal [in PRFA.tp8c]
not_mult4 [in PRFA.live_coding6]
ntree [in PRFA.live_coding3]
ntree [in PRFA.tp3c]

P

prop_bool [in PRFA.live_coding5]
prop_bool [in PRFA.tp5c]

R

rtclos [in PRFA.tp2c]
rtclos [in PRFA.live_coding2]
rtclos' [in PRFA.tp2c]

S

Show_Definitions.or [in PRFA.live_coding3]
Show_Definitions.and [in PRFA.live_coding3]
Show_Definitions.True [in PRFA.live_coding3]
Show_Definitions.False [in PRFA.live_coding3]
sorted [in PRFA.tp5c]
stuck [in PRFA.tp8c]

T

term [in PRFA.tp8c]
term [in PRFA.live_coding8]
tree [in PRFA.live_coding5]
tree [in PRFA.live_coding3]
tree [in PRFA.tp5c]
tree [in PRFA.tp3c]
type [in PRFA.tp8c]
type [in PRFA.live_coding8]

V

vec [in PRFA.tp8c]
vec [in PRFA.live_coding8]

X

xtree [in PRFA.tp3c]

---

Projection Index

D

denominator [in PRFA.live_coding4]
denominator' [in PRFA.live_coding4]
denominator'' [in PRFA.live_coding4]
den_not_zero [in PRFA.live_coding4]

E

eqb [in PRFA.live_coding4]
eqb [in PRFA.tp4c]
eqb_iff [in PRFA.live_coding4]
eqb_iff [in PRFA.tp4c]

F

fst' [in PRFA.review4]
fst' [in PRFA.live_coding4]
fst' [in PRFA.tp4c]

G

group_inv [in PRFA.tp4c]
group_assoc [in PRFA.tp4c]
group_right_neutral [in PRFA.tp4c]
group_left_neutral [in PRFA.tp4c]
g_inv [in PRFA.tp4c]
g_mon [in PRFA.tp4c]

L

l_to_l [in PRFA.tp8c]
l_to_r [in PRFA.tp8c]

M

mon_assoc [in PRFA.live_coding4]
mon_right_neutral [in PRFA.live_coding4]
mon_left_neutral [in PRFA.live_coding4]
mon_assoc [in PRFA.tp4c]
mon_right_neutral [in PRFA.tp4c]
mon_left_neutral [in PRFA.tp4c]
m_assoc [in PRFA.live_coding4]
m_r_ne [in PRFA.live_coding4]
m_l_ne [in PRFA.live_coding4]
m_op [in PRFA.live_coding4]
m_ne [in PRFA.live_coding4]
m_ty [in PRFA.live_coding4]
m_assoc [in PRFA.tp4c]
m_r_ne [in PRFA.tp4c]
m_l_ne [in PRFA.tp4c]
m_op [in PRFA.tp4c]
m_ne [in PRFA.tp4c]
m_ty [in PRFA.tp4c]

N

num [in PRFA.tp6c]
numerator [in PRFA.live_coding4]
numerator' [in PRFA.live_coding4]
numerator'' [in PRFA.live_coding4]

P

positive [in PRFA.tp6c]
px [in PRFA.tp6c]
py [in PRFA.tp6c]
pz [in PRFA.tp6c]
p1 [in PRFA.tp6c]
p2 [in PRFA.tp6c]
p3 [in PRFA.tp6c]

R

r_to_r [in PRFA.tp8c]
r_to_l [in PRFA.tp8c]

S

snd' [in PRFA.review4]
snd' [in PRFA.live_coding4]
snd' [in PRFA.tp4c]

V

v1 [in PRFA.tp6c]
v2 [in PRFA.tp6c]
v3 [in PRFA.tp6c]

---

Section Index

A

Advanced [in PRFA.tp1c]
assums [in PRFA.tp6c]

C

ConstructiveIndefiniteGroundDescription_Acc [in PRFA.tp5c]

D

Demo [in PRFA.live_coding3]

H

Hilbert [in PRFA.tp5c]

L

Live [in PRFA.live_coding1]

M

Merge [in PRFA.tp5c]

T

Tauto [in PRFA.tp6c]
TP1 [in PRFA.tp1c]

U

Universes [in PRFA.live_coding5]

W

Well_founded [in PRFA.live_coding5]
WO [in PRFA.live_coding5]

---

Instance Index

E

Eq_nat [in PRFA.live_coding4]
Eq_nat [in PRFA.tp4c]

G

Group_Z [in PRFA.tp4c]

L

list_set_eq_trans [in PRFA.tp4c]
list_set_eq_sym [in PRFA.tp4c]
list_set_eq_refl [in PRFA.tp4c]

M

MonoidList [in PRFA.tp4c]
MonoidNat [in PRFA.live_coding4]
MonoidNat [in PRFA.tp4c]
MonoidProd [in PRFA.live_coding4]
MonoidProd [in PRFA.tp4c]
Monoid_Group [in PRFA.tp4c]

W

wpermut_trans [in PRFA.tp5c]
wpermut_sym [in PRFA.tp5c]
wpermut_refl [in PRFA.tp5c]

---

Abbreviation Index

A

acc [in PRFA.tp5c]

T

tLam [in PRFA.MetaCoqPrelude]
tLet [in PRFA.MetaCoqPrelude]

---

Definition Index

A

Acc_sind [in PRFA.review6]
Acc_ind [in PRFA.review6]
Acc_sind [in PRFA.live_coding5]
Acc_rec [in PRFA.live_coding5]
Acc_ind [in PRFA.live_coding5]
Acc_rect [in PRFA.live_coding5]
add [in PRFA.tp2c]
add [in PRFA.live_coding3]
add' [in PRFA.review7]
all_equal [in PRFA.live_coding7]
all_equal [in PRFA.tp7c]
All_sind [in PRFA.tp3c]
All_rec [in PRFA.tp3c]
All_ind [in PRFA.tp3c]
All_rect [in PRFA.tp3c]
app [in PRFA.live_coding8]
arith_sind [in PRFA.tp6c]
arith_rec [in PRFA.tp6c]
arith_ind [in PRFA.tp6c]
arith_rect [in PRFA.tp6c]
assms [in PRFA.tp6c]
assumptions [in PRFA.tp6c]
assumptions_alt [in PRFA.tp6c]
assum_fold [in PRFA.tp6c]

B

bar [in PRFA.live_coding3]
bar [in PRFA.tp6c]
baz [in PRFA.live_coding3]
below [in PRFA.tp3c]
bintree_sind [in PRFA.live_coding5]
bintree_rec [in PRFA.live_coding5]
bintree_ind [in PRFA.live_coding5]
bintree_rect [in PRFA.live_coding5]
bintree_sind [in PRFA.tp5c]
bintree_rec [in PRFA.tp5c]
bintree_ind [in PRFA.tp5c]
bintree_rect [in PRFA.tp5c]
Box_sind [in PRFA.live_coding5]
Box_rec [in PRFA.live_coding5]
Box_ind [in PRFA.live_coding5]
Box_rect [in PRFA.live_coding5]
brec [in PRFA.tp3c]
brec' [in PRFA.tp3c]
bt_to_tree [in PRFA.live_coding5]
bt_map [in PRFA.live_coding5]
bt_to_tree [in PRFA.tp5c]
bt_map [in PRFA.tp5c]

C

car [in PRFA.tp2c]
car [in PRFA.live_coding2]
car' [in PRFA.tp2c]
car'' [in PRFA.tp2c]
count [in PRFA.live_coding3]
count [in PRFA.tp3c]
count_list [in PRFA.live_coding3]
count_list [in PRFA.tp3c]
cur [in PRFA.tp2c]
cur [in PRFA.live_coding2]

D

debug_derive_updates [in PRFA.tp6c]
debug_def_list [in PRFA.tp6c]
define_nat.sub [in PRFA.tp2c]
define_nat.add [in PRFA.tp2c]
define_nat.nat_sind [in PRFA.tp2c]
define_nat.nat_rec [in PRFA.tp2c]
define_nat.nat_ind [in PRFA.tp2c]
define_nat.nat_rect [in PRFA.tp2c]
define_sigma.pair2 [in PRFA.live_coding2]
define_sigma.pair1 [in PRFA.live_coding2]
define_sigma.T [in PRFA.live_coding2]
define_sigma.sigT_sind [in PRFA.live_coding2]
define_sigma.sigT_rec [in PRFA.live_coding2]
define_sigma.sigT_ind [in PRFA.live_coding2]
define_sigma.sigT_rect [in PRFA.live_coding2]
define_list.list_sind [in PRFA.live_coding2]
define_list.list_rec [in PRFA.live_coding2]
define_list.list_ind [in PRFA.live_coding2]
define_list.list_rect [in PRFA.live_coding2]
define_prod.snd [in PRFA.live_coding2]
define_prod.fst [in PRFA.live_coding2]
define_prod.pair' [in PRFA.live_coding2]
define_prod.prod_sind [in PRFA.live_coding2]
define_prod.prod_rec [in PRFA.live_coding2]
define_prod.prod_ind [in PRFA.live_coding2]
define_prod.prod_rect [in PRFA.live_coding2]
define_bool.bool_sind [in PRFA.live_coding2]
define_bool.bool_rec [in PRFA.live_coding2]
define_bool.bool_ind [in PRFA.live_coding2]
define_bool.bool_rect [in PRFA.live_coding2]
define_nat.eq_nat [in PRFA.live_coding2]
define_nat.pred [in PRFA.live_coding2]
define_nat.is_zero [in PRFA.live_coding2]
define_nat.is_zerob [in PRFA.live_coding2]
define_nat.sub [in PRFA.live_coding2]
define_nat.add [in PRFA.live_coding2]
define_nat.variant2.nat_sind [in PRFA.live_coding2]
define_nat.variant2.nat_rec [in PRFA.live_coding2]
define_nat.variant2.nat_ind [in PRFA.live_coding2]
define_nat.variant2.nat_rect [in PRFA.live_coding2]
define_nat.variant1.nat_sind [in PRFA.live_coding2]
define_nat.variant1.nat_rec [in PRFA.live_coding2]
define_nat.variant1.nat_ind [in PRFA.live_coding2]
define_nat.variant1.nat_rect [in PRFA.live_coding2]
define_nat.nat_sind [in PRFA.live_coding2]
define_nat.nat_rec [in PRFA.live_coding2]
define_nat.nat_ind [in PRFA.live_coding2]
define_nat.nat_rect [in PRFA.live_coding2]
def_list [in PRFA.tp6c]
dependent [in PRFA.live_coding3]
derive_updates [in PRFA.tp6c]
div2 [in PRFA.tp7c]
DNS [in PRFA.tp1c]
double [in PRFA.live_coding1]
double_S [in PRFA.live_coding6]

E

elim_or [in PRFA.live_coding3]
elim_and [in PRFA.live_coding3]
elim_False [in PRFA.live_coding3]
empty_tree [in PRFA.live_coding3]
env [in PRFA.tp8c]
env [in PRFA.live_coding8]
equal [in PRFA.live_coding8]
equivalence [in PRFA.tp7c]
equivalence_neg_bool [in PRFA.tp7c]
eq_nat [in PRFA.tp2c]
eq_dec_term [in PRFA.tp8c]
eq_nat [in PRFA.tp8c]
eq_nat [in PRFA.review2]
eq_nat [in PRFA.live_coding7]
eq_trans' [in PRFA.live_coding7]
eq_trans' [in PRFA.live_coding7]
eq_sym' [in PRFA.live_coding7]
eq_trans [in PRFA.live_coding7]
eq_sym [in PRFA.live_coding7]
eq_dec_term [in PRFA.tp7c]
eq_nat [in PRFA.tp7c]
eq_ts_sind [in PRFA.tp7c]
eq_ts_ind [in PRFA.tp7c]
eq_trans' [in PRFA.tp7c]
eq_sym' [in PRFA.tp7c]
eq_trans [in PRFA.tp7c]
eq_sym [in PRFA.tp7c]
eval [in PRFA.tp8c]
evenb [in PRFA.live_coding2]
evenSS_inv_alt [in PRFA.live_coding7]
evenSS_inv_alt [in PRFA.tp7c]
even_sind [in PRFA.live_coding2]
even_ind [in PRFA.live_coding2]
even_plus_four_term [in PRFA.live_coding3]
even_four' [in PRFA.live_coding3]
even_sind [in PRFA.live_coding3]
even_ind [in PRFA.live_coding3]
even_sind [in PRFA.review3]
even_ind [in PRFA.review3]
even_sind [in PRFA.live_coding7]
even_ind [in PRFA.live_coding7]
even_sind [in PRFA.tp7c]
even_ind [in PRFA.tp7c]
even1 [in PRFA.tp2c]
even2 [in PRFA.tp2c]
even2 [in PRFA.review2]
even3 [in PRFA.tp2c]
even3 [in PRFA.review2]
even4_sind [in PRFA.tp2c]
even4_ind [in PRFA.tp2c]
exfalso' [in PRFA.live_coding5]
exfalso' [in PRFA.tp5c]
exists_unique [in PRFA.tp7c]
exp [in PRFA.tp2c]
extend [in PRFA.tp8c]
extend [in PRFA.live_coding8]
ex1 [in PRFA.tp3c]
ex2 [in PRFA.tp3c]
ex3 [in PRFA.tp3c]
ex3_alt [in PRFA.tp3c]
ex4 [in PRFA.tp3c]

F

f [in PRFA.live_coding3]
f [in PRFA.tp3c]
fact_iter [in PRFA.tp2c]
fact_iter_f [in PRFA.tp2c]
fact_fix [in PRFA.tp2c]
fast_rev [in PRFA.tp2c]
fast_rev [in PRFA.live_coding2]
fib [in PRFA.tp5c]
fib [in PRFA.tp3c]
Fib_Iter.fib [in PRFA.tp2c]
Fib_Iter.sigma [in PRFA.tp2c]
fib_brec [in PRFA.tp3c]
fib_natrec [in PRFA.tp3c]
filter [in PRFA.live_coding8]
fin_sind [in PRFA.tp8c]
fin_rec [in PRFA.tp8c]
fin_ind [in PRFA.tp8c]
fin_rect [in PRFA.tp8c]
fin_sind [in PRFA.live_coding8]
fin_rec [in PRFA.live_coding8]
fin_ind [in PRFA.live_coding8]
fin_rect [in PRFA.live_coding8]
fold_def [in PRFA.MetaCoqPrelude]
fold_branches [in PRFA.MetaCoqPrelude]
fold_branch [in PRFA.MetaCoqPrelude]
fold_predicate [in PRFA.MetaCoqPrelude]
fold_handler [in PRFA.MetaCoqPrelude]
fold_muladd_alt [in PRFA.tp6c]
fold_muladd [in PRFA.tp6c]
foo [in PRFA.live_coding3]
foo [in PRFA.live_coding4]
foo [in PRFA.tp4c]
foo_env [in PRFA.tp6c]
from_nat [in PRFA.tp2c]
from_mind [in PRFA.tp6c]
from_ctor [in PRFA.tp6c]
from_arg [in PRFA.tp6c]
from_to_tree_list [in PRFA.tp3c]
from_to_tree [in PRFA.tp3c]
from_tree_list [in PRFA.tp3c]
from_tree [in PRFA.tp3c]
FunctionExtensionality [in PRFA.tp7c]
FunExt [in PRFA.tp5c]
FunExt [in PRFA.live_coding7]
FunExt [in PRFA.tp7c]
fun_choice [in PRFA.tp5c]
f_equal'' [in PRFA.live_coding7]
f_equal_term' [in PRFA.tp7c]
f_equal_term [in PRFA.tp7c]
f_equal [in PRFA.review7]

G

get_kername [in PRFA.MetaCoqPrelude]
get_inductive' [in PRFA.tp6c]
get_name [in PRFA.tp6c]
get_inductive [in PRFA.tp6c]
G_sind [in PRFA.live_coding5]
G_rec [in PRFA.live_coding5]
G_ind [in PRFA.live_coding5]
G_rect [in PRFA.live_coding5]

H

half [in PRFA.live_coding4]
half' [in PRFA.live_coding4]
has_body [in PRFA.tp6c]
hd [in PRFA.tp8c]
head [in PRFA.tp8c]
head [in PRFA.live_coding8]
head' [in PRFA.live_coding8]
heq [in PRFA.tp7c]
Heq_sind [in PRFA.tp7c]
Heq_rec [in PRFA.tp7c]
Heq_ind [in PRFA.tp7c]
Heq_rect [in PRFA.tp7c]
HF [in PRFA.tp7c]
Hierarchy.embeds [in PRFA.tp3c]
Hierarchy.sub [in PRFA.tp3c]
Hierarchy.tree_sind [in PRFA.tp3c]
Hierarchy.tree_rec [in PRFA.tp3c]
Hierarchy.tree_ind [in PRFA.tp3c]
Hierarchy.tree_rect [in PRFA.tp3c]
Hierarchy.Tyi [in PRFA.tp3c]

I

iAnd [in PRFA.review3]
iAnd [in PRFA.tp3c]
identity [in PRFA.tp6c]
idNat [in PRFA.live_coding6]
idnat [in PRFA.tp3c]
idren [in PRFA.tp8c]
idval [in PRFA.tp8c]
iEx [in PRFA.review3]
iEx [in PRFA.tp3c]
iFalse [in PRFA.review3]
iFalse [in PRFA.tp3c]
ilist [in PRFA.tp8c]
In [in PRFA.tp2c]
instantiate_axiom [in PRFA.tp6c]
interp [in PRFA.live_coding8]
interp_type [in PRFA.live_coding8]
In_i_sind [in PRFA.tp2c]
In_i_ind [in PRFA.tp2c]
iOr [in PRFA.tp3c]
isEquiv [in PRFA.tp7c]
isnil [in PRFA.tp8c]
iter [in PRFA.tp2c]
iter [in PRFA.live_coding2]
iTrue [in PRFA.tp3c]

J

J [in PRFA.tp7c]

K

K [in PRFA.tp7c]
K_UIP [in PRFA.tp7c]

L

least [in PRFA.live_coding5]
leb [in PRFA.tp2c]
leibniz_sym [in PRFA.review7]
Leibniz.EqDef.eq_sind [in PRFA.live_coding7]
Leibniz.EqDef.eq_rec [in PRFA.live_coding7]
Leibniz.EqDef.eq_ind [in PRFA.live_coding7]
Leibniz.EqDef.eq_rect [in PRFA.live_coding7]
Leibniz.eq_to_leib [in PRFA.tp7c]
Leibniz.f_equal [in PRFA.tp7c]
Leibniz.leib_eq [in PRFA.live_coding7]
Leibniz.leib_to_eq [in PRFA.tp7c]
Leibniz.leib_eq [in PRFA.tp7c]
Leibniz.refl [in PRFA.live_coding7]
Leibniz.refl [in PRFA.tp7c]
Leibniz.sym [in PRFA.live_coding7]
Leibniz.sym [in PRFA.tp7c]
Leibniz.trans [in PRFA.tp7c]
Leibniz2.all_equal [in PRFA.tp7c]
Leibniz2.incl [in PRFA.tp7c]
Leibniz2.J_prop [in PRFA.tp7c]
Leibniz2.leib_eq [in PRFA.tp7c]
Leibniz2.refl [in PRFA.tp7c]
Leibniz2.singleton [in PRFA.tp7c]
Leibniz2.sym [in PRFA.tp7c]
LEM [in PRFA.tp1c]
le_sind [in PRFA.live_coding2]
le_ind [in PRFA.live_coding2]
le_dec [in PRFA.tp5c]
le_alt [in PRFA.tp5c]
le'_sind [in PRFA.tp2c]
le'_ind [in PRFA.tp2c]
le'_sind [in PRFA.tp5c]
le'_rec [in PRFA.tp5c]
le'_ind [in PRFA.tp5c]
le'_rect [in PRFA.tp5c]
list_sind [in PRFA.review6]
list_rec [in PRFA.review6]
list_ind [in PRFA.review6]
list_rect [in PRFA.review6]
list_rect [in PRFA.live_coding3]
list_set_eq [in PRFA.tp4c]
list_monoid [in PRFA.tp4c]
lt_plus_4' [in PRFA.review3]
lt_plus_4 [in PRFA.review3]
lt_sind [in PRFA.review3]
lt_ind [in PRFA.review3]
lt_plus_4' [in PRFA.tp3c]
lt_sind [in PRFA.tp3c]
lt_ind [in PRFA.tp3c]

M

map [in PRFA.live_coding7]
map [in PRFA.tp7c]
memb [in PRFA.live_coding4]
memb [in PRFA.tp4c]
merge [in PRFA.live_coding8]
merge [in PRFA.live_coding8]
merge [in PRFA.tp5c]
merge [in PRFA.tp5c]
min [in PRFA.tp1c]
mkargs [in PRFA.tp6c]
mkargs_aux [in PRFA.tp6c]
mkr [in PRFA.tp6c]
more_deps [in PRFA.tp6c]
mpow [in PRFA.live_coding6]
mpow' [in PRFA.live_coding6]
mul [in PRFA.tp2c]
muladd [in PRFA.tp6c]
muladd_handler [in PRFA.tp6c]
mult4_sind [in PRFA.live_coding6]
mult4_ind [in PRFA.live_coding6]

N

nat_rect [in PRFA.live_coding3]
nat_monoid [in PRFA.live_coding4]
nat_monoid [in PRFA.tp4c]
nbe [in PRFA.tp8c]
neg [in PRFA.live_coding8]
nforest_sind [in PRFA.live_coding3]
nforest_rec [in PRFA.live_coding3]
nforest_ind [in PRFA.live_coding3]
nforest_rect [in PRFA.live_coding3]
nforest_ntree_rec [in PRFA.tp3c]
nforest_map [in PRFA.tp3c]
nforest_sind [in PRFA.tp3c]
nforest_rec [in PRFA.tp3c]
nforest_ind [in PRFA.tp3c]
nforest_rect [in PRFA.tp3c]
normal_sind [in PRFA.tp8c]
normal_rec [in PRFA.tp8c]
normal_ind [in PRFA.tp8c]
normal_rect [in PRFA.tp8c]
not_mult4_sind [in PRFA.live_coding6]
not_mult4_ind [in PRFA.live_coding6]
not_even1_term [in PRFA.tp7c]
nren [in PRFA.tp8c]
ntree_sind [in PRFA.live_coding3]
ntree_rec [in PRFA.live_coding3]
ntree_ind [in PRFA.live_coding3]
ntree_rect [in PRFA.live_coding3]
ntree_nforest_rec [in PRFA.tp3c]
ntree_map [in PRFA.tp3c]
ntree_sind [in PRFA.tp3c]
ntree_rec [in PRFA.tp3c]
ntree_ind [in PRFA.tp3c]
ntree_rect [in PRFA.tp3c]
num [in PRFA.tp2c]

O

of_nat [in PRFA.tp2c]
or_imp [in PRFA.review3]
or_comm [in PRFA.tp3c]

P

PI [in PRFA.live_coding5]
PI_UIP [in PRFA.live_coding7]
PI_UIP [in PRFA.tp7c]
PL [in PRFA.tp1c]
pneg [in PRFA.live_coding5]
pow13 [in PRFA.live_coding6]
pow3 [in PRFA.live_coding6]
pow5 [in PRFA.live_coding6]
pred [in PRFA.tp2c]
pred' [in PRFA.tp2c]
prod_monoid [in PRFA.live_coding4]
prod_monoid [in PRFA.tp4c]
prod'_ind [in PRFA.review4]
ProofIrrelevance [in PRFA.live_coding7]
ProofIrrelevance [in PRFA.tp7c]
PropExt [in PRFA.tp5c]
PropExt [in PRFA.live_coding7]
PropExt [in PRFA.tp7c]
prop_bool_sind [in PRFA.live_coding5]
prop_bool_ind [in PRFA.live_coding5]
prop_bool_sind [in PRFA.tp5c]
prop_bool_ind [in PRFA.tp5c]

Q

quarter [in PRFA.live_coding4]
quarter'' [in PRFA.live_coding4]
q_upd_num [in PRFA.tp6c]
q_foo [in PRFA.tp6c]

R

reflect [in PRFA.tp8c]
reify [in PRFA.tp8c]
reify [in PRFA.tp6c]
ren [in PRFA.tp8c]
rencomp [in PRFA.tp8c]
renval [in PRFA.tp8c]
repeat [in PRFA.tp8c]
REPLACE_ME [in PRFA.tp1c]
replace_const_lift [in PRFA.tp6c]
rev_acc [in PRFA.tp8c]
rho0 [in PRFA.live_coding8]
rtclos_sind [in PRFA.tp2c]
rtclos_ind [in PRFA.tp2c]
rtclos_sind [in PRFA.live_coding2]
rtclos_ind [in PRFA.live_coding2]
rtclos'_sind [in PRFA.tp2c]
rtclos'_ind [in PRFA.tp2c]
Russel [in PRFA.review3]
Russel [in PRFA.review3]
Russel [in PRFA.tp3c]

S

sem [in PRFA.tp8c]
semren [in PRFA.tp8c]
Show_Definitions.or_sind [in PRFA.live_coding3]
Show_Definitions.or_ind [in PRFA.live_coding3]
Show_Definitions.and_sind [in PRFA.live_coding3]
Show_Definitions.and_rec [in PRFA.live_coding3]
Show_Definitions.and_ind [in PRFA.live_coding3]
Show_Definitions.and_rect [in PRFA.live_coding3]
Show_Definitions.True_sind [in PRFA.live_coding3]
Show_Definitions.True_rec [in PRFA.live_coding3]
Show_Definitions.True_ind [in PRFA.live_coding3]
Show_Definitions.True_rect [in PRFA.live_coding3]
Show_Definitions.False_sind [in PRFA.live_coding3]
Show_Definitions.False_rec [in PRFA.live_coding3]
Show_Definitions.False_ind [in PRFA.live_coding3]
Show_Definitions.False_rect [in PRFA.live_coding3]
some_tree [in PRFA.live_coding3]
some_other_pair [in PRFA.live_coding4]
some_pair [in PRFA.live_coding4]
some_other_pair [in PRFA.tp4c]
some_pair [in PRFA.tp4c]
sorted_sind [in PRFA.tp5c]
sorted_ind [in PRFA.tp5c]
split_two [in PRFA.live_coding8]
sren [in PRFA.tp8c]
stable [in PRFA.tp7c]
stuck_sind [in PRFA.tp8c]
stuck_rec [in PRFA.tp8c]
stuck_ind [in PRFA.tp8c]
stuck_rect [in PRFA.tp8c]
succ [in PRFA.tp2c]
sval [in PRFA.tp8c]
swap [in PRFA.tp2c]

T

T [in PRFA.live_coding3]
tail [in PRFA.tp8c]
tail [in PRFA.live_coding8]
tail' [in PRFA.live_coding8]
term_eqb [in PRFA.MetaCoqPrelude]
term_sind [in PRFA.tp8c]
term_rec [in PRFA.tp8c]
term_ind [in PRFA.tp8c]
term_rect [in PRFA.tp8c]
term_sind [in PRFA.live_coding8]
term_rec [in PRFA.live_coding8]
term_ind [in PRFA.live_coding8]
term_rect [in PRFA.live_coding8]
test [in PRFA.tp8c]
test [in PRFA.live_coding8]
test [in PRFA.tp6c]
test' [in PRFA.live_coding8]
theDNS [in PRFA.tp1c]
theLEM [in PRFA.tp1c]
thePL [in PRFA.tp1c]
tid [in PRFA.tp8c]
tl [in PRFA.tp8c]
tmDebugDefinition [in PRFA.tp6c]
tm_fold [in PRFA.MetaCoqPrelude]
tm_nb_handler [in PRFA.MetaCoqPrelude]
tm_handler [in PRFA.MetaCoqPrelude]
tNat [in PRFA.live_coding6]
to_nat [in PRFA.tp2c]
to_nat' [in PRFA.tp2c]
to_vec [in PRFA.tp8c]
to_list [in PRFA.tp8c]
to_ilist [in PRFA.tp8c]
to_bool [in PRFA.live_coding5]
to_prop_bool [in PRFA.live_coding5]
to_prod_alt3 [in PRFA.live_coding4]
to_prod_alt2 [in PRFA.live_coding4]
to_prod_alt [in PRFA.live_coding4]
to_prod [in PRFA.live_coding4]
to_disj [in PRFA.tp5c]
to_prop_bool [in PRFA.tp5c]
to_prod_alt3 [in PRFA.tp4c]
to_prod_alt2 [in PRFA.tp4c]
to_prod_alt [in PRFA.tp4c]
to_prod [in PRFA.tp4c]
to_equiv [in PRFA.tp7c]
to_tree_list [in PRFA.tp3c]
to_tree [in PRFA.tp3c]
transform [in PRFA.MetaCoqPrelude]
transform_nb [in PRFA.MetaCoqPrelude]
transport [in PRFA.tp8c]
transport [in PRFA.tp5c]
transport [in PRFA.live_coding7]
transport [in PRFA.tp7c]
tree_map_id [in PRFA.live_coding5]
tree_map [in PRFA.live_coding5]
tree_sind [in PRFA.live_coding5]
tree_rec [in PRFA.live_coding5]
tree_ind [in PRFA.live_coding5]
tree_rect [in PRFA.live_coding5]
tree_sind [in PRFA.live_coding3]
tree_rec [in PRFA.live_coding3]
tree_ind [in PRFA.live_coding3]
tree_rect [in PRFA.live_coding3]
tree_map [in PRFA.tp5c]
tree_sind [in PRFA.tp5c]
tree_rec [in PRFA.tp5c]
tree_ind [in PRFA.tp5c]
tree_rect [in PRFA.tp5c]
tree_rect_strong [in PRFA.tp3c]
tree_sind [in PRFA.tp3c]
tree_rec [in PRFA.tp3c]
tree_ind [in PRFA.tp3c]
tree_rect [in PRFA.tp3c]
type_sind [in PRFA.tp8c]
type_rec [in PRFA.tp8c]
type_ind [in PRFA.tp8c]
type_rect [in PRFA.tp8c]
type_sind [in PRFA.live_coding8]
type_rec [in PRFA.live_coding8]
type_ind [in PRFA.live_coding8]
type_rect [in PRFA.live_coding8]

U

UIP [in PRFA.live_coding7]
UIP [in PRFA.tp7c]
UIP_for [in PRFA.tp7c]
UIP_K [in PRFA.tp7c]
unaxiom [in PRFA.tp6c]
unfold_toplevel [in PRFA.MetaCoqPrelude]
unit_bool [in PRFA.tp7c]
Univalence [in PRFA.tp7c]
Unnamed_thm2 [in PRFA.live_coding6]
Unnamed_thm1 [in PRFA.live_coding6]
Unnamed_thm1 [in PRFA.live_coding6]
Unnamed_thm0 [in PRFA.live_coding6]
Unnamed_thm [in PRFA.live_coding6]
Unnamed_thm1 [in PRFA.review4]
Unnamed_thm0 [in PRFA.review4]
Unnamed_thm [in PRFA.review4]
Unnamed_thm [in PRFA.review6]
Unnamed_thm [in PRFA.review6]
Unnamed_thm [in PRFA.review6]
Unnamed_thm4 [in PRFA.live_coding2]
Unnamed_thm3 [in PRFA.live_coding2]
Unnamed_thm2 [in PRFA.live_coding2]
Unnamed_thm1 [in PRFA.live_coding2]
Unnamed_thm1 [in PRFA.live_coding2]
Unnamed_thm0 [in PRFA.live_coding2]
Unnamed_thm [in PRFA.live_coding2]
Unnamed_thm2 [in PRFA.live_coding5]
Unnamed_thm2 [in PRFA.live_coding5]
Unnamed_thm1 [in PRFA.live_coding5]
Unnamed_thm0 [in PRFA.live_coding5]
Unnamed_thm [in PRFA.live_coding5]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm6 [in PRFA.live_coding3]
Unnamed_thm5 [in PRFA.live_coding3]
Unnamed_thm4 [in PRFA.live_coding3]
Unnamed_thm3 [in PRFA.live_coding3]
Unnamed_thm2 [in PRFA.live_coding3]
Unnamed_thm1 [in PRFA.live_coding3]
Unnamed_thm0 [in PRFA.live_coding3]
Unnamed_thm [in PRFA.live_coding3]
Unnamed_thm2 [in PRFA.live_coding4]
Unnamed_thm1 [in PRFA.live_coding4]
Unnamed_thm0 [in PRFA.live_coding4]
Unnamed_thm [in PRFA.live_coding4]
Unnamed_thm [in PRFA.review2]
Unnamed_thm0 [in PRFA.tp5c]
Unnamed_thm0 [in PRFA.tp5c]
Unnamed_thm [in PRFA.tp5c]
Unnamed_thm18 [in PRFA.tp4c]
Unnamed_thm17 [in PRFA.tp4c]
Unnamed_thm16 [in PRFA.tp4c]
Unnamed_thm15 [in PRFA.tp4c]
Unnamed_thm14 [in PRFA.tp4c]
Unnamed_thm13 [in PRFA.tp4c]
Unnamed_thm12 [in PRFA.tp4c]
Unnamed_thm11 [in PRFA.tp4c]
Unnamed_thm10 [in PRFA.tp4c]
Unnamed_thm9 [in PRFA.tp4c]
Unnamed_thm8 [in PRFA.tp4c]
Unnamed_thm7 [in PRFA.tp4c]
Unnamed_thm6 [in PRFA.tp4c]
Unnamed_thm5 [in PRFA.tp4c]
Unnamed_thm4 [in PRFA.tp4c]
Unnamed_thm3 [in PRFA.tp4c]
Unnamed_thm2 [in PRFA.tp4c]
Unnamed_thm1 [in PRFA.tp4c]
Unnamed_thm0 [in PRFA.tp4c]
Unnamed_thm [in PRFA.tp4c]
Unnamed_thm1 [in PRFA.live_coding7]
Unnamed_thm0 [in PRFA.live_coding7]
Unnamed_thm0 [in PRFA.live_coding7]
Unnamed_thm [in PRFA.live_coding7]
Unnamed_thm8 [in PRFA.tp6c]
Unnamed_thm7 [in PRFA.tp6c]
Unnamed_thm6 [in PRFA.tp6c]
Unnamed_thm5 [in PRFA.tp6c]
Unnamed_thm4 [in PRFA.tp6c]
Unnamed_thm3 [in PRFA.tp6c]
Unnamed_thm2 [in PRFA.tp6c]
Unnamed_thm1 [in PRFA.tp6c]
Unnamed_thm1 [in PRFA.tp6c]
Unnamed_thm1 [in PRFA.tp6c]
Unnamed_thm0 [in PRFA.tp6c]
Unnamed_thm0 [in PRFA.tp6c]
Unnamed_thm0 [in PRFA.tp6c]
Unnamed_thm0 [in PRFA.tp6c]
Unnamed_thm [in PRFA.tp6c]
Unnamed_thm0 [in PRFA.tp3c]
Unnamed_thm [in PRFA.tp3c]
upd_num [in PRFA.tp6c]

V

valuation [in PRFA.live_coding8]
vec_sind [in PRFA.tp8c]
vec_rec [in PRFA.tp8c]
vec_ind [in PRFA.tp8c]
vec_rect [in PRFA.tp8c]
vec_sind [in PRFA.live_coding8]
vec_rec [in PRFA.live_coding8]
vec_ind [in PRFA.live_coding8]
vec_rect [in PRFA.live_coding8]
vmap [in PRFA.tp8c]
vnth [in PRFA.tp8c]
vnth [in PRFA.live_coding8]

W

weak [in PRFA.tp8c]
what [in PRFA.tp6c]
wpermut [in PRFA.tp5c]

X

xren [in PRFA.tp8c]
xtree_rect_strong [in PRFA.tp3c]
xtree_sind [in PRFA.tp3c]
xtree_rec [in PRFA.tp3c]
xtree_ind [in PRFA.tp3c]
xtree_rect [in PRFA.tp3c]

Z

zero [in PRFA.tp2c]
zip [in PRFA.tp8c]
zip [in PRFA.live_coding8]
zip [in PRFA.live_coding8]

---

Record Index

B

bad_rational2 [in PRFA.live_coding4]
bad_rational1 [in PRFA.live_coding4]

E

Eq [in PRFA.live_coding4]
Eq [in PRFA.tp4c]
equiv [in PRFA.tp8c]

G

Group [in PRFA.tp4c]
group [in PRFA.tp4c]

M

Monoid [in PRFA.live_coding4]
monoid [in PRFA.live_coding4]
Monoid [in PRFA.tp4c]
monoid [in PRFA.tp4c]

P

point3D [in PRFA.tp6c]
prod' [in PRFA.review4]
prod' [in PRFA.live_coding4]
prod' [in PRFA.tp4c]

R

rational [in PRFA.live_coding4]

T

trap [in PRFA.tp6c]
triple [in PRFA.tp6c]

Z

Zalt [in PRFA.tp6c]

---

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

(1398 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

(35 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

(16 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(20 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

(22 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

(342 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

(120 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 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

(66 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

(56 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

(12 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

(15 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 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

(660 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

(19 entries)

---

This page has been generated by coqdoc