| 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 | (68863 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 | (985 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 | (44709 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 | (761 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 | (1497 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 | (570 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 | (11380 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 | (976 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 | (603 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 | (298 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 | (460 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 | (476 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 | (811 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 | (1157 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 | (4018 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) |
S
S [module, in Coq.MSets.MSetInterface]S [module, in Coq.FSets.FMapInterface]
S [module, in Coq.FSets.FSetInterface]
S [section, in Coq.micromega.Env]
S [constructor, in Coq.Init.Datatypes]
S [section, in Coq.micromega.Tauto]
S [section, in Coq.micromega.Tauto]
sAbs:201 [binder, in Coq.Reals.Abstract.ConstructiveSum]
sAbs:216 [binder, in Coq.Reals.Abstract.ConstructiveSum]
sameP [lemma, in Coq.ssr.ssrbool]
same_genZ [lemma, in Coq.setoid_ring.Ncring_initial]
same_gen [lemma, in Coq.setoid_ring.Ncring_initial]
Same_set [definition, in Coq.Sets.Ensembles]
same_genN [lemma, in Coq.setoid_ring.InitialRing]
same_genZ [lemma, in Coq.setoid_ring.InitialRing]
same_gen [lemma, in Coq.setoid_ring.InitialRing]
same_relation_is_equivalence [lemma, in Coq.Sets.Relations_1_facts]
same_relation [definition, in Coq.Sets.Relations_1]
same_relation [definition, in Coq.Relations.Relation_Definitions]
SatOk [projection, in Coq.micromega.ZifyClasses]
SatPowPos [instance, in Coq.micromega.ZifyInst]
SatProd [instance, in Coq.micromega.ZifyInst]
SatProdPos [instance, in Coq.micromega.ZifyInst]
Saturate [record, in Coq.micromega.ZifyClasses]
sa:10 [binder, in Coq.Classes.SetoidClass]
sa:12 [binder, in Coq.Classes.CEquivalence]
sa:12 [binder, in Coq.Classes.Equivalence]
sa:15 [binder, in Coq.Classes.CEquivalence]
sa:15 [binder, in Coq.Classes.Equivalence]
sa:22 [binder, in Coq.Classes.SetoidClass]
sa:24 [binder, in Coq.Classes.SetoidClass]
sa:6 [binder, in Coq.Classes.SetoidClass]
sa:8 [binder, in Coq.Classes.SetoidClass]
sa:9 [binder, in Coq.Classes.CEquivalence]
sa:9 [binder, in Coq.Classes.Equivalence]
scal_sum [lemma, in Coq.Reals.PartSum]
SCANNING [section, in Coq.Vectors.VectorDef]
SCHEMES [section, in Coq.Vectors.Fin]
SCHEMES [section, in Coq.Vectors.VectorDef]
Sdep [module, in Coq.FSets.FSetInterface]
Sdep.add [axiom, in Coq.FSets.FSetInterface]
Sdep.Add [definition, in Coq.FSets.FSetInterface]
Sdep.cardinal [axiom, in Coq.FSets.FSetInterface]
Sdep.choose [axiom, in Coq.FSets.FSetInterface]
Sdep.choose_equal [axiom, in Coq.FSets.FSetInterface]
Sdep.compare [axiom, in Coq.FSets.FSetInterface]
Sdep.diff [axiom, in Coq.FSets.FSetInterface]
Sdep.E [module, in Coq.FSets.FSetInterface]
Sdep.elements [axiom, in Coq.FSets.FSetInterface]
Sdep.elt [definition, in Coq.FSets.FSetInterface]
Sdep.empty [axiom, in Coq.FSets.FSetInterface]
Sdep.Empty [definition, in Coq.FSets.FSetInterface]
Sdep.eq [definition, in Coq.FSets.FSetInterface]
Sdep.equal [axiom, in Coq.FSets.FSetInterface]
Sdep.Equal [definition, in Coq.FSets.FSetInterface]
Sdep.eq_In [axiom, in Coq.FSets.FSetInterface]
Sdep.eq_trans [axiom, in Coq.FSets.FSetInterface]
Sdep.eq_sym [axiom, in Coq.FSets.FSetInterface]
Sdep.eq_refl [axiom, in Coq.FSets.FSetInterface]
Sdep.Exists [definition, in Coq.FSets.FSetInterface]
Sdep.exists_ [axiom, in Coq.FSets.FSetInterface]
Sdep.filter [axiom, in Coq.FSets.FSetInterface]
Sdep.fold [axiom, in Coq.FSets.FSetInterface]
Sdep.for_all [axiom, in Coq.FSets.FSetInterface]
Sdep.For_all [definition, in Coq.FSets.FSetInterface]
Sdep.In [axiom, in Coq.FSets.FSetInterface]
Sdep.inter [axiom, in Coq.FSets.FSetInterface]
Sdep.is_empty [axiom, in Coq.FSets.FSetInterface]
Sdep.lt [axiom, in Coq.FSets.FSetInterface]
Sdep.lt_not_eq [axiom, in Coq.FSets.FSetInterface]
Sdep.lt_trans [axiom, in Coq.FSets.FSetInterface]
Sdep.max_elt [axiom, in Coq.FSets.FSetInterface]
Sdep.mem [axiom, in Coq.FSets.FSetInterface]
Sdep.min_elt [axiom, in Coq.FSets.FSetInterface]
Sdep.partition [axiom, in Coq.FSets.FSetInterface]
Sdep.remove [axiom, in Coq.FSets.FSetInterface]
Sdep.singleton [axiom, in Coq.FSets.FSetInterface]
Sdep.subset [axiom, in Coq.FSets.FSetInterface]
Sdep.Subset [definition, in Coq.FSets.FSetInterface]
Sdep.t [axiom, in Coq.FSets.FSetInterface]
Sdep.union [axiom, in Coq.FSets.FSetInterface]
_ [=] _ [notation, in Coq.FSets.FSetInterface]
second_index:51 [binder, in Coq.Reals.Runcountable]
selectOneInSum [lemma, in Coq.Reals.Abstract.ConstructiveSum]
self_inverse [definition, in Coq.ssr.ssrfun]
Seminus_Empty_set_r [lemma, in Coq.Sets.Powerset_facts]
Seminus_Empty_set_l [lemma, in Coq.Sets.Powerset_facts]
semi_field_theory [record, in Coq.setoid_ring.Field_theory]
semi_morph [record, in Coq.setoid_ring.Ring_theory]
semi_ring_theory [record, in Coq.setoid_ring.Ring_theory]
sEmpty [inductive, in Coq.Logic.StrictProp]
sep:55 [binder, in Coq.Strings.String]
seq [definition, in Coq.Lists.List]
seq [definition, in Coq.Sets.Uniset]
SeqProp [library]
SeqSeries [library]
sequence [section, in Coq.Reals.Rseries]
sequence_minorant [abbreviation, in Coq.Reals.SeqProp]
sequence_majorant [abbreviation, in Coq.Reals.SeqProp]
sequence_lb [definition, in Coq.Reals.SeqProp]
sequence_ub [definition, in Coq.Reals.SeqProp]
sequence.Un [variable, in Coq.Reals.Rseries]
seq_cv_morph [instance, in Coq.Reals.Cauchy.ConstructiveRcomplete]
seq_cv_proper [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
seq_cv [definition, in Coq.Reals.Cauchy.ConstructiveRcomplete]
seq_S [lemma, in Coq.Lists.List]
seq_app [lemma, in Coq.Lists.List]
seq_NoDup [lemma, in Coq.Lists.List]
seq_shift [lemma, in Coq.Lists.List]
seq_nth [lemma, in Coq.Lists.List]
seq_length [lemma, in Coq.Lists.List]
seq_congr [lemma, in Coq.Sets.Uniset]
seq_right [lemma, in Coq.Sets.Uniset]
seq_left [lemma, in Coq.Sets.Uniset]
seq_sym [lemma, in Coq.Sets.Uniset]
seq_trans [lemma, in Coq.Sets.Uniset]
seq_refl [lemma, in Coq.Sets.Uniset]
Seq_trans [definition, in Coq.Setoids.Setoid]
Seq_sym [definition, in Coq.Setoids.Setoid]
Seq_refl [definition, in Coq.Setoids.Setoid]
series_cv_shift' [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_shift [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_triangle [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_abs_remainder [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_remainder_maj [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_eq [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_nonneg [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_minus [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_plus [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_scale [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_opp [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_abs_cv [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_abs_eq [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_unique [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_abs [definition, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_abs_lt [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_maj [lemma, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_le_lim [definition, in Coq.Reals.Abstract.ConstructiveSum]
series_cv_lim_lt [definition, in Coq.Reals.Abstract.ConstructiveSum]
series_cv [definition, in Coq.Reals.Abstract.ConstructiveSum]
set [definition, in Coq.Lists.ListSet]
setcover_intro [lemma, in Coq.Sets.Powerset_facts]
setcover_inv [lemma, in Coq.Sets.Powerset_Classical_facts]
SetIncl [section, in Coq.Lists.List]
SetIncl.A [variable, in Coq.Lists.List]
SetIsType [library]
Setminus [definition, in Coq.Sets.Ensembles]
Setminus_intro [lemma, in Coq.Sets.Constructive_sets]
Setminus_Included_empty [lemma, in Coq.Sets.Powerset_facts]
Setminus_Disjoint_noop [lemma, in Coq.Sets.Powerset_facts]
Setminus_Union_r [lemma, in Coq.Sets.Powerset_facts]
Setminus_Union_l [lemma, in Coq.Sets.Powerset_facts]
Setoid [record, in Coq.Classes.SetoidClass]
Setoid [library]
SetoidChoice [library]
SetoidClass [library]
SetoidDec [library]
SetoidFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
SetoidFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
SetoidList [library]
SetoidPermutation [library]
SetoidTactics [library]
setoid_choice [lemma, in Coq.Logic.SetoidChoice]
setoid_functional_choice_second_characterization [lemma, in Coq.Logic.ChoiceFacts]
setoid_functional_choice_first_characterization [lemma, in Coq.Logic.ChoiceFacts]
setoid_fun_choice_imp_repr_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
setoid_fun_choice_imp_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
setoid_fun_choice_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
setoid_fun_choice_iff_simple_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
setoid_fun_choice_imp_simple_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
setoid_fun_choice_iff_gen_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
setoid_fun_choice_imp_gen_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
setoid_decidable [projection, in Coq.Classes.EquivDec]
setoid_decidable [constructor, in Coq.Classes.EquivDec]
setoid_partial_app_morphism [instance, in Coq.Classes.SetoidClass]
setoid_morphism [instance, in Coq.Classes.SetoidClass]
setoid_trans [definition, in Coq.Classes.SetoidClass]
setoid_sym [definition, in Coq.Classes.SetoidClass]
setoid_refl [definition, in Coq.Classes.SetoidClass]
setoid_equiv [projection, in Coq.Classes.SetoidClass]
setoid_decidable [projection, in Coq.Classes.SetoidDec]
setoid_decidable [constructor, in Coq.Classes.SetoidDec]
Setoid_Theory [definition, in Coq.Setoids.Setoid]
Sets [module, in Coq.MSets.MSetInterface]
SetsOn [module, in Coq.MSets.MSetInterface]
SetsOn.choose_spec3 [axiom, in Coq.MSets.MSetInterface]
SetsOn.compare_spec [axiom, in Coq.MSets.MSetInterface]
SetsOn.elements_spec2 [axiom, in Coq.MSets.MSetInterface]
SetsOn.max_elt_spec3 [axiom, in Coq.MSets.MSetInterface]
SetsOn.max_elt_spec2 [axiom, in Coq.MSets.MSetInterface]
SetsOn.max_elt_spec1 [axiom, in Coq.MSets.MSetInterface]
SetsOn.min_elt_spec3 [axiom, in Coq.MSets.MSetInterface]
SetsOn.min_elt_spec2 [axiom, in Coq.MSets.MSetInterface]
SetsOn.min_elt_spec1 [axiom, in Coq.MSets.MSetInterface]
SetsOn.Spec [section, in Coq.MSets.MSetInterface]
SetsOn.Spec.s [variable, in Coq.MSets.MSetInterface]
SetsOn.Spec.s' [variable, in Coq.MSets.MSetInterface]
SetsOn.Spec.x [variable, in Coq.MSets.MSetInterface]
SetsOn.Spec.y [variable, in Coq.MSets.MSetInterface]
Sets_as_an_algebra.U [variable, in Coq.Sets.Powerset_facts]
Sets_as_an_algebra [section, in Coq.Sets.Powerset_facts]
Sets_as_an_algebra.U [variable, in Coq.Sets.Powerset_Classical_facts]
Sets_as_an_algebra [section, in Coq.Sets.Powerset_Classical_facts]
Sets.E [module, in Coq.MSets.MSetInterface]
set_digit [definition, in Coq.Numbers.Cyclic.Int63.Int63]
set_map [definition, in Coq.Lists.ListSet]
set_fold_right [definition, in Coq.Lists.ListSet]
set_fold_left [definition, in Coq.Lists.ListSet]
set_power [definition, in Coq.Lists.ListSet]
set_prod [definition, in Coq.Lists.ListSet]
set_diff_trivial [lemma, in Coq.Lists.ListSet]
set_diff_nodup [lemma, in Coq.Lists.ListSet]
set_diff_iff [lemma, in Coq.Lists.ListSet]
set_diff_elim2 [lemma, in Coq.Lists.ListSet]
set_diff_elim1 [lemma, in Coq.Lists.ListSet]
set_diff_intro [lemma, in Coq.Lists.ListSet]
set_inter_nodup [lemma, in Coq.Lists.ListSet]
set_inter_iff [lemma, in Coq.Lists.ListSet]
set_inter_elim [lemma, in Coq.Lists.ListSet]
set_inter_elim2 [lemma, in Coq.Lists.ListSet]
set_inter_elim1 [lemma, in Coq.Lists.ListSet]
set_inter_intro [lemma, in Coq.Lists.ListSet]
set_union_emptyR [lemma, in Coq.Lists.ListSet]
set_union_emptyL [lemma, in Coq.Lists.ListSet]
set_union_nodup [lemma, in Coq.Lists.ListSet]
set_union_iff [lemma, in Coq.Lists.ListSet]
set_union_elim [lemma, in Coq.Lists.ListSet]
set_union_intro [lemma, in Coq.Lists.ListSet]
set_union_intro2 [lemma, in Coq.Lists.ListSet]
set_union_intro1 [lemma, in Coq.Lists.ListSet]
set_remove_nodup [lemma, in Coq.Lists.ListSet]
set_remove_iff [lemma, in Coq.Lists.ListSet]
set_remove_3 [lemma, in Coq.Lists.ListSet]
set_remove_2 [lemma, in Coq.Lists.ListSet]
set_remove_1 [lemma, in Coq.Lists.ListSet]
set_add_nodup [lemma, in Coq.Lists.ListSet]
set_add_iff [lemma, in Coq.Lists.ListSet]
set_add_not_empty [lemma, in Coq.Lists.ListSet]
set_add_elim2 [lemma, in Coq.Lists.ListSet]
set_add_elim [lemma, in Coq.Lists.ListSet]
set_add_intro [lemma, in Coq.Lists.ListSet]
set_add_intro2 [lemma, in Coq.Lists.ListSet]
set_add_intro1 [lemma, in Coq.Lists.ListSet]
set_mem_complete2 [lemma, in Coq.Lists.ListSet]
set_mem_complete1 [lemma, in Coq.Lists.ListSet]
set_mem_correct2 [lemma, in Coq.Lists.ListSet]
set_mem_correct1 [lemma, in Coq.Lists.ListSet]
set_mem_ind2 [lemma, in Coq.Lists.ListSet]
set_mem_ind [lemma, in Coq.Lists.ListSet]
set_In_dec [lemma, in Coq.Lists.ListSet]
set_In [definition, in Coq.Lists.ListSet]
set_diff [definition, in Coq.Lists.ListSet]
set_union [definition, in Coq.Lists.ListSet]
set_inter [definition, in Coq.Lists.ListSet]
set_remove [definition, in Coq.Lists.ListSet]
set_mem [definition, in Coq.Lists.ListSet]
set_add [definition, in Coq.Lists.ListSet]
Sexists [constructor, in Coq.Logic.StrictProp]
se:3 [binder, in Coq.Floats.FloatOps]
SFabs [definition, in Coq.Floats.SpecFloat]
SFadd [definition, in Coq.Floats.SpecFloat]
SFclassify [definition, in Coq.Floats.SpecFloat]
SFcompare [definition, in Coq.Floats.SpecFloat]
SFdiv [definition, in Coq.Floats.SpecFloat]
SFdiv_core_binary [definition, in Coq.Floats.SpecFloat]
SFdiv_def [projection, in Coq.setoid_ring.Field_theory]
SFeqb [definition, in Coq.Floats.SpecFloat]
SFfrexp [definition, in Coq.Floats.SpecFloat]
SFinv_l [projection, in Coq.setoid_ring.Field_theory]
SFL [definition, in Coq.Reals.PSeries_reg]
SFldexp [definition, in Coq.Floats.SpecFloat]
SFleb [definition, in Coq.Floats.SpecFloat]
SFltb [definition, in Coq.Floats.SpecFloat]
SFL_continuity [lemma, in Coq.Reals.PSeries_reg]
SFL_continuity_pt [lemma, in Coq.Reals.PSeries_reg]
SFmax_float [definition, in Coq.Floats.SpecFloat]
SFmul [definition, in Coq.Floats.SpecFloat]
SFnormfr_mantissa [definition, in Coq.Floats.SpecFloat]
SFone [definition, in Coq.Floats.SpecFloat]
SFopp [definition, in Coq.Floats.SpecFloat]
SFpred [definition, in Coq.Floats.SpecFloat]
SFpred_pos [definition, in Coq.Floats.SpecFloat]
SFsqrt [definition, in Coq.Floats.SpecFloat]
SFsqrt_core_binary [definition, in Coq.Floats.SpecFloat]
SFsub [definition, in Coq.Floats.SpecFloat]
SFsucc [definition, in Coq.Floats.SpecFloat]
SFulp [definition, in Coq.Floats.SpecFloat]
Sfun [module, in Coq.FSets.FMapInterface]
Sfun [module, in Coq.FSets.FSetInterface]
Sfun.choose_3 [axiom, in Coq.FSets.FSetInterface]
Sfun.compare [axiom, in Coq.FSets.FSetInterface]
Sfun.elements_3 [axiom, in Coq.FSets.FMapInterface]
Sfun.elements_3 [axiom, in Coq.FSets.FSetInterface]
Sfun.elt [section, in Coq.FSets.FMapInterface]
Sfun.elt.elt [variable, in Coq.FSets.FMapInterface]
Sfun.lt [axiom, in Coq.FSets.FSetInterface]
Sfun.lt_key [definition, in Coq.FSets.FMapInterface]
Sfun.lt_not_eq [axiom, in Coq.FSets.FSetInterface]
Sfun.lt_trans [axiom, in Coq.FSets.FSetInterface]
Sfun.max_elt_3 [axiom, in Coq.FSets.FSetInterface]
Sfun.max_elt_2 [axiom, in Coq.FSets.FSetInterface]
Sfun.max_elt_1 [axiom, in Coq.FSets.FSetInterface]
Sfun.max_elt [axiom, in Coq.FSets.FSetInterface]
Sfun.min_elt_3 [axiom, in Coq.FSets.FSetInterface]
Sfun.min_elt_2 [axiom, in Coq.FSets.FSetInterface]
Sfun.min_elt_1 [axiom, in Coq.FSets.FSetInterface]
Sfun.min_elt [axiom, in Coq.FSets.FSetInterface]
Sfun.Spec [section, in Coq.FSets.FSetInterface]
Sfun.Spec.s [variable, in Coq.FSets.FSetInterface]
Sfun.Spec.s' [variable, in Coq.FSets.FSetInterface]
Sfun.Spec.s'' [variable, in Coq.FSets.FSetInterface]
Sfun.Spec.x [variable, in Coq.FSets.FSetInterface]
Sfun.Spec.y [variable, in Coq.FSets.FSetInterface]
SF_1_neq_0 [projection, in Coq.setoid_ring.Field_theory]
SF_SR [projection, in Coq.setoid_ring.Field_theory]
SF2AF [definition, in Coq.setoid_ring.Field_theory]
SF2Prim [definition, in Coq.Floats.FloatOps]
SF2Prim_inj [lemma, in Coq.Floats.FloatAxioms]
SF2Prim_Prim2SF [axiom, in Coq.Floats.FloatAxioms]
SF64add [definition, in Coq.Floats.FloatAxioms]
SF64classify [definition, in Coq.Floats.FloatAxioms]
SF64div [definition, in Coq.Floats.FloatAxioms]
SF64mul [definition, in Coq.Floats.FloatAxioms]
SF64pred [definition, in Coq.Floats.FloatAxioms]
SF64sqrt [definition, in Coq.Floats.FloatAxioms]
SF64sub [definition, in Coq.Floats.FloatAxioms]
SF64succ [definition, in Coq.Floats.FloatAxioms]
sf:449 [binder, in Coq.setoid_ring.Field_theory]
shift [definition, in Coq.Floats.FloatOps]
shift [definition, in Coq.ZArith.Zpower]
shift [definition, in Coq.Strings.Ascii]
shiftin [definition, in Coq.Vectors.VectorDef]
shiftin_last [lemma, in Coq.Vectors.VectorSpec]
shiftin_nth [lemma, in Coq.Vectors.VectorSpec]
shiftl [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
shiftl [definition, in Coq.Init.Nat]
shiftl [definition, in Coq.Numbers.Cyclic.Int31.Int31]
shiftl_spec_low [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
shiftl_spec_high [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
shiftout [definition, in Coq.Vectors.VectorDef]
shiftr [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
shiftr [definition, in Coq.Init.Nat]
shiftr [definition, in Coq.Numbers.Cyclic.Int31.Int31]
shiftrepeat [definition, in Coq.Vectors.VectorDef]
shiftrepeat_last [lemma, in Coq.Vectors.VectorSpec]
shiftrepeat_nth [lemma, in Coq.Vectors.VectorSpec]
shiftr_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
shift_unshift_mod_2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
shift_value [lemma, in Coq.Floats.FloatLemmas]
shift_pos_correct [lemma, in Coq.ZArith.Zpower]
shift_pos_nat [lemma, in Coq.ZArith.Zpower]
shift_nat_correct [lemma, in Coq.ZArith.Zpower]
shift_nat_plus [lemma, in Coq.ZArith.Zpower]
shift_equiv [lemma, in Coq.ZArith.Zpower]
shift_pos_equiv [lemma, in Coq.ZArith.Zpower]
shift_nat_equiv [lemma, in Coq.ZArith.Zpower]
shift_pos [definition, in Coq.ZArith.Zpower]
shift_nat [definition, in Coq.ZArith.Zpower]
shift_unshift_mod_3 [lemma, in Coq.Numbers.Cyclic.Int63.Cyclic63]
shift_unshift_mod_2 [lemma, in Coq.Numbers.Cyclic.Int63.Cyclic63]
shift:234 [binder, in Coq.Reals.Abstract.ConstructiveSum]
shl_align [definition, in Coq.Floats.SpecFloat]
shr [definition, in Coq.Floats.SpecFloat]
shr_fexp [definition, in Coq.Floats.SpecFloat]
shr_record_of_loc [definition, in Coq.Floats.SpecFloat]
shr_1 [definition, in Coq.Floats.SpecFloat]
shr_s [projection, in Coq.Floats.SpecFloat]
shr_r [projection, in Coq.Floats.SpecFloat]
shr_m [projection, in Coq.Floats.SpecFloat]
shr_record [record, in Coq.Floats.SpecFloat]
shr:12 [binder, in Coq.Floats.FloatOps]
sig [section, in Coq.Init.Specif]
sig [inductive, in Coq.Init.Specif]
Sig [section, in Coq.ssr.ssrfun]
sigma [definition, in Coq.Reals.Rsigma]
Sigma [section, in Coq.Reals.Rsigma]
sigma_eq_arg [lemma, in Coq.Reals.Rsigma]
sigma_last [lemma, in Coq.Reals.Rsigma]
sigma_first [lemma, in Coq.Reals.Rsigma]
sigma_diff_neg [lemma, in Coq.Reals.Rsigma]
sigma_diff [lemma, in Coq.Reals.Rsigma]
sigma_split [lemma, in Coq.Reals.Rsigma]
Sigma.f [variable, in Coq.Reals.Rsigma]
Signed [module, in Coq.Numbers.HexadecimalPos]
Signed [module, in Coq.Numbers.HexadecimalNat]
Signed [module, in Coq.Numbers.DecimalN]
Signed [module, in Coq.Numbers.HexadecimalN]
Signed [module, in Coq.Numbers.DecimalPos]
Signed [module, in Coq.Numbers.DecimalNat]
Signed.of_inj_pos [lemma, in Coq.Numbers.HexadecimalPos]
Signed.of_int_norm [lemma, in Coq.Numbers.HexadecimalPos]
Signed.of_to [lemma, in Coq.Numbers.HexadecimalPos]
Signed.of_inj_pos [lemma, in Coq.Numbers.HexadecimalNat]
Signed.of_int_norm [lemma, in Coq.Numbers.HexadecimalNat]
Signed.of_to [lemma, in Coq.Numbers.HexadecimalNat]
Signed.of_inj_pos [lemma, in Coq.Numbers.DecimalN]
Signed.of_int_norm [lemma, in Coq.Numbers.DecimalN]
Signed.of_to [lemma, in Coq.Numbers.DecimalN]
Signed.of_inj_pos [lemma, in Coq.Numbers.HexadecimalN]
Signed.of_int_norm [lemma, in Coq.Numbers.HexadecimalN]
Signed.of_to [lemma, in Coq.Numbers.HexadecimalN]
Signed.of_inj_pos [lemma, in Coq.Numbers.DecimalPos]
Signed.of_int_norm [lemma, in Coq.Numbers.DecimalPos]
Signed.of_to [lemma, in Coq.Numbers.DecimalPos]
Signed.of_inj_pos [lemma, in Coq.Numbers.DecimalNat]
Signed.of_int_norm [lemma, in Coq.Numbers.DecimalNat]
Signed.of_to [lemma, in Coq.Numbers.DecimalNat]
Signed.to_int_pos_surj [lemma, in Coq.Numbers.HexadecimalPos]
Signed.to_int_inj [lemma, in Coq.Numbers.HexadecimalPos]
Signed.to_of [lemma, in Coq.Numbers.HexadecimalPos]
Signed.to_int_pos_surj [lemma, in Coq.Numbers.HexadecimalNat]
Signed.to_int_inj [lemma, in Coq.Numbers.HexadecimalNat]
Signed.to_of [lemma, in Coq.Numbers.HexadecimalNat]
Signed.to_int_pos_surj [lemma, in Coq.Numbers.DecimalN]
Signed.to_int_inj [lemma, in Coq.Numbers.DecimalN]
Signed.to_of [lemma, in Coq.Numbers.DecimalN]
Signed.to_int_pos_surj [lemma, in Coq.Numbers.HexadecimalN]
Signed.to_int_inj [lemma, in Coq.Numbers.HexadecimalN]
Signed.to_of [lemma, in Coq.Numbers.HexadecimalN]
Signed.to_int_pos_surj [lemma, in Coq.Numbers.DecimalPos]
Signed.to_int_inj [lemma, in Coq.Numbers.DecimalPos]
Signed.to_of [lemma, in Coq.Numbers.DecimalPos]
Signed.to_int_pos_surj [lemma, in Coq.Numbers.DecimalNat]
Signed.to_int_inj [lemma, in Coq.Numbers.DecimalNat]
Signed.to_of [lemma, in Coq.Numbers.DecimalNat]
sign_spec [projection, in Coq.setoid_ring.Ring_theory]
sign_theory [record, in Coq.setoid_ring.Ring_theory]
sign:6 [binder, in Coq.Numbers.Cyclic.Abstract.DoubleType]
sigT [section, in Coq.Init.Specif]
sigT [inductive, in Coq.Init.Specif]
sigT_of_sigT2_eq [definition, in Coq.Init.Specif]
sigT_eta [definition, in Coq.Init.Specif]
sigT_of_sig [definition, in Coq.Init.Specif]
sigT_of_sigT2 [definition, in Coq.Init.Specif]
(= _ ; _ ) [notation, in Coq.Init.Specif]
sigT2 [section, in Coq.Init.Specif]
sigT2 [inductive, in Coq.Init.Specif]
sigT2_eta [definition, in Coq.Init.Specif]
sigT2_of_sig2 [definition, in Coq.Init.Specif]
sig_lub [lemma, in Coq.Reals.Abstract.ConstructiveLUB]
sig_not_dec:108 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
sig_forall_dec:107 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
sig_not_dec_T [definition, in Coq.Reals.Abstract.ConstructiveLUB]
sig_forall_dec_T [definition, in Coq.Reals.Abstract.ConstructiveLUB]
sig_of_sig2_eq [definition, in Coq.Init.Specif]
sig_eta [definition, in Coq.Init.Specif]
sig_of_sigT [definition, in Coq.Init.Specif]
sig_of_sig2 [definition, in Coq.Init.Specif]
sig_of_sig2 [definition, in Coq.ssr.ssrfun]
sig_not_dec [lemma, in Coq.Reals.Rlogic]
sig_forall_dec [lemma, in Coq.Reals.Rlogic]
sig_not_dec [axiom, in Coq.Reals.ClassicalDedekindReals]
sig_forall_dec [axiom, in Coq.Reals.ClassicalDedekindReals]
Sig.P [variable, in Coq.ssr.ssrfun]
Sig.Q [variable, in Coq.ssr.ssrfun]
Sig.T [variable, in Coq.ssr.ssrfun]
sig2 [section, in Coq.Init.Specif]
sig2 [inductive, in Coq.Init.Specif]
sig2_eta [definition, in Coq.Init.Specif]
sig2_of_sigT2 [definition, in Coq.Init.Specif]
sig:39 [binder, in Coq.Classes.Morphisms]
sig:39 [binder, in Coq.Classes.CMorphisms]
SimpleMergeExample [definition, in Coq.Sorting.Mergesort]
SimpleSetoidFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
SimpleSetoidFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
simple_setoid_fun_choice_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
SimplFun [section, in Coq.ssr.ssrfun]
SimplFun [constructor, in Coq.ssr.ssrfun]
SimplFunDelta [definition, in Coq.ssr.ssrfun]
SimplFun.aT [variable, in Coq.ssr.ssrfun]
SimplFun.rT [variable, in Coq.ssr.ssrfun]
simplification_K [lemma, in Coq.Program.Equality]
simplification_existT1 [lemma, in Coq.Program.Equality]
simplification_existT2 [lemma, in Coq.Program.Equality]
simplification_heq [lemma, in Coq.Program.Equality]
Simplify_add [lemma, in Coq.Sets.Powerset_Classical_facts]
SimplPred [definition, in Coq.ssr.ssrbool]
simplPredType [definition, in Coq.ssr.ssrbool]
SimplRel [definition, in Coq.ssr.ssrbool]
simpl_sin_n [lemma, in Coq.Reals.Rtrigo_def]
simpl_cos_n [lemma, in Coq.Reals.Rtrigo_def]
simpl_cone [definition, in Coq.micromega.RingMicromega]
simpl_fact [lemma, in Coq.Reals.Rfunctions]
simpl_predE [lemma, in Coq.ssr.ssrbool]
simpl_pred_value [projection, in Coq.ssr.ssrbool]
simpl_of_mem [definition, in Coq.ssr.ssrbool]
simpl_rel [definition, in Coq.ssr.ssrbool]
simpl_pred [definition, in Coq.ssr.ssrbool]
simpl_fun [inductive, in Coq.ssr.ssrfun]
sin [definition, in Coq.Reals.Rtrigo_def]
SIN [lemma, in Coq.Reals.Rtrigo1]
sincl_add_x [lemma, in Coq.Sets.Powerset_Classical_facts]
sind [definition, in Coq.Reals.Rtrigo_calc]
Singleton [inductive, in Coq.Sets.Ensembles]
Singleton [definition, in Coq.Sets.Uniset]
singleton [definition, in Coq.micromega.VarMap]
SingletonBag [definition, in Coq.Sets.Multiset]
Singleton_is_finite [lemma, in Coq.Sets.Finite_sets_facts]
Singleton_intro [lemma, in Coq.Sets.Constructive_sets]
Singleton_inv [lemma, in Coq.Sets.Constructive_sets]
singleton_choice [lemma, in Coq.Logic.ClassicalChoice]
Singleton_atomic [lemma, in Coq.Sets.Powerset_Classical_facts]
single_limit [lemma, in Coq.Reals.Rlimit]
single_z_r_R1 [lemma, in Coq.Reals.RIneq]
singlx [lemma, in Coq.Sets.Powerset_facts]
sinh [definition, in Coq.Reals.Rtrigo_def]
sinh_0 [lemma, in Coq.Reals.Rtrigo_def]
sinh_lt [lemma, in Coq.Reals.Ranalysis4]
sinh_arcsinh [lemma, in Coq.Reals.Rpower]
sin_0 [lemma, in Coq.Reals.Rtrigo_def]
sin_antisym [lemma, in Coq.Reals.Rtrigo_def]
sin_in [definition, in Coq.Reals.Rtrigo_def]
sin_no_R0 [lemma, in Coq.Reals.Rtrigo_def]
sin_n [definition, in Coq.Reals.Rtrigo_def]
sin_pi_plus [lemma, in Coq.Reals.Rtrigo_facts]
sin_pi_minus [lemma, in Coq.Reals.Rtrigo_facts]
sin_tan [lemma, in Coq.Reals.Rtrigo_facts]
sin_cos_Rabs [lemma, in Coq.Reals.Rtrigo_facts]
sin_cos_opp [lemma, in Coq.Reals.Rtrigo_facts]
sin_cos [lemma, in Coq.Reals.Rtrigo_facts]
sin_eq_O_2PI_1 [lemma, in Coq.Reals.Rtrigo1]
sin_eq_O_2PI_0 [lemma, in Coq.Reals.Rtrigo1]
sin_eq_0_0 [lemma, in Coq.Reals.Rtrigo1]
sin_eq_0_1 [lemma, in Coq.Reals.Rtrigo1]
sin_decr_1 [lemma, in Coq.Reals.Rtrigo1]
sin_decr_0 [lemma, in Coq.Reals.Rtrigo1]
sin_incr_1 [lemma, in Coq.Reals.Rtrigo1]
sin_incr_0 [lemma, in Coq.Reals.Rtrigo1]
sin_inj [lemma, in Coq.Reals.Rtrigo1]
sin_decreasing_1 [lemma, in Coq.Reals.Rtrigo1]
sin_decreasing_0 [lemma, in Coq.Reals.Rtrigo1]
sin_increasing_1 [lemma, in Coq.Reals.Rtrigo1]
sin_increasing_0 [lemma, in Coq.Reals.Rtrigo1]
sin_lt_0_var [lemma, in Coq.Reals.Rtrigo1]
sin_lt_0 [lemma, in Coq.Reals.Rtrigo1]
sin_le_0 [lemma, in Coq.Reals.Rtrigo1]
sin_ge_0 [lemma, in Coq.Reals.Rtrigo1]
sin_gt_0 [lemma, in Coq.Reals.Rtrigo1]
sin_lb_gt_0 [lemma, in Coq.Reals.Rtrigo1]
sin_ub [definition, in Coq.Reals.Rtrigo1]
sin_lb [definition, in Coq.Reals.Rtrigo1]
SIN_bound [lemma, in Coq.Reals.Rtrigo1]
sin_shift [lemma, in Coq.Reals.Rtrigo1]
sin_period [lemma, in Coq.Reals.Rtrigo1]
sin_PI_x [lemma, in Coq.Reals.Rtrigo1]
sin_2PI [lemma, in Coq.Reals.Rtrigo1]
sin_neg [lemma, in Coq.Reals.Rtrigo1]
sin_2a [lemma, in Coq.Reals.Rtrigo1]
sin_minus [lemma, in Coq.Reals.Rtrigo1]
sin_plus [lemma, in Coq.Reals.Rtrigo1]
sin_cos [lemma, in Coq.Reals.Rtrigo1]
sin_bound [lemma, in Coq.Reals.Rtrigo1]
sin_PI [lemma, in Coq.Reals.Rtrigo1]
sin_PI2 [lemma, in Coq.Reals.Rtrigo1]
sin_pos_tech [lemma, in Coq.Reals.Rtrigo1]
sin_gt_cos_7_8 [lemma, in Coq.Reals.Rtrigo1]
sin_approx [definition, in Coq.Reals.Rtrigo_alt]
sin_term [definition, in Coq.Reals.Rtrigo_alt]
sin_acos [lemma, in Coq.Reals.Ratan]
sin_asin [lemma, in Coq.Reals.Ratan]
sin_atan [lemma, in Coq.Reals.Ratan]
sin_lb_ge_0 [lemma, in Coq.Reals.Rtrigo_calc]
sin_cos5PI4 [lemma, in Coq.Reals.Rtrigo_calc]
sin_5PI4 [lemma, in Coq.Reals.Rtrigo_calc]
sin_2PI3 [lemma, in Coq.Reals.Rtrigo_calc]
sin_PI3 [lemma, in Coq.Reals.Rtrigo_calc]
sin_3PI4 [lemma, in Coq.Reals.Rtrigo_calc]
sin_PI4 [lemma, in Coq.Reals.Rtrigo_calc]
sin_PI6 [lemma, in Coq.Reals.Rtrigo_calc]
sin_PI6_cos_PI3 [lemma, in Coq.Reals.Rtrigo_calc]
sin_PI3_cos_PI6 [lemma, in Coq.Reals.Rtrigo_calc]
sin_cos_PI4 [lemma, in Coq.Reals.Rtrigo_calc]
sin_3PI2 [lemma, in Coq.Reals.Rtrigo_calc]
sin2 [lemma, in Coq.Reals.Rtrigo1]
sin2_bound [lemma, in Coq.Reals.Rtrigo_facts]
sin2_cos2 [lemma, in Coq.Reals.Rtrigo1]
sin3PI4 [abbreviation, in Coq.Reals.Rtrigo_calc]
sixteen [abbreviation, in Coq.Init.Nat]
size [definition, in Coq.Numbers.Cyclic.Int63.Int63]
size [definition, in Coq.Numbers.Cyclic.Int31.Int31]
size1:406 [binder, in Coq.MSets.MSetRBT]
size1:682 [binder, in Coq.MSets.MSetRBT]
size2:407 [binder, in Coq.MSets.MSetRBT]
size2:683 [binder, in Coq.MSets.MSetRBT]
size:399 [binder, in Coq.MSets.MSetRBT]
size:408 [binder, in Coq.MSets.MSetRBT]
size:50 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
size:676 [binder, in Coq.MSets.MSetRBT]
size:684 [binder, in Coq.MSets.MSetRBT]
si:164 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
si:170 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
si:21 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
si:29 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
si:39 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
si:59 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
si:65 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
SI:80 [binder, in Coq.Reals.Runcountable]
si:90 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
skipn [definition, in Coq.Lists.List]
skipn_rev [lemma, in Coq.Lists.List]
skipn_app [lemma, in Coq.Lists.List]
skipn_length [lemma, in Coq.Lists.List]
skipn_all2 [lemma, in Coq.Lists.List]
skipn_none [abbreviation, in Coq.Lists.List]
skipn_all [lemma, in Coq.Lists.List]
skipn_cons [lemma, in Coq.Lists.List]
skipn_nil [lemma, in Coq.Lists.List]
skipn_O [lemma, in Coq.Lists.List]
skipn_firstn_comm [lemma, in Coq.Lists.List]
SlowConstructiveRealsMorphism [definition, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
SlowMorph [definition, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
SlowMorph_increasing [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
SlowMorph_increasing_Ql [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
SlowMorph_increasing_Qr [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
SmallDrinker'sParadox [definition, in Coq.Logic.ChoiceFacts]
small_drinkers'_paradox [lemma, in Coq.Logic.Epsilon]
Smorph_morph [lemma, in Coq.setoid_ring.Ring_theory]
Smorph_sub [lemma, in Coq.setoid_ring.Ring_theory]
Smorph_opp [lemma, in Coq.setoid_ring.Ring_theory]
Smorph_eq [projection, in Coq.setoid_ring.Ring_theory]
Smorph_mul [projection, in Coq.setoid_ring.Ring_theory]
Smorph_add [projection, in Coq.setoid_ring.Ring_theory]
Smorph0 [projection, in Coq.setoid_ring.Ring_theory]
Smorph1 [projection, in Coq.setoid_ring.Ring_theory]
Snd [abbreviation, in Coq.Classes.RelationPairs]
snd [definition, in Coq.Init.Datatypes]
SndRel_sub [instance, in Coq.Classes.RelationPairs]
SndRel_ProdRel [lemma, in Coq.Classes.RelationPairs]
sndT [abbreviation, in Coq.Init.Datatypes]
snd_compat [instance, in Coq.Classes.RelationPairs]
snd_measure [instance, in Coq.Classes.RelationPairs]
sneakl [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sneakl_shiftr [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sneakr [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sneakr_shiftl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
solution_right [lemma, in Coq.Program.Equality]
solution_left [lemma, in Coq.Program.Equality]
sol_x2 [definition, in Coq.Reals.R_sqrt]
sol_x1 [definition, in Coq.Reals.R_sqrt]
some [abbreviation, in Coq.ssr.ssrfun]
Some [constructor, in Coq.Init.Datatypes]
Some_inj [lemma, in Coq.ssr.ssrfun]
SOR [record, in Coq.micromega.OrderedRing]
SORaddon [record, in Coq.micromega.RingMicromega]
SORcleb_morph [projection, in Coq.micromega.RingMicromega]
SORcneqb_morph [projection, in Coq.micromega.RingMicromega]
Sord [module, in Coq.FSets.FMapInterface]
Sord.cmp [definition, in Coq.FSets.FMapInterface]
Sord.compare [axiom, in Coq.FSets.FMapInterface]
Sord.Data [module, in Coq.FSets.FMapInterface]
Sord.eq [axiom, in Coq.FSets.FMapInterface]
Sord.eq_2 [axiom, in Coq.FSets.FMapInterface]
Sord.eq_1 [axiom, in Coq.FSets.FMapInterface]
Sord.eq_trans [axiom, in Coq.FSets.FMapInterface]
Sord.eq_sym [axiom, in Coq.FSets.FMapInterface]
Sord.eq_refl [axiom, in Coq.FSets.FMapInterface]
Sord.lt [axiom, in Coq.FSets.FMapInterface]
Sord.lt_not_eq [axiom, in Coq.FSets.FMapInterface]
Sord.lt_trans [axiom, in Coq.FSets.FMapInterface]
Sord.MapS [module, in Coq.FSets.FMapInterface]
Sord.t [definition, in Coq.FSets.FMapInterface]
SORle_trans [projection, in Coq.micromega.OrderedRing]
SORle_antisymm [projection, in Coq.micromega.OrderedRing]
SORle_refl [projection, in Coq.micromega.OrderedRing]
SORle_wd [projection, in Coq.micromega.OrderedRing]
SORlt_trichotomy [projection, in Coq.micromega.OrderedRing]
SORlt_le_neq [projection, in Coq.micromega.OrderedRing]
SORlt_wd [projection, in Coq.micromega.OrderedRing]
SORneq_0_1 [projection, in Coq.micromega.OrderedRing]
SORopp_wd [projection, in Coq.micromega.OrderedRing]
SORplus_le_mono_l [projection, in Coq.micromega.OrderedRing]
SORplus_wd [projection, in Coq.micromega.OrderedRing]
SORpower [projection, in Coq.micromega.RingMicromega]
SORrm [projection, in Coq.micromega.RingMicromega]
SORrt [projection, in Coq.micromega.OrderedRing]
SORsetoid [projection, in Coq.micromega.OrderedRing]
sort [abbreviation, in Coq.Sorting.Sorted]
Sort [module, in Coq.Sorting.Mergesort]
SortA [abbreviation, in Coq.Lists.SetoidList]
SortA_equivlistA_eqlistA [lemma, in Coq.Lists.SetoidList]
SortA_NoDupA [lemma, in Coq.Lists.SetoidList]
SortA_app [lemma, in Coq.Lists.SetoidList]
SortA_InfA_InA [lemma, in Coq.Lists.SetoidList]
Sorted [inductive, in Coq.Sorting.Sorted]
Sorted [library]
Sorted_StronglySorted [lemma, in Coq.Sorting.Sorted]
Sorted_extends [lemma, in Coq.Sorting.Sorted]
Sorted_LocallySorted_iff [lemma, in Coq.Sorting.Sorted]
Sorted_rect [lemma, in Coq.Sorting.Sorted]
Sorted_inv [lemma, in Coq.Sorting.Sorted]
Sorted_cons [constructor, in Coq.Sorting.Sorted]
Sorted_nil [constructor, in Coq.Sorting.Sorted]
SORtimes_pos_pos [projection, in Coq.micromega.OrderedRing]
SORtimes_wd [projection, in Coq.micromega.OrderedRing]
Sorting [library]
sort_rect [abbreviation, in Coq.Sorting.Sorted]
sort_inv [abbreviation, in Coq.Sorting.Sorted]
Sort.flatten_stack [definition, in Coq.Sorting.Mergesort]
Sort.iter_merge [definition, in Coq.Sorting.Mergesort]
Sort.LocallySorted_sort [lemma, in Coq.Sorting.Mergesort]
Sort.merge [definition, in Coq.Sorting.Mergesort]
Sort.merge_stack [definition, in Coq.Sorting.Mergesort]
Sort.merge_list_to_stack [definition, in Coq.Sorting.Mergesort]
Sort.Permuted_sort [lemma, in Coq.Sorting.Mergesort]
Sort.Permuted_iter_merge [lemma, in Coq.Sorting.Mergesort]
Sort.Permuted_merge_stack [lemma, in Coq.Sorting.Mergesort]
Sort.Permuted_merge_list_to_stack [lemma, in Coq.Sorting.Mergesort]
Sort.Permuted_merge [lemma, in Coq.Sorting.Mergesort]
Sort.sort [definition, in Coq.Sorting.Mergesort]
Sort.Sorted [abbreviation, in Coq.Sorting.Mergesort]
Sort.SortedStack [definition, in Coq.Sorting.Mergesort]
Sort.Sorted_sort [lemma, in Coq.Sorting.Mergesort]
Sort.Sorted_iter_merge [lemma, in Coq.Sorting.Mergesort]
Sort.Sorted_merge_stack [lemma, in Coq.Sorting.Mergesort]
Sort.Sorted_merge_list_to_stack [lemma, in Coq.Sorting.Mergesort]
Sort.Sorted_merge [lemma, in Coq.Sorting.Mergesort]
Sort.StronglySorted_sort [lemma, in Coq.Sorting.Mergesort]
source [projection, in Coq.micromega.ZifyClasses]
source_prop [projection, in Coq.micromega.ZifyClasses]
SP [definition, in Coq.Reals.PartSum]
Space [definition, in Coq.Strings.Ascii]
SpecFloat [library]
Specif [library]
Specific_orders.U [variable, in Coq.Sets.Cpo]
Specific_orders [section, in Coq.Sets.Cpo]
specs:174 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
specs:197 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
spec_lxor [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_land [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_lor [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_is_even [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_eq0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_sqrt2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_sqrt [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_tail0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_tail00 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_head0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_head00 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_pos_mod [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_add_mul_div [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_gcd [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_mod [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_div [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_div21 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_square_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_mul [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_mul_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_pred [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_pred_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_opp_carry [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_opp [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_opp_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_sub_carry [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_sub [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_sub_carry_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_sub_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_succ [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_add_carry [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_add [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_add_carry_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_succ_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_add_c [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_compare [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_m1 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_1 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_more_than_1_digit [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_zdigits [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
spec_lxor [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_land [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_lor [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_tail0 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_tail00 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_head0 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_head00 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_sqrt2 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_sqrt [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_is_even [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_pos_mod [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_add_mul_div [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_div21 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_gcd_gt [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_gcd [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_modulo_gt [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_modulo [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_div_gt [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_div [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_square_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_mul [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_mul_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_sub_carry [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_sub [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_pred [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_sub_carry_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_sub_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_pred_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_add_carry [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_add [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_succ [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_add_carry_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_add_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_succ_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_opp_carry [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_opp [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_opp_c [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_eq0 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_compare [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_Bm1 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_1 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_0 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_zdigits [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_of_pos [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_to_Z [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_to_Z_2 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_to_Z_1 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_more_than_1_digit [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
spec_float [inductive, in Coq.Floats.SpecFloat]
split [definition, in Coq.Lists.List]
split [definition, in Coq.setoid_ring.Field_theory]
SplitAbsolu [library]
splitat [definition, in Coq.Vectors.VectorDef]
splitat_append [lemma, in Coq.Vectors.VectorSpec]
SplitRmult [library]
splitSum [lemma, in Coq.Reals.Abstract.ConstructiveSum]
split_lt_succ [lemma, in Coq.Reals.Runcountable]
split_couple_eq [lemma, in Coq.Reals.Runcountable]
split_combine [lemma, in Coq.Lists.List]
split_length_r [lemma, in Coq.Lists.List]
split_length_l [lemma, in Coq.Lists.List]
split_nth [lemma, in Coq.Lists.List]
split_nz_r [lemma, in Coq.setoid_ring.Field_theory]
split_nz_l [lemma, in Coq.setoid_ring.Field_theory]
split_ok_r [lemma, in Coq.setoid_ring.Field_theory]
split_ok_l [lemma, in Coq.setoid_ring.Field_theory]
split_aux_ok [lemma, in Coq.setoid_ring.Field_theory]
split_aux_ok1 [lemma, in Coq.setoid_ring.Field_theory]
split_aux [definition, in Coq.setoid_ring.Field_theory]
Splus_lt [lemma, in Coq.funind.Recdef]
Spr1 [projection, in Coq.Logic.StrictProp]
Spr1_inj [lemma, in Coq.Logic.StrictProp]
Spr2 [projection, in Coq.Logic.StrictProp]
sp_swap [constructor, in Coq.Relations.Relation_Operators]
sp_noswap [constructor, in Coq.Relations.Relation_Operators]
sp:288 [binder, in Coq.ssr.ssrbool]
sp:372 [binder, in Coq.ssr.ssrbool]
sp:374 [binder, in Coq.ssr.ssrbool]
sp:381 [binder, in Coq.ssr.ssrbool]
sp:415 [binder, in Coq.ssr.ssrbool]
sqrt [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
sqrt [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sqrt [axiom, in Coq.Floats.PrimFloat]
sqrt [definition, in Coq.Reals.R_sqrt]
sqrt [definition, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt [definition, in Coq.Init.Nat]
Sqrt [module, in Coq.Numbers.NatInt.NZSqrt]
SqrtNotation [module, in Coq.Numbers.NatInt.NZSqrt]
√ _ [notation, in Coq.Numbers.NatInt.NZSqrt]
sqrt_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
sqrt_iter_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
sqrt_iter [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
sqrt_test_false [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt_test_true [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt_init [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt_main [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt_main_trick [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt_continuity_pt [lemma, in Coq.Reals.Sqrt_reg]
sqrt_continuity_pt_R1 [lemma, in Coq.Reals.Sqrt_reg]
sqrt_var_maj [lemma, in Coq.Reals.Sqrt_reg]
sqrt_cauchy [lemma, in Coq.Reals.R_sqrt]
sqrt_more [lemma, in Coq.Reals.R_sqrt]
sqrt_less [lemma, in Coq.Reals.R_sqrt]
sqrt_less_alt [lemma, in Coq.Reals.R_sqrt]
sqrt_inj [lemma, in Coq.Reals.R_sqrt]
sqrt_neg_0 [lemma, in Coq.Reals.R_sqrt]
sqrt_le_1 [lemma, in Coq.Reals.R_sqrt]
sqrt_le_1_alt [lemma, in Coq.Reals.R_sqrt]
sqrt_le_0 [lemma, in Coq.Reals.R_sqrt]
sqrt_lt_1 [lemma, in Coq.Reals.R_sqrt]
sqrt_lt_1_alt [lemma, in Coq.Reals.R_sqrt]
sqrt_lt_0 [lemma, in Coq.Reals.R_sqrt]
sqrt_lt_0_alt [lemma, in Coq.Reals.R_sqrt]
sqrt_div [lemma, in Coq.Reals.R_sqrt]
sqrt_div_alt [lemma, in Coq.Reals.R_sqrt]
sqrt_lt_R0 [lemma, in Coq.Reals.R_sqrt]
sqrt_mult [lemma, in Coq.Reals.R_sqrt]
sqrt_mult_alt [lemma, in Coq.Reals.R_sqrt]
sqrt_Rsqr_abs [lemma, in Coq.Reals.R_sqrt]
sqrt_pow2 [lemma, in Coq.Reals.R_sqrt]
sqrt_Rsqr [lemma, in Coq.Reals.R_sqrt]
sqrt_square [lemma, in Coq.Reals.R_sqrt]
sqrt_def [lemma, in Coq.Reals.R_sqrt]
sqrt_lem_1 [lemma, in Coq.Reals.R_sqrt]
sqrt_lem_0 [lemma, in Coq.Reals.R_sqrt]
sqrt_eq_0 [lemma, in Coq.Reals.R_sqrt]
sqrt_1 [lemma, in Coq.Reals.R_sqrt]
sqrt_0 [lemma, in Coq.Reals.R_sqrt]
sqrt_sqrt [lemma, in Coq.Reals.R_sqrt]
sqrt_positivity [lemma, in Coq.Reals.R_sqrt]
sqrt_pos [lemma, in Coq.Reals.R_sqrt]
sqrt_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_init [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_step_correct [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_test_true [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_test_false [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_main [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_main_trick [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_step [definition, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_iter [definition, in Coq.Init.Nat]
sqrt_spec [axiom, in Coq.Floats.FloatAxioms]
Sqrt_reg [library]
Sqrt' [module, in Coq.Numbers.NatInt.NZSqrt]
Sqrt.sqrt [axiom, in Coq.Numbers.NatInt.NZSqrt]
sqrt2 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sqrt2 [definition, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_step_correct [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_lower_bound [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_step_def [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_step [definition, in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_neq_0 [lemma, in Coq.Reals.Rtrigo_calc]
sqrt3_2_neq_0 [lemma, in Coq.Reals.Rtrigo_calc]
sqrt31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sqrt31_step_correct [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt31_step_def [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt31_step [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sqrt312 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sqrt312_step_correct [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt312_lower_bound [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt312_step_def [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
sqrt312_step [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sqr_pos [lemma, in Coq.ZArith.Zcomplements]
square [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
square [definition, in Coq.Init.Nat]
squarec_spec [lemma, in Coq.Numbers.Cyclic.Int63.Cyclic63]
square_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
square_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
square_not_prime [lemma, in Coq.ZArith.Znumtheory]
squash [constructor, in Coq.Logic.StrictProp]
Squash [inductive, in Coq.Logic.StrictProp]
SRadd_ext [projection, in Coq.setoid_ring.Ring_theory]
SRadd_assoc [projection, in Coq.setoid_ring.Ring_theory]
SRadd_comm [projection, in Coq.setoid_ring.Ring_theory]
SRadd_0_l [projection, in Coq.setoid_ring.Ring_theory]
SRdistr_l [projection, in Coq.setoid_ring.Ring_theory]
SReqe_Reqe [lemma, in Coq.setoid_ring.Ring_theory]
sreq:119 [binder, in Coq.setoid_ring.InitialRing]
sreq:120 [binder, in Coq.setoid_ring.InitialRing]
sreq:121 [binder, in Coq.setoid_ring.InitialRing]
sreq:125 [binder, in Coq.setoid_ring.InitialRing]
sreq:126 [binder, in Coq.setoid_ring.InitialRing]
sreq:127 [binder, in Coq.setoid_ring.InitialRing]
SRIDmorph [definition, in Coq.setoid_ring.Ring_theory]
sring_eq_ext [record, in Coq.setoid_ring.Ring_theory]
SRmorph_Rmorph [lemma, in Coq.setoid_ring.Ring_theory]
SRmul_ext [projection, in Coq.setoid_ring.Ring_theory]
SRmul_assoc [projection, in Coq.setoid_ring.Ring_theory]
SRmul_comm [projection, in Coq.setoid_ring.Ring_theory]
SRmul_0_l [projection, in Coq.setoid_ring.Ring_theory]
SRmul_1_l [projection, in Coq.setoid_ring.Ring_theory]
SRopp [definition, in Coq.setoid_ring.Ring_theory]
SRopp_add [lemma, in Coq.setoid_ring.Ring_theory]
SRopp_mul_l [lemma, in Coq.setoid_ring.Ring_theory]
SRopp_ext [lemma, in Coq.setoid_ring.Ring_theory]
SRsub [definition, in Coq.setoid_ring.Ring_theory]
SRsub_def [lemma, in Coq.setoid_ring.Ring_theory]
SRth_ARth [lemma, in Coq.setoid_ring.Ring_theory]
sr:301 [binder, in Coq.ssr.ssrbool]
Ssig [record, in Coq.Logic.StrictProp]
SSorted_cons [constructor, in Coq.Sorting.Sorted]
SSorted_nil [constructor, in Coq.Sorting.Sorted]
SSplus_lt [lemma, in Coq.funind.Recdef]
ssrbool [library]
ssrclasses [library]
ssreflect [library]
ssrfun [library]
ssrmatching [library]
SsrMatchingSyntax [module, in Coq.ssrmatching.ssrmatching]
SsrMatchingSyntax.LHS [abbreviation, in Coq.ssrmatching.ssrmatching]
SsrMatchingSyntax.RHS [abbreviation, in Coq.ssrmatching.ssrmatching]
( _ in _ ) (ssrpatternscope) [notation, in Coq.ssrmatching.ssrmatching]
ssrsearch [library]
ssrsetoid [library]
SsrSyntax [module, in Coq.ssr.ssreflect]
ssrunder [library]
ssr_congr_arrow [lemma, in Coq.ssr.ssreflect]
ssr_wlog [definition, in Coq.ssr.ssreflect]
ssr_suff [definition, in Coq.ssr.ssreflect]
ssr_have_let [definition, in Coq.ssr.ssreflect]
ssr_have [definition, in Coq.ssr.ssreflect]
ssr_converse [definition, in Coq.ssr.ssreflect]
Sstar_contains_Rstar [lemma, in Coq.Sets.Relations_2_facts]
stack:13 [binder, in Coq.Sorting.Mergesort]
stack:16 [binder, in Coq.Sorting.Mergesort]
stack:20 [binder, in Coq.Sorting.Mergesort]
stack:23 [binder, in Coq.Sorting.Mergesort]
stack:36 [binder, in Coq.Sorting.Mergesort]
stack:38 [binder, in Coq.Sorting.Mergesort]
stack:40 [binder, in Coq.Sorting.Mergesort]
stack:41 [binder, in Coq.Sorting.Mergesort]
stack:42 [binder, in Coq.Sorting.Mergesort]
stack:45 [binder, in Coq.Sorting.Mergesort]
stack:9 [binder, in Coq.Sorting.Mergesort]
start:27 [binder, in Coq.Logic.ConstructiveEpsilon]
start:859 [binder, in Coq.Lists.List]
start:864 [binder, in Coq.Lists.List]
start:866 [binder, in Coq.Lists.List]
start:868 [binder, in Coq.Lists.List]
start:872 [binder, in Coq.Lists.List]
start:874 [binder, in Coq.Lists.List]
start:877 [binder, in Coq.Lists.List]
start:880 [binder, in Coq.Lists.List]
start:882 [binder, in Coq.Lists.List]
star_monotone [lemma, in Coq.Sets.Relations_2_facts]
statement:6 [binder, in Coq.ssr.ssreflect]
Std [library]
Step [abbreviation, in Coq.NArith.Ndigits]
StepFun [record, in Coq.Reals.RiemannInt_SF]
StepFun_P46 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P45 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P44 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P43 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P42 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P41 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P40 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P39 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P38 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P37 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P36 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P35 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P34 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P33 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P32 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P31 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P30 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P29 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P28 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P27 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P26 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P25 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P24 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P23 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P22 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P21 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P20 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P19 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P18 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P17 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P16 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P15 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P14 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P13 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P12 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P11 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P10 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P9 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P8 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P7 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P6 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P5 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P4 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P3 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P2 [lemma, in Coq.Reals.RiemannInt_SF]
StepFun_P1 [lemma, in Coq.Reals.RiemannInt_SF]
step:76 [binder, in Coq.ssr.ssreflect]
step:80 [binder, in Coq.ssr.ssreflect]
step:85 [binder, in Coq.ssr.ssreflect]
stop [constructor, in Coq.Logic.ConstructiveEpsilon]
Store [record, in Coq.rtauto.Bintree]
Store [section, in Coq.rtauto.Bintree]
Store.A [variable, in Coq.rtauto.Bintree]
Stream [abbreviation, in Coq.Lists.Streams]
Stream [inductive, in Coq.Lists.Streams]
StreamMemo [library]
Streams [section, in Coq.Lists.Streams]
Streams [library]
Streams.A [variable, in Coq.Lists.Streams]
Streams.Stream_Properties.Co_Induction_ForAll.InvIsStable [variable, in Coq.Lists.Streams]
Streams.Stream_Properties.Co_Induction_ForAll.InvThenP [variable, in Coq.Lists.Streams]
Streams.Stream_Properties.Co_Induction_ForAll.Inv [variable, in Coq.Lists.Streams]
Streams.Stream_Properties.Co_Induction_ForAll [section, in Coq.Lists.Streams]
Streams.Stream_Properties.P [variable, in Coq.Lists.Streams]
Streams.Stream_Properties [section, in Coq.Lists.Streams]
Streicher_K:178 [binder, in Coq.Logic.EqdepFacts]
Streicher_K__eq_rect_eq [lemma, in Coq.Logic.EqdepFacts]
Streicher_K_on__eq_rect_eq_on [lemma, in Coq.Logic.EqdepFacts]
Streicher_K_ [definition, in Coq.Logic.EqdepFacts]
Streicher_K_on_ [definition, in Coq.Logic.EqdepFacts]
Strict [constructor, in Coq.micromega.RingMicromega]
strictincreasing_strictdecreasing_opp [lemma, in Coq.Reals.MVT]
StrictOrder [record, in Coq.Classes.RelationClasses]
StrictOrder [record, in Coq.Classes.CRelationClasses]
StrictOrder_Asymmetric [instance, in Coq.Classes.RelationClasses]
StrictOrder_Transitive [projection, in Coq.Classes.RelationClasses]
StrictOrder_Irreflexive [projection, in Coq.Classes.RelationClasses]
StrictOrder_PartialOrder [lemma, in Coq.Classes.Morphisms]
StrictOrder_PreOrder [lemma, in Coq.Classes.Morphisms]
StrictOrder_PartialOrder [lemma, in Coq.Classes.CMorphisms]
StrictOrder_PreOrder [lemma, in Coq.Classes.CMorphisms]
StrictOrder_Asymmetric [instance, in Coq.Classes.CRelationClasses]
StrictOrder_Transitive [projection, in Coq.Classes.CRelationClasses]
StrictOrder_Irreflexive [projection, in Coq.Classes.CRelationClasses]
StrictProp [library]
strict_decreasing [definition, in Coq.Reals.Ranalysis1]
strict_increasing [definition, in Coq.Reals.Ranalysis1]
Strict_Included_strict [lemma, in Coq.Sets.Constructive_sets]
Strict_Included_intro [lemma, in Coq.Sets.Constructive_sets]
Strict_Included [definition, in Coq.Sets.Ensembles]
_ < _ [notation, in Coq.micromega.OrderedRing]
_ <= _ [notation, in Coq.micromega.OrderedRing]
_ ~= _ [notation, in Coq.micromega.OrderedRing]
_ == _ [notation, in Coq.micromega.OrderedRing]
- _ [notation, in Coq.micromega.OrderedRing]
_ - _ [notation, in Coq.micromega.OrderedRing]
_ * _ [notation, in Coq.micromega.OrderedRing]
_ + _ [notation, in Coq.micromega.OrderedRing]
1 [notation, in Coq.micromega.OrderedRing]
0 [notation, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.sor [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.rlt [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.rle [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.req [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.ropp [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.rminus [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.rtimes [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.rplus [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.rI [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.rO [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING.R [variable, in Coq.micromega.OrderedRing]
STRICT_ORDERED_RING [section, in Coq.micromega.OrderedRing]
Strict_Rel_Transitive [lemma, in Coq.Sets.Partial_Order]
Strict_Rel_Transitive_with_Rel_left [lemma, in Coq.Sets.Partial_Order]
Strict_Rel_Transitive_with_Rel [lemma, in Coq.Sets.Partial_Order]
Strict_Rel_of [definition, in Coq.Sets.Partial_Order]
Strict_Included_inv [lemma, in Coq.Sets.Classical_sets]
Strict_super_set_contains_new_element [lemma, in Coq.Sets.Classical_sets]
Strict_inclusion_is_transitive [lemma, in Coq.Sets.Powerset]
Strict_inclusion_is_transitive_with_inclusion_left [lemma, in Coq.Sets.Powerset]
Strict_inclusion_is_transitive_with_inclusion [lemma, in Coq.Sets.Powerset]
Strict_Rel_is_Strict_Included [lemma, in Coq.Sets.Powerset]
String [constructor, in Coq.Strings.String]
string [inductive, in Coq.Strings.String]
String [library]
String [library]
StringSyntax [module, in Coq.Strings.String]
string_of_list_byte_of_string [lemma, in Coq.Strings.String]
string_of_list_byte [definition, in Coq.Strings.String]
string_of_list_ascii_of_string [lemma, in Coq.Strings.String]
string_of_list_ascii [definition, in Coq.Strings.String]
string_dec [definition, in Coq.Strings.String]
String_as_OT.eq_dec [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.compare [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.compare_helper_eq [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.compare_helper_gt [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.compare_helper_lt [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.cmp_lt [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.cmp_antisym [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.cmp_eq [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.cmp [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.lt_not_eq [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.lt_trans [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.lts_tail_unique [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.nat_of_ascii_inverse [lemma, in Coq.Structures.OrderedTypeEx]
String_as_OT.lt [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.lts_head [constructor, in Coq.Structures.OrderedTypeEx]
String_as_OT.lts_tail [constructor, in Coq.Structures.OrderedTypeEx]
String_as_OT.lts_empty [constructor, in Coq.Structures.OrderedTypeEx]
String_as_OT.lts [inductive, in Coq.Structures.OrderedTypeEx]
String_as_OT.eq_trans [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.eq_sym [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.eq_refl [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.eq [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT.t [definition, in Coq.Structures.OrderedTypeEx]
String_as_OT [module, in Coq.Structures.OrderedTypeEx]
strip_commut [lemma, in Coq.Wellfounded.Union]
StronglySorted [inductive, in Coq.Sorting.Sorted]
StronglySorted_Sorted [lemma, in Coq.Sorting.Sorted]
StronglySorted_rec [lemma, in Coq.Sorting.Sorted]
StronglySorted_rect [lemma, in Coq.Sorting.Sorted]
StronglySorted_inv [lemma, in Coq.Sorting.Sorted]
Strongly_confluent [definition, in Coq.Sets.Relations_2]
Strong_confluence_direct [lemma, in Coq.Sets.Relations_3_facts]
Strong_confluence [lemma, in Coq.Sets.Relations_3_facts]
StrOrder [module, in Coq.Structures.Orders]
StrOrder' [module, in Coq.Structures.Orders]
Str_nth_zipWith [lemma, in Coq.Lists.Streams]
Str_nth_tl_zipWith [lemma, in Coq.Lists.Streams]
Str_nth_map [lemma, in Coq.Lists.Streams]
Str_nth_tl_map [lemma, in Coq.Lists.Streams]
Str_nth_plus [lemma, in Coq.Lists.Streams]
Str_nth_tl_plus [lemma, in Coq.Lists.Streams]
Str_nth [definition, in Coq.Lists.Streams]
Str_nth_tl [definition, in Coq.Lists.Streams]
stt [constructor, in Coq.Logic.StrictProp]
st:125 [binder, in Coq.MSets.MSetEqProperties]
st:125 [binder, in Coq.FSets.FSetEqProperties]
st:126 [binder, in Coq.MSets.MSetProperties]
st:126 [binder, in Coq.FSets.FSetProperties]
sT:13 [binder, in Coq.ssr.ssreflect]
st:134 [binder, in Coq.MSets.MSetProperties]
st:134 [binder, in Coq.FSets.FSetProperties]
sT:20 [binder, in Coq.ssr.ssreflect]
sT:26 [binder, in Coq.ssr.ssreflect]
st:281 [binder, in Coq.MSets.MSetProperties]
st:281 [binder, in Coq.FSets.FSetProperties]
st:289 [binder, in Coq.MSets.MSetProperties]
st:289 [binder, in Coq.FSets.FSetProperties]
st:544 [binder, in Coq.FSets.FMapFacts]
st:681 [binder, in Coq.FSets.FMapFacts]
st:690 [binder, in Coq.FSets.FMapFacts]
st:700 [binder, in Coq.FSets.FMapFacts]
sub [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub [axiom, in Coq.Floats.PrimFloat]
sub [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
sub [definition, in Coq.Init.Nat]
subc [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
subcarry [definition, in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc_def_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc_def [definition, in Coq.Numbers.Cyclic.Int63.Int63]
subcarry_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
subc_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
subc_def_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
subc_def [definition, in Coq.Numbers.Cyclic.Int63.Int63]
subdivision [definition, in Coq.Reals.RiemannInt_SF]
subdivision_val [definition, in Coq.Reals.RiemannInt_SF]
SubEqui [definition, in Coq.Reals.RiemannInt]
SubEquiN [definition, in Coq.Reals.RiemannInt]
SubEqui_P9 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P8 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P7 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P6 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P5 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P4 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P3 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P2 [lemma, in Coq.Reals.RiemannInt]
SubEqui_P1 [lemma, in Coq.Reals.RiemannInt]
subfamily [definition, in Coq.Reals.Rtopology]
subl:54 [binder, in Coq.Classes.Morphisms]
subl:56 [binder, in Coq.Classes.CMorphisms]
subon_bij [lemma, in Coq.ssr.ssrbool]
subon1 [lemma, in Coq.ssr.ssrbool]
subon1l [lemma, in Coq.ssr.ssrbool]
subon2 [lemma, in Coq.ssr.ssrbool]
subpred [definition, in Coq.ssr.ssrbool]
subrel [definition, in Coq.ssr.ssrbool]
subrelation [record, in Coq.Classes.RelationClasses]
subrelation [inductive, in Coq.Classes.RelationClasses]
subrelation [record, in Coq.Classes.CRelationClasses]
subrelation [inductive, in Coq.Classes.CRelationClasses]
subrelation [definition, in Coq.Init.Logic]
subrelation_partial_order [instance, in Coq.Classes.RelationClasses]
subrelation_symmetric [lemma, in Coq.Classes.RelationClasses]
subrelation_proper [lemma, in Coq.Classes.Morphisms]
subrelation_refl [lemma, in Coq.Classes.Morphisms]
subrelation_respectful [lemma, in Coq.Classes.Morphisms]
subrelation_id_proper [instance, in Coq.Classes.Morphisms]
subrelation_proper [lemma, in Coq.Classes.CMorphisms]
subrelation_refl [lemma, in Coq.Classes.CMorphisms]
subrelation_respectful [lemma, in Coq.Classes.CMorphisms]
subrelation_id_proper [instance, in Coq.Classes.CMorphisms]
subrelation_symmetric [lemma, in Coq.Classes.CRelationClasses]
subrelation_pointwise [instance, in Coq.Classes.Morphisms_Relations]
subrelUl [lemma, in Coq.ssr.ssrbool]
subrelUr [lemma, in Coq.ssr.ssrbool]
subr:57 [binder, in Coq.Classes.Morphisms]
subr:60 [binder, in Coq.Classes.CMorphisms]
subset [definition, in Coq.Logic.ClassicalChoice]
Subset [library]
subset_types_imp_guarded_rel_choice_iff_rel_choice [lemma, in Coq.Logic.ChoiceFacts]
Subset_projections2.Q [variable, in Coq.Init.Specif]
Subset_projections2.P [variable, in Coq.Init.Specif]
Subset_projections2.A [variable, in Coq.Init.Specif]
Subset_projections2 [section, in Coq.Init.Specif]
Subset_projections.P [variable, in Coq.Init.Specif]
Subset_projections.A [variable, in Coq.Init.Specif]
Subset_projections [section, in Coq.Init.Specif]
subset_eq [lemma, in Coq.Program.Subset]
subset_r1:327 [binder, in Coq.MSets.MSetGenTree]
subset_l1:318 [binder, in Coq.MSets.MSetGenTree]
subset_r1:73 [binder, in Coq.MSets.MSetGenTree]
subset_l1:68 [binder, in Coq.MSets.MSetGenTree]
substring [definition, in Coq.Strings.String]
substring_correct2 [lemma, in Coq.Strings.String]
substring_correct1 [lemma, in Coq.Strings.String]
Subtract [definition, in Coq.Sets.Ensembles]
subtraction [projection, in Coq.setoid_ring.Algebra_syntax]
Subtraction [record, in Coq.setoid_ring.Algebra_syntax]
subtraction [constructor, in Coq.setoid_ring.Algebra_syntax]
Subtraction [inductive, in Coq.setoid_ring.Algebra_syntax]
Subtract_inv [lemma, in Coq.Sets.Classical_sets]
Subtract_intro [lemma, in Coq.Sets.Classical_sets]
sub_carry [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub_carry_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
sub_in21 [lemma, in Coq.ssr.ssrbool]
sub_in12 [lemma, in Coq.ssr.ssrbool]
sub_in3 [lemma, in Coq.ssr.ssrbool]
sub_in2 [lemma, in Coq.ssr.ssrbool]
sub_in_bij [lemma, in Coq.ssr.ssrbool]
sub_in111 [lemma, in Coq.ssr.ssrbool]
sub_in11 [lemma, in Coq.ssr.ssrbool]
sub_in1 [lemma, in Coq.ssr.ssrbool]
sub_refl [lemma, in Coq.ssr.ssrbool]
sub_mem [definition, in Coq.ssr.ssrbool]
Sub_Add_new [lemma, in Coq.Sets.Powerset_Classical_facts]
sub_notation [instance, in Coq.setoid_ring.Ncring]
sub_spec [axiom, in Coq.Floats.FloatAxioms]
sub31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sub31c [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sub31carryc [definition, in Coq.Numbers.Cyclic.Int31.Int31]
sub:10 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]
sub:10 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]
sub:6 [binder, in Coq.setoid_ring.Ncring]
sub:64 [binder, in Coq.Classes.Morphisms]
sub:67 [binder, in Coq.Classes.Morphisms]
sub:67 [binder, in Coq.Classes.CMorphisms]
sub:71 [binder, in Coq.Classes.CMorphisms]
succ [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
succ [definition, in Coq.Numbers.Cyclic.Int63.Int63]
succ [definition, in Coq.Init.Nat]
succc [definition, in Coq.Numbers.Cyclic.Int63.Int63]
succc_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
SuccNat2Pos [module, in Coq.PArith.Pnat]
SuccNat2Pos.id_succ [lemma, in Coq.PArith.Pnat]
SuccNat2Pos.inj [lemma, in Coq.PArith.Pnat]
SuccNat2Pos.inj_compare [lemma, in Coq.PArith.Pnat]
SuccNat2Pos.inj_succ [lemma, in Coq.PArith.Pnat]
SuccNat2Pos.inj_iff [lemma, in Coq.PArith.Pnat]
SuccNat2Pos.inv [lemma, in Coq.PArith.Pnat]
SuccNat2Pos.pred_id [lemma, in Coq.PArith.Pnat]
succ_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
succ_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
succ_plus_discr [lemma, in Coq.Arith.Plus]
succ_min_distr [definition, in Coq.Arith.Min]
succ_IZR [lemma, in Coq.Reals.RIneq]
succ_max_distr [definition, in Coq.Arith.Max]
sum [inductive, in Coq.Init.Datatypes]
sumbool [inductive, in Coq.Init.Specif]
Sumbool [library]
sumboolP [lemma, in Coq.ssr.ssrbool]
sumbool_not [definition, in Coq.Bool.Sumbool]
sumbool_or [definition, in Coq.Bool.Sumbool]
sumbool_and [definition, in Coq.Bool.Sumbool]
sumbool_of_bool [definition, in Coq.Bool.Sumbool]
sumor [inductive, in Coq.Init.Specif]
sum_plus [lemma, in Coq.Reals.Cauchy_prod]
sum_N_predN [lemma, in Coq.Reals.Cauchy_prod]
sum_f_R0_triangle [lemma, in Coq.Reals.Rfunctions]
sum_f [definition, in Coq.Reals.Rfunctions]
sum_f_R0 [definition, in Coq.Reals.Rfunctions]
sum_nat [definition, in Coq.Reals.Rfunctions]
sum_nat_O [definition, in Coq.Reals.Rfunctions]
sum_nat_f [definition, in Coq.Reals.Rfunctions]
sum_nat_f_O [definition, in Coq.Reals.Rfunctions]
sum_maj1 [lemma, in Coq.Reals.SeqSeries]
sum_eqdec [instance, in Coq.Classes.EquivDec]
sum_Ratan_seq_opp [lemma, in Coq.Reals.Ratan]
sum_inequa_Rle_lt [lemma, in Coq.Reals.RIneq]
sum_cv_maj [lemma, in Coq.Reals.PartSum]
sum_incr [lemma, in Coq.Reals.PartSum]
sum_eq_R0 [lemma, in Coq.Reals.PartSum]
sum_growing [lemma, in Coq.Reals.PartSum]
sum_cte [lemma, in Coq.Reals.PartSum]
sum_Rle [lemma, in Coq.Reals.PartSum]
sum_decomposition [lemma, in Coq.Reals.PartSum]
sum_eq [lemma, in Coq.Reals.PartSum]
sum_plus [lemma, in Coq.Reals.Abstract.ConstructiveSum]
sum_scale [lemma, in Coq.Reals.Abstract.ConstructiveSum]
sum_opp [lemma, in Coq.Reals.Abstract.ConstructiveSum]
sum_Rle [lemma, in Coq.Reals.Abstract.ConstructiveSum]
sum_assoc [lemma, in Coq.Reals.Abstract.ConstructiveSum]
sum_const [lemma, in Coq.Reals.Abstract.ConstructiveSum]
sum_eq_R0 [lemma, in Coq.Reals.Abstract.ConstructiveSum]
sUnit [inductive, in Coq.Logic.StrictProp]
sUnit_ind [definition, in Coq.Logic.StrictProp]
sUnit_rec [definition, in Coq.Logic.StrictProp]
sUnit_rect [definition, in Coq.Logic.StrictProp]
sup [constructor, in Coq.Wellfounded.Well_Ordering]
Surjective [definition, in Coq.Logic.FinFun]
surjective_pairing [lemma, in Coq.Init.Datatypes]
Surjective_inverse [lemma, in Coq.Logic.FinFun]
Surjective_carac [lemma, in Coq.Logic.FinFun]
Surjective_list_carac [lemma, in Coq.Logic.FinFun]
sval [abbreviation, in Coq.ssr.ssrfun]
svalP [lemma, in Coq.ssr.ssrfun]
Swap [section, in Coq.Wellfounded.Lexicographic_Product]
Swap [section, in Coq.Relations.Relation_Operators]
SwapProd [abbreviation, in Coq.Wellfounded.Lexicographic_Product]
swapprod [inductive, in Coq.Relations.Relation_Operators]
swap_Acc [lemma, in Coq.Wellfounded.Lexicographic_Product]
swap_sumbool [definition, in Coq.Classes.EquivDec]
swap_sumbool [definition, in Coq.Classes.SetoidDec]
Swap.A [variable, in Coq.Wellfounded.Lexicographic_Product]
Swap.A [variable, in Coq.Relations.Relation_Operators]
Swap.R [variable, in Coq.Wellfounded.Lexicographic_Product]
Swap.R [variable, in Coq.Relations.Relation_Operators]
SWithLeibniz [module, in Coq.MSets.MSetList]
SWithLeibniz.E [module, in Coq.MSets.MSetList]
SWithLeibniz.eq_leibniz [axiom, in Coq.MSets.MSetList]
sx:53 [binder, in Coq.Floats.SpecFloat]
sx:60 [binder, in Coq.Floats.SpecFloat]
symb:40 [binder, in Coq.Classes.CEquivalence]
symb:40 [binder, in Coq.Classes.Equivalence]
Symmetric [record, in Coq.Classes.RelationClasses]
Symmetric [inductive, in Coq.Classes.RelationClasses]
symmetric [definition, in Coq.ssr.ssrbool]
Symmetric [record, in Coq.Classes.CRelationClasses]
Symmetric [inductive, in Coq.Classes.CRelationClasses]
Symmetric [definition, in Coq.Sets.Relations_1]
symmetric [definition, in Coq.Relations.Relation_Definitions]
symmetric_equiv_flip [lemma, in Coq.Classes.Morphisms]
symmetric_from_pre [lemma, in Coq.ssr.ssrbool]
symmetric_equiv_flip [lemma, in Coq.Classes.CMorphisms]
Symmetric_Product.leB [variable, in Coq.Relations.Relation_Operators]
Symmetric_Product.leA [variable, in Coq.Relations.Relation_Operators]
Symmetric_Product.B [variable, in Coq.Relations.Relation_Operators]
Symmetric_Product.A [variable, in Coq.Relations.Relation_Operators]
Symmetric_Product [section, in Coq.Relations.Relation_Operators]
symmetry [projection, in Coq.Classes.RelationClasses]
symmetry [constructor, in Coq.Classes.RelationClasses]
symmetry [projection, in Coq.Classes.CRelationClasses]
symmetry [constructor, in Coq.Classes.CRelationClasses]
Symprod [abbreviation, in Coq.Wellfounded.Lexicographic_Product]
symprod [inductive, in Coq.Relations.Relation_Operators]
sym_EqSt [lemma, in Coq.Lists.Streams]
sym_JMeq [abbreviation, in Coq.Logic.JMeq]
sym_right_transitive [lemma, in Coq.ssr.ssrbool]
sym_left_transitive [lemma, in Coq.ssr.ssrbool]
sym_not_id [abbreviation, in Coq.Init.Logic_Type]
sym_id [abbreviation, in Coq.Init.Logic_Type]
sym_not_equal [abbreviation, in Coq.Init.Logic]
sym_equal [abbreviation, in Coq.Init.Logic]
sym_not_eq [abbreviation, in Coq.Init.Logic]
sym_eq [abbreviation, in Coq.Init.Logic]
SYM1 [abbreviation, in Coq.ZArith.BinInt]
SYM2 [abbreviation, in Coq.ZArith.BinInt]
SYM3 [abbreviation, in Coq.ZArith.BinInt]
Syntax [library]
szero:65 [binder, in Coq.Floats.SpecFloat]
S_to_Finite_set [module, in Coq.FSets.FSetToFiniteSet]
S_to_Finite_set [module, in Coq.MSets.MSetToFiniteSet]
S_O_plus_INR [lemma, in Coq.Reals.RIneq]
S_INR [lemma, in Coq.Reals.RIneq]
S_pred_pos [lemma, in Coq.Arith.Lt]
S_pred [lemma, in Coq.Arith.Lt]
s'':149 [binder, in Coq.FSets.FSetPositive]
s'':150 [binder, in Coq.FSets.FSetCompat]
s'':154 [binder, in Coq.FSets.FSetInterface]
s'':158 [binder, in Coq.FSets.FSetInterface]
s'':189 [binder, in Coq.FSets.FSetInterface]
s'':194 [binder, in Coq.FSets.FSetInterface]
s'':199 [binder, in Coq.FSets.FSetInterface]
s'':201 [binder, in Coq.FSets.FSetBridge]
s'':21 [binder, in Coq.FSets.FSetBridge]
s'':213 [binder, in Coq.FSets.FSetBridge]
s'':22 [binder, in Coq.FSets.FSetFacts]
s'':225 [binder, in Coq.FSets.FSetBridge]
s'':231 [binder, in Coq.FSets.FSetPositive]
s'':25 [binder, in Coq.FSets.FSetBridge]
s'':26 [binder, in Coq.FSets.FSetCompat]
s'':29 [binder, in Coq.FSets.FSetBridge]
s'':38 [binder, in Coq.MSets.MSetProperties]
s'':38 [binder, in Coq.FSets.FSetProperties]
s'':43 [binder, in Coq.MSets.MSetProperties]
s'':43 [binder, in Coq.FSets.FSetProperties]
s'':47 [binder, in Coq.MSets.MSetProperties]
s'':47 [binder, in Coq.FSets.FSetProperties]
s':100 [binder, in Coq.MSets.MSetInterface]
s':101 [binder, in Coq.Lists.SetoidList]
s':102 [binder, in Coq.MSets.MSetGenTree]
s':104 [binder, in Coq.FSets.FSetBridge]
s':104 [binder, in Coq.MSets.MSetWeakList]
s':104 [binder, in Coq.FSets.FSetInterface]
s':107 [binder, in Coq.FSets.FSetBridge]
s':108 [binder, in Coq.MSets.MSetWeakList]
s':109 [binder, in Coq.MSets.MSetProperties]
s':109 [binder, in Coq.FSets.FSetProperties]
s':11 [binder, in Coq.FSets.FSetBridge]
s':113 [binder, in Coq.MSets.MSetWeakList]
s':117 [binder, in Coq.MSets.MSetWeakList]
s':118 [binder, in Coq.MSets.MSetInterface]
s':12 [binder, in Coq.FSets.FSetToFiniteSet]
s':12 [binder, in Coq.MSets.MSetToFiniteSet]
s':121 [binder, in Coq.Lists.SetoidList]
s':122 [binder, in Coq.MSets.MSetInterface]
s':122 [binder, in Coq.MSets.MSetWeakList]
s':122 [binder, in Coq.Lists.SetoidList]
s':123 [binder, in Coq.MSets.MSetPositive]
s':126 [binder, in Coq.MSets.MSetInterface]
s':126 [binder, in Coq.MSets.MSetWeakList]
s':126 [binder, in Coq.FSets.FSetInterface]
s':126 [binder, in Coq.FSets.FSetPositive]
s':126 [binder, in Coq.MSets.MSetPositive]
s':1274 [binder, in Coq.FSets.FMapAVL]
s':1276 [binder, in Coq.FSets.FMapAVL]
s':128 [binder, in Coq.FSets.FSetBridge]
s':129 [binder, in Coq.FSets.FSetInterface]
s':129 [binder, in Coq.FSets.FSetPositive]
s':130 [binder, in Coq.FSets.FSetBridge]
s':130 [binder, in Coq.MSets.MSetProperties]
s':130 [binder, in Coq.FSets.FSetProperties]
s':130 [binder, in Coq.Lists.SetoidList]
s':131 [binder, in Coq.MSets.MSetWeakList]
s':131 [binder, in Coq.Lists.SetoidList]
s':132 [binder, in Coq.FSets.FSetBridge]
s':133 [binder, in Coq.FSets.FSetInterface]
s':134 [binder, in Coq.FSets.FSetBridge]
s':135 [binder, in Coq.MSets.MSetWeakList]
s':136 [binder, in Coq.FSets.FSetBridge]
s':137 [binder, in Coq.MSets.MSetList]
s':138 [binder, in Coq.FSets.FSetBridge]
s':14 [binder, in Coq.FSets.FSetToFiniteSet]
s':14 [binder, in Coq.MSets.MSetToFiniteSet]
s':140 [binder, in Coq.Lists.SetoidList]
s':142 [binder, in Coq.MSets.MSetList]
s':144 [binder, in Coq.FSets.FSetBridge]
s':145 [binder, in Coq.FSets.FSetInterface]
s':145 [binder, in Coq.FSets.FSetCompat]
s':146 [binder, in Coq.MSets.MSetList]
s':146 [binder, in Coq.FSets.FSetPositive]
s':148 [binder, in Coq.FSets.FSetPositive]
s':148 [binder, in Coq.MSets.MSetPositive]
s':149 [binder, in Coq.FSets.FSetCompat]
s':150 [binder, in Coq.FSets.FSetInterface]
s':150 [binder, in Coq.MSets.MSetPositive]
s':151 [binder, in Coq.MSets.MSetList]
s':152 [binder, in Coq.MSets.MSetPositive]
s':152 [binder, in Coq.FSets.FSetCompat]
s':153 [binder, in Coq.FSets.FSetInterface]
s':154 [binder, in Coq.MSets.MSetPositive]
s':154 [binder, in Coq.FSets.FSetCompat]
s':1555 [binder, in Coq.FSets.FMapAVL]
s':156 [binder, in Coq.MSets.MSetList]
s':156 [binder, in Coq.FSets.FSetCompat]
s':157 [binder, in Coq.FSets.FSetInterface]
s':159 [binder, in Coq.MSets.MSetProperties]
s':159 [binder, in Coq.FSets.FSetProperties]
s':159 [binder, in Coq.FSets.FSetCompat]
s':16 [binder, in Coq.FSets.FSetCompat]
s':160 [binder, in Coq.MSets.MSetList]
s':161 [binder, in Coq.FSets.FSetInterface]
s':162 [binder, in Coq.MSets.MSetPositive]
s':164 [binder, in Coq.FSets.FSetPositive]
s':165 [binder, in Coq.MSets.MSetList]
s':166 [binder, in Coq.FSets.FSetPositive]
s':167 [binder, in Coq.Lists.SetoidList]
s':168 [binder, in Coq.FSets.FSetPositive]
s':168 [binder, in Coq.MSets.MSetPositive]
s':17 [binder, in Coq.FSets.FSetBridge]
s':17 [binder, in Coq.MSets.MSetEqProperties]
s':17 [binder, in Coq.FSets.FSetEqProperties]
s':170 [binder, in Coq.MSets.MSetList]
s':170 [binder, in Coq.FSets.FSetPositive]
s':170 [binder, in Coq.MSets.MSetPositive]
s':170 [binder, in Coq.Lists.SetoidList]
s':170 [binder, in Coq.FSets.FSetCompat]
s':171 [binder, in Coq.FSets.FSetBridge]
s':172 [binder, in Coq.FSets.FSetPositive]
s':172 [binder, in Coq.MSets.MSetPositive]
s':174 [binder, in Coq.MSets.MSetList]
s':174 [binder, in Coq.FSets.FSetPositive]
s':174 [binder, in Coq.MSets.MSetPositive]
s':175 [binder, in Coq.MSets.MSetProperties]
s':175 [binder, in Coq.FSets.FSetProperties]
s':176 [binder, in Coq.FSets.FSetInterface]
s':176 [binder, in Coq.FSets.FSetPositive]
s':178 [binder, in Coq.MSets.MSetProperties]
s':178 [binder, in Coq.FSets.FSetPositive]
s':178 [binder, in Coq.FSets.FSetProperties]
s':179 [binder, in Coq.MSets.MSetList]
s':18 [binder, in Coq.MSets.MSetList]
s':181 [binder, in Coq.MSets.MSetProperties]
s':181 [binder, in Coq.FSets.FSetProperties]
s':182 [binder, in Coq.Lists.SetoidList]
s':183 [binder, in Coq.FSets.FSetBridge]
s':183 [binder, in Coq.MSets.MSetList]
s':184 [binder, in Coq.FSets.FSetInterface]
s':185 [binder, in Coq.Lists.SetoidList]
s':186 [binder, in Coq.FSets.FSetPositive]
s':188 [binder, in Coq.FSets.FSetInterface]
s':19 [binder, in Coq.MSets.MSetEqProperties]
s':19 [binder, in Coq.FSets.FSetToFiniteSet]
s':19 [binder, in Coq.MSets.MSetWeakList]
s':19 [binder, in Coq.MSets.MSetList]
s':19 [binder, in Coq.FSets.FSetEqProperties]
s':19 [binder, in Coq.MSets.MSetToFiniteSet]
s':192 [binder, in Coq.MSets.MSetInterface]
s':192 [binder, in Coq.FSets.FSetPositive]
s':193 [binder, in Coq.FSets.FSetInterface]
s':194 [binder, in Coq.FSets.FSetPositive]
s':195 [binder, in Coq.MSets.MSetInterface]
s':195 [binder, in Coq.MSets.MSetProperties]
s':195 [binder, in Coq.FSets.FSetProperties]
s':196 [binder, in Coq.FSets.FSetPositive]
s':198 [binder, in Coq.FSets.FSetInterface]
s':198 [binder, in Coq.FSets.FSetPositive]
s':2 [binder, in Coq.FSets.FSetCompat]
s':20 [binder, in Coq.FSets.FSetBridge]
s':200 [binder, in Coq.FSets.FSetBridge]
s':201 [binder, in Coq.FSets.FSetCompat]
s':203 [binder, in Coq.FSets.FSetBridge]
s':203 [binder, in Coq.FSets.FSetInterface]
s':205 [binder, in Coq.MSets.MSetProperties]
s':205 [binder, in Coq.FSets.FSetProperties]
s':205 [binder, in Coq.FSets.FSetCompat]
s':206 [binder, in Coq.FSets.FSetBridge]
s':206 [binder, in Coq.FSets.FSetInterface]
s':207 [binder, in Coq.FSets.FSetCompat]
s':208 [binder, in Coq.MSets.MSetProperties]
s':208 [binder, in Coq.FSets.FSetProperties]
s':209 [binder, in Coq.FSets.FSetBridge]
s':21 [binder, in Coq.MSets.MSetWeakList]
s':21 [binder, in Coq.FSets.FSetFacts]
s':210 [binder, in Coq.MSets.MSetProperties]
s':210 [binder, in Coq.FSets.FSetProperties]
s':211 [binder, in Coq.MSets.MSetList]
s':212 [binder, in Coq.FSets.FSetBridge]
s':212 [binder, in Coq.FSets.FSetInterface]
s':213 [binder, in Coq.MSets.MSetInterface]
s':213 [binder, in Coq.MSets.MSetProperties]
s':213 [binder, in Coq.FSets.FSetProperties]
s':214 [binder, in Coq.MSets.MSetPositive]
s':215 [binder, in Coq.MSets.MSetInterface]
s':215 [binder, in Coq.FSets.FSetBridge]
s':215 [binder, in Coq.MSets.MSetProperties]
s':215 [binder, in Coq.FSets.FSetProperties]
s':217 [binder, in Coq.MSets.MSetInterface]
s':217 [binder, in Coq.MSets.MSetPositive]
s':218 [binder, in Coq.FSets.FSetBridge]
s':218 [binder, in Coq.MSets.MSetProperties]
s':218 [binder, in Coq.FSets.FSetProperties]
s':219 [binder, in Coq.MSets.MSetInterface]
s':220 [binder, in Coq.MSets.MSetProperties]
s':220 [binder, in Coq.MSets.MSetPositive]
s':220 [binder, in Coq.FSets.FSetProperties]
s':221 [binder, in Coq.MSets.MSetInterface]
s':221 [binder, in Coq.FSets.FSetBridge]
s':222 [binder, in Coq.MSets.MSetProperties]
s':222 [binder, in Coq.FSets.FSetProperties]
s':224 [binder, in Coq.FSets.FSetBridge]
s':227 [binder, in Coq.FSets.FSetBridge]
s':23 [binder, in Coq.FSets.FSetCompat]
s':230 [binder, in Coq.FSets.FSetBridge]
s':230 [binder, in Coq.FSets.FSetPositive]
s':233 [binder, in Coq.FSets.FSetBridge]
s':233 [binder, in Coq.FSets.FSetPositive]
s':239 [binder, in Coq.MSets.MSetInterface]
s':24 [binder, in Coq.FSets.FSetBridge]
s':25 [binder, in Coq.MSets.MSetWeakList]
s':25 [binder, in Coq.MSets.MSetList]
s':25 [binder, in Coq.FSets.FSetFacts]
s':25 [binder, in Coq.FSets.FSetCompat]
s':250 [binder, in Coq.MSets.MSetProperties]
s':250 [binder, in Coq.FSets.FSetProperties]
s':256 [binder, in Coq.FSets.FSetBridge]
s':259 [binder, in Coq.MSets.MSetProperties]
s':259 [binder, in Coq.MSets.MSetGenTree]
s':259 [binder, in Coq.FSets.FSetProperties]
s':26 [binder, in Coq.MSets.MSetInterface]
s':260 [binder, in Coq.MSets.MSetList]
s':262 [binder, in Coq.MSets.MSetProperties]
s':262 [binder, in Coq.MSets.MSetList]
s':262 [binder, in Coq.FSets.FSetProperties]
s':264 [binder, in Coq.FSets.FSetInterface]
s':264 [binder, in Coq.FSets.FSetPositive]
s':266 [binder, in Coq.FSets.FSetPositive]
s':267 [binder, in Coq.MSets.MSetProperties]
s':267 [binder, in Coq.FSets.FSetProperties]
s':269 [binder, in Coq.FSets.FSetPositive]
s':27 [binder, in Coq.MSets.MSetWeakList]
s':27 [binder, in Coq.FSets.FSetInterface]
s':272 [binder, in Coq.MSets.MSetList]
s':272 [binder, in Coq.FSets.FSetPositive]
s':273 [binder, in Coq.MSets.MSetProperties]
s':273 [binder, in Coq.FSets.FSetProperties]
s':274 [binder, in Coq.MSets.MSetInterface]
s':276 [binder, in Coq.FSets.FSetPositive]
s':277 [binder, in Coq.MSets.MSetProperties]
s':277 [binder, in Coq.FSets.FSetProperties]
s':278 [binder, in Coq.MSets.MSetInterface]
s':278 [binder, in Coq.FSets.FSetPositive]
s':28 [binder, in Coq.FSets.FSetBridge]
s':281 [binder, in Coq.FSets.FSetPositive]
s':284 [binder, in Coq.FSets.FSetPositive]
s':285 [binder, in Coq.MSets.MSetProperties]
s':285 [binder, in Coq.FSets.FSetProperties]
s':287 [binder, in Coq.MSets.MSetInterface]
s':288 [binder, in Coq.FSets.FSetPositive]
s':29 [binder, in Coq.MSets.MSetInterface]
s':29 [binder, in Coq.FSets.FSetFacts]
s':290 [binder, in Coq.FSets.FSetPositive]
s':293 [binder, in Coq.FSets.FSetPositive]
s':296 [binder, in Coq.FSets.FSetBridge]
s':296 [binder, in Coq.FSets.FSetPositive]
s':299 [binder, in Coq.MSets.MSetInterface]
s':299 [binder, in Coq.FSets.FSetBridge]
s':299 [binder, in Coq.MSets.MSetProperties]
s':303 [binder, in Coq.FSets.FSetBridge]
s':303 [binder, in Coq.MSets.MSetPositive]
s':303 [binder, in Coq.FSets.FSetProperties]
s':305 [binder, in Coq.MSets.MSetPositive]
s':306 [binder, in Coq.MSets.MSetInterface]
s':307 [binder, in Coq.MSets.MSetProperties]
s':31 [binder, in Coq.MSets.MSetList]
s':310 [binder, in Coq.MSets.MSetInterface]
s':311 [binder, in Coq.FSets.FSetProperties]
s':313 [binder, in Coq.MSets.MSetInterface]
s':32 [binder, in Coq.FSets.FSetBridge]
s':32 [binder, in Coq.FSets.FSetCompat]
s':33 [binder, in Coq.FSets.FSetFacts]
s':332 [binder, in Coq.MSets.MSetInterface]
s':338 [binder, in Coq.MSets.MSetGenTree]
s':34 [binder, in Coq.FSets.FSetBridge]
s':34 [binder, in Coq.FSets.FSetCompat]
s':341 [binder, in Coq.MSets.MSetInterface]
s':345 [binder, in Coq.MSets.MSetInterface]
s':347 [binder, in Coq.MSets.MSetInterface]
s':349 [binder, in Coq.MSets.MSetInterface]
s':35 [binder, in Coq.MSets.MSetFacts]
s':36 [binder, in Coq.MSets.MSetList]
s':36 [binder, in Coq.FSets.FSetCompat]
s':365 [binder, in Coq.FSets.FMapFullAVL]
s':37 [binder, in Coq.MSets.MSetProperties]
s':37 [binder, in Coq.FSets.FSetProperties]
s':38 [binder, in Coq.FSets.FSetCompat]
s':39 [binder, in Coq.MSets.MSetProperties]
s':39 [binder, in Coq.FSets.FSetProperties]
s':390 [binder, in Coq.MSets.MSetRBT]
s':393 [binder, in Coq.FSets.FSetPositive]
s':394 [binder, in Coq.MSets.MSetRBT]
s':395 [binder, in Coq.FSets.FSetPositive]
s':4 [binder, in Coq.FSets.FSetInterface]
s':4 [binder, in Coq.MSets.MSetRBT]
s':40 [binder, in Coq.MSets.MSetList]
s':41 [binder, in Coq.MSets.MSetEqProperties]
s':41 [binder, in Coq.FSets.FSetEqProperties]
s':42 [binder, in Coq.MSets.MSetProperties]
s':42 [binder, in Coq.FSets.FSetProperties]
s':44 [binder, in Coq.MSets.MSetEqProperties]
s':44 [binder, in Coq.FSets.FSetEqProperties]
s':46 [binder, in Coq.MSets.MSetProperties]
s':46 [binder, in Coq.FSets.FSetProperties]
s':5 [binder, in Coq.MSets.MSetProperties]
s':5 [binder, in Coq.FSets.FSetProperties]
s':5 [binder, in Coq.FSets.FSetCompat]
s':57 [binder, in Coq.MSets.MSetProperties]
s':57 [binder, in Coq.FSets.FSetProperties]
s':59 [binder, in Coq.MSets.MSetProperties]
s':59 [binder, in Coq.MSets.MSetWeakList]
s':59 [binder, in Coq.FSets.FSetProperties]
s':6 [binder, in Coq.FSets.FSetToFiniteSet]
s':6 [binder, in Coq.MSets.MSetToFiniteSet]
s':60 [binder, in Coq.FSets.FSetBridge]
s':60 [binder, in Coq.FSets.FSetCompat]
s':61 [binder, in Coq.MSets.MSetEqProperties]
s':61 [binder, in Coq.FSets.FSetEqProperties]
s':62 [binder, in Coq.MSets.MSetWeakList]
s':63 [binder, in Coq.FSets.FSetCompat]
s':64 [binder, in Coq.MSets.MSetEqProperties]
s':64 [binder, in Coq.FSets.FSetEqProperties]
s':66 [binder, in Coq.FSets.FSetCompat]
s':69 [binder, in Coq.FSets.FSetCompat]
s':7 [binder, in Coq.FSets.FSetBridge]
s':7 [binder, in Coq.FSets.FSetInterface]
s':715 [binder, in Coq.MSets.MSetRBT]
s':717 [binder, in Coq.MSets.MSetRBT]
s':719 [binder, in Coq.MSets.MSetRBT]
s':72 [binder, in Coq.FSets.FSetCompat]
s':73 [binder, in Coq.MSets.MSetEqProperties]
s':73 [binder, in Coq.FSets.FSetEqProperties]
s':74 [binder, in Coq.MSets.MSetList]
s':75 [binder, in Coq.FSets.FSetCompat]
s':77 [binder, in Coq.MSets.MSetProperties]
s':77 [binder, in Coq.FSets.FSetProperties]
s':78 [binder, in Coq.FSets.FSetCompat]
s':8 [binder, in Coq.FSets.FSetToFiniteSet]
s':8 [binder, in Coq.MSets.MSetToFiniteSet]
s':81 [binder, in Coq.FSets.FSetCompat]
s':84 [binder, in Coq.FSets.FSetCompat]
s':9 [binder, in Coq.MSets.MSetProperties]
s':9 [binder, in Coq.FSets.FSetProperties]
s':90 [binder, in Coq.PArith.BinPosDef]
s':96 [binder, in Coq.FSets.FSetBridge]
s':96 [binder, in Coq.MSets.MSetList]
s':97 [binder, in Coq.MSets.MSetInterface]
s':98 [binder, in Coq.FSets.FSetDecide]
s':98 [binder, in Coq.MSets.MSetDecide]
s':99 [binder, in Coq.MSets.MSetProperties]
s':99 [binder, in Coq.MSets.MSetList]
s':99 [binder, in Coq.MSets.MSetGenTree]
s':99 [binder, in Coq.FSets.FSetProperties]
S.Annot [variable, in Coq.micromega.Tauto]
S.checker [variable, in Coq.micromega.Tauto]
S.checker_sound [variable, in Coq.micromega.Tauto]
S.CNFAnnot [section, in Coq.micromega.Tauto]
S.CNFAnnot.Abstraction [section, in Coq.micromega.Tauto]
S.CNFAnnot.Abstraction.AF [variable, in Coq.micromega.Tauto]
S.CNFAnnot.Abstraction.needA [variable, in Coq.micromega.Tauto]
S.CNFAnnot.Abstraction.needA_all [variable, in Coq.micromega.Tauto]
S.CNFAnnot.Abstraction.TX [variable, in Coq.micromega.Tauto]
S.D [variable, in Coq.micromega.Env]
S.deduce [variable, in Coq.micromega.Tauto]
S.deduce_prop [variable, in Coq.micromega.Tauto]
S.E [module, in Coq.FSets.FMapInterface]
S.E [module, in Coq.FSets.FSetInterface]
S.Env [variable, in Coq.micromega.Tauto]
S.eval [variable, in Coq.micromega.Tauto]
S.EVAL [section, in Coq.micromega.Tauto]
S.eval' [variable, in Coq.micromega.Tauto]
S.EVAL.ea [variable, in Coq.micromega.Tauto]
S.ex [variable, in Coq.micromega.Tauto]
S.FOLDANNOT [section, in Coq.micromega.Tauto]
S.FOLDANNOT.ACC [variable, in Coq.micromega.Tauto]
S.FOLDANNOT.F [variable, in Coq.micromega.Tauto]
S.MAPX [section, in Coq.micromega.Tauto]
S.MAPX.F [variable, in Coq.micromega.Tauto]
S.negate [variable, in Coq.micromega.Tauto]
S.negate_correct [variable, in Coq.micromega.Tauto]
S.normalise [variable, in Coq.micromega.Tauto]
S.normalise_correct [variable, in Coq.micromega.Tauto]
S.no_middle_eval' [variable, in Coq.micromega.Tauto]
S.Term [variable, in Coq.micromega.Tauto]
S.Term' [variable, in Coq.micromega.Tauto]
S.unsat [variable, in Coq.micromega.Tauto]
S.unsat_prop [variable, in Coq.micromega.Tauto]
S.Witness [variable, in Coq.micromega.Tauto]
s1x:146 [binder, in Coq.MSets.MSetRBT]
s1':322 [binder, in Coq.MSets.MSetInterface]
s1':328 [binder, in Coq.MSets.MSetInterface]
s1':341 [binder, in Coq.MSets.MSetGenTree]
s1:10 [binder, in Coq.Strings.String]
S1:104 [binder, in Coq.micromega.ZifyClasses]
s1:107 [binder, in Coq.FSets.FSetDecide]
s1:107 [binder, in Coq.MSets.MSetDecide]
s1:109 [binder, in Coq.Structures.OrderedTypeEx]
s1:113 [binder, in Coq.Structures.OrderedTypeEx]
s1:116 [binder, in Coq.micromega.ZifyClasses]
s1:116 [binder, in Coq.Reals.RiemannInt_SF]
s1:117 [binder, in Coq.Lists.SetoidList]
s1:118 [binder, in Coq.FSets.FSetDecide]
s1:118 [binder, in Coq.MSets.MSetDecide]
s1:118 [binder, in Coq.Structures.OrderedTypeEx]
s1:121 [binder, in Coq.MSets.MSetRBT]
S1:122 [binder, in Coq.micromega.ZifyClasses]
s1:124 [binder, in Coq.FSets.FSetDecide]
s1:124 [binder, in Coq.MSets.MSetDecide]
s1:126 [binder, in Coq.Lists.SetoidList]
s1:131 [binder, in Coq.micromega.ZifyClasses]
s1:131 [binder, in Coq.MSets.MSetRBT]
s1:134 [binder, in Coq.Reals.RiemannInt_SF]
S1:136 [binder, in Coq.setoid_ring.Ring_polynom]
s1:141 [binder, in Coq.MSets.MSetRBT]
s1:142 [binder, in Coq.micromega.ZifyClasses]
S1:146 [binder, in Coq.micromega.EnvRing]
s1:147 [binder, in Coq.MSets.MSetRBT]
s1:148 [binder, in Coq.micromega.ZifyClasses]
S1:150 [binder, in Coq.micromega.EnvRing]
S1:151 [binder, in Coq.setoid_ring.Ring_polynom]
s1:1514 [binder, in Coq.FSets.FMapAVL]
s1:152 [binder, in Coq.micromega.ZifyClasses]
S1:152 [binder, in Coq.micromega.EnvRing]
s1:1521 [binder, in Coq.FSets.FMapAVL]
S1:154 [binder, in Coq.micromega.EnvRing]
s1:1543 [binder, in Coq.FSets.FMapAVL]
s1:1548 [binder, in Coq.FSets.FMapAVL]
S1:155 [binder, in Coq.setoid_ring.Ring_polynom]
s1:156 [binder, in Coq.micromega.ZifyClasses]
S1:157 [binder, in Coq.setoid_ring.Ring_polynom]
S1:159 [binder, in Coq.setoid_ring.Ring_polynom]
s1:160 [binder, in Coq.micromega.ZifyClasses]
s1:160 [binder, in Coq.Lists.SetoidList]
s1:164 [binder, in Coq.micromega.ZifyClasses]
s1:17 [binder, in Coq.Sets.Uniset]
s1:176 [binder, in Coq.Lists.SetoidList]
s1:19 [binder, in Coq.Strings.String]
s1:20 [binder, in Coq.Sets.Uniset]
S1:21 [binder, in Coq.micromega.ZifyClasses]
s1:230 [binder, in Coq.FSets.FSetInterface]
s1:24 [binder, in Coq.Sets.Uniset]
s1:25 [binder, in Coq.Lists.Streams]
s1:26 [binder, in Coq.Sets.Uniset]
s1:27 [binder, in Coq.FSets.FSetDecide]
s1:27 [binder, in Coq.MSets.MSetDecide]
s1:277 [binder, in Coq.setoid_ring.Field_theory]
s1:283 [binder, in Coq.setoid_ring.Field_theory]
s1:29 [binder, in Coq.FSets.FSetDecide]
s1:29 [binder, in Coq.MSets.MSetDecide]
s1:3 [binder, in Coq.Strings.String]
s1:30 [binder, in Coq.Lists.Streams]
s1:31 [binder, in Coq.Strings.String]
s1:316 [binder, in Coq.MSets.MSetInterface]
s1:32 [binder, in Coq.Lists.Streams]
s1:321 [binder, in Coq.MSets.MSetInterface]
s1:327 [binder, in Coq.MSets.MSetInterface]
s1:333 [binder, in Coq.MSets.MSetGenTree]
s1:339 [binder, in Coq.MSets.MSetGenTree]
s1:34 [binder, in Coq.Strings.String]
s1:34 [binder, in Coq.MSets.MSetAVL]
s1:36 [binder, in Coq.Lists.Streams]
s1:363 [binder, in Coq.MSets.MSetGenTree]
s1:368 [binder, in Coq.MSets.MSetGenTree]
s1:37 [binder, in Coq.Strings.String]
s1:370 [binder, in Coq.MSets.MSetGenTree]
s1:374 [binder, in Coq.MSets.MSetGenTree]
s1:38 [binder, in Coq.Lists.Streams]
s1:44 [binder, in Coq.MSets.MSetWeakList]
s1:44 [binder, in Coq.MSets.MSetAVL]
s1:461 [binder, in Coq.MSets.MSetRBT]
s1:47 [binder, in Coq.FSets.FMapAVL]
s1:488 [binder, in Coq.MSets.MSetRBT]
s1:492 [binder, in Coq.MSets.MSetRBT]
s1:496 [binder, in Coq.MSets.MSetRBT]
s1:5 [binder, in Coq.Strings.String]
s1:504 [binder, in Coq.MSets.MSetRBT]
s1:507 [binder, in Coq.MSets.MSetRBT]
s1:510 [binder, in Coq.MSets.MSetRBT]
s1:513 [binder, in Coq.MSets.MSetRBT]
s1:521 [binder, in Coq.MSets.MSetRBT]
s1:525 [binder, in Coq.MSets.MSetRBT]
s1:533 [binder, in Coq.MSets.MSetRBT]
s1:541 [binder, in Coq.MSets.MSetRBT]
s1:549 [binder, in Coq.MSets.MSetRBT]
s1:553 [binder, in Coq.MSets.MSetAVL]
s1:553 [binder, in Coq.MSets.MSetRBT]
s1:556 [binder, in Coq.MSets.MSetAVL]
s1:556 [binder, in Coq.MSets.MSetRBT]
s1:564 [binder, in Coq.MSets.MSetRBT]
s1:569 [binder, in Coq.MSets.MSetRBT]
s1:57 [binder, in Coq.MSets.MSetGenTree]
s1:570 [binder, in Coq.MSets.MSetAVL]
s1:573 [binder, in Coq.MSets.MSetAVL]
s1:573 [binder, in Coq.MSets.MSetRBT]
s1:59 [binder, in Coq.Strings.String]
s1:604 [binder, in Coq.MSets.MSetAVL]
s1:609 [binder, in Coq.MSets.MSetAVL]
s1:614 [binder, in Coq.MSets.MSetAVL]
s1:618 [binder, in Coq.MSets.MSetAVL]
s1:623 [binder, in Coq.MSets.MSetAVL]
s1:628 [binder, in Coq.MSets.MSetAVL]
s1:632 [binder, in Coq.MSets.MSetAVL]
s1:637 [binder, in Coq.MSets.MSetAVL]
s1:64 [binder, in Coq.Strings.String]
s1:64 [binder, in Coq.MSets.MSetList]
s1:64 [binder, in Coq.MSets.MSetAVL]
s1:64 [binder, in Coq.MSets.MSetGenTree]
s1:66 [binder, in Coq.MSets.MSetGenTree]
s1:67 [binder, in Coq.Strings.String]
s1:67 [binder, in Coq.Sets.Powerset_facts]
s1:696 [binder, in Coq.MSets.MSetRBT]
s1:698 [binder, in Coq.MSets.MSetRBT]
s1:700 [binder, in Coq.MSets.MSetRBT]
s1:702 [binder, in Coq.MSets.MSetRBT]
s1:704 [binder, in Coq.MSets.MSetRBT]
s1:72 [binder, in Coq.MSets.MSetAVL]
s1:75 [binder, in Coq.FSets.FSetBridge]
s1:75 [binder, in Coq.Strings.String]
s1:78 [binder, in Coq.MSets.MSetGenTree]
s1:78 [binder, in Coq.Sets.Powerset_facts]
s1:79 [binder, in Coq.Strings.String]
S1:8 [binder, in Coq.micromega.ZifyClasses]
s1:80 [binder, in Coq.MSets.MSetAVL]
s1:82 [binder, in Coq.Sets.Powerset_facts]
s1:84 [binder, in Coq.Strings.String]
s1:85 [binder, in Coq.FSets.FSetDecide]
s1:85 [binder, in Coq.MSets.MSetDecide]
s1:86 [binder, in Coq.Sets.Powerset_facts]
s1:89 [binder, in Coq.Strings.String]
s1:89 [binder, in Coq.Sets.Powerset_facts]
s1:91 [binder, in Coq.FSets.FSetDecide]
s1:91 [binder, in Coq.MSets.MSetDecide]
s2val [definition, in Coq.ssr.ssrfun]
s2valP [lemma, in Coq.ssr.ssrfun]
s2valP' [lemma, in Coq.ssr.ssrfun]
s2x:149 [binder, in Coq.MSets.MSetRBT]
s2':318 [binder, in Coq.MSets.MSetInterface]
s2':324 [binder, in Coq.MSets.MSetInterface]
s2':330 [binder, in Coq.MSets.MSetInterface]
s2':342 [binder, in Coq.MSets.MSetGenTree]
s2':38 [binder, in Coq.MSets.MSetAVL]
s2':48 [binder, in Coq.MSets.MSetAVL]
S2:105 [binder, in Coq.micromega.ZifyClasses]
s2:108 [binder, in Coq.FSets.FSetDecide]
s2:108 [binder, in Coq.MSets.MSetDecide]
s2:11 [binder, in Coq.Strings.String]
s2:110 [binder, in Coq.Structures.OrderedTypeEx]
s2:114 [binder, in Coq.Structures.OrderedTypeEx]
s2:117 [binder, in Coq.Reals.RiemannInt_SF]
s2:118 [binder, in Coq.Lists.SetoidList]
s2:119 [binder, in Coq.micromega.ZifyClasses]
s2:119 [binder, in Coq.FSets.FSetDecide]
s2:119 [binder, in Coq.MSets.MSetDecide]
s2:119 [binder, in Coq.Structures.OrderedTypeEx]
s2:122 [binder, in Coq.MSets.MSetRBT]
S2:123 [binder, in Coq.micromega.ZifyClasses]
s2:125 [binder, in Coq.FSets.FSetDecide]
s2:125 [binder, in Coq.MSets.MSetDecide]
s2:127 [binder, in Coq.Lists.SetoidList]
s2:132 [binder, in Coq.MSets.MSetRBT]
s2:135 [binder, in Coq.Reals.RiemannInt_SF]
S2:138 [binder, in Coq.setoid_ring.Ring_polynom]
s2:142 [binder, in Coq.MSets.MSetRBT]
s2:145 [binder, in Coq.micromega.ZifyClasses]
S2:148 [binder, in Coq.micromega.EnvRing]
s2:148 [binder, in Coq.MSets.MSetRBT]
s2:149 [binder, in Coq.micromega.ZifyClasses]
s2:1522 [binder, in Coq.FSets.FMapAVL]
s2:153 [binder, in Coq.micromega.ZifyClasses]
S2:153 [binder, in Coq.setoid_ring.Ring_polynom]
s2:1549 [binder, in Coq.FSets.FMapAVL]
s2:157 [binder, in Coq.micromega.ZifyClasses]
s2:161 [binder, in Coq.micromega.ZifyClasses]
s2:161 [binder, in Coq.Lists.SetoidList]
s2:177 [binder, in Coq.Lists.SetoidList]
s2:18 [binder, in Coq.Sets.Uniset]
s2:20 [binder, in Coq.Strings.String]
s2:21 [binder, in Coq.Sets.Uniset]
S2:22 [binder, in Coq.micromega.ZifyClasses]
s2:231 [binder, in Coq.FSets.FSetInterface]
s2:25 [binder, in Coq.Sets.Uniset]
s2:26 [binder, in Coq.Lists.Streams]
s2:27 [binder, in Coq.Sets.Uniset]
s2:278 [binder, in Coq.setoid_ring.Field_theory]
s2:28 [binder, in Coq.FSets.FSetDecide]
s2:28 [binder, in Coq.MSets.MSetDecide]
s2:284 [binder, in Coq.setoid_ring.Field_theory]
s2:30 [binder, in Coq.FSets.FSetDecide]
s2:30 [binder, in Coq.MSets.MSetDecide]
s2:31 [binder, in Coq.Lists.Streams]
s2:317 [binder, in Coq.MSets.MSetInterface]
s2:32 [binder, in Coq.Strings.String]
s2:322 [binder, in Coq.MSets.MSetGenTree]
s2:323 [binder, in Coq.MSets.MSetInterface]
s2:329 [binder, in Coq.MSets.MSetInterface]
s2:33 [binder, in Coq.Lists.Streams]
s2:331 [binder, in Coq.MSets.MSetGenTree]
s2:334 [binder, in Coq.MSets.MSetGenTree]
s2:340 [binder, in Coq.MSets.MSetGenTree]
s2:35 [binder, in Coq.Strings.String]
s2:35 [binder, in Coq.MSets.MSetAVL]
s2:369 [binder, in Coq.MSets.MSetGenTree]
s2:37 [binder, in Coq.Lists.Streams]
s2:371 [binder, in Coq.MSets.MSetGenTree]
s2:375 [binder, in Coq.MSets.MSetGenTree]
s2:38 [binder, in Coq.Strings.String]
s2:39 [binder, in Coq.Lists.Streams]
s2:4 [binder, in Coq.Strings.String]
s2:45 [binder, in Coq.MSets.MSetWeakList]
s2:45 [binder, in Coq.MSets.MSetAVL]
s2:462 [binder, in Coq.MSets.MSetRBT]
s2:48 [binder, in Coq.FSets.FMapAVL]
s2:489 [binder, in Coq.MSets.MSetRBT]
s2:493 [binder, in Coq.MSets.MSetRBT]
s2:497 [binder, in Coq.MSets.MSetRBT]
s2:505 [binder, in Coq.MSets.MSetRBT]
s2:508 [binder, in Coq.MSets.MSetRBT]
s2:511 [binder, in Coq.MSets.MSetRBT]
s2:514 [binder, in Coq.MSets.MSetRBT]
s2:522 [binder, in Coq.MSets.MSetRBT]
s2:526 [binder, in Coq.MSets.MSetRBT]
s2:534 [binder, in Coq.MSets.MSetRBT]
s2:542 [binder, in Coq.MSets.MSetRBT]
s2:550 [binder, in Coq.MSets.MSetRBT]
s2:554 [binder, in Coq.MSets.MSetAVL]
s2:554 [binder, in Coq.MSets.MSetRBT]
s2:557 [binder, in Coq.MSets.MSetAVL]
s2:557 [binder, in Coq.MSets.MSetRBT]
s2:565 [binder, in Coq.MSets.MSetRBT]
s2:570 [binder, in Coq.MSets.MSetRBT]
s2:571 [binder, in Coq.MSets.MSetAVL]
s2:574 [binder, in Coq.MSets.MSetAVL]
s2:574 [binder, in Coq.MSets.MSetRBT]
s2:6 [binder, in Coq.Strings.String]
s2:60 [binder, in Coq.Strings.String]
s2:605 [binder, in Coq.MSets.MSetAVL]
s2:610 [binder, in Coq.MSets.MSetAVL]
s2:615 [binder, in Coq.MSets.MSetAVL]
s2:619 [binder, in Coq.MSets.MSetAVL]
s2:624 [binder, in Coq.MSets.MSetAVL]
s2:629 [binder, in Coq.MSets.MSetAVL]
s2:633 [binder, in Coq.MSets.MSetAVL]
s2:638 [binder, in Coq.MSets.MSetAVL]
s2:65 [binder, in Coq.Strings.String]
s2:65 [binder, in Coq.MSets.MSetList]
s2:65 [binder, in Coq.MSets.MSetAVL]
s2:65 [binder, in Coq.MSets.MSetGenTree]
s2:67 [binder, in Coq.MSets.MSetGenTree]
s2:68 [binder, in Coq.Strings.String]
s2:68 [binder, in Coq.Sets.Powerset_facts]
s2:697 [binder, in Coq.MSets.MSetRBT]
s2:699 [binder, in Coq.MSets.MSetRBT]
s2:70 [binder, in Coq.MSets.MSetGenTree]
s2:701 [binder, in Coq.MSets.MSetRBT]
s2:703 [binder, in Coq.MSets.MSetRBT]
s2:705 [binder, in Coq.MSets.MSetRBT]
s2:73 [binder, in Coq.MSets.MSetAVL]
s2:75 [binder, in Coq.MSets.MSetGenTree]
s2:76 [binder, in Coq.FSets.FSetBridge]
s2:76 [binder, in Coq.Strings.String]
s2:79 [binder, in Coq.MSets.MSetGenTree]
s2:79 [binder, in Coq.Sets.Powerset_facts]
s2:80 [binder, in Coq.Strings.String]
s2:81 [binder, in Coq.MSets.MSetAVL]
s2:83 [binder, in Coq.Sets.Powerset_facts]
s2:85 [binder, in Coq.Strings.String]
s2:86 [binder, in Coq.FSets.FSetDecide]
s2:86 [binder, in Coq.MSets.MSetDecide]
s2:87 [binder, in Coq.Sets.Powerset_facts]
S2:9 [binder, in Coq.micromega.ZifyClasses]
s2:90 [binder, in Coq.Strings.String]
s2:90 [binder, in Coq.Sets.Powerset_facts]
s2:92 [binder, in Coq.FSets.FSetDecide]
s2:92 [binder, in Coq.MSets.MSetDecide]
S3:10 [binder, in Coq.micromega.ZifyClasses]
S3:106 [binder, in Coq.micromega.ZifyClasses]
s3:109 [binder, in Coq.FSets.FSetDecide]
s3:109 [binder, in Coq.MSets.MSetDecide]
s3:121 [binder, in Coq.Reals.RiemannInt_SF]
s3:139 [binder, in Coq.Reals.RiemannInt_SF]
s3:34 [binder, in Coq.Lists.Streams]
s3:80 [binder, in Coq.Sets.Powerset_facts]
s3:84 [binder, in Coq.Sets.Powerset_facts]
s3:87 [binder, in Coq.FSets.FSetDecide]
s3:87 [binder, in Coq.MSets.MSetDecide]
s3:93 [binder, in Coq.FSets.FSetDecide]
s3:93 [binder, in Coq.MSets.MSetDecide]
s4:110 [binder, in Coq.FSets.FSetDecide]
s4:110 [binder, in Coq.MSets.MSetDecide]
s4:88 [binder, in Coq.FSets.FSetDecide]
s4:88 [binder, in Coq.MSets.MSetDecide]
s4:94 [binder, in Coq.FSets.FSetDecide]
s4:94 [binder, in Coq.MSets.MSetDecide]
S754_finite [constructor, in Coq.Floats.SpecFloat]
S754_nan [constructor, in Coq.Floats.SpecFloat]
S754_infinity [constructor, in Coq.Floats.SpecFloat]
S754_zero [constructor, in Coq.Floats.SpecFloat]
s:1 [binder, in Coq.FSets.FSetBridge]
S:1 [binder, in Coq.micromega.ZifyClasses]
s:1 [binder, in Coq.FSets.FSetToFiniteSet]
s:1 [binder, in Coq.MSets.MSetAVL]
s:1 [binder, in Coq.MSets.MSetToFiniteSet]
s:1 [binder, in Coq.FSets.FSetCompat]
s:10 [binder, in Coq.Lists.Streams]
s:10 [binder, in Coq.Strings.OctalString]
s:10 [binder, in Coq.FSets.FSetBridge]
s:10 [binder, in Coq.Strings.HexString]
s:10 [binder, in Coq.Strings.BinaryString]
s:10 [binder, in Coq.FSets.FMapWeakList]
s:10 [binder, in Coq.FSets.FMapList]
s:10 [binder, in Coq.FSets.FSetCompat]
s:100 [binder, in Coq.FSets.FSetBridge]
s:100 [binder, in Coq.Strings.String]
S:100 [binder, in Coq.rtauto.Bintree]
s:100 [binder, in Coq.Lists.SetoidList]
s:100 [binder, in Coq.FSets.FSetCompat]
s:101 [binder, in Coq.MSets.MSetProperties]
s:101 [binder, in Coq.Strings.String]
s:101 [binder, in Coq.MSets.MSetList]
s:101 [binder, in Coq.MSets.MSetRBT]
s:101 [binder, in Coq.FSets.FMapWeakList]
s:101 [binder, in Coq.MSets.MSetGenTree]
s:101 [binder, in Coq.FSets.FSetProperties]
s:102 [binder, in Coq.MSets.MSetInterface]
s:102 [binder, in Coq.FSets.FSetDecide]
s:102 [binder, in Coq.MSets.MSetEqProperties]
s:102 [binder, in Coq.MSets.MSetProperties]
s:102 [binder, in Coq.Strings.String]
s:102 [binder, in Coq.MSets.MSetDecide]
s:102 [binder, in Coq.FSets.FSetEqProperties]
s:102 [binder, in Coq.FSets.FMapList]
s:102 [binder, in Coq.FSets.FSetProperties]
s:103 [binder, in Coq.FSets.FSetBridge]
s:103 [binder, in Coq.MSets.MSetProperties]
s:103 [binder, in Coq.MSets.MSetWeakList]
s:103 [binder, in Coq.FSets.FSetInterface]
s:103 [binder, in Coq.MSets.MSetRBT]
s:103 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:103 [binder, in Coq.FSets.FSetProperties]
s:103 [binder, in Coq.FSets.FSetCompat]
s:104 [binder, in Coq.MSets.MSetList]
s:104 [binder, in Coq.FSets.FMapWeakList]
s:104 [binder, in Coq.MSets.MSetGenTree]
s:105 [binder, in Coq.MSets.MSetInterface]
s:105 [binder, in Coq.MSets.MSetProperties]
s:105 [binder, in Coq.FSets.FSetProperties]
s:106 [binder, in Coq.FSets.FSetBridge]
s:106 [binder, in Coq.FSets.FSetCompat]
s:107 [binder, in Coq.MSets.MSetProperties]
s:107 [binder, in Coq.MSets.MSetWeakList]
s:107 [binder, in Coq.MSets.MSetList]
s:107 [binder, in Coq.Structures.OrderedTypeEx]
s:107 [binder, in Coq.MSets.MSetGenTree]
s:107 [binder, in Coq.FSets.FMapList]
s:107 [binder, in Coq.FSets.FSetProperties]
s:108 [binder, in Coq.MSets.MSetInterface]
s:108 [binder, in Coq.MSets.MSetProperties]
s:108 [binder, in Coq.FSets.FMapWeakList]
s:108 [binder, in Coq.FSets.FSetProperties]
s:109 [binder, in Coq.FSets.FSetBridge]
s:109 [binder, in Coq.MSets.MSetList]
s:109 [binder, in Coq.FSets.FSetCompat]
s:11 [binder, in Coq.Numbers.DecimalString]
s:11 [binder, in Coq.FSets.FSetToFiniteSet]
s:11 [binder, in Coq.Numbers.HexadecimalString]
s:11 [binder, in Coq.MSets.MSetToFiniteSet]
s:110 [binder, in Coq.MSets.MSetInterface]
s:110 [binder, in Coq.MSets.MSetProperties]
s:110 [binder, in Coq.MSets.MSetGenTree]
s:110 [binder, in Coq.FSets.FMapList]
s:110 [binder, in Coq.FSets.FSetProperties]
s:111 [binder, in Coq.MSets.MSetProperties]
s:111 [binder, in Coq.MSets.MSetRBT]
s:111 [binder, in Coq.FSets.FSetProperties]
s:112 [binder, in Coq.FSets.FSetBridge]
s:112 [binder, in Coq.MSets.MSetProperties]
s:112 [binder, in Coq.MSets.MSetWeakList]
s:112 [binder, in Coq.MSets.MSetList]
s:112 [binder, in Coq.FSets.FMapWeakList]
s:112 [binder, in Coq.FSets.FSetProperties]
s:112 [binder, in Coq.FSets.FSetCompat]
s:113 [binder, in Coq.MSets.MSetInterface]
s:113 [binder, in Coq.MSets.MSetProperties]
s:113 [binder, in Coq.MSets.MSetGenTree]
s:113 [binder, in Coq.FSets.FSetProperties]
S:114 [binder, in Coq.rtauto.Bintree]
s:114 [binder, in Coq.FSets.FMapList]
s:115 [binder, in Coq.FSets.FSetBridge]
s:115 [binder, in Coq.FSets.FSetDecide]
s:115 [binder, in Coq.MSets.MSetProperties]
s:115 [binder, in Coq.ZArith.BinInt]
s:115 [binder, in Coq.Floats.SpecFloat]
s:115 [binder, in Coq.MSets.MSetDecide]
s:115 [binder, in Coq.MSets.MSetList]
s:115 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:115 [binder, in Coq.FSets.FSetProperties]
s:115 [binder, in Coq.FSets.FSetCompat]
s:116 [binder, in Coq.MSets.MSetWeakList]
S:116 [binder, in Coq.rtauto.Bintree]
s:116 [binder, in Coq.MSets.MSetGenTree]
s:117 [binder, in Coq.MSets.MSetInterface]
s:117 [binder, in Coq.FSets.FSetBridge]
s:117 [binder, in Coq.MSets.MSetEqProperties]
s:117 [binder, in Coq.MSets.MSetProperties]
s:117 [binder, in Coq.FSets.FSetEqProperties]
s:117 [binder, in Coq.FSets.FSetProperties]
s:118 [binder, in Coq.FSets.FSetBridge]
s:118 [binder, in Coq.ZArith.BinInt]
s:118 [binder, in Coq.MSets.MSetList]
S:118 [binder, in Coq.rtauto.Bintree]
s:118 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
s:118 [binder, in Coq.FSets.FMapList]
s:118 [binder, in Coq.FSets.FSetCompat]
s:1181 [binder, in Coq.FSets.FMapAVL]
s:1185 [binder, in Coq.FSets.FMapAVL]
s:1188 [binder, in Coq.FSets.FMapAVL]
s:119 [binder, in Coq.FSets.FSetBridge]
S:119 [binder, in Coq.rtauto.Bintree]
s:1190 [binder, in Coq.FSets.FMapAVL]
s:1195 [binder, in Coq.FSets.FMapAVL]
s:1196 [binder, in Coq.FSets.FMapAVL]
s:12 [binder, in Coq.MSets.MSetWeakList]
s:12 [binder, in Coq.MSets.MSetList]
s:12 [binder, in Coq.FSets.FSetInterface]
s:12 [binder, in Coq.Setoids.Setoid]
s:120 [binder, in Coq.FSets.FSetBridge]
s:120 [binder, in Coq.Lists.SetoidList]
s:120 [binder, in Coq.FSets.FSetCompat]
s:1202 [binder, in Coq.FSets.FMapAVL]
s:121 [binder, in Coq.MSets.MSetInterface]
s:121 [binder, in Coq.MSets.MSetWeakList]
s:1212 [binder, in Coq.FSets.FMapAVL]
s:1214 [binder, in Coq.FSets.FMapAVL]
s:1219 [binder, in Coq.FSets.FMapAVL]
s:122 [binder, in Coq.FSets.FSetBridge]
s:122 [binder, in Coq.MSets.MSetList]
s:122 [binder, in Coq.MSets.MSetPositive]
s:1222 [binder, in Coq.FSets.FMapAVL]
s:123 [binder, in Coq.FSets.FSetBridge]
s:123 [binder, in Coq.MSets.MSetProperties]
s:123 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
s:123 [binder, in Coq.FSets.FSetProperties]
s:123 [binder, in Coq.Lists.SetoidList]
s:123 [binder, in Coq.FSets.FSetCompat]
s:1238 [binder, in Coq.FSets.FMapAVL]
s:124 [binder, in Coq.MSets.MSetGenTree]
s:125 [binder, in Coq.MSets.MSetInterface]
s:125 [binder, in Coq.FSets.FSetBridge]
s:125 [binder, in Coq.MSets.MSetWeakList]
s:125 [binder, in Coq.FSets.FSetInterface]
s:125 [binder, in Coq.FSets.FSetPositive]
s:125 [binder, in Coq.MSets.MSetPositive]
s:125 [binder, in Coq.FSets.FSetCompat]
s:126 [binder, in Coq.Floats.SpecFloat]
s:126 [binder, in Coq.MSets.MSetList]
s:126 [binder, in Coq.FSets.FSetCompat]
s:127 [binder, in Coq.FSets.FSetBridge]
s:127 [binder, in Coq.MSets.MSetGenTree]
s:1273 [binder, in Coq.FSets.FMapAVL]
s:1275 [binder, in Coq.FSets.FMapAVL]
s:128 [binder, in Coq.FSets.FSetInterface]
s:128 [binder, in Coq.FSets.FSetPositive]
s:128 [binder, in Coq.MSets.MSetPositive]
s:128 [binder, in Coq.FSets.FSetCompat]
s:129 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
s:129 [binder, in Coq.MSets.MSetInterface]
s:129 [binder, in Coq.FSets.FSetBridge]
s:129 [binder, in Coq.FSets.FSetDecide]
s:129 [binder, in Coq.MSets.MSetEqProperties]
s:129 [binder, in Coq.MSets.MSetProperties]
s:129 [binder, in Coq.MSets.MSetDecide]
s:129 [binder, in Coq.MSets.MSetList]
s:129 [binder, in Coq.FSets.FSetEqProperties]
s:129 [binder, in Coq.FSets.FSetProperties]
s:129 [binder, in Coq.Lists.SetoidList]
s:13 [binder, in Coq.FSets.FSetBridge]
s:13 [binder, in Coq.MSets.MSetEqProperties]
s:13 [binder, in Coq.FSets.FSetToFiniteSet]
s:13 [binder, in Coq.Floats.FloatLemmas]
s:13 [binder, in Coq.FSets.FSetEqProperties]
s:13 [binder, in Coq.MSets.MSetToFiniteSet]
s:13 [binder, in Coq.FSets.FSetCompat]
s:130 [binder, in Coq.MSets.MSetWeakList]
s:130 [binder, in Coq.MSets.MSetGenTree]
s:130 [binder, in Coq.FSets.FSetCompat]
s:131 [binder, in Coq.FSets.FSetBridge]
s:131 [binder, in Coq.FSets.FSetPositive]
s:131 [binder, in Coq.MSets.MSetPositive]
s:131 [binder, in Coq.FSets.FSetCompat]
s:132 [binder, in Coq.MSets.MSetInterface]
s:132 [binder, in Coq.FSets.FSetInterface]
s:132 [binder, in Coq.Lists.SetoidList]
s:133 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
s:133 [binder, in Coq.FSets.FSetBridge]
s:133 [binder, in Coq.FSets.FSetCompat]
S:134 [binder, in Coq.micromega.ZifyClasses]
s:134 [binder, in Coq.MSets.MSetEqProperties]
S:134 [binder, in Coq.setoid_ring.Ring_polynom]
s:134 [binder, in Coq.MSets.MSetWeakList]
s:134 [binder, in Coq.FSets.FSetEqProperties]
s:134 [binder, in Coq.FSets.FSetPositive]
s:134 [binder, in Coq.MSets.MSetPositive]
s:134 [binder, in Coq.MSets.MSetGenTree]
s:135 [binder, in Coq.MSets.MSetInterface]
s:135 [binder, in Coq.FSets.FSetBridge]
s:135 [binder, in Coq.FSets.FSetInterface]
s:136 [binder, in Coq.MSets.MSetList]
s:136 [binder, in Coq.FSets.FSetCompat]
s:137 [binder, in Coq.FSets.FSetBridge]
s:137 [binder, in Coq.MSets.MSetProperties]
s:137 [binder, in Coq.FSets.FSetPositive]
s:137 [binder, in Coq.MSets.MSetGenTree]
s:137 [binder, in Coq.FSets.FSetProperties]
s:137 [binder, in Coq.FSets.FSetCompat]
s:138 [binder, in Coq.MSets.MSetWeakList]
s:138 [binder, in Coq.FSets.FSetInterface]
s:138 [binder, in Coq.MSets.MSetPositive]
s:139 [binder, in Coq.FSets.FSetBridge]
s:139 [binder, in Coq.Lists.SetoidList]
s:139 [binder, in Coq.FSets.FSetCompat]
s:14 [binder, in Coq.Lists.Streams]
s:14 [binder, in Coq.MSets.MSetEqProperties]
s:14 [binder, in Coq.FSets.FSetEqProperties]
s:14 [binder, in Coq.FSets.FMapWeakList]
s:14 [binder, in Coq.FSets.FMapList]
s:140 [binder, in Coq.FSets.FSetBridge]
s:140 [binder, in Coq.MSets.MSetWeakList]
S:141 [binder, in Coq.micromega.EnvRing]
s:141 [binder, in Coq.MSets.MSetWeakList]
s:141 [binder, in Coq.MSets.MSetList]
s:141 [binder, in Coq.FSets.FSetInterface]
s:141 [binder, in Coq.FSets.FSetPositive]
s:141 [binder, in Coq.MSets.MSetGenTree]
s:142 [binder, in Coq.FSets.FSetBridge]
s:142 [binder, in Coq.FSets.FSetCompat]
s:143 [binder, in Coq.FSets.FSetBridge]
S:143 [binder, in Coq.micromega.EnvRing]
s:143 [binder, in Coq.MSets.MSetWeakList]
s:143 [binder, in Coq.MSets.MSetGenTree]
s:143 [binder, in Coq.FSets.FSetCompat]
s:144 [binder, in Coq.FSets.FSetInterface]
s:144 [binder, in Coq.FSets.FSetPositive]
s:144 [binder, in Coq.MSets.MSetGenTree]
s:144 [binder, in Coq.FSets.FSetCompat]
s:145 [binder, in Coq.MSets.MSetList]
s:145 [binder, in Coq.FSets.FSetPositive]
s:145 [binder, in Coq.MSets.MSetPositive]
s:145 [binder, in Coq.MSets.MSetGenTree]
S:146 [binder, in Coq.setoid_ring.Ring_polynom]
s:146 [binder, in Coq.MSets.MSetWeakList]
s:146 [binder, in Coq.MSets.MSetPositive]
s:146 [binder, in Coq.MSets.MSetGenTree]
s:147 [binder, in Coq.FSets.FSetBridge]
s:147 [binder, in Coq.FSets.FSetInterface]
s:147 [binder, in Coq.FSets.FSetPositive]
s:147 [binder, in Coq.MSets.MSetPositive]
s:147 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:148 [binder, in Coq.MSets.MSetProperties]
S:148 [binder, in Coq.setoid_ring.Ring_polynom]
s:148 [binder, in Coq.FSets.FSetProperties]
s:148 [binder, in Coq.FSets.FSetCompat]
s:149 [binder, in Coq.FSets.FSetBridge]
s:149 [binder, in Coq.MSets.MSetWeakList]
s:149 [binder, in Coq.FSets.FSetInterface]
s:149 [binder, in Coq.MSets.MSetPositive]
s:15 [binder, in Coq.FSets.FSetDecide]
s:15 [binder, in Coq.Floats.FloatLemmas]
s:15 [binder, in Coq.MSets.MSetDecide]
s:15 [binder, in Coq.MSets.MSetList]
s:15 [binder, in Coq.FSets.FSetInterface]
s:15 [binder, in Coq.Sets.Uniset]
s:15 [binder, in Coq.Logic.HLevels]
s:15 [binder, in Coq.FSets.FSetCompat]
s:150 [binder, in Coq.MSets.MSetList]
s:150 [binder, in Coq.FSets.FSetPositive]
s:151 [binder, in Coq.FSets.FSetBridge]
s:151 [binder, in Coq.MSets.MSetPositive]
s:151 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
s:151 [binder, in Coq.FSets.FSetCompat]
s:152 [binder, in Coq.MSets.MSetWeakList]
s:152 [binder, in Coq.FSets.FSetInterface]
s:152 [binder, in Coq.FSets.FSetPositive]
s:153 [binder, in Coq.FSets.FSetBridge]
s:153 [binder, in Coq.MSets.MSetPositive]
s:153 [binder, in Coq.FSets.FSetCompat]
s:154 [binder, in Coq.FSets.FSetBridge]
s:155 [binder, in Coq.FSets.FSetBridge]
s:155 [binder, in Coq.MSets.MSetWeakList]
s:155 [binder, in Coq.MSets.MSetList]
s:155 [binder, in Coq.FSets.FSetCompat]
s:1554 [binder, in Coq.FSets.FMapAVL]
s:156 [binder, in Coq.FSets.FSetBridge]
s:156 [binder, in Coq.MSets.MSetProperties]
s:156 [binder, in Coq.FSets.FSetInterface]
s:156 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:156 [binder, in Coq.FSets.FSetProperties]
s:158 [binder, in Coq.FSets.FSetBridge]
s:158 [binder, in Coq.MSets.MSetProperties]
s:158 [binder, in Coq.MSets.MSetWeakList]
s:158 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
s:158 [binder, in Coq.FSets.FSetProperties]
s:158 [binder, in Coq.FSets.FSetCompat]
s:159 [binder, in Coq.MSets.MSetList]
s:159 [binder, in Coq.FSets.FSetPositive]
s:16 [binder, in Coq.FSets.FSetBridge]
s:16 [binder, in Coq.Numbers.DecimalString]
s:16 [binder, in Coq.MSets.MSetEqProperties]
s:16 [binder, in Coq.FSets.FSetToFiniteSet]
s:16 [binder, in Coq.Floats.FloatLemmas]
s:16 [binder, in Coq.ssr.ssreflect]
s:16 [binder, in Coq.FSets.FSetEqProperties]
s:16 [binder, in Coq.Numbers.HexadecimalString]
s:16 [binder, in Coq.MSets.MSetToFiniteSet]
s:16 [binder, in Coq.FSets.FMapWeakList]
s:16 [binder, in Coq.FSets.FMapList]
s:160 [binder, in Coq.MSets.MSetWeakList]
s:160 [binder, in Coq.FSets.FSetInterface]
s:160 [binder, in Coq.FSets.FSetPositive]
s:161 [binder, in Coq.FSets.FSetBridge]
s:161 [binder, in Coq.FSets.FSetPositive]
s:161 [binder, in Coq.MSets.MSetPositive]
s:161 [binder, in Coq.FSets.FSetCompat]
s:162 [binder, in Coq.FSets.FSetBridge]
s:162 [binder, in Coq.MSets.MSetProperties]
s:162 [binder, in Coq.FSets.FSetPositive]
s:162 [binder, in Coq.FSets.FSetProperties]
s:163 [binder, in Coq.FSets.FSetBridge]
s:163 [binder, in Coq.MSets.MSetWeakList]
s:163 [binder, in Coq.FSets.FSetInterface]
s:163 [binder, in Coq.FSets.FSetPositive]
s:163 [binder, in Coq.MSets.MSetRBT]
s:164 [binder, in Coq.MSets.MSetList]
s:164 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:164 [binder, in Coq.FSets.FSetCompat]
s:165 [binder, in Coq.FSets.FSetBridge]
s:165 [binder, in Coq.Reals.Rfunctions]
s:165 [binder, in Coq.MSets.MSetProperties]
s:165 [binder, in Coq.FSets.FSetPositive]
s:165 [binder, in Coq.MSets.MSetRBT]
s:165 [binder, in Coq.FSets.FSetProperties]
s:166 [binder, in Coq.Lists.SetoidList]
s:167 [binder, in Coq.MSets.MSetWeakList]
s:167 [binder, in Coq.FSets.FSetInterface]
s:167 [binder, in Coq.FSets.FSetPositive]
s:167 [binder, in Coq.MSets.MSetRBT]
s:167 [binder, in Coq.MSets.MSetPositive]
s:167 [binder, in Coq.FSets.FSetCompat]
s:168 [binder, in Coq.FSets.FSetBridge]
s:168 [binder, in Coq.MSets.MSetProperties]
s:168 [binder, in Coq.FSets.FSetProperties]
s:169 [binder, in Coq.MSets.MSetList]
s:169 [binder, in Coq.FSets.FSetInterface]
s:169 [binder, in Coq.FSets.FSetPositive]
s:169 [binder, in Coq.MSets.MSetRBT]
s:169 [binder, in Coq.MSets.MSetPositive]
s:169 [binder, in Coq.FSets.FMapWeakList]
s:169 [binder, in Coq.FSets.FSetCompat]
s:17 [binder, in Coq.Floats.FloatLemmas]
s:17 [binder, in Coq.MSets.MSetWeakList]
s:17 [binder, in Coq.MSets.MSetAVL]
s:170 [binder, in Coq.FSets.FSetBridge]
s:170 [binder, in Coq.FSets.FMapList]
s:171 [binder, in Coq.Reals.Rfunctions]
s:171 [binder, in Coq.MSets.MSetProperties]
s:171 [binder, in Coq.MSets.MSetWeakList]
s:171 [binder, in Coq.FSets.FSetPositive]
s:171 [binder, in Coq.MSets.MSetPositive]
s:171 [binder, in Coq.FSets.FSetProperties]
s:171 [binder, in Coq.Lists.SetoidList]
s:172 [binder, in Coq.FSets.FSetBridge]
s:172 [binder, in Coq.FSets.FSetInterface]
s:172 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:173 [binder, in Coq.MSets.MSetList]
s:173 [binder, in Coq.FSets.FSetPositive]
s:173 [binder, in Coq.MSets.MSetPositive]
s:173 [binder, in Coq.FSets.FMapWeakList]
s:174 [binder, in Coq.MSets.MSetProperties]
s:174 [binder, in Coq.MSets.MSetWeakList]
s:174 [binder, in Coq.FSets.FMapList]
s:174 [binder, in Coq.FSets.FSetProperties]
s:175 [binder, in Coq.FSets.FSetBridge]
s:175 [binder, in Coq.FSets.FSetInterface]
s:175 [binder, in Coq.FSets.FSetPositive]
s:175 [binder, in Coq.FSets.FMapWeakList]
s:176 [binder, in Coq.NArith.BinNat]
s:176 [binder, in Coq.FSets.FMapList]
s:177 [binder, in Coq.MSets.MSetProperties]
s:177 [binder, in Coq.FSets.FSetPositive]
s:177 [binder, in Coq.MSets.MSetGenTree]
s:177 [binder, in Coq.FSets.FSetProperties]
s:178 [binder, in Coq.FSets.FSetBridge]
s:178 [binder, in Coq.Reals.Rfunctions]
s:178 [binder, in Coq.MSets.MSetList]
s:178 [binder, in Coq.FSets.FMapWeakList]
s:178 [binder, in Coq.MSets.MSetGenTree]
s:179 [binder, in Coq.FSets.FSetInterface]
s:179 [binder, in Coq.NArith.BinNat]
s:179 [binder, in Coq.FSets.FMapList]
s:179 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:18 [binder, in Coq.Lists.Streams]
s:18 [binder, in Coq.MSets.MSetEqProperties]
s:18 [binder, in Coq.FSets.FSetToFiniteSet]
s:18 [binder, in Coq.MSets.MSetProperties]
s:18 [binder, in Coq.MSets.MSetWeakList]
s:18 [binder, in Coq.FSets.FSetEqProperties]
s:18 [binder, in Coq.MSets.MSetToFiniteSet]
s:18 [binder, in Coq.FSets.FSetProperties]
s:18 [binder, in Coq.FSets.FSetCompat]
s:180 [binder, in Coq.MSets.MSetProperties]
s:180 [binder, in Coq.FSets.FSetProperties]
s:181 [binder, in Coq.FSets.FMapWeakList]
s:181 [binder, in Coq.Lists.SetoidList]
s:182 [binder, in Coq.FSets.FSetBridge]
s:182 [binder, in Coq.MSets.MSetList]
s:182 [binder, in Coq.FSets.FMapList]
s:183 [binder, in Coq.MSets.MSetProperties]
s:183 [binder, in Coq.FSets.FSetInterface]
s:183 [binder, in Coq.FSets.FSetProperties]
s:184 [binder, in Coq.FSets.FSetBridge]
s:184 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:185 [binder, in Coq.FSets.FSetPositive]
s:186 [binder, in Coq.MSets.MSetList]
s:186 [binder, in Coq.Lists.SetoidList]
s:187 [binder, in Coq.FSets.FSetBridge]
s:187 [binder, in Coq.MSets.MSetList]
s:187 [binder, in Coq.FSets.FSetInterface]
s:187 [binder, in Coq.FSets.FSetCompat]
s:188 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:189 [binder, in Coq.MSets.MSetProperties]
s:189 [binder, in Coq.MSets.MSetList]
s:189 [binder, in Coq.FSets.FSetProperties]
s:189 [binder, in Coq.FSets.FSetCompat]
s:19 [binder, in Coq.FSets.FSetBridge]
s:19 [binder, in Coq.Numbers.DecimalString]
s:19 [binder, in Coq.Numbers.HexadecimalString]
s:19 [binder, in Coq.FSets.FMapWeakList]
s:19 [binder, in Coq.FSets.FMapList]
s:19 [binder, in Coq.FSets.FSetFacts]
s:190 [binder, in Coq.MSets.MSetInterface]
s:190 [binder, in Coq.FSets.FSetBridge]
s:190 [binder, in Coq.MSets.MSetProperties]
s:190 [binder, in Coq.FSets.FSetProperties]
s:191 [binder, in Coq.MSets.MSetInterface]
s:191 [binder, in Coq.MSets.MSetList]
s:191 [binder, in Coq.FSets.FSetPositive]
s:192 [binder, in Coq.FSets.FSetInterface]
s:192 [binder, in Coq.FSets.FSetCompat]
s:193 [binder, in Coq.MSets.MSetProperties]
s:193 [binder, in Coq.MSets.MSetList]
s:193 [binder, in Coq.FSets.FSetPositive]
s:193 [binder, in Coq.FSets.FSetProperties]
s:193 [binder, in Coq.FSets.FSetCompat]
s:194 [binder, in Coq.MSets.MSetInterface]
s:194 [binder, in Coq.FSets.FSetBridge]
s:194 [binder, in Coq.MSets.MSetProperties]
s:194 [binder, in Coq.FSets.FSetProperties]
s:195 [binder, in Coq.MSets.MSetList]
s:195 [binder, in Coq.FSets.FSetPositive]
s:195 [binder, in Coq.FSets.FSetCompat]
s:197 [binder, in Coq.MSets.MSetInterface]
s:197 [binder, in Coq.MSets.MSetProperties]
s:197 [binder, in Coq.FSets.FSetInterface]
s:197 [binder, in Coq.FSets.FSetPositive]
s:197 [binder, in Coq.MSets.MSetPositive]
s:197 [binder, in Coq.FSets.FSetProperties]
s:198 [binder, in Coq.MSets.MSetProperties]
s:198 [binder, in Coq.FSets.FSetProperties]
s:198 [binder, in Coq.FSets.FSetCompat]
s:199 [binder, in Coq.FSets.FSetBridge]
s:199 [binder, in Coq.MSets.MSetProperties]
s:199 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
s:199 [binder, in Coq.MSets.MSetList]
s:199 [binder, in Coq.FSets.FSetProperties]
s:199 [binder, in Coq.FSets.FSetCompat]
s:2 [binder, in Coq.FSets.FSetBridge]
s:2 [binder, in Coq.MSets.MSetProperties]
s:2 [binder, in Coq.MSets.MSetRBT]
S:2 [binder, in Coq.Classes.SetoidDec]
s:2 [binder, in Coq.FSets.FSetProperties]
s:20 [binder, in Coq.MSets.MSetWeakList]
s:20 [binder, in Coq.FSets.FSetFacts]
s:200 [binder, in Coq.MSets.MSetInterface]
s:200 [binder, in Coq.MSets.MSetList]
s:200 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:200 [binder, in Coq.FSets.FSetCompat]
s:202 [binder, in Coq.FSets.FSetBridge]
s:202 [binder, in Coq.MSets.MSetProperties]
s:202 [binder, in Coq.MSets.MSetList]
s:202 [binder, in Coq.FSets.FSetInterface]
s:202 [binder, in Coq.FSets.FSetProperties]
s:203 [binder, in Coq.MSets.MSetInterface]
s:204 [binder, in Coq.MSets.MSetProperties]
s:204 [binder, in Coq.FSets.FSetProperties]
s:204 [binder, in Coq.FSets.FSetCompat]
s:205 [binder, in Coq.FSets.FSetBridge]
s:205 [binder, in Coq.FSets.FSetInterface]
s:205 [binder, in Coq.MSets.MSetPositive]
s:205 [binder, in Coq.Lists.SetoidList]
s:206 [binder, in Coq.MSets.MSetInterface]
s:206 [binder, in Coq.MSets.MSetList]
s:206 [binder, in Coq.FSets.FSetCompat]
s:207 [binder, in Coq.MSets.MSetProperties]
s:207 [binder, in Coq.MSets.MSetList]
s:207 [binder, in Coq.FSets.FSetProperties]
s:208 [binder, in Coq.MSets.MSetInterface]
s:208 [binder, in Coq.FSets.FSetBridge]
s:208 [binder, in Coq.MSets.MSetPositive]
s:209 [binder, in Coq.MSets.MSetProperties]
s:209 [binder, in Coq.MSets.MSetList]
s:209 [binder, in Coq.FSets.FSetProperties]
s:21 [binder, in Coq.Lists.Streams]
s:21 [binder, in Coq.FSets.FSetToFiniteSet]
s:21 [binder, in Coq.MSets.MSetToFiniteSet]
s:21 [binder, in Coq.FSets.FSetCompat]
s:210 [binder, in Coq.MSets.MSetInterface]
s:210 [binder, in Coq.MSets.MSetList]
s:211 [binder, in Coq.FSets.FSetBridge]
s:211 [binder, in Coq.FSets.FSetInterface]
s:212 [binder, in Coq.MSets.MSetInterface]
s:212 [binder, in Coq.Reals.Rfunctions]
s:212 [binder, in Coq.MSets.MSetProperties]
s:212 [binder, in Coq.FSets.FSetProperties]
s:213 [binder, in Coq.MSets.MSetPositive]
s:214 [binder, in Coq.MSets.MSetInterface]
s:214 [binder, in Coq.FSets.FSetBridge]
s:214 [binder, in Coq.MSets.MSetProperties]
s:214 [binder, in Coq.MSets.MSetList]
s:214 [binder, in Coq.FSets.FSetProperties]
s:215 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:216 [binder, in Coq.MSets.MSetInterface]
s:216 [binder, in Coq.MSets.MSetPositive]
s:217 [binder, in Coq.FSets.FSetBridge]
s:217 [binder, in Coq.MSets.MSetProperties]
s:217 [binder, in Coq.FSets.FSetProperties]
s:218 [binder, in Coq.MSets.MSetInterface]
s:218 [binder, in Coq.MSets.MSetList]
s:218 [binder, in Coq.FSets.FSetInterface]
s:219 [binder, in Coq.MSets.MSetProperties]
s:219 [binder, in Coq.MSets.MSetPositive]
s:219 [binder, in Coq.FSets.FSetProperties]
s:22 [binder, in Coq.Numbers.DecimalString]
s:22 [binder, in Coq.FSets.FSetToFiniteSet]
s:22 [binder, in Coq.MSets.MSetList]
s:22 [binder, in Coq.ssr.ssreflect]
s:22 [binder, in Coq.Numbers.HexadecimalString]
S:22 [binder, in Coq.Sets.Relations_2_facts]
s:22 [binder, in Coq.MSets.MSetToFiniteSet]
s:22 [binder, in Coq.FSets.FMapWeakList]
s:22 [binder, in Coq.FSets.FMapList]
s:22 [binder, in Coq.FSets.FSetCompat]
s:220 [binder, in Coq.MSets.MSetInterface]
s:220 [binder, in Coq.FSets.FSetBridge]
s:220 [binder, in Coq.MSets.MSetList]
s:221 [binder, in Coq.MSets.MSetProperties]
s:221 [binder, in Coq.FSets.FSetPositive]
s:221 [binder, in Coq.FSets.FSetProperties]
s:222 [binder, in Coq.MSets.MSetInterface]
s:222 [binder, in Coq.MSets.MSetPositive]
s:223 [binder, in Coq.MSets.MSetInterface]
s:223 [binder, in Coq.FSets.FSetBridge]
s:223 [binder, in Coq.MSets.MSetProperties]
s:223 [binder, in Coq.FSets.FSetInterface]
s:223 [binder, in Coq.FSets.FSetProperties]
s:224 [binder, in Coq.MSets.MSetInterface]
s:224 [binder, in Coq.MSets.MSetList]
s:225 [binder, in Coq.MSets.MSetProperties]
s:225 [binder, in Coq.FSets.FSetProperties]
s:226 [binder, in Coq.FSets.FSetBridge]
s:227 [binder, in Coq.MSets.MSetInterface]
s:227 [binder, in Coq.MSets.MSetProperties]
s:227 [binder, in Coq.MSets.MSetList]
s:227 [binder, in Coq.FSets.FSetProperties]
s:228 [binder, in Coq.MSets.MSetInterface]
s:228 [binder, in Coq.FSets.FSetInterface]
s:229 [binder, in Coq.FSets.FSetBridge]
s:229 [binder, in Coq.MSets.MSetProperties]
s:229 [binder, in Coq.FSets.FSetPositive]
s:229 [binder, in Coq.FSets.FSetProperties]
s:23 [binder, in Coq.FSets.FSetBridge]
s:23 [binder, in Coq.FSets.FSetToFiniteSet]
s:23 [binder, in Coq.Strings.String]
s:23 [binder, in Coq.MSets.MSetWeakList]
s:23 [binder, in Coq.MSets.MSetToFiniteSet]
s:23 [binder, in Coq.MSets.MSetGenTree]
s:230 [binder, in Coq.MSets.MSetInterface]
s:230 [binder, in Coq.MSets.MSetList]
s:232 [binder, in Coq.MSets.MSetInterface]
s:232 [binder, in Coq.FSets.FSetBridge]
s:232 [binder, in Coq.FSets.FSetPositive]
s:232 [binder, in Coq.MSets.MSetPositive]
s:233 [binder, in Coq.MSets.MSetList]
s:233 [binder, in Coq.Reals.Abstract.ConstructiveSum]
s:234 [binder, in Coq.MSets.MSetInterface]
s:235 [binder, in Coq.FSets.FSetBridge]
s:235 [binder, in Coq.FSets.FSetInterface]
s:236 [binder, in Coq.MSets.MSetInterface]
s:236 [binder, in Coq.MSets.MSetList]
s:236 [binder, in Coq.FSets.FSetPositive]
s:236 [binder, in Coq.MSets.MSetPositive]
s:237 [binder, in Coq.FSets.FSetBridge]
s:237 [binder, in Coq.FSets.FSetPositive]
s:238 [binder, in Coq.MSets.MSetInterface]
s:238 [binder, in Coq.MSets.MSetProperties]
s:238 [binder, in Coq.FSets.FSetProperties]
s:24 [binder, in Coq.Lists.Streams]
s:24 [binder, in Coq.MSets.MSetWeakList]
s:24 [binder, in Coq.FSets.FSetFacts]
s:24 [binder, in Coq.FSets.FSetCompat]
s:240 [binder, in Coq.MSets.MSetProperties]
s:240 [binder, in Coq.MSets.MSetList]
s:240 [binder, in Coq.FSets.FSetPositive]
s:240 [binder, in Coq.MSets.MSetPositive]
s:240 [binder, in Coq.FSets.FSetProperties]
s:241 [binder, in Coq.FSets.FSetBridge]
s:241 [binder, in Coq.FSets.FSetInterface]
s:241 [binder, in Coq.MSets.MSetPositive]
s:241 [binder, in Coq.MSets.MSetGenTree]
s:243 [binder, in Coq.FSets.FSetBridge]
s:243 [binder, in Coq.FSets.FSetPositive]
s:243 [binder, in Coq.MSets.MSetGenTree]
s:244 [binder, in Coq.MSets.MSetList]
s:244 [binder, in Coq.MSets.MSetPositive]
s:247 [binder, in Coq.MSets.MSetList]
s:247 [binder, in Coq.MSets.MSetGenTree]
s:248 [binder, in Coq.MSets.MSetProperties]
s:248 [binder, in Coq.FSets.FSetInterface]
s:248 [binder, in Coq.FSets.FSetPositive]
s:248 [binder, in Coq.MSets.MSetPositive]
s:248 [binder, in Coq.MSets.MSetGenTree]
s:248 [binder, in Coq.FSets.FSetProperties]
s:249 [binder, in Coq.MSets.MSetProperties]
s:249 [binder, in Coq.FSets.FSetPositive]
s:249 [binder, in Coq.FSets.FSetProperties]
s:25 [binder, in Coq.MSets.MSetInterface]
s:25 [binder, in Coq.Strings.OctalString]
s:25 [binder, in Coq.Strings.HexString]
s:25 [binder, in Coq.FSets.FSetToFiniteSet]
s:25 [binder, in Coq.MSets.MSetProperties]
s:25 [binder, in Coq.Strings.BinaryString]
S:25 [binder, in Coq.Sets.Relations_2_facts]
s:25 [binder, in Coq.MSets.MSetToFiniteSet]
s:25 [binder, in Coq.FSets.FSetProperties]
s:250 [binder, in Coq.MSets.MSetList]
s:250 [binder, in Coq.MSets.MSetGenTree]
s:251 [binder, in Coq.Reals.Abstract.ConstructiveReals]
s:251 [binder, in Coq.MSets.MSetPositive]
s:252 [binder, in Coq.MSets.MSetList]
s:252 [binder, in Coq.FSets.FSetInterface]
s:252 [binder, in Coq.FSets.FSetPositive]
s:253 [binder, in Coq.MSets.MSetProperties]
s:253 [binder, in Coq.FSets.FSetProperties]
s:254 [binder, in Coq.FSets.FSetBridge]
s:254 [binder, in Coq.MSets.MSetGenTree]
s:255 [binder, in Coq.FSets.FSetPositive]
s:255 [binder, in Coq.MSets.MSetPositive]
s:255 [binder, in Coq.MSets.MSetGenTree]
s:256 [binder, in Coq.MSets.MSetProperties]
s:256 [binder, in Coq.FSets.FSetInterface]
s:256 [binder, in Coq.FSets.FSetProperties]
s:257 [binder, in Coq.FSets.FSetBridge]
s:257 [binder, in Coq.MSets.MSetGenTree]
s:258 [binder, in Coq.MSets.MSetProperties]
s:258 [binder, in Coq.MSets.MSetPositive]
s:258 [binder, in Coq.MSets.MSetGenTree]
s:258 [binder, in Coq.FSets.FSetProperties]
s:259 [binder, in Coq.MSets.MSetList]
s:26 [binder, in Coq.FSets.FSetDecide]
s:26 [binder, in Coq.Numbers.DecimalString]
s:26 [binder, in Coq.MSets.MSetProperties]
s:26 [binder, in Coq.MSets.MSetDecide]
s:26 [binder, in Coq.MSets.MSetWeakList]
s:26 [binder, in Coq.FSets.FSetInterface]
s:26 [binder, in Coq.Numbers.HexadecimalString]
s:26 [binder, in Coq.FSets.FSetProperties]
s:260 [binder, in Coq.FSets.FSetBridge]
s:260 [binder, in Coq.FSets.FSetInterface]
s:261 [binder, in Coq.MSets.MSetProperties]
s:261 [binder, in Coq.MSets.MSetList]
s:261 [binder, in Coq.FSets.FSetProperties]
s:262 [binder, in Coq.MSets.MSetPositive]
s:263 [binder, in Coq.FSets.FSetBridge]
s:263 [binder, in Coq.FSets.FSetInterface]
s:263 [binder, in Coq.FSets.FSetPositive]
s:264 [binder, in Coq.MSets.MSetGenTree]
s:265 [binder, in Coq.MSets.MSetProperties]
s:265 [binder, in Coq.FSets.FSetPositive]
s:265 [binder, in Coq.MSets.MSetPositive]
s:265 [binder, in Coq.FSets.FSetProperties]
s:266 [binder, in Coq.MSets.MSetProperties]
s:266 [binder, in Coq.FSets.FSetProperties]
s:267 [binder, in Coq.FSets.FSetBridge]
s:267 [binder, in Coq.MSets.MSetGenTree]
s:268 [binder, in Coq.FSets.FSetPositive]
s:268 [binder, in Coq.MSets.MSetPositive]
s:269 [binder, in Coq.FSets.FSetBridge]
s:269 [binder, in Coq.MSets.MSetProperties]
s:269 [binder, in Coq.MSets.MSetGenTree]
s:269 [binder, in Coq.FSets.FSetProperties]
s:27 [binder, in Coq.Strings.OctalString]
s:27 [binder, in Coq.FSets.FSetBridge]
s:27 [binder, in Coq.Strings.HexString]
s:27 [binder, in Coq.Strings.String]
s:27 [binder, in Coq.Strings.BinaryString]
s:27 [binder, in Coq.MSets.MSetGenTree]
s:27 [binder, in Coq.FSets.FSetCompat]
s:271 [binder, in Coq.MSets.MSetProperties]
s:271 [binder, in Coq.setoid_ring.Field_theory]
s:271 [binder, in Coq.MSets.MSetList]
s:271 [binder, in Coq.FSets.FSetPositive]
s:271 [binder, in Coq.MSets.MSetPositive]
s:271 [binder, in Coq.FSets.FSetProperties]
s:272 [binder, in Coq.FSets.FSetBridge]
s:272 [binder, in Coq.MSets.MSetProperties]
s:272 [binder, in Coq.FSets.FSetProperties]
s:273 [binder, in Coq.MSets.MSetInterface]
s:273 [binder, in Coq.MSets.MSetPositive]
s:274 [binder, in Coq.setoid_ring.Field_theory]
s:274 [binder, in Coq.MSets.MSetGenTree]
s:275 [binder, in Coq.MSets.MSetInterface]
s:275 [binder, in Coq.MSets.MSetProperties]
s:275 [binder, in Coq.FSets.FSetPositive]
s:275 [binder, in Coq.FSets.FSetProperties]
s:276 [binder, in Coq.MSets.MSetInterface]
s:276 [binder, in Coq.FSets.FSetBridge]
s:276 [binder, in Coq.MSets.MSetProperties]
s:276 [binder, in Coq.MSets.MSetPositive]
s:276 [binder, in Coq.MSets.MSetGenTree]
s:276 [binder, in Coq.FSets.FSetProperties]
s:277 [binder, in Coq.MSets.MSetInterface]
s:277 [binder, in Coq.FSets.FSetPositive]
s:278 [binder, in Coq.FSets.FSetBridge]
s:278 [binder, in Coq.MSets.MSetGenTree]
s:28 [binder, in Coq.MSets.MSetInterface]
s:28 [binder, in Coq.Strings.OctalString]
s:28 [binder, in Coq.Strings.HexString]
s:28 [binder, in Coq.MSets.MSetList]
s:28 [binder, in Coq.ssr.ssreflect]
s:28 [binder, in Coq.Strings.BinaryString]
s:28 [binder, in Coq.FSets.FSetFacts]
s:280 [binder, in Coq.FSets.FSetPositive]
s:280 [binder, in Coq.MSets.MSetGenTree]
s:281 [binder, in Coq.FSets.FSetBridge]
s:281 [binder, in Coq.MSets.MSetPositive]
s:281 [binder, in Coq.MSets.MSetGenTree]
s:282 [binder, in Coq.FSets.FMapFacts]
s:282 [binder, in Coq.MSets.MSetGenTree]
s:283 [binder, in Coq.FSets.FSetPositive]
s:283 [binder, in Coq.MSets.MSetGenTree]
s:284 [binder, in Coq.MSets.MSetProperties]
s:284 [binder, in Coq.FSets.FSetProperties]
s:285 [binder, in Coq.FSets.FSetBridge]
s:285 [binder, in Coq.MSets.MSetGenTree]
s:286 [binder, in Coq.MSets.MSetInterface]
s:286 [binder, in Coq.MSets.MSetPositive]
s:287 [binder, in Coq.FSets.FSetPositive]
s:287 [binder, in Coq.MSets.MSetPositive]
s:288 [binder, in Coq.FSets.FSetBridge]
s:289 [binder, in Coq.MSets.MSetInterface]
s:289 [binder, in Coq.FSets.FSetPositive]
s:29 [binder, in Coq.Lists.Streams]
s:29 [binder, in Coq.Program.Wf]
s:29 [binder, in Coq.MSets.MSetWeakList]
s:29 [binder, in Coq.ssr.ssreflect]
s:29 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
s:29 [binder, in Coq.FSets.FSetCompat]
s:290 [binder, in Coq.FSets.FSetBridge]
s:291 [binder, in Coq.MSets.MSetGenTree]
s:292 [binder, in Coq.MSets.MSetInterface]
s:292 [binder, in Coq.FSets.FSetPositive]
s:292 [binder, in Coq.MSets.MSetPositive]
s:295 [binder, in Coq.MSets.MSetInterface]
s:295 [binder, in Coq.FSets.FSetBridge]
s:295 [binder, in Coq.FSets.FSetPositive]
s:297 [binder, in Coq.MSets.MSetPositive]
s:297 [binder, in Coq.MSets.MSetGenTree]
s:298 [binder, in Coq.MSets.MSetInterface]
s:298 [binder, in Coq.FSets.FSetBridge]
s:298 [binder, in Coq.MSets.MSetProperties]
s:298 [binder, in Coq.FSets.FSetPositive]
s:298 [binder, in Coq.MSets.MSetPositive]
s:3 [binder, in Coq.FSets.FSetToFiniteSet]
s:3 [binder, in Coq.Floats.SpecFloat]
s:3 [binder, in Coq.MSets.MSetWeakList]
s:3 [binder, in Coq.MSets.MSetList]
s:3 [binder, in Coq.FSets.FSetInterface]
s:3 [binder, in Coq.MSets.MSetToFiniteSet]
s:3 [binder, in Coq.Setoids.Setoid]
s:30 [binder, in Coq.Numbers.DecimalString]
s:30 [binder, in Coq.Numbers.HexadecimalString]
s:30 [binder, in Coq.MSets.MSetGenTree]
s:300 [binder, in Coq.MSets.MSetPositive]
s:301 [binder, in Coq.MSets.MSetProperties]
s:301 [binder, in Coq.MSets.MSetPositive]
s:302 [binder, in Coq.FSets.FSetBridge]
s:302 [binder, in Coq.MSets.MSetPositive]
s:302 [binder, in Coq.MSets.MSetGenTree]
s:302 [binder, in Coq.FSets.FSetProperties]
s:303 [binder, in Coq.MSets.MSetInterface]
s:303 [binder, in Coq.MSets.MSetGenTree]
s:304 [binder, in Coq.MSets.MSetProperties]
s:304 [binder, in Coq.MSets.MSetPositive]
s:305 [binder, in Coq.MSets.MSetInterface]
s:305 [binder, in Coq.FSets.FSetBridge]
s:305 [binder, in Coq.MSets.MSetRBT]
s:305 [binder, in Coq.FSets.FSetProperties]
s:306 [binder, in Coq.MSets.MSetProperties]
s:306 [binder, in Coq.MSets.MSetGenTree]
s:308 [binder, in Coq.FSets.FSetBridge]
s:308 [binder, in Coq.FSets.FSetPositive]
s:308 [binder, in Coq.MSets.MSetRBT]
s:308 [binder, in Coq.MSets.MSetPositive]
s:308 [binder, in Coq.FSets.FSetProperties]
s:309 [binder, in Coq.MSets.MSetInterface]
s:31 [binder, in Coq.MSets.MSetInterface]
s:31 [binder, in Coq.Strings.OctalString]
s:31 [binder, in Coq.FSets.FSetBridge]
S:31 [binder, in Coq.micromega.ZifyClasses]
s:31 [binder, in Coq.Strings.HexString]
s:31 [binder, in Coq.Strings.BinaryString]
s:31 [binder, in Coq.FSets.FSetCompat]
s:310 [binder, in Coq.MSets.MSetPositive]
s:310 [binder, in Coq.FSets.FSetProperties]
s:311 [binder, in Coq.FSets.FSetBridge]
s:311 [binder, in Coq.MSets.MSetRBT]
s:311 [binder, in Coq.MSets.MSetPositive]
s:311 [binder, in Coq.MSets.MSetGenTree]
s:312 [binder, in Coq.MSets.MSetInterface]
s:312 [binder, in Coq.micromega.RingMicromega]
s:312 [binder, in Coq.FSets.FSetPositive]
s:314 [binder, in Coq.MSets.MSetRBT]
s:314 [binder, in Coq.MSets.MSetPositive]
s:314 [binder, in Coq.MSets.MSetGenTree]
s:316 [binder, in Coq.FSets.FSetPositive]
s:316 [binder, in Coq.MSets.MSetPositive]
s:317 [binder, in Coq.FSets.FSetPositive]
s:317 [binder, in Coq.MSets.MSetPositive]
s:318 [binder, in Coq.MSets.MSetRBT]
s:32 [binder, in Coq.Numbers.DecimalString]
s:32 [binder, in Coq.MSets.MSetEqProperties]
s:32 [binder, in Coq.FSets.FSetEqProperties]
s:32 [binder, in Coq.Numbers.HexadecimalString]
s:32 [binder, in Coq.FSets.FSetFacts]
s:320 [binder, in Coq.FSets.FSetPositive]
s:324 [binder, in Coq.FSets.FSetPositive]
s:325 [binder, in Coq.MSets.MSetGenTree]
s:327 [binder, in Coq.FSets.FSetPositive]
s:33 [binder, in Coq.FSets.FSetBridge]
s:33 [binder, in Coq.FSets.FSetDecide]
s:33 [binder, in Coq.Numbers.DecimalString]
s:33 [binder, in Coq.MSets.MSetDecide]
s:33 [binder, in Coq.MSets.MSetWeakList]
s:33 [binder, in Coq.Numbers.HexadecimalString]
s:33 [binder, in Coq.MSets.MSetGenTree]
s:33 [binder, in Coq.FSets.FSetCompat]
s:330 [binder, in Coq.FSets.FSetPositive]
s:331 [binder, in Coq.MSets.MSetInterface]
s:332 [binder, in Coq.MSets.MSetGenTree]
s:333 [binder, in Coq.FSets.FSetPositive]
s:337 [binder, in Coq.MSets.MSetInterface]
s:337 [binder, in Coq.FSets.FSetPositive]
s:337 [binder, in Coq.MSets.MSetGenTree]
s:34 [binder, in Coq.MSets.MSetInterface]
s:34 [binder, in Coq.MSets.MSetEqProperties]
s:34 [binder, in Coq.MSets.MSetProperties]
s:34 [binder, in Coq.MSets.MSetFacts]
s:34 [binder, in Coq.MSets.MSetList]
s:34 [binder, in Coq.FSets.FSetEqProperties]
s:34 [binder, in Coq.Arith.Mult]
s:34 [binder, in Coq.FSets.FSetProperties]
s:340 [binder, in Coq.MSets.MSetInterface]
s:340 [binder, in Coq.FSets.FSetPositive]
s:343 [binder, in Coq.FSets.FSetPositive]
s:344 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
s:344 [binder, in Coq.MSets.MSetInterface]
s:346 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
s:346 [binder, in Coq.MSets.MSetInterface]
s:347 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
s:347 [binder, in Coq.FSets.FSetPositive]
s:348 [binder, in Coq.MSets.MSetInterface]
s:35 [binder, in Coq.FSets.FSetBridge]
s:35 [binder, in Coq.FSets.FSetCompat]
s:350 [binder, in Coq.FSets.FSetPositive]
s:351 [binder, in Coq.MSets.MSetGenTree]
s:353 [binder, in Coq.FSets.FSetPositive]
s:356 [binder, in Coq.FSets.FSetPositive]
s:359 [binder, in Coq.FSets.FSetPositive]
s:36 [binder, in Coq.MSets.MSetEqProperties]
s:36 [binder, in Coq.Floats.SpecFloat]
s:36 [binder, in Coq.FSets.FSetEqProperties]
s:36 [binder, in Coq.MSets.MSetGenTree]
s:361 [binder, in Coq.FSets.FSetPositive]
s:364 [binder, in Coq.FSets.FMapFullAVL]
s:364 [binder, in Coq.FSets.FSetPositive]
s:369 [binder, in Coq.FSets.FMapFacts]
s:369 [binder, in Coq.FSets.FSetPositive]
s:37 [binder, in Coq.MSets.MSetInterface]
s:37 [binder, in Coq.MSets.MSetWeakList]
s:37 [binder, in Coq.FSets.FSetCompat]
s:370 [binder, in Coq.FSets.FMapFacts]
s:371 [binder, in Coq.FSets.FSetPositive]
s:371 [binder, in Coq.MSets.MSetRBT]
s:375 [binder, in Coq.MSets.MSetRBT]
s:376 [binder, in Coq.FSets.FSetPositive]
s:377 [binder, in Coq.FSets.FSetPositive]
s:378 [binder, in Coq.FSets.FMapFacts]
s:378 [binder, in Coq.MSets.MSetRBT]
s:378 [binder, in Coq.MSets.MSetGenTree]
s:379 [binder, in Coq.FSets.FMapFacts]
s:379 [binder, in Coq.MSets.MSetGenTree]
S:38 [binder, in Coq.micromega.ZifyClasses]
s:38 [binder, in Coq.Numbers.DecimalString]
s:38 [binder, in Coq.MSets.MSetEqProperties]
s:38 [binder, in Coq.FSets.FSetEqProperties]
s:38 [binder, in Coq.Numbers.HexadecimalString]
s:38 [binder, in Coq.MSets.MSetRBT]
s:380 [binder, in Coq.MSets.MSetGenTree]
s:381 [binder, in Coq.MSets.MSetGenTree]
s:382 [binder, in Coq.FSets.FSetPositive]
s:382 [binder, in Coq.MSets.MSetRBT]
s:382 [binder, in Coq.MSets.MSetGenTree]
s:383 [binder, in Coq.PArith.BinPos]
s:387 [binder, in Coq.FSets.FSetPositive]
s:388 [binder, in Coq.FSets.FSetPositive]
s:39 [binder, in Coq.MSets.MSetList]
s:39 [binder, in Coq.FSets.FSetCompat]
s:390 [binder, in Coq.FSets.FSetPositive]
s:391 [binder, in Coq.FSets.FSetPositive]
s:392 [binder, in Coq.FSets.FSetPositive]
s:392 [binder, in Coq.MSets.MSetRBT]
s:393 [binder, in Coq.PArith.BinPos]
s:394 [binder, in Coq.FSets.FSetPositive]
s:396 [binder, in Coq.MSets.MSetRBT]
s:397 [binder, in Coq.MSets.MSetRBT]
s:398 [binder, in Coq.FSets.FSetPositive]
s:4 [binder, in Coq.FSets.FSetBridge]
s:4 [binder, in Coq.MSets.MSetProperties]
s:4 [binder, in Coq.Floats.SpecFloat]
s:4 [binder, in Coq.Strings.ByteVector]
s:4 [binder, in Coq.FSets.FSetProperties]
s:4 [binder, in Coq.FSets.FSetCompat]
s:40 [binder, in Coq.FSets.FSetBridge]
s:40 [binder, in Coq.MSets.MSetEqProperties]
s:40 [binder, in Coq.PArith.BinPos]
s:40 [binder, in Coq.FSets.FSetEqProperties]
s:40 [binder, in Coq.MSets.MSetGenTree]
s:40 [binder, in Coq.FSets.FSetCompat]
s:400 [binder, in Coq.FSets.FSetPositive]
s:401 [binder, in Coq.FSets.FSetPositive]
s:404 [binder, in Coq.FSets.FSetPositive]
s:406 [binder, in Coq.FSets.FSetPositive]
s:407 [binder, in Coq.FSets.FSetPositive]
s:409 [binder, in Coq.PArith.BinPos]
s:41 [binder, in Coq.MSets.MSetWeakList]
s:41 [binder, in Coq.MSets.MSetAVL]
s:41 [binder, in Coq.FSets.FSetCompat]
s:418 [binder, in Coq.MSets.MSetRBT]
s:419 [binder, in Coq.PArith.BinPos]
s:42 [binder, in Coq.Strings.String]
s:421 [binder, in Coq.MSets.MSetRBT]
s:423 [binder, in Coq.MSets.MSetRBT]
s:426 [binder, in Coq.MSets.MSetRBT]
s:429 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
s:429 [binder, in Coq.MSets.MSetRBT]
s:43 [binder, in Coq.MSets.MSetEqProperties]
s:43 [binder, in Coq.FSets.FSetEqProperties]
s:431 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
s:432 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
s:434 [binder, in Coq.MSets.MSetRBT]
s:437 [binder, in Coq.MSets.MSetRBT]
s:439 [binder, in Coq.MSets.MSetRBT]
s:44 [binder, in Coq.MSets.MSetRBT]
s:44 [binder, in Coq.MSets.MSetGenTree]
s:44 [binder, in Coq.FSets.FSetCompat]
s:442 [binder, in Coq.MSets.MSetRBT]
s:445 [binder, in Coq.MSets.MSetRBT]
s:46 [binder, in Coq.FSets.FSetBridge]
s:46 [binder, in Coq.MSets.MSetWeakList]
s:46 [binder, in Coq.MSets.MSetList]
s:47 [binder, in Coq.Strings.String]
s:47 [binder, in Coq.MSets.MSetWeakList]
s:47 [binder, in Coq.FSets.FSetCompat]
s:478 [binder, in Coq.Reals.RIneq]
s:48 [binder, in Coq.MSets.MSetEqProperties]
s:48 [binder, in Coq.MSets.MSetWeakList]
s:48 [binder, in Coq.FSets.FSetEqProperties]
s:49 [binder, in Coq.MSets.MSetList]
s:49 [binder, in Coq.MSets.MSetGenTree]
s:5 [binder, in Coq.FSets.FSetToFiniteSet]
s:5 [binder, in Coq.Floats.SpecFloat]
s:5 [binder, in Coq.MSets.MSetToFiniteSet]
s:50 [binder, in Coq.MSets.MSetEqProperties]
s:50 [binder, in Coq.MSets.MSetWeakList]
s:50 [binder, in Coq.Init.Wf]
s:50 [binder, in Coq.FSets.FSetEqProperties]
s:50 [binder, in Coq.FSets.FMapWeakList]
s:50 [binder, in Coq.FSets.FSetCompat]
s:51 [binder, in Coq.Strings.String]
s:517 [binder, in Coq.MSets.MSetAVL]
s:52 [binder, in Coq.MSets.MSetEqProperties]
s:52 [binder, in Coq.FSets.FSetEqProperties]
s:520 [binder, in Coq.MSets.MSetAVL]
s:524 [binder, in Coq.MSets.MSetAVL]
s:53 [binder, in Coq.MSets.MSetEqProperties]
s:53 [binder, in Coq.MSets.MSetWeakList]
s:53 [binder, in Coq.MSets.MSetList]
s:53 [binder, in Coq.FSets.FSetEqProperties]
s:53 [binder, in Coq.FSets.FSetCompat]
s:538 [binder, in Coq.MSets.MSetRBT]
s:54 [binder, in Coq.MSets.MSetEqProperties]
s:54 [binder, in Coq.MSets.MSetProperties]
s:54 [binder, in Coq.FSets.FSetEqProperties]
s:54 [binder, in Coq.FSets.FMapWeakList]
s:54 [binder, in Coq.FSets.FSetProperties]
s:548 [binder, in Coq.PArith.BinPos]
s:55 [binder, in Coq.FSets.FSetDecide]
s:55 [binder, in Coq.MSets.MSetDecide]
s:55 [binder, in Coq.MSets.MSetAVL]
s:55 [binder, in Coq.FSets.FMapList]
s:550 [binder, in Coq.PArith.BinPos]
s:56 [binder, in Coq.MSets.MSetEqProperties]
s:56 [binder, in Coq.FSets.FSetEqProperties]
s:56 [binder, in Coq.FSets.FMapWeakList]
s:56 [binder, in Coq.FSets.FSetCompat]
s:563 [binder, in Coq.PArith.BinPos]
s:563 [binder, in Coq.MSets.MSetAVL]
s:567 [binder, in Coq.MSets.MSetAVL]
s:57 [binder, in Coq.MSets.MSetList]
s:572 [binder, in Coq.Reals.RIneq]
s:58 [binder, in Coq.MSets.MSetEqProperties]
s:58 [binder, in Coq.MSets.MSetProperties]
s:58 [binder, in Coq.MSets.MSetWeakList]
s:58 [binder, in Coq.FSets.FSetEqProperties]
s:58 [binder, in Coq.FSets.FSetProperties]
s:580 [binder, in Coq.MSets.MSetAVL]
s:584 [binder, in Coq.MSets.MSetAVL]
s:588 [binder, in Coq.MSets.MSetAVL]
s:59 [binder, in Coq.Lists.Streams]
s:59 [binder, in Coq.FSets.FSetBridge]
S:59 [binder, in Coq.micromega.ZifyClasses]
s:59 [binder, in Coq.FSets.FMapWeakList]
s:59 [binder, in Coq.FSets.FMapList]
s:59 [binder, in Coq.FSets.FSetCompat]
s:591 [binder, in Coq.MSets.MSetAVL]
s:598 [binder, in Coq.MSets.MSetAVL]
s:6 [binder, in Coq.FSets.FSetBridge]
s:6 [binder, in Coq.FSets.FSetInterface]
s:6 [binder, in Coq.MSets.MSetRBT]
s:60 [binder, in Coq.FSets.FSetDecide]
s:60 [binder, in Coq.MSets.MSetEqProperties]
s:60 [binder, in Coq.MSets.MSetDecide]
s:60 [binder, in Coq.FSets.FSetEqProperties]
s:601 [binder, in Coq.MSets.MSetAVL]
s:608 [binder, in Coq.MSets.MSetRBT]
s:609 [binder, in Coq.MSets.MSetRBT]
s:61 [binder, in Coq.MSets.MSetWeakList]
s:61 [binder, in Coq.MSets.MSetList]
s:61 [binder, in Coq.FSets.FMapList]
s:611 [binder, in Coq.MSets.MSetRBT]
s:613 [binder, in Coq.MSets.MSetRBT]
s:614 [binder, in Coq.MSets.MSetRBT]
s:62 [binder, in Coq.Lists.Streams]
s:62 [binder, in Coq.FSets.FMapWeakList]
s:62 [binder, in Coq.FSets.FSetCompat]
s:63 [binder, in Coq.MSets.MSetEqProperties]
s:63 [binder, in Coq.FSets.FSetEqProperties]
s:64 [binder, in Coq.Lists.Streams]
s:64 [binder, in Coq.MSets.MSetWeakList]
s:64 [binder, in Coq.FSets.FMapList]
s:641 [binder, in Coq.MSets.MSetAVL]
s:644 [binder, in Coq.MSets.MSetAVL]
s:647 [binder, in Coq.MSets.MSetAVL]
s:648 [binder, in Coq.MSets.MSetRBT]
s:65 [binder, in Coq.FSets.FSetBridge]
s:65 [binder, in Coq.FSets.FSetDecide]
s:65 [binder, in Coq.MSets.MSetProperties]
s:65 [binder, in Coq.MSets.MSetDecide]
s:65 [binder, in Coq.FSets.FSetProperties]
s:65 [binder, in Coq.FSets.FSetCompat]
s:650 [binder, in Coq.MSets.MSetAVL]
s:651 [binder, in Coq.MSets.MSetRBT]
s:652 [binder, in Coq.MSets.MSetAVL]
s:654 [binder, in Coq.MSets.MSetRBT]
s:655 [binder, in Coq.MSets.MSetAVL]
s:657 [binder, in Coq.MSets.MSetAVL]
s:658 [binder, in Coq.MSets.MSetRBT]
S:66 [binder, in Coq.Lists.Streams]
s:66 [binder, in Coq.MSets.MSetList]
s:66 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
s:660 [binder, in Coq.MSets.MSetAVL]
s:661 [binder, in Coq.MSets.MSetRBT]
s:663 [binder, in Coq.MSets.MSetAVL]
s:664 [binder, in Coq.MSets.MSetRBT]
s:668 [binder, in Coq.MSets.MSetRBT]
s:67 [binder, in Coq.Lists.Streams]
s:67 [binder, in Coq.MSets.MSetWeakList]
s:67 [binder, in Coq.FSets.FMapList]
s:671 [binder, in Coq.MSets.MSetRBT]
s:674 [binder, in Coq.MSets.MSetRBT]
S:68 [binder, in Coq.micromega.ZifyClasses]
s:68 [binder, in Coq.MSets.MSetEqProperties]
s:68 [binder, in Coq.MSets.MSetList]
s:68 [binder, in Coq.FSets.FSetEqProperties]
s:68 [binder, in Coq.FSets.FSetCompat]
S:69 [binder, in Coq.Lists.Streams]
s:69 [binder, in Coq.FSets.FSetBridge]
s:69 [binder, in Coq.ssr.ssrfun]
s:691 [binder, in Coq.MSets.MSetRBT]
s:693 [binder, in Coq.MSets.MSetRBT]
s:695 [binder, in Coq.MSets.MSetRBT]
s:7 [binder, in Coq.FSets.FSetToFiniteSet]
s:7 [binder, in Coq.MSets.MSetWeakList]
s:7 [binder, in Coq.MSets.MSetList]
s:7 [binder, in Coq.MSets.MSetToFiniteSet]
s:7 [binder, in Coq.Setoids.Setoid]
s:7 [binder, in Coq.Strings.ByteVector]
s:7 [binder, in Coq.FSets.FSetCompat]
s:70 [binder, in Coq.Lists.Streams]
S:70 [binder, in Coq.Classes.Morphisms]
s:70 [binder, in Coq.MSets.MSetWeakList]
s:70 [binder, in Coq.MSets.MSetList]
s:70 [binder, in Coq.Sets.Powerset_facts]
s:71 [binder, in Coq.FSets.FSetCompat]
s:712 [binder, in Coq.MSets.MSetRBT]
s:713 [binder, in Coq.MSets.MSetRBT]
s:72 [binder, in Coq.FSets.FSetDecide]
s:72 [binder, in Coq.MSets.MSetEqProperties]
s:72 [binder, in Coq.MSets.MSetProperties]
s:72 [binder, in Coq.MSets.MSetDecide]
s:72 [binder, in Coq.MSets.MSetWeakList]
s:72 [binder, in Coq.FSets.FSetEqProperties]
s:72 [binder, in Coq.Sets.Powerset_facts]
s:72 [binder, in Coq.FSets.FSetProperties]
s:720 [binder, in Coq.MSets.MSetRBT]
s:73 [binder, in Coq.FSets.FSetBridge]
S:73 [binder, in Coq.Logic.ChoiceFacts]
s:73 [binder, in Coq.MSets.MSetList]
S:73 [binder, in Coq.rtauto.Bintree]
s:74 [binder, in Coq.MSets.MSetEqProperties]
s:74 [binder, in Coq.FSets.FSetEqProperties]
s:74 [binder, in Coq.Sets.Powerset_facts]
s:74 [binder, in Coq.FSets.FSetCompat]
s:75 [binder, in Coq.MSets.MSetProperties]
S:75 [binder, in Coq.rtauto.Bintree]
S:75 [binder, in Coq.Classes.CMorphisms]
s:75 [binder, in Coq.FSets.FSetProperties]
s:76 [binder, in Coq.FSets.FSetDecide]
s:76 [binder, in Coq.MSets.MSetEqProperties]
s:76 [binder, in Coq.MSets.MSetProperties]
s:76 [binder, in Coq.MSets.MSetDecide]
s:76 [binder, in Coq.FSets.FSetEqProperties]
s:76 [binder, in Coq.Sets.Powerset_facts]
s:76 [binder, in Coq.FSets.FSetProperties]
s:77 [binder, in Coq.MSets.MSetWeakList]
s:77 [binder, in Coq.FSets.FSetCompat]
s:78 [binder, in Coq.FSets.FSetDecide]
s:78 [binder, in Coq.MSets.MSetEqProperties]
s:78 [binder, in Coq.MSets.MSetDecide]
s:78 [binder, in Coq.FSets.FSetEqProperties]
s:8 [binder, in Coq.MSets.MSetProperties]
s:8 [binder, in Coq.Sets.Uniset]
S:8 [binder, in Coq.Classes.SetoidDec]
s:8 [binder, in Coq.FSets.FSetProperties]
s:80 [binder, in Coq.MSets.MSetEqProperties]
S:80 [binder, in Coq.rtauto.Bintree]
s:80 [binder, in Coq.FSets.FSetEqProperties]
s:80 [binder, in Coq.FSets.FSetCompat]
s:81 [binder, in Coq.MSets.MSetWeakList]
S:81 [binder, in Coq.rtauto.Bintree]
s:82 [binder, in Coq.MSets.MSetEqProperties]
s:82 [binder, in Coq.FSets.FSetEqProperties]
S:83 [binder, in Coq.rtauto.Bintree]
s:83 [binder, in Coq.FSets.FSetCompat]
s:84 [binder, in Coq.MSets.MSetWeakList]
s:84 [binder, in Coq.MSets.MSetList]
s:85 [binder, in Coq.FSets.FSetBridge]
S:85 [binder, in Coq.micromega.ZifyClasses]
s:85 [binder, in Coq.MSets.MSetList]
s:86 [binder, in Coq.MSets.MSetProperties]
S:86 [binder, in Coq.rtauto.Bintree]
s:86 [binder, in Coq.FSets.FSetProperties]
s:87 [binder, in Coq.FSets.FSetBridge]
s:87 [binder, in Coq.MSets.MSetEqProperties]
s:87 [binder, in Coq.Strings.String]
s:87 [binder, in Coq.FSets.FSetEqProperties]
s:88 [binder, in Coq.MSets.MSetWeakList]
s:88 [binder, in Coq.MSets.MSetList]
s:88 [binder, in Coq.MSets.MSetAVL]
s:89 [binder, in Coq.MSets.MSetInterface]
s:89 [binder, in Coq.FSets.FSetBridge]
s:89 [binder, in Coq.MSets.MSetEqProperties]
S:89 [binder, in Coq.rtauto.Bintree]
s:89 [binder, in Coq.Arith.PeanoNat]
s:89 [binder, in Coq.FSets.FSetEqProperties]
S:9 [binder, in Coq.FSets.FSetDecide]
s:9 [binder, in Coq.FSets.FSetToFiniteSet]
S:9 [binder, in Coq.MSets.MSetDecide]
s:9 [binder, in Coq.FSets.FSetInterface]
s:9 [binder, in Coq.FSets.FMapFullAVL]
s:9 [binder, in Coq.MSets.MSetToFiniteSet]
s:90 [binder, in Coq.FSets.FSetCompat]
s:91 [binder, in Coq.MSets.MSetEqProperties]
s:91 [binder, in Coq.Strings.String]
S:91 [binder, in Coq.rtauto.Bintree]
s:91 [binder, in Coq.FSets.FSetEqProperties]
s:93 [binder, in Coq.MSets.MSetInterface]
s:93 [binder, in Coq.FSets.FSetBridge]
s:93 [binder, in Coq.MSets.MSetEqProperties]
s:93 [binder, in Coq.MSets.MSetList]
S:93 [binder, in Coq.rtauto.Bintree]
s:93 [binder, in Coq.FSets.FSetEqProperties]
s:94 [binder, in Coq.Strings.String]
s:94 [binder, in Coq.MSets.MSetWeakList]
s:94 [binder, in Coq.MSets.MSetAVL]
s:95 [binder, in Coq.FSets.FSetBridge]
s:95 [binder, in Coq.MSets.MSetWeakList]
s:95 [binder, in Coq.MSets.MSetList]
S:95 [binder, in Coq.rtauto.Bintree]
s:95 [binder, in Coq.MSets.MSetRBT]
s:96 [binder, in Coq.MSets.MSetInterface]
s:96 [binder, in Coq.FSets.FMapWeakList]
s:96 [binder, in Coq.FSets.FSetCompat]
s:97 [binder, in Coq.FSets.FSetBridge]
s:97 [binder, in Coq.FSets.FSetDecide]
s:97 [binder, in Coq.MSets.MSetProperties]
s:97 [binder, in Coq.Strings.String]
s:97 [binder, in Coq.MSets.MSetDecide]
s:97 [binder, in Coq.MSets.MSetWeakList]
s:97 [binder, in Coq.FSets.FSetProperties]
s:97 [binder, in Coq.FSets.FSetCompat]
s:98 [binder, in Coq.MSets.MSetEqProperties]
s:98 [binder, in Coq.MSets.MSetProperties]
s:98 [binder, in Coq.Strings.String]
s:98 [binder, in Coq.MSets.MSetList]
s:98 [binder, in Coq.Arith.PeanoNat]
s:98 [binder, in Coq.FSets.FSetEqProperties]
s:98 [binder, in Coq.MSets.MSetGenTree]
s:98 [binder, in Coq.FSets.FSetProperties]
s:99 [binder, in Coq.MSets.MSetInterface]
s:99 [binder, in Coq.Strings.String]
s:99 [binder, in Coq.MSets.MSetWeakList]
| 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 | (68863 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 | (985 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 | (44709 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 | (761 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 | (1497 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 | (570 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 | (11380 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 | (976 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 | (603 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 | (298 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 | (460 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 | (476 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 | (811 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 | (1157 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 | (4018 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) |