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) |

## W (section)

Wcbv [in MetaCoq.PCUIC.PCUICWcbvEval]Wcbv [in MetaCoq.Template.WcbvEval]

Wcbv [in MetaCoq.Erasure.EWcbvEval]

Wcbv [in MetaCoq.Erasure.EWcbvEval]

WcbvEnv [in MetaCoq.Erasure.EWcbvEval]

WeakEtaExp [in MetaCoq.Erasure.EEtaExpanded]

WeakNormalization [in MetaCoq.PCUIC.PCUICCanonicity]

WeakNormalization.reducible [in MetaCoq.PCUIC.PCUICCanonicity]

WeightedGraph.ExtendLabelling [in MetaCoq.Template.utils.wGraph]

WeightedGraph.FirstVertexIn [in MetaCoq.Template.utils.wGraph]

WeightedGraph.graph [in MetaCoq.Template.utils.wGraph]

WeightedGraph.IsFullSubgraph.Border [in MetaCoq.Template.utils.wGraph]

WeightedGraph.IsFullSubgraph.LspBoundExtendBorder [in MetaCoq.Template.utils.wGraph]

WeightedGraph.MapSPath [in MetaCoq.Template.utils.wGraph]

WeightedGraph.RelabelOn [in MetaCoq.Template.utils.wGraph]

WeightedGraph.RelabelWrtEdge.RelabelWrtEdge [in MetaCoq.Template.utils.wGraph]

WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling [in MetaCoq.Template.utils.wGraph]

WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs [in MetaCoq.Template.utils.wGraph]

WeightedGraph.subgraph [in MetaCoq.Template.utils.wGraph]

WeightedGraph.subgraph.subgraph2 [in MetaCoq.Template.utils.wGraph]

WeightedGraph.Subgraph1.graph2 [in MetaCoq.Template.utils.wGraph]

wellscoped [in MetaCoq.Erasure.ErasureProperties]

wellscoped.Def [in MetaCoq.Erasure.ErasureProperties]

wf [in MetaCoq.Erasure.EWellformed]

WfAst [in MetaCoq.Template.TypingWf]

WfEnv [in MetaCoq.SafeChecker.PCUICWfEnvImpl]

WfEnv [in MetaCoq.PCUIC.PCUICProgress]

WfEnv [in MetaCoq.PCUIC.PCUICArities]

WfEnv [in MetaCoq.PCUIC.PCUICContexts]

WfEnv [in MetaCoq.PCUIC.PCUICSpine]

WfEnv [in MetaCoq.PCUIC.PCUICSpine]

wffix [in MetaCoq.Erasure.ErasureFunction]

WfLookup [in MetaCoq.Template.TypingWf]

WfRed [in MetaCoq.Template.TypingWf]

whne_red1_ind [in MetaCoq.PCUIC.PCUICNormal]

WtContextConversion [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]

wtcumul [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]

wtcumul [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]

wtcumul' [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]

wtsub [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]

wtsub [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]

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) |