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 | (25959 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 | (999 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 | (811 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 | (1769 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 | (588 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 | (11879 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 | (960 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 | (508 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 | (307 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 | (479 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 | (495 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 | (905 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 | (1199 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 | (4894 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 | (166 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]

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]

HdRel [inductive, in Coq.Sorting.Sorted]

HdRel_inv [lemma, in Coq.Sorting.Sorted]

HdRel_sind [definition, in Coq.Sorting.Sorted]

HdRel_ind [definition, in Coq.Sorting.Sorted]

HdRel_cons [constructor, in Coq.Sorting.Sorted]

HdRel_nil [constructor, in Coq.Sorting.Sorted]

hd_error_skipn [lemma, in Coq.Lists.List]

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

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

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

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

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]

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]

hexadecimal_eq_dec [definition, in Coq.Init.Hexadecimal]

HexString [library]

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

HLevels [library]

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]

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]

hset_hOneType [lemma, in Coq.Logic.HLevels]

hset_hprop [lemma, in Coq.Logic.HLevels]

Hurkens [library]

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]

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 | (25959 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 | (999 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 | (811 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 | (1769 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 | (588 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 | (11879 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 | (960 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 | (508 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 | (307 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 | (479 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 | (495 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 | (905 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 | (1199 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 | (4894 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 | (166 entries) |