| 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 (lemma)
wat_welltyped [in MetaCoq.PCUIC.PCUICSafeLemmata]wcbeval_red [in MetaCoq.PCUIC.PCUICCanonicity]
wcbv_standardization [in MetaCoq.PCUIC.PCUICProgress]
wcored_wf [in MetaCoq.SafeChecker.PCUICSafeConversion]
weakening [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_env_declared_projection [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constructor [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_inductive [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_minductive [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constant [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_consistent_instance [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_is_allowed_elimination [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_constraints [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels' [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_cumul_ctx [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_ctx [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_decls [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_decls [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_convSpec [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec0 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_gen [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_red1 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_pred1_0 [in MetaCoq.PCUIC.PCUICParallelReduction]
weakening_pred1_pred1 [in MetaCoq.PCUIC.PCUICParallelReduction]
weakening_pred1 [in MetaCoq.PCUIC.PCUICParallelReduction]
weakening_conv_wt [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_conv [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_cumul [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red_0 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red' [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red1 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_renaming [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_is_closed_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
weakening_cumulSpec0 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
weakening_gen [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_length [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_typing [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_rename_typing [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local_eq [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_ws_cumul_pb_eq [in MetaCoq.PCUIC.PCUICConversion]
weakening_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
weakening_cumul0 [in MetaCoq.PCUIC.PCUICContextConversion]
weakening_env_declared_constructor [in MetaCoq.Erasure.EExtends]
weakening_env_declared_inductive [in MetaCoq.Erasure.EExtends]
weakening_env_declared_minductive [in MetaCoq.Erasure.EExtends]
weakening_env_declared_constant [in MetaCoq.Erasure.EExtends]
weakening_closed_red1 [in MetaCoq.PCUIC.PCUICSR]
weakening_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICSR]
weakening_eval_env [in MetaCoq.Erasure.EWcbvEval]
weakening_env_lookup_on_global_env [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_decls_lookup_on_global_env [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_ext [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_closed_red [in MetaCoq.PCUIC.PCUICSpine]
weaken_lookup_on_global_env' [in MetaCoq.PCUIC.PCUICWeakeningEnv]
weaken_subslet [in MetaCoq.PCUIC.PCUICArities]
weaken_wf_universes [in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_universe_instance [in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_universe_level [in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_universe [in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_decl_pred [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
weaken_env_prop_isType [in MetaCoq.PCUIC.PCUICValidity]
weaken_wf_subslet [in MetaCoq.PCUIC.PCUICInductiveInversion]
weaken_nth_error_lt [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_nth_error_ge [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_prop [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
weaken_prefix [in MetaCoq.Erasure.ErasureFunction]
weaken_ctx [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_wf_local [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_ws_cumul_ctx_pb_rel [in MetaCoq.PCUIC.PCUICConversion]
weaken_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
weaken_env_prop_closed [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
weaken_sorts_local_ctx [in MetaCoq.PCUIC.PCUICContexts]
weaken_type_local_ctx [in MetaCoq.PCUIC.PCUICContexts]
weaken_wf_local [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_env_decls_prop_typing [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_env_prop_typing [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_decls_lookup_on_global_env [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_lookup_on_global_env [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_subslet [in MetaCoq.PCUIC.PCUICSpine]
WeightedGraph.acyclic_relabel_on [in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_loop_sloop [in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_relabel [in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_caract2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_caract1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_lsp0_xx [in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_labelling [in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_loop_loop' [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Add_Add [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Add_In [in MetaCoq.Template.utils.wGraph]
WeightedGraph.correct_labelling_lsp_G' [in MetaCoq.Template.utils.wGraph]
WeightedGraph.correct_labelling_lsp [in MetaCoq.Template.utils.wGraph]
WeightedGraph.correct_labelling_PathOf [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_In [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add4 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove_inv [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_Equal_l [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_Equal [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove_add [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_union [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_Subset [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add3 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Disjoint_DisjointAdd [in MetaCoq.Template.utils.wGraph]
WeightedGraph.edge_map_spec2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.edge_map_spec1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.extends_correct_labelling [in MetaCoq.Template.utils.wGraph]
WeightedGraph.extends_labelling [in MetaCoq.Template.utils.wGraph]
WeightedGraph.first_in_first [in MetaCoq.Template.utils.wGraph]
WeightedGraph.first_in_in [in MetaCoq.Template.utils.wGraph]
WeightedGraph.from_G'_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.from_G'_path_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.invariants_relabel [in MetaCoq.Template.utils.wGraph]
WeightedGraph.In_nodes_app_end [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.add_from_orig_spec [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.border_set_spec [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.EdgeSet_fold_spec_right2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.fold_fun_spec [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_subgraph_spec [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_spec [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_lsp_dominate [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_eq_is_full_extension [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_bound_extend_border [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.spath_on_border [in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.sweight_bound0 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_acyclic_correct [in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_acyclic_spec [in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_nonpos_nbar [in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_nonpos_spec [in MetaCoq.Template.utils.wGraph]
WeightedGraph.labelling_ext_lsp [in MetaCoq.Template.utils.wGraph]
WeightedGraph.leqb_vertices_correct [in MetaCoq.Template.utils.wGraph]
WeightedGraph.leq_vertices_caract [in MetaCoq.Template.utils.wGraph]
WeightedGraph.leq_vertices_caract0 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.le_Some_lsp [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_Gl_between_G1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_Gl_upperbound_G1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_edge [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_vset_in [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_spec_left [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_incr [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_sx [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_yx [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_pathOf [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_source_max [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_to_source [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_from_source [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_xx [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_xx_acyclic [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_to_s [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_sym [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_codistance [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_correctness [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_s [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_triangle_inequality [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_spec_eq0 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_spec_eq [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_spec_le [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_VSet_Equal [in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_eq [in MetaCoq.Template.utils.wGraph]
WeightedGraph.negbe [in MetaCoq.Template.utils.wGraph]
WeightedGraph.nodes_subset [in MetaCoq.Template.utils.wGraph]
WeightedGraph.pathOf_add_end_simpl [in MetaCoq.Template.utils.wGraph]
WeightedGraph.PathOf_add_end_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.PathOf_In [in MetaCoq.Template.utils.wGraph]
WeightedGraph.reflect_logically_equiv [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.dxy_bound [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_diff [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_y [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_x [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_correct [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.r_correct [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_mon [in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_add [in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_correct_labelling [in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_invariants [in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_lsp_G2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_lsp_G1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_lsp [in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath [in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath_aux3 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath_aux2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath_aux1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify_aux3 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify_aux2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify_aux1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.source_bottom [in MetaCoq.Template.utils.wGraph]
WeightedGraph.spathG1_lsp_Gl [in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath_sets [in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath_In' [in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath_In [in MetaCoq.Template.utils.wGraph]
WeightedGraph.sto_G'_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.subgraph_acyclic [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.correct_labelling_lsp_G' [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.from_G'_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.from_G'_path_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_spec_left [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_sx [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_incr [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_yx [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_pathOf [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.sto_G'_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.to_G'_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_relabel_on_G2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_relabel_on_G1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_inverse [in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_sconcat [in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_label_to_nat [in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_G'_weight [in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_label_max [in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_Forall_reflect [in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_add_add_same [in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_add_add [in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_remove_add [in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_add_remove [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_from2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_from1 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_inverse [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_simplify2' [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_simplify2 [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_reduce [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_simplify [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_split' [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_split [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_add_end [in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_concat [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Zle_opp' [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Zle_opp [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Z_of_to_label_pos [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Z_of_to_label_s [in MetaCoq.Template.utils.wGraph]
WeightedGraph.Z_of_to_label [in MetaCoq.Template.utils.wGraph]
wellformed_optimize_decl_extends [in MetaCoq.Erasure.EInlineProjections]
wellformed_optimize_extends [in MetaCoq.Erasure.EInlineProjections]
wellformed_projection_args [in MetaCoq.Erasure.EInlineProjections]
wellformed_lookup_constructor_pars_args [in MetaCoq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_constructor_pars [in MetaCoq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_inductive_pars [in MetaCoq.Erasure.EConstructorsAsBlocks]
wellformed_closed_env [in MetaCoq.Erasure.EWellformed]
wellformed_mkApps [in MetaCoq.Erasure.EWellformed]
wellformed_iota_red_brs [in MetaCoq.Erasure.EWellformed]
wellformed_iota_red [in MetaCoq.Erasure.EWellformed]
wellformed_cunfold_cofix [in MetaCoq.Erasure.EWellformed]
wellformed_cunfold_fix [in MetaCoq.Erasure.EWellformed]
wellformed_cofix_subst [in MetaCoq.Erasure.EWellformed]
wellformed_fix_subst [in MetaCoq.Erasure.EWellformed]
wellformed_substl [in MetaCoq.Erasure.EWellformed]
wellformed_csubst [in MetaCoq.Erasure.EWellformed]
wellformed_subst [in MetaCoq.Erasure.EWellformed]
wellformed_subst_eq [in MetaCoq.Erasure.EWellformed]
wellformed_lift [in MetaCoq.Erasure.EWellformed]
wellformed_up [in MetaCoq.Erasure.EWellformed]
wellformed_closed_decl [in MetaCoq.Erasure.EWellformed]
wellformed_closed [in MetaCoq.Erasure.EWellformed]
wellformed_gen_transform_decl_extends [in MetaCoq.Erasure.EGenericMapEnv]
wellformed_optimize_decl_extends [in MetaCoq.Erasure.EOptimizePropDiscr]
wellformed_optimize_extends [in MetaCoq.Erasure.EOptimizePropDiscr]
welltyped_mkApps_inv [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
welltyped_brs [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_zipp [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_stack_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_zipx [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn_iff [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_fill_context_hole [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_alpha [in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_subterm [in MetaCoq.SafeChecker.PCUICSafeRetyping]
welltyped_wellformed [in MetaCoq.Erasure.ErasureProperties]
welltyped_mkApps_inv [in MetaCoq.Erasure.ErasureFunction]
welltyped_R_pres [in MetaCoq.SafeChecker.PCUICSafeReduce]
welltyped_is_open_term [in MetaCoq.SafeChecker.PCUICSafeReduce]
welltyped_is_closed_context [in MetaCoq.SafeChecker.PCUICSafeReduce]
welltyped_R_zipc [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_wf [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_inv [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipp_inv [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tProd_appstack_nil [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tCase_brs_length [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tConst_inv [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_wf_local [in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_letin_red [in MetaCoq.SafeChecker.PCUICSafeChecker]
welltyped_letin_inv [in MetaCoq.SafeChecker.PCUICSafeChecker]
welltyped_prod_inv [in MetaCoq.SafeChecker.PCUICSafeChecker]
well_sorted_wellinferred [in MetaCoq.SafeChecker.PCUICSafeRetyping]
well_subst_app_up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_app [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up' [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_ext [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_prop_wf [in MetaCoq.Examples.tauto]
WfArity_build_case_predicate_type [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_fixpoint_rarg [in MetaCoq.Template.EtaExpand]
wf_env_fresh [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_fresh_globals [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_eta [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_ext_gc_of_uctx [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_gc_of_uctx [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_ext_wf [in MetaCoq.PCUIC.PCUICElimination]
wf_precompose [in MetaCoq.Template.utils.MCRelations]
wf_fun [in MetaCoq.PCUIC.PCUICSafeLemmata]
wf_case_inst_case_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
wf_inst_case_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
wf_local_def [in MetaCoq.PCUIC.PCUICArities]
wf_local_ass [in MetaCoq.PCUIC.PCUICArities]
wf_types [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_ctx_universes_closed [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_closedu [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instance_closed [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_closed [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_level_closed [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_extended_subst [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_projs [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_abstract_instance [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_sorts_local_ctx_nth_error [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_sorts_local_ctx_smash [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_mkApps [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_inds [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_weaken [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_weaken_full [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_inst [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_subst [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_lift [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universeb_instance_forall [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_reflect [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_subst_instance [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instance_In [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instance_sub [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_level_sub [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_level_mono [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instantiate [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_subst_instance_univ [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instanceP [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_levelP [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_product [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_sup [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_super [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_type1 [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_type0 [in MetaCoq.PCUIC.PCUICWfUniverses]
wf_local_closed_context [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wf_ind_arities [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_expand_lets_ctx [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_expand_lets [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_it_mkProd_or_LetIn [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_wf_decl_pred [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_fresh_globals [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_local_inv [in MetaCoq.Template.Typing]
wf_local_app_l [in MetaCoq.Template.Typing]
wf_dlexprod [in MetaCoq.PCUIC.utils.PCUICUtils]
wf_nth [in MetaCoq.Template.WfAst]
wf_subst_instance [in MetaCoq.Template.WfAst]
wf_mkApps_inv [in MetaCoq.Template.WfAst]
wf_mkApps_napp [in MetaCoq.Template.WfAst]
wf_strip_outer_cast [in MetaCoq.Template.WfAst]
wf_subst1 [in MetaCoq.Template.WfAst]
wf_subst [in MetaCoq.Template.WfAst]
wf_lift [in MetaCoq.Template.WfAst]
wf_mkApps [in MetaCoq.Template.WfAst]
wf_mkApp [in MetaCoq.Template.WfAst]
wf_inv [in MetaCoq.Template.WfAst]
wf_arities_context [in MetaCoq.PCUIC.PCUICSubstitution]
wf_arities_context' [in MetaCoq.PCUIC.PCUICSubstitution]
wf_mkApps [in MetaCoq.Erasure.EInlineProjections]
wf_optimize [in MetaCoq.Erasure.EInlineProjections]
wf_ind_predicate [in MetaCoq.PCUIC.PCUICInductives]
wf_local_expand_lets [in MetaCoq.PCUIC.PCUICInductives]
wf_projection_context [in MetaCoq.PCUIC.PCUICInductives]
wf_local_nth_isType [in MetaCoq.PCUIC.PCUICInductives]
wf_projection_arg_ctx [in MetaCoq.PCUIC.PCUICInductives]
wf_projection_context_gen [in MetaCoq.PCUIC.PCUICInductives]
wf_subslet_dom [in MetaCoq.PCUIC.PCUICInductives]
wf_arities_context_inst [in MetaCoq.PCUIC.PCUICInductives]
wf_pre_case_predicate_context_gen [in MetaCoq.PCUIC.PCUICValidity]
wf_case_branches_types' [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_branches_types [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type' [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_pre_case_branch_context_gen [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_predicate_context [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_set_binder_name [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_local_vass [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_typing_spine [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_all [in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_local_alpha [in MetaCoq.PCUIC.PCUICAlpha]
wf_local_eq_context_upto_names [in MetaCoq.PCUIC.PCUICAlpha]
wf_local_nth_error_vass [in MetaCoq.PCUIC.PCUICAlpha]
wf_cons_inv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_ind_indices [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_local_ind_params_weaken [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_local_subst_instance_decl [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate_poly [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_cumul_context_closed [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wf_conv_context_closed [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wf_branch_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pcontext [in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pars [in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branchesP [in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branchP [in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicateP [in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_local_rel_conv [in MetaCoq.Erasure.ErasureProperties]
wf_local_All_fold [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wf_lookup [in MetaCoq.Erasure.ErasureFunction]
wf_cod' [in MetaCoq.Erasure.ErasureFunction]
wf_cod [in MetaCoq.Erasure.ErasureFunction]
wf_local_rel_alpha_eq_end [in MetaCoq.Erasure.ErasureFunction]
wf_local_app_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wf_fix_inv [in MetaCoq.Erasure.EWellformed]
wf_glob_fresh [in MetaCoq.Erasure.EProgram]
wf_consistent [in MetaCoq.PCUIC.PCUICGlobalEnv]
wf_cunfold_cofix [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_cunfold_fix [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_cofix_subst [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_fix_subst [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_substl [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_csubst [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_local_app_skipn [in MetaCoq.PCUIC.PCUICTyping]
wf_local_app_ind [in MetaCoq.PCUIC.PCUICTyping]
wf_local_inv [in MetaCoq.PCUIC.PCUICTyping]
wf_local_app_l [in MetaCoq.PCUIC.PCUICTyping]
wf_ext_consistent [in MetaCoq.PCUIC.PCUICTyping]
wf_ext_wf [in MetaCoq.PCUIC.PCUICTyping]
wf_env_non_var_levels [in MetaCoq.PCUIC.PCUICTyping]
wf_cofixpoint_spine [in MetaCoq.PCUIC.PCUICCanonicity]
wf_fixpoint_spine [in MetaCoq.PCUIC.PCUICCanonicity]
wf_cofixpoint_inv [in MetaCoq.PCUIC.PCUICCanonicity]
wf_fixpoint_inv [in MetaCoq.PCUIC.PCUICCanonicity]
wf_universe_nl [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
wf_local_subst1 [in MetaCoq.PCUIC.PCUICSR]
wf_local_red [in MetaCoq.PCUIC.PCUICSR]
wf_local_red1 [in MetaCoq.PCUIC.PCUICSR]
wf_local_isType_nth [in MetaCoq.PCUIC.PCUICSR]
wf_subslet_skipn [in MetaCoq.PCUIC.PCUICSR]
wf_pre_case_branch_context [in MetaCoq.PCUIC.PCUICSR]
wf_cofixpoint_red1_body [in MetaCoq.PCUIC.PCUICSR]
wf_cofixpoint_red1_type [in MetaCoq.PCUIC.PCUICSR]
wf_fixpoint_red1_body [in MetaCoq.PCUIC.PCUICSR]
wf_fixpoint_red1_type [in MetaCoq.PCUIC.PCUICSR]
wf_context_sorts [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wf_cons_inv [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wf_universe_super [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_universe_type1 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_universe_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_ext_wk_wf [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_local_app_renaming [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wf_ctx_universes_app [in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_local_wf_ctx_universes [in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_ctx_universes_subst_instance [in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_decl_universes_subst_instance [in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_ind_types_wf_arities [in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_local_bd_rel_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_bd_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_local_rel [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_rel_weak [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_rel_subst1 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_it_mkLambda_or_LetIn [in MetaCoq.Template.TypingWf]
wf_Lambda_or_LetIn [in MetaCoq.Template.TypingWf]
wf_it_mkProd_or_LetIn_inv [in MetaCoq.Template.TypingWf]
wf_lift_wf [in MetaCoq.Template.TypingWf]
wf_red1 [in MetaCoq.Template.TypingWf]
wf_projs [in MetaCoq.Template.TypingWf]
wf_case_branches_context [in MetaCoq.Template.TypingWf]
wf_case_branch_context_gen [in MetaCoq.Template.TypingWf]
wf_inds [in MetaCoq.Template.TypingWf]
wf_case_predicate_context [in MetaCoq.Template.TypingWf]
wf_extended_subst [in MetaCoq.Template.TypingWf]
wf_subst_instance_context [in MetaCoq.Template.TypingWf]
wf_lift_context [in MetaCoq.Template.TypingWf]
wf_map2_set_binder_name [in MetaCoq.Template.TypingWf]
wf_reln [in MetaCoq.Template.TypingWf]
wf_smash_context [in MetaCoq.Template.TypingWf]
wf_subst_context [in MetaCoq.Template.TypingWf]
wf_it_mkProd_or_LetIn [in MetaCoq.Template.TypingWf]
wf_decl_extends [in MetaCoq.Template.TypingWf]
wf_extends [in MetaCoq.Template.TypingWf]
wf_local_smash_context [in MetaCoq.PCUIC.PCUICContexts]
wf_local_rel_empty [in MetaCoq.PCUIC.PCUICContexts]
wf_local_smash_end [in MetaCoq.PCUIC.PCUICContexts]
wf_local_rel_smash_context [in MetaCoq.PCUIC.PCUICContexts]
wf_local_rel_smash_context_gen [in MetaCoq.PCUIC.PCUICContexts]
wf_mkApps [in MetaCoq.Erasure.EGenericMapEnv]
wf_arity_spine_typing_spine [in MetaCoq.PCUIC.PCUICSpine]
wf_local_alpha [in MetaCoq.PCUIC.PCUICSpine]
wf_local_rel_wf_local_bd [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wf_local_wf_local_bd [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
whne_conv_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
whne_All2_fold [in MetaCoq.PCUIC.PCUICSafeLemmata]
whne_eq_term_upto_univ_napp [in MetaCoq.PCUIC.PCUICNormal]
whne_red1_inv [in MetaCoq.PCUIC.PCUICNormal]
whne_pres [in MetaCoq.PCUIC.PCUICNormal]
whne_pres1 [in MetaCoq.PCUIC.PCUICNormal]
whne_red1_ind [in MetaCoq.PCUIC.PCUICNormal]
whne_isConstruct_app [in MetaCoq.PCUIC.PCUICNormal]
whne_mkApps_inv [in MetaCoq.PCUIC.PCUICNormal]
whne_mkApps [in MetaCoq.PCUIC.PCUICNormal]
whnf_conv_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
whnf_All2_fold [in MetaCoq.PCUIC.PCUICSafeLemmata]
whnf_eq_term [in MetaCoq.PCUIC.PCUICNormal]
whnf_eq_term_upto_univ_napp [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_isApp [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_red1_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_trans [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_refl [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_refl_whne [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps_r_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps_l_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_red [in MetaCoq.PCUIC.PCUICNormal]
whnf_pres [in MetaCoq.PCUIC.PCUICNormal]
whnf_pres1 [in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_tLambda_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_tProd_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_tSort_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_whne_nodelta_upgrade [in MetaCoq.PCUIC.PCUICNormal]
whnf_fixapp' [in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_inv [in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps [in MetaCoq.PCUIC.PCUICNormal]
whnf_red_isIndConstructApp [in MetaCoq.PCUIC.PCUICConvCumInversion]
whnf_proj_arg_whne [in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_case_arg_whne [in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_fix_arg_whne [in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_non_cofix_ind_typed [in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_finite_ind_typed [in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_ind_finite [in MetaCoq.PCUIC.PCUICCanonicity]
wh_normal_ind_discr [in MetaCoq.PCUIC.PCUICCanonicity]
wh_neutral_empty [in MetaCoq.PCUIC.PCUICCanonicity]
wh_neutral_empty_gen [in MetaCoq.PCUIC.PCUICCanonicity]
WN [in MetaCoq.PCUIC.PCUICProgress]
ws_wcbv_standardization [in MetaCoq.PCUIC.PCUICProgress]
ws_cumul_pb_zippx [in MetaCoq.PCUIC.PCUICSafeLemmata]
ws_cumul_ctx_pb_app [in MetaCoq.PCUIC.PCUICArities]
ws_cumul_ctx_pb_vass [in MetaCoq.PCUIC.PCUICArities]
ws_cumul_ctx_pb_wf_local [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_inst_variance [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_Prod_Prod_inv_l [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_subst [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_inv [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_eq [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_terms_confl [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_tRel [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_ctx_pb_rel_context_assumptions [in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_l_inv_alt [in MetaCoq.PCUIC.PCUICCumulProp]
ws_cumul_pb_it_mkProd_or_LetIn_smash [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_pb_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_ctx_pb_refl [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_forget [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_inv [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_left [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_right [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_inv [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_cumul_pb_decls [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_right [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_left [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt_closed [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_conv [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_cumul [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_right [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_left [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_closed_context [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl' [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_red_confluence [in MetaCoq.PCUIC.PCUICConfluence]
ws_pred_pred [in MetaCoq.PCUIC.PCUICConfluence]
ws_pred_curry_red [in MetaCoq.PCUIC.PCUICConfluence]
ws_red_refl_irrel [in MetaCoq.PCUIC.PCUICConfluence]
ws_red_irrel [in MetaCoq.PCUIC.PCUICConfluence]
ws_red_red_ctx [in MetaCoq.PCUIC.PCUICConfluence]
ws_red_red_ctx_aux [in MetaCoq.PCUIC.PCUICConfluence]
ws_red_red [in MetaCoq.PCUIC.PCUICConfluence]
ws_red_ctx_length [in MetaCoq.PCUIC.PCUICConfluence]
ws_term_eq [in MetaCoq.PCUIC.PCUICConfluence]
ws_pred1_diamond [in MetaCoq.PCUIC.PCUICConfluence]
ws_pred1_red [in MetaCoq.PCUIC.PCUICConfluence]
ws_pred_ws_pred_curry [in MetaCoq.PCUIC.PCUICConfluence]
ws_red1_pred1 [in MetaCoq.PCUIC.PCUICConfluence]
ws_red1_pred1_curry [in MetaCoq.PCUIC.PCUICConfluence]
ws_context_on_free_vars_xpredT [in MetaCoq.PCUIC.PCUICConfluence]
ws_context_xpredT [in MetaCoq.PCUIC.PCUICConfluence]
ws_term_xpredT [in MetaCoq.PCUIC.PCUICConfluence]
ws_cumul_pb_Construct [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Evar [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_subst [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_weaken [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_conv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_ws_cumul_ctx [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_alt [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_rel_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_rel_app [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_elim [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_substs_red [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_ty [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_tm [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps_weak [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn_codom [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn_codom [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_bo [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_r [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_l [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_eq_le_gen [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_CoFix [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Fix [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_or_cofix [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_bodies [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_body [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_types [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_type [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_brs [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_one_brs [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_c [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_p [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_App [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Proj_c [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_App_r [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_App_l [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_r_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_right [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_left [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_l_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_r_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_l_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_red_l_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_red_r_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Prod_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_r_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_r_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_l_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Sort_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_Prod_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_inv [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l [in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_app_same [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_refl [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_true_forget [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_false_forget [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_decls_ws_cumul_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx_inv [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_le [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_red [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx_inv [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_context_upto [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context_inv [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red [in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_terms_refl [in MetaCoq.PCUIC.PCUICSR]
ws_cumul_pb_terms_eq_trans [in MetaCoq.PCUIC.PCUICSR]
ws_cumul_pb_eq_trans [in MetaCoq.PCUIC.PCUICSR]
ws_cumul_pb_meta_refl [in MetaCoq.PCUIC.PCUICSR]
ws_cumul_ctx_pb_rel_trans [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_ws_cumul_ctx [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_length [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_ws_cumul_ctx [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_smash [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_conv_extended_subst [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_eq_le [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_le_le [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_le_le [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_lift [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_k [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_context_assumptions [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel'_context_assumptions [in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_cons [in MetaCoq.SafeChecker.PCUICTypeChecker]
wt_inv [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_cumul_pb_equalityP [in MetaCoq.PCUIC.PCUICSubstitution]
wt_ind_app_variance [in MetaCoq.PCUIC.PCUICInductiveInversion]
wt_closed [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_subst_instance [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_convSpec_convAlgo [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_inv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_wt [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_mkApps_inv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_on_free_vars [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_inv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_wf_local [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cum_ws_cumul_ctx_pb [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wt_cum_ws_cumul_pb [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wt_ws_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_ctx_pb_forget [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_trans [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_ws_cumul_pb [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_zip_mkapps [in MetaCoq.SafeChecker.PCUICSafeConversion]
wt_closed_red_refl [in MetaCoq.PCUIC.PCUICCanonicity]
wt_closed_red1 [in MetaCoq.PCUIC.PCUICSR]
wt_terms_ws_cumul_pb [in MetaCoq.PCUIC.PCUICSR]
wt_cumul_pb_refl [in MetaCoq.PCUIC.PCUICSR]
wt_cstrs [in MetaCoq.SafeChecker.PCUICSafeChecker]
| 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) |