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 (845 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 (26 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 (11 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 (11 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 (14 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 (218 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 (72 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 (1 entry)
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 (43 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 (41 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 (7 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 (12 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 (2 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 (373 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 (14 entries)

Global Index

A

Acc [inductive, in PRFA.live_coding5]
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]
add [definition, in PRFA.tp2c]
add [definition, in PRFA.live_coding3]
add_from_nat [lemma, in PRFA.tp2c]
add_sub [lemma, in PRFA.review2]
Advanced [section, in PRFA.tp1c]
All [inductive, in PRFA.tp3c]
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]
app_assoc [lemma, in PRFA.tp2c]
app_nil_r [lemma, in PRFA.tp2c]
app_nil_r [lemma, in PRFA.live_coding2]


B

bad [inductive, in PRFA.live_coding3]
bad [inductive, in PRFA.tp3c]
bad_not_bad [lemma, in PRFA.tp3c]
bad_rational2 [record, in PRFA.live_coding4]
bad_rational1 [record, in PRFA.live_coding4]
bar [definition, in PRFA.live_coding3]
baz [definition, in PRFA.live_coding3]
below [definition, in PRFA.tp3c]
bintree [inductive, in PRFA.live_coding5]
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]
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]


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

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]
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]
de_morgan [lemma, in PRFA.tp1c]
distr [lemma, in PRFA.tp1c]
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_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]
Eq [record, in PRFA.tp4c]
Eq [record, in PRFA.live_coding4]
eqb [projection, in PRFA.tp4c]
eqb [projection, in PRFA.live_coding4]
eqb_iff [projection, in PRFA.tp4c]
eqb_iff [projection, in PRFA.live_coding4]
eq_nat_spec [lemma, in PRFA.tp2c]
eq_nat [definition, in PRFA.tp2c]
Eq_nat [instance, in PRFA.tp4c]
Eq_nat [instance, in PRFA.live_coding4]
eq_nat_spec [lemma, in PRFA.review2]
eq_nat [definition, in PRFA.review2]
even [inductive, in PRFA.review3]
even [inductive, in PRFA.live_coding2]
even [inductive, in PRFA.live_coding3]
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.review3]
evenO [constructor, in PRFA.tp2c]
evenO [constructor, in PRFA.live_coding2]
evenO [constructor, in PRFA.live_coding3]
evenS [constructor, in PRFA.review3]
evenS [constructor, in PRFA.tp2c]
evenS [constructor, in PRFA.live_coding2]
evenS [constructor, in PRFA.live_coding3]
even_sind [definition, in PRFA.review3]
even_ind [definition, in PRFA.review3]
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]
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]
exp [definition, in PRFA.tp2c]
exp_from_nat [lemma, in PRFA.tp2c]
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]
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_brec [definition, in PRFA.tp3c]
fib_natrec [definition, in PRFA.tp3c]
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]
foo [definition, in PRFA.tp4c]
foo [definition, in PRFA.live_coding3]
foo [definition, in PRFA.live_coding4]
forall_or [lemma, in PRFA.tp1c]
forall_False' [lemma, in PRFA.tp1c]
forall_False [lemma, in PRFA.tp1c]
Forall_set_eq [lemma, in PRFA.tp4c]
Forall_In [lemma, in PRFA.tp4c]
from_nat [definition, in PRFA.tp2c]
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.tp4c]
fst' [projection, in PRFA.live_coding4]


G

G [inductive, in PRFA.live_coding5]
get_kername [definition, in PRFA.MetaCoqPrelude]
GI [constructor, in PRFA.live_coding5]
good_tree_ind [lemma, in PRFA.live_coding5]
good_tree_ind' [lemma, in PRFA.live_coding5]
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_inv [projection, in PRFA.tp4c]
g_mon [projection, 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]


H

half [definition, in PRFA.live_coding4]
half' [definition, in PRFA.live_coding4]
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]


I

iAnd [definition, in PRFA.review3]
iAnd [definition, in PRFA.tp3c]
iAnd_and [lemma, in PRFA.review3]
iAnd_iff [lemma, in PRFA.tp3c]
idNat [definition, in PRFA.live_coding6]
idnat [definition, in PRFA.tp3c]
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]
imp_trans [lemma, in PRFA.tp1c]
In [definition, in PRFA.tp2c]
incl [constructor, in PRFA.tp2c]
incl [constructor, in PRFA.live_coding2]
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_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]
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]
iOr [definition, in PRFA.tp3c]
iOr_iff [lemma, in PRFA.tp3c]
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]


L

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]
LEM [definition, in PRFA.tp1c]
lem_dns [lemma, in PRFA.tp1c]
lem_pl [lemma, in PRFA.tp1c]
leO [constructor, in PRFA.live_coding2]
leO' [constructor, in PRFA.tp2c]
leS [constructor, in PRFA.live_coding2]
leS' [constructor, in PRFA.tp2c]
le_n_S [lemma, in PRFA.review3]
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' [inductive, in PRFA.tp2c]
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]
linear_search [lemma, in PRFA.live_coding5]
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]
list_rect [definition, in PRFA.live_coding3]
Live [section, in PRFA.live_coding1]
live_coding6 [library]
live_coding5 [library]
live_coding2 [library]
live_coding1 [library]
live_coding4 [library]
live_coding3 [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]


M

memb [definition, in PRFA.tp4c]
memb [definition, in PRFA.live_coding4]
memb_spec [lemma, in PRFA.tp4c]
MetaCoqPrelude [library]
min [definition, in PRFA.tp1c]
min_comm [lemma, in PRFA.tp1c]
Monoid [record, in PRFA.tp4c]
monoid [record, in PRFA.tp4c]
Monoid [record, in PRFA.live_coding4]
monoid [record, in PRFA.live_coding4]
MonoidList [instance, in PRFA.tp4c]
MonoidNat [instance, in PRFA.tp4c]
MonoidNat [instance, in PRFA.live_coding4]
MonoidProd [instance, in PRFA.tp4c]
MonoidProd [instance, in PRFA.live_coding4]
Monoid_Group [instance, in PRFA.tp4c]
monoid_fact [lemma, in PRFA.tp4c]
monoid_fact [lemma, in PRFA.live_coding4]
mon_assoc [projection, in PRFA.tp4c]
mon_right_neutral [projection, in PRFA.tp4c]
mon_left_neutral [projection, 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]
mpow [definition, in PRFA.live_coding6]
mpow' [definition, in PRFA.live_coding6]
mul [definition, in PRFA.tp2c]
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]
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]
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]


N

N [constructor, in PRFA.live_coding3]
N [constructor, in PRFA.tp3c]
nat_fact [lemma, in PRFA.tp4c]
nat_monoid [definition, in PRFA.tp4c]
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]
ncons [constructor, in PRFA.live_coding3]
ncons [constructor, in PRFA.tp3c]
negb_invol [lemma, in PRFA.live_coding1]
negb_true [lemma, in PRFA.live_coding1]
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]
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]
nofalse [lemma, in PRFA.tp1c]
nofalse [lemma, in PRFA.live_coding1]
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]
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]
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 [definition, in PRFA.review3]
or_imp [lemma, in PRFA.tp1c]
or_comm [lemma, in PRFA.tp1c]
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]
PI [definition, in PRFA.live_coding5]
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]
pow13 [definition, in PRFA.live_coding6]
pow3 [definition, in PRFA.live_coding6]
pow5 [definition, in PRFA.live_coding6]
pred [definition, in PRFA.tp2c]
pred_from_nat [lemma, in PRFA.tp2c]
pred' [definition, in PRFA.tp2c]
pred'_from_nat [lemma, in PRFA.tp2c]
prod_monoid [definition, in PRFA.tp4c]
prod_monoid [definition, in PRFA.live_coding4]
prod' [record, in PRFA.review4]
prod' [record, in PRFA.tp4c]
prod' [record, in PRFA.live_coding4]
prod'_ind [definition, in PRFA.review4]
prop_bool_sind [definition, in PRFA.live_coding5]
prop_bool_ind [definition, in PRFA.live_coding5]
prop_bool [inductive, in PRFA.live_coding5]
ptrue [constructor, in PRFA.live_coding5]
P_iff_P [lemma, in PRFA.tp1c]
P_imp_P [lemma, in PRFA.tp1c]
P_imp_P [lemma, in PRFA.live_coding1]


Q

quarter [definition, in PRFA.live_coding4]
quarter'' [definition, in PRFA.live_coding4]


R

rational [record, in PRFA.live_coding4]
refl [constructor, in PRFA.tp2c]
refl [constructor, in PRFA.live_coding2]
refl' [constructor, in PRFA.tp2c]
REPLACE_ME [definition, in PRFA.tp1c]
review2 [library]
review3 [library]
review4 [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]
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 [definition, in PRFA.review3]
Russel [definition, in PRFA.review3]
Russel [lemma, in PRFA.tp1c]
Russel [definition, in PRFA.tp3c]
Russell [lemma, in PRFA.live_coding3]


S

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]
size_recursion [lemma, in PRFA.live_coding5]
snd' [projection, in PRFA.review4]
snd' [projection, in PRFA.tp4c]
snd' [projection, in PRFA.live_coding4]
some_other_pair [definition, in PRFA.tp4c]
some_pair [definition, 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]
strong_nat_ind [lemma, in PRFA.tp2c]
strong_nat_ind [lemma, in PRFA.live_coding2]
strong_nat_ind [lemma, in PRFA.review2]
succ [definition, in PRFA.tp2c]
swap [definition, in PRFA.tp2c]
swap_invol [lemma, in PRFA.tp2c]
S_neq [lemma, in PRFA.tp3c]


T

T [definition, in PRFA.live_coding3]
term_eqb [definition, in PRFA.MetaCoqPrelude]
test [lemma, in PRFA.live_coding6]
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_nat' [lemma, in PRFA.live_coding4]
test_monoid [lemma, in PRFA.live_coding4]
test_nat [lemma, in PRFA.live_coding4]
theDNS [definition, in PRFA.tp1c]
theLEM [definition, in PRFA.tp1c]
thePL [definition, in PRFA.tp1c]
tLam [abbreviation, in PRFA.MetaCoqPrelude]
tLet [abbreviation, in PRFA.MetaCoqPrelude]
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_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_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_from_tree [lemma, in PRFA.tp3c]
to_tree_list [definition, in PRFA.tp3c]
to_tree [definition, in PRFA.tp3c]
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]
TP1 [section, in PRFA.tp1c]
tp1c [library]
tp2c [library]
tp3c [library]
tp4c [library]
trans [constructor, in PRFA.tp2c]
trans [constructor, in PRFA.live_coding2]
transform [definition, in PRFA.MetaCoqPrelude]
transform_nb [definition, in PRFA.MetaCoqPrelude]
trans' [constructor, in PRFA.tp2c]
tree [inductive, in PRFA.live_coding5]
tree [inductive, in PRFA.live_coding3]
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_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]
truetrue [lemma, in PRFA.tp1c]
truetrue [lemma, in PRFA.live_coding1]
true_false [lemma, in PRFA.review3]
true_false [lemma, in PRFA.tp2c]
twice [lemma, in PRFA.tp1c]


U

unfold_toplevel [definition, in PRFA.MetaCoqPrelude]
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]
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_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_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_thm0 [definition, in PRFA.tp3c]
Unnamed_thm [definition, in PRFA.tp3c]
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]


W

Well_founded.R [variable, in PRFA.live_coding5]
Well_founded.A [variable, in PRFA.live_coding5]
Well_founded [section, in PRFA.live_coding5]
WO [section, in PRFA.live_coding5]
WO.f [variable, in PRFA.live_coding5]


X

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

zero [definition, in PRFA.tp2c]


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.tp4c]
_ ** _ [notation, in PRFA.tp4c]
_ ** _ [notation, in PRFA.tp4c]
_ ** _ [notation, in PRFA.live_coding4]
__ [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 Index

D

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


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.tp4c]
_ ** _ [in PRFA.tp4c]
_ ** _ [in PRFA.tp4c]
_ ** _ [in PRFA.live_coding4]
__ [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]



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]


S

Show_Definitions [in PRFA.live_coding3]



Variable Index

D

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


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_coding2
live_coding1
live_coding4
live_coding3


M

MetaCoqPrelude


R

review2
review3
review4


T

tp1c
tp2c
tp3c
tp4c



Lemma Index

A

Acc_iff [in PRFA.live_coding5]
add_from_nat [in PRFA.tp2c]
add_sub [in PRFA.review2]
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]


B

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


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]
car_cur [in PRFA.tp2c]
car_cur [in PRFA.live_coding2]
classical_impl [in PRFA.tp1c]
classical_or_contra_r [in PRFA.tp1c]
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]
de_morgan [in PRFA.tp1c]
distr [in PRFA.tp1c]
dns_lem [in PRFA.tp1c]
dn_functorial [in PRFA.tp1c]
double_eq [in PRFA.tp1c]
double_eq2 [in PRFA.live_coding1]
double_eq [in PRFA.live_coding1]


E

eq_nat_spec [in PRFA.tp2c]
eq_nat_spec [in PRFA.review2]
evenb_to_even [in PRFA.live_coding2]
evenb_to_even [in PRFA.live_coding2]
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]
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]
Fib_Iter.fib_eq3 [in PRFA.tp2c]
Fib_Iter.fib_eq1 [in PRFA.tp2c]
Fib_Iter.fib_eq0 [in PRFA.tp2c]
forall_or [in PRFA.tp1c]
forall_False' [in PRFA.tp1c]
forall_False [in PRFA.tp1c]
Forall_set_eq [in PRFA.tp4c]
Forall_In [in PRFA.tp4c]
from_to_tree_alt [in PRFA.tp3c]


G

good_tree_ind [in PRFA.live_coding5]
good_tree_ind' [in PRFA.live_coding5]
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

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]
imp_trans [in PRFA.tp1c]
in_cons [in PRFA.review4]
in_add_left [in PRFA.review4]
in_add_right [in PRFA.review4]
In_iff [in PRFA.tp2c]
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]
In_hd' [in PRFA.live_coding4]
In_4 [in PRFA.live_coding4]
In_tl [in PRFA.live_coding4]
In_hd [in PRFA.live_coding4]
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

leb_spec_alt [in PRFA.tp2c]
leb_spec [in PRFA.tp2c]
lem_dns [in PRFA.tp1c]
lem_pl [in PRFA.tp1c]
le_n_S [in PRFA.review3]
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.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

memb_spec [in PRFA.tp4c]
min_comm [in PRFA.tp1c]
monoid_fact [in PRFA.tp4c]
monoid_fact [in PRFA.live_coding4]
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_fact [in PRFA.tp4c]
nat_nat_fact [in PRFA.live_coding4]
nat_nat_fact [in PRFA.live_coding4]
nat_fact [in PRFA.live_coding4]
negb_invol [in PRFA.live_coding1]
negb_true [in PRFA.live_coding1]
nofalse [in PRFA.tp1c]
nofalse [in PRFA.live_coding1]
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]
pred_from_nat [in PRFA.tp2c]
pred'_from_nat [in PRFA.tp2c]
P_iff_P [in PRFA.tp1c]
P_imp_P [in PRFA.tp1c]
P_imp_P [in PRFA.live_coding1]


R

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]


S

size_recursion [in PRFA.live_coding5]
strong_nat_ind [in PRFA.tp2c]
strong_nat_ind [in PRFA.live_coding2]
strong_nat_ind [in PRFA.review2]
swap_invol [in PRFA.tp2c]
S_neq [in PRFA.tp3c]


T

test [in PRFA.live_coding6]
test_list [in PRFA.tp4c]
test_nat' [in PRFA.tp4c]
test_monoid [in PRFA.tp4c]
test_nat [in PRFA.tp4c]
test_nat' [in PRFA.live_coding4]
test_monoid [in PRFA.live_coding4]
test_nat [in PRFA.live_coding4]
to_nat_inj [in PRFA.tp2c]
to_not_not [in PRFA.tp1c]
to_prod_eq [in PRFA.tp4c]
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_from_tree [in PRFA.tp3c]
tree_map_id_again' [in PRFA.live_coding5]
tree_map_id_again [in PRFA.live_coding5]
tree_map_id [in PRFA.live_coding5]
truetrue [in PRFA.tp1c]
truetrue [in PRFA.live_coding1]
true_false [in PRFA.review3]
true_false [in PRFA.tp2c]
twice [in PRFA.tp1c]



Constructor Index

A

Acc_intro [in PRFA.live_coding5]
All_cons [in PRFA.tp3c]
All_nil [in PRFA.tp3c]


B

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


C

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


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.review3]
evenO [in PRFA.tp2c]
evenO [in PRFA.live_coding2]
evenO [in PRFA.live_coding3]
evenS [in PRFA.review3]
evenS [in PRFA.tp2c]
evenS [in PRFA.live_coding2]
evenS [in PRFA.live_coding3]


G

GI [in PRFA.live_coding5]


H

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

leO [in PRFA.live_coding2]
leO' [in PRFA.tp2c]
leS [in PRFA.live_coding2]
leS' [in PRFA.tp2c]
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]
nnil [in PRFA.live_coding3]
nnil [in PRFA.tp3c]
nnode [in PRFA.live_coding3]
nnode [in PRFA.tp3c]
node [in PRFA.live_coding5]
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]
Nx [in PRFA.tp3c]


P

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


R

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


S

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]


T

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



Axiom Index

D

DNE [in PRFA.live_coding4]



Inductive Index

A

Acc [in PRFA.live_coding5]
All [in PRFA.tp3c]


B

bad [in PRFA.live_coding3]
bad [in PRFA.tp3c]
bintree [in PRFA.live_coding5]
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

even [in PRFA.review3]
even [in PRFA.live_coding2]
even [in PRFA.live_coding3]
even4 [in PRFA.tp2c]


G

G [in PRFA.live_coding5]


H

Hierarchy.tree [in PRFA.tp3c]


I

In_i [in PRFA.tp2c]


L

le [in PRFA.live_coding2]
le' [in PRFA.tp2c]
lt [in PRFA.review3]
lt [in PRFA.tp3c]


M

mult4 [in PRFA.live_coding6]


N

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


P

prop_bool [in PRFA.live_coding5]


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]


T

tree [in PRFA.live_coding5]
tree [in PRFA.live_coding3]
tree [in PRFA.tp3c]


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.tp4c]
eqb [in PRFA.live_coding4]
eqb_iff [in PRFA.tp4c]
eqb_iff [in PRFA.live_coding4]


F

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


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]


M

mon_assoc [in PRFA.tp4c]
mon_right_neutral [in PRFA.tp4c]
mon_left_neutral [in PRFA.tp4c]
mon_assoc [in PRFA.live_coding4]
mon_right_neutral [in PRFA.live_coding4]
mon_left_neutral [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]
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]


N

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


S

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



Section Index

A

Advanced [in PRFA.tp1c]


D

Demo [in PRFA.live_coding3]


L

Live [in PRFA.live_coding1]


T

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.tp4c]
Eq_nat [in PRFA.live_coding4]


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.tp4c]
MonoidNat [in PRFA.live_coding4]
MonoidProd [in PRFA.tp4c]
MonoidProd [in PRFA.live_coding4]
Monoid_Group [in PRFA.tp4c]



Abbreviation Index

T

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



Definition Index

A

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]
All_sind [in PRFA.tp3c]
All_rec [in PRFA.tp3c]
All_ind [in PRFA.tp3c]
All_rect [in PRFA.tp3c]


B

bar [in PRFA.live_coding3]
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]
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]


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

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]
dependent [in PRFA.live_coding3]
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]
eq_nat [in PRFA.tp2c]
eq_nat [in PRFA.review2]
evenb [in PRFA.live_coding2]
even_sind [in PRFA.review3]
even_ind [in PRFA.review3]
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]
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]
exp [in PRFA.tp2c]
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.tp3c]
Fib_Iter.fib [in PRFA.tp2c]
Fib_Iter.sigma [in PRFA.tp2c]
fib_brec [in PRFA.tp3c]
fib_natrec [in PRFA.tp3c]
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]
foo [in PRFA.tp4c]
foo [in PRFA.live_coding3]
foo [in PRFA.live_coding4]
from_nat [in PRFA.tp2c]
from_to_tree_list [in PRFA.tp3c]
from_to_tree [in PRFA.tp3c]
from_tree_list [in PRFA.tp3c]
from_tree [in PRFA.tp3c]


G

get_kername [in PRFA.MetaCoqPrelude]
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]
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]
idNat [in PRFA.live_coding6]
idnat [in PRFA.tp3c]
iEx [in PRFA.review3]
iEx [in PRFA.tp3c]
iFalse [in PRFA.review3]
iFalse [in PRFA.tp3c]
In [in PRFA.tp2c]
In_i_sind [in PRFA.tp2c]
In_i_ind [in PRFA.tp2c]
iOr [in PRFA.tp3c]
iter [in PRFA.tp2c]
iter [in PRFA.live_coding2]
iTrue [in PRFA.tp3c]


L

least [in PRFA.live_coding5]
leb [in PRFA.tp2c]
LEM [in PRFA.tp1c]
le_sind [in PRFA.live_coding2]
le_ind [in PRFA.live_coding2]
le'_sind [in PRFA.tp2c]
le'_ind [in PRFA.tp2c]
list_set_eq [in PRFA.tp4c]
list_monoid [in PRFA.tp4c]
list_rect [in PRFA.live_coding3]
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

memb [in PRFA.tp4c]
memb [in PRFA.live_coding4]
min [in PRFA.tp1c]
mpow [in PRFA.live_coding6]
mpow' [in PRFA.live_coding6]
mul [in PRFA.tp2c]
mult4_sind [in PRFA.live_coding6]
mult4_ind [in PRFA.live_coding6]


N

nat_monoid [in PRFA.tp4c]
nat_rect [in PRFA.live_coding3]
nat_monoid [in PRFA.live_coding4]
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]
not_mult4_sind [in PRFA.live_coding6]
not_mult4_ind [in PRFA.live_coding6]
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]
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.tp4c]
prod_monoid [in PRFA.live_coding4]
prod'_ind [in PRFA.review4]
prop_bool_sind [in PRFA.live_coding5]
prop_bool_ind [in PRFA.live_coding5]


Q

quarter [in PRFA.live_coding4]
quarter'' [in PRFA.live_coding4]


R

REPLACE_ME [in PRFA.tp1c]
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

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_other_pair [in PRFA.tp4c]
some_pair [in PRFA.tp4c]
some_tree [in PRFA.live_coding3]
some_other_pair [in PRFA.live_coding4]
some_pair [in PRFA.live_coding4]
succ [in PRFA.tp2c]
swap [in PRFA.tp2c]


T

T [in PRFA.live_coding3]
term_eqb [in PRFA.MetaCoqPrelude]
theDNS [in PRFA.tp1c]
theLEM [in PRFA.tp1c]
thePL [in PRFA.tp1c]
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_prod_alt3 [in PRFA.tp4c]
to_prod_alt2 [in PRFA.tp4c]
to_prod_alt [in PRFA.tp4c]
to_prod [in PRFA.tp4c]
to_bool [in PRFA.live_coding5]
to_prop_bool [in PRFA.live_coding5]
to_tree_list [in PRFA.tp3c]
to_tree [in PRFA.tp3c]
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]
transform [in PRFA.MetaCoqPrelude]
transform_nb [in PRFA.MetaCoqPrelude]
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_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]


U

unfold_toplevel [in PRFA.MetaCoqPrelude]
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_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_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_thm0 [in PRFA.tp3c]
Unnamed_thm [in PRFA.tp3c]
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]


X

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]



Record Index

B

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


E

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


G

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


M

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


P

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


R

rational [in PRFA.live_coding4]



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 (845 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 (26 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 (11 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 (11 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 (14 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 (218 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 (72 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 (1 entry)
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 (43 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 (41 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 (7 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 (12 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 (2 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 (373 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 (14 entries)

This page has been generated by coqdoc