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 | (75519 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 | (245 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |

## F (constructor)

Fa [in MetaCoq.Examples.tauto]Fallback [in MetaCoq.SafeChecker.PCUICSafeConversion]

Finite [in MetaCoq.Template.BasicAst]

Finite [in MetaCoq.Erasure.EAst]

firstorder_spine_cons [in MetaCoq.PCUIC.PCUICFirstorder]

firstorder_spine_nil [in MetaCoq.PCUIC.PCUICFirstorder]

firstorder_value_C [in MetaCoq.PCUIC.PCUICFirstorder]

Fix [in MetaCoq.PCUIC.Syntax.PCUICPosition]

Fix [in MetaCoq.PCUIC.PCUICTyping]

FixMfixMismatch [in MetaCoq.SafeChecker.PCUICErrors]

FixRargMismatch [in MetaCoq.SafeChecker.PCUICErrors]

fix_lambda_other [in MetaCoq.PCUIC.Syntax.PCUICViews]

fix_lambda_fix [in MetaCoq.PCUIC.Syntax.PCUICViews]

fix_lambda_lambda [in MetaCoq.PCUIC.Syntax.PCUICViews]

fix_lambda_app_other [in MetaCoq.PCUIC.Syntax.PCUICViews]

fix_lambda_app_lambda [in MetaCoq.PCUIC.Syntax.PCUICViews]

fix_lambda_app_fix [in MetaCoq.PCUIC.Syntax.PCUICViews]

fix_red_body [in MetaCoq.Template.Typing]

fix_red_ty [in MetaCoq.Template.Typing]

Fix_app [in MetaCoq.PCUIC.Syntax.PCUICPosition]

fix_mfix_bd [in MetaCoq.PCUIC.Syntax.PCUICPosition]

fix_mfix_ty [in MetaCoq.PCUIC.Syntax.PCUICPosition]

fix_red_body [in MetaCoq.PCUIC.PCUICReduction]

fix_red_ty [in MetaCoq.PCUIC.PCUICReduction]

Forall_type_spine_cons [in MetaCoq.Template.Typing]

Forall_type_spine_nil [in MetaCoq.Template.Typing]

fo_None [in MetaCoq.Template.utils.MCOption]

fo_Some [in MetaCoq.Template.utils.MCOption]

fuel [in MetaCoq.Template.utils.MCUtils]