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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)

O (lemma)

odd_plus_odd_inv_l [in odd_plus_odd_inv_l]
odd_even_lem [in odd_even_lem]
odd_plus_even_inv_r [in odd_plus_even_inv_r]
odd_mult [in odd_mult]
odd_plus_r [in odd_plus_r]
odd_spec [in odd_spec]
odd_mult_inv_l [in odd_mult_inv_l]
odd_S2n [in odd_S2n]
odd_plus_even_inv_l [in odd_plus_even_inv_l]
odd_plus_odd_inv_r [in odd_plus_odd_inv_r]
odd_even_plus [in odd_even_plus]
Odd_equiv [in Odd_equiv]
odd_mult_inv_r [in odd_mult_inv_r]
odd_div2 [in odd_div2]
odd_plus_split [in odd_plus_split]
odd_double [in odd_double]
odd_bitwise [in odd_bitwise]
odd_plus_l [in odd_plus_l]
of_nat_to_nat_inv [in of_nat_to_nat_inv]
Omega [in Omega]
omniscient_fun_choice_imp_fun_choice [in omniscient_fun_choice_imp_fun_choice]
omniscient_fun_choice_imp_small_drinker [in omniscient_fun_choice_imp_small_drinker]
one_IZR_r_R1 [in one_IZR_r_R1]
one_IZR_lt1 [in one_IZR_lt1]
open_set_P2 [in open_set_P2]
open_set_P6 [in open_set_P6]
open_set_P4 [in open_set_P4]
open_set_P5 [in open_set_P5]
open_set_P1 [in open_set_P1]
open_set_P3 [in open_set_P3]
opp_IZR [in opp_IZR]
op_rotate [in op_rotate]
orb_true_iff [in orb_true_iff]
orb_diag [in orb_diag]
orb_prop_intro [in orb_prop_intro]
orb_false_iff [in orb_false_iff]
orb_andb_distrib_l [in orb_andb_distrib_l]
orb_prop_elim [in orb_prop_elim]
orb_false_l [in orb_false_l]
orb_true_elim [in orb_true_elim]
orb_true_l [in orb_true_l]
orb_false_intro [in orb_false_intro]
orb_comm [in orb_comm]
orb_false_elim [in orb_false_elim]
orb_andb_distrib_r [in orb_andb_distrib_r]
orb_negb_r [in orb_negb_r]
orb_lazy_alt [in orb_lazy_alt]
orb_false_r [in orb_false_r]
orb_assoc [in orb_assoc]
orb_true_intro [in orb_true_intro]
orb_prop [in orb_prop]
orb_true_r [in orb_true_r]
OrderedTypeFacts.elim_compare_eq [in elim_compare_eq]
OrderedTypeFacts.elim_compare_gt [in elim_compare_gt]
OrderedTypeFacts.elim_compare_lt [in elim_compare_lt]
OrderedTypeFacts.eqb_alt [in eqb_alt]
OrderedTypeFacts.eqb_alt [in eqb_alt]
OrderedTypeFacts.eq_not_lt [in eq_not_lt]
OrderedTypeFacts.eq_lt [in eq_lt]
OrderedTypeFacts.eq_neq [in eq_neq]
OrderedTypeFacts.eq_not_gt [in eq_not_gt]
OrderedTypeFacts.eq_le [in eq_le]
OrderedTypeFacts.gt_not_eq [in gt_not_eq]
OrderedTypeFacts.if_eq_dec [in if_eq_dec]
OrderedTypeFacts.Inf_alt [in Inf_alt]
OrderedTypeFacts.Inf_eq [in Inf_eq]
OrderedTypeFacts.Inf_lt [in Inf_lt]
OrderedTypeFacts.In_eq [in In_eq]
OrderedTypeFacts.In_Inf [in In_Inf]
OrderedTypeFacts.le_trans [in le_trans]
OrderedTypeFacts.le_neq [in le_neq]
OrderedTypeFacts.le_antisym [in le_antisym]
OrderedTypeFacts.le_lt_trans [in le_lt_trans]
OrderedTypeFacts.le_eq [in le_eq]
OrderedTypeFacts.ListIn_Inf [in ListIn_Inf]
OrderedTypeFacts.ListIn_In [in ListIn_In]
OrderedTypeFacts.lt_dec [in lt_dec]
OrderedTypeFacts.lt_dec [in lt_dec]
OrderedTypeFacts.lt_le_trans [in lt_le_trans]
OrderedTypeFacts.lt_not_gt [in lt_not_gt]
OrderedTypeFacts.lt_antirefl [in lt_antirefl]
OrderedTypeFacts.lt_total [in lt_total]
OrderedTypeFacts.lt_eq [in lt_eq]
OrderedTypeFacts.lt_le [in lt_le]
OrderedTypeFacts.neq_eq [in neq_eq]
OrderedTypeFacts.neq_sym [in neq_sym]
OrderedTypeFacts.OrderElts.le_lteq [in le_lteq]
OrderedTypeFacts.Sort_NoDup [in Sort_NoDup]
OrderedTypeFacts.Sort_Inf_In [in Sort_Inf_In]
OrderedTypeFullFacts.compare_le_iff [in compare_le_iff]
OrderedTypeFullFacts.compare_ge_iff [in compare_ge_iff]
OrderedTypeFullFacts.eq_is_le_ge [in eq_is_le_ge]
OrderedTypeFullFacts.le_not_gt_iff [in le_not_gt_iff]
OrderedTypeFullFacts.le_or_gt [in le_or_gt]
OrderedTypeFullFacts.lt_or_ge [in lt_or_ge]
OrderedTypeFullFacts.lt_not_ge_iff [in lt_not_ge_iff]
OrderedTypeLists.Inf_alt [in Inf_alt]
OrderedTypeLists.Inf_eq [in Inf_eq]
OrderedTypeLists.Inf_lt [in Inf_lt]
OrderedTypeLists.In_eq [in In_eq]
OrderedTypeLists.In_Inf [in In_Inf]
OrderedTypeLists.ListIn_Inf [in ListIn_Inf]
OrderedTypeLists.ListIn_In [in ListIn_In]
OrderedTypeLists.Sort_NoDup [in Sort_NoDup]
OrderedTypeLists.Sort_Inf_In [in Sort_Inf_In]
OrderedTypeRev.compare_spec [in compare_spec]
OrderedTypeRev.le_lteq [in le_lteq]
OrderedTypeTest.eq_not_lt [in eq_not_lt]
OrderedTypeTest.eq_lt [in eq_lt]
OrderedTypeTest.eq_is_nlt_ngt [in eq_is_nlt_ngt]
OrderedTypeTest.eq_neq [in eq_neq]
OrderedTypeTest.eq_not_gt [in eq_not_gt]
OrderedTypeTest.eq_le [in eq_le]
OrderedTypeTest.gt_not_eq [in gt_not_eq]
OrderedTypeTest.le_trans [in le_trans]
OrderedTypeTest.le_neq [in le_neq]
OrderedTypeTest.le_antisym [in le_antisym]
OrderedTypeTest.le_lt_trans [in le_lt_trans]
OrderedTypeTest.le_eq [in le_eq]
OrderedTypeTest.lt_le_trans [in lt_le_trans]
OrderedTypeTest.lt_not_gt [in lt_not_gt]
OrderedTypeTest.lt_not_eq [in lt_not_eq]
OrderedTypeTest.lt_eq [in lt_eq]
OrderedTypeTest.lt_le [in lt_le]
OrderedTypeTest.neq_eq [in neq_eq]
OrderedTypeTest.neq_sym [in neq_sym]
OrderedType_from_Alt.eq_refl [in eq_refl]
OrderedType_to_Alt.compare_trans [in compare_trans]
OrderedType_from_Alt.eq_sym [in eq_sym]
OrderedType_from_Alt.lt_not_eq [in lt_not_eq]
OrderedType_to_Alt.compare_sym [in compare_sym]
OrderFacts.eq_refl [in eq_refl]
OrderFacts.eq_sym [in eq_sym]
OrderFacts.eq_neq [in eq_neq]
OrderFacts.le_neq_lt [in le_neq_lt]
OrderFacts.le_antisym [in le_antisym]
OrderFacts.le_refl [in le_refl]
OrderFacts.lt_irrefl [in lt_irrefl]
OrderFacts.neq_eq [in neq_eq]
OrderFacts.neq_sym [in neq_sym]
OrderFacts.not_ge_lt [in not_ge_lt]
OrderFacts.not_gt_le [in not_gt_le]
OrderFacts.not_neq_eq [in not_neq_eq]
OrderFacts.trans [in trans]
OrdProperties.add_fold [in add_fold]
OrdProperties.add_fold [in add_fold]
OrdProperties.choose_equal [in choose_equal]
OrdProperties.choose_equal [in choose_equal]
OrdProperties.elements_Add_Above [in elements_Add_Above]
OrdProperties.elements_Add_Above [in elements_Add_Above]
OrdProperties.elements_Add_Above [in elements_Add_Above]
OrdProperties.elements_split [in elements_split]
OrdProperties.elements_split [in elements_split]
OrdProperties.elements_split [in elements_split]
OrdProperties.elements_Add_Below [in elements_Add_Below]
OrdProperties.elements_Add_Below [in elements_Add_Below]
OrdProperties.elements_Add_Below [in elements_Add_Below]
OrdProperties.elements_Add [in elements_Add]
OrdProperties.elements_Add [in elements_Add]
OrdProperties.elements_Add [in elements_Add]
OrdProperties.elements_Equal_eqlistA [in elements_Equal_eqlistA]
OrdProperties.fold_Add_Above [in fold_Add_Above]
OrdProperties.fold_4 [in fold_4]
OrdProperties.fold_4 [in fold_4]
OrdProperties.fold_3 [in fold_3]
OrdProperties.fold_3 [in fold_3]
OrdProperties.fold_Equal [in fold_Equal]
OrdProperties.fold_equal [in fold_equal]
OrdProperties.fold_equal [in fold_equal]
OrdProperties.fold_Add_Below [in fold_Add_Below]
OrdProperties.gtb_1 [in gtb_1]
OrdProperties.gtb_1 [in gtb_1]
OrdProperties.gtb_1 [in gtb_1]
OrdProperties.gtb_compat [in gtb_compat]
OrdProperties.gtb_compat [in gtb_compat]
OrdProperties.leb_compat [in leb_compat]
OrdProperties.leb_compat [in leb_compat]
OrdProperties.leb_1 [in leb_1]
OrdProperties.leb_1 [in leb_1]
OrdProperties.leb_1 [in leb_1]
OrdProperties.map_induction_max [in map_induction_max]
OrdProperties.map_induction_min [in map_induction_min]
OrdProperties.max_elt_MapsTo [in max_elt_MapsTo]
OrdProperties.max_elt_Empty [in max_elt_Empty]
OrdProperties.max_elt_Above [in max_elt_Above]
OrdProperties.min_elt_Empty [in min_elt_Empty]
OrdProperties.min_elt_MapsTo [in min_elt_MapsTo]
OrdProperties.min_elt_Below [in min_elt_Below]
OrdProperties.remove_fold_2 [in remove_fold_2]
OrdProperties.remove_fold_2 [in remove_fold_2]
OrdProperties.set_induction_max [in set_induction_max]
OrdProperties.set_induction_max [in set_induction_max]
OrdProperties.set_induction_min [in set_induction_min]
OrdProperties.set_induction_min [in set_induction_min]
OrdProperties.sort_equivlistA_eqlistA [in sort_equivlistA_eqlistA]
OrdProperties.sort_equivlistA_eqlistA [in sort_equivlistA_eqlistA]
OrdProperties.sort_equivlistA_eqlistA [in sort_equivlistA_eqlistA]
or_to_imply [in or_to_imply]
or_cancel_l [in or_cancel_l]
or_not_r_iff_2 [in or_not_r_iff_2]
or_cancel_r [in or_cancel_r]
or_assoc [in or_assoc]
or_iff_compat_r [in or_iff_compat_r]
or_comm [in or_comm]
or_not_l_iff_1 [in or_not_l_iff_1]
or_not_r_iff_1 [in or_not_r_iff_1]
or_not_and [in or_not_and]
or_not_l_iff_2 [in or_not_l_iff_2]
or_iff_compat_l [in or_iff_compat_l]
OTF_to_TTLB.leb_le [in leb_le]
OTF_to_TTLB.leb_trans [in leb_trans]
OTF_LtIsTotal.lt_total [in lt_total]
OTF_to_TTLB.leb_total [in leb_total]
OT_to_Full.le_lteq [in le_lteq]
OT_from_Alt.eq_lt [in eq_lt]
OT_from_Alt.compare_spec [in compare_spec]
OT_to_Alt.compare_trans [in compare_trans]
OT_to_Alt.compare_Eq [in compare_Eq]
OT_to_Alt.compare_Lt [in compare_Lt]
OT_to_Alt.compare_sym [in compare_sym]
OT_from_Alt.lt_eq [in lt_eq]
OT_to_Alt.compare_Gt [in compare_Gt]
O_or_S [in O_or_S]
O_S [in O_S]



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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)