| 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
wat_welltyped [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]wat:1730 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wcbeval_red [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
Wcbv [section, in MetaCoq.PCUIC.PCUICWcbvEval]
Wcbv [section, in MetaCoq.Template.WcbvEval]
Wcbv [section, in MetaCoq.Erasure.EWcbvEval]
Wcbv [section, in MetaCoq.Erasure.EWcbvEval]
WcbvEnv [section, in MetaCoq.Erasure.EWcbvEval]
WcbvEval [library]
WcbvFlags [record, in MetaCoq.Erasure.EWcbvEval]
wcbv_standardization [lemma, in MetaCoq.PCUIC.PCUICProgress]
wcon:127 [binder, in MetaCoq.Erasure.EInlineProjections]
wcon:142 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
wcon:37 [binder, in MetaCoq.Erasure.ETransform]
wcon:371 [binder, in MetaCoq.Erasure.ERemoveParams]
wcon:450 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
wcon:498 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
wcon:550 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
wcon:559 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
wcon:62 [binder, in MetaCoq.Erasure.ETransform]
wcon:73 [binder, in MetaCoq.Erasure.ETransform]
wcon:83 [binder, in MetaCoq.Erasure.ETransform]
wcon:95 [binder, in MetaCoq.Erasure.ETransform]
wcored [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
wcored_wf [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
weakening [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_env_declared_projection [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constructor [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_inductive [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_minductive [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_declared_constant [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_consistent_instance [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_is_allowed_elimination [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_constraints [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels' [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_global_ext_levels [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weakening_env_cumul_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_decls [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv_decls [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_convSpec [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumulSpec0 [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_conv [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_cumul_gen [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_env_red1 [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
weakening_pred1_0 [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
weakening_pred1_pred1 [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
weakening_pred1 [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
weakening_conv_wt [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_conv [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_cumul [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red_0 [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red' [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_red1 [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_renaming [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weakening_is_closed_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
weakening_cumulSpec0 [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
weakening_gen [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_length [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_typing [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_rename_typing [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local_eq [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_wf_local [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weakening_ws_cumul_pb_eq [lemma, in MetaCoq.PCUIC.PCUICConversion]
weakening_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
weakening_cumul0 [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
weakening_env_declared_constructor [lemma, in MetaCoq.Erasure.EExtends]
weakening_env_declared_inductive [lemma, in MetaCoq.Erasure.EExtends]
weakening_env_declared_minductive [lemma, in MetaCoq.Erasure.EExtends]
weakening_env_declared_constant [lemma, in MetaCoq.Erasure.EExtends]
weakening_closed_red1 [lemma, in MetaCoq.PCUIC.PCUICSR]
weakening_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICSR]
weakening_eval_env [lemma, in MetaCoq.Erasure.EWcbvEval]
weakening_env_lookup_on_global_env [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env_decls_lookup_on_global_env [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl_ext [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_on_global_decl [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_env [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weakening_closed_red [lemma, in MetaCoq.PCUIC.PCUICSpine]
weaken_env_decls_prop [definition, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop [definition, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weaken_env_prop_full [definition, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weaken_lookup_on_global_env' [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
weaken_subslet [lemma, in MetaCoq.PCUIC.PCUICArities]
weaken_wf_universes [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_universe_instance [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_universe_level [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_universe [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
weaken_wf_decl_pred [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
weaken_env_prop_isType [lemma, in MetaCoq.PCUIC.PCUICValidity]
weaken_wf_subslet [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
weaken_nth_error_lt [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_nth_error_ge [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
weaken_prop [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
weaken_prefix [lemma, in MetaCoq.Erasure.ErasureFunction]
weaken_ctx [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_wf_local [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
weaken_ws_cumul_ctx_pb_rel [lemma, in MetaCoq.PCUIC.PCUICConversion]
weaken_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
weaken_env_prop_closed [lemma, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
weaken_sorts_local_ctx [lemma, in MetaCoq.PCUIC.PCUICContexts]
weaken_type_local_ctx [lemma, in MetaCoq.PCUIC.PCUICContexts]
weaken_wf_local [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_env_decls_prop_typing [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_env_prop_typing [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_decls_lookup_on_global_env [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_lookup_on_global_env [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
weaken_subslet [lemma, in MetaCoq.PCUIC.PCUICSpine]
WeakEtaExp [section, in MetaCoq.Erasure.EEtaExpanded]
weakFunext [definition, in MetaCoq.Translations.times_bool_fun2]
WeakNormalization [section, in MetaCoq.PCUIC.PCUICCanonicity]
WeakNormalization.reducible [section, in MetaCoq.PCUIC.PCUICCanonicity]
WeightedGraph [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_relabel_on [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_loop_sloop [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_sloop [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_relabel [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_caract2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_caract1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_lsp0_xx [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_labelling [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_loop_loop' [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_loop' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_loop [record, in MetaCoq.Template.utils.wGraph]
WeightedGraph.acyclic_no_loop [inductive, in MetaCoq.Template.utils.wGraph]
WeightedGraph.add_end [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.add_edge [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.add_node [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Add_Add [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Add_In [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Add_Proper [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Build_acyclic_no_loop [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Build_acyclic_no_loop [constructor, in MetaCoq.Template.utils.wGraph]
WeightedGraph.concat [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.correct_labelling_lsp_G' [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.correct_labelling_lsp [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.correct_labelling_PathOf [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.correct_labelling [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.diff [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Disjoint [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_In [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add4 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove_inv [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_Equal_l [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_Equal [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove_add [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_Proper [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_union [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_Subset [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_remove [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add3 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.DisjointAdd_add1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Disjoint_DisjointAdd [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.E [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.EdgeOf [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.EdgeSet [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.EdgeSetDecide [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.EdgeSetFact [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.EdgeSetProp [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.edges_sub [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.edges_vertices [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.edge_map_spec2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.edge_map_spec1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.edge_map [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.edge_pathOf [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.compare [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.compare_spec [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.eq [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.eqb [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.eq_leibniz [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.eq_dec [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.eq_equiv [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.lt [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.lt_compat [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.lt_strorder [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Edge.t [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.ExtendLabelling [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.ExtendLabelling.Gl [variable, in MetaCoq.Template.utils.wGraph]
WeightedGraph.ExtendLabelling.l' [variable, in MetaCoq.Template.utils.wGraph]
WeightedGraph.extends_correct_labelling [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.extends_labelling [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.e_weight [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.e_target [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.e_source [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.FirstVertexIn [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.first_in_first [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.first_in_in [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.first_in [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.from_G'_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.from_G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.from_G'_path_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.from_G'_path [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.from1 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.from2 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.full_subgraph [record, in MetaCoq.Template.utils.wGraph]
WeightedGraph.graph [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.HG' [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.HI' [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.invariants [record, in MetaCoq.Template.utils.wGraph]
WeightedGraph.invariants_relabel [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.In_nodes_app_end [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.add_from_orig_spec [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.add_from_orig [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.Border [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.border_set_spec [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.border_set [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.EdgeSet_fold_spec_right2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.fold_fun_spec [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.fold_fun [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_subgraph_spec [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_subgraph [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_spec [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension_lsp_dominate [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.is_full_extension [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.LspBoundExtendBorder.bs [variable, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_eq_is_full_extension [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.lsp_bound_extend_border [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.spath_on_border [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.IsFullSubgraph.sweight_bound0 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_subgraph [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_acyclic_correct [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_acyclic_spec [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_acyclic [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_nonpos_nbar [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_nonpos_spec [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_nonpos [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.is_simple [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.labelling [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.labelling_ext_lsp [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.length [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.leqb_vertices_correct [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.leqb_vertices [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.leq_vertices_caract [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.leq_vertices_caract0 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.leq_vertices [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.le_Some_lsp [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_dominate [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_Gl_between_G1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_Gl_upperbound_G1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_edge [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_map_path2 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_vset_in [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_spec_left [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_incr [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_sx [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_G'_yx [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_pathOf [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_source_max [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_to_source [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_from_source [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_xx [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_xx_acyclic [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_to_s [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_sym [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_codistance [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_correctness [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp_s [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_sub [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_triangle_inequality [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_spec_eq0 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_spec_eq [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_spec_le [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_VSet_Equal [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp0_eq [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.lsp00 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.MapSPath [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.map_spath [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.map_path [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.negbe [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.nodes [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.nodes_subset [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.opp_edge [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.PathOf [inductive, in MetaCoq.Template.utils.wGraph]
WeightedGraph.pathOf_add_end_simpl [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.PathOf_add_end_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.PathOf_add_end [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.PathOf_In [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.pathOf_step [constructor, in MetaCoq.Template.utils.wGraph]
WeightedGraph.pathOf_refl [constructor, in MetaCoq.Template.utils.wGraph]
WeightedGraph.PosPathOf [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reduce [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reflectEq_nbar [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reflectEq_Z [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reflectEq_vertices [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reflect_logically_equiv [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelOn [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.dxy [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.dxy_bound [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_diff [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_y [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_on_x [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.l'_correct [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.r [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.BuildLabelling [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.RelabelWrtEdge.RelabelCoefs [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.r_correct [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.stdl [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_mon [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.RelabelWrtEdge.to_label_add [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_correct_labelling [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_invariants [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_lsp_G2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on_lsp_G1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_on [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_map [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_path [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_lsp [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.relabel_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath_aux [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath_aux3 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath_aux2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.reroot_spath_aux1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.s [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.same_src [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sconcat [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify_aux3 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify_aux2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify_aux1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify2 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.simplify2' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.snodes [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.snodes_Subset [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.source_bottom [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.source_pathOf [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.source_vertex [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath [inductive, in MetaCoq.Template.utils.wGraph]
WeightedGraph.spathG1_lsp_Gl [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath_sets [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath_In' [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath_In [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.spath_one [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.SPath_sub [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.spath_step [constructor, in MetaCoq.Template.utils.wGraph]
WeightedGraph.spath_refl [constructor, in MetaCoq.Template.utils.wGraph]
WeightedGraph.split [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.split' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sto_G'_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sto_G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.subgraph [record, in MetaCoq.Template.utils.wGraph]
WeightedGraph.subgraph [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.subgraph_acyclic [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.subgraph_on_edge [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.subgraph.subgraph2 [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1 [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.correct_labelling_lsp_G' [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.from_G'_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.from_G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.from_G'_path_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.from_G'_path [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.graph2 [section, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.HG' [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.HI' [instance, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_spec_left [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_sx [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_incr [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_G'_yx [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.lsp_pathOf [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.sto_G'_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.sto_G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.to_G'_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Subgraph1.to_G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.succs [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_relabel_on_G2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_relabel_on_G1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_inverse [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_sconcat [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.sweight_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.t [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_label_to_nat [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_G'_weight [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_G' [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_label_max [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_label [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_simple [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.to_pathOf [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.V [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.vertices_sub [projection, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSetDecide [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSetFact [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSetProp [module, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_Forall_reflect [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_add_add_same [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_add_add [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_remove_add [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.VSet_add_remove [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_from2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_from1 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_map_spath2 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_map_spath1 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_map_path2 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_map_path1 [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_inverse [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_simplify2' [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_simplify2 [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_reduce [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_simplify [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_split' [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_split [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_SPath_sub [definition, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_add_end [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.weight_concat [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Zle_opp' [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Zle_opp [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Z_of_to_label_pos [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Z_of_to_label_s [lemma, in MetaCoq.Template.utils.wGraph]
WeightedGraph.Z_of_to_label [lemma, in MetaCoq.Template.utils.wGraph]
_ ..w [notation, in MetaCoq.Template.utils.wGraph]
_ ..t [notation, in MetaCoq.Template.utils.wGraph]
_ ..s [notation, in MetaCoq.Template.utils.wGraph]
weight_on_edge:935 [binder, in MetaCoq.Template.utils.wGraph]
weight_on_edge:926 [binder, in MetaCoq.Template.utils.wGraph]
weight_on_edge:918 [binder, in MetaCoq.Template.utils.wGraph]
weight_on_edge:896 [binder, in MetaCoq.Template.utils.wGraph]
weight_on_edge:889 [binder, in MetaCoq.Template.utils.wGraph]
wellformed [definition, in MetaCoq.Erasure.ErasureProperties]
wellformed [abbreviation, in MetaCoq.Erasure.EWellformed]
wellformed [definition, in MetaCoq.Erasure.EWellformed]
wellformed_optimize_decl_extends [lemma, in MetaCoq.Erasure.EInlineProjections]
wellformed_optimize_extends [lemma, in MetaCoq.Erasure.EInlineProjections]
wellformed_projection_args [lemma, in MetaCoq.Erasure.EInlineProjections]
wellformed_lookup_constructor_pars_args [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_constructor_pars [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
wellformed_lookup_inductive_pars [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
wellformed_closed_env [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_mkApps [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_iota_red_brs [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_iota_red [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_cunfold_cofix [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_cunfold_fix [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_cofix_subst [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_fix_subst [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_substl [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_csubst [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_subst [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_subst_eq [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_lift [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_up [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_closed_decl [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_closed [lemma, in MetaCoq.Erasure.EWellformed]
wellformed_gen_transform_decl_extends [lemma, in MetaCoq.Erasure.EGenericMapEnv]
wellformed_optimize_decl_extends [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
wellformed_optimize_extends [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
wellfounded [instance, in MetaCoq.SafeChecker.PCUICSafeReduce]
wellinferred [inductive, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wellscoped [section, in MetaCoq.Erasure.ErasureProperties]
wellscoped.Def [section, in MetaCoq.Erasure.ErasureProperties]
welltyped [inductive, in MetaCoq.PCUIC.PCUICTyping]
welltyped [abbreviation, in MetaCoq.PCUIC.PCUICSR]
welltyped_mkApps_inv [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
welltyped_brs [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_zipp [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_zipc_stack_context [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_zipx [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn_iff [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_context [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_fill_context_hole [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_alpha [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
welltyped_subterm [lemma, in MetaCoq.SafeChecker.PCUICSafeRetyping]
welltyped_wellformed [lemma, in MetaCoq.Erasure.ErasureProperties]
welltyped_mkApps_inv [lemma, in MetaCoq.Erasure.ErasureFunction]
welltyped_R_pres [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
welltyped_is_open_term [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
welltyped_is_closed_context [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
welltyped_R_zipc [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_wf [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_inv [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipp_inv [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tProd_appstack_nil [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tCase_brs_length [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_zipc_tConst_inv [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_wf_local [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
welltyped_terms [abbreviation, in MetaCoq.PCUIC.PCUICSR]
welltyped_letin_red [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
welltyped_letin_inv [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
welltyped_prod_inv [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
well_subst_closed_subst [definition, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
well_subst_usubst [definition, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
well_sorted_wellinferred [lemma, in MetaCoq.SafeChecker.PCUICSafeRetyping]
well_sorted [definition, in MetaCoq.SafeChecker.PCUICSafeRetyping]
well_subst_app_up [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_app [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up' [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_Up [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_subst_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
well_prop_wf [lemma, in MetaCoq.Examples.tauto]
well_prop_True [constructor, in MetaCoq.Examples.tauto]
well_prop_False [constructor, in MetaCoq.Examples.tauto]
well_prop_Or [constructor, in MetaCoq.Examples.tauto]
well_prop_And [constructor, in MetaCoq.Examples.tauto]
well_prop_Impl [constructor, in MetaCoq.Examples.tauto]
well_prop_Rel [constructor, in MetaCoq.Examples.tauto]
well_prop [inductive, in MetaCoq.Examples.tauto]
well_subst [definition, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
well_typed [definition, in MetaCoq.Erasure.Prelim]
weqt [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
wf [definition, in MetaCoq.Template.Typing]
wf [inductive, in MetaCoq.Template.WfAst]
wf [section, in MetaCoq.Erasure.EWellformed]
wf [definition, in MetaCoq.PCUIC.PCUICTyping]
WfArity_build_case_predicate_type [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfars:974 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:350 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:403 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:631 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:797 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
WfAst [section, in MetaCoq.Template.TypingWf]
WfAst [library]
wfA:264 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfcofix:1111 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfcs:932 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfd':231 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfd:229 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
WfEnv [section, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
WfEnv [section, in MetaCoq.PCUIC.PCUICProgress]
WfEnv [section, in MetaCoq.PCUIC.PCUICArities]
WfEnv [section, in MetaCoq.PCUIC.PCUICContexts]
WfEnv [section, in MetaCoq.PCUIC.PCUICSpine]
WfEnv [section, in MetaCoq.PCUIC.PCUICSpine]
wfext:10 [binder, in MetaCoq.Erasure.ETransform]
wfext:1318 [binder, in MetaCoq.Erasure.ErasureFunction]
wfext:1335 [binder, in MetaCoq.Erasure.ErasureFunction]
wfext:1356 [binder, in MetaCoq.Erasure.ErasureFunction]
wfext:1371 [binder, in MetaCoq.Erasure.ErasureFunction]
wfext:1393 [binder, in MetaCoq.Erasure.ErasureFunction]
wfext:946 [binder, in MetaCoq.Erasure.ErasureFunction]
wfext:958 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfe:9 [binder, in MetaCoq.Erasure.ETransform]
wffix [section, in MetaCoq.Erasure.ErasureFunction]
wffix:1107 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfg:551 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfi:935 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
WfLookup [section, in MetaCoq.Template.TypingWf]
wfl_size_rel [abbreviation, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfl_size [abbreviation, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfl':273 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl':298 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl:1 [binder, in MetaCoq.Erasure.ErasureCorrectness]
wfl:11 [binder, in MetaCoq.Erasure.EProgram]
wfl:127 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
wfl:1307 [binder, in MetaCoq.Erasure.ErasureFunction]
wfl:1314 [binder, in MetaCoq.Erasure.ErasureFunction]
wfl:1331 [binder, in MetaCoq.Erasure.ErasureFunction]
wfl:1367 [binder, in MetaCoq.Erasure.ErasureFunction]
wfl:1389 [binder, in MetaCoq.Erasure.ErasureFunction]
wfl:155 [binder, in MetaCoq.Erasure.ErasureProperties]
wfl:16 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:160 [binder, in MetaCoq.Erasure.ErasureProperties]
wfl:167 [binder, in MetaCoq.Erasure.ErasureProperties]
wfl:170 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:174 [binder, in MetaCoq.Erasure.ErasureProperties]
wfl:181 [binder, in MetaCoq.Erasure.ErasureProperties]
wfl:271 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl:296 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl:311 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:317 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:343 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:352 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:362 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:370 [binder, in MetaCoq.Erasure.ERemoveParams]
wfl:375 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:381 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:399 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:421 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:434 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:457 [binder, in MetaCoq.Erasure.EWcbvEval]
wfl:5 [binder, in MetaCoq.Erasure.EProgram]
wfl:54 [binder, in MetaCoq.Erasure.EDeps]
wfl:59 [binder, in MetaCoq.Erasure.EInlineProjections]
wfl:59 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
wfl:64 [binder, in MetaCoq.Erasure.EInlineProjections]
wfl:81 [binder, in MetaCoq.Erasure.Prelim]
wfl:88 [binder, in MetaCoq.Erasure.Prelim]
wfl:92 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
wfl:942 [binder, in MetaCoq.Erasure.ErasureFunction]
wfl:95 [binder, in MetaCoq.Erasure.Prelim]
wfl:97 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
wfparams:928 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:352 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:405 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:633 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:799 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:972 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpret:730 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfP:107 [binder, in MetaCoq.Template.LiftSubst]
wfp:1094 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfP:112 [binder, in MetaCoq.Template.LiftSubst]
wfp:726 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
WfRed [section, in MetaCoq.Template.TypingWf]
wfterm [definition, in MetaCoq.Template.TemplateCheckWf]
wfty:577 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfty:579 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wft:219 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wFunext [definition, in MetaCoq.Translations.times_bool_fun]
wfunivs:650 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfu:221 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfu:651 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfX:344 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:438 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:445 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:456 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:466 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:494 [binder, in MetaCoq.Template.Universes]
wfX:534 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:715 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:940 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:948 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_fixpoint_rarg [lemma, in MetaCoq.Template.EtaExpand]
wf_env_init [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_empty [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_fresh [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_fresh_globals [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_eta [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext_map_repr [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext_map [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext_referenced [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_ext [record, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_map_repr [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_map [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env_referenced [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_env [record, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_ext_gc_of_uctx [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_gc_of_uctx [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wf_ext_wf [lemma, in MetaCoq.PCUIC.PCUICElimination]
Wf_size_lt [instance, in MetaCoq.Erasure.EInduction]
wf_precompose [lemma, in MetaCoq.Template.utils.MCRelations]
wf_fun [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
wf_case_inst_case_context [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
wf_inst_case_context [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
wf_program [definition, in MetaCoq.Template.TemplateCheckWf]
wf_global_env [definition, in MetaCoq.Template.TemplateCheckWf]
wf_global_declarations [definition, in MetaCoq.Template.TemplateCheckWf]
wf_global_decl [definition, in MetaCoq.Template.TemplateCheckWf]
wf_local_def [lemma, in MetaCoq.PCUIC.PCUICArities]
wf_local_ass [lemma, in MetaCoq.PCUIC.PCUICArities]
wf_typing_spine [definition, in MetaCoq.PCUIC.PCUICArities]
wf_types [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_ctx_universes_closed [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_closedu [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instance_closed [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_closed [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_level_closed [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_extended_subst [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_projs [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_ctx_universes [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_decl_universes [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_abstract_instance [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_sorts_local_ctx_nth_error [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_sorts_local_ctx_smash [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_mkApps [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_inds [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_weaken [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_weaken_full [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_inst [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_subst [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes_lift [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universeb_instance_forall [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universes [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_reflect [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universeb [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_subst_instance [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instance_In [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instance_sub [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_level_sub [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_level_mono [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instantiate [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_subst_instance_univ [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instanceP [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_levelP [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universeb_instance [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_instance [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_level [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universeb_level [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_product [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_sup [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_super [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_type1 [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_universe_type0 [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
wf_local_closed_context [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wf_ind_arities [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_expand_lets_ctx [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_expand_lets [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_trans_env [instance, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_wf_decl_pred [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_global_decl [definition, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_fresh_globals [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wf_ext_wf [definition, in MetaCoq.Template.Typing]
wf_local_inv [lemma, in MetaCoq.Template.Typing]
wf_local_app_l [lemma, in MetaCoq.Template.Typing]
wf_ext [definition, in MetaCoq.Template.Typing]
wf_cofixpoint [definition, in MetaCoq.Template.Typing]
wf_fixpoint [definition, in MetaCoq.Template.Typing]
WF_precompose [instance, in MetaCoq.PCUIC.utils.PCUICUtils]
wf_dlexprod [lemma, in MetaCoq.PCUIC.utils.PCUICUtils]
wf_nth [lemma, in MetaCoq.Template.WfAst]
wf_subst_instance [lemma, in MetaCoq.Template.WfAst]
wf_mkApps_inv [lemma, in MetaCoq.Template.WfAst]
wf_mkApps_napp [lemma, in MetaCoq.Template.WfAst]
wf_strip_outer_cast [lemma, in MetaCoq.Template.WfAst]
wf_subst1 [lemma, in MetaCoq.Template.WfAst]
wf_subst [lemma, in MetaCoq.Template.WfAst]
wf_lift [lemma, in MetaCoq.Template.WfAst]
wf_mkApps [lemma, in MetaCoq.Template.WfAst]
wf_mkApp [lemma, in MetaCoq.Template.WfAst]
wf_decl_pred [definition, in MetaCoq.Template.WfAst]
wf_decl [definition, in MetaCoq.Template.WfAst]
wf_inv [lemma, in MetaCoq.Template.WfAst]
wf_Inv [definition, in MetaCoq.Template.WfAst]
wf_tCoFix [constructor, in MetaCoq.Template.WfAst]
wf_tFix [constructor, in MetaCoq.Template.WfAst]
wf_tProj [constructor, in MetaCoq.Template.WfAst]
wf_tCase [constructor, in MetaCoq.Template.WfAst]
wf_tConstruct [constructor, in MetaCoq.Template.WfAst]
wf_tInd [constructor, in MetaCoq.Template.WfAst]
wf_tConst [constructor, in MetaCoq.Template.WfAst]
wf_tApp [constructor, in MetaCoq.Template.WfAst]
wf_tLetIn [constructor, in MetaCoq.Template.WfAst]
wf_tLambda [constructor, in MetaCoq.Template.WfAst]
wf_tProd [constructor, in MetaCoq.Template.WfAst]
wf_tCast [constructor, in MetaCoq.Template.WfAst]
wf_tSort [constructor, in MetaCoq.Template.WfAst]
wf_tEvar [constructor, in MetaCoq.Template.WfAst]
wf_tVar [constructor, in MetaCoq.Template.WfAst]
wf_tRel [constructor, in MetaCoq.Template.WfAst]
wf_nactx [abbreviation, in MetaCoq.Template.WfAst]
wf_arities_context [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
wf_arities_context' [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
wf_mkApps [lemma, in MetaCoq.Erasure.EInlineProjections]
wf_optimize [lemma, in MetaCoq.Erasure.EInlineProjections]
wf_term:196 [binder, in MetaCoq.Template.EnvironmentTyping]
wf_ind_predicate [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_local_expand_lets [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_projection_context [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_local_nth_isType [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_projection_arg_ctx [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_projection_context_gen [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_subslet_dom [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_subslet_subslet [projection, in MetaCoq.PCUIC.PCUICInductives]
wf_subslet_ctx [projection, in MetaCoq.PCUIC.PCUICInductives]
wf_subslet [record, in MetaCoq.PCUIC.PCUICInductives]
wf_arities_context_inst [lemma, in MetaCoq.PCUIC.PCUICInductives]
wf_pre_case_predicate_context_gen [lemma, in MetaCoq.PCUIC.PCUICValidity]
wf_case_branches_types' [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_branches_types [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type' [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_branch_type [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_pre_case_branch_context_gen [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_case_predicate_context [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_local_vass [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_typing_spine [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_cofixpoint_all [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wf_brs:130 [binder, in MetaCoq.PCUIC.PCUICInversion]
wf_pctx:122 [binder, in MetaCoq.PCUIC.PCUICInversion]
wf_pred:120 [binder, in MetaCoq.PCUIC.PCUICInversion]
wf_local_alpha [lemma, in MetaCoq.PCUIC.PCUICAlpha]
wf_local_eq_context_upto_names [lemma, in MetaCoq.PCUIC.PCUICAlpha]
wf_local_nth_error_vass [lemma, in MetaCoq.PCUIC.PCUICAlpha]
wf_cons_inv [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_ind_indices [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_ext_trans [abbreviation, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_trans [abbreviation, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_local_ind_params_weaken [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wf_local_subst_instance_decl [lemma, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_subst_instance [lemma, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate [lemma, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_local_instantiate_poly [lemma, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
wf_redp_subterm [instance, in MetaCoq.SafeChecker.PCUICWfReduction]
wf_redp_subterm_rel [definition, in MetaCoq.SafeChecker.PCUICWfReduction]
wf_hnf_subterm [instance, in MetaCoq.SafeChecker.PCUICWfReduction]
wf_hnf_subterm_rel [definition, in MetaCoq.SafeChecker.PCUICWfReduction]
wf_cumul_context_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wf_conv_context_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wf_branch_length [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pcontext [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicate_length_pars [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branchesP [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branchesb [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branches [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branches_gen [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branchP [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branchb [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branch [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_branch_gen [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicateP [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicateb [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicate [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_predicate_gen [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
wf_local_rel_conv [lemma, in MetaCoq.Erasure.ErasureProperties]
wf_local_All_fold [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wf_lookup [lemma, in MetaCoq.Erasure.ErasureFunction]
wf_fixpoints [definition, in MetaCoq.Erasure.ErasureFunction]
wf_reduction [instance, in MetaCoq.Erasure.ErasureFunction]
wf_reduction_aux [definition, in MetaCoq.Erasure.ErasureFunction]
wf_cod' [lemma, in MetaCoq.Erasure.ErasureFunction]
wf_cod [lemma, in MetaCoq.Erasure.ErasureFunction]
wf_local_rel_alpha_eq_end [lemma, in MetaCoq.Erasure.ErasureFunction]
wf_proof [instance, in MetaCoq.SafeChecker.PCUICSafeReduce]
wf_local_app_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wf_glob_cons [constructor, in MetaCoq.Erasure.EWellformed]
wf_glob_nil [constructor, in MetaCoq.Erasure.EWellformed]
wf_glob [inductive, in MetaCoq.Erasure.EWellformed]
wf_global_decl [definition, in MetaCoq.Erasure.EWellformed]
wf_minductive [definition, in MetaCoq.Erasure.EWellformed]
wf_inductive [definition, in MetaCoq.Erasure.EWellformed]
wf_projections [definition, in MetaCoq.Erasure.EWellformed]
wf_fix_inv [lemma, in MetaCoq.Erasure.EWellformed]
wf_fix [abbreviation, in MetaCoq.Erasure.EWellformed]
wf_fix_gen [definition, in MetaCoq.Erasure.EWellformed]
wf_universe_instance_iff [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
wf_universe_iff [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
wf_glob_fresh [lemma, in MetaCoq.Erasure.EProgram]
wf_eprogram_env [definition, in MetaCoq.Erasure.EProgram]
wf_eprogram [definition, in MetaCoq.Erasure.EProgram]
wf_consistent [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
wf_ext_global_uctx_invariants [definition, in MetaCoq.PCUIC.PCUICGlobalEnv]
wf_global_uctx_invariants [definition, in MetaCoq.PCUIC.PCUICGlobalEnv]
wf_cunfold_cofix [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_cunfold_fix [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_cofix_subst [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_fix_subst [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_substl [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_csubst [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wf_local_app_skipn [lemma, in MetaCoq.PCUIC.PCUICTyping]
wf_local_app_ind [lemma, in MetaCoq.PCUIC.PCUICTyping]
wf_local_app_inv [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_local_app [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_local_rel_app [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_local_rel_app_inv [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_local_inv [lemma, in MetaCoq.PCUIC.PCUICTyping]
wf_local_app_l [lemma, in MetaCoq.PCUIC.PCUICTyping]
wf_ext_consistent [lemma, in MetaCoq.PCUIC.PCUICTyping]
wf_ext_wf [lemma, in MetaCoq.PCUIC.PCUICTyping]
wf_ext [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_env_non_var_levels [lemma, in MetaCoq.PCUIC.PCUICTyping]
wf_brs:75 [binder, in MetaCoq.PCUIC.PCUICTyping]
wf_local_fun:62 [binder, in MetaCoq.PCUIC.PCUICTyping]
wf_pctx:56 [binder, in MetaCoq.PCUIC.PCUICTyping]
wf_pred:54 [binder, in MetaCoq.PCUIC.PCUICTyping]
wf_local_fun:40 [binder, in MetaCoq.PCUIC.PCUICTyping]
wf_cofixpoint [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_cofixpoint_gen [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_fixpoint [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_fixpoint_gen [definition, in MetaCoq.PCUIC.PCUICTyping]
wf_cofixpoint_spine [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wf_fixpoint_spine [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wf_cofixpoint_inv [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wf_fixpoint_inv [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wf_universe_nl [lemma, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
wf_local_subst1 [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_local_red [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_local_red1 [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_local_isType_nth [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_subslet_skipn [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_pre_case_branch_context [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_cofixpoint_red1_body [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_cofixpoint_red1_type [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_fixpoint_red1_body [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_fixpoint_red1_type [lemma, in MetaCoq.PCUIC.PCUICSR]
wf_context_sorts [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wf_cons_inv [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wf_universe_super [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_universe_type1 [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_global_ext [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_universe_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_ext_wk_wf [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_ext_wk [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wf_local_app_renaming [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wf_:1031 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_cs_sorts [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_ctx_universes_app [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_local_wf_ctx_universes [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_ctx_universes_subst_instance [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_decl_universes_subst_instance [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_ind_types_wf_arities [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_ind_types [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_env_check_ws_cumul_ctx [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_env_check_cumul_decl [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_env_conv [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_local_bd_rel_typing [lemma, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_bd_typing [lemma, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_local_rel [lemma, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_rel_weak [lemma, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_local_rel_subst1 [lemma, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wf_it_mkLambda_or_LetIn [lemma, in MetaCoq.Template.TypingWf]
wf_Lambda_or_LetIn [lemma, in MetaCoq.Template.TypingWf]
wf_it_mkProd_or_LetIn_inv [lemma, in MetaCoq.Template.TypingWf]
wf_lift_wf [lemma, in MetaCoq.Template.TypingWf]
wf_red1 [lemma, in MetaCoq.Template.TypingWf]
wf_projs [lemma, in MetaCoq.Template.TypingWf]
wf_ind_projs [projection, in MetaCoq.Template.TypingWf]
wf_ind_ctors_indices [projection, in MetaCoq.Template.TypingWf]
wf_ind_ctor_args [projection, in MetaCoq.Template.TypingWf]
wf_ind_ctors [projection, in MetaCoq.Template.TypingWf]
wf_ind_indices [projection, in MetaCoq.Template.TypingWf]
wf_ind_type [projection, in MetaCoq.Template.TypingWf]
wf_inductive_body [record, in MetaCoq.Template.TypingWf]
wf_case_branches_context [lemma, in MetaCoq.Template.TypingWf]
wf_case_branch_context_gen [lemma, in MetaCoq.Template.TypingWf]
wf_inds [lemma, in MetaCoq.Template.TypingWf]
wf_case_predicate_context [lemma, in MetaCoq.Template.TypingWf]
wf_extended_subst [lemma, in MetaCoq.Template.TypingWf]
wf_subst_instance_context [lemma, in MetaCoq.Template.TypingWf]
wf_lift_context [lemma, in MetaCoq.Template.TypingWf]
wf_map2_set_binder_name [lemma, in MetaCoq.Template.TypingWf]
wf_reln [lemma, in MetaCoq.Template.TypingWf]
wf_smash_context [lemma, in MetaCoq.Template.TypingWf]
wf_subst_context [lemma, in MetaCoq.Template.TypingWf]
wf_it_mkProd_or_LetIn [lemma, in MetaCoq.Template.TypingWf]
wf_decl_extends [lemma, in MetaCoq.Template.TypingWf]
wf_extends [lemma, in MetaCoq.Template.TypingWf]
wf_local_smash_context [lemma, in MetaCoq.PCUIC.PCUICContexts]
wf_local_rel_empty [lemma, in MetaCoq.PCUIC.PCUICContexts]
wf_local_smash_end [lemma, in MetaCoq.PCUIC.PCUICContexts]
wf_local_rel_smash_context [lemma, in MetaCoq.PCUIC.PCUICContexts]
wf_local_rel_smash_context_gen [lemma, in MetaCoq.PCUIC.PCUICContexts]
wf_mkApps [lemma, in MetaCoq.Erasure.EGenericMapEnv]
wf_arity_spine_typing_spine [lemma, in MetaCoq.PCUIC.PCUICSpine]
wf_arity_spine_spine [projection, in MetaCoq.PCUIC.PCUICSpine]
wf_arity_spine_wf [projection, in MetaCoq.PCUIC.PCUICSpine]
wf_arity_spine [record, in MetaCoq.PCUIC.PCUICSpine]
wf_local_alpha [lemma, in MetaCoq.PCUIC.PCUICSpine]
wf_local_rel_wf_local_bd [lemma, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wf_local_wf_local_bd [lemma, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wf_bodies:1109 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_types:1108 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_bodies:1105 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_types:1104 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_types:805 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wf':130 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf':167 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf':233 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf.Σ [variable, in MetaCoq.Erasure.EWellformed]
wf:101 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wf:128 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf:165 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf:231 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf:25 [binder, in MetaCoq.Erasure.EWellformed]
wf:31 [binder, in MetaCoq.Erasure.ErasureCorrectness]
wf:430 [binder, in MetaCoq.PCUIC.PCUICSpine]
wf:443 [binder, in MetaCoq.PCUIC.PCUICSpine]
wf:531 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wf:577 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wf:591 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wf:92 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wf:975 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΓ':276 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ':342 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ':357 [binder, in MetaCoq.Template.EnvironmentTyping]
wfΓ':433 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΓ':446 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΓ':460 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ':56 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
wfΓ:1003 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:1005 [binder, in MetaCoq.Template.Typing]
wfΓ:1007 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:1015 [binder, in MetaCoq.Template.Typing]
wfΓ:1019 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:1026 [binder, in MetaCoq.Template.Typing]
wfΓ:1033 [binder, in MetaCoq.Template.Typing]
wfΓ:104 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1040 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΓ:1042 [binder, in MetaCoq.Template.Typing]
wfΓ:1047 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:105 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:1053 [binder, in MetaCoq.Template.Typing]
wfΓ:1053 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1060 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1066 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1073 [binder, in MetaCoq.Template.Typing]
wfΓ:1086 [binder, in MetaCoq.Template.Typing]
wfΓ:109 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:1094 [binder, in MetaCoq.Template.Typing]
wfΓ:1102 [binder, in MetaCoq.Template.Typing]
wfΓ:115 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:117 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:121 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:124 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1298 [binder, in MetaCoq.Template.Typing]
wfΓ:1303 [binder, in MetaCoq.Template.Typing]
wfΓ:131 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:131 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1313 [binder, in MetaCoq.Template.Typing]
wfΓ:1317 [binder, in MetaCoq.Template.Typing]
wfΓ:1330 [binder, in MetaCoq.Template.Typing]
wfΓ:134 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:138 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:146 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:147 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:156 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:158 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:158 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:17 [binder, in MetaCoq.Examples.metacoq_tour_prelude]
wfΓ:170 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:178 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:18 [binder, in MetaCoq.Examples.typing_correctness]
wfΓ:191 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:199 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:207 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:216 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:225 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:229 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:235 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:240 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:242 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:249 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:250 [binder, in MetaCoq.Template.TypingWf]
wfΓ:251 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:258 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:268 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:27 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΓ:273 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:276 [binder, in MetaCoq.Template.TypingWf]
wfΓ:281 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:284 [binder, in MetaCoq.Template.TypingWf]
wfΓ:288 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:292 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:297 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:308 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:316 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:323 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:328 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:339 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:340 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:341 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:349 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:356 [binder, in MetaCoq.Template.EnvironmentTyping]
wfΓ:357 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:4 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΓ:42 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:440 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΓ:456 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:457 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:465 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:469 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:475 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:480 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:484 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΓ:489 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:498 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:500 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:508 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:51 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:523 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:530 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:531 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wfΓ:539 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:550 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:562 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΓ:570 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:576 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:578 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:583 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:59 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:591 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:599 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:63 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:67 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:69 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΓ:7 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΓ:713 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:717 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:72 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:75 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:76 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:775 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΓ:777 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΓ:784 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:788 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:793 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:795 [binder, in MetaCoq.Template.Typing]
wfΓ:797 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:800 [binder, in MetaCoq.Template.Typing]
wfΓ:803 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:808 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:810 [binder, in MetaCoq.Template.Typing]
wfΓ:817 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:819 [binder, in MetaCoq.Template.Typing]
wfΓ:82 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:826 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:83 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:836 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:846 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:85 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΓ:853 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:862 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:87 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:873 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:89 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:893 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:906 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:914 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:922 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:953 [binder, in MetaCoq.Template.Typing]
wfΓ:953 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:96 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΓ:964 [binder, in MetaCoq.Template.Typing]
wfΓ:968 [binder, in MetaCoq.Template.Typing]
wfΓ:97 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:974 [binder, in MetaCoq.Template.Typing]
wfΓ:979 [binder, in MetaCoq.Template.Typing]
wfΓ:98 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:983 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:987 [binder, in MetaCoq.Template.Typing]
wfΓ:994 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΓ:996 [binder, in MetaCoq.Template.Typing]
wfΔ':211 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΔ':411 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:209 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΔ:253 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΔ:261 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:267 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:408 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:461 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:809 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:87 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ':1322 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ':181 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':224 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':358 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ':364 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ':533 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':642 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':647 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ':978 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ0:484 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:486 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:492 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:494 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:496 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:498 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:579 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:584 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:10 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:10 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:10 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:100 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:100 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:1001 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:1003 [binder, in MetaCoq.Template.Typing]
wfΣ:1006 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:1008 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:101 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:101 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:1013 [binder, in MetaCoq.Template.Typing]
wfΣ:1017 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:102 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1024 [binder, in MetaCoq.Template.Typing]
wfΣ:1026 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1028 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:103 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:103 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:103 [binder, in MetaCoq.Erasure.Prelim]
wfΣ:1031 [binder, in MetaCoq.Template.Typing]
wfΣ:1039 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:104 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
wfΣ:104 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:1040 [binder, in MetaCoq.Template.Typing]
wfΣ:1048 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:105 [binder, in MetaCoq.PCUIC.PCUICValidity]
wfΣ:1051 [binder, in MetaCoq.Template.Typing]
wfΣ:1055 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:107 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:107 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:107 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1071 [binder, in MetaCoq.Template.Typing]
wfΣ:1075 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:108 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1084 [binder, in MetaCoq.Template.Typing]
wfΣ:1089 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:109 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:109 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:1092 [binder, in MetaCoq.Template.Typing]
wfΣ:1092 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:11 [binder, in MetaCoq.Erasure.ErasureProperties]
wfΣ:11 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:110 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1100 [binder, in MetaCoq.Template.Typing]
wfΣ:1100 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1108 [binder, in MetaCoq.Template.Typing]
wfΣ:111 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:1113 [binder, in MetaCoq.Template.Typing]
wfΣ:1115 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1118 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:112 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:1121 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1122 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1124 [binder, in MetaCoq.Template.Typing]
wfΣ:1124 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1124 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1129 [binder, in MetaCoq.Template.Typing]
wfΣ:1129 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:113 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:1131 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1137 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1139 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:114 [binder, in MetaCoq.Erasure.EArities]
wfΣ:114 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:114 [binder, in MetaCoq.PCUIC.PCUICValidity]
wfΣ:114 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:114 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:114 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
wfΣ:114 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:114 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:114 [binder, in MetaCoq.Erasure.Prelim]
wfΣ:115 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:1153 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:117 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:117 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1177 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1179 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:118 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:1182 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:119 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:119 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:119 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1192 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1198 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1199 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:12 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:12 [binder, in MetaCoq.Erasure.ETransform]
wfΣ:120 [binder, in MetaCoq.PCUIC.PCUICElimination]
wfΣ:120 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
wfΣ:120 [binder, in MetaCoq.PCUIC.PCUICContexts]
wfΣ:120 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:1201 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1207 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:121 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:121 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:121 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:121 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1211 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1212 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1221 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1223 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:123 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:1233 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1236 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1239 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:124 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:1241 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1242 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:1243 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1245 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1246 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1248 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1251 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1251 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1264 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1265 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1268 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1268 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1268 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1271 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1273 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1278 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:128 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:128 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1281 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1285 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1289 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:129 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:129 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1293 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1294 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1296 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1297 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:13 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:130 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:1300 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1301 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1304 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1308 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1309 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1317 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:132 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:132 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:1328 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:133 [binder, in MetaCoq.Erasure.ErasureProperties]
wfΣ:133 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1334 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1334 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:135 [binder, in MetaCoq.Erasure.EArities]
wfΣ:135 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:135 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:135 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:1359 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:136 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:136 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1365 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:137 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wfΣ:1370 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:138 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1382 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:139 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:14 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:14 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:140 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1403 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:141 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:141 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:1419 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
wfΣ:142 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:142 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:144 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:144 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:1447 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:145 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:145 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:145 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΣ:146 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:146 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1471 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1475 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:148 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:148 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:148 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:148 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wfΣ:148 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:1480 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1483 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1488 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:149 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:1492 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1496 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:150 [binder, in MetaCoq.Erasure.ErasureProperties]
wfΣ:151 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:151 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:152 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:1522 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1525 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1531 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:154 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:1540 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:1544 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:155 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:155 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:1551 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1557 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:156 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:156 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:157 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:158 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:159 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:159 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:16 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:160 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1608 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1617 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:162 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:1623 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:164 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:165 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:165 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:167 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:17 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:171 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:171 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:171 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:171 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:172 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:172 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:172 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:172 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1727 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:173 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:175 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:175 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:1754 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1759 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:176 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:176 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:176 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1765 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:177 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:177 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:177 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:1770 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:178 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:1784 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1789 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:179 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:1795 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:18 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:18 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΣ:180 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:181 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:181 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:181 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:182 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:183 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:185 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:187 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wfΣ:189 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:189 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:189 [binder, in MetaCoq.PCUIC.PCUICContexts]
wfΣ:19 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wfΣ:19 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:190 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:191 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:194 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:195 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1955 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1957 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:197 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:197 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:198 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:20 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:201 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:201 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:202 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:202 [binder, in MetaCoq.PCUIC.PCUICContexts]
wfΣ:203 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2040 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:2048 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:205 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:205 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:2056 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:207 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:207 [binder, in MetaCoq.PCUIC.PCUICContexts]
wfΣ:2076 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:208 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:208 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2092 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:2099 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:210 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:211 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:211 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2111 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:212 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:212 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:2120 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:2134 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:215 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:2167 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:217 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:218 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:219 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:219 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:221 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:222 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:223 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wfΣ:223 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:223 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:223 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:224 [binder, in MetaCoq.Erasure.EArities]
wfΣ:225 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:225 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:226 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:227 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:228 [binder, in MetaCoq.Erasure.EArities]
wfΣ:228 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:229 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:23 [binder, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:23 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:230 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:230 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:230 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:232 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:232 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:233 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:233 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:2338 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:234 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:234 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:235 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:236 [binder, in MetaCoq.Erasure.EArities]
wfΣ:238 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:238 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:238 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2399 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:24 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:24 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:240 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΣ:240 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:241 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:241 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:241 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:242 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:243 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:245 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:245 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:246 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:246 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:247 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:248 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:25 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:25 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:25 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:25 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:25 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:250 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:254 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:255 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:255 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:255 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:2551 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:256 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:256 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:256 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:257 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:257 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:259 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:26 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:26 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:260 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:261 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:261 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:261 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:263 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:263 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:263 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
wfΣ:263 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:264 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:264 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:265 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:265 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:266 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:266 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:266 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:267 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:268 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:269 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:269 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:269 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:269 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:27 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:27 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:271 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:273 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:273 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:273 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:275 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:275 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:276 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:277 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:277 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:278 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:278 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:279 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:279 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:279 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:280 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:281 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:281 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:281 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:282 [binder, in MetaCoq.Template.TypingWf]
wfΣ:283 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:284 [binder, in MetaCoq.Erasure.EArities]
wfΣ:285 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:285 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:285 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:285 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:286 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:286 [binder, in MetaCoq.Template.TypingWf]
wfΣ:287 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:287 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:288 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:288 [binder, in MetaCoq.Template.TypingWf]
wfΣ:289 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:29 [binder, in MetaCoq.PCUIC.PCUICArities]
wfΣ:29 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:29 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
wfΣ:290 [binder, in MetaCoq.Erasure.EArities]
wfΣ:291 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:291 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:291 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:293 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:295 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:295 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:295 [binder, in MetaCoq.Template.TypingWf]
wfΣ:296 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:297 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:297 [binder, in MetaCoq.Template.TypingWf]
wfΣ:299 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:299 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:3 [binder, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:3 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:3 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:3 [binder, in MetaCoq.PCUIC.PCUICInversion]
wfΣ:3 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:3 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:3 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:3 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
wfΣ:3 [binder, in MetaCoq.Erasure.ETransform]
wfΣ:3 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:3 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:3 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:3 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
wfΣ:30 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:30 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:300 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:301 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:303 [binder, in MetaCoq.Template.TypingWf]
wfΣ:304 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:304 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:305 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:306 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:307 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:308 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:31 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:31 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:31 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:31 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:315 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:318 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:32 [binder, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:32 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:32 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΣ:325 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:326 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:326 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:326 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:327 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:337 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:338 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:338 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:339 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:34 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:34 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:342 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
wfΣ:344 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:346 [binder, in MetaCoq.Erasure.EArities]
wfΣ:347 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:347 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:347 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:347 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:349 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:349 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:35 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:35 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:352 [binder, in MetaCoq.Erasure.EArities]
wfΣ:352 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:355 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:355 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:355 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:358 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:359 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:36 [binder, in MetaCoq.PCUIC.PCUICArities]
wfΣ:365 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:369 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:369 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:37 [binder, in MetaCoq.Erasure.EArities]
wfΣ:37 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΣ:371 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:371 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:371 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:377 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:38 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:38 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:38 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:38 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:38 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:380 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:381 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:381 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:384 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:385 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:389 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:39 [binder, in MetaCoq.PCUIC.PCUICElimination]
wfΣ:39 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:39 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:392 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:393 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:398 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:40 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:40 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:40 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:400 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:401 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:402 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:403 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:405 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:405 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:405 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:407 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:408 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:410 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:410 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:413 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:414 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:415 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:415 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:416 [binder, in MetaCoq.Template.EtaExpand]
wfΣ:416 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:418 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:418 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:419 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:419 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:42 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:42 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:42 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΣ:421 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:424 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:426 [binder, in MetaCoq.Template.EtaExpand]
wfΣ:426 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:430 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:433 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:433 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:434 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:434 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:436 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:438 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:4393 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:44 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:44 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:442 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:443 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wfΣ:4430 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:448 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:45 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:45 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
wfΣ:456 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:4577 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:459 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:46 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:46 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
wfΣ:460 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:460 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:461 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:462 [binder, in MetaCoq.PCUIC.PCUICNormal]
wfΣ:463 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:463 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:465 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:467 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:4670 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:47 [binder, in MetaCoq.PCUIC.PCUICArities]
wfΣ:471 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:472 [binder, in MetaCoq.PCUIC.PCUICSpine]
wfΣ:473 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:475 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:478 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:478 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:478 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:479 [binder, in MetaCoq.PCUIC.PCUICNormal]
wfΣ:48 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
wfΣ:485 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:4861 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:487 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:4870 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:488 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:4882 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:489 [binder, in MetaCoq.PCUIC.PCUICNormal]
wfΣ:49 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:49 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:49 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:49 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:490 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:491 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:491 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:492 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:492 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:494 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:496 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:497 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:497 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:499 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:5 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:501 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:502 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:502 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:503 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:506 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:506 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:508 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:5088 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:509 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:5095 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:51 [binder, in MetaCoq.PCUIC.PCUICElimination]
wfΣ:51 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:51 [binder, in MetaCoq.Erasure.EArities]
wfΣ:51 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:51 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:510 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:511 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:511 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:514 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:515 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:515 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:517 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:518 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:519 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5195 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:52 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:52 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:520 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:5203 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:521 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:521 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:521 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:5211 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5225 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:524 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:527 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:528 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:528 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:528 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:53 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:530 [binder, in MetaCoq.Template.EtaExpand]
wfΣ:532 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:532 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:534 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:535 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:536 [binder, in MetaCoq.Template.EtaExpand]
wfΣ:537 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:538 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:538 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:54 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:546 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:548 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:55 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:550 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:553 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:554 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:558 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:56 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:5604 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:562 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:5644 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:565 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:565 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:5651 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5664 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5675 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:568 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:569 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:5690 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5694 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5697 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:57 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:57 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:57 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:57 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:5705 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:571 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:572 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:572 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:577 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:58 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:58 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:58 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:58 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:581 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:582 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:584 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:585 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:589 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:589 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:589 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:59 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:59 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:590 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:591 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:593 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:597 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:6 [binder, in MetaCoq.Erasure.ETransform]
wfΣ:6 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:60 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:601 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:605 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:607 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:608 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:608 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:608 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:610 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:614 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:616 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:617 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:618 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:619 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:62 [binder, in MetaCoq.Erasure.EArities]
wfΣ:620 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:621 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:625 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:626 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:626 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:628 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:63 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:63 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:631 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:631 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:632 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:635 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:636 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:638 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:638 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:639 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:640 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:641 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:642 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:645 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:646 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:647 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:647 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:647 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:649 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:65 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:65 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:650 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:653 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:653 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:654 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:655 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:658 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:659 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:66 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:662 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:665 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:667 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:667 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:667 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:668 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:668 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:67 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:67 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:671 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:674 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:678 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:678 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:68 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:68 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:68 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
wfΣ:681 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:684 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:69 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:690 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:691 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:695 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:696 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:696 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:696 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:70 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:70 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:70 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:701 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:701 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:702 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:703 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:705 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:707 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:708 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:71 [binder, in MetaCoq.Erasure.EArities]
wfΣ:711 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:711 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:712 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:716 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:717 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:721 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:724 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:725 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:725 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:727 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:729 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:73 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:73 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:732 [binder, in MetaCoq.Template.EnvironmentTyping]
wfΣ:735 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:735 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:736 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:738 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:738 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:74 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:74 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:740 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:743 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:749 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:749 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:75 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:76 [binder, in MetaCoq.Erasure.EArities]
wfΣ:76 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
wfΣ:762 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:763 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:765 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:768 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:77 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:771 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:772 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:775 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:778 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:78 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:783 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:786 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:787 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:788 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:79 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:791 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:791 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:795 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:795 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:798 [binder, in MetaCoq.Template.Typing]
wfΣ:799 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:8 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:8 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:8 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:8 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:80 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:80 [binder, in MetaCoq.PCUIC.PCUICInductives]
wfΣ:800 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:801 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:803 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:806 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:807 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:808 [binder, in MetaCoq.Template.Typing]
wfΣ:808 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:81 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:81 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:810 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:811 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:815 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:817 [binder, in MetaCoq.Template.Typing]
wfΣ:82 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:82 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:82 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:824 [binder, in MetaCoq.Template.Typing]
wfΣ:824 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:824 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:825 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:83 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:83 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:831 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:832 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:832 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:834 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:834 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:837 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:84 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:84 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:843 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:843 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:844 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:848 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:848 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:85 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:851 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:853 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:854 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:854 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:859 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:86 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:860 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:862 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:865 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:865 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:869 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:87 [binder, in MetaCoq.Erasure.EArities]
wfΣ:87 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:87 [binder, in MetaCoq.Erasure.Prelim]
wfΣ:87 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:870 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:871 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:871 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:875 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:875 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:879 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:88 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:88 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:880 [binder, in MetaCoq.PCUIC.PCUICSR]
wfΣ:882 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:886 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:887 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:888 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:89 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:89 [binder, in MetaCoq.PCUIC.PCUICConversion]
wfΣ:891 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:892 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:894 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:9 [binder, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:9 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:9 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:90 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:90 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:90 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:90 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:90 [binder, in MetaCoq.Erasure.Prelim]
wfΣ:90 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:900 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:904 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:904 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:905 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:91 [binder, in MetaCoq.PCUIC.PCUICValidity]
wfΣ:91 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:910 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:912 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:913 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:92 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:92 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:920 [binder, in MetaCoq.PCUIC.PCUICTyping]
wfΣ:921 [binder, in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:925 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:927 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:93 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:93 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:936 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:938 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:94 [binder, in MetaCoq.PCUIC.PCUICProgress]
wfΣ:94 [binder, in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:94 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:945 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:945 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:95 [binder, in MetaCoq.Erasure.ESubstitution]
wfΣ:95 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:95 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:95 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:95 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:955 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:956 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:96 [binder, in MetaCoq.Erasure.EArities]
wfΣ:96 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:96 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:962 [binder, in MetaCoq.Template.Typing]
wfΣ:966 [binder, in MetaCoq.Template.Typing]
wfΣ:966 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:97 [binder, in MetaCoq.PCUIC.PCUICValidity]
wfΣ:97 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:97 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:97 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:97 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:972 [binder, in MetaCoq.Template.Typing]
wfΣ:973 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:977 [binder, in MetaCoq.Template.Typing]
wfΣ:977 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:98 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:98 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:982 [binder, in MetaCoq.Erasure.ErasureFunction]
wfΣ:985 [binder, in MetaCoq.Template.Typing]
wfΣ:989 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:994 [binder, in MetaCoq.Template.Typing]
wGraph [module, in MetaCoq.Template.common.uGraph]
wGraph [library]
wguard:39 [binder, in MetaCoq.Erasure.ETransform]
whiskerL [definition, in MetaCoq.Translations.MiniHoTT]
whiskerL [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerL_pVL [definition, in MetaCoq.Translations.MiniHoTT]
whiskerL_VpL [definition, in MetaCoq.Translations.MiniHoTT]
whiskerL_pp [definition, in MetaCoq.Translations.MiniHoTT]
whiskerL_1p_1 [definition, in MetaCoq.Translations.MiniHoTT]
whiskerL_1p [definition, in MetaCoq.Translations.MiniHoTT]
whiskerL_p1 [definition, in MetaCoq.Translations.MiniHoTT]
whiskerL_pVL [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerL_VpL [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerL_pp [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerL_1p_1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerL_1p [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerL_p1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerR [definition, in MetaCoq.Translations.MiniHoTT]
whiskerR [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerR_VpR [definition, in MetaCoq.Translations.MiniHoTT]
whiskerR_pVR [definition, in MetaCoq.Translations.MiniHoTT]
whiskerR_pp [definition, in MetaCoq.Translations.MiniHoTT]
whiskerR_p1_1 [definition, in MetaCoq.Translations.MiniHoTT]
whiskerR_1p [definition, in MetaCoq.Translations.MiniHoTT]
whiskerR_p1 [definition, in MetaCoq.Translations.MiniHoTT]
whiskerR_VpR [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerR_pVR [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerR_pp [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerR_p1_1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerR_1p [definition, in MetaCoq.Translations.MiniHoTT_paths]
whiskerR_p1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
whne [inductive, in MetaCoq.Template.Normal]
whne [inductive, in MetaCoq.PCUIC.PCUICNormal]
whne_conv_context [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
whne_All2_fold [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
whne_proj [constructor, in MetaCoq.Template.Normal]
whne_case [constructor, in MetaCoq.Template.Normal]
whne_app [constructor, in MetaCoq.Template.Normal]
whne_const [constructor, in MetaCoq.Template.Normal]
whne_evar [constructor, in MetaCoq.Template.Normal]
whne_var [constructor, in MetaCoq.Template.Normal]
whne_rel [constructor, in MetaCoq.Template.Normal]
whne_eq_term_upto_univ_napp [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_red1_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_pres [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_pres1 [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_red1_ind [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_red1_ind [section, in MetaCoq.PCUIC.PCUICNormal]
whne_isConstruct_app [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_dec [definition, in MetaCoq.PCUIC.PCUICNormal]
whne_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_mkApps [lemma, in MetaCoq.PCUIC.PCUICNormal]
whne_proj_noiota [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_proj [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_case_noiota [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_case [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_fix_nofix [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_fixapp [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_app [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_const_nodelta [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_const [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_letin_nozeta [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_evar [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_var [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_lam_nobeta [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_rel_nozeta [constructor, in MetaCoq.PCUIC.PCUICNormal]
whne_rel [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf [inductive, in MetaCoq.Template.Normal]
whnf [inductive, in MetaCoq.PCUIC.PCUICNormal]
whnf_conv_context [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
whnf_All2_fold [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
whnf_cofix [constructor, in MetaCoq.Template.Normal]
whnf_fix [constructor, in MetaCoq.Template.Normal]
whnf_indapp [constructor, in MetaCoq.Template.Normal]
whnf_cstrapp [constructor, in MetaCoq.Template.Normal]
whnf_lam [constructor, in MetaCoq.Template.Normal]
whnf_prod [constructor, in MetaCoq.Template.Normal]
whnf_sort [constructor, in MetaCoq.Template.Normal]
whnf_ne [constructor, in MetaCoq.Template.Normal]
whnf_eq_term [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_eq_term_upto_univ_napp [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_isApp [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red1_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_trans [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_refl [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_refl_whne [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps_r_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps_l_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_mkApps [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_red [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tCoFix [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tInd [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tConstruct [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tLambda [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tProd [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tSort [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tProj [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tCase [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tFix [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tApp [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tConst [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tEvar [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tVar [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_tRel [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red [inductive, in MetaCoq.PCUIC.PCUICNormal]
whnf_pres [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_pres1 [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_tLambda_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_tProd_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_tSort_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_dec [definition, in MetaCoq.PCUIC.PCUICNormal]
whnf_whne_dec [definition, in MetaCoq.PCUIC.PCUICNormal]
whnf_whne_nodelta_upgrade [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_fixapp' [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_mkApps [lemma, in MetaCoq.PCUIC.PCUICNormal]
whnf_cofixapp [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_fixapp [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_indapp [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_cstrapp [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_lam [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_prod [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_sort [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_ne [constructor, in MetaCoq.PCUIC.PCUICNormal]
whnf_red_isIndConstructApp [lemma, in MetaCoq.PCUIC.PCUICConvCumInversion]
whnf_proj_arg_whne [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_case_arg_whne [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_fix_arg_whne [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_non_cofix_ind_typed [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_non_ctor_finite_ind_typed [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
whnf_ind_finite [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wh_normal_ind_discr [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wh_neutral_empty [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wh_neutral_empty_gen [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wh_normal [abbreviation, in MetaCoq.PCUIC.PCUICCanonicity]
wh_neutral [abbreviation, in MetaCoq.PCUIC.PCUICCanonicity]
with_constructor_as_block [projection, in MetaCoq.Erasure.EWcbvEval]
with_guarded_fix [projection, in MetaCoq.Erasure.EWcbvEval]
with_prop_case [projection, in MetaCoq.Erasure.EWcbvEval]
with_universes:155 [binder, in MetaCoq.Template.Pretty]
with_universes:152 [binder, in MetaCoq.Template.Pretty]
with_universes:147 [binder, in MetaCoq.Template.Pretty]
with_universes:143 [binder, in MetaCoq.Template.Pretty]
with_universes:133 [binder, in MetaCoq.Template.Pretty]
with_universes:128 [binder, in MetaCoq.Template.Pretty]
with_universes:120 [binder, in MetaCoq.Template.Pretty]
with_universes:53 [binder, in MetaCoq.Template.Pretty]
wi':124 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':134 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':161 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':171 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':210 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':237 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':73 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':99 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:122 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:132 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:1467 [binder, in MetaCoq.Erasure.ErasureFunction]
wi:159 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:169 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:18 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:208 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:235 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:71 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:97 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
WN [lemma, in MetaCoq.PCUIC.PCUICProgress]
wrap_error [definition, in MetaCoq.SafeChecker.PCUICErrors]
wrap_error [definition, in MetaCoq.Template.Checker]
wrong_sizes:104 [binder, in MetaCoq.Template.monad_utils]
ws_wcbv_standardization [lemma, in MetaCoq.PCUIC.PCUICProgress]
ws_empty [definition, in MetaCoq.PCUIC.PCUICProgress]
ws_cumul_pb_zippx [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
ws_cumul_ctx_pb_app [lemma, in MetaCoq.PCUIC.PCUICArities]
ws_cumul_ctx_pb_vass [lemma, in MetaCoq.PCUIC.PCUICArities]
ws_cumul_ctx_pb_wf_local [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_inst_variance [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_Prod_Prod_inv_l [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_subst [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_inv [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_eq [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_terms_confl [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_mkApps_tRel [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_ctx_pb_rel_context_assumptions [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
ws_cumul_pb_LetIn_l_inv_alt [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
ws_cumul_pb_it_mkProd_or_LetIn_smash [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_pb_expand_lets [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ws_cumul_ctx_pb_refl [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_forget [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_sym [instance, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_inv [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_left [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb_closed_right [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_ctx_pb [definition, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_trans [instance, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_inv [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_cumul_pb_decls [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_right [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls_wf_decl_left [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_decls [definition, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_decl [abbreviation, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt_closed [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_trans [instance, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_conv [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget_cumul [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_forget [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_alt [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_right [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term_left [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_closed_context [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_is_open_term [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_sym [instance, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_refl' [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_red_r [constructor, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_red_l [constructor, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb_compare [constructor, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_cumul_pb [inductive, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
ws_red_confluence [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred_pred [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred_curry_red [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_refl_irrel [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_irrel [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_red_ctx [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_red_ctx_aux [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_red [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_ctx_length [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_ctx_trans [instance, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_ctx_refl [instance, in MetaCoq.PCUIC.PCUICConfluence]
ws_pair_eq_ctx [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_term_eq [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred1_ctx [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_red_ctx [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_red1_ctx [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred1_diamond [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred1_red [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred_ws_pred_curry [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red1_pred1 [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_red1_pred1_curry [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred_curry [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred1 [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_pred1_curry [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_pair_term [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_pair_context [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_pair [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_red [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_red1 [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_context_on_free_vars_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_context_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_context_on_free_vars [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_context_proj' [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_context_proj [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_context [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_term_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
ws_term_prop [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_term_proj [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_term [definition, in MetaCoq.PCUIC.PCUICConfluence]
ws_cumul_pb_Construct [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Evar [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_subst [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_weaken [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_conv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_red [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_ws_cumul_ctx [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_alt [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_rel_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_rel_app [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_rel [definition, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_elim [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_substs_red [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_ty [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_tm [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps_weak [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkProd_or_LetIn_codom [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_it_mkLambda_or_LetIn_codom [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_bo [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_r [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Lambda_l [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_eq_le_gen [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_CoFix [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Fix [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_or_cofix [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_bodies [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_body [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_types [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_fix_one_type [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_brs [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_one_brs [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_c [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Case_p [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_App [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Proj_c [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_mkApps [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_App_r [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_App_l [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_brs [definition, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_predicate [definition, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_r_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_right [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_open_terms_left [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Ind_l_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_r_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_LetIn_l_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_red_l_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_red_r_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Prod_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_r_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_r_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_l_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_Sort_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_Prod_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Sort_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_Prod_l [lemma, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_sym [instance, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_trans [instance, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms_Proper [instance, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_pb_terms [abbreviation, in MetaCoq.PCUIC.PCUICConversion]
ws_cumul_ctx_pb_app_same [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_refl [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_true_forget [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_false_forget [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_trans [instance, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_decls_ws_cumul_ctx [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx_inv [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_le [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_ws_cumul_ctx [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_ctx_pb_red [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx_inv [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_eq_context_upto [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context_inv [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_compare_context [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red_ctx [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_red [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
ws_cumul_pb_terms_refl [lemma, in MetaCoq.PCUIC.PCUICSR]
ws_cumul_pb_terms_eq_trans [lemma, in MetaCoq.PCUIC.PCUICSR]
ws_cumul_pb_eq_trans [lemma, in MetaCoq.PCUIC.PCUICSR]
ws_cumul_pb_meta_refl [lemma, in MetaCoq.PCUIC.PCUICSR]
ws_cumul_ctx_pb_rel_trans [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_ws_cumul_ctx [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_length [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_ws_cumul_ctx [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_smash [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_conv_extended_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_eq_le [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_le_le [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_le_le [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_terms_lift [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_pb_expand_lets_k [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_context_assumptions [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel'_context_assumptions [lemma, in MetaCoq.PCUIC.PCUICSpine]
ws_cumul_ctx_pb_rel_cons [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
wt [definition, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
WtContextConversion [section, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wtcumul [section, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wtcumul [section, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wtcumul' [section, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
_ ;;; _ | _ |-- _ <=[ _ ] _ (type_scope) [notation, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
_ ;;; _ |-- _ <= _ (type_scope) [notation, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
_ ;;; _ |-- _ <=[ _ ] _ (type_scope) [notation, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wtd':279 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wtd:276 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wterm [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
wth [projection, in MetaCoq.SafeChecker.PCUICSafeConversion]
wtp [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
wtp:10 [binder, in MetaCoq.PCUIC.PCUICTransform]
wtp:1295 [binder, in MetaCoq.Erasure.ErasureFunction]
wtp:1406 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wtp:1524 [binder, in MetaCoq.Erasure.ErasureFunction]
wtp:18 [binder, in MetaCoq.Erasure.ETransform]
wtp:22 [binder, in MetaCoq.Erasure.ETransform]
wtsub [section, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wtsub [section, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wts':495 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wts:492 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wt_cumul_red_r [constructor, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_cumul_red_l [constructor, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_cumul_refl [constructor, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_cumul [inductive, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_red1_codom [projection, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_red1_dom [projection, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_red1_red1 [projection, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_red1 [record, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_inv [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_subterm [definition, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt_cumul_pb_equalityP [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_red_r [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_red_l [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_refl [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
wt_conv_conv [definition, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_cum [definition, in MetaCoq.PCUIC.PCUICSubstitution]
wt_conv [definition, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul [definition, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_pb_eq [projection, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_pb_codom [projection, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_pb_dom [projection, in MetaCoq.PCUIC.PCUICSubstitution]
wt_cumul_pb [record, in MetaCoq.PCUIC.PCUICSubstitution]
wt_template_program [definition, in MetaCoq.Template.TemplateProgram]
wt_ind_app_variance [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
wt_closed [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_expand_lets [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_subst_instance [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_convSpec_convAlgo [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_conv_hetero [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_hetero [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero_inv [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_r' [constructor, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_l' [constructor, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_refl' [constructor, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_hetero [inductive, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ctx_rel [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb_ctx [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_conv [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_r [constructor, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_red_l [constructor, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_refl [constructor, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cumul_pb [inductive, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_codom [projection, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_dom [projection, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_red1 [projection, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1 [record, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red1_wt [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_on_free_vars [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_inv [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_subterm [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_red [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_wf_local [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt_cum_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wt_cum_ws_cumul_pb [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wt_ws_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_ctx_pb_forget [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_decl [definition, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_conv_context [abbreviation, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_context [abbreviation, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_ctx_pb [definition, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_vdef [constructor, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_vass [constructor, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_decls [inductive, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_trans [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_cumul_pb_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wt_zip_mkapps [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
wt_closed_red_refl [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
wt_pcuic_program [definition, in MetaCoq.PCUIC.PCUICProgram]
wt_closed_red1 [lemma, in MetaCoq.PCUIC.PCUICSR]
wt_terms_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICSR]
wt_cumul_pb_refl [lemma, in MetaCoq.PCUIC.PCUICSR]
wt_cstrs [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
wt_indices [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
wt_terms [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
wt_params:1087 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
wt_brs [abbreviation, in MetaCoq.SafeChecker.PCUICTypeChecker]
wt_decl [definition, in MetaCoq.SafeChecker.PCUICTypeChecker]
wt':1388 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':1410 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':314 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wt':464 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':470 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':474 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':479 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':483 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':487 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':493 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':498 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':504 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':509 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':514 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':520 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':525 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':531 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':536 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':541 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':689 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':702 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':712 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':720 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':725 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':731 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':736 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':741 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':747 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':752 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':758 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':763 [binder, in MetaCoq.Erasure.ErasureFunction]
wt':768 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1048 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1050 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1055 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1057 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1072 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1074 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1080 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1083 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1104 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1144 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1160 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1171 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1202 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1214 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1226 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:126 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1313 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1328 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1345 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1365 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1385 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:1407 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:149 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt:1542 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wt:1543 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:160 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:1606 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
wt:163 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:170 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:238 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt:312 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wt:463 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:469 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:473 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:478 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:482 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:486 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:490 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:502 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:512 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:517 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:523 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:543 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wt:546 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:552 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:557 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:561 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
wt:563 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:573 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:578 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:602 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:606 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:633 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:688 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:701 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:711 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:717 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:744 [binder, in MetaCoq.Erasure.ErasureFunction]
wt:8 [binder, in MetaCoq.Erasure.ETransform]
wt:81 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:956 [binder, in MetaCoq.Erasure.ErasureFunction]
wUnivalence [definition, in MetaCoq.Translations.times_bool_fun]
w':446 [binder, in MetaCoq.PCUIC.PCUICTyping]
w':921 [binder, in MetaCoq.Template.Typing]
w1:126 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w1:144 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w1:158 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w1:2800 [binder, in MetaCoq.Translations.MiniHoTT]
w1:2808 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w2:127 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w2:145 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w2:159 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w2:2803 [binder, in MetaCoq.Translations.MiniHoTT]
w2:2811 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:1006 [binder, in MetaCoq.Template.utils.wGraph]
w:1009 [binder, in MetaCoq.Template.utils.wGraph]
w:1262 [binder, in MetaCoq.Translations.MiniHoTT]
w:1270 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:219 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
w:229 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
w:2578 [binder, in MetaCoq.Template.utils.All_Forall]
w:2791 [binder, in MetaCoq.Translations.MiniHoTT]
w:2799 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:2823 [binder, in MetaCoq.Translations.MiniHoTT]
w:2831 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:2856 [binder, in MetaCoq.Translations.MiniHoTT]
w:2864 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:31 [binder, in MetaCoq.Template.utils.MCRelations]
w:337 [binder, in MetaCoq.Template.EnvironmentTyping]
w:343 [binder, in MetaCoq.Template.EnvironmentTyping]
w:347 [binder, in MetaCoq.Template.EnvironmentTyping]
w:36 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
w:375 [binder, in MetaCoq.Template.EnvironmentTyping]
w:443 [binder, in MetaCoq.PCUIC.PCUICTyping]
w:445 [binder, in MetaCoq.Translations.MiniHoTT]
w:45 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
w:453 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:458 [binder, in MetaCoq.Translations.MiniHoTT]
w:466 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:49 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
w:533 [binder, in MetaCoq.Translations.MiniHoTT]
w:541 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:546 [binder, in MetaCoq.Translations.MiniHoTT]
w:554 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:566 [binder, in MetaCoq.Translations.MiniHoTT]
w:574 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:577 [binder, in MetaCoq.Translations.MiniHoTT]
w:585 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:588 [binder, in MetaCoq.Translations.MiniHoTT]
w:596 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:60 [binder, in MetaCoq.Template.WfAst]
w:606 [binder, in MetaCoq.Translations.MiniHoTT]
w:614 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:65 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w:67 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w:740 [binder, in MetaCoq.Translations.MiniHoTT]
w:748 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:75 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w:79 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
w:799 [binder, in MetaCoq.Translations.MiniHoTT]
w:807 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:886 [binder, in MetaCoq.Translations.MiniHoTT]
w:894 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:918 [binder, in MetaCoq.Template.Typing]
w:92 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
w:926 [binder, in MetaCoq.Translations.MiniHoTT]
w:934 [binder, in MetaCoq.Translations.MiniHoTT_paths]
w:96 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
| 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) |