| 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) |
G
gamma:511 [binder, in MetaCoq.Examples.tauto]Gamma:513 [binder, in MetaCoq.Examples.tauto]
GC [section, in MetaCoq.Template.common.uGraph]
GcOfConstraint [section, in MetaCoq.Template.common.uGraph]
GCS [module, in MetaCoq.Template.common.uGraph]
gcstrs:170 [binder, in MetaCoq.Template.common.uGraph]
gcs_elements_union [lemma, in MetaCoq.Template.common.uGraph]
gcs_levels_declared [definition, in MetaCoq.Template.common.uGraph]
GCS_pair_spec [lemma, in MetaCoq.Template.common.uGraph]
GCS_For_all_Proper [instance, in MetaCoq.Template.common.uGraph]
gcs_equal [definition, in MetaCoq.Template.common.uGraph]
gcs_equal [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
gcs:503 [binder, in MetaCoq.Template.common.uGraph]
gcs:511 [binder, in MetaCoq.Template.common.uGraph]
gcs:626 [binder, in MetaCoq.Template.common.uGraph]
gcs:644 [binder, in MetaCoq.Template.common.uGraph]
gcs:646 [binder, in MetaCoq.Template.common.uGraph]
gcs:651 [binder, in MetaCoq.Template.common.uGraph]
gcs:653 [binder, in MetaCoq.Template.common.uGraph]
gctx [definition, in MetaCoq.Examples.typing_correctness]
gctx [definition, in MetaCoq.Examples.metacoq_tour_prelude]
gctx_wf_env [definition, in MetaCoq.Examples.typing_correctness]
gctx_union [definition, in MetaCoq.Template.common.uGraph]
gctx_wf_env [definition, in MetaCoq.Examples.metacoq_tour_prelude]
gctx':714 [binder, in MetaCoq.Template.common.uGraph]
gctx1:675 [binder, in MetaCoq.Template.common.uGraph]
gctx2:676 [binder, in MetaCoq.Template.common.uGraph]
gctx:167 [binder, in MetaCoq.Template.common.uGraph]
gctx:717 [binder, in MetaCoq.Template.common.uGraph]
gc_of_uctx_levels [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraints_proper [instance, in MetaCoq.Template.common.uGraph]
gc_of_uctx_union [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraints_union [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraintsP [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraints_none [constructor, in MetaCoq.Template.common.uGraph]
gc_of_constraints_ok [constructor, in MetaCoq.Template.common.uGraph]
gc_of_constraints_view [inductive, in MetaCoq.Template.common.uGraph]
gc_result_eq [definition, in MetaCoq.Template.common.uGraph]
gc_of_constraints_declared [lemma, in MetaCoq.Template.common.uGraph]
gc_levels_declared' [definition, in MetaCoq.Template.common.uGraph]
gc_eq_universe [definition, in MetaCoq.Template.common.uGraph]
gc_leq_universe [definition, in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_n_sup [lemma, in MetaCoq.Template.common.uGraph]
gc_levels_declared_univ [definition, in MetaCoq.Template.common.uGraph]
gc_levels_declared [definition, in MetaCoq.Template.common.uGraph]
gc_expr_declared [definition, in MetaCoq.Template.common.uGraph]
gc_level_declared_make_graph [lemma, in MetaCoq.Template.common.uGraph]
gc_level_declared [definition, in MetaCoq.Template.common.uGraph]
gc_of_uctx_invariants [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraint_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraints_of_uctx [lemma, in MetaCoq.Template.common.uGraph]
gc_of_uctx_of_constraints [lemma, in MetaCoq.Template.common.uGraph]
gc_of_uctx [definition, in MetaCoq.Template.common.uGraph]
gc_eq_levelalg_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_leq_levelalg_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_leq_levelalg_n_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_eq0_levelalg_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_n_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_lt_levelalg [definition, in MetaCoq.Template.common.uGraph]
gc_leq_levelalg [definition, in MetaCoq.Template.common.uGraph]
gc_lt0_levelalg [definition, in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg [definition, in MetaCoq.Template.common.uGraph]
gc_eq_levelalg [definition, in MetaCoq.Template.common.uGraph]
gc_eq0_levelalg [definition, in MetaCoq.Template.common.uGraph]
gc_leq_levelalg_n [definition, in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_n [definition, in MetaCoq.Template.common.uGraph]
gc_consistent_iff [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraints_spec [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraints [definition, in MetaCoq.Template.common.uGraph]
gc_of_constraint_spec [lemma, in MetaCoq.Template.common.uGraph]
gc_satisfies_singleton [lemma, in MetaCoq.Template.common.uGraph]
gc_of_constraint [definition, in MetaCoq.Template.common.uGraph]
gc_satisfies_pair [lemma, in MetaCoq.Template.common.uGraph]
gc_consistent [definition, in MetaCoq.Template.common.uGraph]
gc_satisfies [definition, in MetaCoq.Template.common.uGraph]
gc_satisfies0 [abbreviation, in MetaCoq.Template.common.uGraph]
gc_of_constraints_proper [instance, in MetaCoq.SafeChecker.PCUICSafeChecker]
gc1:662 [binder, in MetaCoq.Template.common.uGraph]
gc1:86 [binder, in MetaCoq.Template.common.uGraph]
gc2:663 [binder, in MetaCoq.Template.common.uGraph]
gc2:87 [binder, in MetaCoq.Template.common.uGraph]
gc:111 [binder, in MetaCoq.Template.common.uGraph]
gc:113 [binder, in MetaCoq.Template.common.uGraph]
gc:160 [binder, in MetaCoq.Template.common.uGraph]
gc:174 [binder, in MetaCoq.Template.common.uGraph]
gc:190 [binder, in MetaCoq.Template.common.uGraph]
gc:213 [binder, in MetaCoq.Template.common.uGraph]
gc:216 [binder, in MetaCoq.Template.common.uGraph]
gc:219 [binder, in MetaCoq.Template.common.uGraph]
gc:438 [binder, in MetaCoq.Template.common.uGraph]
gc:441 [binder, in MetaCoq.Template.common.uGraph]
gc:501 [binder, in MetaCoq.Template.common.uGraph]
gc:508 [binder, in MetaCoq.Template.common.uGraph]
gc:514 [binder, in MetaCoq.Template.common.uGraph]
gc:516 [binder, in MetaCoq.Template.common.uGraph]
gc:518 [binder, in MetaCoq.Template.common.uGraph]
gc:521 [binder, in MetaCoq.Template.common.uGraph]
gc:624 [binder, in MetaCoq.Template.common.uGraph]
gc:642 [binder, in MetaCoq.Template.common.uGraph]
gc:664 [binder, in MetaCoq.Template.common.uGraph]
gc:69 [binder, in MetaCoq.Template.common.uGraph]
Generation [section, in MetaCoq.PCUIC.PCUICGeneration]
genv:33 [binder, in MetaCoq.Template.EnvMap]
genv:35 [binder, in MetaCoq.Template.EnvMap]
gen_transform_env_wf [lemma, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_decl_wf [lemma, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_wellformed_decl_irrel [lemma, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_wellformed_irrel [lemma, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_env_eq [lemma, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_env_extends' [lemma, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_env' [definition, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_env [definition, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_decl [definition, in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_constant_decl [definition, in MetaCoq.Erasure.EGenericMapEnv]
gen_compare_global_instance':365 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:364 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:348 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:334 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:318 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance':265 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:264 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:225 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:207 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:151 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:124 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:38 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
get_is_level_correct [lemma, in MetaCoq.Template.Universes]
get_level_make [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
get_wt_indices [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
give [abbreviation, in MetaCoq.SafeChecker.PCUICSafeReduce]
givePr [abbreviation, in MetaCoq.SafeChecker.PCUICSafeReduce]
givePr' [abbreviation, in MetaCoq.SafeChecker.PCUICSafeReduce]
Global [constructor, in MetaCoq.Template.TemplateMonad.Common]
GlobalContextMap [module, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.constructor_isprop_pars_decl_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.constructor_isprop_pars_decl [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.global_decls [projection, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_env_spec [lemma, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_env [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.make [definition, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.map [projection, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.repr [projection, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.t [record, in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.wf [projection, in MetaCoq.Erasure.EEnvMap]
GlobalMaps [module, in MetaCoq.Template.EnvironmentTyping]
GlobalMapsSig [module, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.check_ind_sorts [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.check_constructors_smaller [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.constructor_univs [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_eq [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_args_length [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_concl [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_concl_head [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_respects_variance [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.elim_sort_sprop_ind [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.elim_sort_prop_ind [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.fresh_global [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.GlobalMaps [section, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.globenv_decl [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.globenv_nil [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_sorts [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_cunivs [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_arity_eq [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_respects_variance [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_arities [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_realargs [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.level_var_instance [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_constraints [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_constraint [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_instance [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_level [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onArity [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onConstructors [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onIndices [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onInductives [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onNpars [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onParams [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onProjections [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.onVariance [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_env_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_env_ext [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_env [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_univs [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_decls [inductive, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_decl [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_constant_decl [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_inductive [record, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_variance [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_ind_body [record, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projs [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projs_all [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projs_elim [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projs_noidx [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projs_record [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projections [record, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projection [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_proj_relevance [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_proj_type [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_proj_name [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_proj [record, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_constructors [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_lets_in_type [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_ctype_variance [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_ctype_positive [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_cindices [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_cargs [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_ctype [projection, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_constructor [record, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_udecl [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_type [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_context [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_ass [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_let [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_concl [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr [inductive, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_ass [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_let [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_concl [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_arg_closed [constructor, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.positive_cstr_arg [inductive, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.satisfiable_udecl [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.sorts_local_ctx_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.sorts_local_ctx [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.type_local_ctx_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.type_local_ctx [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.univs_ext_constraints [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.valid_on_mono_udecl [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.variance_universes [definition, in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.variance_cstrs [definition, in MetaCoq.Template.EnvironmentTyping]
globals_erased_with_deps [definition, in MetaCoq.Erasure.EDeps]
global_levels:80 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_levels_sub [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_levels_union_set [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_ext_constraints_app [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_ext_constraints_trans [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_ext_levels_trans [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_constraints_trans [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_levels_trans [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_variance_napp_mon [lemma, in MetaCoq.Template.TermEquality]
global_variance [definition, in MetaCoq.Template.TermEquality]
global_variance_sigma_mon [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
global_levels:469 [binder, in MetaCoq.Template.EnvironmentTyping]
global_uctx_graph_invariants [lemma, in MetaCoq.Template.common.uGraph]
global_gc_uctx_invariants [definition, in MetaCoq.Template.common.uGraph]
global_uctx_invariants [definition, in MetaCoq.Template.common.uGraph]
global_variance_empty [lemma, in MetaCoq.PCUIC.PCUICEquality]
global_variance_napp_mon [lemma, in MetaCoq.PCUIC.PCUICEquality]
global_variance [definition, in MetaCoq.PCUIC.PCUICEquality]
global_reference [inductive, in MetaCoq.Template.Kernames]
global_env_add [definition, in MetaCoq.SafeChecker.PCUICConsistency]
global_erased_with_deps_weaken_prefix [lemma, in MetaCoq.Erasure.ErasureFunction]
global_env_ind [lemma, in MetaCoq.Erasure.ErasureFunction]
global_erases_with_deps_weaken [lemma, in MetaCoq.Erasure.ErasureFunction]
global_erases_with_deps_cons [lemma, in MetaCoq.Erasure.ErasureFunction]
global_erased_with_deps [definition, in MetaCoq.Erasure.ErasureFunction]
global_context [abbreviation, in MetaCoq.Erasure.EAst]
global_declarations [definition, in MetaCoq.Erasure.EAst]
global_decl [inductive, in MetaCoq.Erasure.EAst]
global_ext_uctx_consistent [definition, in MetaCoq.PCUIC.PCUICGlobalEnv]
global_ext_constraints_nlg [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
global_ext_levels_nlg [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
global_variance_nl_sigma_mon [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
global_declarations_size [definition, in MetaCoq.PCUIC.PCUICTyping]
global_subset_cons_right [lemma, in MetaCoq.Erasure.EExtends]
global_subset_cons [lemma, in MetaCoq.Erasure.EExtends]
global_subset_In [lemma, in MetaCoq.Erasure.EExtends]
global_subset [definition, in MetaCoq.Erasure.EExtends]
global_env_ext_map_global_env_map [definition, in MetaCoq.PCUIC.PCUICProgram]
global_env_ext_map_global_env_ext [definition, in MetaCoq.PCUIC.PCUICProgram]
global_env_ext_map [definition, in MetaCoq.PCUIC.PCUICProgram]
global_env_map [record, in MetaCoq.PCUIC.PCUICProgram]
global_context_set_sub_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_context_set [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_ext_context_set [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_uctx_univs [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
global_levels:81 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
global_uctx_invariants_ext [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
globdecls_size [definition, in MetaCoq.Template.Typing]
globenv_size [definition, in MetaCoq.Template.Typing]
globenv_size [definition, in MetaCoq.PCUIC.PCUICTyping]
Gl:793 [binder, in MetaCoq.Template.utils.wGraph]
Gl:799 [binder, in MetaCoq.Template.utils.wGraph]
Gl:805 [binder, in MetaCoq.Template.utils.wGraph]
Gl:808 [binder, in MetaCoq.Template.utils.wGraph]
Gl:813 [binder, in MetaCoq.Template.utils.wGraph]
Gl:990 [binder, in MetaCoq.Template.utils.wGraph]
goal:1 [binder, in MetaCoq.Examples.constructor_tac]
GoodConstraint [module, in MetaCoq.Template.common.uGraph]
GoodConstraintSet [module, in MetaCoq.Template.common.uGraph]
GoodConstraintSetDecide [module, in MetaCoq.Template.common.uGraph]
GoodConstraintSetFact [module, in MetaCoq.Template.common.uGraph]
GoodConstraintSetProp [module, in MetaCoq.Template.common.uGraph]
GoodConstraintSet_pair_In [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraintSet_pair [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.compare [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_spec [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_refl [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_eq [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_trans [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_sym [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.eq [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_dec [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_equiv [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_trans [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_sym [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_refl [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.gc_le_var_set [constructor, in MetaCoq.Template.common.uGraph]
GoodConstraint.gc_le_level_set [constructor, in MetaCoq.Template.common.uGraph]
GoodConstraint.gc_le_set_var [constructor, in MetaCoq.Template.common.uGraph]
GoodConstraint.gc_lt_set_level [constructor, in MetaCoq.Template.common.uGraph]
GoodConstraint.gc_le [constructor, in MetaCoq.Template.common.uGraph]
GoodConstraint.lt [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_compat [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_strorder [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_not_eq [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_trans [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.nat_compare_eq [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.nat_compare_trans [lemma, in MetaCoq.Template.common.uGraph]
GoodConstraint.satisfies [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.t [definition, in MetaCoq.Template.common.uGraph]
GoodConstraint.t_ [inductive, in MetaCoq.Template.common.uGraph]
GoodConstraint.Z_compare_trans [lemma, in MetaCoq.Template.common.uGraph]
_ ?= _ [notation, in MetaCoq.Template.common.uGraph]
gph:679 [binder, in MetaCoq.Template.common.uGraph]
gph:711 [binder, in MetaCoq.Template.common.uGraph]
gph:716 [binder, in MetaCoq.Template.common.uGraph]
GraphSpec [section, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
graph_of_wf_ext [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
graph_of_wf [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
gref_eq_dec [definition, in MetaCoq.Template.Kernames]
gref_eqb [definition, in MetaCoq.Template.Kernames]
gref:227 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
gref:376 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
gref:654 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
grep_reflect_eq [instance, in MetaCoq.Template.Kernames]
gr':113 [binder, in MetaCoq.Translations.translation_utils]
gr':122 [binder, in MetaCoq.Translations.translation_utils]
gr':131 [binder, in MetaCoq.Translations.translation_utils]
gr':148 [binder, in MetaCoq.Translations.translation_utils]
gr':80 [binder, in MetaCoq.Translations.translation_utils]
gr':93 [binder, in MetaCoq.Template.Kernames]
gr':96 [binder, in MetaCoq.Translations.translation_utils]
gr:103 [binder, in MetaCoq.Translations.translation_utils]
gr:12 [binder, in MetaCoq.Translations.translation_utils]
gr:153 [binder, in MetaCoq.Template.TermEquality]
gr:178 [binder, in MetaCoq.Template.TermEquality]
gr:192 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:204 [binder, in MetaCoq.Template.TermEquality]
gr:213 [binder, in MetaCoq.Template.TermEquality]
gr:220 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:24 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:250 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:26 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
gr:27 [binder, in MetaCoq.Template.TermEquality]
gr:271 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:272 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:279 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:286 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:287 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:302 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:31 [binder, in MetaCoq.Translations.translation_utils]
gr:31 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
gr:315 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:32 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:321 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:331 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:34 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:340 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:347 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:350 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:358 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:37 [binder, in MetaCoq.Template.TermEquality]
gr:39 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
gr:48 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
gr:48 [binder, in MetaCoq.Examples.demo]
gr:49 [binder, in MetaCoq.Translations.translation_utils]
gr:54 [binder, in MetaCoq.Translations.translation_utils]
gr:678 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
gr:689 [binder, in MetaCoq.PCUIC.PCUICEquality]
gr:7 [binder, in MetaCoq.Translations.translation_utils]
gr:70 [binder, in MetaCoq.Examples.demo]
gr:71 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:86 [binder, in MetaCoq.Template.Kernames]
gr:92 [binder, in MetaCoq.Template.Kernames]
guard [projection, in MetaCoq.PCUIC.PCUICTyping]
GuardChecker [record, in MetaCoq.Template.Typing]
GuardChecker [record, in MetaCoq.PCUIC.PCUICTyping]
GuardCheckerCorrect [record, in MetaCoq.PCUIC.PCUICGuardCondition]
guarded_to_unguarded_fix [definition, in MetaCoq.Erasure.ETransform]
guarded:1106 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
guarded:1110 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
guarded:67 [binder, in MetaCoq.Erasure.EWcbvEval]
guarded:73 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
guarded:76 [binder, in MetaCoq.Erasure.EWcbvEval]
guarded:83 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
guard_correct [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard_impl [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard_checking [axiom, in MetaCoq.Template.Typing]
guard_checking [axiom, in MetaCoq.PCUIC.PCUICTyping]
guard_checking_correct [axiom, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_rename [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_inst [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_subst_instance [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_nl [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_context_cumulativity [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_extends [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_eq_term [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard_red1 [projection, in MetaCoq.PCUIC.PCUICGuardCondition]
guard:1 [binder, in MetaCoq.Erasure.Erasure]
guard:103 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:109 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:130 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:132 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:147 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:153 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:16 [binder, in MetaCoq.Erasure.ETransform]
guard:170 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:177 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:18 [binder, in MetaCoq.SafeChecker.SafeTemplateChecker]
guard:181 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:185 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:189 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:19 [binder, in MetaCoq.Erasure.ETransform]
guard:200 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:203 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:206 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:214 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:216 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:218 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:220 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:24 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
guard:24 [binder, in MetaCoq.Erasure.ETransform]
guard:3 [binder, in MetaCoq.Erasure.Erasure]
guard:32 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:4 [binder, in MetaCoq.SafeChecker.SafeTemplateChecker]
guard:4 [binder, in MetaCoq.Erasure.ETransform]
guard:4 [binder, in MetaCoq.Erasure.Erasure]
guard:53 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:6 [binder, in MetaCoq.SafeChecker.SafeTemplateChecker]
guard:6 [binder, in MetaCoq.Erasure.Erasure]
guard:69 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:75 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:9 [binder, in MetaCoq.SafeChecker.SafeTemplateChecker]
g'':60 [binder, in MetaCoq.Template.Transform]
g':100 [binder, in MetaCoq.Template.BasicAst]
g':1009 [binder, in MetaCoq.Translations.MiniHoTT]
g':1017 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g':103 [binder, in MetaCoq.Erasure.ETransform]
g':113 [binder, in MetaCoq.Template.BasicAst]
g':113 [binder, in MetaCoq.Erasure.ETransform]
g':121 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':127 [binder, in MetaCoq.Template.BasicAst]
g':134 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':167 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g':174 [binder, in MetaCoq.Template.Ast]
g':18 [binder, in MetaCoq.Template.EnvMap]
g':20 [binder, in MetaCoq.Template.EnvMap]
g':2485 [binder, in MetaCoq.Translations.MiniHoTT]
g':2493 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G':250 [binder, in MetaCoq.Template.common.uGraph]
g':252 [binder, in MetaCoq.Template.common.uGraph]
g':256 [binder, in MetaCoq.Template.common.uGraph]
g':268 [binder, in MetaCoq.PCUIC.PCUICAst]
g':287 [binder, in MetaCoq.PCUIC.PCUICAst]
g':30 [binder, in MetaCoq.Erasure.ETransform]
g':340 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':38 [binder, in MetaCoq.Template.Ast]
g':45 [binder, in MetaCoq.Erasure.ETransform]
g':503 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g':53 [binder, in MetaCoq.Template.Ast]
g':57 [binder, in MetaCoq.Template.Transform]
g':58 [binder, in MetaCoq.Erasure.ETransform]
g':672 [binder, in MetaCoq.Translations.MiniHoTT]
g':680 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g':682 [binder, in MetaCoq.Translations.MiniHoTT]
g':69 [binder, in MetaCoq.Erasure.ETransform]
g':690 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g':693 [binder, in MetaCoq.Translations.MiniHoTT]
G':701 [binder, in MetaCoq.Template.common.uGraph]
g':701 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g':704 [binder, in MetaCoq.Translations.MiniHoTT]
G':709 [binder, in MetaCoq.Template.common.uGraph]
g':712 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g':79 [binder, in MetaCoq.Erasure.ETransform]
g':82 [binder, in MetaCoq.Template.BasicAst]
g':820 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
G':89 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g':898 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':90 [binder, in MetaCoq.Template.BasicAst]
g':91 [binder, in MetaCoq.Erasure.ETransform]
g0:24 [binder, in MetaCoq.Template.EnvMap]
g0:2497 [binder, in MetaCoq.Translations.MiniHoTT]
g0:2505 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g0:2588 [binder, in MetaCoq.Translations.MiniHoTT]
g0:2596 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G1:1048 [binder, in MetaCoq.Template.utils.wGraph]
G1:1054 [binder, in MetaCoq.Template.utils.wGraph]
G1:1058 [binder, in MetaCoq.Template.utils.wGraph]
G1:1060 [binder, in MetaCoq.Template.utils.wGraph]
G1:1069 [binder, in MetaCoq.Template.utils.wGraph]
G1:1094 [binder, in MetaCoq.Template.utils.wGraph]
G1:1122 [binder, in MetaCoq.Template.utils.wGraph]
G1:1128 [binder, in MetaCoq.Template.utils.wGraph]
G1:1132 [binder, in MetaCoq.Template.utils.wGraph]
G1:1139 [binder, in MetaCoq.Template.utils.wGraph]
G1:1144 [binder, in MetaCoq.Template.utils.wGraph]
G1:1148 [binder, in MetaCoq.Template.utils.wGraph]
G1:1150 [binder, in MetaCoq.Template.utils.wGraph]
G1:1182 [binder, in MetaCoq.Template.utils.wGraph]
g1:2499 [binder, in MetaCoq.Translations.MiniHoTT]
g1:2507 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g1:2590 [binder, in MetaCoq.Translations.MiniHoTT]
g1:2598 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G1:814 [binder, in MetaCoq.Template.utils.wGraph]
G1:817 [binder, in MetaCoq.Template.utils.wGraph]
G1:871 [binder, in MetaCoq.Template.utils.wGraph]
G1:943 [binder, in MetaCoq.Template.utils.wGraph]
G1:987 [binder, in MetaCoq.Template.utils.wGraph]
G2:1049 [binder, in MetaCoq.Template.utils.wGraph]
G2:1055 [binder, in MetaCoq.Template.utils.wGraph]
G2:1059 [binder, in MetaCoq.Template.utils.wGraph]
G2:1061 [binder, in MetaCoq.Template.utils.wGraph]
G2:1095 [binder, in MetaCoq.Template.utils.wGraph]
G2:1123 [binder, in MetaCoq.Template.utils.wGraph]
G2:1129 [binder, in MetaCoq.Template.utils.wGraph]
G2:1133 [binder, in MetaCoq.Template.utils.wGraph]
G2:1140 [binder, in MetaCoq.Template.utils.wGraph]
G2:1145 [binder, in MetaCoq.Template.utils.wGraph]
G2:1149 [binder, in MetaCoq.Template.utils.wGraph]
G2:1151 [binder, in MetaCoq.Template.utils.wGraph]
G2:1183 [binder, in MetaCoq.Template.utils.wGraph]
G2:818 [binder, in MetaCoq.Template.utils.wGraph]
G2:872 [binder, in MetaCoq.Template.utils.wGraph]
G2:944 [binder, in MetaCoq.Template.utils.wGraph]
G2:988 [binder, in MetaCoq.Template.utils.wGraph]
g:1 [binder, in MetaCoq.Template.utils.MCPrelude]
G:10 [binder, in MetaCoq.Translations.param_cheap_packed]
g:100 [binder, in MetaCoq.Translations.MiniHoTT]
g:1008 [binder, in MetaCoq.Translations.MiniHoTT]
g:1016 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:102 [binder, in MetaCoq.Erasure.ETransform]
g:104 [binder, in MetaCoq.Translations.param_generous_packed]
g:1053 [binder, in MetaCoq.Translations.MiniHoTT]
g:106 [binder, in MetaCoq.Translations.MiniHoTT]
g:1061 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:107 [binder, in MetaCoq.Template.Ast]
g:1076 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:108 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:108 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1082 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:109 [binder, in MetaCoq.Translations.MiniHoTT]
g:11 [binder, in MetaCoq.PCUIC.PCUICSpine]
g:112 [binder, in MetaCoq.Template.BasicAst]
g:112 [binder, in MetaCoq.Erasure.ETransform]
g:113 [binder, in MetaCoq.Translations.MiniHoTT]
g:114 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:115 [binder, in MetaCoq.Template.utils.MCOption]
g:115 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
G:1160 [binder, in MetaCoq.Template.utils.wGraph]
g:117 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1170 [binder, in MetaCoq.Translations.MiniHoTT]
g:1175 [binder, in MetaCoq.Template.utils.All_Forall]
g:1178 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:118 [binder, in MetaCoq.Translations.MiniHoTT]
g:1181 [binder, in MetaCoq.Translations.MiniHoTT]
g:1187 [binder, in MetaCoq.Template.utils.All_Forall]
g:1189 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:12 [binder, in MetaCoq.Template.EnvMap]
g:121 [binder, in MetaCoq.Template.utils.All_Forall]
g:121 [binder, in MetaCoq.Template.utils.MCList]
g:121 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:122 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:122 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:126 [binder, in MetaCoq.Template.BasicAst]
g:126 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:128 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:128 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
g:13 [binder, in MetaCoq.Template.TemplateCheckWf]
g:130 [binder, in MetaCoq.Template.utils.All_Forall]
g:1308 [binder, in MetaCoq.Template.utils.All_Forall]
g:134 [binder, in MetaCoq.Template.Ast]
g:135 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:135 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
g:136 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
g:1365 [binder, in MetaCoq.Template.utils.All_Forall]
g:137 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
g:138 [binder, in MetaCoq.Erasure.ErasureProperties]
g:139 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
g:139 [binder, in MetaCoq.PCUIC.PCUICContexts]
g:1428 [binder, in MetaCoq.Translations.MiniHoTT]
g:1434 [binder, in MetaCoq.Template.utils.All_Forall]
g:1436 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1437 [binder, in MetaCoq.Translations.MiniHoTT]
g:1441 [binder, in MetaCoq.Translations.MiniHoTT]
g:1445 [binder, in MetaCoq.Erasure.ErasureFunction]
g:1445 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1448 [binder, in MetaCoq.Translations.MiniHoTT]
g:1449 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:145 [binder, in MetaCoq.Template.Ast]
g:1451 [binder, in MetaCoq.Translations.MiniHoTT]
g:1455 [binder, in MetaCoq.Translations.MiniHoTT]
g:1456 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1459 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:146 [binder, in MetaCoq.Template.utils.MCList]
g:1463 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:147 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
g:1478 [binder, in MetaCoq.Translations.MiniHoTT]
g:148 [binder, in MetaCoq.Template.LiftSubst]
g:1486 [binder, in MetaCoq.Translations.MiniHoTT]
g:1486 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:149 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:1492 [binder, in MetaCoq.Translations.MiniHoTT]
g:1494 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:15 [binder, in MetaCoq.Template.TemplateCheckWf]
g:15 [binder, in MetaCoq.Template.utils.MCProd]
G:15 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
g:1500 [binder, in MetaCoq.Translations.MiniHoTT]
g:1500 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1508 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1509 [binder, in MetaCoq.Translations.MiniHoTT]
g:1517 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1521 [binder, in MetaCoq.Translations.MiniHoTT]
g:1529 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:153 [binder, in MetaCoq.Template.Ast]
g:1536 [binder, in MetaCoq.Translations.MiniHoTT]
g:154 [binder, in MetaCoq.Template.utils.MCList]
g:154 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:154 [binder, in MetaCoq.Translations.MiniHoTT]
g:1544 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:157 [binder, in MetaCoq.Template.BasicAst]
g:157 [binder, in MetaCoq.Translations.times_bool_fun]
G:16 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:16 [binder, in MetaCoq.Template.TemplateCheckWf]
G:16 [binder, in MetaCoq.Translations.param_cheap_packed]
g:16 [binder, in MetaCoq.Template.EnvMap]
g:16 [binder, in MetaCoq.Translations.times_bool_fun2]
g:160 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
g:1608 [binder, in MetaCoq.Translations.MiniHoTT]
g:1609 [binder, in MetaCoq.Translations.MiniHoTT]
g:1612 [binder, in MetaCoq.Template.utils.All_Forall]
g:1614 [binder, in MetaCoq.Translations.MiniHoTT]
g:1616 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1617 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:162 [binder, in MetaCoq.Template.Ast]
g:162 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1621 [binder, in MetaCoq.Translations.MiniHoTT]
g:1622 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1627 [binder, in MetaCoq.Translations.MiniHoTT]
g:1629 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:163 [binder, in MetaCoq.Template.BasicAst]
g:163 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:1634 [binder, in MetaCoq.Translations.MiniHoTT]
g:1635 [binder, in MetaCoq.Translations.MiniHoTT]
g:1635 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1640 [binder, in MetaCoq.Translations.MiniHoTT]
g:1642 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1643 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1647 [binder, in MetaCoq.Translations.MiniHoTT]
g:1648 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:165 [binder, in MetaCoq.Translations.MiniHoTT]
g:1653 [binder, in MetaCoq.Translations.MiniHoTT]
g:1655 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:166 [binder, in MetaCoq.Template.utils.All_Forall]
g:166 [binder, in MetaCoq.Template.utils.MCList]
g:166 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:1661 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:168 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:169 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
g:1690 [binder, in MetaCoq.Translations.MiniHoTT]
g:1693 [binder, in MetaCoq.Template.utils.All_Forall]
g:1698 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:17 [binder, in MetaCoq.Template.EnvMap]
g:1706 [binder, in MetaCoq.Translations.MiniHoTT]
g:1714 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:172 [binder, in MetaCoq.Translations.MiniHoTT]
g:1728 [binder, in MetaCoq.Template.utils.All_Forall]
g:173 [binder, in MetaCoq.Template.Ast]
G:173 [binder, in MetaCoq.SafeChecker.PCUICErrors]
g:173 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1738 [binder, in MetaCoq.Translations.MiniHoTT]
g:1746 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1748 [binder, in MetaCoq.Translations.MiniHoTT]
g:175 [binder, in MetaCoq.Template.utils.MCList]
g:1756 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1758 [binder, in MetaCoq.Translations.MiniHoTT]
g:1766 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1767 [binder, in MetaCoq.Translations.MiniHoTT]
g:1775 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:1776 [binder, in MetaCoq.Translations.MiniHoTT]
g:1784 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:180 [binder, in MetaCoq.Translations.MiniHoTT]
g:180 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G:181 [binder, in MetaCoq.SafeChecker.PCUICErrors]
g:183 [binder, in MetaCoq.Template.utils.MCList]
g:1878 [binder, in MetaCoq.Template.utils.All_Forall]
G:188 [binder, in MetaCoq.Template.utils.wGraph]
g:188 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G:189 [binder, in MetaCoq.Template.utils.wGraph]
g:189 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:19 [binder, in MetaCoq.Template.EnvMap]
G:190 [binder, in MetaCoq.Template.utils.wGraph]
g:191 [binder, in MetaCoq.Translations.times_bool_fun]
g:192 [binder, in MetaCoq.Template.common.uGraph]
G:192 [binder, in MetaCoq.Template.utils.wGraph]
G:193 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:193 [binder, in MetaCoq.Template.common.uGraph]
g:1940 [binder, in MetaCoq.Template.utils.All_Forall]
g:1962 [binder, in MetaCoq.Template.utils.All_Forall]
G:199 [binder, in MetaCoq.SafeChecker.PCUICErrors]
g:2 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
g:201 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:203 [binder, in MetaCoq.Template.common.uGraph]
G:204 [binder, in MetaCoq.Template.Checker]
g:2071 [binder, in MetaCoq.Template.utils.All_Forall]
g:21 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
g:212 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:2137 [binder, in MetaCoq.Template.utils.All_Forall]
g:2148 [binder, in MetaCoq.Template.utils.All_Forall]
g:218 [binder, in MetaCoq.Template.BasicAst]
g:218 [binder, in MetaCoq.Template.utils.All_Forall]
g:22 [binder, in MetaCoq.Template.utils.MCProd]
g:221 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:2252 [binder, in MetaCoq.Translations.MiniHoTT]
g:2260 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2263 [binder, in MetaCoq.Translations.MiniHoTT]
g:2271 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2273 [binder, in MetaCoq.Translations.MiniHoTT]
g:2281 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2283 [binder, in MetaCoq.Translations.MiniHoTT]
g:229 [binder, in MetaCoq.Template.utils.All_Forall]
g:2291 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:23 [binder, in MetaCoq.Template.EnvMap]
g:230 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
g:2316 [binder, in MetaCoq.Translations.MiniHoTT]
g:2322 [binder, in MetaCoq.Translations.MiniHoTT]
g:2324 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2330 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2333 [binder, in MetaCoq.Translations.MiniHoTT]
g:2338 [binder, in MetaCoq.Translations.MiniHoTT]
g:2341 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2343 [binder, in MetaCoq.Translations.MiniHoTT]
g:2346 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2348 [binder, in MetaCoq.Translations.MiniHoTT]
g:2351 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2356 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2357 [binder, in MetaCoq.Translations.MiniHoTT]
g:2365 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:238 [binder, in MetaCoq.Erasure.Extract]
G:24 [binder, in MetaCoq.Translations.param_cheap_packed]
g:240 [binder, in MetaCoq.Template.utils.All_Forall]
g:240 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:2408 [binder, in MetaCoq.Translations.MiniHoTT]
g:2416 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2419 [binder, in MetaCoq.Translations.MiniHoTT]
g:2427 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:244 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
g:2447 [binder, in MetaCoq.Translations.MiniHoTT]
g:2455 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2460 [binder, in MetaCoq.Translations.MiniHoTT]
g:2468 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2474 [binder, in MetaCoq.Translations.MiniHoTT]
g:248 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
g:2482 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2484 [binder, in MetaCoq.Translations.MiniHoTT]
g:2487 [binder, in MetaCoq.Template.utils.All_Forall]
G:249 [binder, in MetaCoq.Template.common.uGraph]
g:2492 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:251 [binder, in MetaCoq.Template.common.uGraph]
g:2511 [binder, in MetaCoq.Translations.MiniHoTT]
g:2519 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2524 [binder, in MetaCoq.Translations.MiniHoTT]
g:2532 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2535 [binder, in MetaCoq.Translations.MiniHoTT]
g:2542 [binder, in MetaCoq.Translations.MiniHoTT]
g:2543 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:255 [binder, in MetaCoq.Template.common.uGraph]
g:2550 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2564 [binder, in MetaCoq.Translations.MiniHoTT]
g:2572 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:26 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
G:262 [binder, in MetaCoq.Template.common.uGraph]
g:2625 [binder, in MetaCoq.Translations.MiniHoTT]
g:2626 [binder, in MetaCoq.Translations.MiniHoTT]
g:263 [binder, in MetaCoq.Template.utils.MCList]
g:2633 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2634 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:266 [binder, in MetaCoq.SafeChecker.PCUICErrors]
g:266 [binder, in MetaCoq.PCUIC.PCUICAst]
g:268 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:2685 [binder, in MetaCoq.Translations.MiniHoTT]
g:269 [binder, in MetaCoq.Template.EtaExpand]
g:2693 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:271 [binder, in MetaCoq.Template.utils.MCList]
g:278 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
G:284 [binder, in MetaCoq.Template.Checker]
g:286 [binder, in MetaCoq.PCUIC.PCUICAst]
g:288 [binder, in MetaCoq.Template.utils.MCList]
g:29 [binder, in MetaCoq.Erasure.ETransform]
g:29 [binder, in MetaCoq.Template.EnvMap]
g:2918 [binder, in MetaCoq.Translations.MiniHoTT]
g:2926 [binder, in MetaCoq.Translations.MiniHoTT]
g:2926 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2934 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2939 [binder, in MetaCoq.Translations.MiniHoTT]
G:294 [binder, in MetaCoq.Template.Checker]
g:2947 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:295 [binder, in MetaCoq.PCUIC.PCUICAst]
g:2954 [binder, in MetaCoq.Translations.MiniHoTT]
g:2962 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2963 [binder, in MetaCoq.Translations.MiniHoTT]
g:2968 [binder, in MetaCoq.Translations.MiniHoTT]
g:297 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
g:2971 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:2976 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:300 [binder, in MetaCoq.Template.utils.MCList]
g:308 [binder, in MetaCoq.Template.utils.MCList]
g:308 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:31 [binder, in MetaCoq.Template.EnvMap]
G:318 [binder, in MetaCoq.Template.Checker]
g:32 [binder, in MetaCoq.Template.LiftSubst]
g:324 [binder, in MetaCoq.Template.BasicAst]
g:328 [binder, in MetaCoq.Template.BasicAst]
g:331 [binder, in MetaCoq.Template.BasicAst]
g:336 [binder, in MetaCoq.Template.BasicAst]
g:338 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:339 [binder, in MetaCoq.Template.BasicAst]
g:342 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:343 [binder, in MetaCoq.Template.BasicAst]
g:347 [binder, in MetaCoq.Template.BasicAst]
g:348 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
g:35 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
g:35 [binder, in MetaCoq.Template.utils.MCProd]
g:351 [binder, in MetaCoq.Template.BasicAst]
g:352 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:354 [binder, in MetaCoq.Template.BasicAst]
G:355 [binder, in MetaCoq.Template.common.uGraph]
g:357 [binder, in MetaCoq.Template.BasicAst]
g:36 [binder, in MetaCoq.Template.Ast]
g:361 [binder, in MetaCoq.Template.BasicAst]
g:362 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:362 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
g:366 [binder, in MetaCoq.Template.BasicAst]
g:37 [binder, in MetaCoq.Template.EnvMap]
g:370 [binder, in MetaCoq.Template.BasicAst]
g:38 [binder, in MetaCoq.Template.EnvMap]
g:383 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
G:389 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
g:392 [binder, in MetaCoq.Template.BasicAst]
g:394 [binder, in MetaCoq.PCUIC.PCUICAst]
g:40 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:40 [binder, in MetaCoq.Template.EnvMap]
g:400 [binder, in MetaCoq.PCUIC.PCUICAst]
G:400 [binder, in MetaCoq.Template.Checker]
g:400 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
g:401 [binder, in MetaCoq.Template.BasicAst]
G:404 [binder, in MetaCoq.Template.Checker]
g:406 [binder, in MetaCoq.PCUIC.PCUICAst]
G:408 [binder, in MetaCoq.Template.Checker]
g:410 [binder, in MetaCoq.Template.BasicAst]
g:410 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
G:411 [binder, in MetaCoq.Template.Checker]
g:413 [binder, in MetaCoq.PCUIC.PCUICAst]
g:413 [binder, in MetaCoq.Template.Checker]
g:42 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
g:42 [binder, in MetaCoq.Template.EnvMap]
g:42 [binder, in MetaCoq.Template.utils.MCProd]
G:422 [binder, in MetaCoq.Template.Checker]
G:425 [binder, in MetaCoq.Template.Checker]
g:426 [binder, in MetaCoq.Template.Checker]
G:433 [binder, in MetaCoq.Template.Checker]
g:44 [binder, in MetaCoq.Erasure.ETransform]
g:449 [binder, in MetaCoq.PCUIC.PCUICAst]
g:454 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:463 [binder, in MetaCoq.PCUIC.PCUICAst]
G:47 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:47 [binder, in MetaCoq.Template.EnvMap]
g:47 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
G:470 [binder, in MetaCoq.Template.common.uGraph]
G:473 [binder, in MetaCoq.Template.common.uGraph]
g:473 [binder, in MetaCoq.PCUIC.PCUICAst]
g:481 [binder, in MetaCoq.PCUIC.PCUICAst]
g:482 [binder, in MetaCoq.Translations.MiniHoTT]
g:488 [binder, in MetaCoq.PCUIC.PCUICAst]
g:49 [binder, in MetaCoq.Template.BasicAst]
g:49 [binder, in MetaCoq.Template.utils.MCList]
g:490 [binder, in MetaCoq.Translations.MiniHoTT]
g:490 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:498 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:5 [binder, in MetaCoq.Template.EnvMap]
g:5 [binder, in MetaCoq.PCUIC.PCUICProgram]
g:50 [binder, in MetaCoq.Template.EnvMap]
g:50 [binder, in MetaCoq.Template.monad_utils]
g:504 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:504 [binder, in MetaCoq.Translations.MiniHoTT]
g:51 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
g:512 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:52 [binder, in MetaCoq.Template.Ast]
g:52 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:527 [binder, in MetaCoq.Translations.MiniHoTT]
g:53 [binder, in MetaCoq.Translations.MiniHoTT]
g:535 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G:536 [binder, in MetaCoq.Template.common.uGraph]
g:537 [binder, in MetaCoq.Template.EtaExpand]
g:54 [binder, in MetaCoq.Template.EnvMap]
g:54 [binder, in MetaCoq.Template.utils.MCOption]
g:540 [binder, in MetaCoq.Translations.MiniHoTT]
g:541 [binder, in MetaCoq.Template.EtaExpand]
g:541 [binder, in MetaCoq.PCUIC.PCUICAst]
g:545 [binder, in MetaCoq.Template.EtaExpand]
g:545 [binder, in MetaCoq.Template.common.uGraph]
g:547 [binder, in MetaCoq.Template.common.uGraph]
g:548 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:550 [binder, in MetaCoq.Template.common.uGraph]
g:551 [binder, in MetaCoq.PCUIC.PCUICAst]
g:551 [binder, in MetaCoq.Translations.MiniHoTT]
g:555 [binder, in MetaCoq.Template.common.uGraph]
g:559 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:56 [binder, in MetaCoq.Template.Pretty]
g:56 [binder, in MetaCoq.Template.Transform]
g:563 [binder, in MetaCoq.PCUIC.PCUICAst]
g:57 [binder, in MetaCoq.Erasure.ETransform]
g:571 [binder, in MetaCoq.Translations.MiniHoTT]
g:579 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:59 [binder, in MetaCoq.Template.BasicAst]
g:59 [binder, in MetaCoq.Erasure.ELiftSubst]
g:6 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:6 [binder, in MetaCoq.PCUIC.PCUICProgram]
G:60 [binder, in MetaCoq.Translations.param_cheap_packed]
g:60 [binder, in MetaCoq.Template.utils.MCOption]
g:60 [binder, in MetaCoq.Translations.MiniHoTT]
g:600 [binder, in MetaCoq.Translations.MiniHoTT]
G:608 [binder, in MetaCoq.Template.utils.wGraph]
g:608 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:609 [binder, in MetaCoq.Translations.MiniHoTT]
g:61 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:615 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
G:616 [binder, in MetaCoq.Template.common.uGraph]
G:617 [binder, in MetaCoq.Template.common.uGraph]
g:617 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:624 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:63 [binder, in MetaCoq.Erasure.EEnvMap]
g:631 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:64 [binder, in MetaCoq.Template.BasicAst]
g:64 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
g:64 [binder, in MetaCoq.Erasure.ELiftSubst]
g:640 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:644 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:645 [binder, in MetaCoq.Translations.MiniHoTT]
g:65 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
g:653 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G:654 [binder, in MetaCoq.Template.utils.wGraph]
g:655 [binder, in MetaCoq.Template.utils.MCList]
g:661 [binder, in MetaCoq.Template.EnvironmentTyping]
g:662 [binder, in MetaCoq.Template.EnvironmentTyping]
g:663 [binder, in MetaCoq.Translations.MiniHoTT]
G:669 [binder, in MetaCoq.Template.common.uGraph]
g:67 [binder, in MetaCoq.Template.EnvMap]
g:671 [binder, in MetaCoq.Translations.MiniHoTT]
g:671 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:673 [binder, in MetaCoq.Template.EnvironmentTyping]
g:679 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:68 [binder, in MetaCoq.Erasure.ETransform]
g:68 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:681 [binder, in MetaCoq.Translations.MiniHoTT]
G:682 [binder, in MetaCoq.Template.common.uGraph]
g:682 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
G:685 [binder, in MetaCoq.Template.common.uGraph]
g:686 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:689 [binder, in MetaCoq.Translations.MiniHoTT_paths]
G:690 [binder, in MetaCoq.Template.common.uGraph]
g:692 [binder, in MetaCoq.Translations.MiniHoTT]
G:695 [binder, in MetaCoq.Template.common.uGraph]
G:699 [binder, in MetaCoq.Template.common.uGraph]
g:70 [binder, in MetaCoq.PCUIC.PCUICAst]
g:700 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:703 [binder, in MetaCoq.Translations.MiniHoTT]
G:707 [binder, in MetaCoq.Template.common.uGraph]
g:711 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:725 [binder, in MetaCoq.Template.utils.MCList]
g:73 [binder, in MetaCoq.Translations.times_bool_fun2]
g:738 [binder, in MetaCoq.Template.utils.MCList]
g:748 [binder, in MetaCoq.Template.utils.MCList]
g:77 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:775 [binder, in MetaCoq.Translations.MiniHoTT]
g:775 [binder, in MetaCoq.PCUIC.PCUICReduction]
g:778 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:78 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
g:78 [binder, in MetaCoq.Erasure.ETransform]
g:783 [binder, in MetaCoq.Translations.MiniHoTT_paths]
g:784 [binder, in MetaCoq.PCUIC.PCUICReduction]
G:788 [binder, in MetaCoq.Template.utils.wGraph]
G:791 [binder, in MetaCoq.Template.utils.wGraph]
G:797 [binder, in MetaCoq.Template.utils.wGraph]
G:8 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:8 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
G:803 [binder, in MetaCoq.Template.utils.wGraph]
G:806 [binder, in MetaCoq.Template.utils.wGraph]
g:81 [binder, in MetaCoq.Template.BasicAst]
g:81 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
G:811 [binder, in MetaCoq.Template.utils.wGraph]
g:82 [binder, in MetaCoq.PCUIC.PCUICAst]
G:82 [binder, in MetaCoq.Translations.param_cheap_packed]
g:82 [binder, in MetaCoq.Template.utils.MCOption]
g:82 [binder, in MetaCoq.Translations.times_bool_fun2]
G:820 [binder, in MetaCoq.Template.utils.wGraph]
g:821 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
G:825 [binder, in MetaCoq.Template.utils.wGraph]
g:832 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
G:832 [binder, in MetaCoq.Template.utils.wGraph]
G:836 [binder, in MetaCoq.Template.utils.wGraph]
g:85 [binder, in MetaCoq.Translations.times_bool_fun2]
G:856 [binder, in MetaCoq.Template.utils.wGraph]
g:86 [binder, in MetaCoq.Erasure.EPretty]
g:86 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:86 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
g:86 [binder, in MetaCoq.PCUIC.PCUICEquality]
G:865 [binder, in MetaCoq.Template.utils.wGraph]
g:875 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:876 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:879 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
G:88 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
G:88 [binder, in MetaCoq.Translations.param_cheap_packed]
g:886 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:89 [binder, in MetaCoq.Template.BasicAst]
G:89 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
g:89 [binder, in MetaCoq.Translations.param_generous_packed]
g:897 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:90 [binder, in MetaCoq.Erasure.ETransform]
g:93 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
g:932 [binder, in MetaCoq.PCUIC.PCUICConversion]
G:938 [binder, in MetaCoq.Template.utils.wGraph]
g:94 [binder, in MetaCoq.Translations.param_generous_packed]
g:950 [binder, in MetaCoq.PCUIC.PCUICConversion]
g:960 [binder, in MetaCoq.PCUIC.PCUICConversion]
g:965 [binder, in MetaCoq.Template.utils.All_Forall]
g:98 [binder, in MetaCoq.Template.utils.All_Forall]
g:99 [binder, in MetaCoq.Template.BasicAst]
g:99 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
| 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) |