| 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
HasAbs [module, in Coq.Numbers.Integer.Abstract.ZAxioms]HasAbs.abs [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasAbs.abs_neq [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasAbs.abs_eq [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasBoolOrdFuns [module, in Coq.Structures.Orders]
HasBoolOrdFuns' [module, in Coq.Structures.Orders]
HasCmp [module, in Coq.Structures.Orders]
HasCmp.compare [axiom, in Coq.Structures.Orders]
HasCompare [module, in Coq.Structures.Orders]
HasEq [module, in Coq.Structures.Equalities]
HasEqb [module, in Coq.Structures.Equalities]
HasEqBool [module, in Coq.Structures.Equalities]
HasEqBool2Dec [module, in Coq.Structures.Equalities]
HasEqBool2Dec.eq_dec [lemma, in Coq.Structures.Equalities]
HasEqb.eqb [axiom, in Coq.Structures.Equalities]
HasEqDec [module, in Coq.Structures.Equalities]
HasEqDec.eq_dec [axiom, in Coq.Structures.Equalities]
HasEqDec2Bool [module, in Coq.Structures.Equalities]
HasEqDec2Bool.eqb [definition, in Coq.Structures.Equalities]
HasEqDec2Bool.eqb_eq [lemma, in Coq.Structures.Equalities]
HasEq.eq [axiom, in Coq.Structures.Equalities]
HasLe [module, in Coq.Structures.Orders]
HasLeb [module, in Coq.Structures.Orders]
HasLeb.leb [axiom, in Coq.Structures.Orders]
HasLe.le [axiom, in Coq.Structures.Orders]
HasLt [module, in Coq.Structures.Orders]
HasLtb [module, in Coq.Structures.Orders]
HasLtb.ltb [axiom, in Coq.Structures.Orders]
HasLt.lt [axiom, in Coq.Structures.Orders]
HasMax [module, in Coq.Structures.GenericMinMax]
HasMax.max [axiom, in Coq.Structures.GenericMinMax]
HasMax.max_r [axiom, in Coq.Structures.GenericMinMax]
HasMax.max_l [axiom, in Coq.Structures.GenericMinMax]
HasMin [module, in Coq.Structures.GenericMinMax]
HasMinMax [module, in Coq.Structures.GenericMinMax]
HasMin.min [axiom, in Coq.Structures.GenericMinMax]
HasMin.min_r [axiom, in Coq.Structures.GenericMinMax]
HasMin.min_l [axiom, in Coq.Structures.GenericMinMax]
HasOrdOps [module, in Coq.MSets.MSetInterface]
HasOrdOps.compare [axiom, in Coq.MSets.MSetInterface]
HasOrdOps.max_elt [axiom, in Coq.MSets.MSetInterface]
HasOrdOps.min_elt [axiom, in Coq.MSets.MSetInterface]
HasSgn [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasSgn.sgn [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasSgn.sgn_neg [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasSgn.sgn_pos [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasSgn.sgn_null [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
HasUsualEq [module, in Coq.Structures.Equalities]
HasUsualEq.eq [definition, in Coq.Structures.Equalities]
HasWOps [module, in Coq.MSets.MSetInterface]
HasWOps.add [axiom, in Coq.MSets.MSetInterface]
HasWOps.cardinal [axiom, in Coq.MSets.MSetInterface]
HasWOps.choose [axiom, in Coq.MSets.MSetInterface]
HasWOps.diff [axiom, in Coq.MSets.MSetInterface]
HasWOps.elements [axiom, in Coq.MSets.MSetInterface]
HasWOps.empty [axiom, in Coq.MSets.MSetInterface]
HasWOps.equal [axiom, in Coq.MSets.MSetInterface]
HasWOps.exists_ [axiom, in Coq.MSets.MSetInterface]
HasWOps.filter [axiom, in Coq.MSets.MSetInterface]
HasWOps.fold [axiom, in Coq.MSets.MSetInterface]
HasWOps.for_all [axiom, in Coq.MSets.MSetInterface]
HasWOps.inter [axiom, in Coq.MSets.MSetInterface]
HasWOps.is_empty [axiom, in Coq.MSets.MSetInterface]
HasWOps.mem [axiom, in Coq.MSets.MSetInterface]
HasWOps.partition [axiom, in Coq.MSets.MSetInterface]
HasWOps.remove [axiom, in Coq.MSets.MSetInterface]
HasWOps.singleton [axiom, in Coq.MSets.MSetInterface]
HasWOps.subset [axiom, in Coq.MSets.MSetInterface]
HasWOps.union [axiom, in Coq.MSets.MSetInterface]
has_unique_least_element [definition, in Coq.Arith.Wf_nat]
has_quality [definition, in Coq.ssr.ssrbool]
has_fixpoint [record, in Coq.Logic.ClassicalFacts]
has_infinite_path [definition, in Coq.Logic.WKL]
has_lb [definition, in Coq.Reals.SeqProp]
has_ub [definition, in Coq.Reals.SeqProp]
Ha:92 [binder, in Coq.Arith.PeanoNat]
Hbeq:21 [binder, in Coq.Vectors.VectorEq]
Hb:23 [binder, in Coq.ZArith.Zdiv]
Hb:33 [binder, in Coq.ZArith.Zdiv]
hd [definition, in Coq.Lists.Streams]
hd [abbreviation, in Coq.setoid_ring.Ring_polynom]
hd [definition, in Coq.Lists.List]
hd [definition, in Coq.micromega.Env]
hd [definition, in Coq.Vectors.VectorDef]
Hdiff:220 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
HdRel [inductive, in Coq.Sorting.Sorted]
HdRel_inv [lemma, in Coq.Sorting.Sorted]
HdRel_cons [constructor, in Coq.Sorting.Sorted]
HdRel_nil [constructor, in Coq.Sorting.Sorted]
hd_error_cons [lemma, in Coq.Lists.List]
hd_error_nil [lemma, in Coq.Lists.List]
hd_error_some_nil [lemma, in Coq.Lists.List]
hd_error_tl_repr [lemma, in Coq.Lists.List]
hd_error [definition, in Coq.Lists.List]
head [abbreviation, in Coq.Lists.List]
head_cons [abbreviation, in Coq.Lists.List]
head_nil [abbreviation, in Coq.Lists.List]
head0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
head0 [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
head0_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
head00_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
head031 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
head031_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
head031_alt [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Heap [library]
heap_to_list [lemma, in Coq.Sorting.Heap]
heap_exist [constructor, in Coq.Sorting.Heap]
Heine [lemma, in Coq.Reals.Rtopology]
Heine_cor2 [lemma, in Coq.Reals.RiemannInt]
Heine_cor1 [lemma, in Coq.Reals.RiemannInt]
HelloWorld [definition, in Coq.Strings.String]
heqij:143 [binder, in Coq.Lists.SetoidList]
heqij:165 [binder, in Coq.Lists.SetoidList]
heqss':144 [binder, in Coq.Lists.SetoidList]
Heq:221 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
Heq:228 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
Heq:240 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
Here [constructor, in Coq.Lists.Streams]
here [constructor, in Coq.Logic.WKL]
HereAndFurther [constructor, in Coq.Lists.Streams]
Hex [abbreviation, in Coq.Init.Numeral]
Hex [abbreviation, in Coq.Init.Number]
Hexadecimal [constructor, in Coq.Init.Number]
Hexadecimal [constructor, in Coq.Init.Hexadecimal]
hexadecimal [inductive, in Coq.Init.Hexadecimal]
Hexadecimal [library]
HexadecimalExp [constructor, in Coq.Init.Hexadecimal]
HexadecimalFacts [library]
HexadecimalN [library]
HexadecimalNat [library]
HexadecimalPos [library]
HexadecimalQ [library]
HexadecimalR [library]
HexadecimalString [library]
HexadecimalZ [library]
HexString [library]
hf:110 [binder, in Coq.Logic.FinFun]
hf:125 [binder, in Coq.Logic.FinFun]
hf:129 [binder, in Coq.Logic.FinFun]
Hf:328 [binder, in Coq.Init.Logic]
Hf:333 [binder, in Coq.Init.Logic]
high_bit [definition, in Coq.Numbers.Cyclic.Int63.Int63]
high:25 [binder, in Coq.Reals.Rsigma]
high:28 [binder, in Coq.Reals.Rsigma]
high:3 [binder, in Coq.Reals.Rsigma]
high:31 [binder, in Coq.Reals.Rsigma]
high:33 [binder, in Coq.Reals.Rsigma]
high:6 [binder, in Coq.Reals.Rsigma]
Hi1:256 [binder, in Coq.Vectors.VectorSpec]
Hi2:257 [binder, in Coq.Vectors.VectorSpec]
Hi:230 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
Hi:249 [binder, in Coq.Vectors.VectorSpec]
Hi:299 [binder, in Coq.ZArith.BinInt]
HLevels [library]
hl:10 [binder, in Coq.MSets.MSetAVL]
hl:28 [binder, in Coq.FSets.FMapAVL]
Hl:386 [binder, in Coq.FSets.FMapWeakList]
Hl:387 [binder, in Coq.FSets.FMapWeakList]
Hm':315 [binder, in Coq.FSets.FMapWeakList]
Hm':320 [binder, in Coq.FSets.FMapWeakList]
Hm':325 [binder, in Coq.FSets.FMapWeakList]
Hm':330 [binder, in Coq.FSets.FMapWeakList]
Hm':361 [binder, in Coq.FSets.FMapList]
Hm':391 [binder, in Coq.FSets.FMapWeakList]
Hm':409 [binder, in Coq.FSets.FMapWeakList]
Hm':426 [binder, in Coq.FSets.FMapWeakList]
Hm':447 [binder, in Coq.FSets.FMapWeakList]
Hm':463 [binder, in Coq.FSets.FMapWeakList]
Hm':468 [binder, in Coq.FSets.FMapList]
Hm':473 [binder, in Coq.FSets.FMapWeakList]
Hm':474 [binder, in Coq.FSets.FMapList]
Hm':480 [binder, in Coq.FSets.FMapWeakList]
Hm':484 [binder, in Coq.FSets.FMapList]
Hm':485 [binder, in Coq.FSets.FMapWeakList]
Hm':493 [binder, in Coq.FSets.FMapList]
Hm':500 [binder, in Coq.FSets.FMapList]
Hm':505 [binder, in Coq.FSets.FMapList]
Hm:155 [binder, in Coq.FSets.FMapWeakList]
Hm:159 [binder, in Coq.FSets.FMapWeakList]
Hm:164 [binder, in Coq.FSets.FMapWeakList]
Hm:166 [binder, in Coq.FSets.FMapList]
Hm:203 [binder, in Coq.FSets.FMapWeakList]
Hm:207 [binder, in Coq.FSets.FMapWeakList]
Hm:209 [binder, in Coq.FSets.FMapList]
Hm:212 [binder, in Coq.FSets.FMapWeakList]
Hm:213 [binder, in Coq.FSets.FMapList]
Hm:217 [binder, in Coq.FSets.FMapWeakList]
Hm:218 [binder, in Coq.FSets.FMapList]
Hm:222 [binder, in Coq.FSets.FMapWeakList]
Hm:223 [binder, in Coq.FSets.FMapList]
Hm:228 [binder, in Coq.FSets.FMapList]
Hm:232 [binder, in Coq.FSets.FMapWeakList]
Hm:238 [binder, in Coq.FSets.FMapList]
Hm:240 [binder, in Coq.FSets.FMapList]
Hm:313 [binder, in Coq.FSets.FMapWeakList]
Hm:318 [binder, in Coq.FSets.FMapWeakList]
Hm:323 [binder, in Coq.FSets.FMapWeakList]
Hm:328 [binder, in Coq.FSets.FMapWeakList]
Hm:351 [binder, in Coq.FSets.FMapWeakList]
Hm:359 [binder, in Coq.FSets.FMapList]
Hm:362 [binder, in Coq.FSets.FMapWeakList]
Hm:364 [binder, in Coq.FSets.FMapList]
Hm:366 [binder, in Coq.FSets.FMapList]
Hm:389 [binder, in Coq.FSets.FMapWeakList]
Hm:397 [binder, in Coq.FSets.FMapList]
Hm:407 [binder, in Coq.FSets.FMapWeakList]
Hm:412 [binder, in Coq.FSets.FMapList]
Hm:424 [binder, in Coq.FSets.FMapWeakList]
Hm:44 [binder, in Coq.FSets.FMapWeakList]
Hm:445 [binder, in Coq.FSets.FMapWeakList]
Hm:461 [binder, in Coq.FSets.FMapWeakList]
Hm:466 [binder, in Coq.FSets.FMapList]
Hm:47 [binder, in Coq.FSets.FMapWeakList]
Hm:471 [binder, in Coq.FSets.FMapWeakList]
Hm:472 [binder, in Coq.FSets.FMapList]
Hm:478 [binder, in Coq.FSets.FMapWeakList]
Hm:482 [binder, in Coq.FSets.FMapList]
Hm:483 [binder, in Coq.FSets.FMapWeakList]
Hm:49 [binder, in Coq.FSets.FMapList]
Hm:491 [binder, in Coq.FSets.FMapList]
Hm:498 [binder, in Coq.FSets.FMapList]
Hm:503 [binder, in Coq.FSets.FMapList]
Hm:52 [binder, in Coq.FSets.FMapList]
Hm:87 [binder, in Coq.FSets.FMapWeakList]
Hm:91 [binder, in Coq.FSets.FMapWeakList]
Hm:97 [binder, in Coq.FSets.FMapList]
Hn:298 [binder, in Coq.ZArith.BinInt]
hold [definition, in Coq.micromega.Tauto]
hold_eEQ [lemma, in Coq.micromega.Tauto]
hold_eIFF_IMPL [lemma, in Coq.micromega.Tauto]
hold_eIFF [lemma, in Coq.micromega.Tauto]
hold_eIMPL [lemma, in Coq.micromega.Tauto]
hold_eNOT [lemma, in Coq.micromega.Tauto]
hold_eOR [lemma, in Coq.micromega.Tauto]
hold_eAND [lemma, in Coq.micromega.Tauto]
hold_eFF [lemma, in Coq.micromega.Tauto]
hold_eTT [lemma, in Coq.micromega.Tauto]
hold_eiff [lemma, in Coq.micromega.Tauto]
hole:8 [binder, in Coq.Reals.Runcountable]
homoLR [lemma, in Coq.ssr.ssrbool]
homoLR_in [lemma, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip [section, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip.aD [variable, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip.aD' [variable, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip.aR [variable, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip.aT [variable, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip.f [variable, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip.rR [variable, in Coq.ssr.ssrbool]
HomoMonoMorphismFlip.rT [variable, in Coq.ssr.ssrbool]
Homomorphism [module, in Coq.Numbers.Natural.Abstract.NIso]
homomorphism_2 [definition, in Coq.ssr.ssrfun]
homomorphism_1 [definition, in Coq.ssr.ssrfun]
Homomorphism.homomorphism [definition, in Coq.Numbers.Natural.Abstract.NIso]
Homomorphism.hom_nat_iso [lemma, in Coq.Numbers.Natural.Abstract.NIso]
Homomorphism.natural_isomorphism_succ [lemma, in Coq.Numbers.Natural.Abstract.NIso]
Homomorphism.natural_isomorphism_0 [lemma, in Coq.Numbers.Natural.Abstract.NIso]
Homomorphism.natural_isomorphism_wd [instance, in Coq.Numbers.Natural.Abstract.NIso]
Homomorphism.natural_isomorphism [definition, in Coq.Numbers.Natural.Abstract.NIso]
_ == _ [notation, in Coq.Numbers.Natural.Abstract.NIso]
homoRL [lemma, in Coq.ssr.ssrbool]
homoRL_in [lemma, in Coq.ssr.ssrbool]
homo_sym_in11 [lemma, in Coq.ssr.ssrbool]
homo_sym_in [lemma, in Coq.ssr.ssrbool]
homo_sym [lemma, in Coq.ssr.ssrbool]
homo_mono_in [lemma, in Coq.ssr.ssrbool]
homo_mono [lemma, in Coq.ssr.ssrbool]
hprop_hset [lemma, in Coq.Logic.HLevels]
hprop_hprop [lemma, in Coq.Logic.HLevels]
Hp:275 [binder, in Coq.ZArith.BinInt]
Hp:276 [binder, in Coq.ZArith.BinInt]
Hp:280 [binder, in Coq.ZArith.BinInt]
Hp:281 [binder, in Coq.ZArith.BinInt]
Hqgt0:113 [binder, in Coq.Reals.Cauchy.QExtra]
Hqgt0:115 [binder, in Coq.Reals.Cauchy.QExtra]
Hqgt0:121 [binder, in Coq.Reals.Cauchy.QExtra]
Hqgt0:124 [binder, in Coq.Reals.Cauchy.QExtra]
Hrpos:115 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hrpos:147 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
hr:11 [binder, in Coq.MSets.MSetAVL]
hr:29 [binder, in Coq.FSets.FMapAVL]
hset_hOneType [lemma, in Coq.Logic.HLevels]
hset_hprop [lemma, in Coq.Logic.HLevels]
Hs':111 [binder, in Coq.MSets.MSetWeakList]
Hs':120 [binder, in Coq.MSets.MSetWeakList]
Hs':129 [binder, in Coq.MSets.MSetWeakList]
Hs':133 [binder, in Coq.MSets.MSetWeakList]
Hs':137 [binder, in Coq.MSets.MSetWeakList]
Hs':140 [binder, in Coq.MSets.MSetList]
Hs':149 [binder, in Coq.MSets.MSetList]
Hs':154 [binder, in Coq.MSets.MSetList]
Hs':163 [binder, in Coq.MSets.MSetList]
Hs':167 [binder, in Coq.MSets.MSetList]
Hs':177 [binder, in Coq.MSets.MSetList]
Hs':181 [binder, in Coq.MSets.MSetList]
Hs':185 [binder, in Coq.MSets.MSetList]
Hs:110 [binder, in Coq.MSets.MSetWeakList]
Hs:111 [binder, in Coq.MSets.MSetList]
Hs:119 [binder, in Coq.MSets.MSetWeakList]
Hs:121 [binder, in Coq.MSets.MSetList]
Hs:1223 [binder, in Coq.FSets.FMapAVL]
Hs:125 [binder, in Coq.MSets.MSetList]
Hs:128 [binder, in Coq.MSets.MSetWeakList]
Hs:128 [binder, in Coq.MSets.MSetGenTree]
Hs:132 [binder, in Coq.MSets.MSetWeakList]
Hs:132 [binder, in Coq.MSets.MSetList]
Hs:136 [binder, in Coq.MSets.MSetWeakList]
Hs:139 [binder, in Coq.MSets.MSetList]
Hs:142 [binder, in Coq.MSets.MSetWeakList]
Hs:148 [binder, in Coq.MSets.MSetList]
Hs:153 [binder, in Coq.MSets.MSetList]
Hs:162 [binder, in Coq.MSets.MSetList]
Hs:164 [binder, in Coq.MSets.MSetWeakList]
Hs:166 [binder, in Coq.MSets.MSetList]
Hs:168 [binder, in Coq.MSets.MSetWeakList]
Hs:176 [binder, in Coq.MSets.MSetList]
Hs:180 [binder, in Coq.MSets.MSetList]
Hs:184 [binder, in Coq.MSets.MSetList]
Hs:190 [binder, in Coq.MSets.MSetList]
Hs:192 [binder, in Coq.MSets.MSetList]
Hs:198 [binder, in Coq.MSets.MSetList]
Hs:205 [binder, in Coq.MSets.MSetList]
Hs:219 [binder, in Coq.MSets.MSetList]
Hs:223 [binder, in Coq.MSets.MSetList]
Hs:239 [binder, in Coq.MSets.MSetList]
Hs:243 [binder, in Coq.MSets.MSetList]
Hs:284 [binder, in Coq.MSets.MSetGenTree]
HS:35 [binder, in Coq.Vectors.VectorSpec]
HS:61 [binder, in Coq.Vectors.Fin]
Hs:80 [binder, in Coq.MSets.MSetWeakList]
Hs:87 [binder, in Coq.MSets.MSetWeakList]
Hs:89 [binder, in Coq.MSets.MSetList]
Hs:98 [binder, in Coq.MSets.MSetWeakList]
Hurkens [library]
Hxpos:137 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hxpos:139 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hxrange:366 [binder, in Coq.Reals.Ratan]
Hxrange:380 [binder, in Coq.Reals.Ratan]
Hx:178 [binder, in Coq.Reals.Ratan]
Hx:186 [binder, in Coq.Reals.Ratan]
Hx:47 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hx:53 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hx:7 [binder, in Coq.QArith.Qcabs]
Hx:9 [binder, in Coq.QArith.Qcabs]
Hyp [constructor, in Coq.micromega.Ztac]
hypo [record, in Coq.setoid_ring.InitialRing]
hypo_proof [projection, in Coq.setoid_ring.InitialRing]
hypo_type [projection, in Coq.setoid_ring.InitialRing]
hyps_of_pt [definition, in Coq.micromega.ZMicromega]
hyps:27 [binder, in Coq.rtauto.Rtauto]
hyps:32 [binder, in Coq.rtauto.Rtauto]
hyps:35 [binder, in Coq.rtauto.Rtauto]
hyps:39 [binder, in Coq.rtauto.Rtauto]
hyps:44 [binder, in Coq.rtauto.Rtauto]
hyps:50 [binder, in Coq.rtauto.Rtauto]
hyps:54 [binder, in Coq.rtauto.Rtauto]
hyps:57 [binder, in Coq.rtauto.Rtauto]
hyps:63 [binder, in Coq.rtauto.Rtauto]
hyps:73 [binder, in Coq.rtauto.Rtauto]
Hy:48 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Hy:54 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
h':101 [binder, in Coq.Logic.FinFun]
h':107 [binder, in Coq.Vectors.Fin]
h':115 [binder, in Coq.Logic.Hurkens]
H':116 [binder, in Coq.Logic.FunctionalExtensionality]
h':116 [binder, in Coq.Logic.Hurkens]
h':198 [binder, in Coq.Reals.Ratan]
h':258 [binder, in Coq.Reals.Ranalysis1]
h':259 [binder, in Coq.Reals.Ranalysis1]
h':261 [binder, in Coq.Reals.Ranalysis1]
h':262 [binder, in Coq.Reals.Ranalysis1]
h':271 [binder, in Coq.Reals.Ranalysis1]
h':272 [binder, in Coq.Reals.Ranalysis1]
h':274 [binder, in Coq.Reals.Ranalysis1]
h':275 [binder, in Coq.Reals.Ranalysis1]
h':291 [binder, in Coq.ssr.ssrfun]
h':293 [binder, in Coq.ssr.ssrfun]
H':491 [binder, in Coq.ZArith.BinInt]
h':652 [binder, in Coq.ssr.ssrbool]
H':81 [binder, in Coq.Classes.RelationClasses]
H':88 [binder, in Coq.Classes.RelationClasses]
H':90 [binder, in Coq.Classes.CRelationClasses]
H':97 [binder, in Coq.Classes.CRelationClasses]
h0:101 [binder, in Coq.Logic.Hurkens]
H0:106 [binder, in Coq.MSets.MSetWeakList]
H0:11 [binder, in Coq.Classes.Morphisms_Prop]
H0:115 [binder, in Coq.MSets.MSetWeakList]
H0:120 [binder, in Coq.MSets.MSetInterface]
H0:122 [binder, in Coq.Classes.Morphisms]
H0:124 [binder, in Coq.MSets.MSetInterface]
H0:124 [binder, in Coq.MSets.MSetWeakList]
h0:127 [binder, in Coq.Logic.Hurkens]
H0:128 [binder, in Coq.MSets.MSetInterface]
h0:129 [binder, in Coq.Logic.Hurkens]
H0:144 [binder, in Coq.setoid_ring.Ncring_tac]
H0:144 [binder, in Coq.MSets.MSetList]
H0:144 [binder, in Coq.Classes.CMorphisms]
H0:146 [binder, in Coq.MSets.MSetInterface]
H0:149 [binder, in Coq.MSets.MSetInterface]
H0:157 [binder, in Coq.Classes.Morphisms]
H0:158 [binder, in Coq.MSets.MSetList]
H0:159 [binder, in Coq.MSets.MSetInterface]
H0:162 [binder, in Coq.MSets.MSetInterface]
H0:165 [binder, in Coq.MSets.MSetInterface]
H0:172 [binder, in Coq.MSets.MSetList]
H0:173 [binder, in Coq.Classes.Morphisms]
H0:179 [binder, in Coq.Classes.Morphisms]
H0:187 [binder, in Coq.Classes.CMorphisms]
H0:188 [binder, in Coq.Classes.Morphisms]
H0:194 [binder, in Coq.Classes.Morphisms]
H0:195 [binder, in Coq.setoid_ring.Ncring_tac]
H0:203 [binder, in Coq.Classes.CMorphisms]
H0:209 [binder, in Coq.Classes.CMorphisms]
H0:213 [binder, in Coq.Classes.Morphisms]
H0:218 [binder, in Coq.Classes.CMorphisms]
H0:219 [binder, in Coq.Classes.Morphisms]
H0:223 [binder, in Coq.Classes.CMorphisms]
H0:229 [binder, in Coq.Classes.CMorphisms]
H0:237 [binder, in Coq.Classes.CMorphisms]
H0:24 [binder, in Coq.Classes.RelationPairs]
H0:256 [binder, in Coq.Classes.CMorphisms]
H0:258 [binder, in Coq.MSets.MSetInterface]
H0:262 [binder, in Coq.Classes.CMorphisms]
H0:263 [binder, in Coq.MSets.MSetGenTree]
H0:27 [binder, in Coq.Classes.RelationPairs]
H0:271 [binder, in Coq.MSets.MSetInterface]
H0:280 [binder, in Coq.MSets.MSetRBT]
H0:291 [binder, in Coq.MSets.MSetRBT]
H0:30 [binder, in Coq.Classes.RelationPairs]
H0:302 [binder, in Coq.MSets.MSetRBT]
H0:324 [binder, in Coq.MSets.MSetGenTree]
H0:329 [binder, in Coq.MSets.MSetRBT]
H0:33 [binder, in Coq.Classes.RelationPairs]
H0:336 [binder, in Coq.MSets.MSetGenTree]
H0:340 [binder, in Coq.MSets.MSetRBT]
H0:36 [binder, in Coq.Classes.RelationPairs]
H0:370 [binder, in Coq.MSets.MSetRBT]
H0:373 [binder, in Coq.MSets.MSetGenTree]
H0:377 [binder, in Coq.MSets.MSetGenTree]
H0:39 [binder, in Coq.Classes.RelationPairs]
H0:44 [binder, in Coq.Classes.EquivDec]
H0:45 [binder, in Coq.Classes.RelationPairs]
H0:464 [binder, in Coq.MSets.MSetRBT]
H0:47 [binder, in Coq.Classes.RelationPairs]
H0:49 [binder, in Coq.Classes.RelationPairs]
H0:491 [binder, in Coq.MSets.MSetRBT]
H0:495 [binder, in Coq.MSets.MSetRBT]
H0:499 [binder, in Coq.MSets.MSetRBT]
H0:503 [binder, in Coq.MSets.MSetAVL]
H0:51 [binder, in Coq.Classes.RelationPairs]
H0:51 [binder, in Coq.Vectors.Fin]
H0:514 [binder, in Coq.MSets.MSetAVL]
H0:517 [binder, in Coq.MSets.MSetRBT]
H0:524 [binder, in Coq.MSets.MSetRBT]
H0:528 [binder, in Coq.MSets.MSetRBT]
H0:535 [binder, in Coq.MSets.MSetAVL]
H0:537 [binder, in Coq.MSets.MSetRBT]
H0:54 [binder, in Coq.Classes.EquivDec]
H0:545 [binder, in Coq.MSets.MSetRBT]
H0:552 [binder, in Coq.MSets.MSetRBT]
H0:559 [binder, in Coq.MSets.MSetAVL]
H0:559 [binder, in Coq.MSets.MSetRBT]
H0:568 [binder, in Coq.MSets.MSetRBT]
H0:576 [binder, in Coq.MSets.MSetAVL]
H0:577 [binder, in Coq.MSets.MSetRBT]
H0:607 [binder, in Coq.MSets.MSetAVL]
H0:613 [binder, in Coq.MSets.MSetAVL]
H0:617 [binder, in Coq.MSets.MSetAVL]
H0:621 [binder, in Coq.MSets.MSetAVL]
H0:627 [binder, in Coq.MSets.MSetAVL]
H0:631 [binder, in Coq.MSets.MSetAVL]
H0:636 [binder, in Coq.MSets.MSetAVL]
H0:640 [binder, in Coq.MSets.MSetAVL]
H0:80 [binder, in Coq.Classes.Morphisms]
H0:84 [binder, in Coq.Classes.CMorphisms]
h0:99 [binder, in Coq.Logic.Hurkens]
H1':288 [binder, in Coq.Init.Logic]
H1:10 [binder, in Coq.Reals.Rtrigo_fun]
H1:100 [binder, in Coq.Reals.Rderiv]
H1:102 [binder, in Coq.Reals.Rderiv]
H1:103 [binder, in Coq.Logic.EqdepFacts]
H1:104 [binder, in Coq.Reals.Rderiv]
H1:12 [binder, in Coq.Reals.Rtrigo_fun]
H1:135 [binder, in Coq.Reals.Rderiv]
H1:137 [binder, in Coq.Reals.Rderiv]
H1:139 [binder, in Coq.Reals.Rderiv]
H1:14 [binder, in Coq.Reals.Rtrigo_fun]
H1:16 [binder, in Coq.Reals.Rderiv]
H1:16 [binder, in Coq.Reals.Rtrigo_fun]
H1:164 [binder, in Coq.Reals.Rderiv]
H1:166 [binder, in Coq.Reals.Rderiv]
H1:168 [binder, in Coq.Reals.Rderiv]
H1:18 [binder, in Coq.Reals.Rderiv]
H1:18 [binder, in Coq.Reals.Rtrigo_fun]
H1:183 [binder, in Coq.Classes.Morphisms]
H1:196 [binder, in Coq.Classes.Morphisms]
H1:2 [binder, in Coq.Reals.Rtrigo_fun]
H1:20 [binder, in Coq.Reals.Rderiv]
H1:20 [binder, in Coq.Reals.Rtrigo_fun]
h1:21 [binder, in Coq.Numbers.Natural.Abstract.NStrongRec]
H1:210 [binder, in Coq.Bool.Bool]
H1:213 [binder, in Coq.Classes.CMorphisms]
H1:214 [binder, in Coq.Classes.Morphisms]
H1:22 [binder, in Coq.Reals.Rderiv]
H1:22 [binder, in Coq.Reals.Rtrigo_fun]
H1:220 [binder, in Coq.Classes.Morphisms]
H1:231 [binder, in Coq.Classes.CMorphisms]
H1:239 [binder, in Coq.Classes.CMorphisms]
H1:24 [binder, in Coq.Reals.Rderiv]
H1:24 [binder, in Coq.Reals.Rtrigo_fun]
H1:257 [binder, in Coq.Classes.CMorphisms]
H1:26 [binder, in Coq.Reals.Rderiv]
H1:26 [binder, in Coq.Reals.Rtrigo_fun]
H1:263 [binder, in Coq.Classes.CMorphisms]
H1:28 [binder, in Coq.Reals.Rderiv]
H1:28 [binder, in Coq.Reals.Rtrigo_fun]
H1:286 [binder, in Coq.Init.Logic]
H1:30 [binder, in Coq.Reals.Rderiv]
H1:30 [binder, in Coq.Reals.Rtrigo_fun]
H1:32 [binder, in Coq.Reals.Rderiv]
H1:32 [binder, in Coq.Reals.Rtrigo_fun]
H1:322 [binder, in Coq.Init.Logic]
H1:326 [binder, in Coq.MSets.MSetGenTree]
H1:34 [binder, in Coq.Reals.Rderiv]
H1:34 [binder, in Coq.Reals.Rtrigo_fun]
H1:36 [binder, in Coq.Reals.Rderiv]
H1:36 [binder, in Coq.Reals.Rtrigo_fun]
H1:38 [binder, in Coq.Reals.Rderiv]
H1:39 [binder, in Coq.Reals.Rfunctions]
H1:4 [binder, in Coq.Reals.Rfunctions]
H1:4 [binder, in Coq.Reals.Rtrigo_fun]
H1:40 [binder, in Coq.Reals.Rderiv]
H1:41 [binder, in Coq.Reals.Rfunctions]
H1:42 [binder, in Coq.Reals.Rderiv]
H1:43 [binder, in Coq.Reals.Rfunctions]
H1:44 [binder, in Coq.Reals.Rderiv]
H1:44 [binder, in Coq.Vectors.VectorSpec]
H1:46 [binder, in Coq.Reals.Rderiv]
H1:47 [binder, in Coq.Reals.Rfunctions]
H1:48 [binder, in Coq.Reals.Rderiv]
H1:49 [binder, in Coq.Reals.Rfunctions]
H1:50 [binder, in Coq.Reals.Rderiv]
H1:51 [binder, in Coq.Reals.Rfunctions]
H1:54 [binder, in Coq.Vectors.Fin]
H1:562 [binder, in Coq.MSets.MSetAVL]
H1:579 [binder, in Coq.MSets.MSetAVL]
H1:6 [binder, in Coq.Reals.Rfunctions]
H1:6 [binder, in Coq.Reals.Rtrigo_fun]
H1:64 [binder, in Coq.Reals.Rfunctions]
H1:66 [binder, in Coq.Reals.Rfunctions]
H1:68 [binder, in Coq.Reals.Rfunctions]
h1:72 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
H1:75 [binder, in Coq.Logic.EqdepFacts]
H1:77 [binder, in Coq.Reals.Rfunctions]
H1:79 [binder, in Coq.Reals.Rfunctions]
H1:8 [binder, in Coq.Reals.Rtrigo_fun]
H1:81 [binder, in Coq.Vectors.VectorSpec]
H1:81 [binder, in Coq.Reals.Rfunctions]
H1:82 [binder, in Coq.Logic.EqdepFacts]
H1:89 [binder, in Coq.Vectors.VectorSpec]
H1:89 [binder, in Coq.Logic.EqdepFacts]
H1:96 [binder, in Coq.Logic.EqdepFacts]
H2':289 [binder, in Coq.Init.Logic]
H2:101 [binder, in Coq.Reals.Rderiv]
H2:103 [binder, in Coq.Reals.Rderiv]
H2:104 [binder, in Coq.Logic.EqdepFacts]
H2:105 [binder, in Coq.Reals.Rderiv]
H2:11 [binder, in Coq.Reals.Rtrigo_fun]
H2:13 [binder, in Coq.Reals.Rtrigo_fun]
H2:136 [binder, in Coq.Reals.Rderiv]
H2:138 [binder, in Coq.Reals.Rderiv]
H2:140 [binder, in Coq.Reals.Rderiv]
H2:15 [binder, in Coq.Reals.Rtrigo_fun]
H2:165 [binder, in Coq.Reals.Rderiv]
H2:167 [binder, in Coq.Reals.Rderiv]
H2:169 [binder, in Coq.Reals.Rderiv]
H2:17 [binder, in Coq.Reals.Rderiv]
H2:17 [binder, in Coq.Reals.Rtrigo_fun]
H2:19 [binder, in Coq.Reals.Rderiv]
H2:19 [binder, in Coq.Reals.Rtrigo_fun]
H2:21 [binder, in Coq.Reals.Rderiv]
H2:21 [binder, in Coq.Reals.Rtrigo_fun]
H2:211 [binder, in Coq.Bool.Bool]
h2:22 [binder, in Coq.Numbers.Natural.Abstract.NStrongRec]
H2:23 [binder, in Coq.Reals.Rderiv]
H2:23 [binder, in Coq.Reals.Rtrigo_fun]
H2:25 [binder, in Coq.Reals.Rderiv]
H2:25 [binder, in Coq.Reals.Rtrigo_fun]
H2:27 [binder, in Coq.Reals.Rderiv]
H2:27 [binder, in Coq.Reals.Rtrigo_fun]
H2:287 [binder, in Coq.Init.Logic]
H2:29 [binder, in Coq.Reals.Rderiv]
H2:29 [binder, in Coq.Reals.Rtrigo_fun]
H2:3 [binder, in Coq.Reals.Rtrigo_fun]
H2:31 [binder, in Coq.Reals.Rderiv]
H2:31 [binder, in Coq.Reals.Rtrigo_fun]
H2:323 [binder, in Coq.Init.Logic]
H2:33 [binder, in Coq.Reals.Rderiv]
H2:33 [binder, in Coq.Reals.Rtrigo_fun]
H2:35 [binder, in Coq.Reals.Rderiv]
H2:35 [binder, in Coq.Reals.Rtrigo_fun]
H2:37 [binder, in Coq.Reals.Rderiv]
H2:37 [binder, in Coq.Reals.Rtrigo_fun]
H2:39 [binder, in Coq.Reals.Rderiv]
H2:40 [binder, in Coq.Reals.Rfunctions]
H2:41 [binder, in Coq.Reals.Rderiv]
H2:42 [binder, in Coq.Reals.Rfunctions]
H2:43 [binder, in Coq.Reals.Rderiv]
H2:44 [binder, in Coq.Reals.Rfunctions]
H2:45 [binder, in Coq.Reals.Rderiv]
H2:45 [binder, in Coq.Vectors.VectorSpec]
H2:47 [binder, in Coq.Reals.Rderiv]
H2:48 [binder, in Coq.Reals.Rfunctions]
H2:49 [binder, in Coq.Reals.Rderiv]
H2:5 [binder, in Coq.Reals.Rfunctions]
H2:5 [binder, in Coq.Reals.Rtrigo_fun]
H2:50 [binder, in Coq.Reals.Rfunctions]
H2:51 [binder, in Coq.Reals.Rderiv]
H2:52 [binder, in Coq.Reals.Rfunctions]
H2:57 [binder, in Coq.Vectors.Fin]
H2:65 [binder, in Coq.Reals.Rfunctions]
H2:67 [binder, in Coq.Reals.Rfunctions]
h2:68 [binder, in Coq.Vectors.VectorDef]
H2:69 [binder, in Coq.Reals.Rfunctions]
H2:7 [binder, in Coq.Reals.Rfunctions]
H2:7 [binder, in Coq.Reals.Rtrigo_fun]
h2:73 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
H2:76 [binder, in Coq.Logic.EqdepFacts]
H2:78 [binder, in Coq.Reals.Rfunctions]
H2:80 [binder, in Coq.Reals.Rfunctions]
H2:82 [binder, in Coq.Vectors.VectorSpec]
H2:82 [binder, in Coq.Reals.Rfunctions]
H2:83 [binder, in Coq.Logic.EqdepFacts]
H2:9 [binder, in Coq.Reals.Rtrigo_fun]
H2:90 [binder, in Coq.Vectors.VectorSpec]
H2:90 [binder, in Coq.Logic.EqdepFacts]
H2:97 [binder, in Coq.Logic.EqdepFacts]
h:1 [binder, in Coq.Reals.Sqrt_reg]
H:10 [binder, in Coq.setoid_ring.Ncring_initial]
H:10 [binder, in Coq.Classes.Morphisms_Prop]
H:10 [binder, in Coq.Classes.DecidableClass]
H:10 [binder, in Coq.Init.Tactics]
H:10 [binder, in Coq.Bool.DecBool]
H:100 [binder, in Coq.Classes.RelationClasses]
h:100 [binder, in Coq.Logic.FunctionalExtensionality]
h:100 [binder, in Coq.Reals.PSeries_reg]
h:100 [binder, in Coq.Logic.FinFun]
h:101 [binder, in Coq.Reals.MVT]
H:101 [binder, in Coq.Classes.Morphisms]
H:101 [binder, in Coq.Classes.CRelationClasses]
H:101 [binder, in Coq.Vectors.Fin]
H:102 [binder, in Coq.Classes.RelationClasses]
h:102 [binder, in Coq.Reals.MVT]
H:102 [binder, in Coq.Classes.CMorphisms]
H:103 [binder, in Coq.Classes.CRelationClasses]
H:103 [binder, in Coq.Vectors.Fin]
H:104 [binder, in Coq.Classes.RelationClasses]
H:104 [binder, in Coq.Classes.Morphisms]
H:104 [binder, in Coq.omega.OmegaLemmas]
H:105 [binder, in Coq.Logic.EqdepFacts]
H:105 [binder, in Coq.Logic.FunctionalExtensionality]
H:105 [binder, in Coq.MSets.MSetWeakList]
H:105 [binder, in Coq.Classes.CRelationClasses]
h:106 [binder, in Coq.Logic.Eqdep_dec]
H:106 [binder, in Coq.setoid_ring.Ncring_tac]
h:106 [binder, in Coq.Reals.RiemannInt]
H:106 [binder, in Coq.Classes.CMorphisms]
h:106 [binder, in Coq.Vectors.Fin]
H:107 [binder, in Coq.Classes.Morphisms]
h:107 [binder, in Coq.Logic.FunctionalExtensionality]
H:107 [binder, in Coq.Classes.CRelationClasses]
H:107 [binder, in Coq.Vectors.VectorDef]
H:108 [binder, in Coq.Classes.RelationClasses]
h:1086 [binder, in Coq.FSets.FMapAVL]
H:109 [binder, in Coq.Classes.Morphisms]
H:109 [binder, in Coq.Classes.CRelationClasses]
h:1092 [binder, in Coq.FSets.FMapAVL]
h:1099 [binder, in Coq.FSets.FMapAVL]
h:11 [binder, in Coq.Reals.PSeries_reg]
h:110 [binder, in Coq.Logic.EqdepFacts]
H:110 [binder, in Coq.Classes.CMorphisms]
h:1104 [binder, in Coq.FSets.FMapAVL]
h:1109 [binder, in Coq.FSets.FMapAVL]
H:111 [binder, in Coq.Classes.Morphisms]
h:111 [binder, in Coq.Reals.RiemannInt]
H:111 [binder, in Coq.Classes.CRelationClasses]
H:112 [binder, in Coq.MSets.MSetInterface]
h:112 [binder, in Coq.Vectors.Fin]
H:113 [binder, in Coq.omega.OmegaLemmas]
H:113 [binder, in Coq.Classes.CRelationClasses]
h:113 [binder, in Coq.Logic.FinFun]
H:114 [binder, in Coq.MSets.MSetWeakList]
H:114 [binder, in Coq.Classes.CMorphisms]
H:115 [binder, in Coq.MSets.MSetInterface]
h:116 [binder, in Coq.Reals.Ranalysis1]
H:116 [binder, in Coq.Classes.Morphisms]
h:116 [binder, in Coq.Vectors.VectorDef]
H:117 [binder, in Coq.MSets.MSetList]
H:117 [binder, in Coq.Classes.CRelationClasses]
h:118 [binder, in Coq.Logic.FunctionalExtensionality]
H:118 [binder, in Coq.Classes.CMorphisms]
H:119 [binder, in Coq.MSets.MSetInterface]
h:119 [binder, in Coq.Vectors.VectorDef]
h:12 [binder, in Coq.Init.Number]
H:12 [binder, in Coq.Classes.CMorphisms]
h:12 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
H:12 [binder, in Coq.Classes.SetoidClass]
H:12 [binder, in Coq.Classes.DecidableClass]
H:120 [binder, in Coq.Classes.Morphisms]
h:120 [binder, in Coq.Reals.Rpower]
H:120 [binder, in Coq.omega.OmegaLemmas]
H:121 [binder, in Coq.setoid_ring.Ncring_tac]
H:121 [binder, in Coq.Classes.CMorphisms]
h:122 [binder, in Coq.Logic.FinFun]
H:123 [binder, in Coq.MSets.MSetInterface]
H:123 [binder, in Coq.MSets.MSetWeakList]
H:124 [binder, in Coq.Classes.CMorphisms]
H:125 [binder, in Coq.Vectors.VectorDef]
H:127 [binder, in Coq.MSets.MSetInterface]
H:127 [binder, in Coq.Classes.Morphisms]
H:127 [binder, in Coq.omega.OmegaLemmas]
H:127 [binder, in Coq.setoid_ring.Ncring]
H:128 [binder, in Coq.MSets.MSetList]
H:129 [binder, in Coq.Reals.Runcountable]
h:129 [binder, in Coq.Vectors.VectorDef]
h:13 [binder, in Coq.Reals.Runcountable]
h:13 [binder, in Coq.Reals.Ranalysis4]
H:13 [binder, in Coq.Classes.Morphisms]
h:13 [binder, in Coq.Program.Combinators]
H:130 [binder, in Coq.Classes.Morphisms]
H:131 [binder, in Coq.MSets.MSetInterface]
H:131 [binder, in Coq.setoid_ring.Ncring_tac]
h:131 [binder, in Coq.Logic.FinFun]
H:132 [binder, in Coq.Classes.Morphisms]
H:133 [binder, in Coq.Classes.CMorphisms]
H:134 [binder, in Coq.MSets.MSetInterface]
h:134 [binder, in Coq.Logic.Hurkens]
h:135 [binder, in Coq.Logic.Eqdep_dec]
H:135 [binder, in Coq.omega.OmegaLemmas]
H:137 [binder, in Coq.MSets.MSetInterface]
H:137 [binder, in Coq.Classes.Morphisms]
h:138 [binder, in Coq.Vectors.VectorDef]
h:138 [binder, in Coq.Logic.FinFun]
H:139 [binder, in Coq.Vectors.VectorDef]
h:14 [binder, in Coq.Reals.Ranalysis4]
H:14 [binder, in Coq.Classes.DecidableClass]
H:141 [binder, in Coq.omega.OmegaLemmas]
H:141 [binder, in Coq.Classes.CRelationClasses]
h:141 [binder, in Coq.Logic.FinFun]
H:142 [binder, in Coq.Classes.CMorphisms]
H:143 [binder, in Coq.MSets.MSetInterface]
H:143 [binder, in Coq.MSets.MSetList]
H:145 [binder, in Coq.MSets.MSetInterface]
h:145 [binder, in Coq.Reals.RiemannInt]
H:146 [binder, in Coq.Classes.CRelationClasses]
H:147 [binder, in Coq.omega.OmegaLemmas]
h:148 [binder, in Coq.Reals.Ranalysis1]
H:148 [binder, in Coq.MSets.MSetInterface]
H:148 [binder, in Coq.setoid_ring.Ncring]
h:148 [binder, in Coq.Vectors.VectorDef]
h:149 [binder, in Coq.Reals.Ranalysis1]
h:149 [binder, in Coq.Reals.RiemannInt]
h:149 [binder, in Coq.Vectors.VectorDef]
h:15 [binder, in Coq.Reals.Ranalysis4]
h:15 [binder, in Coq.ZArith.Zcompare]
h:150 [binder, in Coq.Reals.Ranalysis1]
H:150 [binder, in Coq.Vectors.VectorDef]
h:151 [binder, in Coq.Reals.Ranalysis1]
H:151 [binder, in Coq.MSets.MSetWeakList]
h:152 [binder, in Coq.Reals.Ranalysis1]
h:153 [binder, in Coq.Reals.Ranalysis1]
H:153 [binder, in Coq.MSets.MSetInterface]
H:153 [binder, in Coq.omega.OmegaLemmas]
h:154 [binder, in Coq.Reals.Ranalysis1]
h:155 [binder, in Coq.Reals.Ranalysis1]
H:155 [binder, in Coq.MSets.MSetInterface]
H:155 [binder, in Coq.Classes.Morphisms]
H:156 [binder, in Coq.omega.OmegaLemmas]
H:156 [binder, in Coq.Classes.CMorphisms]
H:157 [binder, in Coq.MSets.MSetList]
H:157 [binder, in Coq.Init.Logic]
h:158 [binder, in Coq.Numbers.DecimalFacts]
H:158 [binder, in Coq.MSets.MSetInterface]
h:158 [binder, in Coq.Numbers.HexadecimalFacts]
h:159 [binder, in Coq.Reals.Ranalysis1]
H:159 [binder, in Coq.setoid_ring.Ncring_tac]
H:159 [binder, in Coq.omega.OmegaLemmas]
h:16 [binder, in Coq.Reals.Ranalysis2]
h:16 [binder, in Coq.Reals.Ranalysis4]
H:16 [binder, in Coq.Classes.CMorphisms]
H:16 [binder, in Coq.Bool.BoolEq]
H:16 [binder, in Coq.Classes.DecidableClass]
H:16 [binder, in Coq.Bool.DecBool]
h:160 [binder, in Coq.Reals.Ranalysis1]
H:160 [binder, in Coq.Classes.CMorphisms]
H:161 [binder, in Coq.MSets.MSetInterface]
h:161 [binder, in Coq.FSets.FMapAVL]
H:163 [binder, in Coq.omega.OmegaLemmas]
H:163 [binder, in Coq.Classes.CMorphisms]
h:164 [binder, in Coq.Reals.Ranalysis1]
H:164 [binder, in Coq.MSets.MSetInterface]
h:165 [binder, in Coq.Reals.Ranalysis1]
h:165 [binder, in Coq.FSets.FMapAVL]
H:167 [binder, in Coq.omega.OmegaLemmas]
h:168 [binder, in Coq.Reals.RiemannInt]
H:168 [binder, in Coq.MSets.MSetRBT]
H:168 [binder, in Coq.NArith.Ndigits]
H:169 [binder, in Coq.Classes.Morphisms]
H:169 [binder, in Coq.Init.Logic]
h:17 [binder, in Coq.Reals.Ranalysis4]
H:17 [binder, in Coq.Classes.Morphisms]
H:17 [binder, in Coq.Classes.SetoidClass]
h:17 [binder, in Coq.Reals.PSeries_reg]
h:170 [binder, in Coq.FSets.FMapAVL]
H:170 [binder, in Coq.Classes.CMorphisms]
H:170 [binder, in Coq.MSets.MSetRBT]
H:171 [binder, in Coq.MSets.MSetInterface]
H:171 [binder, in Coq.MSets.MSetList]
H:171 [binder, in Coq.omega.OmegaLemmas]
H:172 [binder, in Coq.setoid_ring.Ncring_tac]
h:172 [binder, in Coq.Reals.RiemannInt]
H:173 [binder, in Coq.MSets.MSetWeakList]
H:173 [binder, in Coq.NArith.Ndigits]
h:173 [binder, in Coq.Logic.ClassicalFacts]
H:174 [binder, in Coq.Init.Logic]
H:176 [binder, in Coq.micromega.ZifyClasses]
H:176 [binder, in Coq.Classes.RelationClasses]
H:176 [binder, in Coq.Classes.Morphisms]
H:176 [binder, in Coq.MSets.MSetWeakList]
H:176 [binder, in Coq.Arith.PeanoNat]
H:176 [binder, in Coq.omega.OmegaLemmas]
H:177 [binder, in Coq.micromega.ZifyClasses]
h:177 [binder, in Coq.Logic.EqdepFacts]
h:177 [binder, in Coq.Reals.RiemannInt]
h:177 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
h:178 [binder, in Coq.FSets.FMapAVL]
h:179 [binder, in Coq.PArith.BinPos]
h:18 [binder, in Coq.Reals.Runcountable]
H:18 [binder, in Coq.setoid_ring.Ncring]
H:180 [binder, in Coq.MSets.MSetGenTree]
H:180 [binder, in Coq.Init.Logic]
h:181 [binder, in Coq.Vectors.VectorSpec]
H:181 [binder, in Coq.Classes.RelationClasses]
h:181 [binder, in Coq.Reals.RiemannInt]
H:181 [binder, in Coq.omega.OmegaLemmas]
H:182 [binder, in Coq.MSets.MSetInterface]
H:182 [binder, in Coq.setoid_ring.Ncring_tac]
h:183 [binder, in Coq.FSets.FMapAVL]
H:184 [binder, in Coq.omega.OmegaLemmas]
h:185 [binder, in Coq.Vectors.VectorSpec]
h:185 [binder, in Coq.Logic.ChoiceFacts]
H:185 [binder, in Coq.Classes.CMorphisms]
H:186 [binder, in Coq.Classes.Morphisms]
h:187 [binder, in Coq.Reals.RiemannInt]
h:187 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
h:188 [binder, in Coq.FSets.FMapAVL]
H:188 [binder, in Coq.omega.OmegaLemmas]
h:189 [binder, in Coq.Logic.ChoiceFacts]
h:19 [binder, in Coq.Reals.Ranalysis2]
H:19 [binder, in Coq.Classes.SetoidDec]
H:191 [binder, in Coq.Classes.Morphisms]
H:191 [binder, in Coq.Vectors.Fin]
h:191 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
H:192 [binder, in Coq.omega.OmegaLemmas]
H:192 [binder, in Coq.Vectors.Fin]
h:193 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
H:195 [binder, in Coq.Vectors.Fin]
h:196 [binder, in Coq.Logic.ChoiceFacts]
H:196 [binder, in Coq.Vectors.Fin]
H:197 [binder, in Coq.omega.OmegaLemmas]
h:197 [binder, in Coq.Reals.Ratan]
H:199 [binder, in Coq.Classes.CMorphisms]
h:2 [binder, in Coq.Reals.Ranalysis2]
H:2 [binder, in Coq.btauto.Algebra]
H:20 [binder, in Coq.Bool.BoolEq]
H:200 [binder, in Coq.setoid_ring.Ncring_tac]
H:201 [binder, in Coq.omega.OmegaLemmas]
H:202 [binder, in Coq.Classes.Morphisms]
H:204 [binder, in Coq.omega.OmegaLemmas]
H:205 [binder, in Coq.Vectors.Fin]
h:206 [binder, in Coq.FSets.FMapAVL]
H:206 [binder, in Coq.Classes.CMorphisms]
H:206 [binder, in Coq.Vectors.Fin]
H:208 [binder, in Coq.Classes.Morphisms]
H:208 [binder, in Coq.Init.Specif]
H:209 [binder, in Coq.Vectors.Fin]
h:21 [binder, in Coq.Numbers.Natural.Abstract.NBits]
h:21 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
H:210 [binder, in Coq.Vectors.Fin]
H:211 [binder, in Coq.Classes.Morphisms]
H:211 [binder, in Coq.Vectors.VectorDef]
H:216 [binder, in Coq.Classes.CMorphisms]
H:217 [binder, in Coq.Classes.Morphisms]
h:219 [binder, in Coq.Logic.EqdepFacts]
H:219 [binder, in Coq.Logic.ChoiceFacts]
H:22 [binder, in Coq.Classes.EquivDec]
H:221 [binder, in Coq.Classes.CMorphisms]
H:222 [binder, in Coq.Logic.ChoiceFacts]
h:225 [binder, in Coq.Logic.EqdepFacts]
H:226 [binder, in Coq.MSets.MSetList]
H:226 [binder, in Coq.Classes.CMorphisms]
h:229 [binder, in Coq.Logic.EqdepFacts]
H:23 [binder, in Coq.Classes.RelationPairs]
H:234 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
H:234 [binder, in Coq.Classes.CMorphisms]
h:238 [binder, in Coq.Logic.Hurkens]
H:238 [binder, in Coq.Vectors.VectorDef]
h:239 [binder, in Coq.Logic.Hurkens]
H:24 [binder, in Coq.Classes.SetoidDec]
H:24 [binder, in Coq.Logic.Diaconescu]
H:24 [binder, in Coq.Vectors.VectorDef]
H:245 [binder, in Coq.Classes.CMorphisms]
H:246 [binder, in Coq.MSets.MSetList]
H:246 [binder, in Coq.MSets.MSetGenTree]
H:249 [binder, in Coq.MSets.MSetList]
h:25 [binder, in Coq.Reals.Runcountable]
h:25 [binder, in Coq.Reals.Ranalysis5]
H:25 [binder, in Coq.Logic.Diaconescu]
h:251 [binder, in Coq.Logic.Hurkens]
H:251 [binder, in Coq.Classes.CMorphisms]
h:252 [binder, in Coq.Logic.Hurkens]
H:253 [binder, in Coq.MSets.MSetGenTree]
H:254 [binder, in Coq.Classes.CMorphisms]
h:256 [binder, in Coq.Reals.Ranalysis1]
h:257 [binder, in Coq.Reals.Ranalysis1]
H:257 [binder, in Coq.MSets.MSetInterface]
h:26 [binder, in Coq.Logic.EqdepFacts]
H:26 [binder, in Coq.Classes.RelationPairs]
h:260 [binder, in Coq.Reals.Ranalysis1]
H:260 [binder, in Coq.MSets.MSetInterface]
H:260 [binder, in Coq.Classes.CMorphisms]
h:262 [binder, in Coq.ssr.ssrfun]
H:262 [binder, in Coq.MSets.MSetGenTree]
h:263 [binder, in Coq.Reals.Ranalysis1]
H:263 [binder, in Coq.MSets.MSetInterface]
H:263 [binder, in Coq.setoid_ring.Ncring_tac]
h:265 [binder, in Coq.NArith.BinNat]
H:267 [binder, in Coq.MSets.MSetInterface]
h:269 [binder, in Coq.Reals.Ranalysis1]
h:269 [binder, in Coq.Reals.Ranalysis5]
H:27 [binder, in Coq.Logic.Eqdep_dec]
h:27 [binder, in Coq.Reals.PSeries_reg]
H:27 [binder, in Coq.setoid_ring.Ncring]
h:270 [binder, in Coq.Reals.Ranalysis1]
H:270 [binder, in Coq.MSets.MSetInterface]
H:271 [binder, in Coq.MSets.MSetGenTree]
h:272 [binder, in Coq.Reals.Ranalysis5]
h:273 [binder, in Coq.Reals.Ranalysis1]
h:273 [binder, in Coq.Reals.Ranalysis5]
h:274 [binder, in Coq.Reals.Ranalysis5]
H:275 [binder, in Coq.MSets.MSetGenTree]
h:275 [binder, in Coq.Reals.Ranalysis5]
H:275 [binder, in Coq.Init.Logic]
h:276 [binder, in Coq.Reals.Ranalysis1]
h:276 [binder, in Coq.Reals.Ranalysis5]
H:277 [binder, in Coq.setoid_ring.Ncring_tac]
H:277 [binder, in Coq.MSets.MSetGenTree]
H:279 [binder, in Coq.Init.Specif]
H:279 [binder, in Coq.MSets.MSetRBT]
H:28 [binder, in Coq.Logic.FunctionalExtensionality]
H:28 [binder, in Coq.Classes.EquivDec]
h:28 [binder, in Coq.Reals.PSeries_reg]
h:280 [binder, in Coq.Reals.Ranalysis5]
h:284 [binder, in Coq.Reals.Ranalysis5]
H:29 [binder, in Coq.Vectors.VectorSpec]
h:29 [binder, in Coq.Reals.Ranalysis2]
H:29 [binder, in Coq.Classes.RelationPairs]
H:29 [binder, in Coq.MSets.MSetFacts]
H:29 [binder, in Coq.Classes.SetoidDec]
h:29 [binder, in Coq.Reals.PSeries_reg]
H:290 [binder, in Coq.MSets.MSetRBT]
H:292 [binder, in Coq.ZArith.BinInt]
H:295 [binder, in Coq.ZArith.BinInt]
H:297 [binder, in Coq.Init.Logic]
H:3 [binder, in Coq.Classes.CEquivalence]
H:3 [binder, in Coq.Classes.Equivalence]
h:30 [binder, in Coq.Reals.PSeries_reg]
h:30 [binder, in Coq.Reals.Ranalysis5]
H:301 [binder, in Coq.MSets.MSetRBT]
H:308 [binder, in Coq.Init.Logic]
h:31 [binder, in Coq.Reals.Runcountable]
H:31 [binder, in Coq.MSets.MSetFacts]
h:31 [binder, in Coq.Reals.PSeries_reg]
h:31 [binder, in Coq.Reals.Ranalysis5]
h:31 [binder, in Coq.Vectors.VectorDef]
H:310 [binder, in Coq.NArith.BinNat]
H:310 [binder, in Coq.MSets.MSetRBT]
H:314 [binder, in Coq.Init.Logic]
H:317 [binder, in Coq.MSets.MSetRBT]
h:319 [binder, in Coq.Vectors.VectorDef]
H:32 [binder, in Coq.Classes.RelationPairs]
h:32 [binder, in Coq.Reals.PSeries_reg]
H:320 [binder, in Coq.MSets.MSetRBT]
H:320 [binder, in Coq.Vectors.VectorDef]
H:323 [binder, in Coq.MSets.MSetGenTree]
H:328 [binder, in Coq.MSets.MSetRBT]
h:33 [binder, in Coq.Logic.ExtensionalityFacts]
h:33 [binder, in Coq.Reals.PSeries_reg]
H:331 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
H:335 [binder, in Coq.MSets.MSetGenTree]
H:339 [binder, in Coq.MSets.MSetRBT]
H:34 [binder, in Coq.Vectors.VectorSpec]
H:34 [binder, in Coq.Classes.EquivDec]
h:34 [binder, in Coq.Reals.PSeries_reg]
H:34 [binder, in Coq.Vectors.VectorDef]
H:343 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
H:346 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
H:35 [binder, in Coq.Classes.RelationPairs]
H:35 [binder, in Coq.Logic.FunctionalExtensionality]
h:35 [binder, in Coq.Init.Wf]
h:35 [binder, in Coq.Reals.PSeries_reg]
h:35 [binder, in Coq.Logic.Classical_Prop]
h:36 [binder, in Coq.Reals.Rtrigo_reg]
h:36 [binder, in Coq.Reals.PSeries_reg]
H:36 [binder, in Coq.setoid_ring.Ncring]
H:369 [binder, in Coq.MSets.MSetRBT]
h:37 [binder, in Coq.Reals.Ranalysis2]
h:37 [binder, in Coq.Reals.Rtrigo_reg]
h:37 [binder, in Coq.Reals.PSeries_reg]
H:37 [binder, in Coq.Numbers.Natural.Abstract.NGcd]
H:372 [binder, in Coq.Init.Specif]
H:372 [binder, in Coq.MSets.MSetGenTree]
H:374 [binder, in Coq.MSets.MSetRBT]
H:376 [binder, in Coq.MSets.MSetGenTree]
H:377 [binder, in Coq.MSets.MSetRBT]
h:38 [binder, in Coq.Reals.Runcountable]
H:38 [binder, in Coq.Classes.RelationClasses]
H:38 [binder, in Coq.Classes.RelationPairs]
h:38 [binder, in Coq.Reals.PSeries_reg]
H:38 [binder, in Coq.Numbers.Natural.Abstract.NGcd]
H:381 [binder, in Coq.MSets.MSetRBT]
H:384 [binder, in Coq.MSets.MSetRBT]
H:39 [binder, in Coq.Vectors.VectorSpec]
h:39 [binder, in Coq.Reals.PSeries_reg]
H:39 [binder, in Coq.Numbers.Natural.Abstract.NGcd]
H:395 [binder, in Coq.MSets.MSetRBT]
H:398 [binder, in Coq.MSets.MSetRBT]
h:4 [binder, in Coq.Reals.Sqrt_reg]
H:4 [binder, in Coq.Init.Peano]
H:4 [binder, in Coq.btauto.Algebra]
H:4 [binder, in Coq.ZArith.Znumtheory]
h:4 [binder, in Coq.Vectors.VectorDef]
H:4 [binder, in Coq.Bool.DecBool]
h:40 [binder, in Coq.Reals.Ranalysis2]
h:40 [binder, in Coq.Numbers.Natural.Abstract.NBits]
h:40 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
h:40 [binder, in Coq.Reals.PSeries_reg]
H:40 [binder, in Coq.Numbers.Natural.Abstract.NGcd]
H:41 [binder, in Coq.Classes.EquivDec]
H:41 [binder, in Coq.Vectors.VectorEq]
H:42 [binder, in Coq.Logic.FunctionalExtensionality]
h:42 [binder, in Coq.Logic.Berardi]
H:428 [binder, in Coq.MSets.MSetRBT]
h:43 [binder, in Coq.Vectors.VectorDef]
h:431 [binder, in Coq.Reals.RiemannInt]
h:438 [binder, in Coq.Reals.RiemannInt]
H:44 [binder, in Coq.Classes.RelationPairs]
H:44 [binder, in Coq.Vectors.VectorEq]
H:444 [binder, in Coq.MSets.MSetRBT]
H:447 [binder, in Coq.MSets.MSetRBT]
H:45 [binder, in Coq.setoid_ring.Ncring_tac]
h:45 [binder, in Coq.FSets.FMapFullAVL]
H:45 [binder, in Coq.setoid_ring.Ncring]
H:45 [binder, in Coq.Vectors.VectorEq]
H:45 [binder, in Coq.Vectors.VectorDef]
H:459 [binder, in Coq.Init.Logic]
H:46 [binder, in Coq.Classes.RelationPairs]
H:463 [binder, in Coq.MSets.MSetRBT]
H:48 [binder, in Coq.Classes.RelationPairs]
h:48 [binder, in Coq.Reals.Ranalysis5]
H:48 [binder, in Coq.Vectors.VectorDef]
H:49 [binder, in Coq.Classes.CRelationClasses]
h:49 [binder, in Coq.Reals.Ranalysis5]
H:490 [binder, in Coq.ZArith.BinInt]
H:490 [binder, in Coq.MSets.MSetRBT]
H:494 [binder, in Coq.MSets.MSetRBT]
H:498 [binder, in Coq.MSets.MSetRBT]
h:5 [binder, in Coq.Reals.Sqrt_reg]
h:5 [binder, in Coq.Logic.Eqdep]
H:5 [binder, in Coq.Logic.ClassicalFacts]
H:50 [binder, in Coq.Classes.RelationPairs]
h:50 [binder, in Coq.FSets.FMapFullAVL]
H:502 [binder, in Coq.MSets.MSetAVL]
h:508 [binder, in Coq.Reals.RiemannInt]
H:51 [binder, in Coq.Classes.Morphisms]
H:51 [binder, in Coq.Logic.FunctionalExtensionality]
H:51 [binder, in Coq.Classes.EquivDec]
h:51 [binder, in Coq.Reals.Ratan]
H:513 [binder, in Coq.MSets.MSetAVL]
h:515 [binder, in Coq.Reals.RiemannInt]
H:516 [binder, in Coq.MSets.MSetRBT]
H:516 [binder, in Coq.Init.Logic]
H:523 [binder, in Coq.MSets.MSetAVL]
H:523 [binder, in Coq.MSets.MSetRBT]
H:524 [binder, in Coq.Init.Specif]
H:526 [binder, in Coq.MSets.MSetAVL]
H:527 [binder, in Coq.MSets.MSetRBT]
h:529 [binder, in Coq.Reals.RiemannInt]
H:53 [binder, in Coq.Numbers.Integer.Abstract.ZGcd]
H:53 [binder, in Coq.Classes.CMorphisms]
H:534 [binder, in Coq.MSets.MSetAVL]
H:536 [binder, in Coq.MSets.MSetRBT]
H:539 [binder, in Coq.MSets.MSetRBT]
H:54 [binder, in Coq.Numbers.Integer.Abstract.ZGcd]
H:54 [binder, in Coq.setoid_ring.Ncring]
h:542 [binder, in Coq.MSets.MSetAVL]
H:544 [binder, in Coq.MSets.MSetRBT]
h:546 [binder, in Coq.MSets.MSetAVL]
H:547 [binder, in Coq.MSets.MSetAVL]
H:55 [binder, in Coq.Numbers.Integer.Abstract.ZGcd]
H:55 [binder, in Coq.Classes.RelationPairs]
H:55 [binder, in Coq.Vectors.VectorEq]
H:55 [binder, in Coq.Reals.ClassicalConstructiveReals]
h:551 [binder, in Coq.MSets.MSetAVL]
H:551 [binder, in Coq.MSets.MSetRBT]
H:552 [binder, in Coq.MSets.MSetAVL]
H:555 [binder, in Coq.MSets.MSetRBT]
H:558 [binder, in Coq.MSets.MSetAVL]
H:558 [binder, in Coq.MSets.MSetRBT]
H:56 [binder, in Coq.setoid_ring.Ncring_initial]
H:56 [binder, in Coq.Numbers.Integer.Abstract.ZGcd]
H:56 [binder, in Coq.setoid_ring.Ncring_tac]
h:562 [binder, in Coq.Reals.RiemannInt]
H:566 [binder, in Coq.MSets.MSetAVL]
H:567 [binder, in Coq.MSets.MSetRBT]
H:569 [binder, in Coq.MSets.MSetAVL]
H:572 [binder, in Coq.MSets.MSetRBT]
H:575 [binder, in Coq.MSets.MSetAVL]
H:576 [binder, in Coq.MSets.MSetRBT]
H:58 [binder, in Coq.Vectors.VectorEq]
H:583 [binder, in Coq.MSets.MSetAVL]
H:587 [binder, in Coq.MSets.MSetAVL]
H:59 [binder, in Coq.Vectors.VectorEq]
H:590 [binder, in Coq.MSets.MSetAVL]
H:593 [binder, in Coq.MSets.MSetAVL]
H:6 [binder, in Coq.btauto.Algebra]
H:6 [binder, in Coq.Classes.SetoidTactics]
H:6 [binder, in Coq.Classes.CEquivalence]
H:6 [binder, in Coq.Classes.DecidableClass]
H:6 [binder, in Coq.Logic.ClassicalFacts]
H:6 [binder, in Coq.Init.Tactics]
H:6 [binder, in Coq.Classes.Equivalence]
H:60 [binder, in Coq.Classes.CRelationClasses]
H:600 [binder, in Coq.MSets.MSetAVL]
H:603 [binder, in Coq.MSets.MSetAVL]
H:606 [binder, in Coq.MSets.MSetAVL]
h:61 [binder, in Coq.Numbers.HexadecimalPos]
H:61 [binder, in Coq.Classes.EquivDec]
h:61 [binder, in Coq.Numbers.DecimalPos]
H:612 [binder, in Coq.MSets.MSetAVL]
H:616 [binder, in Coq.MSets.MSetAVL]
h:618 [binder, in Coq.PArith.BinPos]
H:620 [binder, in Coq.MSets.MSetAVL]
H:626 [binder, in Coq.MSets.MSetAVL]
h:63 [binder, in Coq.Reals.Ranalysis2]
H:63 [binder, in Coq.setoid_ring.Ncring]
H:630 [binder, in Coq.MSets.MSetAVL]
H:635 [binder, in Coq.MSets.MSetAVL]
H:639 [binder, in Coq.MSets.MSetAVL]
H:649 [binder, in Coq.MSets.MSetAVL]
H:65 [binder, in Coq.Logic.Eqdep_dec]
H:66 [binder, in Coq.Classes.RelationClasses]
H:662 [binder, in Coq.MSets.MSetAVL]
H:665 [binder, in Coq.MSets.MSetAVL]
H:67 [binder, in Coq.Program.Wf]
h:67 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
H:67 [binder, in Coq.setoid_ring.Ncring_tac]
H:675 [binder, in Coq.Init.Specif]
H:68 [binder, in Coq.Classes.RelationClasses]
h:69 [binder, in Coq.Reals.Ranalysis2]
h:69 [binder, in Coq.Init.Wf]
H:7 [binder, in Coq.Strings.Byte]
H:7 [binder, in Coq.Logic.ClassicalFacts]
H:70 [binder, in Coq.Classes.RelationClasses]
H:72 [binder, in Coq.Classes.RelationClasses]
H:72 [binder, in Coq.setoid_ring.Ncring]
H:74 [binder, in Coq.MSets.MSetWeakList]
h:74 [binder, in Coq.Vectors.VectorDef]
H:75 [binder, in Coq.Classes.RelationClasses]
H:75 [binder, in Coq.PArith.Pnat]
H:75 [binder, in Coq.Classes.CRelationClasses]
H:77 [binder, in Coq.Logic.EqdepFacts]
H:77 [binder, in Coq.Classes.RelationClasses]
h:77 [binder, in Coq.ssr.ssrfun]
H:77 [binder, in Coq.Classes.CRelationClasses]
H:78 [binder, in Coq.Classes.Morphisms]
H:79 [binder, in Coq.setoid_ring.Ncring_tac]
H:79 [binder, in Coq.Classes.CRelationClasses]
H:79 [binder, in Coq.Vectors.VectorDef]
h:8 [binder, in Coq.Reals.Ranalysis2]
H:8 [binder, in Coq.btauto.Algebra]
h:8 [binder, in Coq.FSets.FMapFullAVL]
H:8 [binder, in Coq.Classes.DecidableClass]
H:8 [binder, in Coq.Logic.ClassicalFacts]
h:80 [binder, in Coq.Logic.Eqdep_dec]
H:80 [binder, in Coq.Classes.RelationClasses]
H:81 [binder, in Coq.Classes.CMorphisms]
H:81 [binder, in Coq.Classes.CRelationClasses]
H:83 [binder, in Coq.Classes.RelationClasses]
H:83 [binder, in Coq.MSets.MSetWeakList]
H:84 [binder, in Coq.Logic.EqdepFacts]
H:84 [binder, in Coq.Classes.CRelationClasses]
h:85 [binder, in Coq.Program.Wf]
H:85 [binder, in Coq.Logic.FunctionalExtensionality]
H:86 [binder, in Coq.Classes.CRelationClasses]
H:87 [binder, in Coq.Classes.RelationClasses]
H:87 [binder, in Coq.Structures.OrderedType]
h:87 [binder, in Coq.Reals.Rlimit]
h:88 [binder, in Coq.Reals.MVT]
h:89 [binder, in Coq.Reals.MVT]
H:89 [binder, in Coq.omega.OmegaLemmas]
H:89 [binder, in Coq.Classes.CRelationClasses]
H:9 [binder, in Coq.Classes.SetoidTactics]
h:9 [binder, in Coq.Logic.ProofIrrelevanceFacts]
H:90 [binder, in Coq.Classes.Morphisms]
H:90 [binder, in Coq.MSets.MSetWeakList]
H:90 [binder, in Coq.Structures.OrderedType]
H:91 [binder, in Coq.FSets.FSetBridge]
H:91 [binder, in Coq.Logic.EqdepFacts]
H:91 [binder, in Coq.setoid_ring.Ncring_tac]
h:91 [binder, in Coq.Vectors.VectorDef]
H:92 [binder, in Coq.Classes.RelationClasses]
H:92 [binder, in Coq.Classes.Morphisms]
H:92 [binder, in Coq.Classes.CRelationClasses]
H:92 [binder, in Coq.ZArith.Znumtheory]
H:93 [binder, in Coq.Structures.OrderedType]
H:93 [binder, in Coq.ZArith.Znumtheory]
H:94 [binder, in Coq.MSets.MSetInterface]
H:94 [binder, in Coq.FSets.FSetBridge]
H:94 [binder, in Coq.Classes.RelationClasses]
H:94 [binder, in Coq.MSets.MSetList]
H:94 [binder, in Coq.omega.OmegaLemmas]
H:94 [binder, in Coq.ZArith.Znumtheory]
h:941 [binder, in Coq.FSets.FMapAVL]
H:95 [binder, in Coq.Classes.Morphisms]
H:95 [binder, in Coq.Classes.CMorphisms]
H:95 [binder, in Coq.ZArith.Znumtheory]
h:950 [binder, in Coq.FSets.FMapAVL]
h:956 [binder, in Coq.FSets.FMapAVL]
H:96 [binder, in Coq.Classes.RelationClasses]
H:96 [binder, in Coq.Logic.FunctionalExtensionality]
H:96 [binder, in Coq.Classes.CRelationClasses]
h:962 [binder, in Coq.FSets.FMapAVL]
h:968 [binder, in Coq.FSets.FMapAVL]
H:97 [binder, in Coq.Init.Datatypes]
h:97 [binder, in Coq.Vectors.VectorDef]
h:97 [binder, in Coq.Logic.FinFun]
h:974 [binder, in Coq.FSets.FMapAVL]
H:98 [binder, in Coq.Logic.EqdepFacts]
H:98 [binder, in Coq.Classes.RelationClasses]
H:98 [binder, in Coq.Classes.Morphisms]
h:98 [binder, in Coq.Logic.FunctionalExtensionality]
H:98 [binder, in Coq.Classes.CMorphisms]
h:98 [binder, in Coq.Reals.PSeries_reg]
h:980 [binder, in Coq.FSets.FMapAVL]
H:99 [binder, in Coq.Program.Wf]
h:99 [binder, in Coq.Logic.FunctionalExtensionality]
H:99 [binder, 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) |