| 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 | (70451 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 | (1003 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |
H (binder)
Ha:92 [in Coq.Arith.PeanoNat]Hbeq:21 [in Coq.Vectors.VectorEq]
Hb:23 [in Coq.ZArith.Zdiv]
Hb:33 [in Coq.ZArith.Zdiv]
Hdiff:220 [in Coq.Numbers.Cyclic.Int63.Int63]
heqij:143 [in Coq.Lists.SetoidList]
heqij:165 [in Coq.Lists.SetoidList]
heqss':144 [in Coq.Lists.SetoidList]
Heq:221 [in Coq.Numbers.Cyclic.Int63.Int63]
Heq:228 [in Coq.Numbers.Cyclic.Int63.Int63]
Heq:240 [in Coq.Numbers.Cyclic.Int63.Int63]
hf:110 [in Coq.Logic.FinFun]
hf:125 [in Coq.Logic.FinFun]
hf:129 [in Coq.Logic.FinFun]
Hf:328 [in Coq.Init.Logic]
Hf:333 [in Coq.Init.Logic]
high:25 [in Coq.Reals.Rsigma]
high:28 [in Coq.Reals.Rsigma]
high:3 [in Coq.Reals.Rsigma]
high:31 [in Coq.Reals.Rsigma]
high:33 [in Coq.Reals.Rsigma]
high:6 [in Coq.Reals.Rsigma]
Hi1:256 [in Coq.Vectors.VectorSpec]
Hi2:257 [in Coq.Vectors.VectorSpec]
Hi:230 [in Coq.Numbers.Cyclic.Int63.Int63]
Hi:249 [in Coq.Vectors.VectorSpec]
Hi:299 [in Coq.ZArith.BinInt]
hl:10 [in Coq.MSets.MSetAVL]
hl:28 [in Coq.FSets.FMapAVL]
Hl:386 [in Coq.FSets.FMapWeakList]
Hl:387 [in Coq.FSets.FMapWeakList]
Hm':315 [in Coq.FSets.FMapWeakList]
Hm':320 [in Coq.FSets.FMapWeakList]
Hm':325 [in Coq.FSets.FMapWeakList]
Hm':330 [in Coq.FSets.FMapWeakList]
Hm':361 [in Coq.FSets.FMapList]
Hm':391 [in Coq.FSets.FMapWeakList]
Hm':409 [in Coq.FSets.FMapWeakList]
Hm':426 [in Coq.FSets.FMapWeakList]
Hm':447 [in Coq.FSets.FMapWeakList]
Hm':463 [in Coq.FSets.FMapWeakList]
Hm':468 [in Coq.FSets.FMapList]
Hm':473 [in Coq.FSets.FMapWeakList]
Hm':474 [in Coq.FSets.FMapList]
Hm':480 [in Coq.FSets.FMapWeakList]
Hm':484 [in Coq.FSets.FMapList]
Hm':485 [in Coq.FSets.FMapWeakList]
Hm':493 [in Coq.FSets.FMapList]
Hm':500 [in Coq.FSets.FMapList]
Hm':505 [in Coq.FSets.FMapList]
Hm:155 [in Coq.FSets.FMapWeakList]
Hm:159 [in Coq.FSets.FMapWeakList]
Hm:164 [in Coq.FSets.FMapWeakList]
Hm:166 [in Coq.FSets.FMapList]
Hm:203 [in Coq.FSets.FMapWeakList]
Hm:207 [in Coq.FSets.FMapWeakList]
Hm:209 [in Coq.FSets.FMapList]
Hm:212 [in Coq.FSets.FMapWeakList]
Hm:213 [in Coq.FSets.FMapList]
Hm:217 [in Coq.FSets.FMapWeakList]
Hm:218 [in Coq.FSets.FMapList]
Hm:222 [in Coq.FSets.FMapWeakList]
Hm:223 [in Coq.FSets.FMapList]
Hm:228 [in Coq.FSets.FMapList]
Hm:232 [in Coq.FSets.FMapWeakList]
Hm:238 [in Coq.FSets.FMapList]
Hm:240 [in Coq.FSets.FMapList]
Hm:313 [in Coq.FSets.FMapWeakList]
Hm:318 [in Coq.FSets.FMapWeakList]
Hm:323 [in Coq.FSets.FMapWeakList]
Hm:328 [in Coq.FSets.FMapWeakList]
Hm:351 [in Coq.FSets.FMapWeakList]
Hm:359 [in Coq.FSets.FMapList]
Hm:362 [in Coq.FSets.FMapWeakList]
Hm:364 [in Coq.FSets.FMapList]
Hm:366 [in Coq.FSets.FMapList]
Hm:389 [in Coq.FSets.FMapWeakList]
Hm:397 [in Coq.FSets.FMapList]
Hm:407 [in Coq.FSets.FMapWeakList]
Hm:412 [in Coq.FSets.FMapList]
Hm:424 [in Coq.FSets.FMapWeakList]
Hm:44 [in Coq.FSets.FMapWeakList]
Hm:445 [in Coq.FSets.FMapWeakList]
Hm:461 [in Coq.FSets.FMapWeakList]
Hm:466 [in Coq.FSets.FMapList]
Hm:47 [in Coq.FSets.FMapWeakList]
Hm:471 [in Coq.FSets.FMapWeakList]
Hm:472 [in Coq.FSets.FMapList]
Hm:478 [in Coq.FSets.FMapWeakList]
Hm:482 [in Coq.FSets.FMapList]
Hm:483 [in Coq.FSets.FMapWeakList]
Hm:49 [in Coq.FSets.FMapList]
Hm:491 [in Coq.FSets.FMapList]
Hm:498 [in Coq.FSets.FMapList]
Hm:503 [in Coq.FSets.FMapList]
Hm:52 [in Coq.FSets.FMapList]
Hm:87 [in Coq.FSets.FMapWeakList]
Hm:91 [in Coq.FSets.FMapWeakList]
Hm:97 [in Coq.FSets.FMapList]
Hn:298 [in Coq.ZArith.BinInt]
hole:8 [in Coq.Reals.Runcountable]
Hp:275 [in Coq.ZArith.BinInt]
Hp:276 [in Coq.ZArith.BinInt]
Hp:280 [in Coq.ZArith.BinInt]
Hp:281 [in Coq.ZArith.BinInt]
Hqgt0:113 [in Coq.Reals.Cauchy.QExtra]
Hqgt0:115 [in Coq.Reals.Cauchy.QExtra]
Hqgt0:121 [in Coq.Reals.Cauchy.QExtra]
Hqgt0:124 [in Coq.Reals.Cauchy.QExtra]
Hrpos:115 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hrpos:147 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
hr:11 [in Coq.MSets.MSetAVL]
hr:29 [in Coq.FSets.FMapAVL]
Hs':111 [in Coq.MSets.MSetWeakList]
Hs':120 [in Coq.MSets.MSetWeakList]
Hs':129 [in Coq.MSets.MSetWeakList]
Hs':133 [in Coq.MSets.MSetWeakList]
Hs':137 [in Coq.MSets.MSetWeakList]
Hs':140 [in Coq.MSets.MSetList]
Hs':149 [in Coq.MSets.MSetList]
Hs':154 [in Coq.MSets.MSetList]
Hs':163 [in Coq.MSets.MSetList]
Hs':167 [in Coq.MSets.MSetList]
Hs':177 [in Coq.MSets.MSetList]
Hs':181 [in Coq.MSets.MSetList]
Hs':185 [in Coq.MSets.MSetList]
Hs:110 [in Coq.MSets.MSetWeakList]
Hs:111 [in Coq.MSets.MSetList]
Hs:119 [in Coq.MSets.MSetWeakList]
Hs:121 [in Coq.MSets.MSetList]
Hs:1223 [in Coq.FSets.FMapAVL]
Hs:125 [in Coq.MSets.MSetList]
Hs:128 [in Coq.MSets.MSetWeakList]
Hs:128 [in Coq.MSets.MSetGenTree]
Hs:132 [in Coq.MSets.MSetWeakList]
Hs:132 [in Coq.MSets.MSetList]
Hs:136 [in Coq.MSets.MSetWeakList]
Hs:139 [in Coq.MSets.MSetList]
Hs:142 [in Coq.MSets.MSetWeakList]
Hs:148 [in Coq.MSets.MSetList]
Hs:153 [in Coq.MSets.MSetList]
Hs:162 [in Coq.MSets.MSetList]
Hs:164 [in Coq.MSets.MSetWeakList]
Hs:166 [in Coq.MSets.MSetList]
Hs:168 [in Coq.MSets.MSetWeakList]
Hs:176 [in Coq.MSets.MSetList]
Hs:180 [in Coq.MSets.MSetList]
Hs:184 [in Coq.MSets.MSetList]
Hs:190 [in Coq.MSets.MSetList]
Hs:192 [in Coq.MSets.MSetList]
Hs:198 [in Coq.MSets.MSetList]
Hs:205 [in Coq.MSets.MSetList]
Hs:219 [in Coq.MSets.MSetList]
Hs:223 [in Coq.MSets.MSetList]
Hs:239 [in Coq.MSets.MSetList]
Hs:243 [in Coq.MSets.MSetList]
Hs:284 [in Coq.MSets.MSetGenTree]
HS:35 [in Coq.Vectors.VectorSpec]
HS:61 [in Coq.Vectors.Fin]
Hs:80 [in Coq.MSets.MSetWeakList]
Hs:87 [in Coq.MSets.MSetWeakList]
Hs:89 [in Coq.MSets.MSetList]
Hs:98 [in Coq.MSets.MSetWeakList]
Hxpos:137 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hxpos:139 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hxrange:366 [in Coq.Reals.Ratan]
Hxrange:380 [in Coq.Reals.Ratan]
Hx:178 [in Coq.Reals.Ratan]
Hx:186 [in Coq.Reals.Ratan]
Hx:47 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hx:53 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hx:7 [in Coq.QArith.Qcabs]
Hx:9 [in Coq.QArith.Qcabs]
hyps:27 [in Coq.rtauto.Rtauto]
hyps:32 [in Coq.rtauto.Rtauto]
hyps:35 [in Coq.rtauto.Rtauto]
hyps:39 [in Coq.rtauto.Rtauto]
hyps:44 [in Coq.rtauto.Rtauto]
hyps:50 [in Coq.rtauto.Rtauto]
hyps:54 [in Coq.rtauto.Rtauto]
hyps:57 [in Coq.rtauto.Rtauto]
hyps:63 [in Coq.rtauto.Rtauto]
hyps:73 [in Coq.rtauto.Rtauto]
Hy:48 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hy:54 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
h':101 [in Coq.Logic.FinFun]
h':107 [in Coq.Vectors.Fin]
h':115 [in Coq.Logic.Hurkens]
H':116 [in Coq.Logic.FunctionalExtensionality]
h':116 [in Coq.Logic.Hurkens]
h':198 [in Coq.Reals.Ratan]
h':258 [in Coq.Reals.Ranalysis1]
h':259 [in Coq.Reals.Ranalysis1]
h':261 [in Coq.Reals.Ranalysis1]
h':262 [in Coq.Reals.Ranalysis1]
h':271 [in Coq.Reals.Ranalysis1]
h':272 [in Coq.Reals.Ranalysis1]
h':274 [in Coq.Reals.Ranalysis1]
h':275 [in Coq.Reals.Ranalysis1]
h':291 [in Coq.ssr.ssrfun]
h':293 [in Coq.ssr.ssrfun]
H':491 [in Coq.ZArith.BinInt]
h':652 [in Coq.ssr.ssrbool]
H':81 [in Coq.Classes.RelationClasses]
H':88 [in Coq.Classes.RelationClasses]
H':90 [in Coq.Classes.CRelationClasses]
H':97 [in Coq.Classes.CRelationClasses]
h0:101 [in Coq.Logic.Hurkens]
H0:106 [in Coq.MSets.MSetWeakList]
H0:11 [in Coq.Classes.Morphisms_Prop]
H0:115 [in Coq.MSets.MSetWeakList]
H0:120 [in Coq.MSets.MSetInterface]
H0:122 [in Coq.Classes.Morphisms]
H0:124 [in Coq.MSets.MSetInterface]
H0:124 [in Coq.MSets.MSetWeakList]
h0:127 [in Coq.Logic.Hurkens]
H0:128 [in Coq.MSets.MSetInterface]
h0:129 [in Coq.Logic.Hurkens]
H0:144 [in Coq.setoid_ring.Ncring_tac]
H0:144 [in Coq.MSets.MSetList]
H0:144 [in Coq.Classes.CMorphisms]
H0:146 [in Coq.MSets.MSetInterface]
H0:149 [in Coq.MSets.MSetInterface]
H0:157 [in Coq.Classes.Morphisms]
H0:158 [in Coq.MSets.MSetList]
H0:159 [in Coq.MSets.MSetInterface]
H0:162 [in Coq.MSets.MSetInterface]
H0:165 [in Coq.MSets.MSetInterface]
H0:172 [in Coq.MSets.MSetList]
H0:173 [in Coq.Classes.Morphisms]
H0:179 [in Coq.Classes.Morphisms]
H0:187 [in Coq.Classes.CMorphisms]
H0:188 [in Coq.Classes.Morphisms]
H0:194 [in Coq.Classes.Morphisms]
H0:195 [in Coq.setoid_ring.Ncring_tac]
H0:203 [in Coq.Classes.CMorphisms]
H0:209 [in Coq.Classes.CMorphisms]
H0:213 [in Coq.Classes.Morphisms]
H0:218 [in Coq.Classes.CMorphisms]
H0:219 [in Coq.Classes.Morphisms]
H0:223 [in Coq.Classes.CMorphisms]
H0:229 [in Coq.Classes.CMorphisms]
H0:237 [in Coq.Classes.CMorphisms]
H0:24 [in Coq.Classes.RelationPairs]
H0:256 [in Coq.Classes.CMorphisms]
H0:258 [in Coq.MSets.MSetInterface]
H0:262 [in Coq.Classes.CMorphisms]
H0:263 [in Coq.MSets.MSetGenTree]
H0:27 [in Coq.Classes.RelationPairs]
H0:271 [in Coq.MSets.MSetInterface]
H0:280 [in Coq.MSets.MSetRBT]
H0:291 [in Coq.MSets.MSetRBT]
H0:30 [in Coq.Classes.RelationPairs]
H0:302 [in Coq.MSets.MSetRBT]
H0:324 [in Coq.MSets.MSetGenTree]
H0:329 [in Coq.MSets.MSetRBT]
H0:33 [in Coq.Classes.RelationPairs]
H0:336 [in Coq.MSets.MSetGenTree]
H0:340 [in Coq.MSets.MSetRBT]
H0:36 [in Coq.Classes.RelationPairs]
H0:370 [in Coq.MSets.MSetRBT]
H0:373 [in Coq.MSets.MSetGenTree]
H0:377 [in Coq.MSets.MSetGenTree]
H0:39 [in Coq.Classes.RelationPairs]
H0:44 [in Coq.Classes.EquivDec]
H0:45 [in Coq.Classes.RelationPairs]
H0:464 [in Coq.MSets.MSetRBT]
H0:47 [in Coq.Classes.RelationPairs]
H0:49 [in Coq.Classes.RelationPairs]
H0:491 [in Coq.MSets.MSetRBT]
H0:495 [in Coq.MSets.MSetRBT]
H0:499 [in Coq.MSets.MSetRBT]
H0:503 [in Coq.MSets.MSetAVL]
H0:51 [in Coq.Classes.RelationPairs]
H0:51 [in Coq.Vectors.Fin]
H0:514 [in Coq.MSets.MSetAVL]
H0:517 [in Coq.MSets.MSetRBT]
H0:524 [in Coq.MSets.MSetRBT]
H0:528 [in Coq.MSets.MSetRBT]
H0:535 [in Coq.MSets.MSetAVL]
H0:537 [in Coq.MSets.MSetRBT]
H0:54 [in Coq.Classes.EquivDec]
H0:545 [in Coq.MSets.MSetRBT]
H0:552 [in Coq.MSets.MSetRBT]
H0:559 [in Coq.MSets.MSetAVL]
H0:559 [in Coq.MSets.MSetRBT]
H0:568 [in Coq.MSets.MSetRBT]
H0:576 [in Coq.MSets.MSetAVL]
H0:577 [in Coq.MSets.MSetRBT]
H0:607 [in Coq.MSets.MSetAVL]
H0:613 [in Coq.MSets.MSetAVL]
H0:617 [in Coq.MSets.MSetAVL]
H0:621 [in Coq.MSets.MSetAVL]
H0:627 [in Coq.MSets.MSetAVL]
H0:631 [in Coq.MSets.MSetAVL]
H0:636 [in Coq.MSets.MSetAVL]
H0:640 [in Coq.MSets.MSetAVL]
H0:80 [in Coq.Classes.Morphisms]
H0:84 [in Coq.Classes.CMorphisms]
h0:99 [in Coq.Logic.Hurkens]
H1':288 [in Coq.Init.Logic]
H1:10 [in Coq.Reals.Rtrigo_fun]
H1:100 [in Coq.Reals.Rderiv]
H1:102 [in Coq.Reals.Rderiv]
H1:103 [in Coq.Logic.EqdepFacts]
H1:104 [in Coq.Reals.Rderiv]
H1:12 [in Coq.Reals.Rtrigo_fun]
H1:135 [in Coq.Reals.Rderiv]
H1:137 [in Coq.Reals.Rderiv]
H1:139 [in Coq.Reals.Rderiv]
H1:14 [in Coq.Reals.Rtrigo_fun]
H1:16 [in Coq.Reals.Rderiv]
H1:16 [in Coq.Reals.Rtrigo_fun]
H1:164 [in Coq.Reals.Rderiv]
H1:166 [in Coq.Reals.Rderiv]
H1:168 [in Coq.Reals.Rderiv]
H1:18 [in Coq.Reals.Rderiv]
H1:18 [in Coq.Reals.Rtrigo_fun]
H1:183 [in Coq.Classes.Morphisms]
H1:196 [in Coq.Classes.Morphisms]
H1:2 [in Coq.Reals.Rtrigo_fun]
H1:20 [in Coq.Reals.Rderiv]
H1:20 [in Coq.Reals.Rtrigo_fun]
h1:21 [in Coq.Numbers.Natural.Abstract.NStrongRec]
H1:210 [in Coq.Bool.Bool]
H1:213 [in Coq.Classes.CMorphisms]
H1:214 [in Coq.Classes.Morphisms]
H1:22 [in Coq.Reals.Rderiv]
H1:22 [in Coq.Reals.Rtrigo_fun]
H1:220 [in Coq.Classes.Morphisms]
H1:231 [in Coq.Classes.CMorphisms]
H1:239 [in Coq.Classes.CMorphisms]
H1:24 [in Coq.Reals.Rderiv]
H1:24 [in Coq.Reals.Rtrigo_fun]
H1:257 [in Coq.Classes.CMorphisms]
H1:26 [in Coq.Reals.Rderiv]
H1:26 [in Coq.Reals.Rtrigo_fun]
H1:263 [in Coq.Classes.CMorphisms]
H1:28 [in Coq.Reals.Rderiv]
H1:28 [in Coq.Reals.Rtrigo_fun]
H1:286 [in Coq.Init.Logic]
H1:30 [in Coq.Reals.Rderiv]
H1:30 [in Coq.Reals.Rtrigo_fun]
H1:32 [in Coq.Reals.Rderiv]
H1:32 [in Coq.Reals.Rtrigo_fun]
H1:322 [in Coq.Init.Logic]
H1:326 [in Coq.MSets.MSetGenTree]
H1:34 [in Coq.Reals.Rderiv]
H1:34 [in Coq.Reals.Rtrigo_fun]
H1:36 [in Coq.Reals.Rderiv]
H1:36 [in Coq.Reals.Rtrigo_fun]
H1:38 [in Coq.Reals.Rderiv]
H1:39 [in Coq.Reals.Rfunctions]
H1:4 [in Coq.Reals.Rfunctions]
H1:4 [in Coq.Reals.Rtrigo_fun]
H1:40 [in Coq.Reals.Rderiv]
H1:41 [in Coq.Reals.Rfunctions]
H1:42 [in Coq.Reals.Rderiv]
H1:43 [in Coq.Reals.Rfunctions]
H1:44 [in Coq.Reals.Rderiv]
H1:44 [in Coq.Vectors.VectorSpec]
H1:46 [in Coq.Reals.Rderiv]
H1:47 [in Coq.Reals.Rfunctions]
H1:48 [in Coq.Reals.Rderiv]
H1:49 [in Coq.Reals.Rfunctions]
H1:50 [in Coq.Reals.Rderiv]
H1:51 [in Coq.Reals.Rfunctions]
H1:54 [in Coq.Vectors.Fin]
H1:562 [in Coq.MSets.MSetAVL]
H1:579 [in Coq.MSets.MSetAVL]
H1:6 [in Coq.Reals.Rfunctions]
H1:6 [in Coq.Reals.Rtrigo_fun]
H1:64 [in Coq.Reals.Rfunctions]
H1:66 [in Coq.Reals.Rfunctions]
H1:68 [in Coq.Reals.Rfunctions]
h1:72 [in Coq.Numbers.Natural.Abstract.NDefOps]
H1:75 [in Coq.Logic.EqdepFacts]
H1:77 [in Coq.Reals.Rfunctions]
H1:79 [in Coq.Reals.Rfunctions]
H1:8 [in Coq.Reals.Rtrigo_fun]
H1:81 [in Coq.Vectors.VectorSpec]
H1:81 [in Coq.Reals.Rfunctions]
H1:82 [in Coq.Logic.EqdepFacts]
H1:89 [in Coq.Vectors.VectorSpec]
H1:89 [in Coq.Logic.EqdepFacts]
H1:96 [in Coq.Logic.EqdepFacts]
H2':289 [in Coq.Init.Logic]
H2:101 [in Coq.Reals.Rderiv]
H2:103 [in Coq.Reals.Rderiv]
H2:104 [in Coq.Logic.EqdepFacts]
H2:105 [in Coq.Reals.Rderiv]
H2:11 [in Coq.Reals.Rtrigo_fun]
H2:13 [in Coq.Reals.Rtrigo_fun]
H2:136 [in Coq.Reals.Rderiv]
H2:138 [in Coq.Reals.Rderiv]
H2:140 [in Coq.Reals.Rderiv]
H2:15 [in Coq.Reals.Rtrigo_fun]
H2:165 [in Coq.Reals.Rderiv]
H2:167 [in Coq.Reals.Rderiv]
H2:169 [in Coq.Reals.Rderiv]
H2:17 [in Coq.Reals.Rderiv]
H2:17 [in Coq.Reals.Rtrigo_fun]
H2:19 [in Coq.Reals.Rderiv]
H2:19 [in Coq.Reals.Rtrigo_fun]
H2:21 [in Coq.Reals.Rderiv]
H2:21 [in Coq.Reals.Rtrigo_fun]
H2:211 [in Coq.Bool.Bool]
h2:22 [in Coq.Numbers.Natural.Abstract.NStrongRec]
H2:23 [in Coq.Reals.Rderiv]
H2:23 [in Coq.Reals.Rtrigo_fun]
H2:25 [in Coq.Reals.Rderiv]
H2:25 [in Coq.Reals.Rtrigo_fun]
H2:27 [in Coq.Reals.Rderiv]
H2:27 [in Coq.Reals.Rtrigo_fun]
H2:287 [in Coq.Init.Logic]
H2:29 [in Coq.Reals.Rderiv]
H2:29 [in Coq.Reals.Rtrigo_fun]
H2:3 [in Coq.Reals.Rtrigo_fun]
H2:31 [in Coq.Reals.Rderiv]
H2:31 [in Coq.Reals.Rtrigo_fun]
H2:323 [in Coq.Init.Logic]
H2:33 [in Coq.Reals.Rderiv]
H2:33 [in Coq.Reals.Rtrigo_fun]
H2:35 [in Coq.Reals.Rderiv]
H2:35 [in Coq.Reals.Rtrigo_fun]
H2:37 [in Coq.Reals.Rderiv]
H2:37 [in Coq.Reals.Rtrigo_fun]
H2:39 [in Coq.Reals.Rderiv]
H2:40 [in Coq.Reals.Rfunctions]
H2:41 [in Coq.Reals.Rderiv]
H2:42 [in Coq.Reals.Rfunctions]
H2:43 [in Coq.Reals.Rderiv]
H2:44 [in Coq.Reals.Rfunctions]
H2:45 [in Coq.Reals.Rderiv]
H2:45 [in Coq.Vectors.VectorSpec]
H2:47 [in Coq.Reals.Rderiv]
H2:48 [in Coq.Reals.Rfunctions]
H2:49 [in Coq.Reals.Rderiv]
H2:5 [in Coq.Reals.Rfunctions]
H2:5 [in Coq.Reals.Rtrigo_fun]
H2:50 [in Coq.Reals.Rfunctions]
H2:51 [in Coq.Reals.Rderiv]
H2:52 [in Coq.Reals.Rfunctions]
H2:57 [in Coq.Vectors.Fin]
H2:65 [in Coq.Reals.Rfunctions]
H2:67 [in Coq.Reals.Rfunctions]
h2:68 [in Coq.Vectors.VectorDef]
H2:69 [in Coq.Reals.Rfunctions]
H2:7 [in Coq.Reals.Rfunctions]
H2:7 [in Coq.Reals.Rtrigo_fun]
h2:73 [in Coq.Numbers.Natural.Abstract.NDefOps]
H2:76 [in Coq.Logic.EqdepFacts]
H2:78 [in Coq.Reals.Rfunctions]
H2:80 [in Coq.Reals.Rfunctions]
H2:82 [in Coq.Vectors.VectorSpec]
H2:82 [in Coq.Reals.Rfunctions]
H2:83 [in Coq.Logic.EqdepFacts]
H2:9 [in Coq.Reals.Rtrigo_fun]
H2:90 [in Coq.Vectors.VectorSpec]
H2:90 [in Coq.Logic.EqdepFacts]
H2:97 [in Coq.Logic.EqdepFacts]
h:1 [in Coq.Reals.Sqrt_reg]
H:10 [in Coq.setoid_ring.Ncring_initial]
H:10 [in Coq.Classes.Morphisms_Prop]
H:10 [in Coq.Classes.DecidableClass]
H:10 [in Coq.Init.Tactics]
H:10 [in Coq.Bool.DecBool]
H:100 [in Coq.Classes.RelationClasses]
h:100 [in Coq.Logic.FunctionalExtensionality]
h:100 [in Coq.Reals.PSeries_reg]
h:100 [in Coq.Logic.FinFun]
h:101 [in Coq.Reals.MVT]
H:101 [in Coq.Classes.Morphisms]
H:101 [in Coq.Classes.CRelationClasses]
H:101 [in Coq.Vectors.Fin]
H:102 [in Coq.Classes.RelationClasses]
h:102 [in Coq.Reals.MVT]
H:102 [in Coq.Classes.CMorphisms]
H:103 [in Coq.Classes.CRelationClasses]
H:103 [in Coq.Vectors.Fin]
H:104 [in Coq.Classes.RelationClasses]
H:104 [in Coq.Classes.Morphisms]
H:104 [in Coq.omega.OmegaLemmas]
H:105 [in Coq.Logic.EqdepFacts]
H:105 [in Coq.Logic.FunctionalExtensionality]
H:105 [in Coq.MSets.MSetWeakList]
H:105 [in Coq.Classes.CRelationClasses]
h:106 [in Coq.Logic.Eqdep_dec]
H:106 [in Coq.setoid_ring.Ncring_tac]
h:106 [in Coq.Reals.RiemannInt]
H:106 [in Coq.Classes.CMorphisms]
h:106 [in Coq.Vectors.Fin]
H:107 [in Coq.Classes.Morphisms]
h:107 [in Coq.Logic.FunctionalExtensionality]
H:107 [in Coq.Classes.CRelationClasses]
H:107 [in Coq.Vectors.VectorDef]
H:108 [in Coq.Classes.RelationClasses]
h:1086 [in Coq.FSets.FMapAVL]
H:109 [in Coq.Classes.Morphisms]
H:109 [in Coq.Classes.CRelationClasses]
h:1092 [in Coq.FSets.FMapAVL]
h:1099 [in Coq.FSets.FMapAVL]
h:11 [in Coq.Reals.PSeries_reg]
h:110 [in Coq.Logic.EqdepFacts]
H:110 [in Coq.Classes.CMorphisms]
h:1104 [in Coq.FSets.FMapAVL]
h:1109 [in Coq.FSets.FMapAVL]
H:111 [in Coq.Classes.Morphisms]
h:111 [in Coq.Reals.RiemannInt]
H:111 [in Coq.Classes.CRelationClasses]
H:112 [in Coq.MSets.MSetInterface]
h:112 [in Coq.Vectors.Fin]
H:113 [in Coq.omega.OmegaLemmas]
H:113 [in Coq.Classes.CRelationClasses]
h:113 [in Coq.Logic.FinFun]
H:114 [in Coq.MSets.MSetWeakList]
H:114 [in Coq.Classes.CMorphisms]
H:115 [in Coq.MSets.MSetInterface]
h:116 [in Coq.Reals.Ranalysis1]
H:116 [in Coq.Classes.Morphisms]
h:116 [in Coq.Vectors.VectorDef]
H:117 [in Coq.MSets.MSetList]
H:117 [in Coq.Classes.CRelationClasses]
h:118 [in Coq.Logic.FunctionalExtensionality]
H:118 [in Coq.Classes.CMorphisms]
H:119 [in Coq.MSets.MSetInterface]
h:119 [in Coq.Vectors.VectorDef]
h:12 [in Coq.Init.Number]
H:12 [in Coq.Classes.CMorphisms]
h:12 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
H:12 [in Coq.Classes.SetoidClass]
H:12 [in Coq.Classes.DecidableClass]
H:120 [in Coq.Classes.Morphisms]
h:120 [in Coq.Reals.Rpower]
H:120 [in Coq.omega.OmegaLemmas]
H:121 [in Coq.setoid_ring.Ncring_tac]
H:121 [in Coq.Classes.CMorphisms]
h:122 [in Coq.Logic.FinFun]
H:123 [in Coq.MSets.MSetInterface]
H:123 [in Coq.MSets.MSetWeakList]
H:124 [in Coq.Classes.CMorphisms]
H:125 [in Coq.Vectors.VectorDef]
H:127 [in Coq.MSets.MSetInterface]
H:127 [in Coq.Classes.Morphisms]
H:127 [in Coq.omega.OmegaLemmas]
H:127 [in Coq.setoid_ring.Ncring]
H:128 [in Coq.MSets.MSetList]
H:129 [in Coq.Reals.Runcountable]
h:129 [in Coq.Vectors.VectorDef]
h:13 [in Coq.Reals.Runcountable]
h:13 [in Coq.Reals.Ranalysis4]
H:13 [in Coq.Classes.Morphisms]
h:13 [in Coq.Program.Combinators]
H:130 [in Coq.Classes.Morphisms]
H:131 [in Coq.MSets.MSetInterface]
H:131 [in Coq.setoid_ring.Ncring_tac]
h:131 [in Coq.Logic.FinFun]
H:132 [in Coq.Classes.Morphisms]
H:133 [in Coq.Classes.CMorphisms]
H:134 [in Coq.MSets.MSetInterface]
h:134 [in Coq.Logic.Hurkens]
h:135 [in Coq.Logic.Eqdep_dec]
H:135 [in Coq.omega.OmegaLemmas]
H:137 [in Coq.MSets.MSetInterface]
H:137 [in Coq.Classes.Morphisms]
h:138 [in Coq.Vectors.VectorDef]
h:138 [in Coq.Logic.FinFun]
H:139 [in Coq.Vectors.VectorDef]
h:14 [in Coq.Reals.Ranalysis4]
H:14 [in Coq.Classes.DecidableClass]
H:141 [in Coq.omega.OmegaLemmas]
H:141 [in Coq.Classes.CRelationClasses]
h:141 [in Coq.Logic.FinFun]
H:142 [in Coq.Classes.CMorphisms]
H:143 [in Coq.MSets.MSetInterface]
H:143 [in Coq.MSets.MSetList]
H:145 [in Coq.MSets.MSetInterface]
h:145 [in Coq.Reals.RiemannInt]
H:146 [in Coq.Classes.CRelationClasses]
H:147 [in Coq.omega.OmegaLemmas]
h:148 [in Coq.Reals.Ranalysis1]
H:148 [in Coq.MSets.MSetInterface]
H:148 [in Coq.setoid_ring.Ncring]
h:148 [in Coq.Vectors.VectorDef]
h:149 [in Coq.Reals.Ranalysis1]
h:149 [in Coq.Reals.RiemannInt]
h:149 [in Coq.Vectors.VectorDef]
h:15 [in Coq.Reals.Ranalysis4]
h:15 [in Coq.ZArith.Zcompare]
h:150 [in Coq.Reals.Ranalysis1]
H:150 [in Coq.Vectors.VectorDef]
h:151 [in Coq.Reals.Ranalysis1]
H:151 [in Coq.MSets.MSetWeakList]
h:152 [in Coq.Reals.Ranalysis1]
h:153 [in Coq.Reals.Ranalysis1]
H:153 [in Coq.MSets.MSetInterface]
H:153 [in Coq.omega.OmegaLemmas]
h:154 [in Coq.Reals.Ranalysis1]
h:155 [in Coq.Reals.Ranalysis1]
H:155 [in Coq.MSets.MSetInterface]
H:155 [in Coq.Classes.Morphisms]
H:156 [in Coq.omega.OmegaLemmas]
H:156 [in Coq.Classes.CMorphisms]
H:157 [in Coq.MSets.MSetList]
H:157 [in Coq.Init.Logic]
h:158 [in Coq.Numbers.DecimalFacts]
H:158 [in Coq.MSets.MSetInterface]
h:158 [in Coq.Numbers.HexadecimalFacts]
h:159 [in Coq.Reals.Ranalysis1]
H:159 [in Coq.setoid_ring.Ncring_tac]
H:159 [in Coq.omega.OmegaLemmas]
h:16 [in Coq.Reals.Ranalysis2]
h:16 [in Coq.Reals.Ranalysis4]
H:16 [in Coq.Classes.CMorphisms]
H:16 [in Coq.Bool.BoolEq]
H:16 [in Coq.Classes.DecidableClass]
H:16 [in Coq.Bool.DecBool]
h:160 [in Coq.Reals.Ranalysis1]
H:160 [in Coq.Classes.CMorphisms]
H:161 [in Coq.MSets.MSetInterface]
h:161 [in Coq.FSets.FMapAVL]
H:163 [in Coq.omega.OmegaLemmas]
H:163 [in Coq.Classes.CMorphisms]
h:164 [in Coq.Reals.Ranalysis1]
H:164 [in Coq.MSets.MSetInterface]
h:165 [in Coq.Reals.Ranalysis1]
h:165 [in Coq.FSets.FMapAVL]
H:167 [in Coq.omega.OmegaLemmas]
h:168 [in Coq.Reals.RiemannInt]
H:168 [in Coq.MSets.MSetRBT]
H:168 [in Coq.NArith.Ndigits]
H:169 [in Coq.Classes.Morphisms]
H:169 [in Coq.Init.Logic]
h:17 [in Coq.Reals.Ranalysis4]
H:17 [in Coq.Classes.Morphisms]
H:17 [in Coq.Classes.SetoidClass]
h:17 [in Coq.Reals.PSeries_reg]
h:170 [in Coq.FSets.FMapAVL]
H:170 [in Coq.Classes.CMorphisms]
H:170 [in Coq.MSets.MSetRBT]
H:171 [in Coq.MSets.MSetInterface]
H:171 [in Coq.MSets.MSetList]
H:171 [in Coq.omega.OmegaLemmas]
H:172 [in Coq.setoid_ring.Ncring_tac]
h:172 [in Coq.Reals.RiemannInt]
H:173 [in Coq.MSets.MSetWeakList]
H:173 [in Coq.NArith.Ndigits]
h:173 [in Coq.Logic.ClassicalFacts]
H:174 [in Coq.Init.Logic]
H:176 [in Coq.micromega.ZifyClasses]
H:176 [in Coq.Classes.RelationClasses]
H:176 [in Coq.Classes.Morphisms]
H:176 [in Coq.MSets.MSetWeakList]
H:176 [in Coq.Arith.PeanoNat]
H:176 [in Coq.omega.OmegaLemmas]
H:177 [in Coq.micromega.ZifyClasses]
h:177 [in Coq.Logic.EqdepFacts]
h:177 [in Coq.Reals.RiemannInt]
h:177 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
h:178 [in Coq.FSets.FMapAVL]
h:179 [in Coq.PArith.BinPos]
h:18 [in Coq.Reals.Runcountable]
H:18 [in Coq.setoid_ring.Ncring]
H:180 [in Coq.MSets.MSetGenTree]
H:180 [in Coq.Init.Logic]
h:181 [in Coq.Vectors.VectorSpec]
H:181 [in Coq.Classes.RelationClasses]
h:181 [in Coq.Reals.RiemannInt]
H:181 [in Coq.omega.OmegaLemmas]
H:182 [in Coq.MSets.MSetInterface]
H:182 [in Coq.setoid_ring.Ncring_tac]
h:183 [in Coq.FSets.FMapAVL]
H:184 [in Coq.omega.OmegaLemmas]
h:185 [in Coq.Vectors.VectorSpec]
h:185 [in Coq.Logic.ChoiceFacts]
H:185 [in Coq.Classes.CMorphisms]
H:186 [in Coq.Classes.Morphisms]
h:187 [in Coq.Reals.RiemannInt]
h:187 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
h:188 [in Coq.FSets.FMapAVL]
H:188 [in Coq.omega.OmegaLemmas]
h:189 [in Coq.Logic.ChoiceFacts]
h:19 [in Coq.Reals.Ranalysis2]
H:19 [in Coq.Classes.SetoidDec]
H:191 [in Coq.Classes.Morphisms]
H:191 [in Coq.Vectors.Fin]
h:191 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
H:192 [in Coq.omega.OmegaLemmas]
H:192 [in Coq.Vectors.Fin]
h:193 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
H:195 [in Coq.Vectors.Fin]
h:196 [in Coq.Logic.ChoiceFacts]
H:196 [in Coq.Vectors.Fin]
H:197 [in Coq.omega.OmegaLemmas]
h:197 [in Coq.Reals.Ratan]
H:199 [in Coq.Classes.CMorphisms]
h:2 [in Coq.Reals.Ranalysis2]
H:2 [in Coq.btauto.Algebra]
H:20 [in Coq.Bool.BoolEq]
H:200 [in Coq.setoid_ring.Ncring_tac]
H:201 [in Coq.omega.OmegaLemmas]
H:202 [in Coq.Classes.Morphisms]
H:204 [in Coq.omega.OmegaLemmas]
H:205 [in Coq.Vectors.Fin]
h:206 [in Coq.FSets.FMapAVL]
H:206 [in Coq.Classes.CMorphisms]
H:206 [in Coq.Vectors.Fin]
H:208 [in Coq.Classes.Morphisms]
H:208 [in Coq.Init.Specif]
H:209 [in Coq.Vectors.Fin]
h:21 [in Coq.Numbers.Natural.Abstract.NBits]
h:21 [in Coq.Numbers.Integer.Abstract.ZBits]
H:210 [in Coq.Vectors.Fin]
H:211 [in Coq.Classes.Morphisms]
H:211 [in Coq.Vectors.VectorDef]
H:216 [in Coq.Classes.CMorphisms]
H:217 [in Coq.Classes.Morphisms]
h:219 [in Coq.Logic.EqdepFacts]
H:219 [in Coq.Logic.ChoiceFacts]
H:22 [in Coq.Classes.EquivDec]
H:221 [in Coq.Classes.CMorphisms]
H:222 [in Coq.Logic.ChoiceFacts]
h:225 [in Coq.Logic.EqdepFacts]
H:226 [in Coq.MSets.MSetList]
H:226 [in Coq.Classes.CMorphisms]
h:229 [in Coq.Logic.EqdepFacts]
H:23 [in Coq.Classes.RelationPairs]
H:234 [in Coq.Numbers.Cyclic.Int63.Int63]
H:234 [in Coq.Classes.CMorphisms]
h:238 [in Coq.Logic.Hurkens]
H:238 [in Coq.Vectors.VectorDef]
h:239 [in Coq.Logic.Hurkens]
H:24 [in Coq.Classes.SetoidDec]
H:24 [in Coq.Logic.Diaconescu]
H:24 [in Coq.Vectors.VectorDef]
H:245 [in Coq.Classes.CMorphisms]
H:246 [in Coq.MSets.MSetList]
H:246 [in Coq.MSets.MSetGenTree]
H:249 [in Coq.MSets.MSetList]
h:25 [in Coq.Reals.Runcountable]
h:25 [in Coq.Reals.Ranalysis5]
H:25 [in Coq.Logic.Diaconescu]
h:251 [in Coq.Logic.Hurkens]
H:251 [in Coq.Classes.CMorphisms]
h:252 [in Coq.Logic.Hurkens]
H:253 [in Coq.MSets.MSetGenTree]
H:254 [in Coq.Classes.CMorphisms]
h:256 [in Coq.Reals.Ranalysis1]
h:257 [in Coq.Reals.Ranalysis1]
H:257 [in Coq.MSets.MSetInterface]
h:26 [in Coq.Logic.EqdepFacts]
H:26 [in Coq.Classes.RelationPairs]
h:260 [in Coq.Reals.Ranalysis1]
H:260 [in Coq.MSets.MSetInterface]
H:260 [in Coq.Classes.CMorphisms]
h:262 [in Coq.ssr.ssrfun]
H:262 [in Coq.MSets.MSetGenTree]
h:263 [in Coq.Reals.Ranalysis1]
H:263 [in Coq.MSets.MSetInterface]
H:263 [in Coq.setoid_ring.Ncring_tac]
h:265 [in Coq.NArith.BinNat]
H:267 [in Coq.MSets.MSetInterface]
h:269 [in Coq.Reals.Ranalysis1]
h:269 [in Coq.Reals.Ranalysis5]
H:27 [in Coq.Logic.Eqdep_dec]
h:27 [in Coq.Reals.PSeries_reg]
H:27 [in Coq.setoid_ring.Ncring]
h:270 [in Coq.Reals.Ranalysis1]
H:270 [in Coq.MSets.MSetInterface]
H:271 [in Coq.MSets.MSetGenTree]
h:272 [in Coq.Reals.Ranalysis5]
h:273 [in Coq.Reals.Ranalysis1]
h:273 [in Coq.Reals.Ranalysis5]
h:274 [in Coq.Reals.Ranalysis5]
H:275 [in Coq.MSets.MSetGenTree]
h:275 [in Coq.Reals.Ranalysis5]
H:275 [in Coq.Init.Logic]
h:276 [in Coq.Reals.Ranalysis1]
h:276 [in Coq.Reals.Ranalysis5]
H:277 [in Coq.setoid_ring.Ncring_tac]
H:277 [in Coq.MSets.MSetGenTree]
H:279 [in Coq.Init.Specif]
H:279 [in Coq.MSets.MSetRBT]
H:28 [in Coq.Logic.FunctionalExtensionality]
H:28 [in Coq.Classes.EquivDec]
h:28 [in Coq.Reals.PSeries_reg]
h:280 [in Coq.Reals.Ranalysis5]
h:284 [in Coq.Reals.Ranalysis5]
H:29 [in Coq.Vectors.VectorSpec]
h:29 [in Coq.Reals.Ranalysis2]
H:29 [in Coq.Classes.RelationPairs]
H:29 [in Coq.MSets.MSetFacts]
H:29 [in Coq.Classes.SetoidDec]
h:29 [in Coq.Reals.PSeries_reg]
H:290 [in Coq.MSets.MSetRBT]
H:292 [in Coq.ZArith.BinInt]
H:295 [in Coq.ZArith.BinInt]
H:297 [in Coq.Init.Logic]
H:3 [in Coq.Classes.CEquivalence]
H:3 [in Coq.Classes.Equivalence]
h:30 [in Coq.Reals.PSeries_reg]
h:30 [in Coq.Reals.Ranalysis5]
H:301 [in Coq.MSets.MSetRBT]
H:308 [in Coq.Init.Logic]
h:31 [in Coq.Reals.Runcountable]
H:31 [in Coq.MSets.MSetFacts]
h:31 [in Coq.Reals.PSeries_reg]
h:31 [in Coq.Reals.Ranalysis5]
h:31 [in Coq.Vectors.VectorDef]
H:310 [in Coq.NArith.BinNat]
H:310 [in Coq.MSets.MSetRBT]
H:314 [in Coq.Init.Logic]
H:317 [in Coq.MSets.MSetRBT]
h:319 [in Coq.Vectors.VectorDef]
H:32 [in Coq.Classes.RelationPairs]
h:32 [in Coq.Reals.PSeries_reg]
H:320 [in Coq.MSets.MSetRBT]
H:320 [in Coq.Vectors.VectorDef]
H:323 [in Coq.MSets.MSetGenTree]
H:328 [in Coq.MSets.MSetRBT]
h:33 [in Coq.Logic.ExtensionalityFacts]
h:33 [in Coq.Reals.PSeries_reg]
H:331 [in Coq.Numbers.Cyclic.Int63.Int63]
H:335 [in Coq.MSets.MSetGenTree]
H:339 [in Coq.MSets.MSetRBT]
H:34 [in Coq.Vectors.VectorSpec]
H:34 [in Coq.Classes.EquivDec]
h:34 [in Coq.Reals.PSeries_reg]
H:34 [in Coq.Vectors.VectorDef]
H:343 [in Coq.Numbers.Cyclic.Int63.Int63]
H:346 [in Coq.Numbers.Cyclic.Int63.Int63]
H:35 [in Coq.Classes.RelationPairs]
H:35 [in Coq.Logic.FunctionalExtensionality]
h:35 [in Coq.Init.Wf]
h:35 [in Coq.Reals.PSeries_reg]
h:35 [in Coq.Logic.Classical_Prop]
h:36 [in Coq.Reals.Rtrigo_reg]
h:36 [in Coq.Reals.PSeries_reg]
H:36 [in Coq.setoid_ring.Ncring]
H:369 [in Coq.MSets.MSetRBT]
h:37 [in Coq.Reals.Ranalysis2]
h:37 [in Coq.Reals.Rtrigo_reg]
h:37 [in Coq.Reals.PSeries_reg]
H:37 [in Coq.Numbers.Natural.Abstract.NGcd]
H:372 [in Coq.Init.Specif]
H:372 [in Coq.MSets.MSetGenTree]
H:374 [in Coq.MSets.MSetRBT]
H:376 [in Coq.MSets.MSetGenTree]
H:377 [in Coq.MSets.MSetRBT]
h:38 [in Coq.Reals.Runcountable]
H:38 [in Coq.Classes.RelationClasses]
H:38 [in Coq.Classes.RelationPairs]
h:38 [in Coq.Reals.PSeries_reg]
H:38 [in Coq.Numbers.Natural.Abstract.NGcd]
H:381 [in Coq.MSets.MSetRBT]
H:384 [in Coq.MSets.MSetRBT]
H:39 [in Coq.Vectors.VectorSpec]
h:39 [in Coq.Reals.PSeries_reg]
H:39 [in Coq.Numbers.Natural.Abstract.NGcd]
H:395 [in Coq.MSets.MSetRBT]
H:398 [in Coq.MSets.MSetRBT]
h:4 [in Coq.Reals.Sqrt_reg]
H:4 [in Coq.Init.Peano]
H:4 [in Coq.btauto.Algebra]
H:4 [in Coq.ZArith.Znumtheory]
h:4 [in Coq.Vectors.VectorDef]
H:4 [in Coq.Bool.DecBool]
h:40 [in Coq.Reals.Ranalysis2]
h:40 [in Coq.Numbers.Natural.Abstract.NBits]
h:40 [in Coq.Numbers.Integer.Abstract.ZBits]
h:40 [in Coq.Reals.PSeries_reg]
H:40 [in Coq.Numbers.Natural.Abstract.NGcd]
H:41 [in Coq.Classes.EquivDec]
H:41 [in Coq.Vectors.VectorEq]
H:42 [in Coq.Logic.FunctionalExtensionality]
h:42 [in Coq.Logic.Berardi]
H:428 [in Coq.MSets.MSetRBT]
h:43 [in Coq.Vectors.VectorDef]
h:431 [in Coq.Reals.RiemannInt]
h:438 [in Coq.Reals.RiemannInt]
H:44 [in Coq.Classes.RelationPairs]
H:44 [in Coq.Vectors.VectorEq]
H:444 [in Coq.MSets.MSetRBT]
H:447 [in Coq.MSets.MSetRBT]
H:45 [in Coq.setoid_ring.Ncring_tac]
h:45 [in Coq.FSets.FMapFullAVL]
H:45 [in Coq.setoid_ring.Ncring]
H:45 [in Coq.Vectors.VectorEq]
H:45 [in Coq.Vectors.VectorDef]
H:459 [in Coq.Init.Logic]
H:46 [in Coq.Classes.RelationPairs]
H:463 [in Coq.MSets.MSetRBT]
H:48 [in Coq.Classes.RelationPairs]
h:48 [in Coq.Reals.Ranalysis5]
H:48 [in Coq.Vectors.VectorDef]
H:49 [in Coq.Classes.CRelationClasses]
h:49 [in Coq.Reals.Ranalysis5]
H:490 [in Coq.ZArith.BinInt]
H:490 [in Coq.MSets.MSetRBT]
H:494 [in Coq.MSets.MSetRBT]
H:498 [in Coq.MSets.MSetRBT]
h:5 [in Coq.Reals.Sqrt_reg]
h:5 [in Coq.Logic.Eqdep]
H:5 [in Coq.Logic.ClassicalFacts]
H:50 [in Coq.Classes.RelationPairs]
h:50 [in Coq.FSets.FMapFullAVL]
H:502 [in Coq.MSets.MSetAVL]
h:508 [in Coq.Reals.RiemannInt]
H:51 [in Coq.Classes.Morphisms]
H:51 [in Coq.Logic.FunctionalExtensionality]
H:51 [in Coq.Classes.EquivDec]
h:51 [in Coq.Reals.Ratan]
H:513 [in Coq.MSets.MSetAVL]
h:515 [in Coq.Reals.RiemannInt]
H:516 [in Coq.MSets.MSetRBT]
H:516 [in Coq.Init.Logic]
H:523 [in Coq.MSets.MSetAVL]
H:523 [in Coq.MSets.MSetRBT]
H:524 [in Coq.Init.Specif]
H:526 [in Coq.MSets.MSetAVL]
H:527 [in Coq.MSets.MSetRBT]
h:529 [in Coq.Reals.RiemannInt]
H:53 [in Coq.Numbers.Integer.Abstract.ZGcd]
H:53 [in Coq.Classes.CMorphisms]
H:534 [in Coq.MSets.MSetAVL]
H:536 [in Coq.MSets.MSetRBT]
H:539 [in Coq.MSets.MSetRBT]
H:54 [in Coq.Numbers.Integer.Abstract.ZGcd]
H:54 [in Coq.setoid_ring.Ncring]
h:542 [in Coq.MSets.MSetAVL]
H:544 [in Coq.MSets.MSetRBT]
h:546 [in Coq.MSets.MSetAVL]
H:547 [in Coq.MSets.MSetAVL]
H:55 [in Coq.Numbers.Integer.Abstract.ZGcd]
H:55 [in Coq.Classes.RelationPairs]
H:55 [in Coq.Vectors.VectorEq]
H:55 [in Coq.Reals.ClassicalConstructiveReals]
h:551 [in Coq.MSets.MSetAVL]
H:551 [in Coq.MSets.MSetRBT]
H:552 [in Coq.MSets.MSetAVL]
H:555 [in Coq.MSets.MSetRBT]
H:558 [in Coq.MSets.MSetAVL]
H:558 [in Coq.MSets.MSetRBT]
H:56 [in Coq.setoid_ring.Ncring_initial]
H:56 [in Coq.Numbers.Integer.Abstract.ZGcd]
H:56 [in Coq.setoid_ring.Ncring_tac]
h:562 [in Coq.Reals.RiemannInt]
H:566 [in Coq.MSets.MSetAVL]
H:567 [in Coq.MSets.MSetRBT]
H:569 [in Coq.MSets.MSetAVL]
H:572 [in Coq.MSets.MSetRBT]
H:575 [in Coq.MSets.MSetAVL]
H:576 [in Coq.MSets.MSetRBT]
H:58 [in Coq.Vectors.VectorEq]
H:583 [in Coq.MSets.MSetAVL]
H:587 [in Coq.MSets.MSetAVL]
H:59 [in Coq.Vectors.VectorEq]
H:590 [in Coq.MSets.MSetAVL]
H:593 [in Coq.MSets.MSetAVL]
H:6 [in Coq.btauto.Algebra]
H:6 [in Coq.Classes.SetoidTactics]
H:6 [in Coq.Classes.CEquivalence]
H:6 [in Coq.Classes.DecidableClass]
H:6 [in Coq.Logic.ClassicalFacts]
H:6 [in Coq.Init.Tactics]
H:6 [in Coq.Classes.Equivalence]
H:60 [in Coq.Classes.CRelationClasses]
H:600 [in Coq.MSets.MSetAVL]
H:603 [in Coq.MSets.MSetAVL]
H:606 [in Coq.MSets.MSetAVL]
h:61 [in Coq.Numbers.HexadecimalPos]
H:61 [in Coq.Classes.EquivDec]
h:61 [in Coq.Numbers.DecimalPos]
H:612 [in Coq.MSets.MSetAVL]
H:616 [in Coq.MSets.MSetAVL]
h:618 [in Coq.PArith.BinPos]
H:620 [in Coq.MSets.MSetAVL]
H:626 [in Coq.MSets.MSetAVL]
h:63 [in Coq.Reals.Ranalysis2]
H:63 [in Coq.setoid_ring.Ncring]
H:630 [in Coq.MSets.MSetAVL]
H:635 [in Coq.MSets.MSetAVL]
H:639 [in Coq.MSets.MSetAVL]
H:649 [in Coq.MSets.MSetAVL]
H:65 [in Coq.Logic.Eqdep_dec]
H:66 [in Coq.Classes.RelationClasses]
H:662 [in Coq.MSets.MSetAVL]
H:665 [in Coq.MSets.MSetAVL]
H:67 [in Coq.Program.Wf]
h:67 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
H:67 [in Coq.setoid_ring.Ncring_tac]
H:675 [in Coq.Init.Specif]
H:68 [in Coq.Classes.RelationClasses]
h:69 [in Coq.Reals.Ranalysis2]
h:69 [in Coq.Init.Wf]
H:7 [in Coq.Strings.Byte]
H:7 [in Coq.Logic.ClassicalFacts]
H:70 [in Coq.Classes.RelationClasses]
H:72 [in Coq.Classes.RelationClasses]
H:72 [in Coq.setoid_ring.Ncring]
H:74 [in Coq.MSets.MSetWeakList]
h:74 [in Coq.Vectors.VectorDef]
H:75 [in Coq.Classes.RelationClasses]
H:75 [in Coq.PArith.Pnat]
H:75 [in Coq.Classes.CRelationClasses]
H:77 [in Coq.Logic.EqdepFacts]
H:77 [in Coq.Classes.RelationClasses]
h:77 [in Coq.ssr.ssrfun]
H:77 [in Coq.Classes.CRelationClasses]
H:78 [in Coq.Classes.Morphisms]
H:79 [in Coq.setoid_ring.Ncring_tac]
H:79 [in Coq.Classes.CRelationClasses]
H:79 [in Coq.Vectors.VectorDef]
h:8 [in Coq.Reals.Ranalysis2]
H:8 [in Coq.btauto.Algebra]
h:8 [in Coq.FSets.FMapFullAVL]
H:8 [in Coq.Classes.DecidableClass]
H:8 [in Coq.Logic.ClassicalFacts]
h:80 [in Coq.Logic.Eqdep_dec]
H:80 [in Coq.Classes.RelationClasses]
H:81 [in Coq.Classes.CMorphisms]
H:81 [in Coq.Classes.CRelationClasses]
H:83 [in Coq.Classes.RelationClasses]
H:83 [in Coq.MSets.MSetWeakList]
H:84 [in Coq.Logic.EqdepFacts]
H:84 [in Coq.Classes.CRelationClasses]
h:85 [in Coq.Program.Wf]
H:85 [in Coq.Logic.FunctionalExtensionality]
H:86 [in Coq.Classes.CRelationClasses]
H:87 [in Coq.Classes.RelationClasses]
H:87 [in Coq.Structures.OrderedType]
h:87 [in Coq.Reals.Rlimit]
h:88 [in Coq.Reals.MVT]
h:89 [in Coq.Reals.MVT]
H:89 [in Coq.omega.OmegaLemmas]
H:89 [in Coq.Classes.CRelationClasses]
H:9 [in Coq.Classes.SetoidTactics]
h:9 [in Coq.Logic.ProofIrrelevanceFacts]
H:90 [in Coq.Classes.Morphisms]
H:90 [in Coq.MSets.MSetWeakList]
H:90 [in Coq.Structures.OrderedType]
H:91 [in Coq.FSets.FSetBridge]
H:91 [in Coq.Logic.EqdepFacts]
H:91 [in Coq.setoid_ring.Ncring_tac]
h:91 [in Coq.Vectors.VectorDef]
H:92 [in Coq.Classes.RelationClasses]
H:92 [in Coq.Classes.Morphisms]
H:92 [in Coq.Classes.CRelationClasses]
H:92 [in Coq.ZArith.Znumtheory]
H:93 [in Coq.Structures.OrderedType]
H:93 [in Coq.ZArith.Znumtheory]
H:94 [in Coq.MSets.MSetInterface]
H:94 [in Coq.FSets.FSetBridge]
H:94 [in Coq.Classes.RelationClasses]
H:94 [in Coq.MSets.MSetList]
H:94 [in Coq.omega.OmegaLemmas]
H:94 [in Coq.ZArith.Znumtheory]
h:941 [in Coq.FSets.FMapAVL]
H:95 [in Coq.Classes.Morphisms]
H:95 [in Coq.Classes.CMorphisms]
H:95 [in Coq.ZArith.Znumtheory]
h:950 [in Coq.FSets.FMapAVL]
h:956 [in Coq.FSets.FMapAVL]
H:96 [in Coq.Classes.RelationClasses]
H:96 [in Coq.Logic.FunctionalExtensionality]
H:96 [in Coq.Classes.CRelationClasses]
h:962 [in Coq.FSets.FMapAVL]
h:968 [in Coq.FSets.FMapAVL]
H:97 [in Coq.Init.Datatypes]
h:97 [in Coq.Vectors.VectorDef]
h:97 [in Coq.Logic.FinFun]
h:974 [in Coq.FSets.FMapAVL]
H:98 [in Coq.Logic.EqdepFacts]
H:98 [in Coq.Classes.RelationClasses]
H:98 [in Coq.Classes.Morphisms]
h:98 [in Coq.Logic.FunctionalExtensionality]
H:98 [in Coq.Classes.CMorphisms]
h:98 [in Coq.Reals.PSeries_reg]
h:980 [in Coq.FSets.FMapAVL]
H:99 [in Coq.Program.Wf]
h:99 [in Coq.Logic.FunctionalExtensionality]
H:99 [in Coq.omega.OmegaLemmas]
| 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 | (70451 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 | (1003 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |