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 | (21445 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 | (889 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 | (714 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 | (1464 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 | (482 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 | (10031 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 | (663 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 | (537 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 | (374 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 | (285 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 | (457 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 | (616 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 | (1328 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 | (3468 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 | (137 entries) |

## F (definition)

f [in Coq.Logic.Berardi]fact [in Coq.Arith.Factorial]

FalseP [in Coq.Logic.ClassicalFacts]

false_predicate [in Coq.Classes.RelationClasses]

family_closed_set [in Coq.Reals.Rtopology]

family_finite [in Coq.Reals.Rtopology]

family_open_set [in Coq.Reals.Rtopology]

Fapp [in Coq.setoid_ring.Field_theory]

fast_Zred_factor6 [in Coq.omega.OmegaLemmas]

fast_Zred_factor5 [in Coq.omega.OmegaLemmas]

fast_Zred_factor4 [in Coq.omega.OmegaLemmas]

fast_Zred_factor3 [in Coq.omega.OmegaLemmas]

fast_Zred_factor2 [in Coq.omega.OmegaLemmas]

fast_Zred_factor1 [in Coq.omega.OmegaLemmas]

fast_Zmult_assoc_reverse [in Coq.omega.OmegaLemmas]

fast_Zmult_opp_comm [in Coq.omega.OmegaLemmas]

fast_Zmult_plus_distr_l [in Coq.omega.OmegaLemmas]

fast_Zopp_mult_distr_r [in Coq.omega.OmegaLemmas]

fast_Zopp_involutive [in Coq.omega.OmegaLemmas]

fast_Zopp_plus_distr [in Coq.omega.OmegaLemmas]

fast_Zmult_comm [in Coq.omega.OmegaLemmas]

fast_Zopp_eq_mult_neg_1 [in Coq.omega.OmegaLemmas]

fast_Zred_factor0 [in Coq.omega.OmegaLemmas]

fast_OMEGA14 [in Coq.omega.OmegaLemmas]

fast_OMEGA13 [in Coq.omega.OmegaLemmas]

fast_OMEGA16 [in Coq.omega.OmegaLemmas]

fast_OMEGA15 [in Coq.omega.OmegaLemmas]

fast_OMEGA12 [in Coq.omega.OmegaLemmas]

fast_OMEGA11 [in Coq.omega.OmegaLemmas]

fast_OMEGA10 [in Coq.omega.OmegaLemmas]

fast_Zplus_permute [in Coq.omega.OmegaLemmas]

fast_Zplus_assoc [in Coq.omega.OmegaLemmas]

fast_Zplus_assoc_reverse [in Coq.omega.OmegaLemmas]

fast_Zplus_comm [in Coq.omega.OmegaLemmas]

Fcons [in Coq.setoid_ring.Field_theory]

Fcons0 [in Coq.setoid_ring.Field_theory]

Fcons00 [in Coq.setoid_ring.Field_theory]

Fcons1 [in Coq.setoid_ring.Field_theory]

Fcons2 [in Coq.setoid_ring.Field_theory]

fct_cte [in Coq.Reals.Ranalysis1]

FEeval [in Coq.setoid_ring.Field_theory]

FF [in Coq.Reals.RList]

ff [in Coq.micromega.Tauto]

fibonacci [in Coq.ZArith.Zgcd_alt]

filter [in Coq.Lists.List]

find [in Coq.micromega.VarMap]

find [in Coq.Lists.List]

findA [in Coq.Lists.SetoidList]

findex [in Coq.Strings.String]

Finite [in Coq.Logic.FinFun]

Finite' [in Coq.Logic.FinFun]

Fin2Restrict.extend [in Coq.Logic.FinFun]

Fin2Restrict.f2n [in Coq.Logic.FinFun]

Fin2Restrict.f2n_inj [in Coq.Logic.FinFun]

Fin2Restrict.f2n_n2f [in Coq.Logic.FinFun]

Fin2Restrict.f2n_ok [in Coq.Logic.FinFun]

Fin2Restrict.n2f_ext [in Coq.Logic.FinFun]

Fin2Restrict.n2f_f2n [in Coq.Logic.FinFun]

Fin2Restrict.restrict [in Coq.Logic.FinFun]

firstl [in Coq.Numbers.Cyclic.Int31.Int31]

firstn [in Coq.Lists.List]

firstr [in Coq.Numbers.Cyclic.Int31.Int31]

Fix [in Coq.Init.Wf]

Fix_sub [in Coq.Program.Wf]

Fix_F_sub [in Coq.Program.Wf]

Fix_F_2 [in Coq.Init.Wf]

Fix_F [in Coq.Init.Wf]

fix_proto [in Coq.Program.Tactics]

flat_map [in Coq.Lists.List]

flip [in Coq.Classes.CRelationClasses]

flip [in Coq.Program.Basics]

flip_proper [in Coq.Classes.Morphisms]

flip_Antisymmetric [in Coq.Classes.CRelationClasses]

flip_Transitive [in Coq.Classes.CRelationClasses]

flip_Asymmetric [in Coq.Classes.CRelationClasses]

flip_Symmetric [in Coq.Classes.CRelationClasses]

flip_Irreflexive [in Coq.Classes.CRelationClasses]

flip_Antisymmetric [in Coq.Classes.RelationClasses]

flip_Transitive [in Coq.Classes.RelationClasses]

flip_Asymmetric [in Coq.Classes.RelationClasses]

flip_Symmetric [in Coq.Classes.RelationClasses]

flip_Irreflexive [in Coq.Classes.RelationClasses]

flip_proper [in Coq.Classes.CMorphisms]

floor [in Coq.ZArith.Zcomplements]

floor_pos [in Coq.ZArith.Zcomplements]

Fnorm [in Coq.setoid_ring.Field_theory]

fold_left2 [in Coq.Vectors.VectorDef]

fold_right2 [in Coq.Vectors.VectorDef]

fold_right [in Coq.Vectors.VectorDef]

fold_left [in Coq.Vectors.VectorDef]

fold_right [in Coq.Lists.List]

fold_left [in Coq.Lists.List]

forallb [in Coq.Lists.List]

ForallPairs [in Coq.Lists.List]

forall_relation [in Coq.Classes.Morphisms]

forall_def [in Coq.Classes.Morphisms]

forall_eq_rect_comp [in Coq.Logic.FunctionalExtensionality]

forall_eq_rect [in Coq.Logic.FunctionalExtensionality]

forall_relation [in Coq.Classes.CMorphisms]

forall_def [in Coq.Classes.CMorphisms]

formula_eval [in Coq.btauto.Reflect]

form_eq [in Coq.rtauto.Rtauto]

frac_part [in Coq.Reals.R_Ifp]

frame_tan [in Coq.Reals.Ratan]

fst [in Coq.Init.Datatypes]

FS_inj [in Coq.Vectors.Fin]

Full [in Coq.Logic.FinFun]

Fullset [in Coq.Sets.Uniset]

funcomp [in Coq.ssr.ssrfun]

FunctionalChoice_on [in Coq.Logic.ChoiceFacts]

FunctionalChoice_on_rel [in Coq.Logic.ChoiceFacts]

FunctionalCountableChoice_on [in Coq.Logic.ChoiceFacts]

FunctionalDependentChoice_on [in Coq.Logic.ChoiceFacts]

FunctionalRelReification_on [in Coq.Logic.ChoiceFacts]

functional_extensionality_dep_good [in Coq.Logic.FunctionalExtensionality]

fun_of_simpl [in Coq.ssr.ssrfun]

f_equal_R [in Coq.Reals.RIneq]

f_equal__functional_extensionality_dep_good__fun [in Coq.Logic.FunctionalExtensionality]

f_equal__functional_extensionality_dep_good [in Coq.Logic.FunctionalExtensionality]

f_equal2_mult [in Coq.Init.Peano]

f_equal2_nat [in Coq.Init.Peano]

f_equal2_plus [in Coq.Init.Peano]

f_equal_pred [in Coq.Init.Peano]

f_equal_nat [in Coq.Init.Peano]

F2AF [in Coq.setoid_ring.Field_theory]

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 | (21445 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 | (889 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 | (714 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 | (1464 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 | (482 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 | (10031 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 | (663 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 | (537 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 | (374 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 | (285 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 | (457 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 | (616 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 | (1328 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 | (3468 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 | (137 entries) |