| 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 | (19204 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 | (228 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 | (298 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 | (1273 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 | (313 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 | (8163 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 | (1514 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 | (52 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 | (352 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 | (534 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 | (727 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 | (402 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 | (333 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 | (4833 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 | (182 entries) |
W (lemma)
wat_welltyped [in MetaRocq.PCUIC.PCUICSafeLemmata]wcbveval_red [in MetaRocq.PCUIC.PCUICClassification]
wcbv_standardization_fst [in MetaRocq.PCUIC.PCUICNormalization]
wcbv_standardization [in MetaRocq.PCUIC.PCUICNormalization]
wcbv_normalization [in MetaRocq.PCUIC.PCUICNormalization]
wcbv_red1_mkApps_left [in MetaRocq.PCUIC.PCUICProgress]
wcbv_red1_eval [in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_red1 [in MetaRocq.PCUIC.PCUICWcbvEval]
wcbv_red1_closed [in MetaRocq.PCUIC.PCUICWcbvEval]
wcored_wf [in MetaRocq.SafeChecker.PCUICSafeConversion]
weakening [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_env_normalization_in [in MetaRocq.PCUIC.PCUICWeakeningEnvSN]
weakening_closed_red1 [in MetaRocq.PCUIC.PCUICSR]
weakening_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICSR]
weakening_gen [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_length [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_typing [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_rename_typing [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local_eq [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_closed_red [in MetaRocq.PCUIC.PCUICSpine]
weakening_env_cumul_ctx [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_ctx [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_decls [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_decls [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_convSpec [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec0 [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_gen [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_red1 [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_config_normalization_in [in MetaRocq.PCUIC.PCUICWeakeningConfigSN]
weakening_env_cored [in MetaRocq.PCUIC.PCUICSafeLemmata]
weakening_env_declared_projection [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constructor [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_inductive [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_minductive [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constant [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_consistent_instance [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_is_allowed_elimination [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_constraints [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels' [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weakening_cumulSpec0 [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
weakening_cumul0 [in MetaRocq.PCUIC.PCUICContextConversion]
weakening_is_closed_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
weakening_env_declared_constructor [in MetaRocq.Erasure.EExtends]
weakening_env_declared_inductive [in MetaRocq.Erasure.EExtends]
weakening_env_declared_minductive [in MetaRocq.Erasure.EExtends]
weakening_env_declared_constant [in MetaRocq.Erasure.EExtends]
weakening_ws_cumul_pb_eq [in MetaRocq.PCUIC.PCUICConversion]
weakening_ws_cumul_pb [in MetaRocq.PCUIC.PCUICConversion]
weakening_config_wf [in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config [in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config_wf_local_sized [in MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp]
weakening_config_consistent_instance [in MetaRocq.PCUIC.PCUICWeakeningConfig]
weakening_config_is_allowed_elimination [in MetaRocq.PCUIC.PCUICWeakeningConfig]
weakening_pred1_0 [in MetaRocq.PCUIC.PCUICParallelReduction]
weakening_pred1_pred1 [in MetaRocq.PCUIC.PCUICParallelReduction]
weakening_pred1 [in MetaRocq.PCUIC.PCUICParallelReduction]
weakening_eval_env [in MetaRocq.Erasure.EWcbvEval]
weakening_conv_wt [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_conv [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_cumul [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red_0 [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red' [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red1 [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_renaming [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_config_cumul_ctx [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_conv_ctx [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumul_decls [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_conv_decls [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumulSpec [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_convSpec [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumulSpec0 [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumul [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_conv [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_config_cumul_gen [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
weakening_type_local_ctx [in MetaRocq.PCUIC.PCUICCasesHelper]
weakening_env_strictly_on_decls_lookup_on_global_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_strictly_decls_lookup_on_global_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_decls_lookup_on_global_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_lookup_on_global_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_gen_lookup_on_global_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_strictly_ext [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_strictly [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_ext [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_gen [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening0 [in MetaRocq.PCUIC.PCUICCasesHelper]
weaken_env_prop_closed [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
weaken_ctx [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_subslet [in MetaRocq.PCUIC.PCUICSpine]
weaken_lookup_on_global_env' [in MetaRocq.PCUIC.PCUICWeakeningEnv]
weaken_prefix [in MetaRocq.Erasure.ErasureFunctionProperties]
weaken_prop [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
weaken_prop_gen [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
weaken_wf_subslet [in MetaRocq.PCUIC.PCUICInductiveInversion]
weaken_ws_cumul_ctx_pb_rel [in MetaRocq.PCUIC.PCUICConversion]
weaken_ws_cumul_pb [in MetaRocq.PCUIC.PCUICConversion]
weaken_subslet [in MetaRocq.PCUIC.PCUICArities]
weaken_sorts_local_ctx [in MetaRocq.PCUIC.PCUICContexts]
weaken_type_local_ctx [in MetaRocq.PCUIC.PCUICContexts]
weaken_nth_error_lt [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_nth_error_ge [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_wf_universes [in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_instance [in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_level [in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_universe [in MetaRocq.PCUIC.PCUICWfUniverses]
weaken_wf_decl_pred [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
weaken_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_env_prop_typing [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_decls_lookup_on_global_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_lookup_on_global_env [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
WeightedGraph.acyclic_relabel_on [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop_sloop [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_relabel [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_caract2 [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_caract1 [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_lsp0_xx [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_labelling [in MetaRocq.Utils.wGraph]
WeightedGraph.acyclic_no_loop_loop' [in MetaRocq.Utils.wGraph]
WeightedGraph.Add_Add [in MetaRocq.Utils.wGraph]
WeightedGraph.Add_In [in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling_lsp_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling_lsp [in MetaRocq.Utils.wGraph]
WeightedGraph.correct_labelling_PathOf [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_In [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add4 [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove_inv [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_Equal_l [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_Equal [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove_add [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove1 [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_union [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_Subset [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_remove [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add3 [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add2 [in MetaRocq.Utils.wGraph]
WeightedGraph.DisjointAdd_add1 [in MetaRocq.Utils.wGraph]
WeightedGraph.Disjoint_DisjointAdd [in MetaRocq.Utils.wGraph]
WeightedGraph.edge_map_spec2 [in MetaRocq.Utils.wGraph]
WeightedGraph.edge_map_spec1 [in MetaRocq.Utils.wGraph]
WeightedGraph.extends_correct_labelling [in MetaRocq.Utils.wGraph]
WeightedGraph.extends_labelling [in MetaRocq.Utils.wGraph]
WeightedGraph.first_in_first [in MetaRocq.Utils.wGraph]
WeightedGraph.first_in_in [in MetaRocq.Utils.wGraph]
WeightedGraph.fold_left_equiv [in MetaRocq.Utils.wGraph]
WeightedGraph.fold_left_filter [in MetaRocq.Utils.wGraph]
WeightedGraph.fold_left_map [in MetaRocq.Utils.wGraph]
WeightedGraph.from_G'_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.from_G'_path_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.invariants_relabel [in MetaRocq.Utils.wGraph]
WeightedGraph.In_nodes_app_end [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.add_from_orig_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.border_set_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.EdgeSet_fold_spec_right2 [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.fold_fun_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_subgraph_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_lsp_dominate [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_eq_is_full_extension [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_bound_extend_border [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.spath_on_border [in MetaRocq.Utils.wGraph]
WeightedGraph.IsFullSubgraph.sweight_bound0 [in MetaRocq.Utils.wGraph]
WeightedGraph.is_acyclic_correct [in MetaRocq.Utils.wGraph]
WeightedGraph.is_acyclic_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.is_nonpos_nbar [in MetaRocq.Utils.wGraph]
WeightedGraph.is_nonpos_spec [in MetaRocq.Utils.wGraph]
WeightedGraph.labelling_ext_lsp [in MetaRocq.Utils.wGraph]
WeightedGraph.leqb_vertices_correct [in MetaRocq.Utils.wGraph]
WeightedGraph.leq_vertices_caract [in MetaRocq.Utils.wGraph]
WeightedGraph.leq_vertices_caract0 [in MetaRocq.Utils.wGraph]
WeightedGraph.le_Some_lsp [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_Gl_between_G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_Gl_upperbound_G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_edge [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_vset_in [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_spec_left [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_incr [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_sx [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_G'_yx [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_pathOf [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_source_max [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_to_source [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_from_source [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_xx [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_xx_acyclic [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_to_s [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_sym [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_codistance [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_correctness [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_s [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp_optim [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_triangle_inequality [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_spec_eq0 [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_spec_eq [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_spec_le [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_VSet_Equal [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp0_eq [in MetaRocq.Utils.wGraph]
WeightedGraph.lsp00_optim [in MetaRocq.Utils.wGraph]
WeightedGraph.negbe [in MetaRocq.Utils.wGraph]
WeightedGraph.nodes_subset [in MetaRocq.Utils.wGraph]
WeightedGraph.pathOf_add_end_simpl [in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_add_end_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.PathOf_In [in MetaRocq.Utils.wGraph]
WeightedGraph.reflect_logically_equiv [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.dxy_bound [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_diff [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_y [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_x [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_correct [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.r_correct [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_mon [in MetaRocq.Utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_add [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_correct_labelling [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_invariants [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_lsp_G2 [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_on_lsp_G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_lsp [in MetaRocq.Utils.wGraph]
WeightedGraph.relabel_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath [in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux3 [in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux2 [in MetaRocq.Utils.wGraph]
WeightedGraph.reroot_spath_aux1 [in MetaRocq.Utils.wGraph]
WeightedGraph.simplify_aux3 [in MetaRocq.Utils.wGraph]
WeightedGraph.simplify_aux2 [in MetaRocq.Utils.wGraph]
WeightedGraph.simplify_aux1 [in MetaRocq.Utils.wGraph]
WeightedGraph.source_bottom [in MetaRocq.Utils.wGraph]
WeightedGraph.spathG1_lsp_Gl [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_sets [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_In' [in MetaRocq.Utils.wGraph]
WeightedGraph.SPath_In [in MetaRocq.Utils.wGraph]
WeightedGraph.sto_G'_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.subgraph_acyclic [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.correct_labelling_lsp_G' [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G'_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.from_G'_path_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_spec_left [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_sx [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_incr [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_yx [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.lsp_pathOf [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.sto_G'_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.Subgraph1.to_G'_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_relabel_on_G2 [in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_relabel_on_G1 [in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_inverse [in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_sconcat [in MetaRocq.Utils.wGraph]
WeightedGraph.sweight_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.to_label_to_nat [in MetaRocq.Utils.wGraph]
WeightedGraph.to_G'_weight [in MetaRocq.Utils.wGraph]
WeightedGraph.to_label_max [in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_Forall_reflect [in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_add_add_same [in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_add_add [in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_remove_add [in MetaRocq.Utils.wGraph]
WeightedGraph.VSet_add_remove [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_from2 [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_from1 [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_inverse [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_simplify2' [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_simplify2 [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_reduce [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_simplify [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_split' [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_split [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_add_end [in MetaRocq.Utils.wGraph]
WeightedGraph.weight_concat [in MetaRocq.Utils.wGraph]
WeightedGraph.Zle_opp' [in MetaRocq.Utils.wGraph]
WeightedGraph.Zle_opp [in MetaRocq.Utils.wGraph]
WeightedGraph.Z_of_to_label_pos [in MetaRocq.Utils.wGraph]
WeightedGraph.Z_of_to_label_s [in MetaRocq.Utils.wGraph]
WeightedGraph.Z_of_to_label [in MetaRocq.Utils.wGraph]
wellformed_lookup_constructor_pars_args [in MetaRocq.Erasure.EImplementBox]
wellformed_lookup_constructor_pars [in MetaRocq.Erasure.EImplementBox]
wellformed_lookup_inductive_pars [in MetaRocq.Erasure.EImplementBox]
wellformed_gen_transform_decl_extends [in MetaRocq.Erasure.EGenericGlobalMap]
wellformed_remove_match_on_box_decl_extends [in MetaRocq.Erasure.EOptimizePropDiscr]
wellformed_remove_match_on_box_extends [in MetaRocq.Erasure.EOptimizePropDiscr]
wellformed_gen_transform_decl_extends [in MetaRocq.Erasure.EGenericMapEnv]
wellformed_lookup_constructor_pars_args [in MetaRocq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_constructor_pars [in MetaRocq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_inductive_pars [in MetaRocq.Erasure.EConstructorsAsBlocks]
wellformed_annotate [in MetaRocq.Erasure.EWcbvEvalNamed]
wellformed_annotate' [in MetaRocq.Erasure.EWcbvEvalNamed]
wellformed_closed_env [in MetaRocq.Erasure.EWellformed]
wellformed_mkApps [in MetaRocq.Erasure.EWellformed]
wellformed_iota_red_brs [in MetaRocq.Erasure.EWellformed]
wellformed_iota_red [in MetaRocq.Erasure.EWellformed]
wellformed_cunfold_cofix [in MetaRocq.Erasure.EWellformed]
wellformed_cunfold_fix [in MetaRocq.Erasure.EWellformed]
wellformed_cofix_subst [in MetaRocq.Erasure.EWellformed]
wellformed_fix_subst [in MetaRocq.Erasure.EWellformed]
wellformed_substl [in MetaRocq.Erasure.EWellformed]
wellformed_csubst [in MetaRocq.Erasure.EWellformed]
wellformed_subst [in MetaRocq.Erasure.EWellformed]
wellformed_subst_eq [in MetaRocq.Erasure.EWellformed]
wellformed_lift [in MetaRocq.Erasure.EWellformed]
wellformed_up [in MetaRocq.Erasure.EWellformed]
wellformed_closed_decl [in MetaRocq.Erasure.EWellformed]
wellformed_closed [in MetaRocq.Erasure.EWellformed]
wellformed_optimize_decl_extends [in MetaRocq.Erasure.EInlineProjections]
wellformed_optimize_extends [in MetaRocq.Erasure.EInlineProjections]
wellformed_projection_args [in MetaRocq.Erasure.EInlineProjections]
wellformed_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_case_branch_body_rec [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_lambdas [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_dearg_single [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wellformed_trans_decl_extends [in MetaRocq.Erasure.ECoInductiveToInductive]
wellformed_trans_extends [in MetaRocq.Erasure.ECoInductiveToInductive]
welltyped_R_pres [in MetaRocq.SafeChecker.PCUICSafeReduce]
welltyped_is_open_term [in MetaRocq.SafeChecker.PCUICSafeReduce]
welltyped_is_closed_context [in MetaRocq.SafeChecker.PCUICSafeReduce]
welltyped_brs [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_zipp [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_stack_context [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_zipx [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn_iff [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_context [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_fill_context_hole [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_alpha [in MetaRocq.PCUIC.PCUICSafeLemmata]
welltyped_wellformed [in MetaRocq.Erasure.ErasureProperties]
welltyped_subterm [in MetaRocq.SafeChecker.PCUICSafeRetyping]
welltyped_mkApps_inv [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
welltyped_mkApps_inv [in MetaRocq.Erasure.ErasureFunctionProperties]
welltyped_letin_red [in MetaRocq.SafeChecker.PCUICSafeChecker]
welltyped_letin_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
welltyped_prod_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
welltyped_R_zipc [in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_wf [in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipp_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tProd_appstack_nil [in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tCase_brs_length [in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tConst_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
welltyped_wf_local [in MetaRocq.SafeChecker.PCUICSafeConversion]
well_founded_erase_rel [in MetaRocq.Erasure.Typed.Erasure]
well_founded_term_sub_ctx [in MetaRocq.Erasure.Typed.Erasure]
well_prop_wf [in MetaRocq.Examples.tauto]
well_sorted_wellinferred [in MetaRocq.SafeChecker.PCUICSafeRetyping]
well_subst_app_up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_app [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up' [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
well_subst_ext [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
WfArity_build_case_predicate_type [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_fresh_globals [in MetaRocq.Template.TemplateEnvMap]
wf_pop_decl [in MetaRocq.Erasure.Typed.Erasure]
wf_local_subst1 [in MetaRocq.PCUIC.PCUICSR]
wf_local_red [in MetaRocq.PCUIC.PCUICSR]
wf_local_red1 [in MetaRocq.PCUIC.PCUICSR]
wf_local_isType_nth [in MetaRocq.PCUIC.PCUICSR]
wf_subslet_skipn [in MetaRocq.PCUIC.PCUICSR]
wf_pre_case_branch_context [in MetaRocq.PCUIC.PCUICSR]
wf_cofixpoint_red1_body [in MetaRocq.PCUIC.PCUICSR]
wf_cofixpoint_red1_type [in MetaRocq.PCUIC.PCUICSR]
wf_fixpoint_red1_body [in MetaRocq.PCUIC.PCUICSR]
wf_fixpoint_red1_type [in MetaRocq.PCUIC.PCUICSR]
wf_arities_context [in MetaRocq.PCUIC.PCUICSubstitution]
wf_arities_context' [in MetaRocq.PCUIC.PCUICSubstitution]
wf_ext_wf [in MetaRocq.PCUIC.PCUICElimination]
wf_local_nth_isType [in MetaRocq.PCUIC.PCUICSpine]
wf_arity_spine_typing_spine [in MetaRocq.PCUIC.PCUICSpine]
wf_local_alpha [in MetaRocq.PCUIC.PCUICSpine]
wf_cod' [in MetaRocq.Erasure.ErasureFunction]
wf_cod [in MetaRocq.Erasure.ErasureFunction]
wf_global_decl_deps [in MetaRocq.Erasure.ErasureFunction]
wf_local_rel_alpha_eq_end [in MetaRocq.Erasure.ErasureFunction]
wf_fun [in MetaRocq.PCUIC.PCUICSafeLemmata]
wf_case_inst_case_context [in MetaRocq.PCUIC.PCUICSafeLemmata]
wf_inst_case_context [in MetaRocq.PCUIC.PCUICSafeLemmata]
wf_local_All_fold [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wf_local_inv [in MetaRocq.PCUIC.PCUICTyping]
wf_local_app_l [in MetaRocq.PCUIC.PCUICTyping]
wf_ext_consistent [in MetaRocq.PCUIC.PCUICTyping]
wf_ext_wf [in MetaRocq.PCUIC.PCUICTyping]
wf_env_non_var_levels [in MetaRocq.PCUIC.PCUICTyping]
wf_ext_gc_of_uctx_irr [in MetaRocq.SafeChecker.PCUICEqualityDec]
wf_ext_gc_of_uctx [in MetaRocq.SafeChecker.PCUICEqualityDec]
wf_gc_of_uctx [in MetaRocq.SafeChecker.PCUICEqualityDec]
wf_local_rel_conv [in MetaRocq.Erasure.ErasureProperties]
wf_local_app_renaming [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
wf_consistent [in MetaRocq.PCUIC.PCUICGlobalEnv]
wf_cumul_context_closed [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
wf_conv_context_closed [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
wf_dlexprod [in MetaRocq.PCUIC.utils.PCUICUtils]
wf_local_validity [in MetaRocq.PCUIC.PCUICValidity]
wf_pre_case_predicate_context_gen [in MetaRocq.PCUIC.PCUICValidity]
wf_lookup [in MetaRocq.Erasure.ErasureFunctionProperties]
wf_fresh_globals [in MetaRocq.Erasure.ErasureFunctionProperties]
wf_fixpoint_rarg [in MetaRocq.Template.EtaExpand]
wf_cons_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_ind_indices [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_local_ind_params_weaken [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wf_mkApps [in MetaRocq.Erasure.EGenericGlobalMap]
wf_local_bd_rel_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_bd_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_local_rel [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_rel_weak [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_rel_subst1 [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_subst_instance_decl [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate_poly [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_case_branches_types' [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_branches_types [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type' [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_pre_case_branch_context_gen [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_case_predicate_context [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_set_binder_name [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_local_vass [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_typing_spine [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_all [in MetaRocq.PCUIC.PCUICInductiveInversion]
wf_cunfold_cofix [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_cunfold_fix [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_cofix_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_fix_subst [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_substl [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_csubst [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
wf_nth [in MetaRocq.Template.WfAst]
wf_subst_instance [in MetaRocq.Template.WfAst]
wf_mkApps_inv [in MetaRocq.Template.WfAst]
wf_mkApps_napp [in MetaRocq.Template.WfAst]
wf_strip_outer_cast [in MetaRocq.Template.WfAst]
wf_subst1 [in MetaRocq.Template.WfAst]
wf_subst [in MetaRocq.Template.WfAst]
wf_lift [in MetaRocq.Template.WfAst]
wf_mkApps [in MetaRocq.Template.WfAst]
wf_mkApp [in MetaRocq.Template.WfAst]
wf_inv [in MetaRocq.Template.WfAst]
wf_local_def [in MetaRocq.PCUIC.PCUICArities]
wf_local_ass [in MetaRocq.PCUIC.PCUICArities]
wf_local_alpha [in MetaRocq.PCUIC.PCUICAlpha]
wf_local_eq_context_upto_names [in MetaRocq.PCUIC.PCUICAlpha]
wf_local_nth_error_vass [in MetaRocq.PCUIC.PCUICAlpha]
wf_glob_lookup_inductive_pars [in MetaRocq.ErasurePlugin.ErasureCorrectness]
wf_glob_fresh [in MetaRocq.Erasure.EProgram]
wf_local_smash_context [in MetaRocq.PCUIC.PCUICContexts]
wf_local_rel_empty [in MetaRocq.PCUIC.PCUICContexts]
wf_local_smash_end [in MetaRocq.PCUIC.PCUICContexts]
wf_local_rel_smash_context [in MetaRocq.PCUIC.PCUICContexts]
wf_local_rel_smash_context_gen [in MetaRocq.PCUIC.PCUICContexts]
wf_erase_global_decls_recursive [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_erase_global_decl [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_trans_inductives [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_squash [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
wf_ctx_universes_app [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_local_wf_ctx_universes [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_ctx_universes_subst_instance [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_decl_universes_subst_instance [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_ind_types_wf_arities [in MetaRocq.SafeChecker.PCUICSafeChecker]
wf_mkApps [in MetaRocq.Erasure.EGenericMapEnv]
wf_inductive_mapping_inv [in MetaRocq.Erasure.EReorderCstrs]
wf_mkApps [in MetaRocq.Erasure.EReorderCstrs]
wf_optimize [in MetaRocq.Erasure.EReorderCstrs]
wf_ind_mapping_wf_brs [in MetaRocq.Erasure.EReorderCstrs]
wf_glob_ind_projs [in MetaRocq.Erasure.EReorderCstrs]
wf_local_inv [in MetaRocq.Template.Typing]
wf_local_app_l [in MetaRocq.Template.Typing]
wf_inductive_mapping_trans [in MetaRocq.ErasurePlugin.Erasure]
wf_local_rel_wf_local_bd [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
wf_local_wf_local_bd [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
wf_ind_predicate [in MetaRocq.PCUIC.PCUICInductives]
wf_local_expand_lets [in MetaRocq.PCUIC.PCUICInductives]
wf_projection_context [in MetaRocq.PCUIC.PCUICInductives]
wf_projection_arg_ctx [in MetaRocq.PCUIC.PCUICInductives]
wf_projection_context_gen [in MetaRocq.PCUIC.PCUICInductives]
wf_subslet_dom [in MetaRocq.PCUIC.PCUICInductives]
wf_arities_context_inst [in MetaRocq.PCUIC.PCUICInductives]
wf_precompose [in MetaRocq.Utils.MRRelations]
wf_consistent_extension_on_consistent [in MetaRocq.SafeChecker.PCUICWfEnv]
wf_fix_env [in MetaRocq.Erasure.EWcbvEvalNamed]
wf_add_multiple [in MetaRocq.Erasure.EWcbvEvalNamed]
wf_fix_inv [in MetaRocq.Erasure.EWellformed]
wf_it_mkLambda_or_LetIn [in MetaRocq.Template.TypingWf]
wf_Lambda_or_LetIn [in MetaRocq.Template.TypingWf]
wf_it_mkProd_or_LetIn_inv [in MetaRocq.Template.TypingWf]
wf_lift_wf [in MetaRocq.Template.TypingWf]
wf_red1 [in MetaRocq.Template.TypingWf]
wf_projs [in MetaRocq.Template.TypingWf]
wf_case_branches_context [in MetaRocq.Template.TypingWf]
wf_case_branch_context_gen [in MetaRocq.Template.TypingWf]
wf_inds [in MetaRocq.Template.TypingWf]
wf_case_predicate_context [in MetaRocq.Template.TypingWf]
wf_extended_subst [in MetaRocq.Template.TypingWf]
wf_subst_instance_context [in MetaRocq.Template.TypingWf]
wf_lift_context [in MetaRocq.Template.TypingWf]
wf_map2_set_binder_name [in MetaRocq.Template.TypingWf]
wf_reln [in MetaRocq.Template.TypingWf]
wf_smash_context [in MetaRocq.Template.TypingWf]
wf_subst_context [in MetaRocq.Template.TypingWf]
wf_it_mkProd_or_LetIn [in MetaRocq.Template.TypingWf]
wf_decl_extends [in MetaRocq.Template.TypingWf]
wf_extends [in MetaRocq.Template.TypingWf]
wf_mkApps [in MetaRocq.Erasure.EInlineProjections]
wf_optimize [in MetaRocq.Erasure.EInlineProjections]
wf_cofixpoint_spine [in MetaRocq.PCUIC.PCUICClassification]
wf_fixpoint_spine [in MetaRocq.PCUIC.PCUICClassification]
wf_cofixpoint_inv [in MetaRocq.PCUIC.PCUICClassification]
wf_fixpoint_inv [in MetaRocq.PCUIC.PCUICClassification]
wf_sort_super [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_sort_type1 [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_sort_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_universe_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_ext_wk_wf [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_glob_debox [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wf_glob_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
wf_branch_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pcontext [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pars [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branchesP [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_branchP [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_predicateP [in MetaRocq.PCUIC.Syntax.PCUICCases]
wf_types [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_ctx_universes_closed [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_closedu [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_make [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_closed [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_closed [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_closed [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level_closed [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_extended_subst [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_projs [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_abstract_instance [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_local_ctx_nth_error [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_local_ctx_smash [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_mkApps [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_inds [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_weaken [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_weaken_full [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_inst [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_subst [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universes_lift [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universeb_instance_forall [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_reflect [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_reflect [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_subst_instance [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_In [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instance_sub [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level_sub [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_level_mono [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_instantiate [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_subst_instance_sort [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_universe_subst_instance_univ [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_instanceP [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_levelP [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_product [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_sup [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_super [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_type1 [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_sort_type0 [in MetaRocq.PCUIC.PCUICWfUniverses]
wf_local_app_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
wf_ind_arities [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_expand_lets_ctx [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_expand_lets [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_it_mkProd_or_LetIn [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_wf_decl_pred [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_fresh_globals [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
wf_local_closed_context [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
wf_context_sorts [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
wf_cons_inv [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
wf_local_expand_lets0 [in MetaRocq.PCUIC.PCUICCasesHelper]
wf_env_fresh [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_fresh_globals [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wf_env_eta [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
wfΣ [in MetaRocq.Erasure.Typed.TypeAnnotations]
whne_eq_term_upto_univ_napp [in MetaRocq.PCUIC.PCUICNormal]
whne_red1_inv [in MetaRocq.PCUIC.PCUICNormal]
whne_pres [in MetaRocq.PCUIC.PCUICNormal]
whne_pres1 [in MetaRocq.PCUIC.PCUICNormal]
whne_red1_ind [in MetaRocq.PCUIC.PCUICNormal]
whne_isConstruct_app [in MetaRocq.PCUIC.PCUICNormal]
whne_mkApps_inv [in MetaRocq.PCUIC.PCUICNormal]
whne_mkApps [in MetaRocq.PCUIC.PCUICNormal]
whne_conv_context [in MetaRocq.PCUIC.PCUICSafeLemmata]
whne_All2_fold [in MetaRocq.PCUIC.PCUICSafeLemmata]
whnf_eq_term [in MetaRocq.PCUIC.PCUICNormal]
whnf_eq_term_upto_univ_napp [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_isApp [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_red1_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_trans [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_refl [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_refl_whne [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps_r_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps_l_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_mkApps [in MetaRocq.PCUIC.PCUICNormal]
whnf_red_red [in MetaRocq.PCUIC.PCUICNormal]
whnf_pres [in MetaRocq.PCUIC.PCUICNormal]
whnf_pres1 [in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_tLambda_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_tProd_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_tSort_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_whne_nodelta_upgrade [in MetaRocq.PCUIC.PCUICNormal]
whnf_fixapp' [in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps_inv [in MetaRocq.PCUIC.PCUICNormal]
whnf_mkApps [in MetaRocq.PCUIC.PCUICNormal]
whnf_proj_arg_whne [in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_case_arg_whne [in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_fix_arg_whne [in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_non_cofix_ind_typed [in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_finite_ind_typed [in MetaRocq.SafeChecker.PCUICSafeReduce]
whnf_conv_context [in MetaRocq.PCUIC.PCUICSafeLemmata]
whnf_All2_fold [in MetaRocq.PCUIC.PCUICSafeLemmata]
whnf_progress [in MetaRocq.PCUIC.PCUICProgress]
whnf_classification [in MetaRocq.PCUIC.PCUICClassification]
whnf_classification' [in MetaRocq.PCUIC.PCUICClassification]
whnf_red_isIndConstructApp [in MetaRocq.PCUIC.PCUICConvCumInversion]
whnf_mkApps_tPrim_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
wh_normalization [in MetaRocq.PCUIC.PCUICNormalization]
wh_neutral_empty [in MetaRocq.PCUIC.PCUICClassification]
wh_neutral_empty_gen [in MetaRocq.PCUIC.PCUICClassification]
WithTemplate.PrefixUniverse.LevelExprSet.is_empty_prefix_with [in MetaRocq.Quotation.CommonUtils]
WithTemplate.PrefixUniverse.LevelExprSet.prefix_with_Ok [in MetaRocq.Quotation.CommonUtils]
ws_wcbv_standardization_fst [in MetaRocq.PCUIC.PCUICNormalization]
ws_wcbv_standardization [in MetaRocq.PCUIC.PCUICNormalization]
ws_cumul_pb_terms_refl [in MetaRocq.PCUIC.PCUICSR]
ws_cumul_pb_terms_eq_trans [in MetaRocq.PCUIC.PCUICSR]
ws_cumul_pb_eq_trans [in MetaRocq.PCUIC.PCUICSR]
ws_cumul_pb_meta_refl [in MetaRocq.PCUIC.PCUICSR]
ws_cumul_ctx_pb_rel_trans [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_ws_cumul_ctx [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_length [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_ws_cumul_ctx [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_smash [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_conv_extended_subst [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_eq_le [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_le_le [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_le_le [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_lift [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_k [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_context_assumptions [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel'_context_assumptions [in MetaRocq.PCUIC.PCUICSpine]
ws_cumul_pb_zippx [in MetaRocq.PCUIC.PCUICSafeLemmata]
ws_cumul_ctx_pb_refl [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_forget [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_inv [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_left [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_right [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_inv [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_cumul_pb_decls [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_right [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_left [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt_closed [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_conv [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_cumul [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_right [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_left [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_closed_context [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl' [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_app_same [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_refl [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_true_forget [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_false_forget [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_decls_ws_cumul_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx_inv [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_le [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_red [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx_inv [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_context_upto [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context_inv [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red [in MetaRocq.PCUIC.PCUICContextConversion]
ws_red_confluence [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_pred [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_curry_red [in MetaRocq.PCUIC.PCUICConfluence]
ws_red_refl_irrel [in MetaRocq.PCUIC.PCUICConfluence]
ws_red_irrel [in MetaRocq.PCUIC.PCUICConfluence]
ws_red_red_ctx [in MetaRocq.PCUIC.PCUICConfluence]
ws_red_red_ctx_aux [in MetaRocq.PCUIC.PCUICConfluence]
ws_red_red [in MetaRocq.PCUIC.PCUICConfluence]
ws_red_ctx_length [in MetaRocq.PCUIC.PCUICConfluence]
ws_term_eq [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_diamond [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred1_red [in MetaRocq.PCUIC.PCUICConfluence]
ws_pred_ws_pred_curry [in MetaRocq.PCUIC.PCUICConfluence]
ws_red1_pred1 [in MetaRocq.PCUIC.PCUICConfluence]
ws_red1_pred1_curry [in MetaRocq.PCUIC.PCUICConfluence]
ws_context_on_free_vars_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
ws_context_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
ws_term_xpredT [in MetaRocq.PCUIC.PCUICConfluence]
ws_cumul_pb_it_mkProd_or_LetIn_smash [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_pb_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_ctx_pb_wf_local [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_inst_variance [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_Prod_Prod_inv_l [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_subst [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_inv [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_eq [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_terms_confl [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_tRel [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_ctx_pb_rel_context_assumptions [in MetaRocq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_Prim [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Construct [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Evar [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_subst [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_weaken [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_conv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_ws_cumul_ctx [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_alt [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_rel_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_rel_app [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_elim [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_substs_red [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_ty [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_tm [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps_weak [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn_codom [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn_codom [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_bo [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_r [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_l [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_eq_le_gen [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_CoFix [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Fix [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_or_cofix [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_bodies [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_body [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_types [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_type [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_brs [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_one_brs [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_c [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_p [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_App [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Proj_c [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_App_r [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_App_l [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Axiom_r_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Axiom_l_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_r_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_right [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_left [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_l_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_r_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_l_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_red_l_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_red_r_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Prod_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_r_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_r_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_l_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Sort_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_Prod_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_inv [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l [in MetaRocq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_app [in MetaRocq.PCUIC.PCUICArities]
ws_cumul_ctx_pb_vass [in MetaRocq.PCUIC.PCUICArities]
ws_cumul_pb_LetIn_l_inv_alt [in MetaRocq.PCUIC.PCUICCumulProp]
ws_cumul_ctx_pb_rel_cons [in MetaRocq.SafeChecker.PCUICTypeChecker]
wt_template_program_fresh [in MetaRocq.Template.TemplateProgram]
wt_closed_red1 [in MetaRocq.PCUIC.PCUICSR]
wt_terms_ws_cumul_pb [in MetaRocq.PCUIC.PCUICSR]
wt_cumul_pb_refl [in MetaRocq.PCUIC.PCUICSR]
wt_cumul_pb_equalityP [in MetaRocq.PCUIC.PCUICSubstitution]
wt_ws_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_ctx_pb_forget [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_trans [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_ws_cumul_pb [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
wt_cum_ws_cumul_ctx_pb [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
wt_cum_ws_cumul_pb [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
wt_closed [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_subst_instance [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_convSpec_convAlgo [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_wt [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_mkApps_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_on_free_vars [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_red [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_wf_local [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
wt_ind_app_variance [in MetaRocq.PCUIC.PCUICInductiveInversion]
wt_cstrs [in MetaRocq.SafeChecker.PCUICSafeChecker]
wt_closed_red_refl [in MetaRocq.PCUIC.PCUICClassification]
wt_zip_mkapps [in MetaRocq.SafeChecker.PCUICSafeConversion]
wt_inv [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
| 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 | (19204 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 | (228 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 | (298 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 | (1273 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 | (313 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 | (8163 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 | (1514 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 | (52 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 | (352 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 | (534 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 | (727 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 | (402 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 | (333 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 | (4833 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 | (182 entries) |