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)

W

wB [definition, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wB [abbreviation, in wB]
wBwB_lex [lemma, in wBwB_lex]
wBwB_lex_inv [lemma, in wBwB_lex_inv]
wB_div_plus [lemma, in wB_div_plus]
wB_pos [lemma, in wB_pos]
wB_pos [lemma, in wB_pos]
wB_pos [lemma, in wB_pos]
wB_lex_inv [lemma, in wB_lex_inv]
wB_div2 [lemma, in wB_div2]
wB_div_2 [lemma, in wB_div_2]
wB_div [lemma, in wB_div]
wB_div_4 [lemma, in wB_div_4]
WDecide [module, in WDecide]
WDecide [module, in WDecide]
WDecideOn [module, in WDecideOn]
WDecideOn.F [module, in WDecideOn.F]
WDecideOn.MSetDecideAuxiliary [module, in WDecideOn.MSetDecideAuxiliary]
WDecideOn.MSetDecideAuxiliary.conj_elt_prop [constructor, in conj_elt_prop]
WDecideOn.MSetDecideAuxiliary.dec_eq [lemma, in dec_eq]
WDecideOn.MSetDecideAuxiliary.dec_In [lemma, in dec_In]
WDecideOn.MSetDecideAuxiliary.disj_elt_prop [constructor, in disj_elt_prop]
WDecideOn.MSetDecideAuxiliary.elt_MSet_Prop [constructor, in elt_MSet_Prop]
WDecideOn.MSetDecideAuxiliary.Empty_MSet_Prop [constructor, in Empty_MSet_Prop]
WDecideOn.MSetDecideAuxiliary.Equal_MSet_Prop [constructor, in Equal_MSet_Prop]
WDecideOn.MSetDecideAuxiliary.eq_elt_prop [constructor, in eq_elt_prop]
WDecideOn.MSetDecideAuxiliary.eq_Prop [constructor, in eq_Prop]
WDecideOn.MSetDecideAuxiliary.eq_refl_iff [lemma, in eq_refl_iff]
WDecideOn.MSetDecideAuxiliary.False_elt_prop [constructor, in False_elt_prop]
WDecideOn.MSetDecideAuxiliary.impl_elt_prop [constructor, in impl_elt_prop]
WDecideOn.MSetDecideAuxiliary.In_elt_prop [constructor, in In_elt_prop]
WDecideOn.MSetDecideAuxiliary.MSet_Prop [inductive, in MSet_Prop]
WDecideOn.MSetDecideAuxiliary.MSet_elt_Prop [inductive, in MSet_elt_Prop]
WDecideOn.MSetDecideAuxiliary.not_elt_prop [constructor, in not_elt_prop]
WDecideOn.MSetDecideAuxiliary.Subset_MSet_Prop [constructor, in Subset_MSet_Prop]
WDecideOn.MSetDecideAuxiliary.True_elt_prop [constructor, in True_elt_prop]
WDecideOn.MSetDecideTestCases [module, in WDecideOn.MSetDecideTestCases]
WDecideOn.MSetDecideTestCases.eq_chain_test [lemma, in eq_chain_test]
WDecideOn.MSetDecideTestCases.function_test_1 [lemma, in function_test_1]
WDecideOn.MSetDecideTestCases.function_test_2 [lemma, in function_test_2]
WDecideOn.MSetDecideTestCases.test_add_In [lemma, in test_add_In]
WDecideOn.MSetDecideTestCases.test_eq_disjunction [lemma, in test_eq_disjunction]
WDecideOn.MSetDecideTestCases.test_too_complex [lemma, in test_too_complex]
WDecideOn.MSetDecideTestCases.test_eq_trans_2 [lemma, in test_eq_trans_2]
WDecideOn.MSetDecideTestCases.test_not_In_disj [lemma, in test_not_In_disj]
WDecideOn.MSetDecideTestCases.test_In_singleton [lemma, in test_In_singleton]
WDecideOn.MSetDecideTestCases.test_eq_trans_1 [lemma, in test_eq_trans_1]
WDecideOn.MSetDecideTestCases.test_Subset_add_remove [lemma, in test_Subset_add_remove]
WDecideOn.MSetDecideTestCases.test_not_In_conj [lemma, in test_not_In_conj]
WDecideOn.MSetDecideTestCases.test_eq_neq_trans_1 [lemma, in test_eq_neq_trans_1]
WDecideOn.MSetDecideTestCases.test_set_ops_1 [lemma, in test_set_ops_1]
WDecideOn.MSetDecideTestCases.test_baydemir [lemma, in test_baydemir]
WDecideOn.MSetDecideTestCases.test_eq_neq_trans_2 [lemma, in test_eq_neq_trans_2]
WDecideOn.MSetDecideTestCases.test_iff_conj [lemma, in test_iff_conj]
WDecideOn.MSetLogicalFacts [module, in WDecideOn.MSetLogicalFacts]
WDecideOn.MSetLogicalFacts.test_pull [lemma, in test_pull]
WDecideOn.MSetLogicalFacts.test_push [lemma, in test_push]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [constructor, in conj_elt_prop]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [constructor, in disj_elt_prop]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [constructor, in Subset_FSet_Prop]
WDecide_fun.F [module, in WDecide_fun.F]
WDecide_fun.FSetDecideTestCases.test_add_In [lemma, in test_add_In]
WDecide_fun.FSetDecideTestCases.function_test_1 [lemma, in function_test_1]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [constructor, in not_elt_prop]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [lemma, in test_eq_disjunction]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [constructor, in eq_elt_prop]
WDecide_fun.FSetDecideTestCases.test_too_complex [lemma, in test_too_complex]
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [inductive, in FSet_elt_Prop]
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [inductive, in FSet_Prop]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [constructor, in impl_elt_prop]
WDecide_fun.FSetDecideAuxiliary.dec_eq [lemma, in dec_eq]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [lemma, in test_eq_trans_2]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [constructor, in Empty_FSet_Prop]
WDecide_fun.FSetLogicalFacts.test_pull [lemma, in test_pull]
WDecide_fun.FSetDecideTestCases.eq_chain_test [lemma, in eq_chain_test]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [lemma, in test_not_In_disj]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [constructor, in True_elt_prop]
WDecide_fun.FSetLogicalFacts [module, in WDecide_fun.FSetLogicalFacts]
WDecide_fun.FSetDecideTestCases [module, in WDecide_fun.FSetDecideTestCases]
WDecide_fun.FSetDecideTestCases.test_In_singleton [lemma, in test_In_singleton]
WDecide_fun.FSetLogicalFacts.test_push [lemma, in test_push]
WDecide_fun.FSetDecideTestCases.function_test_2 [lemma, in function_test_2]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [constructor, in Equal_FSet_Prop]
WDecide_fun.FSetDecideAuxiliary.dec_In [lemma, in dec_In]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [constructor, in elt_FSet_Prop]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [lemma, in test_eq_trans_1]
WDecide_fun [module, in WDecide_fun]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [lemma, in test_Subset_add_remove]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [lemma, in test_not_In_conj]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [lemma, in test_eq_neq_trans_1]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [lemma, in test_set_ops_1]
WDecide_fun.FSetDecideAuxiliary [module, in WDecide_fun.FSetDecideAuxiliary]
WDecide_fun.FSetDecideTestCases.test_baydemir [lemma, in test_baydemir]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [constructor, in eq_Prop]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [constructor, in In_elt_prop]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [lemma, in test_eq_neq_trans_2]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [constructor, in False_elt_prop]
WDecide_fun.FSetDecideAuxiliary.eq_refl_iff [lemma, in eq_refl_iff]
WDecide_fun.FSetDecideTestCases.test_iff_conj [lemma, in test_iff_conj]
weak [definition, in weak]
weak_excluded_middle [definition, in weak_excluded_middle]
weak_generalized_excluded_middle [definition, in weak_generalized_excluded_middle]
Wellfounded [library]
WellOrdering [section, in WellOrdering]
WellOrdering.A [variable, in A]
WellOrdering.B [variable, in B]
Well_founded.Rwf [variable, in Rwf]
Well_founded_2.Rwf [variable, in Rwf]
Well_founded.Rwf [variable, in Rwf]
well_founded_morphism [instance, in well_founded_morphism]
Well_founded.P [variable, in P]
Well_founded_2.P [variable, in P]
Well_founded.FixPoint.P [variable, in P]
well_founded_inv_lt_rel_compat [lemma, in well_founded_inv_lt_rel_compat]
Well_founded [section, in Well_founded]
Well_founded [section, in Well_founded]
well_founded_lt_compat [lemma, in well_founded_lt_compat]
Well_founded_2.B [variable, in B]
well_founded_induction_type [lemma, in well_founded_induction_type]
Well_founded.R [variable, in R]
Well_founded_Nat.R [variable, in R]
Well_founded_2.R [variable, in R]
Well_founded.R [variable, in R]
well_founded_ltof [lemma, in well_founded_ltof]
Well_founded_Nat.f [variable, in f]
Well_founded.F_ext [variable, in F_ext]
Well_founded.FixPoint.F_ext [variable, in F_ext]
Well_founded_2.FixPoint_2.F [variable, in F]
Well_founded.FixPoint.F [variable, in F]
Well_founded_Nat.H_compat [variable, in H_compat]
well_founded_inv_rel_inv_lt_rel [lemma, in well_founded_inv_rel_inv_lt_rel]
Well_founded_Nat [section, in Well_founded_Nat]
Well_founded.FixPoint [section, in FixPoint]
well_founded_ind [lemma, in well_founded_ind]
well_founded_gtof [lemma, in well_founded_gtof]
Well_founded.A [variable, in A]
Well_founded_Nat.A [variable, in A]
Well_founded_2.A [variable, in A]
Well_founded.A [variable, in A]
well_founded_induction_type_2 [lemma, in well_founded_induction_type_2]
Well_founded.F_sub [variable, in F_sub]
Well_founded_2.FixPoint_2 [section, in FixPoint_2]
well_founded [definition, in well_founded]
well_founded_induction [lemma, in well_founded_induction]
Well_founded_2 [section, in Well_founded_2]
Well_Ordering [library]
WEqProperties [module, in WEqProperties]
WEqProperties [module, in WEqProperties]
WEqPropertiesOn [module, in WEqPropertiesOn]
WEqPropertiesOn.Add [definition, in Add]
WEqPropertiesOn.add_remove [lemma, in add_remove]
WEqPropertiesOn.add_mem_1 [lemma, in add_mem_1]
WEqPropertiesOn.add_filter_2 [lemma, in add_filter_2]
WEqPropertiesOn.add_union_singleton [lemma, in add_union_singleton]
WEqPropertiesOn.add_filter_1 [lemma, in add_filter_1]
WEqPropertiesOn.add_cardinal_2 [lemma, in add_cardinal_2]
WEqPropertiesOn.add_mem_3 [lemma, in add_mem_3]
WEqPropertiesOn.add_mem_2 [lemma, in add_mem_2]
WEqPropertiesOn.add_fold [lemma, in add_fold]
WEqPropertiesOn.add_equal [lemma, in add_equal]
WEqPropertiesOn.add_cardinal_1 [lemma, in add_cardinal_1]
WEqPropertiesOn.BasicProperties [section, in BasicProperties]
WEqPropertiesOn.BasicProperties.s [variable, in s]
WEqPropertiesOn.BasicProperties.s' [variable, in s']
WEqPropertiesOn.BasicProperties.s'' [variable, in s'']
WEqPropertiesOn.BasicProperties.x [variable, in x]
WEqPropertiesOn.BasicProperties.y [variable, in y]
WEqPropertiesOn.BasicProperties.z [variable, in z]
WEqPropertiesOn.Bool [section, in Bool]
WEqPropertiesOn.Bool' [section, in Bool']
WEqPropertiesOn.Bool'.Comp [variable, in Comp]
WEqPropertiesOn.Bool'.Comp' [variable, in Comp']
WEqPropertiesOn.Bool'.f [variable, in f]
WEqPropertiesOn.Bool.Comp [variable, in Comp]
WEqPropertiesOn.Bool.Comp' [variable, in Comp']
WEqPropertiesOn.Bool.f [variable, in f]
WEqPropertiesOn.choose_mem_3 [lemma, in choose_mem_3]
WEqPropertiesOn.choose_mem_2 [lemma, in choose_mem_2]
WEqPropertiesOn.choose_mem_4 [lemma, in choose_mem_4]
WEqPropertiesOn.choose_mem_1 [lemma, in choose_mem_1]
WEqPropertiesOn.compat_opL [abbreviation, in compat_opL]
WEqPropertiesOn.diff_subset_equal [lemma, in diff_subset_equal]
WEqPropertiesOn.diff_inter_all [lemma, in diff_inter_all]
WEqPropertiesOn.diff_subset [lemma, in diff_subset]
WEqPropertiesOn.diff_mem [lemma, in diff_mem]
WEqPropertiesOn.diff_inter_empty [lemma, in diff_inter_empty]
WEqPropertiesOn.empty_mem [lemma, in empty_mem]
WEqPropertiesOn.equal_mem_1 [lemma, in equal_mem_1]
WEqPropertiesOn.equal_equal [lemma, in equal_equal]
WEqPropertiesOn.equal_cardinal [lemma, in equal_cardinal]
WEqPropertiesOn.equal_mem_2 [lemma, in equal_mem_2]
WEqPropertiesOn.equal_trans [lemma, in equal_trans]
WEqPropertiesOn.equal_sym [lemma, in equal_sym]
WEqPropertiesOn.equal_refl [lemma, in equal_refl]
WEqPropertiesOn.exclusive_set [lemma, in exclusive_set]
WEqPropertiesOn.exists_mem_3 [lemma, in exists_mem_3]
WEqPropertiesOn.exists_mem_1 [lemma, in exists_mem_1]
WEqPropertiesOn.exists_mem_2 [lemma, in exists_mem_2]
WEqPropertiesOn.exists_filter [lemma, in exists_filter]
WEqPropertiesOn.exists_mem_4 [lemma, in exists_mem_4]
WEqPropertiesOn.filter_mem [lemma, in filter_mem]
WEqPropertiesOn.filter_add_1 [lemma, in filter_add_1]
WEqPropertiesOn.filter_add_2 [lemma, in filter_add_2]
WEqPropertiesOn.filter_union [lemma, in filter_union]
WEqPropertiesOn.Fold [section, in Fold]
WEqPropertiesOn.fold_empty [lemma, in fold_empty]
WEqPropertiesOn.fold_compat [lemma, in fold_compat]
WEqPropertiesOn.fold_add [lemma, in fold_add]
WEqPropertiesOn.fold_union [lemma, in fold_union]
WEqPropertiesOn.fold_equal [lemma, in fold_equal]
WEqPropertiesOn.Fold.A [variable, in A]
WEqPropertiesOn.Fold.Ass [variable, in Ass]
WEqPropertiesOn.Fold.Comp [variable, in Comp]
WEqPropertiesOn.Fold.eqA [variable, in eqA]
WEqPropertiesOn.Fold.f [variable, in f]
WEqPropertiesOn.Fold.i [variable, in i]
WEqPropertiesOn.Fold.s [variable, in s]
WEqPropertiesOn.Fold.st [variable, in st]
WEqPropertiesOn.Fold.s' [variable, in s']
WEqPropertiesOn.Fold.x [variable, in x]
WEqPropertiesOn.for_all_mem_3 [lemma, in for_all_mem_3]
WEqPropertiesOn.for_all_mem_2 [lemma, in for_all_mem_2]
WEqPropertiesOn.for_all_filter [lemma, in for_all_filter]
WEqPropertiesOn.for_all_mem_4 [lemma, in for_all_mem_4]
WEqPropertiesOn.for_all_exists [lemma, in for_all_exists]
WEqPropertiesOn.for_all_mem_1 [lemma, in for_all_mem_1]
WEqPropertiesOn.inter_assoc [lemma, in inter_assoc]
WEqPropertiesOn.inter_equal_2 [lemma, in inter_equal_2]
WEqPropertiesOn.inter_subset_2 [lemma, in inter_subset_2]
WEqPropertiesOn.inter_subset_equal [lemma, in inter_subset_equal]
WEqPropertiesOn.inter_add_1 [lemma, in inter_add_1]
WEqPropertiesOn.inter_sym [lemma, in inter_sym]
WEqPropertiesOn.inter_subset_1 [lemma, in inter_subset_1]
WEqPropertiesOn.inter_add_2 [lemma, in inter_add_2]
WEqPropertiesOn.inter_equal_1 [lemma, in inter_equal_1]
WEqPropertiesOn.inter_mem [lemma, in inter_mem]
WEqPropertiesOn.inter_subset_3 [lemma, in inter_subset_3]
WEqPropertiesOn.is_empty_cardinal [lemma, in is_empty_cardinal]
WEqPropertiesOn.is_empty_equal_empty [lemma, in is_empty_equal_empty]
WEqPropertiesOn.mem_4 [lemma, in mem_4]
WEqPropertiesOn.mem_3 [lemma, in mem_3]
WEqPropertiesOn.mem_eq [lemma, in mem_eq]
WEqPropertiesOn.MP [module, in WEqPropertiesOn.MP]
WEqPropertiesOn.partition_filter_1 [lemma, in partition_filter_1]
WEqPropertiesOn.partition_filter_2 [lemma, in partition_filter_2]
WEqPropertiesOn.remove_cardinal_1 [lemma, in remove_cardinal_1]
WEqPropertiesOn.remove_add [lemma, in remove_add]
WEqPropertiesOn.remove_fold_2 [lemma, in remove_fold_2]
WEqPropertiesOn.remove_equal [lemma, in remove_equal]
WEqPropertiesOn.remove_fold_1 [lemma, in remove_fold_1]
WEqPropertiesOn.remove_cardinal_2 [lemma, in remove_cardinal_2]
WEqPropertiesOn.remove_inter_singleton [lemma, in remove_inter_singleton]
WEqPropertiesOn.remove_mem_2 [lemma, in remove_mem_2]
WEqPropertiesOn.remove_mem_1 [lemma, in remove_mem_1]
WEqPropertiesOn.remove_mem_3 [lemma, in remove_mem_3]
WEqPropertiesOn.set_rec [lemma, in set_rec]
WEqPropertiesOn.singleton_mem_2 [lemma, in singleton_mem_2]
WEqPropertiesOn.singleton_mem_1 [lemma, in singleton_mem_1]
WEqPropertiesOn.singleton_mem_3 [lemma, in singleton_mem_3]
WEqPropertiesOn.singleton_equal_add [lemma, in singleton_equal_add]
WEqPropertiesOn.subset_trans [lemma, in subset_trans]
WEqPropertiesOn.subset_mem_1 [lemma, in subset_mem_1]
WEqPropertiesOn.subset_mem_2 [lemma, in subset_mem_2]
WEqPropertiesOn.subset_equal [lemma, in subset_equal]
WEqPropertiesOn.subset_cardinal [lemma, in subset_cardinal]
WEqPropertiesOn.subset_antisym [lemma, in subset_antisym]
WEqPropertiesOn.subset_refl [lemma, in subset_refl]
WEqPropertiesOn.sum [definition, in sum]
WEqPropertiesOn.Sum [section, in Sum]
WEqPropertiesOn.sum_compat [lemma, in sum_compat]
WEqPropertiesOn.sum_plus [lemma, in sum_plus]
WEqPropertiesOn.sum_filter [lemma, in sum_filter]
WEqPropertiesOn.transposeL [abbreviation, in transposeL]
WEqPropertiesOn.union_subset_1 [lemma, in union_subset_1]
WEqPropertiesOn.union_inter_2 [lemma, in union_inter_2]
WEqPropertiesOn.union_sym [lemma, in union_sym]
WEqPropertiesOn.union_subset_3 [lemma, in union_subset_3]
WEqPropertiesOn.union_subset_2 [lemma, in union_subset_2]
WEqPropertiesOn.union_mem [lemma, in union_mem]
WEqPropertiesOn.union_cardinal [lemma, in union_cardinal]
WEqPropertiesOn.union_filter [lemma, in union_filter]
WEqPropertiesOn.union_subset_equal [lemma, in union_subset_equal]
WEqPropertiesOn.union_equal_1 [lemma, in union_equal_1]
WEqPropertiesOn.union_add [lemma, in union_add]
WEqPropertiesOn.union_assoc [lemma, in union_assoc]
WEqPropertiesOn.union_inter_1 [lemma, in union_inter_1]
WEqPropertiesOn.union_equal_2 [lemma, in union_equal_2]
WEqProperties_fun.for_all_mem_3 [lemma, in for_all_mem_3]
WEqProperties_fun.compat_opL [abbreviation, in compat_opL]
WEqProperties_fun.add_remove [lemma, in add_remove]
WEqProperties_fun.inter_assoc [lemma, in inter_assoc]
WEqProperties_fun.union_subset_1 [lemma, in union_subset_1]
WEqProperties_fun.singleton_mem_2 [lemma, in singleton_mem_2]
WEqProperties_fun.equal_mem_1 [lemma, in equal_mem_1]
WEqProperties_fun.remove_cardinal_1 [lemma, in remove_cardinal_1]
WEqProperties_fun.add_mem_1 [lemma, in add_mem_1]
WEqProperties_fun.inter_equal_2 [lemma, in inter_equal_2]
WEqProperties_fun.equal_equal [lemma, in equal_equal]
WEqProperties_fun.fold_empty [lemma, in fold_empty]
WEqProperties_fun.empty_mem [lemma, in empty_mem]
WEqProperties_fun.Fold.s' [variable, in s']
WEqProperties_fun.BasicProperties.s' [variable, in s']
WEqProperties_fun.Fold.eqA [variable, in eqA]
WEqProperties_fun.remove_add [lemma, in remove_add]
WEqProperties_fun.add_filter_2 [lemma, in add_filter_2]
WEqProperties_fun.inter_subset_2 [lemma, in inter_subset_2]
WEqProperties_fun.Fold.st [variable, in st]
WEqProperties_fun.mem_4 [lemma, in mem_4]
WEqProperties_fun.singleton_mem_1 [lemma, in singleton_mem_1]
WEqProperties_fun.partition_filter_1 [lemma, in partition_filter_1]
WEqProperties_fun.for_all_mem_2 [lemma, in for_all_mem_2]
WEqProperties_fun.union_inter_2 [lemma, in union_inter_2]
WEqProperties_fun.transposeL [abbreviation, in transposeL]
WEqProperties_fun.union_sym [lemma, in union_sym]
WEqProperties_fun.add_union_singleton [lemma, in add_union_singleton]
WEqProperties_fun.inter_subset_equal [lemma, in inter_subset_equal]
WEqProperties_fun.equal_cardinal [lemma, in equal_cardinal]
WEqProperties_fun.diff_subset_equal [lemma, in diff_subset_equal]
WEqProperties_fun.diff_inter_all [lemma, in diff_inter_all]
WEqProperties_fun.sum_compat [lemma, in sum_compat]
WEqProperties_fun.add_filter_1 [lemma, in add_filter_1]
WEqProperties_fun.equal_mem_2 [lemma, in equal_mem_2]
WEqProperties_fun.Fold.s [variable, in s]
WEqProperties_fun.BasicProperties.s [variable, in s]
WEqProperties_fun.remove_fold_2 [lemma, in remove_fold_2]
WEqProperties_fun.fold_compat [lemma, in fold_compat]
WEqProperties_fun.mem_3 [lemma, in mem_3]
WEqProperties_fun.Add [definition, in Add]
WEqProperties_fun.remove_equal [lemma, in remove_equal]
WEqProperties_fun.subset_trans [lemma, in subset_trans]
WEqProperties_fun.add_cardinal_2 [lemma, in add_cardinal_2]
WEqProperties_fun.sum [definition, in sum]
WEqProperties_fun.fold_add [lemma, in fold_add]
WEqProperties_fun.is_empty_cardinal [lemma, in is_empty_cardinal]
WEqProperties_fun.union_subset_3 [lemma, in union_subset_3]
WEqProperties_fun.union_subset_2 [lemma, in union_subset_2]
WEqProperties_fun.union_mem [lemma, in union_mem]
WEqProperties_fun.remove_fold_1 [lemma, in remove_fold_1]
WEqProperties_fun.subset_mem_1 [lemma, in subset_mem_1]
WEqProperties_fun.is_empty_equal_empty [lemma, in is_empty_equal_empty]
WEqProperties_fun.Fold.i [variable, in i]
WEqProperties_fun.sum_plus [lemma, in sum_plus]
WEqProperties_fun.subset_mem_2 [lemma, in subset_mem_2]
WEqProperties_fun.remove_cardinal_2 [lemma, in remove_cardinal_2]
WEqProperties_fun.subset_equal [lemma, in subset_equal]
WEqProperties_fun.filter_mem [lemma, in filter_mem]
WEqProperties_fun.diff_subset [lemma, in diff_subset]
WEqProperties_fun.remove_inter_singleton [lemma, in remove_inter_singleton]
WEqProperties_fun.Bool'.f [variable, in f]
WEqProperties_fun.Bool.f [variable, in f]
WEqProperties_fun.Fold.f [variable, in f]
WEqProperties_fun.partition_filter_2 [lemma, in partition_filter_2]
WEqProperties_fun.for_all_filter [lemma, in for_all_filter]
WEqProperties_fun.choose_mem_3 [lemma, in choose_mem_3]
WEqProperties_fun.union_cardinal [lemma, in union_cardinal]
WEqProperties_fun.inter_add_1 [lemma, in inter_add_1]
WEqProperties_fun.filter_add_1 [lemma, in filter_add_1]
WEqProperties_fun.sum_filter [lemma, in sum_filter]
WEqProperties_fun.Bool'.Comp' [variable, in Comp']
WEqProperties_fun.Bool.Comp' [variable, in Comp']
WEqProperties_fun.filter_add_2 [lemma, in filter_add_2]
WEqProperties_fun.Bool' [section, in Bool']
WEqProperties_fun.exists_mem_3 [lemma, in exists_mem_3]
WEqProperties_fun.mem_eq [lemma, in mem_eq]
WEqProperties_fun.inter_sym [lemma, in inter_sym]
WEqProperties_fun.exists_mem_1 [lemma, in exists_mem_1]
WEqProperties_fun.Fold.x [variable, in x]
WEqProperties_fun.BasicProperties.x [variable, in x]
WEqProperties_fun.union_filter [lemma, in union_filter]
WEqProperties_fun.filter_union [lemma, in filter_union]
WEqProperties_fun.choose_mem_2 [lemma, in choose_mem_2]
WEqProperties_fun.subset_cardinal [lemma, in subset_cardinal]
WEqProperties_fun.BasicProperties.s'' [variable, in s'']
WEqProperties_fun.union_subset_equal [lemma, in union_subset_equal]
WEqProperties_fun.fold_union [lemma, in fold_union]
WEqProperties_fun.exists_mem_2 [lemma, in exists_mem_2]
WEqProperties_fun.choose_mem_4 [lemma, in choose_mem_4]
WEqProperties_fun.singleton_mem_3 [lemma, in singleton_mem_3]
WEqProperties_fun.Bool [section, in Bool]
WEqProperties_fun.diff_mem [lemma, in diff_mem]
WEqProperties_fun.union_equal_1 [lemma, in union_equal_1]
WEqProperties_fun.subset_antisym [lemma, in subset_antisym]
WEqProperties_fun.equal_trans [lemma, in equal_trans]
WEqProperties_fun.equal_sym [lemma, in equal_sym]
WEqProperties_fun.diff_inter_empty [lemma, in diff_inter_empty]
WEqProperties_fun.BasicProperties.y [variable, in y]
WEqProperties_fun.choose_mem_1 [lemma, in choose_mem_1]
WEqProperties_fun.add_mem_3 [lemma, in add_mem_3]
WEqProperties_fun.union_add [lemma, in union_add]
WEqProperties_fun.add_mem_2 [lemma, in add_mem_2]
WEqProperties_fun.exclusive_set [lemma, in exclusive_set]
WEqProperties_fun.for_all_mem_4 [lemma, in for_all_mem_4]
WEqProperties_fun.MP [module, in WEqProperties_fun.MP]
WEqProperties_fun.Fold.Ass [variable, in Ass]
WEqProperties_fun.inter_subset_1 [lemma, in inter_subset_1]
WEqProperties_fun.Bool'.Comp [variable, in Comp]
WEqProperties_fun.Bool.Comp [variable, in Comp]
WEqProperties_fun.Fold.Comp [variable, in Comp]
WEqProperties_fun.equal_refl [lemma, in equal_refl]
WEqProperties_fun.Fold.A [variable, in A]
WEqProperties_fun.inter_add_2 [lemma, in inter_add_2]
WEqProperties_fun.set_rec [lemma, in set_rec]
WEqProperties_fun.BasicProperties [section, in BasicProperties]
WEqProperties_fun.exists_filter [lemma, in exists_filter]
WEqProperties_fun.inter_equal_1 [lemma, in inter_equal_1]
WEqProperties_fun.singleton_equal_add [lemma, in singleton_equal_add]
WEqProperties_fun.exists_mem_4 [lemma, in exists_mem_4]
WEqProperties_fun.remove_mem_2 [lemma, in remove_mem_2]
WEqProperties_fun.for_all_exists [lemma, in for_all_exists]
WEqProperties_fun.add_fold [lemma, in add_fold]
WEqProperties_fun.Fold [section, in Fold]
WEqProperties_fun.add_equal [lemma, in add_equal]
WEqProperties_fun.union_assoc [lemma, in union_assoc]
WEqProperties_fun.for_all_mem_1 [lemma, in for_all_mem_1]
WEqProperties_fun.inter_mem [lemma, in inter_mem]
WEqProperties_fun.union_inter_1 [lemma, in union_inter_1]
WEqProperties_fun.subset_refl [lemma, in subset_refl]
WEqProperties_fun [module, in WEqProperties_fun]
WEqProperties_fun.fold_equal [lemma, in fold_equal]
WEqProperties_fun.inter_subset_3 [lemma, in inter_subset_3]
WEqProperties_fun.add_cardinal_1 [lemma, in add_cardinal_1]
WEqProperties_fun.remove_mem_1 [lemma, in remove_mem_1]
WEqProperties_fun.Sum [section, in Sum]
WEqProperties_fun.BasicProperties.z [variable, in z]
WEqProperties_fun.union_equal_2 [lemma, in union_equal_2]
WEqProperties_fun.remove_mem_3 [lemma, in remove_mem_3]
WF [definition, in WF]
Wf [library]
Wf [library]
WFacts [module, in WFacts]
WFacts [module, in WFacts]
WFacts [module, in WFacts]
WFactsOn [module, in WFactsOn]
WFactsOn.add_s_m [instance, in add_s_m]
WFactsOn.add_neq_b [lemma, in add_neq_b]
WFactsOn.add_b [lemma, in add_b]
WFactsOn.add_1 [lemma, in add_1]
WFactsOn.add_m [instance, in add_m]
WFactsOn.add_iff [lemma, in add_iff]
WFactsOn.add_2 [lemma, in add_2]
WFactsOn.add_neq_iff [lemma, in add_neq_iff]
WFactsOn.add_3 [lemma, in add_3]
WFactsOn.BoolSpec [section, in BoolSpec]
WFactsOn.BoolSpec.f [variable, in f]
WFactsOn.BoolSpec.s [variable, in s]
WFactsOn.BoolSpec.s' [variable, in s']
WFactsOn.BoolSpec.s'' [variable, in s'']
WFactsOn.BoolSpec.x [variable, in x]
WFactsOn.BoolSpec.y [variable, in y]
WFactsOn.BoolSpec.z [variable, in z]
WFactsOn.cardinal_1 [abbreviation, in cardinal_1]
WFactsOn.choose_1 [abbreviation, in choose_1]
WFactsOn.choose_2 [abbreviation, in choose_2]
WFactsOn.compatb [abbreviation, in compatb]
WFactsOn.diff_m [instance, in diff_m]
WFactsOn.diff_iff [abbreviation, in diff_iff]
WFactsOn.diff_2 [lemma, in diff_2]
WFactsOn.diff_1 [lemma, in diff_1]
WFactsOn.diff_s_m [instance, in diff_s_m]
WFactsOn.diff_3 [lemma, in diff_3]
WFactsOn.diff_b [lemma, in diff_b]
WFactsOn.elements_iff [lemma, in elements_iff]
WFactsOn.elements_3w [abbreviation, in elements_3w]
WFactsOn.elements_b [lemma, in elements_b]
WFactsOn.elements_1 [lemma, in elements_1]
WFactsOn.elements_2 [lemma, in elements_2]
WFactsOn.Empty_s_m [instance, in Empty_s_m]
WFactsOn.Empty_m [instance, in Empty_m]
WFactsOn.empty_iff [lemma, in empty_iff]
WFactsOn.empty_1 [abbreviation, in empty_1]
WFactsOn.empty_b [lemma, in empty_b]
WFactsOn.eqb [definition, in eqb]
WFactsOn.equal_2 [lemma, in equal_2]
WFactsOn.equal_1 [lemma, in equal_1]
WFactsOn.equal_iff [lemma, in equal_iff]
WFactsOn.equal_m [instance, in equal_m]
WFactsOn.eq_dec [abbreviation, in eq_dec]
WFactsOn.exists_b [lemma, in exists_b]
WFactsOn.exists_1 [lemma, in exists_1]
WFactsOn.exists_2 [lemma, in exists_2]
WFactsOn.exists_iff [lemma, in exists_iff]
WFactsOn.filter_iff [abbreviation, in filter_iff]
WFactsOn.filter_1 [lemma, in filter_1]
WFactsOn.filter_ext [lemma, in filter_ext]
WFactsOn.filter_b [lemma, in filter_b]
WFactsOn.filter_3 [lemma, in filter_3]
WFactsOn.filter_subset [instance, in filter_subset]
WFactsOn.filter_2 [lemma, in filter_2]
WFactsOn.filter_equal [instance, in filter_equal]
WFactsOn.fold_1 [abbreviation, in fold_1]
WFactsOn.for_all_1 [lemma, in for_all_1]
WFactsOn.for_all_b [lemma, in for_all_b]
WFactsOn.for_all_2 [lemma, in for_all_2]
WFactsOn.for_all_iff [lemma, in for_all_iff]
WFactsOn.IffSpec [section, in IffSpec]
WFactsOn.IffSpec.f [variable, in f]
WFactsOn.IffSpec.s [variable, in s]
WFactsOn.IffSpec.s' [variable, in s']
WFactsOn.IffSpec.s'' [variable, in s'']
WFactsOn.IffSpec.x [variable, in x]
WFactsOn.IffSpec.y [variable, in y]
WFactsOn.IffSpec.z [variable, in z]
WFactsOn.ImplSpec [section, in ImplSpec]
WFactsOn.ImplSpec.f [variable, in f]
WFactsOn.ImplSpec.s [variable, in s]
WFactsOn.ImplSpec.s' [variable, in s']
WFactsOn.ImplSpec.x [variable, in x]
WFactsOn.ImplSpec.y [variable, in y]
WFactsOn.inter_b [lemma, in inter_b]
WFactsOn.inter_3 [lemma, in inter_3]
WFactsOn.inter_2 [lemma, in inter_2]
WFactsOn.inter_m [instance, in inter_m]
WFactsOn.inter_s_m [instance, in inter_s_m]
WFactsOn.inter_1 [lemma, in inter_1]
WFactsOn.inter_iff [abbreviation, in inter_iff]
WFactsOn.In_m [instance, in In_m]
WFactsOn.In_1 [lemma, in In_1]
WFactsOn.In_s_m [instance, in In_s_m]
WFactsOn.In_eq_iff [lemma, in In_eq_iff]
WFactsOn.is_empty_m [instance, in is_empty_m]
WFactsOn.is_empty_iff [lemma, in is_empty_iff]
WFactsOn.is_empty_1 [lemma, in is_empty_1]
WFactsOn.is_empty_2 [lemma, in is_empty_2]
WFactsOn.mem_1 [lemma, in mem_1]
WFactsOn.mem_2 [lemma, in mem_2]
WFactsOn.mem_b [lemma, in mem_b]
WFactsOn.mem_iff [lemma, in mem_iff]
WFactsOn.mem_m [instance, in mem_m]
WFactsOn.not_mem_iff [lemma, in not_mem_iff]
WFactsOn.partition_1 [abbreviation, in partition_1]
WFactsOn.partition_2 [abbreviation, in partition_2]
WFactsOn.remove_s_m [instance, in remove_s_m]
WFactsOn.remove_b [lemma, in remove_b]
WFactsOn.remove_2 [lemma, in remove_2]
WFactsOn.remove_neq_b [lemma, in remove_neq_b]
WFactsOn.remove_neq_iff [lemma, in remove_neq_iff]
WFactsOn.remove_1 [lemma, in remove_1]
WFactsOn.remove_3 [lemma, in remove_3]
WFactsOn.remove_m [instance, in remove_m]
WFactsOn.remove_iff [lemma, in remove_iff]
WFactsOn.singleton_iff [lemma, in singleton_iff]
WFactsOn.singleton_1 [lemma, in singleton_1]
WFactsOn.singleton_2 [lemma, in singleton_2]
WFactsOn.singleton_b [lemma, in singleton_b]
WFactsOn.singleton_m [instance, in singleton_m]
WFactsOn.SubsetSetoid [instance, in SubsetSetoid]
WFactsOn.subset_iff [lemma, in subset_iff]
WFactsOn.Subset_refl [definition, in Subset_refl]
WFactsOn.subset_m [instance, in subset_m]
WFactsOn.subset_2 [lemma, in subset_2]
WFactsOn.Subset_m [instance, in Subset_m]
WFactsOn.Subset_trans [definition, in Subset_trans]
WFactsOn.subset_1 [lemma, in subset_1]
WFactsOn.union_1 [lemma, in union_1]
WFactsOn.union_s_m [instance, in union_s_m]
WFactsOn.union_b [lemma, in union_b]
WFactsOn.union_2 [lemma, in union_2]
WFactsOn.union_iff [abbreviation, in union_iff]
WFactsOn.union_3 [lemma, in union_3]
WFactsOn.union_m [instance, in union_m]
WFacts_fun.eqb [definition, in eqb]
WFacts_fun.eqb [definition, in eqb]
WFacts_fun.In_iff [lemma, in In_iff]
WFacts_fun.diff_m [instance, in diff_m]
WFacts_fun.inter_b [lemma, in inter_b]
WFacts_fun.Equalities [section, in Equalities]
WFacts_fun.exists_b [lemma, in exists_b]
WFacts_fun.elements_o [lemma, in elements_o]
WFacts_fun.not_find_mapsto_iff [abbreviation, in not_find_mapsto_iff]
WFacts_fun.In_m [instance, in In_m]
WFacts_fun.subset_iff [lemma, in subset_iff]
WFacts_fun.empty_mapsto_iff [lemma, in empty_mapsto_iff]
WFacts_fun.mapi_mapsto_iff [lemma, in mapi_mapsto_iff]
WFacts_fun.remove_neq_mapsto_iff [lemma, in remove_neq_mapsto_iff]
WFacts_fun.Equal_refl [lemma, in Equal_refl]
WFacts_fun.mapi_inv [lemma, in mapi_inv]
WFacts_fun.BoolSpec.s' [variable, in s']
WFacts_fun.IffSpec.s' [variable, in s']
WFacts_fun.Subset_refl [lemma, in Subset_refl]
WFacts_fun.for_all_b [lemma, in for_all_b]
WFacts_fun.option_map [definition, in option_map]
WFacts_fun.add_neq_mapsto_iff [lemma, in add_neq_mapsto_iff]
WFacts_fun.map2_1bis [lemma, in map2_1bis]
WFacts_fun.add_neq_b [lemma, in add_neq_b]
WFacts_fun.add_neq_b [lemma, in add_neq_b]
WFacts_fun.subset_m [instance, in subset_m]
WFacts_fun.not_mem_iff [lemma, in not_mem_iff]
WFacts_fun.remove_mapsto_iff [lemma, in remove_mapsto_iff]
WFacts_fun.singleton_iff [lemma, in singleton_iff]
WFacts_fun.add_b [lemma, in add_b]
WFacts_fun.add_b [lemma, in add_b]
WFacts_fun.remove_b [lemma, in remove_b]
WFacts_fun.remove_b [lemma, in remove_b]
WFacts_fun.map_in_iff [lemma, in map_in_iff]
WFacts_fun.empty_a [lemma, in empty_a]
WFacts_fun.remove_eq_o [lemma, in remove_eq_o]
WFacts_fun.add_m [instance, in add_m]
WFacts_fun.compat_cmp [definition, in compat_cmp]
WFacts_fun.mapi_1bis [lemma, in mapi_1bis]
WFacts_fun.is_empty_m [instance, in is_empty_m]
WFacts_fun.elements_iff [lemma, in elements_iff]
WFacts_fun.BoolSpec.s [variable, in s]
WFacts_fun.IffSpec.s [variable, in s]
WFacts_fun.mem_find_b [lemma, in mem_find_b]
WFacts_fun.Equal_sym [lemma, in Equal_sym]
WFacts_fun.BoolSpec.elt' [variable, in elt']
WFacts_fun.IffSpec.elt' [variable, in elt']
WFacts_fun.Equal_Equivb [lemma, in Equal_Equivb]
WFacts_fun.remove_neq_b [lemma, in remove_neq_b]
WFacts_fun.remove_neq_b [lemma, in remove_neq_b]
WFacts_fun.map_b [lemma, in map_b]
WFacts_fun.eq_option_alt [lemma, in eq_option_alt]
WFacts_fun.E_ST [instance, in E_ST]
WFacts_fun.union_b [lemma, in union_b]
WFacts_fun.BoolSpec [section, in BoolSpec]
WFacts_fun.BoolSpec [section, in BoolSpec]
WFacts_fun.not_find_in_iff [lemma, in not_find_in_iff]
WFacts_fun.remove_neq_iff [lemma, in remove_neq_iff]
WFacts_fun.add_neq_in_iff [lemma, in add_neq_in_iff]
WFacts_fun.diff_iff [lemma, in diff_iff]
WFacts_fun.find_mapsto_iff [lemma, in find_mapsto_iff]
WFacts_fun.filter_iff [lemma, in filter_iff]
WFacts_fun.remove_o [lemma, in remove_o]
WFacts_fun.add_in_iff [lemma, in add_in_iff]
WFacts_fun.mapi_o [lemma, in mapi_o]
WFacts_fun.Equalities.Cmp [section, in Cmp]
WFacts_fun.elements_in_iff [lemma, in elements_in_iff]
WFacts_fun.is_empty_iff [lemma, in is_empty_iff]
WFacts_fun.is_empty_iff [lemma, in is_empty_iff]
WFacts_fun.BoolSpec.f [variable, in f]
WFacts_fun.IffSpec.f [variable, in f]
WFacts_fun.inter_m [instance, in inter_m]
WFacts_fun.add_eq_b [lemma, in add_eq_b]
WFacts_fun.IffSpec [section, in IffSpec]
WFacts_fun.IffSpec [section, in IffSpec]
WFacts_fun.Equalities.elt [variable, in elt]
WFacts_fun.BoolSpec.elt [variable, in elt]
WFacts_fun.IffSpec.elt [variable, in elt]
WFacts_fun.eq_bool_alt [lemma, in eq_bool_alt]
WFacts_fun.mapi_in_iff [lemma, in mapi_in_iff]
WFacts_fun.Equalities.Cmp.cmp [variable, in cmp]
WFacts_fun.elements_b [lemma, in elements_b]
WFacts_fun.elements_b [lemma, in elements_b]
WFacts_fun.Equalities.Cmp.eq_elt [variable, in eq_elt]
WFacts_fun.union_iff [lemma, in union_iff]
WFacts_fun.find_o [lemma, in find_o]
WFacts_fun.empty_o [lemma, in empty_o]
WFacts_fun.in_find_iff [lemma, in in_find_iff]
WFacts_fun.map_o [lemma, in map_o]
WFacts_fun.mapi_b [lemma, in mapi_b]
WFacts_fun.for_all_iff [lemma, in for_all_iff]
WFacts_fun.filter_ext [lemma, in filter_ext]
WFacts_fun.MapsTo_iff [lemma, in MapsTo_iff]
WFacts_fun.Equal_ST [instance, in Equal_ST]
WFacts_fun.Equal_ST [definition, in Equal_ST]
WFacts_fun.add_mapsto_iff [lemma, in add_mapsto_iff]
WFacts_fun.remove_eq_b [lemma, in remove_eq_b]
WFacts_fun.elements_mapsto_iff [lemma, in elements_mapsto_iff]
WFacts_fun.filter_b [lemma, in filter_b]
WFacts_fun.BoolSpec.x [variable, in x]
WFacts_fun.IffSpec.x [variable, in x]
WFacts_fun.Subset_m [instance, in Subset_m]
WFacts_fun.Subset_trans [lemma, in Subset_trans]
WFacts_fun.add_iff [lemma, in add_iff]
WFacts_fun.Equal_Equivb_eqdec [lemma, in Equal_Equivb_eqdec]
WFacts_fun.Equal_Equiv [lemma, in Equal_Equiv]
WFacts_fun.BoolSpec.s'' [variable, in s'']
WFacts_fun.IffSpec.s'' [variable, in s'']
WFacts_fun.equal_iff [lemma, in equal_iff]
WFacts_fun.equal_iff [lemma, in equal_iff]
WFacts_fun.add_eq_o [lemma, in add_eq_o]
WFacts_fun.Empty_m [instance, in Empty_m]
WFacts_fun.add_neq_o [lemma, in add_neq_o]
WFacts_fun.Equal_trans [lemma, in Equal_trans]
WFacts_fun.remove_m [instance, in remove_m]
WFacts_fun.add_neq_iff [lemma, in add_neq_iff]
WFacts_fun.BoolSpec.y [variable, in y]
WFacts_fun.IffSpec.y [variable, in y]
WFacts_fun.remove_neq_in_iff [lemma, in remove_neq_in_iff]
WFacts_fun.map_mapsto_iff [lemma, in map_mapsto_iff]
WFacts_fun.filter_subset [lemma, in filter_subset]
WFacts_fun.mem_b [lemma, in mem_b]
WFacts_fun.mem_b [lemma, in mem_b]
WFacts_fun.exists_iff [lemma, in exists_iff]
WFacts_fun.remove_iff [lemma, in remove_iff]
WFacts_fun.add_o [lemma, in add_o]
WFacts_fun.eq_dec [abbreviation, in eq_dec]
WFacts_fun.eq_dec [abbreviation, in eq_dec]
WFacts_fun.not_mem_in_iff [lemma, in not_mem_in_iff]
WFacts_fun.mem_in_iff [lemma, in mem_in_iff]
WFacts_fun.Equal_mapsto_iff [lemma, in Equal_mapsto_iff]
WFacts_fun.singleton_b [lemma, in singleton_b]
WFacts_fun.mem_iff [lemma, in mem_iff]
WFacts_fun.empty_iff [lemma, in empty_iff]
WFacts_fun.mem_m [instance, in mem_m]
WFacts_fun.union_m [instance, in union_m]
WFacts_fun.Equiv_Equivb [lemma, in Equiv_Equivb]
WFacts_fun.BoolSpec.elt'' [variable, in elt'']
WFacts_fun.IffSpec.elt'' [variable, in elt'']
WFacts_fun.empty_in_iff [lemma, in empty_in_iff]
WFacts_fun.inter_iff [lemma, in inter_iff]
WFacts_fun.In_s_m [instance, in In_s_m]
WFacts_fun.empty_b [lemma, in empty_b]
WFacts_fun.remove_neq_o [lemma, in remove_neq_o]
WFacts_fun.remove_in_iff [lemma, in remove_in_iff]
WFacts_fun.singleton_m [instance, in singleton_m]
WFacts_fun.filter_equal [lemma, in filter_equal]
WFacts_fun.MapsTo_fun [lemma, in MapsTo_fun]
WFacts_fun [module, in WFacts_fun]
WFacts_fun [module, in WFacts_fun]
WFacts_fun.In_dec [lemma, in In_dec]
WFacts_fun.diff_b [lemma, in diff_b]
WFacts_fun.BoolSpec.z [variable, in z]
WFacts_fun.IffSpec.z [variable, in z]
WFacts_fun.In_eq_iff [lemma, in In_eq_iff]
WFacts_fun.equal_m [instance, in equal_m]
WfExtensionality [module, in WfExtensionality]
WfExtensionality.fix_sub_eq_ext [lemma, in fix_sub_eq_ext]
WfInclusion [section, in WfInclusion]
WfInclusion.A [variable, in A]
WfInclusion.R1 [variable, in R1]
WfInclusion.R2 [variable, in R2]
WfLexicographic_Product.leA [variable, in leA]
WfLexicographic_Product.B [variable, in B]
WfLexicographic_Product [section, in WfLexicographic_Product]
WfLexicographic_Product.A [variable, in A]
WfLexicographic_Product.leB [variable, in leB]
WfUnion [section, in WfUnion]
WfUnion.A [variable, in A]
WfUnion.R1 [variable, in R1]
WfUnion.R2 [variable, in R2]
wf_WO [lemma, in wf_WO]
wf_disjoint_sum [lemma, in wf_disjoint_sum]
Wf_Lexicographic_Exponentiation [section, in Wf_Lexicographic_Exponentiation]
wf_symprod [lemma, in wf_symprod]
Wf_Symmetric_Product.leA [variable, in leA]
Wf_Lexicographic_Exponentiation.leA [variable, in leA]
Wf_Disjoint_Union.leA [variable, in leA]
Wf_Symmetric_Product.B [variable, in B]
Wf_Disjoint_Union.B [variable, in B]
wf_lex_exp [lemma, in wf_lex_exp]
wf_clos_trans [lemma, in wf_clos_trans]
Wf_Transitive_Closure.R [variable, in R]
wf_inverse_image [lemma, in wf_inverse_image]
wf_proof_up.f [variable, in f]
wf_proof.f [variable, in f]
wf_incl [lemma, in wf_incl]
wf_lexprod [lemma, in wf_lexprod]
Wf_Disjoint_Union [section, in Wf_Disjoint_Union]
Wf_Symmetric_Product [section, in Wf_Symmetric_Product]
wf_proof_up [section, in wf_proof_up]
Wf_Transitive_Closure [section, in Wf_Transitive_Closure]
wf_swapprod [lemma, in wf_swapprod]
wf_proof_up.c [variable, in c]
wf_proof.c [variable, in c]
wf_proof [section, in wf_proof]
Wf_Transitive_Closure.A [variable, in A]
Wf_Symmetric_Product.A [variable, in A]
Wf_Lexicographic_Exponentiation.A [variable, in A]
Wf_Disjoint_Union.A [variable, in A]
wf_union [lemma, in wf_union]
wf_inverse_rel [lemma, in wf_inverse_rel]
Wf_Symmetric_Product.leB [variable, in leB]
Wf_Disjoint_Union.leB [variable, in leB]
<< _ , _ >> [notation, in ::'<<'_x_','_x_'>>']
Wf_nat [library]
Wf_Z [library]
Wn_decreasing [lemma, in Wn_decreasing]
WO [inductive, in WO]
wof [definition, in wof]
WOps [module, in WOps]
WOps.elt [definition, in elt]
WOps.t [axiom, in t]
word [definition, in word]
WProperties [module, in WProperties]
WProperties [module, in WProperties]
WProperties [module, in WProperties]
WPropertiesOn [module, in WPropertiesOn]
WPropertiesOn.Add [definition, in Add]
WPropertiesOn.add_remove [lemma, in add_remove]
WPropertiesOn.add_add [lemma, in add_add]
WPropertiesOn.add_union_singleton [lemma, in add_union_singleton]
WPropertiesOn.add_cardinal_2 [lemma, in add_cardinal_2]
WPropertiesOn.Add_Equal [lemma, in Add_Equal]
WPropertiesOn.Add_remove [lemma, in Add_remove]
WPropertiesOn.add_fold [lemma, in add_fold]
WPropertiesOn.Add_add [lemma, in Add_add]
WPropertiesOn.add_equal [lemma, in add_equal]
WPropertiesOn.add_cardinal_1 [lemma, in add_cardinal_1]
WPropertiesOn.BasicProperties [section, in BasicProperties]
WPropertiesOn.BasicProperties.s [variable, in s]
WPropertiesOn.BasicProperties.s' [variable, in s']
WPropertiesOn.BasicProperties.s'' [variable, in s'']
WPropertiesOn.BasicProperties.s1 [variable, in s1]
WPropertiesOn.BasicProperties.s2 [variable, in s2]
WPropertiesOn.BasicProperties.s3 [variable, in s3]
WPropertiesOn.BasicProperties.x [variable, in x]
WPropertiesOn.BasicProperties.x' [variable, in x']
WPropertiesOn.cardinal_inv_2b [lemma, in cardinal_inv_2b]
WPropertiesOn.cardinal_inv_1 [lemma, in cardinal_inv_1]
WPropertiesOn.cardinal_1 [lemma, in cardinal_1]
WPropertiesOn.cardinal_2 [lemma, in cardinal_2]
WPropertiesOn.cardinal_m [instance, in cardinal_m]
WPropertiesOn.cardinal_fold [lemma, in cardinal_fold]
WPropertiesOn.cardinal_0 [lemma, in cardinal_0]
WPropertiesOn.cardinal_inv_2 [lemma, in cardinal_inv_2]
WPropertiesOn.cardinal_Empty [lemma, in cardinal_Empty]
WPropertiesOn.Dec [module, in WPropertiesOn.Dec]
WPropertiesOn.diff_subset_equal [lemma, in diff_subset_equal]
WPropertiesOn.diff_inter_all [lemma, in diff_inter_all]
WPropertiesOn.diff_subset [lemma, in diff_subset]
WPropertiesOn.diff_inter_empty [lemma, in diff_inter_empty]
WPropertiesOn.diff_inter_cardinal [lemma, in diff_inter_cardinal]
WPropertiesOn.double_inclusion [lemma, in double_inclusion]
WPropertiesOn.elements_Empty [lemma, in elements_Empty]
WPropertiesOn.elements_empty [lemma, in elements_empty]
WPropertiesOn.empty_cardinal [lemma, in empty_cardinal]
WPropertiesOn.empty_inter_2 [lemma, in empty_inter_2]
WPropertiesOn.empty_inter_1 [lemma, in empty_inter_1]
WPropertiesOn.empty_diff_2 [lemma, in empty_diff_2]
WPropertiesOn.empty_is_empty_2 [lemma, in empty_is_empty_2]
WPropertiesOn.empty_is_empty_1 [lemma, in empty_is_empty_1]
WPropertiesOn.empty_diff_1 [lemma, in empty_diff_1]
WPropertiesOn.empty_union_1 [lemma, in empty_union_1]
WPropertiesOn.empty_union_2 [lemma, in empty_union_2]
WPropertiesOn.Equal_remove [lemma, in Equal_remove]
WPropertiesOn.equal_trans [lemma, in equal_trans]
WPropertiesOn.equal_sym [lemma, in equal_sym]
WPropertiesOn.equal_refl [lemma, in equal_refl]
WPropertiesOn.Equal_cardinal [lemma, in Equal_cardinal]
WPropertiesOn.FM [module, in WPropertiesOn.FM]
WPropertiesOn.Fold [section, in Fold]
WPropertiesOn.fold_0 [lemma, in fold_0]
WPropertiesOn.fold_empty [lemma, in fold_empty]
WPropertiesOn.fold_commutes [lemma, in fold_commutes]
WPropertiesOn.fold_rec_weak [lemma, in fold_rec_weak]
WPropertiesOn.fold_identity [lemma, in fold_identity]
WPropertiesOn.fold_diff_inter [lemma, in fold_diff_inter]
WPropertiesOn.fold_add [lemma, in fold_add]
WPropertiesOn.fold_rec_bis [lemma, in fold_rec_bis]
WPropertiesOn.fold_plus [lemma, in fold_plus]
WPropertiesOn.fold_init [lemma, in fold_init]
WPropertiesOn.fold_rec [lemma, in fold_rec]
WPropertiesOn.fold_rec_nodep [lemma, in fold_rec_nodep]
WPropertiesOn.fold_2 [lemma, in fold_2]
WPropertiesOn.fold_rel [lemma, in fold_rel]
WPropertiesOn.fold_union [lemma, in fold_union]
WPropertiesOn.fold_1 [lemma, in fold_1]
WPropertiesOn.fold_1b [lemma, in fold_1b]
WPropertiesOn.fold_spec_right [lemma, in fold_spec_right]
WPropertiesOn.fold_union_inter [lemma, in fold_union_inter]
WPropertiesOn.fold_equal [lemma, in fold_equal]
WPropertiesOn.Fold.Fold_More.eqA [variable, in eqA]
WPropertiesOn.Fold.Fold_More.st [variable, in st]
WPropertiesOn.Fold.Fold_More.f [variable, in f]
WPropertiesOn.Fold.Fold_More.Ass [variable, in Ass]
WPropertiesOn.Fold.Fold_More.Comp [variable, in Comp]
WPropertiesOn.Fold.Fold_More.A [variable, in A]
WPropertiesOn.Fold.Fold_More [section, in Fold_More]
WPropertiesOn.InA [abbreviation, in InA]
WPropertiesOn.inter_assoc [lemma, in inter_assoc]
WPropertiesOn.inter_equal_2 [lemma, in inter_equal_2]
WPropertiesOn.inter_subset_2 [lemma, in inter_subset_2]
WPropertiesOn.inter_subset_equal [lemma, in inter_subset_equal]
WPropertiesOn.inter_add_1 [lemma, in inter_add_1]
WPropertiesOn.inter_sym [lemma, in inter_sym]
WPropertiesOn.inter_subset_1 [lemma, in inter_subset_1]
WPropertiesOn.inter_add_2 [lemma, in inter_add_2]
WPropertiesOn.inter_equal_1 [lemma, in inter_equal_1]
WPropertiesOn.inter_Add_2 [lemma, in inter_Add_2]
WPropertiesOn.inter_Add [lemma, in inter_Add]
WPropertiesOn.inter_subset_3 [lemma, in inter_subset_3]
WPropertiesOn.in_subset [lemma, in in_subset]
WPropertiesOn.In_dec [lemma, in In_dec]
WPropertiesOn.NoDup [abbreviation, in NoDup]
WPropertiesOn.not_in_union [lemma, in not_in_union]
WPropertiesOn.of_list_2 [lemma, in of_list_2]
WPropertiesOn.of_list_3 [lemma, in of_list_3]
WPropertiesOn.of_list_1 [lemma, in of_list_1]
WPropertiesOn.of_list [definition, in of_list]
WPropertiesOn.remove_cardinal_1 [lemma, in remove_cardinal_1]
WPropertiesOn.remove_singleton_empty [lemma, in remove_singleton_empty]
WPropertiesOn.remove_add [lemma, in remove_add]
WPropertiesOn.remove_fold_2 [lemma, in remove_fold_2]
WPropertiesOn.remove_equal [lemma, in remove_equal]
WPropertiesOn.remove_fold_1 [lemma, in remove_fold_1]
WPropertiesOn.remove_cardinal_2 [lemma, in remove_cardinal_2]
WPropertiesOn.remove_diff_singleton [lemma, in remove_diff_singleton]
WPropertiesOn.set_induction_bis [lemma, in set_induction_bis]
WPropertiesOn.set_induction [lemma, in set_induction]
WPropertiesOn.singleton_cardinal [lemma, in singleton_cardinal]
WPropertiesOn.singleton_equal_add [lemma, in singleton_equal_add]
WPropertiesOn.subset_add_3 [lemma, in subset_add_3]
WPropertiesOn.subset_diff [lemma, in subset_diff]
WPropertiesOn.subset_cardinal_lt [lemma, in subset_cardinal_lt]
WPropertiesOn.subset_trans [lemma, in subset_trans]
WPropertiesOn.subset_empty [lemma, in subset_empty]
WPropertiesOn.subset_equal [lemma, in subset_equal]
WPropertiesOn.subset_add_2 [lemma, in subset_add_2]
WPropertiesOn.subset_cardinal [lemma, in subset_cardinal]
WPropertiesOn.subset_antisym [lemma, in subset_antisym]
WPropertiesOn.subset_remove_3 [lemma, in subset_remove_3]
WPropertiesOn.subset_refl [lemma, in subset_refl]
WPropertiesOn.to_list [definition, in to_list]
WPropertiesOn.union_subset_1 [lemma, in union_subset_1]
WPropertiesOn.union_inter_2 [lemma, in union_inter_2]
WPropertiesOn.union_sym [lemma, in union_sym]
WPropertiesOn.union_subset_5 [lemma, in union_subset_5]
WPropertiesOn.union_subset_3 [lemma, in union_subset_3]
WPropertiesOn.union_subset_2 [lemma, in union_subset_2]
WPropertiesOn.union_cardinal_inter [lemma, in union_cardinal_inter]
WPropertiesOn.union_subset_4 [lemma, in union_subset_4]
WPropertiesOn.union_remove_add_1 [lemma, in union_remove_add_1]
WPropertiesOn.union_cardinal [lemma, in union_cardinal]
WPropertiesOn.union_subset_equal [lemma, in union_subset_equal]
WPropertiesOn.union_equal_1 [lemma, in union_equal_1]
WPropertiesOn.union_inter_cardinal [lemma, in union_inter_cardinal]
WPropertiesOn.union_add [lemma, in union_add]
WPropertiesOn.union_Equal [lemma, in union_Equal]
WPropertiesOn.union_cardinal_le [lemma, in union_cardinal_le]
WPropertiesOn.union_Add [lemma, in union_Add]
WPropertiesOn.union_remove_add_2 [lemma, in union_remove_add_2]
WPropertiesOn.union_assoc [lemma, in union_assoc]
WPropertiesOn.union_inter_1 [lemma, in union_inter_1]
WPropertiesOn.union_equal_2 [lemma, in union_equal_2]
WProperties_fun.update_dec [lemma, in update_dec]
WProperties_fun.add_remove [lemma, in add_remove]
WProperties_fun.elements_Empty [lemma, in elements_Empty]
WProperties_fun.elements_Empty [lemma, in elements_Empty]
WProperties_fun [module, in WProperties_fun]
WProperties_fun [module, in WProperties_fun]
WProperties_fun.inter_assoc [lemma, in inter_assoc]
WProperties_fun.union_subset_1 [lemma, in union_subset_1]
WProperties_fun.diff_mapsto_iff [lemma, in diff_mapsto_iff]
WProperties_fun.fold_0 [lemma, in fold_0]
WProperties_fun.Partition_partition [lemma, in Partition_partition]
WProperties_fun.partition_Partition [lemma, in partition_Partition]
WProperties_fun.empty_cardinal [lemma, in empty_cardinal]
WProperties_fun.remove_cardinal_1 [lemma, in remove_cardinal_1]
WProperties_fun.remove_singleton_empty [lemma, in remove_singleton_empty]
WProperties_fun.inter_equal_2 [lemma, in inter_equal_2]
WProperties_fun.fold_empty [lemma, in fold_empty]
WProperties_fun.transpose_neqkey [definition, in transpose_neqkey]
WProperties_fun.update_in_iff [lemma, in update_in_iff]
WProperties_fun.fold_commutes [lemma, in fold_commutes]
WProperties_fun.fold_commutes [lemma, in fold_commutes]
WProperties_fun.BasicProperties.s' [variable, in s']
WProperties_fun.Fold.Fold_More.eqA [variable, in eqA]
WProperties_fun.Elt.Fold_More.eqA [variable, in eqA]
WProperties_fun.BasicProperties.s1 [variable, in s1]
WProperties_fun.subset_add_3 [lemma, in subset_add_3]
WProperties_fun.remove_add [lemma, in remove_add]
WProperties_fun.inter_subset_2 [lemma, in inter_subset_2]
WProperties_fun.Fold.Fold_More.st [variable, in st]
WProperties_fun.Elt.Fold_More.st [variable, in st]
WProperties_fun.of_list_2 [lemma, in of_list_2]
WProperties_fun.of_list_2 [lemma, in of_list_2]
WProperties_fun.add_add [lemma, in add_add]
WProperties_fun.union_inter_2 [lemma, in union_inter_2]
WProperties_fun.Partition_Empty [lemma, in Partition_Empty]
WProperties_fun.union_sym [lemma, in union_sym]
WProperties_fun.add_union_singleton [lemma, in add_union_singleton]
WProperties_fun.eqke_equiv [instance, in eqke_equiv]
WProperties_fun.inter_subset_equal [lemma, in inter_subset_equal]
WProperties_fun.fold_rec_weak [lemma, in fold_rec_weak]
WProperties_fun.fold_rec_weak [lemma, in fold_rec_weak]
WProperties_fun.diff_in_iff [lemma, in diff_in_iff]
WProperties_fun.fold_identity [lemma, in fold_identity]
WProperties_fun.fold_identity [lemma, in fold_identity]
WProperties_fun.diff_subset_equal [lemma, in diff_subset_equal]
WProperties_fun.diff_inter_all [lemma, in diff_inter_all]
WProperties_fun.cardinal_inv_2b [lemma, in cardinal_inv_2b]
WProperties_fun.cardinal_inv_2b [lemma, in cardinal_inv_2b]
WProperties_fun.BasicProperties.s2 [variable, in s2]
WProperties_fun.Dec [module, in WProperties_fun.Dec]
WProperties_fun.subset_diff [lemma, in subset_diff]
WProperties_fun.exists_ [definition, in exists_]
WProperties_fun.subset_cardinal_lt [lemma, in subset_cardinal_lt]
WProperties_fun.cardinal_inv_1 [lemma, in cardinal_inv_1]
WProperties_fun.cardinal_inv_1 [lemma, in cardinal_inv_1]
WProperties_fun.BasicProperties.s [variable, in s]
WProperties_fun.to_list [definition, in to_list]
WProperties_fun.to_list [definition, in to_list]
WProperties_fun.cardinal_1 [lemma, in cardinal_1]
WProperties_fun.cardinal_1 [lemma, in cardinal_1]
WProperties_fun.remove_fold_2 [lemma, in remove_fold_2]
WProperties_fun.set_induction_bis [lemma, in set_induction_bis]
WProperties_fun.Add [definition, in Add]
WProperties_fun.Add [definition, in Add]
WProperties_fun.BasicProperties.x' [variable, in x']
WProperties_fun.remove_equal [lemma, in remove_equal]
WProperties_fun.subset_trans [lemma, in subset_trans]
WProperties_fun.add_cardinal_2 [lemma, in add_cardinal_2]
WProperties_fun.filter_range [definition, in filter_range]
WProperties_fun.fold_diff_inter [lemma, in fold_diff_inter]
WProperties_fun.fold_add [lemma, in fold_add]
WProperties_fun.fold_add [lemma, in fold_add]
WProperties_fun.elements_empty [lemma, in elements_empty]
WProperties_fun.elements_empty [lemma, in elements_empty]
WProperties_fun.union_subset_5 [lemma, in union_subset_5]
WProperties_fun.of_list_1b [lemma, in of_list_1b]
WProperties_fun.union_subset_3 [lemma, in union_subset_3]
WProperties_fun.union_subset_2 [lemma, in union_subset_2]
WProperties_fun.union_cardinal_inter [lemma, in union_cardinal_inter]
WProperties_fun.partition [definition, in partition]
WProperties_fun.update [definition, in update]
WProperties_fun.Disjoint [definition, in Disjoint]
WProperties_fun.fold_rec_bis [lemma, in fold_rec_bis]
WProperties_fun.fold_rec_bis [lemma, in fold_rec_bis]
WProperties_fun.fold_plus [lemma, in fold_plus]
WProperties_fun.NoDupA_eqk_eqke [lemma, in NoDupA_eqk_eqke]
WProperties_fun.subset_empty [lemma, in subset_empty]
WProperties_fun.remove_fold_1 [lemma, in remove_fold_1]
WProperties_fun.exists_dom [definition, in exists_dom]
WProperties_fun.fold_Add [lemma, in fold_Add]
WProperties_fun.eqke [abbreviation, in eqke]
WProperties_fun.Partition_Add [lemma, in Partition_Add]
WProperties_fun.of_list_3 [lemma, in of_list_3]
WProperties_fun.of_list_3 [lemma, in of_list_3]
WProperties_fun.FM [module, in WProperties_fun.FM]
WProperties_fun.remove_cardinal_2 [lemma, in remove_cardinal_2]
WProperties_fun.filter_iff [lemma, in filter_iff]
WProperties_fun.Elt.Specs [section, in Specs]
WProperties_fun.subset_equal [lemma, in subset_equal]
WProperties_fun.Add_Equal [lemma, in Add_Equal]
WProperties_fun.of_list_1 [lemma, in of_list_1]
WProperties_fun.of_list_1 [lemma, in of_list_1]
WProperties_fun.fold_init [lemma, in fold_init]
WProperties_fun.fold_init [lemma, in fold_init]
WProperties_fun.filter [definition, in filter]
WProperties_fun.fold_rec [lemma, in fold_rec]
WProperties_fun.fold_rec [lemma, in fold_rec]
WProperties_fun.diff_subset [lemma, in diff_subset]
WProperties_fun.union_subset_4 [lemma, in union_subset_4]
WProperties_fun.Fold.Fold_More.f [variable, in f]
WProperties_fun.Elt.Partition.f [variable, in f]
WProperties_fun.Elt.Specs.f [variable, in f]
WProperties_fun.Elt.Fold_More.f [variable, in f]
WProperties_fun.union_remove_add_1 [lemma, in union_remove_add_1]
WProperties_fun.of_list [definition, in of_list]
WProperties_fun.of_list [definition, in of_list]
WProperties_fun.Elt.elt [variable, in elt]
WProperties_fun.cardinal_2 [lemma, in cardinal_2]
WProperties_fun.cardinal_2 [lemma, in cardinal_2]
WProperties_fun.set_induction [lemma, in set_induction]
WProperties_fun.for_all_dom [definition, in for_all_dom]
WProperties_fun.filter_dom [definition, in filter_dom]
WProperties_fun.InA_eqke_eqk [lemma, in InA_eqke_eqk]
WProperties_fun.union_cardinal [lemma, in union_cardinal]
WProperties_fun.fold_rec_nodep [lemma, in fold_rec_nodep]
WProperties_fun.fold_rec_nodep [lemma, in fold_rec_nodep]
WProperties_fun.fold_2 [lemma, in fold_2]
WProperties_fun.inter_add_1 [lemma, in inter_add_1]
WProperties_fun.diff [definition, in diff]
WProperties_fun.for_all_iff [lemma, in for_all_iff]
WProperties_fun.subset_add_2 [lemma, in subset_add_2]
WProperties_fun.fold_rel [lemma, in fold_rel]
WProperties_fun.fold_rel [lemma, in fold_rel]
WProperties_fun.Equal_remove [lemma, in Equal_remove]
WProperties_fun.cardinal_fold [lemma, in cardinal_fold]
WProperties_fun.cardinal_fold [lemma, in cardinal_fold]
WProperties_fun.exists_range [definition, in exists_range]
WProperties_fun.map_induction [lemma, in map_induction]
WProperties_fun.inter_sym [lemma, in inter_sym]
WProperties_fun.fold_Empty [lemma, in fold_Empty]
WProperties_fun.BasicProperties.x [variable, in x]
WProperties_fun.empty_inter_2 [lemma, in empty_inter_2]
WProperties_fun.map_induction_bis [lemma, in map_induction_bis]
WProperties_fun.Elt.Partition.Hf [variable, in Hf]
WProperties_fun.Elt.Specs.Hf [variable, in Hf]
WProperties_fun.subset_cardinal [lemma, in subset_cardinal]
WProperties_fun.Partition_cardinal [lemma, in Partition_cardinal]
WProperties_fun.Disjoint_sym [lemma, in Disjoint_sym]
WProperties_fun.BasicProperties.s3 [variable, in s3]
WProperties_fun.empty_inter_1 [lemma, in empty_inter_1]
WProperties_fun.BasicProperties.s'' [variable, in s'']
WProperties_fun.Elt.Partition [section, in Partition]
WProperties_fun.Partition [definition, in Partition]
WProperties_fun.union_subset_equal [lemma, in union_subset_equal]
WProperties_fun.findA_rev [lemma, in findA_rev]
WProperties_fun.fold_union [lemma, in fold_union]
WProperties_fun.Elt.Fold_More.Tra [variable, in Tra]
WProperties_fun.empty_diff_2 [lemma, in empty_diff_2]
WProperties_fun.restrict_mapsto_iff [lemma, in restrict_mapsto_iff]
WProperties_fun.empty_is_empty_2 [lemma, in empty_is_empty_2]
WProperties_fun.union_equal_1 [lemma, in union_equal_1]
WProperties_fun.subset_antisym [lemma, in subset_antisym]
WProperties_fun.equal_trans [lemma, in equal_trans]
WProperties_fun.partition_iff_1 [lemma, in partition_iff_1]
WProperties_fun.empty_is_empty_1 [lemma, in empty_is_empty_1]
WProperties_fun.equal_sym [lemma, in equal_sym]
WProperties_fun.Partition_fold [lemma, in Partition_fold]
WProperties_fun.restrict [definition, in restrict]
WProperties_fun.diff_inter_empty [lemma, in diff_inter_empty]
WProperties_fun.cardinal_0 [lemma, in cardinal_0]
WProperties_fun.union_inter_cardinal [lemma, in union_inter_cardinal]
WProperties_fun.singleton_cardinal [lemma, in singleton_cardinal]
WProperties_fun.uncurry [definition, in uncurry]
WProperties_fun.F [module, in WProperties_fun.F]
WProperties_fun.union_add [lemma, in union_add]
WProperties_fun.fold_1 [lemma, in fold_1]
WProperties_fun.exists_iff [lemma, in exists_iff]
WProperties_fun.empty_diff_1 [lemma, in empty_diff_1]
WProperties_fun.Fold.Fold_More.Ass [variable, in Ass]
WProperties_fun.restrict_in_iff [lemma, in restrict_in_iff]
WProperties_fun.update_mapsto_iff [lemma, in update_mapsto_iff]
WProperties_fun.Add_remove [lemma, in Add_remove]
WProperties_fun.union_Equal [lemma, in union_Equal]
WProperties_fun.inter_subset_1 [lemma, in inter_subset_1]
WProperties_fun.Fold.Fold_More.Comp [variable, in Comp]
WProperties_fun.Elt.Fold_More.Comp [variable, in Comp]
WProperties_fun.fold_1b [lemma, in fold_1b]
WProperties_fun.equal_refl [lemma, in equal_refl]
WProperties_fun.empty_union_1 [lemma, in empty_union_1]
WProperties_fun.partition_iff_2 [lemma, in partition_iff_2]
WProperties_fun.Fold.Fold_More.A [variable, in A]
WProperties_fun.Elt.Fold_More.A [variable, in A]
WProperties_fun.Partition_In [lemma, in Partition_In]
WProperties_fun.Disjoint_alt [lemma, in Disjoint_alt]
WProperties_fun.inter_add_2 [lemma, in inter_add_2]
WProperties_fun.Partition_sym [lemma, in Partition_sym]
WProperties_fun.union_cardinal_le [lemma, in union_cardinal_le]
WProperties_fun.BasicProperties [section, in BasicProperties]
WProperties_fun.subset_remove_3 [lemma, in subset_remove_3]
WProperties_fun.diff_inter_cardinal [lemma, in diff_inter_cardinal]
WProperties_fun.inter_equal_1 [lemma, in inter_equal_1]
WProperties_fun.singleton_equal_add [lemma, in singleton_equal_add]
WProperties_fun.union_Add [lemma, in union_Add]
WProperties_fun.for_all [definition, in for_all]
WProperties_fun.partition_dom [definition, in partition_dom]
WProperties_fun.eqk_equiv [instance, in eqk_equiv]
WProperties_fun.fold_spec_right [lemma, in fold_spec_right]
WProperties_fun.fold_spec_right [lemma, in fold_spec_right]
WProperties_fun.empty_union_2 [lemma, in empty_union_2]
WProperties_fun.partition_range [definition, in partition_range]
WProperties_fun.inter_Add_2 [lemma, in inter_Add_2]
WProperties_fun.add_fold [lemma, in add_fold]
WProperties_fun.eqk [abbreviation, in eqk]
WProperties_fun.Equal_cardinal [lemma, in Equal_cardinal]
WProperties_fun.Equal_cardinal [lemma, in Equal_cardinal]
WProperties_fun.NoDup [abbreviation, in NoDup]
WProperties_fun.double_inclusion [lemma, in double_inclusion]
WProperties_fun.fold_Equal [lemma, in fold_Equal]
WProperties_fun.Add_add [lemma, in Add_add]
WProperties_fun.Fold [section, in Fold]
WProperties_fun.for_all_range [definition, in for_all_range]
WProperties_fun.Elt [section, in Elt]
WProperties_fun.remove_diff_singleton [lemma, in remove_diff_singleton]
WProperties_fun.add_equal [lemma, in add_equal]
WProperties_fun.union_remove_add_2 [lemma, in union_remove_add_2]
WProperties_fun.union_assoc [lemma, in union_assoc]
WProperties_fun.in_subset [lemma, in in_subset]
WProperties_fun.union_inter_1 [lemma, in union_inter_1]
WProperties_fun.subset_refl [lemma, in subset_refl]
WProperties_fun.inter_Add [lemma, in inter_Add]
WProperties_fun.fold_union_inter [lemma, in fold_union_inter]
WProperties_fun.fold_equal [lemma, in fold_equal]
WProperties_fun.Fold.Fold_More [section, in Fold_More]
WProperties_fun.Elt.Fold_More [section, in Fold_More]
WProperties_fun.not_in_union [lemma, in not_in_union]
WProperties_fun.In_dec [lemma, in In_dec]
WProperties_fun.inter_subset_3 [lemma, in inter_subset_3]
WProperties_fun.add_cardinal_1 [lemma, in add_cardinal_1]
WProperties_fun.InA [abbreviation, in InA]
WProperties_fun.cardinal_inv_2 [lemma, in cardinal_inv_2]
WProperties_fun.cardinal_inv_2 [lemma, in cardinal_inv_2]
WProperties_fun.cardinal_Empty [lemma, in cardinal_Empty]
WProperties_fun.cardinal_Empty [lemma, in cardinal_Empty]
WProperties_fun.union_equal_2 [lemma, in union_equal_2]
WRawSets [module, in WRawSets]
WRawSets.add_ok [instance, in add_ok]
WRawSets.add_spec [axiom, in add_spec]
WRawSets.cardinal_spec [axiom, in cardinal_spec]
WRawSets.choose_spec2 [axiom, in choose_spec2]
WRawSets.choose_spec1 [axiom, in choose_spec1]
WRawSets.compatb [abbreviation, in compatb]
WRawSets.diff_spec [axiom, in diff_spec]
WRawSets.diff_ok [instance, in diff_ok]
WRawSets.elements_spec2w [axiom, in elements_spec2w]
WRawSets.elements_spec1 [axiom, in elements_spec1]
WRawSets.Empty [definition, in Empty]
WRawSets.empty_spec [axiom, in empty_spec]
WRawSets.empty_ok [instance, in empty_ok]
WRawSets.eq [definition, in eq]
WRawSets.Equal [definition, in Equal]
WRawSets.equal_spec [axiom, in equal_spec]
WRawSets.eq_equiv [instance, in eq_equiv]
WRawSets.Exists [definition, in Exists]
WRawSets.exists_spec [axiom, in exists_spec]
WRawSets.filter_spec [axiom, in filter_spec]
WRawSets.filter_ok [instance, in filter_ok]
WRawSets.fold_spec [axiom, in fold_spec]
WRawSets.For_all [definition, in For_all]
WRawSets.for_all_spec [axiom, in for_all_spec]
WRawSets.In [axiom, in In]
WRawSets.inter_spec [axiom, in inter_spec]
WRawSets.inter_ok [instance, in inter_ok]
WRawSets.In_compat [instance, in In_compat]
WRawSets.IsOk [axiom, in IsOk]
WRawSets.isok [axiom, in isok]
WRawSets.isok_Ok [instance, in isok_Ok]
WRawSets.is_empty_spec [axiom, in is_empty_spec]
WRawSets.mem_spec [axiom, in mem_spec]
WRawSets.Ok [record, in Ok]
WRawSets.Ok [inductive, in Ok]
WRawSets.ok [projection, in ok]
WRawSets.ok [constructor, in ok]
WRawSets.partition_spec2 [axiom, in partition_spec2]
WRawSets.partition_spec1 [axiom, in partition_spec1]
WRawSets.partition_ok2 [instance, in partition_ok2]
WRawSets.partition_ok1 [instance, in partition_ok1]
WRawSets.remove_spec [axiom, in remove_spec]
WRawSets.remove_ok [instance, in remove_ok]
WRawSets.singleton_spec [axiom, in singleton_spec]
WRawSets.singleton_ok [instance, in singleton_ok]
WRawSets.Spec [section, in Spec]
WRawSets.Spec.f [variable, in f]
WRawSets.Spec.s [variable, in s]
WRawSets.Spec.s' [variable, in s']
WRawSets.Spec.x [variable, in x]
WRawSets.Spec.y [variable, in y]
WRawSets.Subset [definition, in Subset]
WRawSets.subset_spec [axiom, in subset_spec]
WRawSets.union_spec [axiom, in union_spec]
WRawSets.union_ok [instance, in union_ok]
_ [=] _ [notation, in ::x_'[=]'_x]
_ [<=] _ [notation, in ::x_'[<=]'_x]
WRaw2Sets [module, in WRaw2Sets]
WRaw2SetsOn [module, in WRaw2SetsOn]
WRaw2SetsOn.add [definition, in add]
WRaw2SetsOn.add_spec [lemma, in add_spec]
WRaw2SetsOn.cardinal [definition, in cardinal]
WRaw2SetsOn.cardinal_spec [lemma, in cardinal_spec]
WRaw2SetsOn.choose [definition, in choose]
WRaw2SetsOn.choose_spec2 [lemma, in choose_spec2]
WRaw2SetsOn.choose_spec1 [lemma, in choose_spec1]
WRaw2SetsOn.compatb [abbreviation, in compatb]
WRaw2SetsOn.diff [definition, in diff]
WRaw2SetsOn.diff_spec [lemma, in diff_spec]
WRaw2SetsOn.elements [definition, in elements]
WRaw2SetsOn.elements_spec2w [lemma, in elements_spec2w]
WRaw2SetsOn.elements_spec1 [lemma, in elements_spec1]
WRaw2SetsOn.elt [definition, in elt]
WRaw2SetsOn.empty [definition, in empty]
WRaw2SetsOn.Empty [definition, in Empty]
WRaw2SetsOn.empty_spec [lemma, in empty_spec]
WRaw2SetsOn.eq [definition, in eq]
WRaw2SetsOn.equal [definition, in equal]
WRaw2SetsOn.Equal [definition, in Equal]
WRaw2SetsOn.equal_spec [lemma, in equal_spec]
WRaw2SetsOn.eq_dec [definition, in eq_dec]
WRaw2SetsOn.eq_equiv [instance, in eq_equiv]
WRaw2SetsOn.Exists [definition, in Exists]
WRaw2SetsOn.exists_spec [lemma, in exists_spec]
WRaw2SetsOn.exists_ [definition, in exists_]
WRaw2SetsOn.filter [definition, in filter]
WRaw2SetsOn.filter_spec [lemma, in filter_spec]
WRaw2SetsOn.fold [definition, in fold]
WRaw2SetsOn.fold_spec [lemma, in fold_spec]
WRaw2SetsOn.For_all [definition, in For_all]
WRaw2SetsOn.for_all [definition, in for_all]
WRaw2SetsOn.for_all_spec [lemma, in for_all_spec]
WRaw2SetsOn.In [definition, in In]
WRaw2SetsOn.inter [definition, in inter]
WRaw2SetsOn.inter_spec [lemma, in inter_spec]
WRaw2SetsOn.In_compat [instance, in In_compat]
WRaw2SetsOn.is_empty [definition, in is_empty]
WRaw2SetsOn.is_ok [projection, in is_ok]
WRaw2SetsOn.is_empty_spec [lemma, in is_empty_spec]
WRaw2SetsOn.mem [definition, in mem]
WRaw2SetsOn.mem_spec [lemma, in mem_spec]
WRaw2SetsOn.Mkt [constructor, in Mkt]
WRaw2SetsOn.partition [definition, in partition]
WRaw2SetsOn.partition_spec2 [lemma, in partition_spec2]
WRaw2SetsOn.partition_spec1 [lemma, in partition_spec1]
WRaw2SetsOn.remove [definition, in remove]
WRaw2SetsOn.remove_spec [lemma, in remove_spec]
WRaw2SetsOn.singleton [definition, in singleton]
WRaw2SetsOn.singleton_spec [lemma, in singleton_spec]
WRaw2SetsOn.Spec [section, in Spec]
WRaw2SetsOn.Spec.f [variable, in f]
WRaw2SetsOn.Spec.s [variable, in s]
WRaw2SetsOn.Spec.s' [variable, in s']
WRaw2SetsOn.Spec.x [variable, in x]
WRaw2SetsOn.Spec.y [variable, in y]
WRaw2SetsOn.Subset [definition, in Subset]
WRaw2SetsOn.subset [definition, in subset]
WRaw2SetsOn.subset_spec [lemma, in subset_spec]
WRaw2SetsOn.t [definition, in t]
WRaw2SetsOn.this [projection, in this]
WRaw2SetsOn.t_ [record, in t_]
WRaw2SetsOn.union [definition, in union]
WRaw2SetsOn.union_spec [lemma, in union_spec]
WRaw2Sets.E [module, in WRaw2Sets.E]
WS [module, in WS]
WS [module, in WS]
WSets [module, in WSets]
WSetsOn [module, in WSetsOn]
WSetsOn.add_spec [axiom, in add_spec]
WSetsOn.cardinal_spec [axiom, in cardinal_spec]
WSetsOn.choose_spec2 [axiom, in choose_spec2]
WSetsOn.choose_spec1 [axiom, in choose_spec1]
WSetsOn.compatb [abbreviation, in compatb]
WSetsOn.diff_spec [axiom, in diff_spec]
WSetsOn.elements_spec2w [axiom, in elements_spec2w]
WSetsOn.elements_spec1 [axiom, in elements_spec1]
WSetsOn.Empty [definition, in Empty]
WSetsOn.empty_spec [axiom, in empty_spec]
WSetsOn.eq [definition, in eq]
WSetsOn.Equal [definition, in Equal]
WSetsOn.equal_spec [axiom, in equal_spec]
WSetsOn.Exists [definition, in Exists]
WSetsOn.exists_spec [axiom, in exists_spec]
WSetsOn.filter_spec [axiom, in filter_spec]
WSetsOn.fold_spec [axiom, in fold_spec]
WSetsOn.For_all [definition, in For_all]
WSetsOn.for_all_spec [axiom, in for_all_spec]
WSetsOn.In [axiom, in In]
WSetsOn.inter_spec [axiom, in inter_spec]
WSetsOn.In_compat [instance, in In_compat]
WSetsOn.is_empty_spec [axiom, in is_empty_spec]
WSetsOn.mem_spec [axiom, in mem_spec]
WSetsOn.partition_spec2 [axiom, in partition_spec2]
WSetsOn.partition_spec1 [axiom, in partition_spec1]
WSetsOn.remove_spec [axiom, in remove_spec]
WSetsOn.singleton_spec [axiom, in singleton_spec]
WSetsOn.Spec [section, in Spec]
WSetsOn.Spec.f [variable, in f]
WSetsOn.Spec.s [variable, in s]
WSetsOn.Spec.s' [variable, in s']
WSetsOn.Spec.x [variable, in x]
WSetsOn.Spec.y [variable, in y]
WSetsOn.Subset [definition, in Subset]
WSetsOn.subset_spec [axiom, in subset_spec]
WSetsOn.union_spec [axiom, in union_spec]
_ [=] _ [notation, in ::x_'[=]'_x]
_ [<=] _ [notation, in ::x_'[<=]'_x]
WSets.E [module, in WSets.E]
WSfun [module, in WSfun]
WSfun [module, in WSfun]
WSfun.add [axiom, in add]
WSfun.add [axiom, in add]
WSfun.add_1 [axiom, in add_1]
WSfun.add_1 [axiom, in add_1]
WSfun.add_2 [axiom, in add_2]
WSfun.add_2 [axiom, in add_2]
WSfun.add_3 [axiom, in add_3]
WSfun.add_3 [axiom, in add_3]
WSfun.cardinal [axiom, in cardinal]
WSfun.cardinal [axiom, in cardinal]
WSfun.cardinal_1 [axiom, in cardinal_1]
WSfun.cardinal_1 [axiom, in cardinal_1]
WSfun.choose [axiom, in choose]
WSfun.choose_1 [axiom, in choose_1]
WSfun.choose_2 [axiom, in choose_2]
WSfun.diff [axiom, in diff]
WSfun.diff_2 [axiom, in diff_2]
WSfun.diff_1 [axiom, in diff_1]
WSfun.diff_3 [axiom, in diff_3]
WSfun.elements [axiom, in elements]
WSfun.elements [axiom, in elements]
WSfun.elements_3w [axiom, in elements_3w]
WSfun.elements_3w [axiom, in elements_3w]
WSfun.elements_1 [axiom, in elements_1]
WSfun.elements_1 [axiom, in elements_1]
WSfun.elements_2 [axiom, in elements_2]
WSfun.elements_2 [axiom, in elements_2]
WSfun.elt [definition, in elt]
WSfun.empty [axiom, in empty]
WSfun.empty [axiom, in empty]
WSfun.Empty [definition, in Empty]
WSfun.Empty [definition, in Empty]
WSfun.empty_1 [axiom, in empty_1]
WSfun.empty_1 [axiom, in empty_1]
WSfun.eq [definition, in eq]
WSfun.equal [axiom, in equal]
WSfun.equal [axiom, in equal]
WSfun.Equal [definition, in Equal]
WSfun.Equal [definition, in Equal]
WSfun.equal_2 [axiom, in equal_2]
WSfun.equal_2 [axiom, in equal_2]
WSfun.equal_1 [axiom, in equal_1]
WSfun.equal_1 [axiom, in equal_1]
WSfun.Equiv [definition, in Equiv]
WSfun.Equivb [definition, in Equivb]
WSfun.eq_refl [axiom, in eq_refl]
WSfun.eq_key_elt [definition, in eq_key_elt]
WSfun.eq_key [definition, in eq_key]
WSfun.eq_sym [axiom, in eq_sym]
WSfun.eq_trans [axiom, in eq_trans]
WSfun.eq_dec [axiom, in eq_dec]
WSfun.Exists [definition, in Exists]
WSfun.exists_1 [axiom, in exists_1]
WSfun.exists_ [axiom, in exists_]
WSfun.exists_2 [axiom, in exists_2]
WSfun.filter [axiom, in filter]
WSfun.filter_1 [axiom, in filter_1]
WSfun.filter_3 [axiom, in filter_3]
WSfun.filter_2 [axiom, in filter_2]
WSfun.find [axiom, in find]
WSfun.find_2 [axiom, in find_2]
WSfun.find_1 [axiom, in find_1]
WSfun.fold [axiom, in fold]
WSfun.fold [axiom, in fold]
WSfun.fold_1 [axiom, in fold_1]
WSfun.fold_1 [axiom, in fold_1]
WSfun.for_all_1 [axiom, in for_all_1]
WSfun.for_all_2 [axiom, in for_all_2]
WSfun.For_all [definition, in For_all]
WSfun.for_all [axiom, in for_all]
WSfun.In [axiom, in In]
WSfun.In [definition, in In]
WSfun.inter [axiom, in inter]
WSfun.inter_3 [axiom, in inter_3]
WSfun.inter_2 [axiom, in inter_2]
WSfun.inter_1 [axiom, in inter_1]
WSfun.In_1 [axiom, in In_1]
WSfun.is_empty_1 [axiom, in is_empty_1]
WSfun.is_empty_1 [axiom, in is_empty_1]
WSfun.is_empty [axiom, in is_empty]
WSfun.is_empty [axiom, in is_empty]
WSfun.is_empty_2 [axiom, in is_empty_2]
WSfun.is_empty_2 [axiom, in is_empty_2]
WSfun.key [definition, in key]
WSfun.map [axiom, in map]
WSfun.mapi [axiom, in mapi]
WSfun.mapi_2 [axiom, in mapi_2]
WSfun.mapi_1 [axiom, in mapi_1]
WSfun.MapsTo [axiom, in MapsTo]
WSfun.MapsTo_1 [axiom, in MapsTo_1]
WSfun.map_1 [axiom, in map_1]
WSfun.map_2 [axiom, in map_2]
WSfun.map2 [axiom, in map2]
WSfun.map2_2 [axiom, in map2_2]
WSfun.map2_1 [axiom, in map2_1]
WSfun.mem [axiom, in mem]
WSfun.mem [axiom, in mem]
WSfun.mem_1 [axiom, in mem_1]
WSfun.mem_1 [axiom, in mem_1]
WSfun.mem_2 [axiom, in mem_2]
WSfun.mem_2 [axiom, in mem_2]
WSfun.partition [axiom, in partition]
WSfun.partition_1 [axiom, in partition_1]
WSfun.partition_2 [axiom, in partition_2]
WSfun.remove [axiom, in remove]
WSfun.remove [axiom, in remove]
WSfun.remove_2 [axiom, in remove_2]
WSfun.remove_2 [axiom, in remove_2]
WSfun.remove_1 [axiom, in remove_1]
WSfun.remove_1 [axiom, in remove_1]
WSfun.remove_3 [axiom, in remove_3]
WSfun.remove_3 [axiom, in remove_3]
WSfun.singleton [axiom, in singleton]
WSfun.singleton_1 [axiom, in singleton_1]
WSfun.singleton_2 [axiom, in singleton_2]
WSfun.Spec [section, in Spec]
WSfun.Spec.Filter [section, in Filter]
WSfun.Spec.Filter.f [variable, in f]
WSfun.Spec.s [variable, in s]
WSfun.Spec.s' [variable, in s']
WSfun.Spec.s'' [variable, in s'']
WSfun.Spec.x [variable, in x]
WSfun.Spec.y [variable, in y]
WSfun.Subset [definition, in Subset]
WSfun.subset [axiom, in subset]
WSfun.subset_2 [axiom, in subset_2]
WSfun.subset_1 [axiom, in subset_1]
WSfun.t [axiom, in t]
WSfun.t [axiom, in t]
WSfun.Types [section, in Types]
WSfun.Types.elt [variable, in elt]
WSfun.Types.elt' [variable, in elt']
WSfun.Types.elt'' [variable, in elt'']
WSfun.Types.Spec [section, in Spec]
WSfun.Types.Spec.cmp [variable, in cmp]
WSfun.Types.Spec.e [variable, in e]
WSfun.Types.Spec.e' [variable, in e']
WSfun.Types.Spec.m [variable, in m]
WSfun.Types.Spec.m' [variable, in m']
WSfun.Types.Spec.m'' [variable, in m'']
WSfun.Types.Spec.x [variable, in x]
WSfun.Types.Spec.y [variable, in y]
WSfun.Types.Spec.z [variable, in z]
WSfun.union [axiom, in union]
WSfun.union_1 [axiom, in union_1]
WSfun.union_2 [axiom, in union_2]
WSfun.union_3 [axiom, in union_3]
_ [=] _ [notation, in ::x_'[=]'_x]
_ [<=] _ [notation, in ::x_'[<=]'_x]
_ === _ [notation, in ::x_'==='_x]
_ === _ [notation, in ::x_'==='_x]
WS_to_Finite_set.Empty_Empty_set [lemma, in Empty_Empty_set]
WS_to_Finite_set.Empty_Empty_set [lemma, in Empty_Empty_set]
WS_to_Finite_set.remove_Subtract [lemma, in remove_Subtract]
WS_to_Finite_set.remove_Subtract [lemma, in remove_Subtract]
WS_to_Finite_set.Equal_Same_set [lemma, in Equal_Same_set]
WS_to_Finite_set.Equal_Same_set [lemma, in Equal_Same_set]
WS_to_Finite_set.union_Union [lemma, in union_Union]
WS_to_Finite_set.union_Union [lemma, in union_Union]
!! [notation, in ::'!!']
!! [notation, in ::'!!']
WS_to_Finite_set.mkEns_cardinal [lemma, in mkEns_cardinal]
WS_to_Finite_set.mkEns_cardinal [lemma, in mkEns_cardinal]
WS_to_Finite_set [module, in WS_to_Finite_set]
WS_to_Finite_set [module, in WS_to_Finite_set]
WS_to_Finite_set.add_Add [lemma, in add_Add]
WS_to_Finite_set.add_Add [lemma, in add_Add]
WS_to_Finite_set.MP [module, in WS_to_Finite_set.MP]
WS_to_Finite_set.MP [module, in WS_to_Finite_set.MP]
WS_to_Finite_set.Subset_Included [lemma, in Subset_Included]
WS_to_Finite_set.Subset_Included [lemma, in Subset_Included]
WS_to_Finite_set.empty_Empty_Set [lemma, in empty_Empty_Set]
WS_to_Finite_set.empty_Empty_Set [lemma, in empty_Empty_Set]
WS_to_Finite_set.Ens_to_FSet [lemma, in Ens_to_FSet]
WS_to_Finite_set.mkEns [definition, in mkEns]
WS_to_Finite_set.mkEns [definition, in mkEns]
WS_to_Finite_set.In_In [lemma, in In_In]
WS_to_Finite_set.In_In [lemma, in In_In]
WS_to_Finite_set.inter_Intersection [lemma, in inter_Intersection]
WS_to_Finite_set.inter_Intersection [lemma, in inter_Intersection]
WS_to_Finite_set.Add_Add [lemma, in Add_Add]
WS_to_Finite_set.Add_Add [lemma, in Add_Add]
WS_to_Finite_set.Ens_to_MSet [lemma, in Ens_to_MSet]
WS_to_Finite_set.mkEns_Finite [lemma, in mkEns_Finite]
WS_to_Finite_set.mkEns_Finite [lemma, in mkEns_Finite]
WS_to_Finite_set.singleton_Singleton [lemma, in singleton_Singleton]
WS_to_Finite_set.singleton_Singleton [lemma, in singleton_Singleton]
WS.E [module, in WS.E]
WS.E [module, in WS.E]
WW [constructor, in WW]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB [abbreviation, in wwB]
wwB_pos [lemma, in wwB_pos]
wwB_wBwB [lemma, in wwB_wBwB]
wwB_4_wB_4 [lemma, in wwB_4_wB_4]
wwB_div [lemma, in wwB_div]
wwB_div_2 [lemma, in wwB_div_2]
wwB_4_2 [lemma, in wwB_4_2]
ww_add [definition, in ww_add]
ww_add_c [definition, in ww_add_c]
ww_mod_gt_aux [definition, in ww_mod_gt_aux]
ww_mul_c [definition, in ww_mul_c]
ww_gcd_gt [definition, in ww_gcd_gt]
ww_div_gt_aux [definition, in ww_div_gt_aux]
ww_zdigits [definition, in ww_zdigits]
ww_square_c [definition, in ww_square_c]
ww_head0 [definition, in ww_head0]
ww_sub_c [definition, in ww_sub_c]
ww_add_mult_mult_2_plus_1 [lemma, in ww_add_mult_mult_2_plus_1]
ww_div21 [definition, in ww_div21]
ww_to_Z [definition, in ww_to_Z]
ww_opp [definition, in ww_opp]
ww_add_carry [definition, in ww_add_carry]
ww_mod_gt [definition, in ww_mod_gt]
ww_sub_carry_c [definition, in ww_sub_carry_c]
ww_tail0 [definition, in ww_tail0]
ww_sqrt [definition, in ww_sqrt]
ww_div [definition, in ww_div]
ww_gcd_gt_aux [definition, in ww_gcd_gt_aux]
ww_add_mul_div [definition, in ww_add_mul_div]
ww_mod [definition, in ww_mod]
ww_digits [definition, in ww_digits]
ww_karatsuba_c [definition, in ww_karatsuba_c]
ww_pos_mod [definition, in ww_pos_mod]
ww_div_gt [definition, in ww_div_gt]
ww_0W [definition, in ww_0W]
ww_add_mult_mult_2 [lemma, in ww_add_mult_mult_2]
ww_gcd_gt_body [definition, in ww_gcd_gt_body]
ww_opp_carry [definition, in ww_opp_carry]
ww_W0 [definition, in ww_W0]
ww_succ [definition, in ww_succ]
ww_Bm1 [definition, in ww_Bm1]
ww_pred_c [definition, in ww_pred_c]
ww_opp_c [definition, in ww_opp_c]
ww_add_c_cont [definition, in ww_add_c_cont]
ww_head1 [definition, in ww_head1]
ww_pred [definition, in ww_pred]
ww_add_carry_c [definition, in ww_add_carry_c]
ww_is_zero [definition, in ww_is_zero]
ww_is_even [definition, in ww_is_even]
ww_gcd [definition, in ww_gcd]
ww_compare [definition, in ww_compare]
ww_1 [definition, in ww_1]
ww_WW [definition, in ww_WW]
ww_sub_carry [definition, in ww_sub_carry]
ww_mul [definition, in ww_mul]
ww_sub [definition, in ww_sub]
ww_succ_c [definition, in ww_succ_c]
ww_sqrt2 [definition, in ww_sqrt2]
w_to_Z_wwB [lemma, in w_to_Z_wwB]
w_2 [definition, in w_2]
w_div32 [definition, in w_div32]
w_mul_add [definition, in w_mul_add]
W0 [constructor, in W0]



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)