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 (25786 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 (996 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 (807 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 (1538 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 (584 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 (11835 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 (956 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 (627 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 (306 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 (475 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 (493 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 (903 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 (1194 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 (4910 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 (162 entries)

O (lemma)

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