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 | (72679 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 | (1040 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 | (47172 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 | (791 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 | (1553 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 | (585 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 | (11862 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 | (1030 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 | (625 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 | (308 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 | (474 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 | (493 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 | (896 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 | (1443 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 | (4242 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 | (165 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:111 [binder, in Coq.micromega.ZifyInst]

Ha:94 [binder, in Coq.Arith.PeanoNat]

Hbeq:21 [binder, in Coq.Vectors.VectorEq]

Hb:23 [binder, in Coq.ZArith.Zdiv]

Hb:35 [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:215 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

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 [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

head0 [axiom, in Coq.Numbers.Cyclic.Int63.PrimInt63]

head0 [abbreviation, in Coq.Numbers.Cyclic.Int63.Uint63]

head0_spec [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

head0_spec [axiom, in Coq.Numbers.Cyclic.Int63.Uint63]

head00_spec [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

head00_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

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:216 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

Heq:223 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

Heq:235 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

Here [constructor, in Coq.Lists.Streams]

here [constructor, in Coq.Logic.WKL]

HereAndFurther [constructor, in Coq.Lists.Streams]

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:339 [binder, in Coq.Init.Logic]

Hf:344 [binder, in Coq.Init.Logic]

high_bit [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]

high_bit [definition, in Coq.Numbers.Cyclic.Int63.Uint63]

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:254 [binder, in Coq.Vectors.VectorSpec]

Hi2:255 [binder, in Coq.Vectors.VectorSpec]

Hi:225 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

Hi:247 [binder, in Coq.Vectors.VectorSpec]

Hi:301 [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:300 [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:277 [binder, in Coq.ZArith.BinInt]

Hp:278 [binder, in Coq.ZArith.BinInt]

Hp:282 [binder, in Coq.ZArith.BinInt]

Hp:283 [binder, in Coq.ZArith.BinInt]

Hqgt0:24 [binder, in Coq.Reals.Cauchy.QExtra]

Hqgt0:26 [binder, in Coq.Reals.Cauchy.QExtra]

Hqgt0:32 [binder, in Coq.Reals.Cauchy.QExtra]

Hqgt0:35 [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.Hurkens]

H':120 [binder, in Coq.Logic.FunctionalExtensionality]

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':418 [binder, in Coq.micromega.ZMicromega]

H':420 [binder, in Coq.micromega.ZMicromega]

H':422 [binder, in Coq.micromega.ZMicromega]

H':424 [binder, in Coq.micromega.ZMicromega]

H':438 [binder, in Coq.micromega.ZMicromega]

H':440 [binder, in Coq.micromega.ZMicromega]

H':493 [binder, in Coq.ZArith.BinInt]

h':658 [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':299 [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:297 [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:326 [binder, in Coq.MSets.MSetGenTree]

H1:333 [binder, in Coq.Init.Logic]

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':300 [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:29 [binder, in Coq.Reals.Rderiv]

H2:29 [binder, in Coq.Reals.Rtrigo_fun]

H2:298 [binder, in Coq.Init.Logic]

H2:3 [binder, in Coq.Reals.Rtrigo_fun]

H2:31 [binder, in Coq.Reals.Rderiv]

H2:31 [binder, in Coq.Reals.Rtrigo_fun]

H2:33 [binder, in Coq.Reals.Rderiv]

H2:33 [binder, in Coq.Reals.Rtrigo_fun]

H2:334 [binder, in Coq.Init.Logic]

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.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.Logic.FunctionalExtensionality]

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.Logic.FunctionalExtensionality]

H:104 [binder, in Coq.omega.OmegaLemmas]

H:105 [binder, in Coq.Logic.EqdepFacts]

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:1063 [binder, in Coq.Init.Specif]

H:107 [binder, in Coq.Classes.Morphisms]

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.Logic.FunctionalExtensionality]

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.Logic.FunctionalExtensionality]

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.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.omega.OmegaLemmas]

H:121 [binder, in Coq.setoid_ring.Ncring_tac]

H:121 [binder, in Coq.Classes.CMorphisms]

h:122 [binder, in Coq.Logic.FunctionalExtensionality]

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.Reals.Rpower]

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: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:168 [binder, in Coq.Init.Logic]

H:169 [binder, in Coq.Classes.Morphisms]

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: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.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:178 [binder, in Coq.Arith.PeanoNat]

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.micromega.ZifyClasses]

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.micromega.ZifyClasses]

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:185 [binder, in Coq.Init.Logic]

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.Init.Logic]

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: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:228 [binder, in Coq.Init.Specif]

h:229 [binder, in Coq.Logic.EqdepFacts]

H:229 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

H:23 [binder, in Coq.Classes.RelationPairs]

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:268 [binder, in Coq.Vectors.VectorSpec]

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: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.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:286 [binder, in Coq.Vectors.VectorSpec]

H:286 [binder, in Coq.Init.Logic]

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:294 [binder, in Coq.ZArith.BinInt]

H:297 [binder, in Coq.ZArith.BinInt]

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:317 [binder, in Coq.MSets.MSetRBT]

H:319 [binder, in Coq.Init.Logic]

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:325 [binder, in Coq.Init.Logic]

H:326 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

H:328 [binder, in Coq.MSets.MSetRBT]

h:33 [binder, in Coq.Logic.ExtensionalityFacts]

h:33 [binder, in Coq.Reals.PSeries_reg]

H:335 [binder, in Coq.MSets.MSetGenTree]

H:338 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

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:341 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

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:362 [binder, in Coq.micromega.ZMicromega]

H:363 [binder, in Coq.micromega.ZMicromega]

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:370 [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.Logic.Adjointification]

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:41 [binder, in Coq.Reals.ClassicalDedekindReals]

H:42 [binder, in Coq.Logic.FunctionalExtensionality]

h:42 [binder, in Coq.Logic.Berardi]

H:428 [binder, in Coq.MSets.MSetRBT]

H:428 [binder, in Coq.micromega.ZMicromega]

H:429 [binder, in Coq.micromega.ZMicromega]

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.Logic.Adjointification]

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: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.MSets.MSetRBT]

H:492 [binder, in Coq.ZArith.BinInt]

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:523 [binder, in Coq.MSets.MSetAVL]

H:523 [binder, in Coq.MSets.MSetRBT]

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.Init.Specif]

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:644 [binder, in Coq.Init.Logic]

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: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.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.PArith.Pnat]

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:803 [binder, in Coq.Init.Specif]

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:962 [binder, in Coq.Init.Logic]

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.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 | (72679 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 | (1040 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 | (47172 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 | (791 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 | (1553 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 | (585 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 | (11862 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 | (1030 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 | (625 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 | (308 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 | (474 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 | (493 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 | (896 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 | (1443 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 | (4242 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 | (165 entries) |