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 | (22221 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 | (923 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 | (744 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 | (1480 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 | (501 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 | (10364 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 | (910 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 | (573 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 | (386 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 | (286 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 | (465 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 | (632 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 | (1133 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 | (3679 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 | (145 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_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 [definition, in Coq.Vectors.VectorDef]

hd [abbreviation, in Coq.setoid_ring.Ring_polynom]

hd [definition, in Coq.micromega.Env]

hd [definition, in Coq.Lists.List]

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

head0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

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]

Here [constructor, in Coq.Lists.Streams]

here [constructor, in Coq.Logic.WKL]

HereAndFurther [constructor, in Coq.Lists.Streams]

HexString [library]

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

homoLR [lemma, in Coq.ssr.ssrbool]

homoLR_in [lemma, 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_mono_in [lemma, in Coq.ssr.ssrbool]

homo_mono [lemma, in Coq.ssr.ssrbool]

Hurkens [library]

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 | (22221 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 | (923 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 | (744 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 | (1480 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 | (501 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 | (10364 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 | (910 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 | (573 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 | (386 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 | (286 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 | (465 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 | (632 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 | (1133 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 | (3679 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 | (145 entries) |