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 (72487 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 (1049 entries)
Binder 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 (47021 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 (788 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 (1537 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 (588 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 (11841 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 (1025 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 (634 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 (473 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 (486 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 (881 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 (1465 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 (4229 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 (164 entries)

W (instance)

well_founded_morphism [in Coq.Classes.Morphisms_Prop]
WFactsOn.add_s_m [in Coq.MSets.MSetFacts]
WFactsOn.add_m [in Coq.MSets.MSetFacts]
WFactsOn.diff_s_m [in Coq.MSets.MSetFacts]
WFactsOn.diff_m [in Coq.MSets.MSetFacts]
WFactsOn.Empty_s_m [in Coq.MSets.MSetFacts]
WFactsOn.Empty_m [in Coq.MSets.MSetFacts]
WFactsOn.equal_m [in Coq.MSets.MSetFacts]
WFactsOn.filter_subset [in Coq.MSets.MSetFacts]
WFactsOn.filter_equal [in Coq.MSets.MSetFacts]
WFactsOn.inter_s_m [in Coq.MSets.MSetFacts]
WFactsOn.inter_m [in Coq.MSets.MSetFacts]
WFactsOn.In_s_m [in Coq.MSets.MSetFacts]
WFactsOn.In_m [in Coq.MSets.MSetFacts]
WFactsOn.is_empty_m [in Coq.MSets.MSetFacts]
WFactsOn.mem_m [in Coq.MSets.MSetFacts]
WFactsOn.remove_s_m [in Coq.MSets.MSetFacts]
WFactsOn.remove_m [in Coq.MSets.MSetFacts]
WFactsOn.singleton_m [in Coq.MSets.MSetFacts]
WFactsOn.SubsetSetoid [in Coq.MSets.MSetFacts]
WFactsOn.subset_m [in Coq.MSets.MSetFacts]
WFactsOn.Subset_m [in Coq.MSets.MSetFacts]
WFactsOn.union_s_m [in Coq.MSets.MSetFacts]
WFactsOn.union_m [in Coq.MSets.MSetFacts]
WFacts_fun.In_s_m [in Coq.FSets.FSetFacts]
WFacts_fun.equal_m [in Coq.FSets.FSetFacts]
WFacts_fun.subset_m [in Coq.FSets.FSetFacts]
WFacts_fun.Subset_m [in Coq.FSets.FSetFacts]
WFacts_fun.diff_m [in Coq.FSets.FSetFacts]
WFacts_fun.inter_m [in Coq.FSets.FSetFacts]
WFacts_fun.union_m [in Coq.FSets.FSetFacts]
WFacts_fun.remove_m [in Coq.FSets.FSetFacts]
WFacts_fun.add_m [in Coq.FSets.FSetFacts]
WFacts_fun.singleton_m [in Coq.FSets.FSetFacts]
WFacts_fun.mem_m [in Coq.FSets.FSetFacts]
WFacts_fun.Empty_m [in Coq.FSets.FSetFacts]
WFacts_fun.is_empty_m [in Coq.FSets.FSetFacts]
WFacts_fun.In_m [in Coq.FSets.FSetFacts]
WFacts_fun.Equal_ST [in Coq.FSets.FSetFacts]
WFacts_fun.E_ST [in Coq.FSets.FSetFacts]
WPropertiesOn.cardinal_m [in Coq.MSets.MSetProperties]
WProperties_fun.eqke_equiv [in Coq.FSets.FMapFacts]
WProperties_fun.eqk_equiv [in Coq.FSets.FMapFacts]
WRawSets.add_ok [in Coq.MSets.MSetInterface]
WRawSets.diff_ok [in Coq.MSets.MSetInterface]
WRawSets.empty_ok [in Coq.MSets.MSetInterface]
WRawSets.eq_equiv [in Coq.MSets.MSetInterface]
WRawSets.filter_ok [in Coq.MSets.MSetInterface]
WRawSets.inter_ok [in Coq.MSets.MSetInterface]
WRawSets.In_compat [in Coq.MSets.MSetInterface]
WRawSets.isok_Ok [in Coq.MSets.MSetInterface]
WRawSets.partition_ok2 [in Coq.MSets.MSetInterface]
WRawSets.partition_ok1 [in Coq.MSets.MSetInterface]
WRawSets.remove_ok [in Coq.MSets.MSetInterface]
WRawSets.singleton_ok [in Coq.MSets.MSetInterface]
WRawSets.union_ok [in Coq.MSets.MSetInterface]
WRaw2SetsOn.eq_equiv [in Coq.MSets.MSetInterface]
WRaw2SetsOn.In_compat [in Coq.MSets.MSetInterface]
WSetsOn.In_compat [in Coq.MSets.MSetInterface]



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 (72487 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 (1049 entries)
Binder 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 (47021 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 (788 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 (1537 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 (588 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 (11841 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 (1025 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 (634 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 (473 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 (486 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 (881 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 (1465 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 (4229 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 (164 entries)