| 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) |
Y
Y [definition, in Coq.Logic.WKL]Y [definition, in Coq.Logic.WeakFan]
ybound:51 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
yn:12 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
yn:3 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
yr [definition, in Coq.Reals.Rgeom]
ys:270 [binder, in Coq.MSets.MSetList]
yt [definition, in Coq.Reals.Rgeom]
Y_approx [lemma, in Coq.Logic.WKL]
Y_unique [lemma, in Coq.Logic.WKL]
Y_approx [lemma, in Coq.Logic.WeakFan]
Y_unique [lemma, in Coq.Logic.WeakFan]
y'':186 [binder, in Coq.Logic.EqdepFacts]
y'':188 [binder, in Coq.Logic.EqdepFacts]
y':101 [binder, in Coq.Relations.Relation_Operators]
y':112 [binder, in Coq.Relations.Relation_Operators]
y':185 [binder, in Coq.Logic.EqdepFacts]
y':187 [binder, in Coq.Logic.EqdepFacts]
y':259 [binder, in Coq.Logic.ChoiceFacts]
y':262 [binder, in Coq.Logic.ChoiceFacts]
y':34 [binder, in Coq.Logic.Eqdep_dec]
y':36 [binder, in Coq.Relations.Relation_Definitions]
y':37 [binder, in Coq.Relations.Relation_Definitions]
y':377 [binder, in Coq.Logic.ChoiceFacts]
y':383 [binder, in Coq.Logic.ChoiceFacts]
y':386 [binder, in Coq.Logic.ChoiceFacts]
y':389 [binder, in Coq.Logic.ChoiceFacts]
y':4 [binder, in Coq.Logic.Eqdep_dec]
y':52 [binder, in Coq.Logic.Decidable]
y':57 [binder, in Coq.Logic.Eqdep_dec]
y':61 [binder, in Coq.Init.Wf]
y':68 [binder, in Coq.Init.Wf]
y':7 [binder, in Coq.Wellfounded.Union]
y':76 [binder, in Coq.Init.Wf]
y':8 [binder, in Coq.Wellfounded.Union]
y':83 [binder, in Coq.Logic.ChoiceFacts]
y':9 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y':98 [binder, in Coq.Relations.Relation_Operators]
y0:12 [binder, in Coq.Reals.Rgeom]
y0:2 [binder, in Coq.Reals.Rgeom]
y0:22 [binder, in Coq.Wellfounded.Lexicographic_Product]
y0:22 [binder, in Coq.Reals.Rgeom]
y0:23 [binder, in Coq.Wellfounded.Lexicographic_Product]
y0:309 [binder, in Coq.Reals.Rtopology]
y0:312 [binder, in Coq.Reals.Rtopology]
y0:338 [binder, in Coq.Reals.Rtopology]
y0:339 [binder, in Coq.Reals.Rtopology]
y0:341 [binder, in Coq.Reals.Rtopology]
y0:342 [binder, in Coq.Reals.Rtopology]
y0:6 [binder, in Coq.Reals.Rgeom]
y0:625 [binder, in Coq.Lists.List]
y0:8 [binder, in Coq.Reals.Rgeom]
y1:10 [binder, in Coq.Reals.Rgeom]
y1:1120 [binder, in Coq.FSets.FMapAVL]
y1:1174 [binder, in Coq.FSets.FMapAVL]
y1:1179 [binder, in Coq.FSets.FMapAVL]
y1:14 [binder, in Coq.Reals.Rgeom]
y1:15 [binder, in Coq.micromega.OrderedRing]
y1:176 [binder, in Coq.Init.Logic]
y1:196 [binder, in Coq.Init.Logic]
y1:20 [binder, in Coq.micromega.OrderedRing]
y1:205 [binder, in Coq.Init.Logic]
y1:217 [binder, in Coq.Init.Logic]
y1:220 [binder, in Coq.setoid_ring.Ncring]
y1:232 [binder, in Coq.Init.Logic]
y1:24 [binder, in Coq.Reals.Rgeom]
y1:28 [binder, in Coq.micromega.OrderedRing]
y1:292 [binder, in Coq.Init.Logic]
y1:324 [binder, in Coq.Init.Logic]
y1:33 [binder, in Coq.micromega.OrderedRing]
y1:34 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y1:35 [binder, in Coq.Reals.Rgeom]
y1:356 [binder, in Coq.Lists.List]
y1:4 [binder, in Coq.Reals.Rgeom]
y1:50 [binder, in Coq.Reals.Rgeom]
y1:55 [binder, in Coq.Reals.Rgeom]
y1:56 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y1:560 [binder, in Coq.MSets.MSetAVL]
y1:577 [binder, in Coq.MSets.MSetAVL]
y1:58 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y1:60 [binder, in Coq.Reals.Rgeom]
y1:67 [binder, in Coq.Reals.Rgeom]
y1:89 [binder, in Coq.Init.Datatypes]
y2:1121 [binder, in Coq.FSets.FMapAVL]
y2:1175 [binder, in Coq.FSets.FMapAVL]
y2:1180 [binder, in Coq.FSets.FMapAVL]
y2:16 [binder, in Coq.micromega.OrderedRing]
y2:16 [binder, in Coq.Reals.Rgeom]
y2:177 [binder, in Coq.Init.Logic]
y2:198 [binder, in Coq.Init.Logic]
y2:207 [binder, in Coq.Init.Logic]
y2:21 [binder, in Coq.micromega.OrderedRing]
y2:219 [binder, in Coq.Init.Logic]
y2:221 [binder, in Coq.setoid_ring.Ncring]
y2:234 [binder, in Coq.Init.Logic]
y2:26 [binder, in Coq.Reals.Rgeom]
y2:29 [binder, in Coq.micromega.OrderedRing]
y2:293 [binder, in Coq.Init.Logic]
y2:325 [binder, in Coq.Init.Logic]
y2:34 [binder, in Coq.micromega.OrderedRing]
y2:357 [binder, in Coq.Lists.List]
y2:36 [binder, in Coq.Reals.Rgeom]
y2:52 [binder, in Coq.Reals.Rgeom]
y2:561 [binder, in Coq.MSets.MSetAVL]
y2:57 [binder, in Coq.Reals.Rgeom]
y2:578 [binder, in Coq.MSets.MSetAVL]
y2:62 [binder, in Coq.Reals.Rgeom]
y2:69 [binder, in Coq.Reals.Rgeom]
y2:90 [binder, in Coq.Init.Datatypes]
y3:209 [binder, in Coq.Init.Logic]
y3:221 [binder, in Coq.Init.Logic]
y3:236 [binder, in Coq.Init.Logic]
y3:294 [binder, in Coq.Init.Logic]
y4:223 [binder, in Coq.Init.Logic]
y4:238 [binder, in Coq.Init.Logic]
y5:240 [binder, in Coq.Init.Logic]
y:1 [binder, in Coq.Init.Tauto]
y:10 [binder, in Coq.Structures.DecidableTypeEx]
Y:10 [binder, in Coq.Sets.Finite_sets_facts]
y:10 [binder, in Coq.PArith.BinPos]
y:10 [binder, in Coq.ZArith.BinInt]
y:10 [binder, in Coq.QArith.Qreals]
y:10 [binder, in Coq.funind.Recdef]
y:10 [binder, in Coq.Sets.Partial_Order]
y:10 [binder, in Coq.Sets.Relations_1_facts]
y:10 [binder, in Coq.ZArith.Zbool]
y:10 [binder, in Coq.micromega.ZifyComparison]
y:10 [binder, in Coq.Structures.GenericMinMax]
y:10 [binder, in Coq.Reals.PSeries_reg]
y:10 [binder, in Coq.Reals.Ranalysis5]
y:10 [binder, in Coq.omega.PreOmega]
y:10 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:10 [binder, in Coq.Sets.Relations_1]
y:10 [binder, in Coq.Relations.Relation_Definitions]
y:10 [binder, in Coq.Reals.ROrderedType]
y:10 [binder, in Coq.Floats.FloatAxioms]
y:10 [binder, in Coq.Sorting.Heap]
y:10 [binder, in Coq.Structures.OrdersFacts]
y:100 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:100 [binder, in Coq.QArith.Qcanon]
y:100 [binder, in Coq.Lists.List]
y:100 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:100 [binder, in Coq.Structures.EqualitiesFacts]
y:100 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:100 [binder, in Coq.Relations.Relation_Operators]
y:100 [binder, in Coq.QArith.QArith_base]
y:1005 [binder, in Coq.Lists.List]
y:101 [binder, in Coq.Program.Wf]
y:101 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:101 [binder, in Coq.Reals.Rbasic_fun]
y:101 [binder, in Coq.setoid_ring.Ring_theory]
y:101 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:101 [binder, in Coq.Structures.OrdersFacts]
y:1011 [binder, in Coq.Lists.List]
y:1018 [binder, in Coq.Lists.List]
y:102 [binder, in Coq.Program.Wf]
y:102 [binder, in Coq.FSets.FSetBridge]
y:102 [binder, in Coq.Reals.Ranalysis4]
y:102 [binder, in Coq.Init.Nat]
y:102 [binder, in Coq.Arith.PeanoNat]
y:102 [binder, in Coq.Structures.OrderedType]
y:102 [binder, in Coq.Reals.Ranalysis5]
y:102 [binder, in Coq.Structures.EqualitiesFacts]
y:102 [binder, in Coq.setoid_ring.Ncring]
y:102 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:102 [binder, in Coq.QArith.QArith_base]
y:103 [binder, in Coq.QArith.Qcanon]
y:103 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:103 [binder, in Coq.Structures.OrderedTypeEx]
y:103 [binder, in Coq.Reals.Rtopology]
y:103 [binder, in Coq.Reals.Rbasic_fun]
y:103 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:103 [binder, in Coq.Structures.OrdersFacts]
y:103 [binder, in Coq.Reals.Cos_plus]
y:1036 [binder, in Coq.FSets.FMapAVL]
y:104 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:104 [binder, in Coq.FSets.FMapFacts]
y:104 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:104 [binder, in Coq.Logic.ChoiceFacts]
y:104 [binder, in Coq.Sorting.Permutation]
y:104 [binder, in Coq.Reals.PSeries_reg]
y:104 [binder, in Coq.setoid_ring.Ring_theory]
y:104 [binder, in Coq.QArith.QArith_base]
y:104 [binder, in Coq.Logic.FinFun]
y:1045 [binder, in Coq.FSets.FMapAVL]
y:1046 [binder, in Coq.Lists.List]
y:105 [binder, in Coq.Program.Wf]
y:105 [binder, in Coq.QArith.Qcanon]
y:105 [binder, in Coq.Init.Nat]
y:1050 [binder, in Coq.Lists.List]
y:1050 [binder, in Coq.FSets.FMapAVL]
y:1056 [binder, in Coq.FSets.FMapAVL]
y:1059 [binder, in Coq.FSets.FMapAVL]
y:106 [binder, in Coq.Program.Wf]
y:106 [binder, in Coq.Logic.ChoiceFacts]
y:106 [binder, in Coq.Reals.Ranalysis5]
y:106 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:106 [binder, in Coq.setoid_ring.Ncring]
y:106 [binder, in Coq.QArith.QArith_base]
y:106 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:106 [binder, in Coq.Structures.OrdersFacts]
y:1061 [binder, in Coq.Lists.List]
y:1066 [binder, in Coq.FSets.FMapAVL]
y:107 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:107 [binder, in Coq.Program.Wf]
y:107 [binder, in Coq.QArith.Qcanon]
y:107 [binder, in Coq.Logic.Eqdep_dec]
y:107 [binder, in Coq.Reals.Rfunctions]
y:107 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:107 [binder, in Coq.Structures.OrderedType]
y:107 [binder, in Coq.Reals.PSeries_reg]
y:1070 [binder, in Coq.FSets.FMapAVL]
y:1075 [binder, in Coq.FSets.FMapAVL]
y:108 [binder, in Coq.Program.Wf]
y:1080 [binder, in Coq.FSets.FMapAVL]
y:1087 [binder, in Coq.FSets.FMapAVL]
y:109 [binder, in Coq.Program.Wf]
y:109 [binder, in Coq.QArith.Qcanon]
y:109 [binder, in Coq.Logic.Eqdep_dec]
y:109 [binder, in Coq.Reals.Rpower]
y:109 [binder, in Coq.Reals.Rtopology]
y:109 [binder, in Coq.Reals.PSeries_reg]
y:109 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:109 [binder, in Coq.Init.Logic]
y:109 [binder, in Coq.QArith.QArith_base]
y:109 [binder, in Coq.Lists.SetoidList]
y:109 [binder, in Coq.Structures.OrdersFacts]
y:1093 [binder, in Coq.FSets.FMapAVL]
y:11 [binder, in Coq.Structures.Orders]
y:11 [binder, in Coq.Relations.Operators_Properties]
y:11 [binder, in Coq.Structures.OrdersLists]
y:11 [binder, in Coq.Sets.Relations_3]
y:11 [binder, in Coq.FSets.FSetDecide]
y:11 [binder, in Coq.Arith.Bool_nat]
y:11 [binder, in Coq.Reals.Exp_prop]
y:11 [binder, in Coq.MSets.MSetDecide]
y:11 [binder, in Coq.Relations.Relations]
y:11 [binder, in Coq.Init.Logic_Type]
y:11 [binder, in Coq.Lists.SetoidPermutation]
y:11 [binder, in Coq.Structures.OrderedTypeEx]
y:11 [binder, in Coq.Reals.Raxioms]
y:11 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
y:11 [binder, in Coq.Bool.BoolEq]
y:11 [binder, in Coq.Classes.SetoidDec]
y:11 [binder, in Coq.Strings.Byte]
y:11 [binder, in Coq.Logic.HLevels]
y:11 [binder, in Coq.Sets.Relations_2]
Y:11 [binder, in Coq.Sets.Classical_sets]
y:11 [binder, in Coq.Structures.OrdersTac]
y:11 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:11 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:110 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:110 [binder, in Coq.Program.Wf]
y:110 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:110 [binder, in Coq.setoid_ring.Field_theory]
y:110 [binder, in Coq.ssr.ssreflect]
y:110 [binder, in Coq.Structures.OrderedType]
y:110 [binder, in Coq.Reals.Ranalysis5]
y:110 [binder, in Coq.setoid_ring.Ring_theory]
y:110 [binder, in Coq.setoid_ring.Ncring]
y:110 [binder, in Coq.Relations.Relation_Operators]
y:111 [binder, in Coq.Program.Wf]
y:111 [binder, in Coq.QArith.Qcanon]
y:111 [binder, in Coq.Lists.ListSet]
y:111 [binder, in Coq.Reals.PSeries_reg]
y:111 [binder, in Coq.Relations.Relation_Operators]
y:111 [binder, in Coq.QArith.QArith_base]
y:111 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:1110 [binder, in Coq.FSets.FMapAVL]
y:1113 [binder, in Coq.FSets.FMapAVL]
y:1116 [binder, in Coq.FSets.FMapAVL]
y:112 [binder, in Coq.Program.Wf]
y:112 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:112 [binder, in Coq.FSets.FSetDecide]
y:112 [binder, in Coq.FSets.FMapFacts]
y:112 [binder, in Coq.Logic.ChoiceFacts]
y:112 [binder, in Coq.MSets.MSetDecide]
y:112 [binder, in Coq.Reals.PSeries_reg]
y:112 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:112 [binder, in Coq.Structures.OrdersFacts]
y:1124 [binder, in Coq.FSets.FMapAVL]
y:1129 [binder, in Coq.FSets.FMapAVL]
y:113 [binder, in Coq.Program.Wf]
y:113 [binder, in Coq.QArith.Qcanon]
y:113 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:113 [binder, in Coq.Reals.Rtrigo1]
y:113 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:113 [binder, in Coq.Structures.GenericMinMax]
y:113 [binder, in Coq.Reals.Ratan]
y:113 [binder, in Coq.setoid_ring.Ring_theory]
y:1132 [binder, in Coq.FSets.FMapAVL]
y:1136 [binder, in Coq.FSets.FMapAVL]
y:114 [binder, in Coq.Program.Wf]
y:114 [binder, in Coq.MSets.MSetGenTree]
y:114 [binder, in Coq.Lists.ListSet]
y:114 [binder, in Coq.Reals.PSeries_reg]
y:114 [binder, in Coq.setoid_ring.Ncring]
y:114 [binder, in Coq.QArith.QArith_base]
y:114 [binder, in Coq.Lists.SetoidList]
y:1142 [binder, in Coq.FSets.FMapAVL]
y:115 [binder, in Coq.Program.Wf]
y:115 [binder, in Coq.QArith.Qcanon]
y:115 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:115 [binder, in Coq.Reals.Rtrigo1]
y:115 [binder, in Coq.Reals.Rtopology]
y:115 [binder, in Coq.Structures.OrdersFacts]
y:1151 [binder, in Coq.FSets.FMapAVL]
y:1154 [binder, in Coq.FSets.FMapAVL]
y:1157 [binder, in Coq.FSets.FMapAVL]
y:116 [binder, in Coq.Program.Wf]
y:116 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:116 [binder, in Coq.Reals.Rtopology]
y:116 [binder, in Coq.Structures.OrderedType]
y:116 [binder, in Coq.Reals.PSeries_reg]
y:116 [binder, in Coq.QArith.QArith_base]
y:116 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:1168 [binder, in Coq.FSets.FMapAVL]
y:117 [binder, in Coq.Program.Wf]
y:117 [binder, in Coq.Reals.Rtrigo1]
y:117 [binder, in Coq.Logic.EqdepFacts]
y:117 [binder, in Coq.Logic.Hurkens]
y:117 [binder, in Coq.Reals.Rtopology]
y:117 [binder, in Coq.MSets.MSetGenTree]
y:117 [binder, in Coq.Lists.ListSet]
y:117 [binder, in Coq.setoid_ring.Ring_theory]
y:117 [binder, in Coq.Structures.OrdersFacts]
y:1171 [binder, in Coq.FSets.FMapAVL]
y:1178 [binder, in Coq.FSets.FMapAVL]
y:118 [binder, in Coq.Program.Wf]
y:118 [binder, in Coq.Reals.RiemannInt]
y:118 [binder, in Coq.Logic.ChoiceFacts]
y:118 [binder, in Coq.setoid_ring.InitialRing]
y:118 [binder, in Coq.Reals.Rtopology]
y:118 [binder, in Coq.Reals.Ratan]
y:118 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:119 [binder, in Coq.Program.Wf]
y:119 [binder, in Coq.Reals.Rtrigo1]
y:119 [binder, in Coq.Floats.SpecFloat]
y:119 [binder, in Coq.Logic.Hurkens]
y:119 [binder, in Coq.ssr.ssrfun]
y:119 [binder, in Coq.Reals.Rtopology]
y:119 [binder, in Coq.Structures.OrderedType]
y:119 [binder, in Coq.Relations.Relation_Operators]
y:119 [binder, in Coq.QArith.QArith_base]
y:1194 [binder, in Coq.FSets.FMapAVL]
y:12 [binder, in Coq.Program.Wf]
y:12 [binder, in Coq.Structures.DecidableTypeEx]
y:12 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:12 [binder, in Coq.Wellfounded.Inverse_Image]
y:12 [binder, in Coq.Logic.Eqdep_dec]
y:12 [binder, in Coq.Structures.OrdersEx]
y:12 [binder, in Coq.Logic.SetoidChoice]
y:12 [binder, in Coq.Logic.JMeq]
y:12 [binder, in Coq.Structures.OrdersAlt]
y:12 [binder, in Coq.QArith.Qreals]
y:12 [binder, in Coq.Reals.Machin]
y:12 [binder, in Coq.ZArith.Zwf]
y:12 [binder, in Coq.Sets.Cpo]
y:12 [binder, in Coq.funind.Recdef]
y:12 [binder, in Coq.Structures.OrderedTypeAlt]
y:12 [binder, in Coq.ZArith.Zbool]
y:12 [binder, in Coq.Sets.Permut]
y:12 [binder, in Coq.Reals.Ranalysis5]
y:12 [binder, in Coq.Sets.Relations_2]
y:12 [binder, in Coq.omega.PreOmega]
y:12 [binder, in Coq.Reals.Rlogic]
y:12 [binder, in Coq.Reals.ROrderedType]
y:12 [binder, in Coq.Reals.Cos_rel]
Y:12 [binder, in Coq.Sets.Infinite_sets]
y:12 [binder, in Coq.Reals.ClassicalConstructiveReals]
y:12 [binder, in Coq.Relations.Relation_Operators]
y:12 [binder, in Coq.Bool.DecBool]
y:12 [binder, in Coq.Structures.OrdersFacts]
y:12 [binder, in Coq.Sets.Powerset]
y:120 [binder, in Coq.Program.Wf]
y:120 [binder, in Coq.Logic.Eqdep_dec]
y:120 [binder, in Coq.MSets.MSetList]
y:120 [binder, in Coq.Reals.Rtopology]
y:120 [binder, in Coq.Lists.ListSet]
y:120 [binder, in Coq.Reals.Ratan]
y:120 [binder, in Coq.Structures.OrdersFacts]
y:121 [binder, in Coq.Program.Wf]
y:121 [binder, in Coq.Reals.Rtrigo1]
y:121 [binder, in Coq.Reals.MVT]
y:121 [binder, in Coq.Structures.OrderedTypeEx]
y:121 [binder, in Coq.Reals.Ranalysis5]
y:121 [binder, in Coq.setoid_ring.Ring_theory]
y:121 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:122 [binder, in Coq.Program.Wf]
y:122 [binder, in Coq.Logic.EqdepFacts]
y:122 [binder, in Coq.PArith.BinPos]
y:122 [binder, in Coq.FSets.FMapFacts]
y:122 [binder, in Coq.Reals.RiemannInt]
y:122 [binder, in Coq.Logic.ChoiceFacts]
y:122 [binder, in Coq.Classes.CRelationClasses]
y:122 [binder, in Coq.Structures.OrderedType]
y:122 [binder, in Coq.Reals.Ratan]
y:122 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:122 [binder, in Coq.Relations.Relation_Operators]
y:122 [binder, in Coq.QArith.QArith_base]
y:122 [binder, in Coq.Structures.OrdersFacts]
y:123 [binder, in Coq.QArith.Qcanon]
y:123 [binder, in Coq.Reals.Rtrigo1]
y:123 [binder, in Coq.Logic.ChoiceFacts]
y:123 [binder, in Coq.Reals.PSeries_reg]
y:124 [binder, in Coq.Reals.MVT]
y:124 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:124 [binder, in Coq.Structures.OrderedTypeEx]
y:124 [binder, in Coq.Reals.Ratan]
y:124 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:124 [binder, in Coq.Structures.OrdersFacts]
y:125 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
y:125 [binder, in Coq.Reals.Rtrigo1]
y:125 [binder, in Coq.FSets.FMapFacts]
y:125 [binder, in Coq.Reals.RiemannInt]
y:125 [binder, in Coq.Reals.PSeries_reg]
y:125 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:126 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:126 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:126 [binder, in Coq.Logic.EqdepFacts]
y:126 [binder, in Coq.Classes.CRelationClasses]
y:126 [binder, in Coq.Reals.Rbasic_fun]
y:126 [binder, in Coq.Init.Logic]
y:126 [binder, in Coq.QArith.QArith_base]
y:126 [binder, in Coq.Structures.OrdersFacts]
y:127 [binder, in Coq.QArith.Qcanon]
y:127 [binder, in Coq.Logic.Eqdep_dec]
y:127 [binder, in Coq.Reals.Rtrigo1]
y:127 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:127 [binder, in Coq.Logic.ChoiceFacts]
y:128 [binder, in Coq.Program.Wf]
y:128 [binder, in Coq.Reals.Rbasic_fun]
y:128 [binder, in Coq.Lists.ListSet]
y:128 [binder, in Coq.Structures.OrdersFacts]
y:129 [binder, in Coq.Program.Wf]
y:129 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
y:129 [binder, in Coq.Reals.Rtrigo1]
y:129 [binder, in Coq.setoid_ring.InitialRing]
y:129 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:1292 [binder, in Coq.FSets.FMapAVL]
y:13 [binder, in Coq.Program.Wf]
y:13 [binder, in Coq.Relations.Operators_Properties]
y:13 [binder, in Coq.ZArith.BinIntDef]
y:13 [binder, in Coq.FSets.FSetDecide]
y:13 [binder, in Coq.Logic.EqdepFacts]
y:13 [binder, in Coq.Arith.Bool_nat]
y:13 [binder, in Coq.Reals.MVT]
y:13 [binder, in Coq.ZArith.Zpow_facts]
y:13 [binder, in Coq.MSets.MSetDecide]
y:13 [binder, in Coq.Program.Subset]
y:13 [binder, in Coq.setoid_ring.Cring]
y:13 [binder, in Coq.QArith.Qfield]
y:13 [binder, in Coq.QArith.Qabs]
y:13 [binder, in Coq.Lists.ListDec]
y:13 [binder, in Coq.Classes.EquivDec]
y:13 [binder, in Coq.Reals.Raxioms]
y:13 [binder, in Coq.Structures.Equalities]
y:13 [binder, in Coq.Bool.BoolEq]
y:13 [binder, in Coq.Structures.GenericMinMax]
y:13 [binder, in Coq.Logic.ProofIrrelevanceFacts]
y:13 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]
y:13 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:13 [binder, in Coq.Structures.OrdersTac]
y:13 [binder, in Coq.Reals.R_sqr]
y:13 [binder, in Coq.Relations.Relation_Operators]
y:13 [binder, in Coq.Sorting.Heap]
y:13 [binder, in Coq.Lists.SetoidList]
y:13 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]
y:130 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:130 [binder, in Coq.QArith.Qcanon]
y:130 [binder, in Coq.FSets.FMapFacts]
y:130 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:130 [binder, in Coq.Reals.RiemannInt]
y:130 [binder, in Coq.Logic.Hurkens]
y:130 [binder, in Coq.Classes.CRelationClasses]
y:130 [binder, in Coq.Reals.Rtopology]
y:130 [binder, in Coq.Init.Logic]
y:130 [binder, in Coq.Structures.OrdersFacts]
y:131 [binder, in Coq.Reals.Rtrigo1]
y:131 [binder, in Coq.FSets.FSetDecide]
y:131 [binder, in Coq.MSets.MSetEqProperties]
y:131 [binder, in Coq.Reals.MVT]
y:131 [binder, in Coq.Reals.RiemannInt]
y:131 [binder, in Coq.MSets.MSetDecide]
y:131 [binder, in Coq.MSets.MSetList]
y:131 [binder, in Coq.FSets.FSetEqProperties]
y:131 [binder, in Coq.Lists.ListSet]
y:131 [binder, in Coq.QArith.QArith_base]
y:132 [binder, in Coq.Program.Wf]
y:132 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:132 [binder, in Coq.Reals.RiemannInt]
y:132 [binder, in Coq.Logic.Hurkens]
y:132 [binder, in Coq.ssr.ssrfun]
y:132 [binder, in Coq.Reals.Rtopology]
y:132 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:133 [binder, in Coq.Program.Wf]
y:133 [binder, in Coq.QArith.Qcanon]
y:133 [binder, in Coq.Reals.Rtrigo1]
y:133 [binder, in Coq.Arith.Wf_nat]
y:133 [binder, in Coq.Reals.RiemannInt]
y:133 [binder, in Coq.Relations.Relation_Operators]
y:1337 [binder, in Coq.FSets.FMapAVL]
y:134 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:134 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:134 [binder, in Coq.FSets.FMapFacts]
y:134 [binder, in Coq.FSets.FSetInterface]
y:134 [binder, in Coq.Init.Datatypes]
y:134 [binder, in Coq.Lists.ListSet]
y:134 [binder, in Coq.Init.Logic]
y:1342 [binder, in Coq.FSets.FMapAVL]
y:135 [binder, in Coq.Reals.Rtrigo1]
y:135 [binder, in Coq.Reals.Rsqrt_def]
y:135 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:135 [binder, in Coq.MSets.MSetList]
y:135 [binder, in Coq.Reals.Rtopology]
y:135 [binder, in Coq.Reals.Rbasic_fun]
y:135 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:135 [binder, in Coq.QArith.QArith_base]
y:135 [binder, in Coq.FSets.FSetCompat]
y:135 [binder, in Coq.Structures.OrdersFacts]
y:1351 [binder, in Coq.FSets.FMapAVL]
y:1354 [binder, in Coq.FSets.FMapAVL]
y:136 [binder, in Coq.Logic.Eqdep_dec]
y:136 [binder, in Coq.Sorting.PermutSetoid]
y:136 [binder, in Coq.Relations.Relation_Operators]
y:137 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:137 [binder, in Coq.Reals.Rtrigo1]
y:137 [binder, in Coq.Reals.Rsqrt_def]
y:137 [binder, in Coq.Reals.Rtopology]
y:137 [binder, in Coq.FSets.FMapWeakList]
y:137 [binder, in Coq.Reals.Ratan]
y:137 [binder, in Coq.Structures.OrdersFacts]
y:138 [binder, in Coq.Logic.Eqdep_dec]
y:138 [binder, in Coq.Logic.EqdepFacts]
y:138 [binder, in Coq.Reals.MVT]
y:138 [binder, in Coq.Arith.Wf_nat]
y:138 [binder, in Coq.FSets.FMapFacts]
y:138 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:138 [binder, in Coq.Reals.Ratan]
y:138 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:138 [binder, in Coq.Init.Logic]
y:138 [binder, in Coq.QArith.QArith_base]
y:139 [binder, in Coq.Reals.Rtrigo1]
y:139 [binder, in Coq.Init.Datatypes]
y:139 [binder, in Coq.Structures.OrdersFacts]
y:1396 [binder, in Coq.FSets.FMapAVL]
y:14 [binder, in Coq.Structures.Orders]
y:14 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:14 [binder, in Coq.nsatz.NsatzTactic]
y:14 [binder, in Coq.Logic.Eqdep_dec]
y:14 [binder, in Coq.FSets.FSetBridge]
y:14 [binder, in Coq.Reals.Rfunctions]
y:14 [binder, in Coq.Reals.MVT]
y:14 [binder, in Coq.Strings.String]
y:14 [binder, in Coq.Arith.Wf_nat]
y:14 [binder, in Coq.Reals.Exp_prop]
y:14 [binder, in Coq.Structures.OrdersAlt]
y:14 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
y:14 [binder, in Coq.Logic.ChoiceFacts]
y:14 [binder, in Coq.Init.Wf]
y:14 [binder, in Coq.setoid_ring.Integral_domain]
y:14 [binder, in Coq.QArith.Qreals]
y:14 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:14 [binder, in Coq.omega.OmegaLemmas]
y:14 [binder, in Coq.Structures.OrderedTypeEx]
y:14 [binder, in Coq.Sets.Relations_1_facts]
y:14 [binder, in Coq.Structures.OrderedTypeAlt]
y:14 [binder, in Coq.Sets.Relations_2_facts]
y:14 [binder, in Coq.Structures.OrderedType]
y:14 [binder, in Coq.Classes.SetoidClass]
y:14 [binder, in Coq.Reals.Ranalysis5]
y:14 [binder, in Coq.Setoids.Setoid]
y:14 [binder, in Coq.omega.PreOmega]
y:14 [binder, in Coq.Sets.Classical_sets]
y:14 [binder, in Coq.Reals.Rlogic]
y:14 [binder, in Coq.Sets.Relations_1]
y:14 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:14 [binder, in Coq.micromega.ZCoeff]
y:14 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:140 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:140 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:140 [binder, in Coq.Reals.RiemannInt]
y:1406 [binder, in Coq.FSets.FMapAVL]
y:141 [binder, in Coq.Sorting.PermutSetoid]
y:141 [binder, in Coq.Reals.Rtrigo1]
y:141 [binder, in Coq.Reals.Rsqrt_def]
y:141 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:141 [binder, in Coq.Reals.Rtopology]
y:141 [binder, in Coq.FSets.FMapWeakList]
y:141 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:141 [binder, in Coq.Relations.Relation_Operators]
y:141 [binder, in Coq.FSets.FSetCompat]
y:141 [binder, in Coq.Structures.OrdersFacts]
y:1410 [binder, in Coq.FSets.FMapAVL]
y:1415 [binder, in Coq.FSets.FMapAVL]
y:142 [binder, in Coq.FSets.FMapFacts]
y:142 [binder, in Coq.Reals.Rtopology]
y:1420 [binder, in Coq.FSets.FMapAVL]
y:1423 [binder, in Coq.FSets.FMapAVL]
y:1427 [binder, in Coq.FSets.FMapAVL]
y:143 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:143 [binder, in Coq.Reals.Rtrigo1]
y:143 [binder, in Coq.Logic.EqdepFacts]
y:143 [binder, in Coq.Reals.Rpower]
y:143 [binder, in Coq.FSets.FSetPositive]
y:143 [binder, in Coq.Reals.Rtopology]
y:143 [binder, in Coq.Structures.OrdersFacts]
y:144 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:144 [binder, in Coq.QArith.Qcanon]
y:144 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:144 [binder, in Coq.Init.Datatypes]
y:144 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:145 [binder, in Coq.Reals.Rtrigo1]
y:145 [binder, in Coq.FSets.FMapFullAVL]
y:145 [binder, in Coq.ssr.ssrfun]
y:145 [binder, in Coq.setoid_ring.Ring_theory]
y:145 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:145 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:145 [binder, in Coq.Structures.OrdersFacts]
y:1452 [binder, in Coq.FSets.FMapAVL]
y:146 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:146 [binder, in Coq.QArith.Qcanon]
y:146 [binder, in Coq.FSets.FMapFacts]
y:146 [binder, in Coq.ssr.ssrfun]
y:146 [binder, in Coq.Reals.Rtopology]
y:146 [binder, in Coq.FSets.FMapWeakList]
y:147 [binder, in Coq.Reals.Rtrigo1]
y:147 [binder, in Coq.Logic.EqdepFacts]
y:147 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:147 [binder, in Coq.Reals.Rtopology]
y:147 [binder, in Coq.FSets.FSetCompat]
y:147 [binder, in Coq.Structures.OrdersFacts]
y:148 [binder, in Coq.QArith.Qcanon]
y:148 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:148 [binder, in Coq.MSets.MSetGenTree]
y:148 [binder, in Coq.Reals.Ratan]
y:148 [binder, in Coq.setoid_ring.Ring_theory]
y:148 [binder, in Coq.FSets.FMapList]
y:148 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:148 [binder, in Coq.QArith.QArith_base]
y:1487 [binder, in Coq.FSets.FMapAVL]
y:149 [binder, in Coq.Reals.Rtrigo1]
y:149 [binder, in Coq.Reals.Ratan]
y:149 [binder, in Coq.Reals.SeqProp]
y:149 [binder, in Coq.Structures.OrdersFacts]
y:15 [binder, in Coq.Relations.Operators_Properties]
y:15 [binder, in Coq.Structures.OrdersEx]
y:15 [binder, in Coq.QArith.Qcabs]
y:15 [binder, in Coq.Arith.Bool_nat]
y:15 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
y:15 [binder, in Coq.Wellfounded.Lexicographic_Product]
y:15 [binder, in Coq.Program.Subset]
y:15 [binder, in Coq.micromega.ZifyBool]
y:15 [binder, in Coq.Reals.Rpower]
y:15 [binder, in Coq.Init.Logic_Type]
y:15 [binder, in Coq.Reals.Raxioms]
y:15 [binder, in Coq.ZArith.Zbool]
y:15 [binder, in Coq.Bool.BoolEq]
y:15 [binder, in Coq.Reals.PSeries_reg]
y:15 [binder, in Coq.Sets.Powerset_facts]
y:15 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]
y:15 [binder, in Coq.Numbers.HexadecimalQ]
y:15 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:15 [binder, in Coq.Structures.OrdersTac]
y:15 [binder, in Coq.micromega.ZifyInst]
y:15 [binder, in Coq.QArith.Qround]
y:15 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]
y:15 [binder, in Coq.Structures.OrdersFacts]
y:150 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:150 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:150 [binder, in Coq.Sorting.PermutSetoid]
y:150 [binder, in Coq.FSets.FMapFacts]
y:150 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:150 [binder, in Coq.Reals.Rtopology]
y:150 [binder, in Coq.setoid_ring.Ncring]
y:150 [binder, in Coq.QArith.QArith_base]
y:150 [binder, in Coq.Lists.SetoidList]
y:151 [binder, in Coq.Reals.Rtrigo1]
y:151 [binder, in Coq.FSets.FMapWeakList]
y:151 [binder, in Coq.Reals.Ratan]
y:151 [binder, in Coq.setoid_ring.Ring_theory]
y:152 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:152 [binder, in Coq.setoid_ring.InitialRing]
y:152 [binder, in Coq.Structures.OrderedTypeEx]
y:152 [binder, in Coq.FSets.FMapList]
y:152 [binder, in Coq.Structures.OrdersFacts]
y:153 [binder, in Coq.Logic.Eqdep_dec]
y:153 [binder, in Coq.Reals.Rtrigo1]
y:153 [binder, in Coq.MSets.MSetGenTree]
y:153 [binder, in Coq.Reals.Ratan]
y:153 [binder, in Coq.QArith.QArith_base]
y:154 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:154 [binder, in Coq.FSets.FMapFacts]
y:154 [binder, in Coq.Reals.Rpower]
y:155 [binder, in Coq.Reals.Rtrigo1]
y:155 [binder, in Coq.FSets.FMapFullAVL]
y:155 [binder, in Coq.Structures.OrdersFacts]
y:156 [binder, in Coq.Logic.EqdepFacts]
y:156 [binder, in Coq.Lists.ListSet]
y:156 [binder, in Coq.QArith.QArith_base]
y:156 [binder, in Coq.Lists.SetoidList]
y:157 [binder, in Coq.Reals.Rtrigo1]
y:157 [binder, in Coq.FSets.FMapFacts]
y:157 [binder, in Coq.Reals.Ratan]
y:157 [binder, in Coq.setoid_ring.Ring_theory]
y:157 [binder, in Coq.FSets.FMapList]
y:157 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:157 [binder, in Coq.Structures.OrdersFacts]
y:158 [binder, in Coq.Logic.Eqdep_dec]
y:158 [binder, in Coq.Logic.EqdepFacts]
y:158 [binder, in Coq.Reals.Rfunctions]
y:158 [binder, in Coq.MSets.MSetGenTree]
y:158 [binder, in Coq.QArith.QArith_base]
y:159 [binder, in Coq.FSets.FMapFullAVL]
y:159 [binder, in Coq.Structures.OrdersFacts]
y:16 [binder, in Coq.Structures.Orders]
y:16 [binder, in Coq.Program.Wf]
y:16 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:16 [binder, in Coq.QArith.Qcanon]
y:16 [binder, in Coq.nsatz.NsatzTactic]
y:16 [binder, in Coq.Logic.Eqdep_dec]
y:16 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
y:16 [binder, in Coq.Classes.RelationClasses]
y:16 [binder, in Coq.Reals.Binomial]
y:16 [binder, in Coq.Structures.OrdersAlt]
y:16 [binder, in Coq.Program.Subset]
y:16 [binder, in Coq.QArith.Qreals]
y:16 [binder, in Coq.Logic.ClassicalChoice]
y:16 [binder, in Coq.Logic.IndefiniteDescription]
y:16 [binder, in Coq.omega.OmegaLemmas]
y:16 [binder, in Coq.ZArith.Int]
y:16 [binder, in Coq.Strings.Ascii]
y:16 [binder, in Coq.Sets.Permut]
y:16 [binder, in Coq.Numbers.HexadecimalQ]
y:16 [binder, in Coq.omega.PreOmega]
y:16 [binder, in Coq.Classes.DecidableClass]
y:16 [binder, in Coq.Reals.RiemannInt_SF]
y:16 [binder, in Coq.micromega.ZCoeff]
y:16 [binder, in Coq.QArith.Qreduction]
y:16 [binder, in Coq.Floats.FloatAxioms]
Y:16 [binder, in Coq.Sets.Infinite_sets]
y:16 [binder, in Coq.Reals.ClassicalConstructiveReals]
y:16 [binder, in Coq.Sorting.Heap]
y:16 [binder, in Coq.Logic.FinFun]
y:160 [binder, in Coq.Logic.Eqdep_dec]
y:160 [binder, in Coq.FSets.FSetBridge]
y:160 [binder, in Coq.Logic.EqdepFacts]
y:160 [binder, in Coq.FSets.FMapFacts]
y:160 [binder, in Coq.setoid_ring.Ring_theory]
y:160 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:160 [binder, in Coq.QArith.QArith_base]
y:161 [binder, in Coq.omega.OmegaLemmas]
y:161 [binder, in Coq.MSets.MSetRBT]
y:161 [binder, in Coq.Structures.OrdersFacts]
y:162 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:162 [binder, in Coq.FSets.FMapAVL]
y:162 [binder, in Coq.QArith.QArith_base]
y:163 [binder, in Coq.Logic.EqdepFacts]
y:163 [binder, in Coq.FSets.FMapFacts]
y:163 [binder, in Coq.MSets.MSetGenTree]
y:163 [binder, in Coq.setoid_ring.Ring_theory]
y:163 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:164 [binder, in Coq.Reals.MVT]
y:164 [binder, in Coq.FSets.FMapFullAVL]
y:164 [binder, in Coq.Reals.Ratan]
y:164 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:165 [binder, in Coq.Reals.MVT]
y:165 [binder, in Coq.FSets.FSetInterface]
y:165 [binder, in Coq.omega.OmegaLemmas]
y:165 [binder, in Coq.Reals.Ratan]
y:166 [binder, in Coq.Reals.MVT]
y:166 [binder, in Coq.FSets.FMapFacts]
y:166 [binder, in Coq.FSets.FMapAVL]
y:166 [binder, in Coq.Reals.PSeries_reg]
y:166 [binder, in Coq.ZArith.Znumtheory]
y:167 [binder, in Coq.FSets.FSetBridge]
y:167 [binder, in Coq.Reals.MVT]
y:167 [binder, in Coq.Reals.Ratan]
y:167 [binder, in Coq.Reals.Ranalysis5]
y:167 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:168 [binder, in Coq.Reals.MVT]
y:168 [binder, in Coq.Reals.Rpower]
y:168 [binder, in Coq.Reals.PSeries_reg]
y:168 [binder, in Coq.setoid_ring.Ring_theory]
y:169 [binder, in Coq.Reals.MVT]
y:169 [binder, in Coq.FSets.FMapFacts]
y:169 [binder, in Coq.FSets.FMapFullAVL]
y:169 [binder, in Coq.omega.OmegaLemmas]
y:169 [binder, in Coq.Reals.PSeries_reg]
y:169 [binder, in Coq.Reals.Ratan]
y:169 [binder, in Coq.QArith.QArith_base]
y:17 [binder, in Coq.Program.Wf]
y:17 [binder, in Coq.Relations.Operators_Properties]
y:17 [binder, in Coq.Structures.OrdersLists]
y:17 [binder, in Coq.Sets.Relations_3]
y:17 [binder, in Coq.QArith.Qcabs]
y:17 [binder, in Coq.Arith.Bool_nat]
y:17 [binder, in Coq.ZArith.BinInt]
y:17 [binder, in Coq.Reals.Abstract.ConstructivePower]
y:17 [binder, in Coq.Logic.JMeq]
y:17 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
y:17 [binder, in Coq.micromega.ZifyBool]
y:17 [binder, in Coq.Reals.Rpower]
y:17 [binder, in Coq.Sets.Cpo]
y:17 [binder, in Coq.Structures.OrderedTypeEx]
y:17 [binder, in Coq.Logic.ClassicalUniqueChoice]
y:17 [binder, in Coq.Structures.OrderedTypeAlt]
y:17 [binder, in Coq.ZArith.Zbool]
y:17 [binder, in Coq.Structures.Equalities]
y:17 [binder, in Coq.Structures.OrderedType]
y:17 [binder, in Coq.Sets.Powerset_facts]
y:17 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]
y:17 [binder, in Coq.Sets.Relations_2]
y:17 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:17 [binder, in Coq.Logic.Diaconescu]
y:17 [binder, in Coq.Sets.Classical_sets]
y:17 [binder, in Coq.Reals.RiemannInt_SF]
y:17 [binder, in Coq.micromega.ZifyInst]
y:17 [binder, in Coq.QArith.Qround]
y:17 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:17 [binder, in Coq.Reals.Cos_rel]
Y:17 [binder, in Coq.Sets.Infinite_sets]
y:17 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]
y:17 [binder, in Coq.Structures.OrdersFacts]
y:170 [binder, in Coq.Reals.MVT]
y:170 [binder, in Coq.ssr.ssrfun]
y:170 [binder, in Coq.MSets.MSetGenTree]
y:170 [binder, in Coq.Reals.PSeries_reg]
y:170 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:171 [binder, in Coq.Reals.MVT]
y:171 [binder, in Coq.Reals.Rpower]
y:171 [binder, in Coq.FSets.FMapAVL]
y:171 [binder, in Coq.QArith.QArith_base]
y:172 [binder, in Coq.FSets.FMapFullAVL]
y:173 [binder, in Coq.setoid_ring.Field_theory]
y:174 [binder, in Coq.FSets.FSetBridge]
y:174 [binder, in Coq.Reals.Rpower]
y:175 [binder, in Coq.Vectors.VectorSpec]
y:175 [binder, in Coq.MSets.MSetGenTree]
y:175 [binder, in Coq.Reals.PSeries_reg]
y:176 [binder, in Coq.FSets.FMapFullAVL]
y:176 [binder, in Coq.setoid_ring.Ncring]
y:177 [binder, in Coq.FSets.FSetBridge]
y:177 [binder, in Coq.Reals.Rpower]
y:177 [binder, in Coq.Reals.PSeries_reg]
y:179 [binder, in Coq.FSets.FMapAVL]
y:179 [binder, in Coq.Vectors.Fin]
y:179 [binder, in Coq.setoid_ring.Ncring]
y:179 [binder, in Coq.QArith.QArith_base]
y:18 [binder, in Coq.Structures.Orders]
y:18 [binder, in Coq.QArith.Qcanon]
y:18 [binder, in Coq.nsatz.NsatzTactic]
y:18 [binder, in Coq.FSets.FSetBridge]
y:18 [binder, in Coq.Logic.EqdepFacts]
y:18 [binder, in Coq.Strings.String]
y:18 [binder, in Coq.Reals.R_sqrt]
y:18 [binder, in Coq.Structures.OrdersAlt]
y:18 [binder, in Coq.Init.Wf]
y:18 [binder, in Coq.QArith.Qreals]
y:18 [binder, in Coq.QArith.Qabs]
y:18 [binder, in Coq.Reals.Rdefinitions]
y:18 [binder, in Coq.omega.OmegaLemmas]
y:18 [binder, in Coq.Sets.Partial_Order]
y:18 [binder, in Coq.Structures.GenericMinMax]
y:18 [binder, in Coq.Sets.Relations_2]
y:18 [binder, in Coq.ssr.ssrunder]
y:18 [binder, in Coq.Classes.DecidableClass]
y:18 [binder, in Coq.ZArith.Znumtheory]
Y:18 [binder, in Coq.Sets.Infinite_sets]
y:18 [binder, in Coq.Relations.Relation_Operators]
y:18 [binder, in Coq.Bool.DecBool]
y:18 [binder, in Coq.Lists.SetoidList]
y:180 [binder, in Coq.FSets.FSetBridge]
y:180 [binder, in Coq.FSets.FSetInterface]
y:180 [binder, in Coq.Structures.OrderedType]
y:181 [binder, in Coq.ssr.ssrfun]
y:182 [binder, in Coq.ssr.ssrfun]
y:182 [binder, in Coq.Init.Logic]
y:182 [binder, in Coq.setoid_ring.Ncring]
y:182 [binder, in Coq.QArith.QArith_base]
y:184 [binder, in Coq.Logic.EqdepFacts]
y:184 [binder, in Coq.FSets.FMapAVL]
y:184 [binder, in Coq.Structures.OrderedType]
y:185 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:185 [binder, in Coq.FSets.FMapFacts]
y:185 [binder, in Coq.FSets.FSetInterface]
y:185 [binder, in Coq.Reals.Rpower]
y:186 [binder, in Coq.FSets.FSetBridge]
y:186 [binder, in Coq.omega.OmegaLemmas]
y:186 [binder, in Coq.Structures.GenericMinMax]
y:186 [binder, in Coq.setoid_ring.Ring_theory]
y:186 [binder, in Coq.micromega.ZMicromega]
y:186 [binder, in Coq.QArith.QArith_base]
y:186 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:187 [binder, in Coq.Reals.Rpower]
y:187 [binder, in Coq.Reals.Rtopology]
y:187 [binder, in Coq.setoid_ring.Ncring]
y:188 [binder, in Coq.micromega.RingMicromega]
y:188 [binder, in Coq.Init.Logic]
y:188 [binder, in Coq.QArith.QArith_base]
y:189 [binder, in Coq.FSets.FSetBridge]
y:189 [binder, in Coq.FSets.FMapAVL]
y:189 [binder, in Coq.Reals.Rtopology]
y:189 [binder, in Coq.Structures.GenericMinMax]
y:189 [binder, in Coq.Reals.PSeries_reg]
y:189 [binder, in Coq.Reals.Ranalysis5]
y:19 [binder, in Coq.Relations.Operators_Properties]
y:19 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:19 [binder, in Coq.Logic.Eqdep_dec]
y:19 [binder, in Coq.Sets.Constructive_sets]
y:19 [binder, in Coq.QArith.Qcabs]
y:19 [binder, in Coq.FSets.FMapFacts]
y:19 [binder, in Coq.Logic.ChoiceFacts]
y:19 [binder, in Coq.Wellfounded.Lexicographic_Product]
y:19 [binder, in Coq.micromega.ZifyBool]
y:19 [binder, in Coq.Reals.Rpower]
y:19 [binder, in Coq.Init.Logic_Type]
y:19 [binder, in Coq.ZArith.Int]
y:19 [binder, in Coq.micromega.QMicromega]
y:19 [binder, in Coq.Structures.OrderedTypeAlt]
y:19 [binder, in Coq.Classes.CRelationClasses]
y:19 [binder, in Coq.Reals.Rbasic_fun]
y:19 [binder, in Coq.Classes.SetoidClass]
y:19 [binder, in Coq.Bool.BoolEq]
y:19 [binder, in Coq.Logic.ProofIrrelevanceFacts]
y:19 [binder, in Coq.Reals.RList]
y:19 [binder, in Coq.Logic.Diaconescu]
Y:19 [binder, in Coq.Sets.Classical_sets]
y:19 [binder, in Coq.Program.Basics]
y:19 [binder, in Coq.micromega.ZifyInst]
y:19 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:19 [binder, in Coq.micromega.ZMicromega]
y:19 [binder, in Coq.Floats.FloatAxioms]
y:19 [binder, in Coq.Relations.Relation_Operators]
y:19 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]
y:19 [binder, in Coq.Structures.OrdersFacts]
y:190 [binder, in Coq.micromega.RingMicromega]
y:190 [binder, in Coq.omega.OmegaLemmas]
y:191 [binder, in Coq.Arith.PeanoNat]
y:191 [binder, in Coq.Reals.Rtopology]
y:191 [binder, in Coq.Reals.Ranalysis5]
y:191 [binder, in Coq.Lists.SetoidList]
y:191 [binder, in Coq.FSets.FSetCompat]
y:192 [binder, in Coq.FSets.FSetBridge]
y:192 [binder, in Coq.micromega.RingMicromega]
y:192 [binder, in Coq.Reals.PSeries_reg]
y:192 [binder, in Coq.QArith.QArith_base]
y:193 [binder, in Coq.ssr.ssrfun]
y:193 [binder, in Coq.Reals.Rtopology]
y:194 [binder, in Coq.micromega.RingMicromega]
y:194 [binder, in Coq.Reals.Rfunctions]
y:194 [binder, in Coq.Bool.Bool]
y:194 [binder, in Coq.omega.OmegaLemmas]
y:194 [binder, in Coq.Structures.GenericMinMax]
y:194 [binder, in Coq.Reals.Ranalysis5]
y:194 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:194 [binder, in Coq.QArith.QArith_base]
y:196 [binder, in Coq.FSets.FSetBridge]
y:196 [binder, in Coq.Reals.Rfunctions]
y:196 [binder, in Coq.FSets.FMapAVL]
y:196 [binder, in Coq.QArith.QArith_base]
y:197 [binder, in Coq.MSets.MSetList]
y:197 [binder, in Coq.Reals.Ranalysis5]
y:197 [binder, in Coq.FSets.FSetCompat]
y:198 [binder, in Coq.FSets.FSetBridge]
y:198 [binder, in Coq.Reals.Rfunctions]
y:198 [binder, in Coq.FSets.FMapPositive]
y:198 [binder, in Coq.QArith.QArith_base]
y:199 [binder, in Coq.FSets.FMapAVL]
y:199 [binder, in Coq.omega.OmegaLemmas]
y:199 [binder, in Coq.Structures.GenericMinMax]
y:199 [binder, in Coq.Reals.Ranalysis5]
y:2 [binder, in Coq.Reals.Rderiv]
y:2 [binder, in Coq.micromega.Ztac]
y:2 [binder, in Coq.Structures.DecidableTypeEx]
y:2 [binder, in Coq.Reals.Rminmax]
y:2 [binder, in Coq.Structures.OrdersEx]
y:2 [binder, in Coq.PArith.BinPos]
y:2 [binder, in Coq.ZArith.BinInt]
y:2 [binder, in Coq.ZArith.Zmax]
y:2 [binder, in Coq.Numbers.NatInt.NZBase]
y:2 [binder, in Coq.ZArith.Zmin]
y:2 [binder, in Coq.FSets.FMapFacts]
y:2 [binder, in Coq.Reals.Rsqrt_def]
y:2 [binder, in Coq.MSets.MSetFacts]
y:2 [binder, in Coq.QArith.Qfield]
y:2 [binder, in Coq.NArith.BinNat]
y:2 [binder, in Coq.Reals.Raxioms]
y:2 [binder, in Coq.ZArith.Zbool]
y:2 [binder, in Coq.Reals.Rbasic_fun]
y:2 [binder, in Coq.NArith.NArith]
y:2 [binder, in Coq.micromega.Fourier_util]
y:2 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]
y:2 [binder, in Coq.Unicode.Utf8_core]
y:2 [binder, in Coq.omega.PreOmega]
y:2 [binder, in Coq.Numbers.Integer.Binary.ZBinary]
y:2 [binder, in Coq.FSets.FSetFacts]
y:2 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]
y:2 [binder, in Coq.Structures.OrdersFacts]
y:2 [binder, in Coq.Reals.Cos_plus]
y:20 [binder, in Coq.Structures.Orders]
y:20 [binder, in Coq.Program.Wf]
y:20 [binder, in Coq.QArith.Qcanon]
y:20 [binder, in Coq.Structures.OrdersLists]
y:20 [binder, in Coq.Structures.OrdersEx]
y:20 [binder, in Coq.Reals.R_sqrt]
y:20 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:20 [binder, in Coq.Reals.Exp_prop]
y:20 [binder, in Coq.Structures.OrdersAlt]
y:20 [binder, in Coq.Reals.Rsqrt_def]
y:20 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:20 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:20 [binder, in Coq.omega.OmegaLemmas]
y:20 [binder, in Coq.Structures.OrderedTypeEx]
y:20 [binder, in Coq.Structures.Equalities]
y:20 [binder, in Coq.Strings.Ascii]
y:20 [binder, in Coq.Lists.ListSet]
y:20 [binder, in Coq.Sets.Permut]
y:20 [binder, in Coq.Sets.Powerset_facts]
y:20 [binder, in Coq.Sets.Powerset_Classical_facts]
y:20 [binder, in Coq.Sets.Multiset]
y:20 [binder, in Coq.Classes.DecidableClass]
y:20 [binder, in Coq.Sets.Image]
y:20 [binder, in Coq.Reals.R_sqr]
y:20 [binder, in Coq.Sorting.Heap]
y:20 [binder, in Coq.FSets.FSetCompat]
y:200 [binder, in Coq.Reals.Rfunctions]
y:200 [binder, in Coq.ssr.ssrfun]
y:200 [binder, in Coq.QArith.QArith_base]
y:201 [binder, in Coq.FSets.FMapFullAVL]
y:201 [binder, in Coq.Bool.Bool]
y:201 [binder, in Coq.Reals.Ranalysis5]
y:201 [binder, in Coq.Lists.SetoidList]
y:202 [binder, in Coq.QArith.QArith_base]
y:203 [binder, in Coq.Reals.Rfunctions]
y:203 [binder, in Coq.Reals.Rtopology]
y:203 [binder, in Coq.Reals.PSeries_reg]
y:203 [binder, in Coq.FSets.FSetCompat]
y:204 [binder, in Coq.Logic.EqdepFacts]
y:204 [binder, in Coq.MSets.MSetList]
y:204 [binder, in Coq.Reals.Ranalysis5]
y:204 [binder, in Coq.Lists.SetoidList]
y:205 [binder, in Coq.FSets.FMapWeakList]
y:205 [binder, in Coq.QArith.QArith_base]
y:206 [binder, in Coq.Logic.ChoiceFacts]
y:206 [binder, in Coq.omega.OmegaLemmas]
y:206 [binder, in Coq.Structures.GenericMinMax]
y:206 [binder, in Coq.Reals.PSeries_reg]
y:207 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:207 [binder, in Coq.ssr.ssrfun]
y:207 [binder, in Coq.MSets.MSetPositive]
y:207 [binder, in Coq.Reals.Ranalysis5]
y:207 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:208 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:208 [binder, in Coq.Logic.ChoiceFacts]
y:208 [binder, in Coq.MSets.MSetRBT]
y:208 [binder, in Coq.Reals.Rtopology]
y:208 [binder, in Coq.Reals.PSeries_reg]
y:208 [binder, in Coq.QArith.QArith_base]
y:209 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:209 [binder, in Coq.FSets.FMapWeakList]
y:209 [binder, in Coq.Reals.Ranalysis5]
y:209 [binder, in Coq.setoid_ring.Ring_theory]
y:209 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:21 [binder, in Coq.Program.Wf]
y:21 [binder, in Coq.Relations.Operators_Properties]
y:21 [binder, in Coq.Logic.Eqdep_dec]
y:21 [binder, in Coq.Sets.Constructive_sets]
y:21 [binder, in Coq.Classes.RelationClasses]
y:21 [binder, in Coq.Logic.JMeq]
y:21 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
y:21 [binder, in Coq.Wellfounded.Lexicographic_Product]
y:21 [binder, in Coq.micromega.ZifyBool]
y:21 [binder, in Coq.QArith.Qreals]
y:21 [binder, in Coq.QArith.Qabs]
y:21 [binder, in Coq.Reals.Rdefinitions]
y:21 [binder, in Coq.micromega.QMicromega]
y:21 [binder, in Coq.Sets.Partial_Order]
y:21 [binder, in Coq.Structures.OrderedTypeAlt]
y:21 [binder, in Coq.Structures.OrderedType]
y:21 [binder, in Coq.Reals.Rbasic_fun]
y:21 [binder, in Coq.Classes.SetoidDec]
y:21 [binder, in Coq.Strings.Byte]
y:21 [binder, in Coq.Lists.ListSet]
y:21 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:21 [binder, in Coq.Reals.RList]
y:21 [binder, in Coq.Logic.Diaconescu]
Y:21 [binder, in Coq.Sets.Classical_sets]
y:21 [binder, in Coq.Structures.OrdersTac]
y:21 [binder, in Coq.micromega.ZifyInst]
y:21 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:21 [binder, in Coq.micromega.ZMicromega]
y:21 [binder, in Coq.micromega.ZCoeff]
y:21 [binder, in Coq.Structures.OrdersFacts]
y:210 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:210 [binder, in Coq.MSets.MSetPositive]
y:210 [binder, in Coq.Reals.Rtopology]
y:210 [binder, in Coq.Reals.PSeries_reg]
y:211 [binder, in Coq.Structures.GenericMinMax]
y:211 [binder, in Coq.Reals.PSeries_reg]
y:211 [binder, in Coq.Reals.Ranalysis5]
y:211 [binder, in Coq.setoid_ring.Ring_theory]
y:211 [binder, in Coq.FSets.FMapList]
y:211 [binder, in Coq.QArith.QArith_base]
y:212 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:212 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:212 [binder, in Coq.MSets.MSetPositive]
y:212 [binder, in Coq.Reals.Rtopology]
y:212 [binder, in Coq.setoid_ring.Ncring]
y:213 [binder, in Coq.ssr.ssrfun]
y:213 [binder, in Coq.MSets.MSetRBT]
y:213 [binder, in Coq.Reals.PSeries_reg]
y:213 [binder, in Coq.Reals.Ranalysis5]
y:213 [binder, in Coq.setoid_ring.Ring_theory]
y:213 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:213 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:213 [binder, in Coq.micromega.ZMicromega]
y:213 [binder, in Coq.QArith.QArith_base]
y:214 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:214 [binder, in Coq.Reals.Ranalysis1]
y:214 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:214 [binder, in Coq.Logic.ChoiceFacts]
y:214 [binder, in Coq.Reals.Rtopology]
y:214 [binder, in Coq.FSets.FMapWeakList]
y:214 [binder, in Coq.setoid_ring.Ncring]
y:215 [binder, in Coq.Reals.Ranalysis1]
y:215 [binder, in Coq.ssr.ssrfun]
y:215 [binder, in Coq.Reals.Rtopology]
y:215 [binder, in Coq.Reals.Ranalysis5]
y:215 [binder, in Coq.setoid_ring.Ring_theory]
y:215 [binder, in Coq.FSets.FMapList]
y:215 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:215 [binder, in Coq.QArith.QArith_base]
y:215 [binder, in Coq.Lists.SetoidList]
y:216 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:216 [binder, in Coq.Reals.Ranalysis1]
y:216 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:216 [binder, in Coq.Logic.ChoiceFacts]
y:216 [binder, in Coq.Reals.Rtopology]
y:216 [binder, in Coq.Structures.GenericMinMax]
y:216 [binder, in Coq.setoid_ring.Ncring]
y:217 [binder, in Coq.Reals.Ranalysis1]
y:217 [binder, in Coq.ssr.ssrfun]
y:217 [binder, in Coq.Reals.Ranalysis5]
y:217 [binder, in Coq.setoid_ring.Ring_theory]
y:217 [binder, in Coq.QArith.QArith_base]
y:218 [binder, in Coq.Reals.Ranalysis1]
y:218 [binder, in Coq.Logic.ChoiceFacts]
y:218 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:218 [binder, in Coq.Lists.SetoidList]
y:219 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:219 [binder, in Coq.Reals.Ranalysis1]
y:219 [binder, in Coq.ssr.ssrfun]
y:219 [binder, in Coq.FSets.FMapWeakList]
y:219 [binder, in Coq.Structures.GenericMinMax]
y:219 [binder, in Coq.Reals.Ranalysis5]
y:219 [binder, in Coq.QArith.QArith_base]
y:22 [binder, in Coq.Structures.Orders]
y:22 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:22 [binder, in Coq.QArith.Qcanon]
y:22 [binder, in Coq.QArith.Qcabs]
y:22 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:22 [binder, in Coq.Arith.Wf_nat]
y:22 [binder, in Coq.FSets.FMapFacts]
y:22 [binder, in Coq.Structures.OrdersAlt]
y:22 [binder, in Coq.Logic.Hurkens]
y:22 [binder, in Coq.Sets.Cpo]
y:22 [binder, in Coq.Structures.OrderedTypeEx]
y:22 [binder, in Coq.ZArith.Int]
y:22 [binder, in Coq.Structures.Equalities]
y:22 [binder, in Coq.Structures.GenericMinMax]
y:22 [binder, in Coq.Reals.Rlimit]
y:22 [binder, in Coq.Sets.Powerset_facts]
Y:22 [binder, in Coq.Sets.Powerset_Classical_facts]
y:22 [binder, in Coq.Classes.DecidableClass]
y:22 [binder, in Coq.Reals.R_sqr]
y:22 [binder, in Coq.Floats.FloatAxioms]
y:22 [binder, in Coq.Reals.Cos_rel]
Y:22 [binder, in Coq.Sets.Infinite_sets]
y:220 [binder, in Coq.Reals.Ranalysis1]
y:220 [binder, in Coq.Lists.List]
y:220 [binder, in Coq.setoid_ring.Ring_theory]
y:220 [binder, in Coq.FSets.FMapList]
y:221 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:221 [binder, in Coq.Logic.ChoiceFacts]
y:221 [binder, in Coq.Reals.Ranalysis5]
y:221 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:221 [binder, in Coq.QArith.QArith_base]
y:222 [binder, in Coq.Reals.Ranalysis1]
y:222 [binder, in Coq.Structures.GenericMinMax]
y:223 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:223 [binder, in Coq.Reals.Ranalysis5]
y:223 [binder, in Coq.QArith.QArith_base]
y:224 [binder, in Coq.Reals.Ranalysis1]
y:224 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:224 [binder, in Coq.setoid_ring.Ncring]
y:224 [binder, in Coq.Lists.SetoidList]
y:225 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:225 [binder, in Coq.ssr.ssrfun]
y:225 [binder, in Coq.Structures.GenericMinMax]
y:226 [binder, in Coq.Reals.Ranalysis1]
y:226 [binder, in Coq.Logic.ChoiceFacts]
y:226 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:227 [binder, in Coq.ssr.ssrfun]
y:227 [binder, in Coq.Reals.Ranalysis5]
y:227 [binder, in Coq.setoid_ring.Ncring]
y:227 [binder, in Coq.Lists.SetoidList]
y:228 [binder, in Coq.Reals.Ranalysis1]
y:228 [binder, in Coq.Logic.ChoiceFacts]
y:228 [binder, in Coq.ZArith.Znat]
y:228 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:229 [binder, in Coq.Reals.Ranalysis1]
y:229 [binder, in Coq.ssr.ssrfun]
y:23 [binder, in Coq.Relations.Operators_Properties]
y:23 [binder, in Coq.Logic.Eqdep_dec]
y:23 [binder, in Coq.Structures.OrdersLists]
y:23 [binder, in Coq.ZArith.BinIntDef]
y:23 [binder, in Coq.Reals.Rtrigo_reg]
Y:23 [binder, in Coq.Sets.Finite_sets_facts]
y:23 [binder, in Coq.Logic.EqdepFacts]
y:23 [binder, in Coq.Reals.R_sqrt]
y:23 [binder, in Coq.Reals.Abstract.ConstructivePower]
y:23 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:23 [binder, in Coq.micromega.ZifyBool]
y:23 [binder, in Coq.QArith.Qabs]
y:23 [binder, in Coq.Reals.Rpower]
y:23 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:23 [binder, in Coq.omega.OmegaLemmas]
y:23 [binder, in Coq.Classes.CMorphisms]
y:23 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:23 [binder, in Coq.micromega.QMicromega]
y:23 [binder, in Coq.Structures.OrderedTypeAlt]
y:23 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
y:23 [binder, in Coq.Reals.Rbasic_fun]
y:23 [binder, in Coq.Bool.BoolEq]
y:23 [binder, in Coq.Lists.ListSet]
y:23 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:23 [binder, in Coq.Sets.Multiset]
y:23 [binder, in Coq.Logic.Diaconescu]
y:23 [binder, in Coq.micromega.ZifyInst]
y:23 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:23 [binder, in Coq.micromega.ZCoeff]
y:23 [binder, in Coq.Structures.OrdersFacts]
y:230 [binder, in Coq.Reals.Ranalysis1]
y:230 [binder, in Coq.Logic.ChoiceFacts]
y:230 [binder, in Coq.Lists.SetoidList]
y:231 [binder, in Coq.Reals.Ranalysis1]
y:231 [binder, in Coq.ssr.ssrfun]
y:231 [binder, in Coq.Reals.Ranalysis5]
y:232 [binder, in Coq.Logic.ChoiceFacts]
y:233 [binder, in Coq.ssr.ssrfun]
y:233 [binder, in Coq.QArith.QArith_base]
y:234 [binder, in Coq.MSets.MSetProperties]
y:234 [binder, in Coq.ssr.ssrfun]
y:234 [binder, in Coq.Reals.Ranalysis5]
y:234 [binder, in Coq.FSets.FSetProperties]
y:235 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:235 [binder, in Coq.Logic.EqdepFacts]
y:235 [binder, in Coq.FSets.FSetPositive]
y:235 [binder, in Coq.setoid_ring.Ring_theory]
y:236 [binder, in Coq.MSets.MSetProperties]
y:236 [binder, in Coq.Logic.ChoiceFacts]
y:236 [binder, in Coq.FSets.FMapFullAVL]
y:236 [binder, in Coq.MSets.MSetRBT]
y:236 [binder, in Coq.FSets.FSetProperties]
y:237 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:237 [binder, in Coq.Logic.EqdepFacts]
y:237 [binder, in Coq.Lists.List]
y:237 [binder, in Coq.Reals.Ranalysis5]
y:237 [binder, in Coq.setoid_ring.Ring_theory]
y:237 [binder, in Coq.QArith.QArith_base]
y:237 [binder, in Coq.Lists.SetoidList]
y:238 [binder, in Coq.Logic.ChoiceFacts]
y:239 [binder, in Coq.FSets.FSetPositive]
y:239 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:24 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:24 [binder, in Coq.QArith.Qcabs]
y:24 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:24 [binder, in Coq.Classes.Morphisms]
y:24 [binder, in Coq.Structures.OrdersAlt]
y:24 [binder, in Coq.Reals.Rsqrt_def]
y:24 [binder, in Coq.Wellfounded.Lexicographic_Product]
y:24 [binder, in Coq.Init.Wf]
y:24 [binder, in Coq.QArith.Qreals]
y:24 [binder, in Coq.Structures.OrderedTypeEx]
y:24 [binder, in Coq.Classes.EquivDec]
y:24 [binder, in Coq.Structures.Equalities]
y:24 [binder, in Coq.Structures.GenericMinMax]
y:24 [binder, in Coq.Sets.Permut]
y:24 [binder, in Coq.Reals.RList]
y:24 [binder, in Coq.Sets.Image]
y:24 [binder, in Coq.Structures.OrdersTac]
y:24 [binder, in Coq.Reals.R_sqr]
y:24 [binder, in Coq.micromega.ZMicromega]
y:240 [binder, in Coq.Lists.List]
y:240 [binder, in Coq.Logic.ChoiceFacts]
y:240 [binder, in Coq.Reals.Ranalysis5]
y:241 [binder, in Coq.ssr.ssrfun]
y:241 [binder, in Coq.QArith.QArith_base]
y:242 [binder, in Coq.MSets.MSetProperties]
y:242 [binder, in Coq.Logic.ChoiceFacts]
y:242 [binder, in Coq.FSets.FSetPositive]
y:242 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:242 [binder, in Coq.FSets.FSetProperties]
y:243 [binder, in Coq.Lists.List]
y:243 [binder, in Coq.ssr.ssrfun]
y:243 [binder, in Coq.Structures.GenericMinMax]
y:244 [binder, in Coq.MSets.MSetProperties]
y:244 [binder, in Coq.Logic.ChoiceFacts]
y:244 [binder, in Coq.Sorting.Permutation]
y:244 [binder, in Coq.FSets.FSetProperties]
y:244 [binder, in Coq.QArith.QArith_base]
y:245 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:245 [binder, in Coq.Logic.ChoiceFacts]
y:245 [binder, in Coq.ssr.ssrfun]
y:245 [binder, in Coq.FSets.FSetPositive]
y:245 [binder, in Coq.MSets.MSetRBT]
y:245 [binder, in Coq.MSets.MSetGenTree]
y:245 [binder, in Coq.Structures.GenericMinMax]
y:247 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:247 [binder, in Coq.Logic.ChoiceFacts]
y:247 [binder, in Coq.ssr.ssrfun]
y:247 [binder, in Coq.FSets.FSetPositive]
y:247 [binder, in Coq.QArith.QArith_base]
y:248 [binder, in Coq.Logic.ChoiceFacts]
y:248 [binder, in Coq.Reals.Rtopology]
y:249 [binder, in Coq.Logic.EqdepFacts]
y:249 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:249 [binder, in Coq.ssr.ssrfun]
y:25 [binder, in Coq.Program.Wf]
y:25 [binder, in Coq.Relations.Operators_Properties]
y:25 [binder, in Coq.Reals.Rtrigo_reg]
y:25 [binder, in Coq.Reals.MVT]
y:25 [binder, in Coq.Reals.R_sqrt]
y:25 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
y:25 [binder, in Coq.Wellfounded.Lexicographic_Product]
y:25 [binder, in Coq.micromega.ZifyBool]
y:25 [binder, in Coq.QArith.Qabs]
y:25 [binder, in Coq.Reals.Rpower]
y:25 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:25 [binder, in Coq.Structures.OrderedTypeAlt]
y:25 [binder, in Coq.Structures.OrderedType]
y:25 [binder, in Coq.Reals.Rbasic_fun]
y:25 [binder, in Coq.Reals.Rlimit]
y:25 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:25 [binder, in Coq.micromega.ZCoeff]
y:25 [binder, in Coq.QArith.Qreduction]
y:25 [binder, in Coq.Reals.Cos_rel]
y:25 [binder, in Coq.Structures.OrdersFacts]
y:250 [binder, in Coq.Logic.ChoiceFacts]
y:250 [binder, in Coq.ssr.ssrfun]
y:250 [binder, in Coq.QArith.QArith_base]
y:251 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:251 [binder, in Coq.FSets.FSetPositive]
y:251 [binder, in Coq.Reals.Rtopology]
y:252 [binder, in Coq.Logic.ChoiceFacts]
y:252 [binder, in Coq.MSets.MSetGenTree]
y:252 [binder, in Coq.Init.Logic]
y:253 [binder, in Coq.QArith.QArith_base]
y:253 [binder, in Coq.Lists.SetoidList]
y:254 [binder, in Coq.MSets.MSetProperties]
y:254 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:254 [binder, in Coq.FSets.FSetInterface]
y:254 [binder, in Coq.FSets.FSetPositive]
y:254 [binder, in Coq.MSets.MSetRBT]
y:254 [binder, in Coq.Reals.Ranalysis5]
y:254 [binder, in Coq.setoid_ring.Ring_theory]
y:254 [binder, in Coq.FSets.FSetProperties]
y:254 [binder, in Coq.Lists.SetoidList]
y:255 [binder, in Coq.Lists.SetoidList]
y:256 [binder, in Coq.Logic.ChoiceFacts]
y:256 [binder, in Coq.Reals.Rtopology]
y:256 [binder, in Coq.Init.Logic]
y:256 [binder, in Coq.QArith.QArith_base]
y:256 [binder, in Coq.Lists.SetoidList]
y:257 [binder, in Coq.Logic.EqdepFacts]
y:257 [binder, in Coq.MSets.MSetProperties]
y:257 [binder, in Coq.FSets.FSetPositive]
y:257 [binder, in Coq.FSets.FSetProperties]
y:258 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:258 [binder, in Coq.Logic.ChoiceFacts]
y:258 [binder, in Coq.FSets.FSetInterface]
y:258 [binder, in Coq.Reals.Ratan]
y:258 [binder, in Coq.setoid_ring.Ring_theory]
y:258 [binder, in Coq.micromega.ZMicromega]
y:259 [binder, in Coq.FSets.FMapFacts]
y:259 [binder, in Coq.FSets.FSetPositive]
y:259 [binder, in Coq.Reals.Rtopology]
y:259 [binder, in Coq.QArith.QArith_base]
y:26 [binder, in Coq.Structures.Orders]
y:26 [binder, in Coq.Program.Wf]
y:26 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:26 [binder, in Coq.setoid_ring.Ncring_initial]
y:26 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:26 [binder, in Coq.QArith.Qcabs]
y:26 [binder, in Coq.Classes.RelationClasses]
y:26 [binder, in Coq.Reals.MVT]
y:26 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:26 [binder, in Coq.Arith.Wf_nat]
y:26 [binder, in Coq.Logic.JMeq]
y:26 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:26 [binder, in Coq.Reals.Rdefinitions]
y:26 [binder, in Coq.Sets.Cpo]
y:26 [binder, in Coq.Arith.PeanoNat]
y:26 [binder, in Coq.omega.OmegaLemmas]
y:26 [binder, in Coq.Structures.OrderedTypeEx]
y:26 [binder, in Coq.Structures.Equalities]
y:26 [binder, in Coq.Bool.BoolEq]
y:26 [binder, in Coq.Classes.SetoidDec]
y:26 [binder, in Coq.Structures.GenericMinMax]
y:26 [binder, in Coq.Reals.PSeries_reg]
y:26 [binder, in Coq.Reals.R_sqr]
y:26 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:26 [binder, in Coq.Relations.Relation_Operators]
y:260 [binder, in Coq.Init.Logic]
y:260 [binder, in Coq.Logic.ClassicalFacts]
y:260 [binder, in Coq.micromega.Tauto]
y:261 [binder, in Coq.Logic.ChoiceFacts]
y:261 [binder, in Coq.FSets.FSetPositive]
y:262 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:262 [binder, in Coq.Sorting.Permutation]
y:262 [binder, in Coq.MSets.MSetRBT]
y:262 [binder, in Coq.QArith.QArith_base]
y:264 [binder, in Coq.Lists.List]
y:264 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:264 [binder, in Coq.MSets.MSetList]
y:264 [binder, in Coq.Reals.Rtopology]
y:264 [binder, in Coq.setoid_ring.Ring_theory]
y:264 [binder, in Coq.Init.Logic]
y:265 [binder, in Coq.Logic.EqdepFacts]
y:265 [binder, in Coq.setoid_ring.Ncring_tac]
y:265 [binder, in Coq.ssr.ssrfun]
y:265 [binder, in Coq.micromega.Tauto]
y:265 [binder, in Coq.QArith.QArith_base]
y:266 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:266 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:266 [binder, in Coq.Lists.SetoidList]
y:267 [binder, in Coq.Lists.List]
y:267 [binder, in Coq.MSets.MSetList]
y:267 [binder, in Coq.Reals.Rtopology]
y:267 [binder, in Coq.setoid_ring.Ring_theory]
y:268 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:268 [binder, in Coq.Init.Logic]
y:268 [binder, in Coq.micromega.ZMicromega]
y:268 [binder, in Coq.QArith.QArith_base]
y:27 [binder, in Coq.Relations.Operators_Properties]
y:27 [binder, in Coq.Sets.Constructive_sets]
y:27 [binder, in Coq.Reals.R_sqrt]
y:27 [binder, in Coq.Structures.OrdersAlt]
y:27 [binder, in Coq.setoid_ring.InitialRing]
y:27 [binder, in Coq.micromega.ZifyBool]
y:27 [binder, in Coq.Structures.OrderedTypeAlt]
y:27 [binder, in Coq.Classes.CRelationClasses]
y:27 [binder, in Coq.Reals.Rbasic_fun]
y:27 [binder, in Coq.Logic.HLevels]
y:27 [binder, in Coq.Lists.ListSet]
y:27 [binder, in Coq.Sets.Permut]
y:27 [binder, in Coq.Logic.ClassicalDescription]
y:27 [binder, in Coq.Reals.RList]
y:27 [binder, in Coq.Sets.Image]
y:27 [binder, in Coq.Structures.OrdersTac]
y:27 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:27 [binder, in Coq.micromega.ZCoeff]
y:27 [binder, in Coq.Floats.FloatAxioms]
y:27 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:27 [binder, in Coq.Structures.OrdersFacts]
y:270 [binder, in Coq.setoid_ring.Field_theory]
y:270 [binder, in Coq.ssr.ssrfun]
y:270 [binder, in Coq.MSets.MSetRBT]
y:270 [binder, in Coq.setoid_ring.Ring_theory]
y:271 [binder, in Coq.Logic.ChoiceFacts]
y:271 [binder, in Coq.QArith.QArith_base]
y:272 [binder, in Coq.Logic.EqdepFacts]
y:272 [binder, in Coq.Init.Logic]
y:273 [binder, in Coq.Lists.List]
y:273 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:273 [binder, in Coq.Logic.ChoiceFacts]
y:273 [binder, in Coq.setoid_ring.Field_theory]
y:273 [binder, in Coq.ssr.ssrfun]
y:273 [binder, in Coq.MSets.MSetGenTree]
y:273 [binder, in Coq.setoid_ring.Ring_theory]
y:274 [binder, in Coq.Lists.SetoidList]
y:275 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:275 [binder, in Coq.MSets.MSetRBT]
y:276 [binder, in Coq.setoid_ring.Field_theory]
y:276 [binder, in Coq.setoid_ring.Ring_theory]
y:278 [binder, in Coq.Init.Specif]
y:278 [binder, in Coq.ssr.ssrfun]
y:279 [binder, in Coq.MSets.MSetPositive]
y:279 [binder, in Coq.setoid_ring.Ring_theory]
y:28 [binder, in Coq.setoid_ring.Ncring_initial]
y:28 [binder, in Coq.ZArith.BinIntDef]
y:28 [binder, in Coq.Reals.Rfunctions]
y:28 [binder, in Coq.Lists.List]
y:28 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:28 [binder, in Coq.ZArith.Wf_Z]
y:28 [binder, in Coq.Reals.Rsqrt_def]
y:28 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:28 [binder, in Coq.Logic.ChoiceFacts]
y:28 [binder, in Coq.Arith.PeanoNat]
y:28 [binder, in Coq.Structures.Equalities]
y:28 [binder, in Coq.Reals.Rtopology]
y:28 [binder, in Coq.Structures.OrderedType]
y:28 [binder, in Coq.Bool.BoolEq]
y:28 [binder, in Coq.Structures.GenericMinMax]
y:28 [binder, in Coq.Reals.Rlimit]
y:28 [binder, in Coq.Reals.R_sqr]
y:28 [binder, in Coq.ZArith.Znumtheory]
y:28 [binder, in Coq.Relations.Relation_Definitions]
Y:28 [binder, in Coq.Sets.Infinite_sets]
y:280 [binder, in Coq.Strings.Byte]
y:280 [binder, in Coq.Reals.Ratan]
y:281 [binder, in Coq.Logic.ChoiceFacts]
y:281 [binder, in Coq.ssr.ssrfun]
y:282 [binder, in Coq.Reals.Ranalysis1]
y:282 [binder, in Coq.setoid_ring.Field_theory]
y:283 [binder, in Coq.Reals.Ranalysis1]
y:283 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:283 [binder, in Coq.Logic.ChoiceFacts]
y:284 [binder, in Coq.Reals.Ranalysis1]
y:285 [binder, in Coq.Reals.Ranalysis1]
y:285 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:285 [binder, in Coq.MSets.MSetPositive]
y:285 [binder, in Coq.Init.Logic]
y:286 [binder, in Coq.Reals.Ranalysis1]
y:286 [binder, in Coq.MSets.MSetRBT]
y:286 [binder, in Coq.Reals.Ranalysis5]
y:286 [binder, in Coq.setoid_ring.Ring_theory]
y:287 [binder, in Coq.Reals.Ranalysis1]
y:287 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:288 [binder, in Coq.Reals.Ranalysis1]
y:288 [binder, in Coq.Reals.Rtopology]
y:288 [binder, in Coq.Reals.Ranalysis5]
y:289 [binder, in Coq.Reals.Ranalysis1]
y:29 [binder, in Coq.Structures.Orders]
y:29 [binder, in Coq.Relations.Operators_Properties]
y:29 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:29 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:29 [binder, in Coq.Reals.Ranalysis4]
y:29 [binder, in Coq.micromega.RingMicromega]
y:29 [binder, in Coq.Reals.Rfunctions]
y:29 [binder, in Coq.Sets.Ensembles]
y:29 [binder, in Coq.Reals.R_sqrt]
y:29 [binder, in Coq.Init.Wf]
y:29 [binder, in Coq.setoid_ring.InitialRing]
y:29 [binder, in Coq.Reals.Rdefinitions]
y:29 [binder, in Coq.Program.Equality]
y:29 [binder, in Coq.omega.OmegaLemmas]
y:29 [binder, in Coq.Structures.OrderedTypeEx]
y:29 [binder, in Coq.Sets.Relations_2_facts]
y:29 [binder, in Coq.ZArith.ZArith_dec]
y:29 [binder, in Coq.Logic.ClassicalDescription]
y:29 [binder, in Coq.Sets.Image]
y:29 [binder, in Coq.Reals.Rgeom]
y:29 [binder, in Coq.Structures.OrdersFacts]
y:290 [binder, in Coq.Reals.Ranalysis1]
y:290 [binder, in Coq.Strings.Byte]
y:290 [binder, in Coq.Reals.Ranalysis5]
y:291 [binder, in Coq.Reals.Ranalysis1]
y:291 [binder, in Coq.Logic.ChoiceFacts]
y:291 [binder, in Coq.MSets.MSetPositive]
y:293 [binder, in Coq.MSets.MSetInterface]
y:293 [binder, in Coq.Logic.ChoiceFacts]
y:293 [binder, in Coq.Reals.Ranalysis5]
y:294 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:294 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:294 [binder, in Coq.Reals.Rtopology]
y:296 [binder, in Coq.MSets.MSetInterface]
y:296 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:296 [binder, in Coq.MSets.MSetPositive]
y:296 [binder, in Coq.Reals.Ranalysis5]
y:297 [binder, in Coq.MSets.MSetRBT]
y:297 [binder, in Coq.FSets.FMapPositive]
y:298 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:298 [binder, in Coq.ssr.ssrbool]
y:298 [binder, in Coq.Reals.Rtopology]
y:299 [binder, in Coq.Reals.Ranalysis5]
y:3 [binder, in Coq.Sorting.PermutEq]
y:3 [binder, in Coq.Logic.Eqdep_dec]
y:3 [binder, in Coq.Structures.OrdersLists]
y:3 [binder, in Coq.Arith.Bool_nat]
y:3 [binder, in Coq.ZArith.Zwf]
y:3 [binder, in Coq.Lists.ListDec]
y:3 [binder, in Coq.Reals.Rpower]
y:3 [binder, in Coq.Structures.GenericMinMax]
y:3 [binder, in Coq.Lists.ListSet]
y:3 [binder, in Coq.Reals.PSeries_reg]
y:3 [binder, in Coq.micromega.RMicromega]
y:3 [binder, in Coq.Reals.R_sqr]
y:3 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:3 [binder, in Coq.Program.Utils]
y:30 [binder, in Coq.Logic.EqdepFacts]
y:30 [binder, in Coq.Reals.Rfunctions]
y:30 [binder, in Coq.Arith.Wf_nat]
y:30 [binder, in Coq.Logic.JMeq]
y:30 [binder, in Coq.Structures.OrdersAlt]
y:30 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:30 [binder, in Coq.Reals.Rpower]
y:30 [binder, in Coq.Arith.PeanoNat]
y:30 [binder, in Coq.Classes.CMorphisms]
y:30 [binder, in Coq.Classes.EquivDec]
y:30 [binder, in Coq.Sets.Uniset]
y:30 [binder, in Coq.Structures.OrderedTypeAlt]
y:30 [binder, in Coq.Reals.Rbasic_fun]
y:30 [binder, in Coq.Structures.GenericMinMax]
y:30 [binder, in Coq.Sets.Multiset]
y:30 [binder, in Coq.Structures.OrdersTac]
y:30 [binder, in Coq.Reals.R_sqr]
y:30 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:300 [binder, in Coq.MSets.MSetInterface]
y:300 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:302 [binder, in Coq.Reals.Ranalysis1]
y:302 [binder, in Coq.MSets.MSetInterface]
y:302 [binder, in Coq.Reals.Ranalysis5]
y:303 [binder, in Coq.Reals.Ranalysis1]
y:303 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:304 [binder, in Coq.Reals.Ranalysis1]
y:304 [binder, in Coq.FSets.FSetBridge]
y:304 [binder, in Coq.Reals.Rtopology]
y:305 [binder, in Coq.Reals.Ranalysis5]
y:305 [binder, in Coq.Init.Logic]
y:306 [binder, in Coq.ssr.ssrbool]
y:307 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:307 [binder, in Coq.MSets.MSetRBT]
y:307 [binder, in Coq.MSets.MSetPositive]
y:308 [binder, in Coq.MSets.MSetInterface]
y:308 [binder, in Coq.Logic.ChoiceFacts]
y:309 [binder, in Coq.Reals.Ranalysis1]
y:31 [binder, in Coq.Program.Wf]
y:31 [binder, in Coq.Relations.Operators_Properties]
y:31 [binder, in Coq.setoid_ring.Ncring_initial]
y:31 [binder, in Coq.Reals.Ranalysis4]
y:31 [binder, in Coq.Reals.Rfunctions]
y:31 [binder, in Coq.Reals.R_sqrt]
y:31 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:31 [binder, in Coq.Classes.Morphisms]
y:31 [binder, in Coq.Reals.Rdefinitions]
y:31 [binder, in Coq.Sets.Cpo]
y:31 [binder, in Coq.Structures.OrderedTypeEx]
y:31 [binder, in Coq.Structures.Equalities]
y:31 [binder, in Coq.Structures.OrderedType]
y:31 [binder, in Coq.ZArith.ZArith_dec]
y:31 [binder, in Coq.Classes.SetoidDec]
y:31 [binder, in Coq.Reals.Rlimit]
y:31 [binder, in Coq.Numbers.NatInt.NZOrder]
y:31 [binder, in Coq.Logic.HLevels]
y:31 [binder, in Coq.Sets.Permut]
y:31 [binder, in Coq.Logic.ClassicalDescription]
y:31 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:31 [binder, in Coq.Sets.Image]
y:310 [binder, in Coq.Reals.Ranalysis1]
y:310 [binder, in Coq.Lists.List]
y:310 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:310 [binder, in Coq.Logic.ChoiceFacts]
y:310 [binder, in Coq.ssr.ssrbool]
y:311 [binder, in Coq.Reals.Ranalysis1]
y:311 [binder, in Coq.Reals.Ratan]
y:313 [binder, in Coq.Lists.List]
y:313 [binder, in Coq.MSets.MSetRBT]
y:313 [binder, in Coq.MSets.MSetPositive]
y:314 [binder, in Coq.MSets.MSetInterface]
y:316 [binder, in Coq.MSets.MSetRBT]
y:316 [binder, in Coq.Init.Logic]
y:317 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:319 [binder, in Coq.MSets.MSetPositive]
y:32 [binder, in Coq.Structures.Orders]
y:32 [binder, in Coq.Program.Wf]
y:32 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:32 [binder, in Coq.Sets.Constructive_sets]
y:32 [binder, in Coq.micromega.RingMicromega]
y:32 [binder, in Coq.Reals.Rfunctions]
y:32 [binder, in Coq.Structures.OrdersAlt]
y:32 [binder, in Coq.ZArith.Wf_Z]
y:32 [binder, in Coq.Reals.Rsqrt_def]
y:32 [binder, in Coq.Classes.CEquivalence]
y:32 [binder, in Coq.Program.Equality]
y:32 [binder, in Coq.Arith.PeanoNat]
y:32 [binder, in Coq.omega.OmegaLemmas]
y:32 [binder, in Coq.Classes.CRelationClasses]
y:32 [binder, in Coq.Structures.GenericMinMax]
y:32 [binder, in Coq.Sets.Multiset]
y:32 [binder, in Coq.NArith.BinNatDef]
y:32 [binder, in Coq.Reals.Rgeom]
y:32 [binder, in Coq.PArith.BinPosDef]
y:32 [binder, in Coq.Reals.R_sqr]
y:32 [binder, in Coq.Floats.FloatAxioms]
Y:32 [binder, in Coq.Sets.Infinite_sets]
y:32 [binder, in Coq.Relations.Relation_Operators]
y:32 [binder, in Coq.Structures.OrdersFacts]
y:32 [binder, in Coq.Classes.Equivalence]
y:322 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:322 [binder, in Coq.ssr.ssrbool]
y:322 [binder, in Coq.Reals.Rtopology]
y:324 [binder, in Coq.ssr.ssrbool]
y:324 [binder, in Coq.MSets.MSetRBT]
y:324 [binder, in Coq.Reals.RIneq]
y:325 [binder, in Coq.Logic.ChoiceFacts]
y:325 [binder, in Coq.micromega.ZMicromega]
y:327 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:327 [binder, in Coq.Logic.ChoiceFacts]
y:328 [binder, in Coq.Lists.List]
y:33 [binder, in Coq.Relations.Operators_Properties]
y:33 [binder, in Coq.setoid_ring.Ncring_initial]
y:33 [binder, in Coq.Reals.Ranalysis1]
y:33 [binder, in Coq.Logic.Eqdep_dec]
y:33 [binder, in Coq.ZArith.BinIntDef]
y:33 [binder, in Coq.Reals.Ranalysis4]
y:33 [binder, in Coq.Reals.Rfunctions]
y:33 [binder, in Coq.Sets.Ensembles]
y:33 [binder, in Coq.Reals.R_sqrt]
y:33 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:33 [binder, in Coq.Arith.Wf_nat]
y:33 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:33 [binder, in Coq.setoid_ring.InitialRing]
y:33 [binder, in Coq.Reals.Rpower]
y:33 [binder, in Coq.Sets.Cpo]
y:33 [binder, in Coq.Structures.OrderedTypeEx]
y:33 [binder, in Coq.Sets.Uniset]
y:33 [binder, in Coq.Structures.Equalities]
y:33 [binder, in Coq.Reals.Rbasic_fun]
y:33 [binder, in Coq.Logic.Berardi]
y:33 [binder, in Coq.setoid_ring.Ncring_polynom]
y:33 [binder, in Coq.Reals.Ranalysis5]
y:33 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:33 [binder, in Coq.Sets.Image]
y:33 [binder, in Coq.Structures.OrdersTac]
y:33 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:33 [binder, in Coq.micromega.ZMicromega]
y:33 [binder, in Coq.Relations.Relation_Operators]
y:330 [binder, in Coq.Reals.Rtopology]
y:331 [binder, in Coq.ssr.ssrfun]
y:332 [binder, in Coq.Reals.Rtopology]
y:333 [binder, in Coq.Init.Logic]
y:334 [binder, in Coq.Reals.Rtopology]
y:335 [binder, in Coq.MSets.MSetRBT]
y:336 [binder, in Coq.Reals.Rtopology]
y:337 [binder, in Coq.Reals.Rtopology]
y:339 [binder, in Coq.MSets.MSetInterface]
y:34 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:34 [binder, in Coq.Logic.EqdepFacts]
y:34 [binder, in Coq.Logic.JMeq]
y:34 [binder, in Coq.Structures.OrdersAlt]
y:34 [binder, in Coq.Numbers.DecimalQ]
y:34 [binder, in Coq.Init.Wf]
y:34 [binder, in Coq.Reals.Rdefinitions]
y:34 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:34 [binder, in Coq.Structures.OrderedType]
y:34 [binder, in Coq.Classes.SetoidDec]
y:34 [binder, in Coq.Numbers.NatInt.NZOrder]
y:34 [binder, in Coq.Lists.ListSet]
y:34 [binder, in Coq.Sets.Permut]
y:34 [binder, in Coq.NArith.BinNatDef]
y:34 [binder, in Coq.PArith.BinPosDef]
y:34 [binder, in Coq.Reals.R_sqr]
y:34 [binder, in Coq.Relations.Relation_Definitions]
Y:34 [binder, in Coq.Sets.Infinite_sets]
y:34 [binder, in Coq.Structures.OrdersFacts]
y:340 [binder, in Coq.ssr.ssrfun]
y:340 [binder, in Coq.Reals.Rtopology]
y:342 [binder, in Coq.Reals.Ranalysis5]
y:343 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:343 [binder, in Coq.MSets.MSetInterface]
y:343 [binder, in Coq.Reals.Rtopology]
y:344 [binder, in Coq.Reals.Rtopology]
y:345 [binder, in Coq.ssr.ssrfun]
y:349 [binder, in Coq.ssr.ssrfun]
y:35 [binder, in Coq.Program.Wf]
y:35 [binder, in Coq.Sorting.PermutEq]
Y:35 [binder, in Coq.Sets.Finite_sets_facts]
y:35 [binder, in Coq.FSets.FSetDecide]
y:35 [binder, in Coq.Reals.Ranalysis4]
y:35 [binder, in Coq.Reals.R_sqrt]
y:35 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:35 [binder, in Coq.Numbers.DecimalQ]
y:35 [binder, in Coq.Reals.Rsqrt_def]
y:35 [binder, in Coq.MSets.MSetDecide]
y:35 [binder, in Coq.setoid_ring.InitialRing]
y:35 [binder, in Coq.micromega.ZifyBool]
y:35 [binder, in Coq.Structures.DecidableType]
y:35 [binder, in Coq.Structures.OrderedTypeEx]
y:35 [binder, in Coq.Reals.Rbasic_fun]
y:35 [binder, in Coq.Logic.Berardi]
y:35 [binder, in Coq.Logic.HLevels]
y:35 [binder, in Coq.Sets.Powerset_Classical_facts]
y:35 [binder, in Coq.Reals.Ranalysis5]
y:35 [binder, in Coq.ssr.ssrunder]
y:35 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:35 [binder, in Coq.Sets.Multiset]
y:35 [binder, in Coq.Sets.Image]
y:35 [binder, in Coq.Floats.FloatAxioms]
y:35 [binder, in Coq.Reals.ClassicalConstructiveReals]
y:351 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:352 [binder, in Coq.ssr.ssrfun]
y:353 [binder, in Coq.MSets.MSetInterface]
y:353 [binder, in Coq.Init.Logic]
y:354 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:355 [binder, in Coq.MSets.MSetGenTree]
y:356 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:357 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:357 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:357 [binder, in Coq.FSets.FMapWeakList]
y:358 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:36 [binder, in Coq.Structures.Orders]
y:36 [binder, in Coq.Program.Wf]
y:36 [binder, in Coq.QArith.Qcanon]
y:36 [binder, in Coq.Reals.Ranalysis1]
y:36 [binder, in Coq.Reals.Rtrigo1]
y:36 [binder, in Coq.Reals.Ranalysis4]
y:36 [binder, in Coq.micromega.RingMicromega]
y:36 [binder, in Coq.Structures.OrdersAlt]
y:36 [binder, in Coq.ZArith.Wf_Z]
y:36 [binder, in Coq.ZArith.Zeven]
y:36 [binder, in Coq.Reals.Rdefinitions]
y:36 [binder, in Coq.Reals.Rpower]
y:36 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:36 [binder, in Coq.omega.OmegaLemmas]
y:36 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:36 [binder, in Coq.Classes.EquivDec]
y:36 [binder, in Coq.Reals.NewtonInt]
y:36 [binder, in Coq.ZArith.Zbool]
y:36 [binder, in Coq.setoid_ring.Ncring_polynom]
y:36 [binder, in Coq.Logic.Diaconescu]
y:36 [binder, in Coq.Sets.Image]
y:36 [binder, in Coq.Structures.OrdersTac]
y:36 [binder, in Coq.Reals.R_sqr]
y:36 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:36 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
Y:36 [binder, in Coq.Sets.Infinite_sets]
y:360 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:360 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:360 [binder, in Coq.Reals.Rtopology]
y:360 [binder, in Coq.Reals.Ranalysis5]
y:361 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:361 [binder, in Coq.ssr.ssrfun]
y:361 [binder, in Coq.Init.Logic]
y:362 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:362 [binder, in Coq.ssr.ssrbool]
y:363 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:363 [binder, in Coq.Reals.Rtopology]
y:364 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:364 [binder, in Coq.ssr.ssrbool]
y:366 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:366 [binder, in Coq.ssr.ssrbool]
y:366 [binder, in Coq.ssr.ssrfun]
y:366 [binder, in Coq.Reals.Rtopology]
y:366 [binder, in Coq.Init.Logic]
y:367 [binder, in Coq.FSets.FSetPositive]
y:368 [binder, in Coq.ssr.ssrbool]
y:368 [binder, in Coq.Reals.Rtopology]
y:369 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:37 [binder, in Coq.Relations.Operators_Properties]
y:37 [binder, in Coq.Logic.Eqdep_dec]
y:37 [binder, in Coq.Reals.R_sqrt]
y:37 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:37 [binder, in Coq.setoid_ring.InitialRing]
y:37 [binder, in Coq.micromega.ZifyBool]
y:37 [binder, in Coq.ZArith.Zeven]
y:37 [binder, in Coq.Structures.OrderedTypeEx]
y:37 [binder, in Coq.Reals.NewtonInt]
y:37 [binder, in Coq.Classes.CRelationClasses]
y:37 [binder, in Coq.Reals.Rtopology]
y:37 [binder, in Coq.Structures.OrderedType]
y:37 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
y:37 [binder, in Coq.Reals.Rbasic_fun]
y:37 [binder, in Coq.Logic.Berardi]
y:37 [binder, in Coq.Numbers.NatInt.NZOrder]
y:37 [binder, in Coq.Sets.Permut]
y:37 [binder, in Coq.Reals.Ranalysis5]
y:37 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:37 [binder, in Coq.Sets.Image]
y:37 [binder, in Coq.micromega.ZifyInst]
y:37 [binder, in Coq.Structures.OrdersFacts]
y:371 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:371 [binder, in Coq.Init.Specif]
y:372 [binder, in Coq.FSets.FMapList]
y:373 [binder, in Coq.Lists.List]
y:373 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:373 [binder, in Coq.MSets.MSetRBT]
y:373 [binder, in Coq.Init.Logic]
y:375 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:375 [binder, in Coq.FSets.FSetPositive]
y:375 [binder, in Coq.Reals.Rtopology]
y:376 [binder, in Coq.Logic.ChoiceFacts]
y:377 [binder, in Coq.Reals.Rtopology]
y:378 [binder, in Coq.Reals.Rtopology]
y:379 [binder, in Coq.ssr.ssrfun]
y:38 [binder, in Coq.Structures.Orders]
y:38 [binder, in Coq.QArith.Qcanon]
y:38 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Y:38 [binder, in Coq.Sets.Finite_sets_facts]
Y:38 [binder, in Coq.Sets.Constructive_sets]
y:38 [binder, in Coq.Reals.Ranalysis4]
y:38 [binder, in Coq.micromega.RingMicromega]
y:38 [binder, in Coq.Logic.JMeq]
y:38 [binder, in Coq.Structures.OrdersAlt]
y:38 [binder, in Coq.Reals.Rsqrt_def]
y:38 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:38 [binder, in Coq.Logic.ChoiceFacts]
y:38 [binder, in Coq.Init.Wf]
y:38 [binder, in Coq.Reals.Rdefinitions]
y:38 [binder, in Coq.Reals.Rpower]
y:38 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:38 [binder, in Coq.Program.Equality]
y:38 [binder, in Coq.omega.OmegaLemmas]
y:38 [binder, in Coq.Classes.EquivDec]
y:38 [binder, in Coq.Reals.NewtonInt]
y:38 [binder, in Coq.Sets.Multiset]
y:38 [binder, in Coq.Sets.Image]
y:38 [binder, in Coq.Floats.FloatAxioms]
y:38 [binder, in Coq.Reals.ClassicalConstructiveReals]
y:38 [binder, in Coq.Relations.Relation_Operators]
y:380 [binder, in Coq.MSets.MSetRBT]
y:380 [binder, in Coq.Reals.Rtopology]
y:380 [binder, in Coq.Reals.Ranalysis5]
y:381 [binder, in Coq.FSets.FSetPositive]
y:381 [binder, in Coq.Init.Logic]
y:382 [binder, in Coq.Logic.ChoiceFacts]
y:384 [binder, in Coq.ssr.ssrfun]
y:385 [binder, in Coq.Lists.List]
y:385 [binder, in Coq.Logic.ChoiceFacts]
y:386 [binder, in Coq.FSets.FSetPositive]
y:386 [binder, in Coq.MSets.MSetRBT]
y:386 [binder, in Coq.Reals.Rtopology]
y:388 [binder, in Coq.Logic.ChoiceFacts]
y:389 [binder, in Coq.ssr.ssrfun]
y:389 [binder, in Coq.Reals.Rtopology]
y:389 [binder, in Coq.Reals.Ranalysis5]
y:389 [binder, in Coq.Init.Logic]
y:39 [binder, in Coq.Reals.Ranalysis1]
y:39 [binder, in Coq.ZArith.BinIntDef]
y:39 [binder, in Coq.Reals.R_sqrt]
y:39 [binder, in Coq.setoid_ring.InitialRing]
y:39 [binder, in Coq.micromega.ZifyBool]
y:39 [binder, in Coq.Structures.DecidableType]
y:39 [binder, in Coq.Structures.OrderedTypeEx]
y:39 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:39 [binder, in Coq.Reals.NewtonInt]
y:39 [binder, in Coq.Reals.Rbasic_fun]
y:39 [binder, in Coq.Logic.Berardi]
y:39 [binder, in Coq.Logic.HLevels]
y:39 [binder, in Coq.Sets.Image]
y:39 [binder, in Coq.Structures.OrdersTac]
y:39 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:391 [binder, in Coq.ZArith.BinInt]
y:391 [binder, in Coq.Reals.Rtopology]
y:392 [binder, in Coq.Reals.Rtopology]
y:393 [binder, in Coq.ZArith.BinInt]
y:395 [binder, in Coq.Reals.Rtopology]
y:396 [binder, in Coq.Reals.Rtopology]
y:397 [binder, in Coq.FSets.FSetPositive]
y:397 [binder, in Coq.Reals.Rtopology]
y:397 [binder, in Coq.Init.Logic]
y:398 [binder, in Coq.Reals.Rtopology]
y:398 [binder, in Coq.Reals.Ranalysis5]
y:399 [binder, in Coq.Reals.Ranalysis1]
y:399 [binder, in Coq.ZArith.BinInt]
y:399 [binder, in Coq.Logic.ChoiceFacts]
y:399 [binder, in Coq.Reals.Rtopology]
y:399 [binder, in Coq.Init.Logic]
y:4 [binder, in Coq.Structures.Orders]
y:4 [binder, in Coq.Relations.Operators_Properties]
y:4 [binder, in Coq.micromega.Ztac]
y:4 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:4 [binder, in Coq.Reals.Rminmax]
y:4 [binder, in Coq.Structures.OrdersEx]
y:4 [binder, in Coq.Sets.Relations_3]
y:4 [binder, in Coq.PArith.BinPos]
y:4 [binder, in Coq.ZArith.BinInt]
y:4 [binder, in Coq.Structures.OrdersAlt]
y:4 [binder, in Coq.QArith.Qreals]
y:4 [binder, in Coq.NArith.BinNat]
y:4 [binder, in Coq.Structures.OrderedTypeEx]
y:4 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:4 [binder, in Coq.Sets.Uniset]
y:4 [binder, in Coq.Sets.Relations_1_facts]
y:4 [binder, in Coq.Structures.OrderedTypeAlt]
y:4 [binder, in Coq.ZArith.Zbool]
y:4 [binder, in Coq.Strings.Byte]
y:4 [binder, in Coq.Unicode.Utf8_core]
y:4 [binder, in Coq.omega.PreOmega]
y:4 [binder, in Coq.Sets.Relations_3_facts]
y:4 [binder, in Coq.Vectors.VectorEq]
y:4 [binder, in Coq.micromega.ZMicromega]
y:4 [binder, in Coq.Structures.OrdersFacts]
y:40 [binder, in Coq.Structures.Orders]
y:40 [binder, in Coq.QArith.Qcanon]
y:40 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:40 [binder, in Coq.Logic.Eqdep_dec]
y:40 [binder, in Coq.Logic.EqdepFacts]
y:40 [binder, in Coq.Reals.Ranalysis4]
y:40 [binder, in Coq.micromega.RingMicromega]
y:40 [binder, in Coq.Reals.ArithProp]
y:40 [binder, in Coq.Lists.List]
y:40 [binder, in Coq.Structures.OrdersAlt]
y:40 [binder, in Coq.ZArith.Wf_Z]
y:40 [binder, in Coq.Reals.Rpower]
y:40 [binder, in Coq.Reals.NewtonInt]
y:40 [binder, in Coq.Sets.Uniset]
y:40 [binder, in Coq.Structures.OrderedType]
y:40 [binder, in Coq.Classes.SetoidDec]
y:40 [binder, in Coq.Numbers.NatInt.NZOrder]
y:40 [binder, in Coq.Lists.ListSet]
y:40 [binder, in Coq.Sets.Permut]
y:40 [binder, in Coq.Logic.ClassicalDescription]
y:40 [binder, in Coq.Reals.Ranalysis5]
y:40 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:40 [binder, in Coq.Reals.Rgeom]
y:40 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:40 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:401 [binder, in Coq.ZArith.BinInt]
y:402 [binder, in Coq.Reals.Ranalysis1]
y:402 [binder, in Coq.Logic.ChoiceFacts]
y:403 [binder, in Coq.Reals.Ranalysis1]
y:403 [binder, in Coq.FSets.FSetPositive]
y:403 [binder, in Coq.FSets.FMapList]
y:404 [binder, in Coq.Reals.Ranalysis1]
y:404 [binder, in Coq.ZArith.BinInt]
y:405 [binder, in Coq.Reals.Ranalysis1]
y:406 [binder, in Coq.Reals.Ranalysis1]
y:406 [binder, in Coq.ZArith.BinInt]
y:406 [binder, in Coq.Logic.ChoiceFacts]
y:407 [binder, in Coq.Reals.Ranalysis1]
y:407 [binder, in Coq.Reals.Ranalysis5]
y:408 [binder, in Coq.Reals.Ranalysis1]
y:409 [binder, in Coq.Reals.Ranalysis1]
y:409 [binder, in Coq.Logic.ChoiceFacts]
y:409 [binder, in Coq.FSets.FSetPositive]
y:41 [binder, in Coq.setoid_ring.Ncring_initial]
y:41 [binder, in Coq.ZArith.BinIntDef]
y:41 [binder, in Coq.Reals.Ranalysis4]
y:41 [binder, in Coq.Reals.R_sqrt]
y:41 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:41 [binder, in Coq.setoid_ring.InitialRing]
y:41 [binder, in Coq.Reals.Rdefinitions]
y:41 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:41 [binder, in Coq.Structures.OrderedTypeEx]
y:41 [binder, in Coq.Reals.NewtonInt]
y:41 [binder, in Coq.Reals.Rtopology]
y:41 [binder, in Coq.ssr.ssrunder]
y:41 [binder, in Coq.Sets.Multiset]
y:41 [binder, in Coq.Floats.FloatAxioms]
y:41 [binder, in Coq.Structures.OrdersFacts]
y:410 [binder, in Coq.Reals.Ranalysis1]
y:410 [binder, in Coq.ZArith.BinInt]
y:411 [binder, in Coq.Reals.Ranalysis1]
y:412 [binder, in Coq.Reals.Ranalysis1]
y:412 [binder, in Coq.ZArith.BinInt]
y:412 [binder, in Coq.Reals.Rtopology]
y:413 [binder, in Coq.Reals.Ranalysis1]
y:414 [binder, in Coq.Reals.Ranalysis1]
y:414 [binder, in Coq.ZArith.BinInt]
y:416 [binder, in Coq.ZArith.BinInt]
y:417 [binder, in Coq.Reals.Ranalysis1]
y:418 [binder, in Coq.ZArith.BinInt]
y:418 [binder, in Coq.Reals.Rtopology]
y:42 [binder, in Coq.Structures.Orders]
y:42 [binder, in Coq.Reals.Ranalysis1]
y:42 [binder, in Coq.Logic.ConstructiveEpsilon]
y:42 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
y:42 [binder, in Coq.Reals.Ranalysis4]
y:42 [binder, in Coq.micromega.RingMicromega]
y:42 [binder, in Coq.Logic.JMeq]
y:42 [binder, in Coq.Reals.Rsqrt_def]
y:42 [binder, in Coq.Init.Wf]
y:42 [binder, in Coq.Reals.Rpower]
y:42 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:42 [binder, in Coq.Reals.NewtonInt]
y:42 [binder, in Coq.Sets.Uniset]
y:42 [binder, in Coq.Reals.Rbasic_fun]
y:42 [binder, in Coq.Structures.OrdersTac]
y:42 [binder, in Coq.PArith.BinPosDef]
y:42 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:42 [binder, in Coq.Lists.SetoidList]
y:420 [binder, in Coq.Reals.Ranalysis1]
y:420 [binder, in Coq.ZArith.BinInt]
y:422 [binder, in Coq.Reals.Ranalysis1]
y:423 [binder, in Coq.ZArith.BinInt]
y:424 [binder, in Coq.Reals.Rtopology]
y:424 [binder, in Coq.Reals.Ranalysis5]
y:425 [binder, in Coq.Reals.Ranalysis1]
y:425 [binder, in Coq.Logic.ChoiceFacts]
y:426 [binder, in Coq.Reals.Rtopology]
y:427 [binder, in Coq.Logic.ChoiceFacts]
y:428 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:428 [binder, in Coq.Init.Logic]
y:43 [binder, in Coq.Program.Wf]
y:43 [binder, in Coq.Relations.Operators_Properties]
y:43 [binder, in Coq.QArith.Qcanon]
y:43 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:43 [binder, in Coq.ZArith.BinIntDef]
y:43 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
Y:43 [binder, in Coq.Sets.Finite_sets_facts]
y:43 [binder, in Coq.Reals.Ranalysis4]
y:43 [binder, in Coq.Logic.ClassicalEpsilon]
y:43 [binder, in Coq.Reals.R_sqrt]
y:43 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:43 [binder, in Coq.Structures.OrdersAlt]
y:43 [binder, in Coq.Logic.ChoiceFacts]
y:43 [binder, in Coq.setoid_ring.InitialRing]
y:43 [binder, in Coq.Reals.NewtonInt]
y:43 [binder, in Coq.Reals.Rtopology]
y:43 [binder, in Coq.Structures.OrderedType]
y:43 [binder, in Coq.setoid_ring.Ncring_polynom]
y:43 [binder, in Coq.Sets.Permut]
y:43 [binder, in Coq.Sets.Powerset_facts]
y:43 [binder, in Coq.Reals.Ranalysis5]
y:43 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:43 [binder, in Coq.Reals.RList]
y:43 [binder, in Coq.Logic.Diaconescu]
y:43 [binder, in Coq.Reals.Rgeom]
y:43 [binder, in Coq.Reals.R_sqr]
y:43 [binder, in Coq.Relations.Relation_Operators]
y:43 [binder, in Coq.FSets.FSetCompat]
y:43 [binder, in Coq.Structures.OrdersFacts]
y:44 [binder, in Coq.Structures.Orders]
y:44 [binder, in Coq.setoid_ring.Ncring_initial]
y:44 [binder, in Coq.Reals.Ranalysis4]
y:44 [binder, in Coq.micromega.RingMicromega]
y:44 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:44 [binder, in Coq.Structures.OrderedTypeEx]
y:44 [binder, in Coq.Reals.NewtonInt]
y:44 [binder, in Coq.Logic.HLevels]
y:44 [binder, in Coq.Sets.Multiset]
y:44 [binder, in Coq.PArith.BinPosDef]
y:44 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:44 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:448 [binder, in Coq.Reals.Ranalysis5]
y:449 [binder, in Coq.Reals.Ranalysis5]
Y:45 [binder, in Coq.Logic.Decidable]
y:45 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:45 [binder, in Coq.Reals.Ranalysis1]
y:45 [binder, in Coq.Logic.Eqdep_dec]
y:45 [binder, in Coq.ZArith.BinIntDef]
y:45 [binder, in Coq.Lists.List]
y:45 [binder, in Coq.ZArith.Wf_Z]
y:45 [binder, in Coq.Init.Wf]
y:45 [binder, in Coq.setoid_ring.InitialRing]
y:45 [binder, in Coq.Reals.Rpower]
y:45 [binder, in Coq.Program.Equality]
y:45 [binder, in Coq.Reals.NewtonInt]
y:45 [binder, in Coq.Sets.Uniset]
y:45 [binder, in Coq.Structures.OrderedType]
y:45 [binder, in Coq.Reals.Rbasic_fun]
y:45 [binder, in Coq.Reals.RList]
y:45 [binder, in Coq.Logic.Diaconescu]
y:45 [binder, in Coq.Structures.OrdersTac]
y:45 [binder, in Coq.Reals.R_sqr]
y:45 [binder, in Coq.micromega.ZifyInst]
y:45 [binder, in Coq.Structures.OrdersFacts]
y:451 [binder, in Coq.Reals.Ranalysis5]
y:456 [binder, in Coq.MSets.MSetRBT]
y:458 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:459 [binder, in Coq.MSets.MSetRBT]
y:46 [binder, in Coq.Structures.Orders]
y:46 [binder, in Coq.setoid_ring.Ncring_initial]
y:46 [binder, in Coq.QArith.Qcanon]
y:46 [binder, in Coq.Logic.EqdepFacts]
y:46 [binder, in Coq.Reals.R_sqrt]
y:46 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:46 [binder, in Coq.FSets.FMapFacts]
y:46 [binder, in Coq.Logic.JMeq]
y:46 [binder, in Coq.Structures.OrderedTypeEx]
y:46 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:46 [binder, in Coq.Classes.EquivDec]
y:46 [binder, in Coq.Reals.Ranalysis5]
y:46 [binder, in Coq.Reals.Rgeom]
y:46 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:46 [binder, in Coq.FSets.FSetCompat]
y:460 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:462 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:464 [binder, in Coq.setoid_ring.Field_theory]
y:467 [binder, in Coq.Init.Logic]
y:468 [binder, in Coq.ssr.ssrbool]
y:47 [binder, in Coq.ZArith.BinIntDef]
Y:47 [binder, in Coq.Sets.Finite_sets_facts]
y:47 [binder, in Coq.Reals.Rsqrt_def]
y:47 [binder, in Coq.setoid_ring.InitialRing]
y:47 [binder, in Coq.Reals.Rpower]
y:47 [binder, in Coq.Structures.OrderedType]
y:47 [binder, in Coq.Structures.GenericMinMax]
y:47 [binder, in Coq.Sets.Permut]
y:47 [binder, in Coq.Reals.RList]
y:47 [binder, in Coq.Logic.Diaconescu]
y:47 [binder, in Coq.Reals.R_sqr]
y:470 [binder, in Coq.setoid_ring.Field_theory]
y:471 [binder, in Coq.ssr.ssrbool]
y:472 [binder, in Coq.Lists.List]
y:472 [binder, in Coq.setoid_ring.Field_theory]
y:473 [binder, in Coq.ssr.ssrbool]
y:474 [binder, in Coq.setoid_ring.Field_theory]
y:476 [binder, in Coq.setoid_ring.Field_theory]
y:477 [binder, in Coq.Lists.List]
y:479 [binder, in Coq.Lists.List]
y:479 [binder, in Coq.setoid_ring.Field_theory]
y:48 [binder, in Coq.Logic.Decidable]
y:48 [binder, in Coq.Structures.Orders]
y:48 [binder, in Coq.Relations.Operators_Properties]
y:48 [binder, in Coq.QArith.Qcanon]
y:48 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Y:48 [binder, in Coq.Sets.Finite_sets_facts]
y:48 [binder, in Coq.Reals.Rtrigo1]
y:48 [binder, in Coq.Logic.ChoiceFacts]
y:48 [binder, in Coq.ssr.ssrfun]
y:48 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:48 [binder, in Coq.Sets.Uniset]
y:48 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:48 [binder, in Coq.Sets.Multiset]
y:48 [binder, in Coq.Structures.OrdersTac]
y:48 [binder, in Coq.Reals.Rgeom]
y:48 [binder, in Coq.Lists.SetoidList]
y:481 [binder, in Coq.ssr.ssrbool]
y:483 [binder, in Coq.setoid_ring.Field_theory]
y:485 [binder, in Coq.setoid_ring.Field_theory]
y:487 [binder, in Coq.setoid_ring.Field_theory]
y:488 [binder, in Coq.Lists.List]
Y:49 [binder, in Coq.Sets.Finite_sets_facts]
y:49 [binder, in Coq.Reals.Ranalysis4]
y:49 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:49 [binder, in Coq.Structures.OrderedTypeEx]
y:49 [binder, in Coq.Structures.OrderedType]
y:49 [binder, in Coq.Logic.Diaconescu]
y:49 [binder, in Coq.Reals.R_sqr]
y:49 [binder, in Coq.FSets.FSetCompat]
y:490 [binder, in Coq.ssr.ssrbool]
y:493 [binder, in Coq.MSets.MSetAVL]
y:497 [binder, in Coq.PArith.BinPos]
y:498 [binder, in Coq.MSets.MSetAVL]
y:499 [binder, in Coq.PArith.BinPos]
y:499 [binder, in Coq.ssr.ssrbool]
y:5 [binder, in Coq.Wellfounded.Union]
y:5 [binder, in Coq.Structures.DecidableTypeEx]
y:5 [binder, in Coq.setoid_ring.RealField]
y:5 [binder, in Coq.Sorting.PermutSetoid]
y:5 [binder, in Coq.Wellfounded.Transitive_Closure]
y:5 [binder, in Coq.QArith.Qfield]
y:5 [binder, in Coq.Reals.Rdefinitions]
y:5 [binder, in Coq.Reals.Raxioms]
y:5 [binder, in Coq.Structures.OrderedType]
y:5 [binder, in Coq.Classes.SetoidDec]
y:5 [binder, in Coq.Sets.Permut]
y:5 [binder, in Coq.Reals.Rtrigo_calc]
y:5 [binder, in Coq.Sets.Multiset]
y:5 [binder, in Coq.micromega.RMicromega]
y:5 [binder, in Coq.PArith.BinPosDef]
y:5 [binder, in Coq.Reals.R_sqr]
y:5 [binder, in Coq.micromega.ZifyInst]
y:5 [binder, in Coq.Sets.Relations_1]
y:5 [binder, in Coq.Relations.Relation_Definitions]
y:5 [binder, in Coq.Sorting.Heap]
y:5 [binder, in Coq.Logic.FinFun]
y:5 [binder, in Coq.Reals.Cos_plus]
y:50 [binder, in Coq.Logic.Decidable]
y:50 [binder, in Coq.Structures.Orders]
y:50 [binder, in Coq.Relations.Operators_Properties]
y:50 [binder, in Coq.Reals.Rtrigo1]
y:50 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:50 [binder, in Coq.ZArith.Wf_Z]
y:50 [binder, in Coq.Reals.Rpower]
y:50 [binder, in Coq.Reals.PSeries_reg]
y:50 [binder, in Coq.micromega.ZifyInst]
y:50 [binder, in Coq.Relations.Relation_Operators]
y:50 [binder, in Coq.Structures.OrdersFacts]
y:50 [binder, in Coq.Reals.Cos_plus]
y:501 [binder, in Coq.PArith.BinPos]
y:503 [binder, in Coq.PArith.BinPos]
y:503 [binder, in Coq.ssr.ssrbool]
y:504 [binder, in Coq.ssr.ssrbool]
y:508 [binder, in Coq.ssr.ssrbool]
y:509 [binder, in Coq.MSets.MSetAVL]
y:51 [binder, in Coq.Logic.Decidable]
y:51 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:51 [binder, in Coq.Reals.Ranalysis4]
y:51 [binder, in Coq.FSets.FMapFacts]
y:51 [binder, in Coq.Logic.JMeq]
y:51 [binder, in Coq.Reals.Rsqrt_def]
y:51 [binder, in Coq.ssr.ssrfun]
y:51 [binder, in Coq.Sets.Uniset]
y:51 [binder, in Coq.Reals.Ranalysis5]
y:51 [binder, in Coq.Sets.Multiset]
y:51 [binder, in Coq.Logic.Diaconescu]
y:51 [binder, in Coq.Structures.OrdersTac]
y:51 [binder, in Coq.Reals.R_sqr]
y:51 [binder, in Coq.QArith.Qpower]
y:51 [binder, in Coq.Sorting.Mergesort]
y:510 [binder, in Coq.ssr.ssrbool]
y:512 [binder, in Coq.ssr.ssrbool]
y:513 [binder, in Coq.ZArith.BinInt]
y:515 [binder, in Coq.MSets.MSetRBT]
y:516 [binder, in Coq.ssr.ssrbool]
y:518 [binder, in Coq.ssr.ssrbool]
y:519 [binder, in Coq.MSets.MSetAVL]
y:52 [binder, in Coq.Structures.Orders]
y:52 [binder, in Coq.Relations.Operators_Properties]
y:52 [binder, in Coq.Logic.Eqdep_dec]
y:52 [binder, in Coq.Logic.EqdepFacts]
y:52 [binder, in Coq.Reals.Ranalysis4]
y:52 [binder, in Coq.Lists.List]
y:52 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:52 [binder, in Coq.Init.Wf]
y:52 [binder, in Coq.Structures.OrderedTypeEx]
y:52 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:52 [binder, in Coq.Structures.OrderedType]
y:52 [binder, in Coq.Sets.Powerset_facts]
y:52 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:52 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:52 [binder, in Coq.FSets.FSetCompat]
y:52 [binder, in Coq.Structures.OrdersFacts]
y:522 [binder, in Coq.ssr.ssrbool]
y:522 [binder, in Coq.MSets.MSetAVL]
y:523 [binder, in Coq.Init.Specif]
y:524 [binder, in Coq.Init.Logic]
y:527 [binder, in Coq.ssr.ssrbool]
y:529 [binder, in Coq.FSets.FMapWeakList]
y:53 [binder, in Coq.Reals.Rderiv]
y:53 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:53 [binder, in Coq.QArith.Qcanon]
y:53 [binder, in Coq.Reals.Rtrigo1]
y:53 [binder, in Coq.FSets.FSetDecide]
y:53 [binder, in Coq.Reals.Ranalysis4]
y:53 [binder, in Coq.MSets.MSetDecide]
y:53 [binder, in Coq.ssr.ssrfun]
y:53 [binder, in Coq.FSets.FSetPositive]
y:53 [binder, in Coq.MSets.MSetPositive]
y:53 [binder, in Coq.Reals.Ranalysis5]
y:53 [binder, in Coq.Logic.Diaconescu]
y:53 [binder, in Coq.Reals.R_sqr]
y:53 [binder, in Coq.Relations.Relation_Operators]
y:530 [binder, in Coq.ssr.ssrbool]
y:530 [binder, in Coq.MSets.MSetAVL]
y:532 [binder, in Coq.ssr.ssrbool]
y:54 [binder, in Coq.Structures.Orders]
y:54 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:54 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:54 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:54 [binder, in Coq.Structures.OrderedTypeEx]
y:54 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:54 [binder, in Coq.ZArith.Zpower]
y:54 [binder, in Coq.Sets.Uniset]
y:54 [binder, in Coq.Structures.OrdersTac]
y:54 [binder, in Coq.micromega.ZifyInst]
y:54 [binder, in Coq.Reals.ClassicalConstructiveReals]
y:54 [binder, in Coq.Logic.FinFun]
y:54 [binder, in Coq.Structures.OrdersFacts]
y:541 [binder, in Coq.PArith.BinPos]
y:541 [binder, in Coq.MSets.MSetAVL]
y:542 [binder, in Coq.FSets.FMapWeakList]
y:543 [binder, in Coq.MSets.MSetRBT]
y:549 [binder, in Coq.ssr.ssrbool]
y:549 [binder, in Coq.Strings.Byte]
y:549 [binder, in Coq.FSets.FMapList]
y:55 [binder, in Coq.Relations.Operators_Properties]
y:55 [binder, in Coq.Reals.Ranalysis4]
y:55 [binder, in Coq.FSets.FMapFacts]
y:55 [binder, in Coq.Logic.JMeq]
y:55 [binder, in Coq.ssr.ssrfun]
y:55 [binder, in Coq.ZArith.Zbool]
y:55 [binder, in Coq.Structures.OrderedType]
y:55 [binder, in Coq.Sets.Powerset_facts]
y:55 [binder, in Coq.Reals.Ranalysis5]
y:55 [binder, in Coq.Sets.Multiset]
y:55 [binder, in Coq.Reals.R_sqr]
y:55 [binder, in Coq.Relations.Relation_Operators]
y:55 [binder, in Coq.FSets.FSetCompat]
y:552 [binder, in Coq.ssr.ssrbool]
y:552 [binder, in Coq.FSets.FMapWeakList]
y:555 [binder, in Coq.ssr.ssrbool]
y:555 [binder, in Coq.MSets.MSetAVL]
y:556 [binder, in Coq.FSets.FMapWeakList]
y:559 [binder, in Coq.ssr.ssrbool]
y:56 [binder, in Coq.Structures.Orders]
y:56 [binder, in Coq.Logic.Eqdep_dec]
y:56 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:56 [binder, in Coq.Reals.Rsqrt_def]
y:56 [binder, in Coq.Bool.Bool]
y:56 [binder, in Coq.Structures.OrderedTypeEx]
y:56 [binder, in Coq.Classes.EquivDec]
y:56 [binder, in Coq.Reals.Rbasic_fun]
y:56 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:56 [binder, in Coq.Logic.Diaconescu]
y:56 [binder, in Coq.micromega.ZifyInst]
y:56 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:561 [binder, in Coq.FSets.FMapWeakList]
y:562 [binder, in Coq.FSets.FMapList]
y:563 [binder, in Coq.ssr.ssrbool]
y:565 [binder, in Coq.Lists.List]
y:565 [binder, in Coq.MSets.MSetAVL]
y:566 [binder, in Coq.FSets.FMapWeakList]
y:567 [binder, in Coq.ssr.ssrbool]
y:568 [binder, in Coq.Lists.List]
y:569 [binder, in Coq.FSets.FMapWeakList]
y:57 [binder, in Coq.Program.Wf]
y:57 [binder, in Coq.Relations.Operators_Properties]
y:57 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:57 [binder, in Coq.FSets.FSetDecide]
y:57 [binder, in Coq.Reals.Ranalysis4]
y:57 [binder, in Coq.Classes.RelationClasses]
y:57 [binder, in Coq.Logic.ChoiceFacts]
y:57 [binder, in Coq.MSets.MSetDecide]
y:57 [binder, in Coq.ssr.ssrfun]
y:57 [binder, in Coq.Reals.Rpower]
y:57 [binder, in Coq.ZArith.Zpower]
y:57 [binder, in Coq.ZArith.Zbool]
y:57 [binder, in Coq.Structures.OrdersTac]
y:57 [binder, in Coq.Reals.R_sqr]
y:57 [binder, in Coq.Structures.OrdersFacts]
y:572 [binder, in Coq.MSets.MSetAVL]
y:572 [binder, in Coq.FSets.FMapList]
y:573 [binder, in Coq.Lists.List]
y:573 [binder, in Coq.FSets.FMapWeakList]
y:575 [binder, in Coq.MSets.MSetRBT]
y:576 [binder, in Coq.ssr.ssrbool]
y:576 [binder, in Coq.Reals.RIneq]
y:576 [binder, in Coq.FSets.FMapList]
y:578 [binder, in Coq.Reals.RIneq]
y:58 [binder, in Coq.Program.Wf]
y:58 [binder, in Coq.setoid_ring.Ncring_initial]
y:58 [binder, in Coq.Logic.EqdepFacts]
y:58 [binder, in Coq.Reals.Ranalysis4]
y:58 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:58 [binder, in Coq.Sets.Uniset]
y:58 [binder, in Coq.Structures.OrderedType]
y:58 [binder, in Coq.Reals.Rbasic_fun]
y:58 [binder, in Coq.Reals.PSeries_reg]
y:58 [binder, in Coq.Reals.Ranalysis5]
y:58 [binder, in Coq.micromega.RMicromega]
y:58 [binder, in Coq.micromega.ZifyInst]
y:58 [binder, in Coq.QArith.QArith_base]
y:58 [binder, in Coq.FSets.FSetCompat]
y:580 [binder, in Coq.Reals.RIneq]
y:581 [binder, in Coq.FSets.FMapList]
y:582 [binder, in Coq.MSets.MSetAVL]
y:582 [binder, in Coq.Reals.RIneq]
y:586 [binder, in Coq.MSets.MSetAVL]
y:586 [binder, in Coq.Reals.RIneq]
y:586 [binder, in Coq.FSets.FMapList]
y:589 [binder, in Coq.FSets.FMapList]
y:59 [binder, in Coq.Relations.Operators_Properties]
y:59 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:59 [binder, in Coq.Reals.Ranalysis1]
y:59 [binder, in Coq.ZArith.Zbool]
y:59 [binder, in Coq.Sets.Multiset]
y:59 [binder, in Coq.Structures.OrdersTac]
y:59 [binder, in Coq.Lists.SetoidList]
y:593 [binder, in Coq.FSets.FMapList]
y:594 [binder, in Coq.MSets.MSetAVL]
y:595 [binder, in Coq.MSets.MSetAVL]
y:596 [binder, in Coq.MSets.MSetAVL]
y:597 [binder, in Coq.MSets.MSetAVL]
y:6 [binder, in Coq.Program.Wf]
y:6 [binder, in Coq.micromega.Ztac]
y:6 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:6 [binder, in Coq.Wellfounded.Inverse_Image]
y:6 [binder, in Coq.Reals.Rminmax]
y:6 [binder, in Coq.PArith.BinPos]
y:6 [binder, in Coq.MSets.MSetProperties]
y:6 [binder, in Coq.ZArith.BinInt]
y:6 [binder, in Coq.Numbers.NatInt.NZBase]
y:6 [binder, in Coq.Reals.Exp_prop]
y:6 [binder, in Coq.Reals.Rsqrt_def]
y:6 [binder, in Coq.Init.Wf]
y:6 [binder, in Coq.micromega.ZifyBool]
y:6 [binder, in Coq.Relations.Relations]
y:6 [binder, in Coq.QArith.Qreals]
y:6 [binder, in Coq.NArith.BinNat]
y:6 [binder, in Coq.Classes.EquivDec]
y:6 [binder, in Coq.Logic.RelationalChoice]
y:6 [binder, in Coq.ZArith.Zbool]
y:6 [binder, in Coq.Structures.Equalities]
y:6 [binder, in Coq.Reals.Rtopology]
y:6 [binder, in Coq.Bool.BoolEq]
y:6 [binder, in Coq.micromega.ZifyComparison]
y:6 [binder, in Coq.Structures.GenericMinMax]
y:6 [binder, in Coq.Strings.Byte]
y:6 [binder, in Coq.micromega.Fourier_util]
y:6 [binder, in Coq.Logic.HLevels]
y:6 [binder, in Coq.Unicode.Utf8_core]
y:6 [binder, in Coq.Reals.Ranalysis5]
y:6 [binder, in Coq.Sets.Relations_2]
y:6 [binder, in Coq.omega.PreOmega]
y:6 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:6 [binder, in Coq.FSets.FSetProperties]
y:6 [binder, in Coq.Reals.ClassicalConstructiveReals]
y:6 [binder, in Coq.Relations.Relation_Operators]
y:6 [binder, in Coq.Bool.DecBool]
y:6 [binder, in Coq.Lists.SetoidList]
y:6 [binder, in Coq.Structures.OrdersFacts]
y:60 [binder, in Coq.Reals.Ranalysis4]
y:60 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:60 [binder, in Coq.FSets.FMapFacts]
y:60 [binder, in Coq.Logic.JMeq]
y:60 [binder, in Coq.Reals.Rsqrt_def]
y:60 [binder, in Coq.Init.Wf]
y:60 [binder, in Coq.Reals.Rdefinitions]
y:60 [binder, in Coq.Reals.Rbasic_fun]
y:60 [binder, in Coq.Sets.Powerset_facts]
y:60 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:60 [binder, in Coq.Reals.R_sqr]
y:60 [binder, in Coq.micromega.ZifyInst]
y:60 [binder, in Coq.Relations.Relation_Operators]
y:60 [binder, in Coq.QArith.QArith_base]
y:60 [binder, in Coq.Structures.OrdersFacts]
y:605 [binder, in Coq.PArith.BinPos]
y:605 [binder, in Coq.Lists.List]
y:608 [binder, in Coq.FSets.FMapFacts]
y:608 [binder, in Coq.MSets.MSetAVL]
y:609 [binder, in Coq.Lists.List]
y:61 [binder, in Coq.Relations.Operators_Properties]
y:61 [binder, in Coq.Reals.Rpower]
y:61 [binder, in Coq.Sets.Uniset]
y:61 [binder, in Coq.ZArith.Zbool]
y:61 [binder, in Coq.Structures.OrderedType]
y:61 [binder, in Coq.Reals.Ranalysis5]
y:61 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:61 [binder, in Coq.Structures.OrdersTac]
y:61 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:61 [binder, in Coq.Lists.SetoidList]
y:611 [binder, in Coq.FSets.FMapFacts]
y:611 [binder, in Coq.MSets.MSetAVL]
y:616 [binder, in Coq.Lists.List]
y:618 [binder, in Coq.FSets.FMapWeakList]
y:62 [binder, in Coq.Program.Wf]
y:62 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:62 [binder, in Coq.Reals.Ranalysis4]
y:62 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:62 [binder, in Coq.Reals.Rbasic_fun]
y:62 [binder, in Coq.micromega.ZifyInst]
y:62 [binder, in Coq.Logic.FinFun]
y:621 [binder, in Coq.Lists.List]
y:622 [binder, in Coq.MSets.MSetAVL]
y:623 [binder, in Coq.Lists.List]
y:625 [binder, in Coq.MSets.MSetAVL]
y:629 [binder, in Coq.Lists.List]
y:63 [binder, in Coq.Relations.Operators_Properties]
y:63 [binder, in Coq.Logic.Eqdep_dec]
y:63 [binder, in Coq.Reals.Rtrigo1]
y:63 [binder, in Coq.FSets.FSetDecide]
y:63 [binder, in Coq.Classes.RelationClasses]
y:63 [binder, in Coq.MSets.MSetDecide]
y:63 [binder, in Coq.setoid_ring.InitialRing]
y:63 [binder, in Coq.Structures.OrderedTypeEx]
y:63 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:63 [binder, in Coq.Structures.OrdersTac]
y:63 [binder, in Coq.Reals.R_sqr]
y:63 [binder, in Coq.Logic.FinFun]
y:63 [binder, in Coq.Structures.OrdersFacts]
y:631 [binder, in Coq.ssr.ssrbool]
y:633 [binder, in Coq.Lists.List]
y:633 [binder, in Coq.ssr.ssrbool]
y:634 [binder, in Coq.Lists.List]
y:634 [binder, in Coq.MSets.MSetAVL]
y:635 [binder, in Coq.Lists.List]
y:635 [binder, in Coq.ssr.ssrbool]
y:637 [binder, in Coq.ssr.ssrbool]
y:639 [binder, in Coq.FSets.FMapList]
y:64 [binder, in Coq.QArith.Qcanon]
y:64 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:64 [binder, in Coq.Logic.EqdepFacts]
y:64 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:64 [binder, in Coq.FSets.FMapFacts]
y:64 [binder, in Coq.Reals.Rsqrt_def]
y:64 [binder, in Coq.Structures.OrderedType]
y:64 [binder, in Coq.Reals.Rbasic_fun]
y:64 [binder, in Coq.Sets.Powerset_facts]
y:64 [binder, in Coq.Reals.Ranalysis5]
y:64 [binder, in Coq.Sets.Multiset]
y:64 [binder, in Coq.Sets.Image]
y:64 [binder, in Coq.Reals.ClassicalDedekindReals]
y:64 [binder, in Coq.Lists.SetoidList]
y:65 [binder, in Coq.setoid_ring.InitialRing]
y:65 [binder, in Coq.Sets.Uniset]
y:65 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:65 [binder, in Coq.Relations.Relation_Operators]
y:66 [binder, in Coq.Relations.Operators_Properties]
y:66 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:66 [binder, in Coq.QArith.Qcanon]
y:66 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:66 [binder, in Coq.micromega.ZifyClasses]
y:66 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:66 [binder, in Coq.Structures.OrderedTypeEx]
y:66 [binder, in Coq.Reals.Raxioms]
y:66 [binder, in Coq.Classes.CRelationClasses]
y:66 [binder, in Coq.Reals.Rbasic_fun]
y:66 [binder, in Coq.Reals.PSeries_reg]
y:66 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:66 [binder, in Coq.Structures.OrdersFacts]
y:67 [binder, in Coq.Program.Wf]
y:67 [binder, in Coq.Reals.Ranalysis4]
y:67 [binder, in Coq.Logic.JMeq]
y:67 [binder, in Coq.Init.Wf]
y:67 [binder, in Coq.setoid_ring.InitialRing]
y:67 [binder, in Coq.Reals.Rtopology]
y:67 [binder, in Coq.Structures.OrderedType]
y:67 [binder, in Coq.setoid_ring.Ring_theory]
y:67 [binder, in Coq.Reals.ClassicalDedekindReals]
y:670 [binder, in Coq.ssr.ssrbool]
y:674 [binder, in Coq.Init.Specif]
y:68 [binder, in Coq.Program.Wf]
y:68 [binder, in Coq.Relations.Operators_Properties]
y:68 [binder, in Coq.FSets.FSetDecide]
y:68 [binder, in Coq.Reals.Ranalysis4]
y:68 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:68 [binder, in Coq.FSets.FMapFacts]
y:68 [binder, in Coq.Logic.ChoiceFacts]
y:68 [binder, in Coq.FSets.FMapInterface]
y:68 [binder, in Coq.MSets.MSetDecide]
y:68 [binder, in Coq.Classes.EquivDec]
y:68 [binder, in Coq.Reals.Raxioms]
y:68 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:685 [binder, in Coq.Lists.List]
y:685 [binder, in Coq.ssr.ssrbool]
y:687 [binder, in Coq.ssr.ssrbool]
y:689 [binder, in Coq.ssr.ssrbool]
y:69 [binder, in Coq.Program.Wf]
y:69 [binder, in Coq.QArith.Qcanon]
y:69 [binder, in Coq.Logic.Eqdep_dec]
y:69 [binder, in Coq.Reals.Ranalysis4]
y:69 [binder, in Coq.Sets.Uniset]
y:69 [binder, in Coq.Structures.OrderedType]
y:69 [binder, in Coq.Reals.Rbasic_fun]
y:69 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:69 [binder, in Coq.PArith.BinPosDef]
y:69 [binder, in Coq.Structures.OrdersFacts]
y:691 [binder, in Coq.ssr.ssrbool]
y:694 [binder, in Coq.ssr.ssrbool]
y:696 [binder, in Coq.Init.Specif]
y:696 [binder, in Coq.ssr.ssrbool]
y:698 [binder, in Coq.ssr.ssrbool]
y:7 [binder, in Coq.Program.Wf]
y:7 [binder, in Coq.Relations.Operators_Properties]
y:7 [binder, in Coq.Structures.DecidableTypeEx]
y:7 [binder, in Coq.Wellfounded.Inverse_Image]
y:7 [binder, in Coq.Sets.Relations_3]
y:7 [binder, in Coq.Arith.Bool_nat]
y:7 [binder, in Coq.Reals.R_sqrt]
y:7 [binder, in Coq.Logic.ChoiceFacts]
y:7 [binder, in Coq.Wellfounded.Lexicographic_Product]
y:7 [binder, in Coq.QArith.Qfield]
y:7 [binder, in Coq.Sets.Cpo]
y:7 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
y:7 [binder, in Coq.Reals.Raxioms]
y:7 [binder, in Coq.Reals.PSeries_reg]
y:7 [binder, in Coq.ssr.ssrunder]
y:7 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:7 [binder, in Coq.micromega.RMicromega]
Y:7 [binder, in Coq.Sets.Classical_sets]
y:7 [binder, in Coq.PArith.BinPosDef]
y:7 [binder, in Coq.Reals.R_sqr]
y:7 [binder, in Coq.Relations.Relation_Operators]
y:7 [binder, in Coq.Sorting.Heap]
y:7 [binder, in Coq.Reals.Cos_plus]
y:70 [binder, in Coq.Relations.Operators_Properties]
y:70 [binder, in Coq.Logic.EqdepFacts]
y:70 [binder, in Coq.Reals.Ranalysis4]
y:70 [binder, in Coq.Structures.OrderedTypeEx]
y:70 [binder, in Coq.setoid_ring.Ring_theory]
y:70 [binder, in Coq.Relations.Relation_Operators]
y:70 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:700 [binder, in Coq.ssr.ssrbool]
y:702 [binder, in Coq.Init.Specif]
y:702 [binder, in Coq.ssr.ssrbool]
y:704 [binder, in Coq.ssr.ssrbool]
y:706 [binder, in Coq.ssr.ssrbool]
y:708 [binder, in Coq.ssr.ssrbool]
y:71 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:71 [binder, in Coq.FSets.FMapFacts]
y:71 [binder, in Coq.Logic.ChoiceFacts]
y:71 [binder, in Coq.ssr.ssrfun]
y:71 [binder, in Coq.Reals.Ranalysis5]
y:71 [binder, in Coq.Reals.R_sqr]
y:710 [binder, in Coq.ssr.ssrbool]
y:712 [binder, in Coq.ssr.ssrbool]
y:714 [binder, in Coq.ssr.ssrbool]
y:716 [binder, in Coq.Init.Specif]
y:716 [binder, in Coq.ssr.ssrbool]
y:718 [binder, in Coq.ssr.ssrbool]
y:72 [binder, in Coq.Relations.Operators_Properties]
y:72 [binder, in Coq.QArith.Qcanon]
y:72 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:72 [binder, in Coq.Reals.Rsqrt_def]
y:72 [binder, in Coq.Structures.OrderedTypeEx]
y:72 [binder, in Coq.Reals.Raxioms]
y:72 [binder, in Coq.Classes.CRelationClasses]
y:72 [binder, in Coq.Structures.OrderedType]
y:72 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:72 [binder, in Coq.Logic.Diaconescu]
y:72 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:72 [binder, in Coq.Structures.OrdersFacts]
y:720 [binder, in Coq.ssr.ssrbool]
y:722 [binder, in Coq.ssr.ssrbool]
y:724 [binder, in Coq.ssr.ssrbool]
y:726 [binder, in Coq.ssr.ssrbool]
y:728 [binder, in Coq.ssr.ssrbool]
y:73 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:73 [binder, in Coq.micromega.RingMicromega]
y:73 [binder, in Coq.Reals.Exp_prop]
y:73 [binder, in Coq.Logic.JMeq]
y:73 [binder, in Coq.Logic.Diaconescu]
y:73 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:73 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:730 [binder, in Coq.ssr.ssrbool]
y:732 [binder, in Coq.ssr.ssrbool]
y:734 [binder, in Coq.ssr.ssrbool]
y:736 [binder, in Coq.ssr.ssrbool]
y:74 [binder, in Coq.QArith.Qcanon]
y:74 [binder, in Coq.Reals.Rfunctions]
y:74 [binder, in Coq.Classes.RelationClasses]
y:74 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:74 [binder, in Coq.Structures.OrderedTypeEx]
y:74 [binder, in Coq.Reals.Raxioms]
y:74 [binder, in Coq.Sets.Uniset]
y:74 [binder, in Coq.Structures.OrderedType]
y:74 [binder, in Coq.Logic.Diaconescu]
y:74 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:749 [binder, in Coq.ssr.ssrbool]
y:75 [binder, in Coq.FSets.FSetDecide]
y:75 [binder, in Coq.FSets.FMapFacts]
y:75 [binder, in Coq.MSets.MSetDecide]
y:75 [binder, in Coq.Init.Wf]
y:75 [binder, in Coq.Reals.Rbasic_fun]
y:75 [binder, in Coq.Reals.Ranalysis5]
y:75 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:75 [binder, in Coq.Logic.Diaconescu]
y:75 [binder, in Coq.Relations.Relation_Operators]
y:75 [binder, in Coq.Structures.OrdersFacts]
y:751 [binder, in Coq.ssr.ssrbool]
y:753 [binder, in Coq.ssr.ssrbool]
y:755 [binder, in Coq.ssr.ssrbool]
y:76 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:76 [binder, in Coq.Reals.Ranalysis4]
y:76 [binder, in Coq.Arith.PeanoNat]
y:76 [binder, in Coq.Vectors.Fin]
y:76 [binder, in Coq.Reals.Rtopology]
y:76 [binder, in Coq.Structures.OrderedType]
y:76 [binder, in Coq.Logic.Diaconescu]
y:76 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:76 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:76 [binder, in Coq.QArith.QArith_base]
y:762 [binder, in Coq.ssr.ssrbool]
y:764 [binder, in Coq.ssr.ssrbool]
y:766 [binder, in Coq.ssr.ssrbool]
y:768 [binder, in Coq.ssr.ssrbool]
y:77 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:77 [binder, in Coq.Logic.Eqdep_dec]
y:77 [binder, in Coq.omega.OmegaLemmas]
y:77 [binder, in Coq.Reals.Rbasic_fun]
y:77 [binder, in Coq.Init.Datatypes]
y:77 [binder, in Coq.Reals.Ranalysis5]
y:77 [binder, in Coq.Logic.Diaconescu]
y:770 [binder, in Coq.ssr.ssrbool]
y:772 [binder, in Coq.ssr.ssrbool]
y:774 [binder, in Coq.ssr.ssrbool]
y:776 [binder, in Coq.ssr.ssrbool]
y:778 [binder, in Coq.ssr.ssrbool]
y:78 [binder, in Coq.Structures.OrderedType]
y:78 [binder, in Coq.Reals.Ratan]
y:78 [binder, in Coq.setoid_ring.Ring_theory]
y:78 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:78 [binder, in Coq.Structures.EqualitiesFacts]
y:78 [binder, in Coq.QArith.QArith_base]
y:78 [binder, in Coq.Structures.OrdersFacts]
y:780 [binder, in Coq.ssr.ssrbool]
y:782 [binder, in Coq.ssr.ssrbool]
y:784 [binder, in Coq.ssr.ssrbool]
y:786 [binder, in Coq.ssr.ssrbool]
y:788 [binder, in Coq.ssr.ssrbool]
y:79 [binder, in Coq.Classes.RelationClasses]
y:79 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:79 [binder, in Coq.Logic.JMeq]
y:79 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:79 [binder, in Coq.Logic.ChoiceFacts]
y:79 [binder, in Coq.MSets.MSetWeakList]
y:79 [binder, in Coq.Reals.Rtopology]
y:790 [binder, in Coq.ssr.ssrbool]
y:792 [binder, in Coq.ssr.ssrbool]
y:794 [binder, in Coq.ssr.ssrbool]
y:796 [binder, in Coq.ssr.ssrbool]
y:798 [binder, in Coq.ssr.ssrbool]
y:8 [binder, in Coq.Structures.Orders]
y:8 [binder, in Coq.micromega.Ztac]
y:8 [binder, in Coq.Structures.OrdersLists]
y:8 [binder, in Coq.ZArith.BinIntDef]
y:8 [binder, in Coq.FSets.FSetBridge]
y:8 [binder, in Coq.Reals.Rminmax]
y:8 [binder, in Coq.Sets.Constructive_sets]
y:8 [binder, in Coq.PArith.BinPos]
y:8 [binder, in Coq.Classes.RelationClasses]
y:8 [binder, in Coq.ZArith.BinInt]
y:8 [binder, in Coq.Logic.JMeq]
y:8 [binder, in Coq.Structures.OrdersAlt]
y:8 [binder, in Coq.Program.Subset]
y:8 [binder, in Coq.Init.Wf]
y:8 [binder, in Coq.micromega.ZifyBool]
y:8 [binder, in Coq.QArith.Qreals]
y:8 [binder, in Coq.NArith.BinNat]
y:8 [binder, in Coq.Sorting.Permutation]
y:8 [binder, in Coq.funind.Recdef]
y:8 [binder, in Coq.Structures.OrderedTypeEx]
y:8 [binder, in Coq.Structures.OrderedTypeAlt]
y:8 [binder, in Coq.Logic.RelationalChoice]
y:8 [binder, in Coq.ZArith.Zbool]
y:8 [binder, in Coq.ZArith.Zpow_alt]
y:8 [binder, in Coq.micromega.ZifyComparison]
y:8 [binder, in Coq.Sets.Permut]
Y:8 [binder, in Coq.Sets.Powerset_Classical_facts]
y:8 [binder, in Coq.setoid_ring.Ring_theory]
y:8 [binder, in Coq.omega.PreOmega]
y:8 [binder, in Coq.Sets.Image]
y:8 [binder, in Coq.Sets.Relations_1]
y:8 [binder, in Coq.Relations.Relation_Definitions]
y:8 [binder, in Coq.Reals.ROrderedType]
y:8 [binder, in Coq.Floats.FloatAxioms]
y:8 [binder, in Coq.Reals.Cos_rel]
y:8 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:8 [binder, in Coq.Lists.SetoidList]
y:8 [binder, in Coq.Structures.OrdersFacts]
y:80 [binder, in Coq.QArith.Qcanon]
y:80 [binder, in Coq.Reals.Rpower]
y:80 [binder, in Coq.omega.OmegaLemmas]
y:80 [binder, in Coq.Structures.OrderedType]
y:80 [binder, in Coq.Reals.Rbasic_fun]
y:80 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:80 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:800 [binder, in Coq.ssr.ssrbool]
y:802 [binder, in Coq.ssr.ssrbool]
y:804 [binder, in Coq.ssr.ssrbool]
y:81 [binder, in Coq.FSets.FSetDecide]
y:81 [binder, in Coq.Reals.Ranalysis4]
y:81 [binder, in Coq.MSets.MSetDecide]
y:81 [binder, in Coq.Reals.Rpower]
y:81 [binder, in Coq.setoid_ring.Ring_theory]
y:81 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:81 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:81 [binder, in Coq.Reals.ClassicalDedekindReals]
y:81 [binder, in Coq.QArith.QArith_base]
y:81 [binder, in Coq.Structures.OrdersFacts]
y:82 [binder, in Coq.Program.Wf]
y:82 [binder, in Coq.QArith.Qcanon]
y:82 [binder, in Coq.Logic.Eqdep_dec]
y:82 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:82 [binder, in Coq.Logic.ChoiceFacts]
y:82 [binder, in Coq.Arith.PeanoNat]
y:82 [binder, in Coq.Structures.OrderedType]
y:824 [binder, in Coq.Lists.List]
y:83 [binder, in Coq.micromega.ZifyClasses]
y:83 [binder, in Coq.Classes.CRelationClasses]
y:83 [binder, in Coq.Reals.Rbasic_fun]
y:83 [binder, in Coq.Structures.EqualitiesFacts]
y:83 [binder, in Coq.PArith.BinPosDef]
y:83 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:83 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:83 [binder, in Coq.Relations.Relation_Operators]
y:83 [binder, in Coq.QArith.QArith_base]
y:83 [binder, in Coq.Structures.OrdersFacts]
y:84 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:84 [binder, in Coq.Logic.Eqdep_dec]
y:84 [binder, in Coq.FSets.FSetDecide]
y:84 [binder, in Coq.Reals.Rsqrt_def]
y:84 [binder, in Coq.MSets.MSetDecide]
y:84 [binder, in Coq.Init.Wf]
y:84 [binder, in Coq.Arith.PeanoNat]
y:84 [binder, in Coq.omega.OmegaLemmas]
y:84 [binder, in Coq.Structures.OrderedTypeEx]
y:84 [binder, in Coq.Reals.Rtopology]
y:84 [binder, in Coq.Structures.OrderedType]
y:84 [binder, in Coq.Reals.Ranalysis5]
y:84 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:84 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:84 [binder, in Coq.Logic.FinFun]
y:85 [binder, in Coq.QArith.Qcanon]
y:85 [binder, in Coq.Classes.RelationClasses]
y:85 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:85 [binder, in Coq.setoid_ring.Ring_theory]
y:85 [binder, in Coq.PArith.BinPosDef]
y:85 [binder, in Coq.Relations.Relation_Operators]
y:85 [binder, in Coq.Structures.OrdersFacts]
y:86 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:86 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:86 [binder, in Coq.MSets.MSetWeakList]
y:86 [binder, in Coq.Structures.OrderedTypeEx]
y:86 [binder, in Coq.Structures.OrderedType]
y:86 [binder, in Coq.Reals.Rbasic_fun]
y:86 [binder, in Coq.Reals.Ranalysis5]
y:86 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:86 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:86 [binder, in Coq.QArith.QArith_base]
y:86 [binder, in Coq.Lists.SetoidList]
y:87 [binder, in Coq.QArith.Qcanon]
y:87 [binder, in Coq.Reals.Ranalysis4]
y:87 [binder, in Coq.Reals.Exp_prop]
y:87 [binder, in Coq.omega.OmegaLemmas]
y:87 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:87 [binder, in Coq.micromega.ZifyInst]
y:87 [binder, in Coq.Relations.Relation_Operators]
y:87 [binder, in Coq.Logic.FinFun]
y:87 [binder, in Coq.FSets.FSetCompat]
y:87 [binder, in Coq.Structures.OrdersFacts]
y:87 [binder, in Coq.Reals.Cos_plus]
y:88 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:88 [binder, in Coq.Floats.SpecFloat]
y:88 [binder, in Coq.Reals.Rsqrt_def]
y:88 [binder, in Coq.Classes.CRelationClasses]
y:88 [binder, in Coq.Reals.Ranalysis5]
y:88 [binder, in Coq.QArith.QArith_base]
y:89 [binder, in Coq.Program.Wf]
y:89 [binder, in Coq.Logic.Eqdep_dec]
y:89 [binder, in Coq.Reals.Exp_prop]
y:89 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:89 [binder, in Coq.Structures.OrderedTypeEx]
y:89 [binder, in Coq.MSets.MSetGenTree]
y:89 [binder, in Coq.Structures.OrderedType]
y:89 [binder, in Coq.setoid_ring.Ring_theory]
y:89 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:89 [binder, in Coq.FSets.FSetCompat]
y:89 [binder, in Coq.Structures.OrdersFacts]
y:89 [binder, in Coq.Reals.Cos_plus]
y:9 [binder, in Coq.Relations.Operators_Properties]
y:9 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:9 [binder, in Coq.Logic.Eqdep_dec]
y:9 [binder, in Coq.Arith.Bool_nat]
y:9 [binder, in Coq.Logic.SetoidChoice]
y:9 [binder, in Coq.Reals.R_sqrt]
y:9 [binder, in Coq.Logic.ChoiceFacts]
y:9 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
y:9 [binder, in Coq.Logic.ClassicalUniqueChoice]
y:9 [binder, in Coq.Sets.Partial_Order]
y:9 [binder, in Coq.Classes.CRelationClasses]
y:9 [binder, in Coq.Structures.Equalities]
y:9 [binder, in Coq.Bool.BoolEq]
y:9 [binder, in Coq.Strings.Byte]
y:9 [binder, in Coq.Setoids.Setoid]
y:9 [binder, in Coq.Reals.R_sqr]
y:9 [binder, in Coq.Reals.ClassicalConstructiveReals]
y:9 [binder, in Coq.Logic.FinFun]
y:9 [binder, in Coq.Sets.Powerset]
y:90 [binder, in Coq.Program.Wf]
y:90 [binder, in Coq.Reals.Abstract.ConstructiveReals]
y:90 [binder, in Coq.QArith.Qcanon]
y:90 [binder, in Coq.FSets.FSetDecide]
y:90 [binder, in Coq.MSets.MSetDecide]
y:90 [binder, in Coq.Lists.ListSet]
y:90 [binder, in Coq.Reals.Ranalysis5]
y:90 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:90 [binder, in Coq.micromega.ZifyInst]
y:90 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
y:90 [binder, in Coq.QArith.QArith_base]
y:91 [binder, in Coq.Lists.List]
y:91 [binder, in Coq.setoid_ring.Ncring]
y:91 [binder, in Coq.Structures.OrdersFacts]
y:91 [binder, in Coq.Reals.Cos_plus]
y:92 [binder, in Coq.QArith.Qcanon]
y:92 [binder, in Coq.Logic.ChoiceFacts]
y:92 [binder, in Coq.Structures.OrderedType]
y:92 [binder, in Coq.Reals.Ratan]
y:92 [binder, in Coq.Reals.Ranalysis5]
y:92 [binder, in Coq.setoid_ring.Ring_theory]
y:92 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:92 [binder, in Coq.QArith.QArith_base]
y:93 [binder, in Coq.Logic.Eqdep_dec]
y:93 [binder, in Coq.Sorting.PermutSetoid]
y:93 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:93 [binder, in Coq.MSets.MSetWeakList]
y:93 [binder, in Coq.MSets.MSetGenTree]
y:93 [binder, in Coq.Lists.ListSet]
y:93 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:93 [binder, in Coq.Reals.Cos_rel]
y:93 [binder, in Coq.Lists.SetoidList]
y:93 [binder, in Coq.Structures.OrdersFacts]
y:932 [binder, in Coq.FSets.FMapAVL]
y:936 [binder, in Coq.FSets.FMapAVL]
y:94 [binder, in Coq.QArith.Qcanon]
y:94 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:94 [binder, in Coq.Floats.SpecFloat]
y:94 [binder, in Coq.Classes.CRelationClasses]
y:94 [binder, in Coq.Reals.PSeries_reg]
y:94 [binder, in Coq.Reals.Ranalysis5]
y:94 [binder, in Coq.setoid_ring.Ncring]
y:94 [binder, in Coq.QArith.QArith_base]
y:942 [binder, in Coq.FSets.FMapAVL]
y:946 [binder, in Coq.FSets.FMapAVL]
y:95 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:95 [binder, in Coq.Reals.Rsqrt_def]
y:95 [binder, in Coq.Init.Nat]
y:95 [binder, in Coq.Logic.Hurkens]
y:95 [binder, in Coq.Reals.Rtopology]
y:95 [binder, in Coq.Structures.OrderedType]
y:95 [binder, in Coq.setoid_ring.Ring_theory]
y:95 [binder, in Coq.Init.Logic]
y:95 [binder, in Coq.micromega.ZifyInst]
y:95 [binder, in Coq.Structures.OrdersFacts]
y:952 [binder, in Coq.FSets.FMapAVL]
y:958 [binder, in Coq.FSets.FMapAVL]
y:96 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:96 [binder, in Coq.Reals.Rfunctions]
y:96 [binder, in Coq.Lists.ListSet]
y:96 [binder, in Coq.Reals.PSeries_reg]
y:96 [binder, in Coq.Reals.Ratan]
y:96 [binder, in Coq.QArith.QArith_base]
y:964 [binder, in Coq.FSets.FMapAVL]
y:97 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:97 [binder, in Coq.QArith.Qcanon]
y:97 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:97 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
y:97 [binder, in Coq.Logic.Hurkens]
y:97 [binder, in Coq.MSets.MSetGenTree]
y:97 [binder, in Coq.Structures.OrderedType]
y:97 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:97 [binder, in Coq.Relations.Relation_Operators]
y:97 [binder, in Coq.Structures.OrdersFacts]
y:970 [binder, in Coq.FSets.FMapAVL]
y:976 [binder, in Coq.FSets.FMapAVL]
y:98 [binder, in Coq.Program.Wf]
y:98 [binder, in Coq.Logic.Eqdep_dec]
y:98 [binder, in Coq.FSets.FMapFacts]
y:98 [binder, in Coq.Reals.Ranalysis5]
y:98 [binder, in Coq.QArith.QArith_base]
y:984 [binder, in Coq.FSets.FMapAVL]
y:989 [binder, in Coq.FSets.FMapAVL]
y:99 [binder, in Coq.FSets.FSetBridge]
y:99 [binder, in Coq.Floats.SpecFloat]
y:99 [binder, in Coq.Reals.RiemannInt]
y:99 [binder, in Coq.FSets.FMapInterface]
y:99 [binder, in Coq.Structures.OrderedType]
y:99 [binder, in Coq.Lists.ListSet]
y:99 [binder, in Coq.Reals.Ratan]
y:99 [binder, in Coq.Structures.OrdersFacts]
y:994 [binder, in Coq.Lists.List]
| 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) |