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 (26071 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 (1003 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 (815 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 (1771 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 (589 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 (961 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 (12021 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 (508 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 (308 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 (479 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 (496 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 (906 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 (1204 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 (4844 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 (166 entries)

O (lemma)

oappEmap [in Stdlib.ssr.ssrfun]
oapp_comp_f [in Stdlib.ssr.ssrfun]
oapp_comp [in Stdlib.ssr.ssrfun]
obindEapp [in Stdlib.ssr.ssrfun]
ocan_in_comp [in Stdlib.ssr.ssrbool]
ocan_comp [in Stdlib.ssr.ssrfun]
of_pos_spec [in Stdlib.Numbers.Cyclic.Int63.Sint63]
of_Z_cmod [in Stdlib.Numbers.Cyclic.Int63.Sint63]
of_Z_spec [in Stdlib.Numbers.Cyclic.Int63.Sint63]
of_to_Z [in Stdlib.Numbers.Cyclic.Int63.Sint63]
of_list_app [in Stdlib.Strings.PString]
of_list_length [in Stdlib.Strings.PString]
of_list_inj [in Stdlib.Numbers.HexadecimalFacts]
of_list_to_list [in Stdlib.Numbers.HexadecimalFacts]
of_iff [in Stdlib.Numbers.DecimalR]
of_inj [in Stdlib.Numbers.DecimalR]
of_decimal_dnorm [in Stdlib.Numbers.DecimalR]
of_to [in Stdlib.Numbers.DecimalR]
of_IQmake_to_decimal [in Stdlib.Numbers.DecimalR]
of_list_to_list_opp [in Stdlib.Vectors.VectorSpec]
of_nat_to_nat_inv [in Stdlib.Vectors.Fin]
of_nat_ext [in Stdlib.Vectors.Fin]
of_hex_int_double [in Stdlib.Numbers.HexadecimalZ]
of_hex_int_iter_D0 [in Stdlib.Numbers.HexadecimalZ]
of_hex_uint_iter_D0 [in Stdlib.Numbers.HexadecimalZ]
of_iff [in Stdlib.Numbers.HexadecimalZ]
of_inj [in Stdlib.Numbers.HexadecimalZ]
of_int_norm [in Stdlib.Numbers.HexadecimalZ]
of_to [in Stdlib.Numbers.HexadecimalZ]
of_iff [in Stdlib.Numbers.DecimalQ]
of_inj [in Stdlib.Numbers.DecimalQ]
of_decimal_dnorm [in Stdlib.Numbers.DecimalQ]
of_to [in Stdlib.Numbers.DecimalQ]
of_IQmake_to_decimal' [in Stdlib.Numbers.DecimalQ]
of_IQmake_to_decimal [in Stdlib.Numbers.DecimalQ]
of_iff [in Stdlib.Numbers.HexadecimalR]
of_inj [in Stdlib.Numbers.HexadecimalR]
of_hexadecimal_dnorm [in Stdlib.Numbers.HexadecimalR]
of_to [in Stdlib.Numbers.HexadecimalR]
of_IQmake_to_hexadecimal [in Stdlib.Numbers.HexadecimalR]
of_iff [in Stdlib.Numbers.HexadecimalQ]
of_inj [in Stdlib.Numbers.HexadecimalQ]
of_hexadecimal_dnorm [in Stdlib.Numbers.HexadecimalQ]
of_to [in Stdlib.Numbers.HexadecimalQ]
of_IQmake_to_hexadecimal' [in Stdlib.Numbers.HexadecimalQ]
of_IQmake_to_hexadecimal [in Stdlib.Numbers.HexadecimalQ]
of_nat_via_N [in Stdlib.Strings.Byte]
of_N_via_nat [in Stdlib.Strings.Byte]
of_N_None_iff [in Stdlib.Strings.Byte]
of_to_N [in Stdlib.Strings.Byte]
of_nat_None_iff [in Stdlib.Strings.Byte]
of_to_nat [in Stdlib.Strings.Byte]
of_nat_to_nat_eq [in Stdlib.micromega.ZifyInst]
of_bits_to_bits [in Stdlib.Init.Byte]
of_list_inj [in Stdlib.Numbers.DecimalFacts]
of_list_to_list [in Stdlib.Numbers.DecimalFacts]
of_int_iter_D0 [in Stdlib.Numbers.DecimalZ]
of_uint_iter_D0 [in Stdlib.Numbers.DecimalZ]
of_iff [in Stdlib.Numbers.DecimalZ]
of_inj [in Stdlib.Numbers.DecimalZ]
of_int_norm [in Stdlib.Numbers.DecimalZ]
of_to [in Stdlib.Numbers.DecimalZ]
of_nat_inj [in Stdlib.Arith.Cantor]
of_voidK [in Stdlib.ssr.ssrfun]
of_Z_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
of_pos_rec_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
olift_comp [in Stdlib.ssr.ssrfun]
omapEapp [in Stdlib.ssr.ssrfun]
omapEbind [in Stdlib.ssr.ssrfun]
omap_comp [in Stdlib.ssr.ssrfun]
OMEGA1 [in Stdlib.omega.OmegaLemmas]
OMEGA10 [in Stdlib.omega.OmegaLemmas]
OMEGA11 [in Stdlib.omega.OmegaLemmas]
OMEGA12 [in Stdlib.omega.OmegaLemmas]
OMEGA13 [in Stdlib.omega.OmegaLemmas]
OMEGA14 [in Stdlib.omega.OmegaLemmas]
OMEGA15 [in Stdlib.omega.OmegaLemmas]
OMEGA16 [in Stdlib.omega.OmegaLemmas]
OMEGA17 [in Stdlib.omega.OmegaLemmas]
OMEGA18 [in Stdlib.omega.OmegaLemmas]
OMEGA19 [in Stdlib.omega.OmegaLemmas]
OMEGA2 [in Stdlib.omega.OmegaLemmas]
OMEGA20 [in Stdlib.omega.OmegaLemmas]
OMEGA3 [in Stdlib.omega.OmegaLemmas]
OMEGA4 [in Stdlib.omega.OmegaLemmas]
OMEGA5 [in Stdlib.omega.OmegaLemmas]
OMEGA6 [in Stdlib.omega.OmegaLemmas]
OMEGA7 [in Stdlib.omega.OmegaLemmas]
OMEGA8 [in Stdlib.omega.OmegaLemmas]
OMEGA9 [in Stdlib.omega.OmegaLemmas]
omniscient_fun_choice_imp_fun_choice [in Stdlib.Logic.ChoiceFacts]
omniscient_fun_choice_imp_small_drinker [in Stdlib.Logic.ChoiceFacts]
one_IZR_r_R1 [in Stdlib.Reals.RIneq]
one_IZR_lt1 [in Stdlib.Reals.RIneq]
onS_can_in [in Stdlib.ssr.ssrbool]
onS_can [in Stdlib.ssr.ssrbool]
onT_bij [in Stdlib.ssr.ssrbool]
onW_can_in [in Stdlib.ssr.ssrbool]
onW_can [in Stdlib.ssr.ssrbool]
onW_bij [in Stdlib.ssr.ssrbool]
on_can_inj [in Stdlib.ssr.ssrbool]
on1lS [in Stdlib.ssr.ssrbool]
on1lS_in [in Stdlib.ssr.ssrbool]
on1lT [in Stdlib.ssr.ssrbool]
on1lW [in Stdlib.ssr.ssrbool]
on1lW_in [in Stdlib.ssr.ssrbool]
on1S [in Stdlib.ssr.ssrbool]
on1S_in [in Stdlib.ssr.ssrbool]
on1T [in Stdlib.ssr.ssrbool]
on1W [in Stdlib.ssr.ssrbool]
on1W_in [in Stdlib.ssr.ssrbool]
on2S [in Stdlib.ssr.ssrbool]
on2S_in [in Stdlib.ssr.ssrbool]
on2T [in Stdlib.ssr.ssrbool]
on2W [in Stdlib.ssr.ssrbool]
on2W_in [in Stdlib.ssr.ssrbool]
OpAdd_sound [in Stdlib.micromega.RingMicromega]
open_set_P6 [in Stdlib.Reals.Rtopology]
open_set_P5 [in Stdlib.Reals.Rtopology]
open_set_P4 [in Stdlib.Reals.Rtopology]
open_set_P3 [in Stdlib.Reals.Rtopology]
open_set_P2 [in Stdlib.Reals.Rtopology]
open_set_P1 [in Stdlib.Reals.Rtopology]
OpMult_sound [in Stdlib.micromega.RingMicromega]
oppcarry_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
oppc_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
opp_inject_Z [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
opp_inject_Q [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
opp_of_Z [in Stdlib.Numbers.Cyclic.Int63.Sint63]
opp_spec [in Stdlib.Numbers.Cyclic.Int63.Sint63]
opp_IZR [in Stdlib.Reals.RIneq]
opp_to_Z_opp [in Stdlib.Numbers.Cyclic.Int63.Uint63]
opp_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
op_rotate [in Stdlib.Sets.Permut]
orbA [in Stdlib.ssr.ssrbool]
orbAC [in Stdlib.ssr.ssrbool]
orbACA [in Stdlib.ssr.ssrbool]
orbb [in Stdlib.ssr.ssrbool]
orbC [in Stdlib.ssr.ssrbool]
orbCA [in Stdlib.ssr.ssrbool]
orbF [in Stdlib.ssr.ssrbool]
orbK [in Stdlib.ssr.ssrbool]
orbN [in Stdlib.ssr.ssrbool]
orbT [in Stdlib.ssr.ssrbool]
orb_id2r [in Stdlib.ssr.ssrbool]
orb_id2l [in Stdlib.ssr.ssrbool]
orb_idr [in Stdlib.ssr.ssrbool]
orb_idl [in Stdlib.ssr.ssrbool]
orb_andr [in Stdlib.ssr.ssrbool]
orb_andl [in Stdlib.ssr.ssrbool]
orb_lazy_alt [in Stdlib.Bool.Bool]
orb_prop_intro [in Stdlib.Bool.Bool]
orb_prop_elim [in Stdlib.Bool.Bool]
orb_andb_distrib_l [in Stdlib.Bool.Bool]
orb_andb_distrib_r [in Stdlib.Bool.Bool]
orb_assoc [in Stdlib.Bool.Bool]
orb_comm [in Stdlib.Bool.Bool]
orb_negb_l [in Stdlib.Bool.Bool]
orb_negb_r [in Stdlib.Bool.Bool]
orb_false_l [in Stdlib.Bool.Bool]
orb_false_r [in Stdlib.Bool.Bool]
orb_true_l [in Stdlib.Bool.Bool]
orb_true_r [in Stdlib.Bool.Bool]
orb_diag [in Stdlib.Bool.Bool]
orb_false_elim [in Stdlib.Bool.Bool]
orb_false_intro [in Stdlib.Bool.Bool]
orb_true_intro [in Stdlib.Bool.Bool]
orb_prop [in Stdlib.Bool.Bool]
orb_true_elim [in Stdlib.Bool.Bool]
orb_false_iff [in Stdlib.Bool.Bool]
orb_true_iff [in Stdlib.Bool.Bool]
OrderedTypeFacts.elim_compare_gt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.elim_compare_lt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.elim_compare_eq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.eqb_alt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.eqb_alt [in Stdlib.Structures.OrdersFacts]
OrderedTypeFacts.eq_not_gt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.eq_not_lt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.eq_neq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.eq_le [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.eq_lt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.gt_not_eq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.if_eq_dec [in Stdlib.Structures.OrdersFacts]
OrderedTypeFacts.Inf_alt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.Inf_eq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.Inf_lt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.In_Inf [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.In_eq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.IsTO.le_lteq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.le_antisym [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.le_trans [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.le_neq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.le_lt_trans [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.le_eq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.ListIn_Inf [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.ListIn_In [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_dec [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_not_gt [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_le [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_le_trans [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_total [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_eq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_antirefl [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.lt_dec [in Stdlib.Structures.OrdersFacts]
OrderedTypeFacts.neq_sym [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.neq_eq [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.Sort_NoDup [in Stdlib.Structures.OrderedType]
OrderedTypeFacts.Sort_Inf_In [in Stdlib.Structures.OrderedType]
OrderedTypeFullFacts.compare_ge_iff [in Stdlib.Structures.OrdersFacts]
OrderedTypeFullFacts.compare_le_iff [in Stdlib.Structures.OrdersFacts]
OrderedTypeFullFacts.eq_is_le_ge [in Stdlib.Structures.OrdersFacts]
OrderedTypeFullFacts.le_or_gt [in Stdlib.Structures.OrdersFacts]
OrderedTypeFullFacts.le_not_gt_iff [in Stdlib.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_or_ge [in Stdlib.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_not_ge_iff [in Stdlib.Structures.OrdersFacts]
OrderedTypeLists.Inf_alt [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.Inf_eq [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.Inf_lt [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.In_Inf [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.In_eq [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.ListIn_Inf [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.ListIn_In [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.Sort_NoDup [in Stdlib.Structures.OrdersLists]
OrderedTypeLists.Sort_Inf_In [in Stdlib.Structures.OrdersLists]
OrderedTypeRev.compare_spec [in Stdlib.Structures.OrdersFacts]
OrderedTypeRev.le_lteq [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.eq_is_nlt_ngt [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.eq_not_gt [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.eq_not_lt [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.eq_neq [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.eq_le [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.eq_lt [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.gt_not_eq [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.le_neq [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.le_antisym [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.le_trans [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.le_lt_trans [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.le_eq [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.lt_not_gt [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.lt_le [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.lt_le_trans [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.lt_eq [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.lt_not_eq [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.neq_sym [in Stdlib.Structures.OrdersFacts]
OrderedTypeTest.neq_eq [in Stdlib.Structures.OrdersFacts]
OrderedType_to_Alt.compare_trans [in Stdlib.Structures.OrderedTypeAlt]
OrderedType_to_Alt.compare_sym [in Stdlib.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt_not_eq [in Stdlib.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_sym [in Stdlib.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_refl [in Stdlib.Structures.OrderedTypeAlt]
OrderFacts.eq_neq [in Stdlib.Structures.OrdersTac]
OrderFacts.eq_sym [in Stdlib.Structures.OrdersTac]
OrderFacts.eq_refl [in Stdlib.Structures.OrdersTac]
OrderFacts.le_neq_lt [in Stdlib.Structures.OrdersTac]
OrderFacts.le_antisym [in Stdlib.Structures.OrdersTac]
OrderFacts.le_refl [in Stdlib.Structures.OrdersTac]
OrderFacts.lt_irrefl [in Stdlib.Structures.OrdersTac]
OrderFacts.neq_eq [in Stdlib.Structures.OrdersTac]
OrderFacts.neq_sym [in Stdlib.Structures.OrdersTac]
OrderFacts.not_gt_le [in Stdlib.Structures.OrdersTac]
OrderFacts.not_ge_lt [in Stdlib.Structures.OrdersTac]
OrderFacts.not_neq_eq [in Stdlib.Structures.OrdersTac]
OrderFacts.trans [in Stdlib.Structures.OrdersTac]
OrdProperties.add_fold [in Stdlib.MSets.MSetProperties]
OrdProperties.add_fold [in Stdlib.FSets.FSetProperties]
OrdProperties.choose_equal [in Stdlib.MSets.MSetProperties]
OrdProperties.choose_equal [in Stdlib.FSets.FSetProperties]
OrdProperties.elements_Add_Below [in Stdlib.MSets.MSetProperties]
OrdProperties.elements_Add_Above [in Stdlib.MSets.MSetProperties]
OrdProperties.elements_Add [in Stdlib.MSets.MSetProperties]
OrdProperties.elements_split [in Stdlib.MSets.MSetProperties]
OrdProperties.elements_Equal_eqlistA [in Stdlib.FSets.FMapFacts]
OrdProperties.elements_Add_Below [in Stdlib.FSets.FMapFacts]
OrdProperties.elements_Add_Above [in Stdlib.FSets.FMapFacts]
OrdProperties.elements_Add [in Stdlib.FSets.FMapFacts]
OrdProperties.elements_split [in Stdlib.FSets.FMapFacts]
OrdProperties.elements_Add_Below [in Stdlib.FSets.FSetProperties]
OrdProperties.elements_Add_Above [in Stdlib.FSets.FSetProperties]
OrdProperties.elements_Add [in Stdlib.FSets.FSetProperties]
OrdProperties.elements_split [in Stdlib.FSets.FSetProperties]
OrdProperties.fold_equal [in Stdlib.MSets.MSetProperties]
OrdProperties.fold_4 [in Stdlib.MSets.MSetProperties]
OrdProperties.fold_3 [in Stdlib.MSets.MSetProperties]
OrdProperties.fold_Add_Below [in Stdlib.FSets.FMapFacts]
OrdProperties.fold_Add_Above [in Stdlib.FSets.FMapFacts]
OrdProperties.fold_Equal [in Stdlib.FSets.FMapFacts]
OrdProperties.fold_equal [in Stdlib.FSets.FSetProperties]
OrdProperties.fold_4 [in Stdlib.FSets.FSetProperties]
OrdProperties.fold_3 [in Stdlib.FSets.FSetProperties]
OrdProperties.gtb_1 [in Stdlib.MSets.MSetProperties]
OrdProperties.gtb_compat [in Stdlib.FSets.FMapFacts]
OrdProperties.gtb_1 [in Stdlib.FSets.FMapFacts]
OrdProperties.gtb_compat [in Stdlib.FSets.FSetProperties]
OrdProperties.gtb_1 [in Stdlib.FSets.FSetProperties]
OrdProperties.leb_1 [in Stdlib.MSets.MSetProperties]
OrdProperties.leb_compat [in Stdlib.FSets.FMapFacts]
OrdProperties.leb_1 [in Stdlib.FSets.FMapFacts]
OrdProperties.leb_compat [in Stdlib.FSets.FSetProperties]
OrdProperties.leb_1 [in Stdlib.FSets.FSetProperties]
OrdProperties.map_induction_min [in Stdlib.FSets.FMapFacts]
OrdProperties.map_induction_max [in Stdlib.FSets.FMapFacts]
OrdProperties.max_elt_Empty [in Stdlib.FSets.FMapFacts]
OrdProperties.max_elt_MapsTo [in Stdlib.FSets.FMapFacts]
OrdProperties.max_elt_Above [in Stdlib.FSets.FMapFacts]
OrdProperties.min_elt_Empty [in Stdlib.FSets.FMapFacts]
OrdProperties.min_elt_MapsTo [in Stdlib.FSets.FMapFacts]
OrdProperties.min_elt_Below [in Stdlib.FSets.FMapFacts]
OrdProperties.remove_fold_2 [in Stdlib.MSets.MSetProperties]
OrdProperties.remove_fold_2 [in Stdlib.FSets.FSetProperties]
OrdProperties.set_induction_min [in Stdlib.MSets.MSetProperties]
OrdProperties.set_induction_max [in Stdlib.MSets.MSetProperties]
OrdProperties.set_induction_min [in Stdlib.FSets.FSetProperties]
OrdProperties.set_induction_max [in Stdlib.FSets.FSetProperties]
OrdProperties.sort_equivlistA_eqlistA [in Stdlib.MSets.MSetProperties]
OrdProperties.sort_equivlistA_eqlistA [in Stdlib.FSets.FMapFacts]
OrdProperties.sort_equivlistA_eqlistA [in Stdlib.FSets.FSetProperties]
orFb [in Stdlib.ssr.ssrbool]
orKb [in Stdlib.ssr.ssrbool]
orNb [in Stdlib.ssr.ssrbool]
orP [in Stdlib.ssr.ssrbool]
orPP [in Stdlib.ssr.ssrbool]
orTb [in Stdlib.ssr.ssrbool]
or_not_r_iff_2 [in Stdlib.Logic.Decidable]
or_not_r_iff_1 [in Stdlib.Logic.Decidable]
or_not_l_iff_2 [in Stdlib.Logic.Decidable]
or_not_l_iff_1 [in Stdlib.Logic.Decidable]
or_morph [in Stdlib.micromega.ZifyClasses]
or_cnf_opt_correct [in Stdlib.micromega.Tauto]
or_cnf_correct [in Stdlib.micromega.Tauto]
or_clause_cnf_correct [in Stdlib.micromega.Tauto]
or_clause_correct [in Stdlib.micromega.Tauto]
or_is_X_inv [in Stdlib.micromega.Tauto]
or_cnf_opt_cnf_ff_r [in Stdlib.micromega.Tauto]
or_cnf_opt_cnf_ff [in Stdlib.micromega.Tauto]
or_assoc [in Stdlib.Init.Logic]
or_comm [in Stdlib.Init.Logic]
or_cancel_r [in Stdlib.Init.Logic]
or_cancel_l [in Stdlib.Init.Logic]
or_iff_compat_r [in Stdlib.Init.Logic]
or_iff_compat_l [in Stdlib.Init.Logic]
or_not_and [in Stdlib.Logic.Classical_Prop]
or_to_imply [in Stdlib.Logic.Classical_Prop]
or3P [in Stdlib.ssr.ssrbool]
or4P [in Stdlib.ssr.ssrbool]
OTF_to_TTLB.leb_trans [in Stdlib.Structures.Orders]
OTF_to_TTLB.leb_total [in Stdlib.Structures.Orders]
OTF_to_TTLB.leb_le [in Stdlib.Structures.Orders]
OTF_LtIsTotal.lt_total [in Stdlib.Structures.Orders]
OT_to_Alt.compare_trans [in Stdlib.Structures.OrdersAlt]
OT_to_Alt.compare_Gt [in Stdlib.Structures.OrdersAlt]
OT_to_Alt.compare_Lt [in Stdlib.Structures.OrdersAlt]
OT_to_Alt.compare_Eq [in Stdlib.Structures.OrdersAlt]
OT_to_Alt.compare_sym [in Stdlib.Structures.OrdersAlt]
OT_from_Alt.compare_spec [in Stdlib.Structures.OrdersAlt]
OT_from_Alt.eq_lt [in Stdlib.Structures.OrdersAlt]
OT_from_Alt.lt_eq [in Stdlib.Structures.OrdersAlt]
OT_to_Full.le_lteq [in Stdlib.Structures.Orders]
OT.eq_trans [in Stdlib.Strings.PString]
OT.eq_sym [in Stdlib.Strings.PString]
OT.eq_refl [in Stdlib.Strings.PString]
OT.lt_not_eq [in Stdlib.Strings.PString]
OT.lt_trans [in Stdlib.Strings.PString]
O_S [in Stdlib.Init.Peano]
O_or_S [in Stdlib.Arith.Peano_dec]


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 (26071 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 (1003 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 (815 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 (1771 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 (589 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 (961 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 (12021 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 (508 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 (308 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 (479 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 (496 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 (906 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 (1204 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 (4844 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 (166 entries)