| 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) |
M
MakeGraph [section, in MetaCoq.Template.common.uGraph]MakeGraph.ctrs [variable, in MetaCoq.Template.common.uGraph]
MakeGraph.G [variable, in MetaCoq.Template.common.uGraph]
make_wf_env_ext [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
make_typing_spine [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
make_wf_env_ext [definition, in MetaCoq.Examples.typing_correctness]
make_graph_proper [instance, in MetaCoq.Template.common.uGraph]
make_graph_spec2 [lemma, in MetaCoq.Template.common.uGraph]
make_graph_spec' [lemma, in MetaCoq.Template.common.uGraph]
make_graph_spec [lemma, in MetaCoq.Template.common.uGraph]
make_graph_invariants [instance, in MetaCoq.Template.common.uGraph]
make_graph_E [lemma, in MetaCoq.Template.common.uGraph]
make_graph [definition, in MetaCoq.Template.common.uGraph]
make_fresh_name_fresh [lemma, in MetaCoq.SafeChecker.PCUICConsistency]
make_fresh_name [definition, in MetaCoq.SafeChecker.PCUICConsistency]
make_context_subst_spec_inv [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
make_context_subst_recP [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
make_context_subst_spec [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
make_context_subst_rec_spec [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
make_context_subst [definition, in MetaCoq.PCUIC.PCUICContextSubst]
make_abstract_env_ext [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
make_graph_proper [instance, in MetaCoq.SafeChecker.PCUICSafeChecker]
make_wf_env_ext [definition, in MetaCoq.Examples.metacoq_tour_prelude]
make_inductive_body [definition, in MetaCoq.Template.AstUtils]
make_constructor_body [definition, in MetaCoq.Template.AstUtils]
make_context_subst_length [lemma, in MetaCoq.PCUIC.PCUICSpine]
make_context_subst_tele [lemma, in MetaCoq.PCUIC.PCUICSpine]
make_context_subst_skipn [lemma, in MetaCoq.PCUIC.PCUICSpine]
mapi [definition, in MetaCoq.Template.utils.MCList]
MapInP [section, in MetaCoq.PCUIC.utils.PCUICAstUtils]
MapInP [section, in MetaCoq.Template.utils.MCList]
mapi_context_map_context [lemma, in MetaCoq.Template.BasicAst]
mapi_context_map [lemma, in MetaCoq.Template.BasicAst]
mapi_context_In_spec [lemma, in MetaCoq.Template.BasicAst]
mapi_context_In [definition, in MetaCoq.Template.BasicAst]
mapi_context_fold [lemma, in MetaCoq.Template.BasicAst]
mapi_context_length [lemma, in MetaCoq.Template.BasicAst]
mapi_context_proper [instance, in MetaCoq.Template.BasicAst]
mapi_context [definition, in MetaCoq.Template.BasicAst]
mapi_map2 [lemma, in MetaCoq.Template.utils.MCList]
mapi_unfold [lemma, in MetaCoq.Template.utils.MCList]
mapi_irrel_list [lemma, in MetaCoq.Template.utils.MCList]
mapi_nth [lemma, in MetaCoq.Template.utils.MCList]
mapi_cons [lemma, in MetaCoq.Template.utils.MCList]
mapi_length [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_length [lemma, in MetaCoq.Template.utils.MCList]
mapi_rev [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_rev [lemma, in MetaCoq.Template.utils.MCList]
mapi_app [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_app [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_add [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_Sk [lemma, in MetaCoq.Template.utils.MCList]
mapi_ext [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_ext [lemma, in MetaCoq.Template.utils.MCList]
mapi_cst_map [lemma, in MetaCoq.Template.utils.MCList]
mapi_mapi [lemma, in MetaCoq.Template.utils.MCList]
mapi_map [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_eqn [lemma, in MetaCoq.Template.utils.MCList]
mapi_compose [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec_compose [lemma, in MetaCoq.Template.utils.MCList]
mapi_ext_size [lemma, in MetaCoq.Template.utils.MCList]
mapi_rec [definition, in MetaCoq.Template.utils.MCList]
mapi_context_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
mapi_context_lift [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
mapi_context_compose [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
mapi_context_eqP_test_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
mapi_context_eqP_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
mapi_context_eqP_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
mapi_context_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mapi_context_eqP_onctx_k_spec [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mapi_context_rename [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mapi_context_fold_context [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mapOne [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mapOne [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mapopt [definition, in MetaCoq.Template.monad_utils]
MapOpt [section, in MetaCoq.Template.monad_utils]
map_decl_body [definition, in MetaCoq.Template.EtaExpand]
map_squash [lemma, in MetaCoq.Template.utils.MCSquash]
map_decl_name_fold_context_k [lemma, in MetaCoq.Template.BasicAst]
map_context_id [lemma, in MetaCoq.Template.BasicAst]
map_mapi_context [lemma, in MetaCoq.Template.BasicAst]
map_map_context [lemma, in MetaCoq.Template.BasicAst]
map_context_map [lemma, in MetaCoq.Template.BasicAst]
map_context_mapi_context [lemma, in MetaCoq.Template.BasicAst]
map_fold_context_k [lemma, in MetaCoq.Template.BasicAst]
map_decl_id [lemma, in MetaCoq.Template.BasicAst]
map_decl_body [lemma, in MetaCoq.Template.BasicAst]
map_decl_type [lemma, in MetaCoq.Template.BasicAst]
map_context_length [lemma, in MetaCoq.Template.BasicAst]
map_context_proper [instance, in MetaCoq.Template.BasicAst]
map_context [definition, in MetaCoq.Template.BasicAst]
map_decl_pointwise [instance, in MetaCoq.Template.BasicAst]
map_decl_proper [instance, in MetaCoq.Template.BasicAst]
map_decl_ext [lemma, in MetaCoq.Template.BasicAst]
map_decl [definition, in MetaCoq.Template.BasicAst]
map_def_id_spec [lemma, in MetaCoq.Template.BasicAst]
map_def_eq_spec [lemma, in MetaCoq.Template.BasicAst]
map_def_spec [lemma, in MetaCoq.Template.BasicAst]
map_def_id [lemma, in MetaCoq.Template.BasicAst]
map_def_map_def [lemma, in MetaCoq.Template.BasicAst]
map_dbody [lemma, in MetaCoq.Template.BasicAst]
map_dtype [lemma, in MetaCoq.Template.BasicAst]
map_def [definition, in MetaCoq.Template.BasicAst]
map_binder_annot [definition, in MetaCoq.Template.BasicAst]
map_InP_length [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
map_InP_spec [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
map_InP [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
map_All_length [lemma, in MetaCoq.Template.utils.All_Forall]
map_All [definition, in MetaCoq.Template.utils.All_Forall]
map_All [section, in MetaCoq.Template.utils.All_Forall]
map_option_out_All [lemma, in MetaCoq.Template.utils.All_Forall]
map_option_Some [lemma, in MetaCoq.Template.utils.All_Forall]
map_eq_inj [lemma, in MetaCoq.Template.utils.All_Forall]
map_option_out_check_one_cofix [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map_option_out_check_one_fix [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map_context_trans [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map_map2 [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map_repeat [lemma, in MetaCoq.Template.utils.MCList]
map_InP_spec [lemma, in MetaCoq.Template.utils.MCList]
map_InP [definition, in MetaCoq.Template.utils.MCList]
map_In_spec [lemma, in MetaCoq.Template.utils.MCList]
map_In [definition, in MetaCoq.Template.utils.MCList]
map_inj [lemma, in MetaCoq.Template.utils.MCList]
map_mapi [lemma, in MetaCoq.Template.utils.MCList]
map_nil [lemma, in MetaCoq.Template.utils.MCList]
map_skipn [lemma, in MetaCoq.Template.utils.MCList]
map_ext [lemma, in MetaCoq.Template.utils.MCList]
map_ext_size [lemma, in MetaCoq.Template.utils.MCList]
map_id_f [lemma, in MetaCoq.Template.utils.MCList]
map_map_compose [lemma, in MetaCoq.Template.utils.MCList]
map_option_out_check_one_cofix [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map_option_out_check_one_fix [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map_map_comm [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map_decl_subst_instance_set_binder_name [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map_map2 [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map_option_out_impl [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
map_vass_map_def_subst [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
map_optimize_repeat_box [lemma, in MetaCoq.Erasure.EInlineProjections]
map_decl_na [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
map_subst_let_expand_lift [lemma, in MetaCoq.PCUIC.PCUICInductives]
map_subst_let_expand_to_extended_list [lemma, in MetaCoq.PCUIC.PCUICInductives]
map_subst_let_expand_k_to_extended_list_lift [lemma, in MetaCoq.PCUIC.PCUICInductives]
map_subst_let_expand_k [lemma, in MetaCoq.PCUIC.PCUICInductives]
map_expand_lets_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICInductives]
map_branches_k_map_branches_k [lemma, in MetaCoq.Template.Ast]
map_branches_k [abbreviation, in MetaCoq.Template.Ast]
map_branches [definition, in MetaCoq.Template.Ast]
map_branches_map_branches [lemma, in MetaCoq.Template.Ast]
map_branch_id_spec [lemma, in MetaCoq.Template.Ast]
map_branch_proper [instance, in MetaCoq.Template.Ast]
map_branch_eq_spec [lemma, in MetaCoq.Template.Ast]
map_branch_id [lemma, in MetaCoq.Template.Ast]
map_branch_map_branch [lemma, in MetaCoq.Template.Ast]
map_bbody [lemma, in MetaCoq.Template.Ast]
map_branch [definition, in MetaCoq.Template.Ast]
map_branch [section, in MetaCoq.Template.Ast]
map_k_puinst [lemma, in MetaCoq.Template.Ast]
map_k_pcontext [lemma, in MetaCoq.Template.Ast]
map_k_preturn [lemma, in MetaCoq.Template.Ast]
map_k_pparams [lemma, in MetaCoq.Template.Ast]
map_predicate_k [definition, in MetaCoq.Template.Ast]
map_predicate_k [section, in MetaCoq.Template.Ast]
map_predicate_proper' [instance, in MetaCoq.Template.Ast]
map_predicate_proper [instance, in MetaCoq.Template.Ast]
map_predicate_id_spec [lemma, in MetaCoq.Template.Ast]
map_predicate_eq_spec [lemma, in MetaCoq.Template.Ast]
map_predicate_id [lemma, in MetaCoq.Template.Ast]
map_predicate_map_predicate [lemma, in MetaCoq.Template.Ast]
map_puints [lemma, in MetaCoq.Template.Ast]
map_preturn [lemma, in MetaCoq.Template.Ast]
map_pparams [lemma, in MetaCoq.Template.Ast]
map_predicate [definition, in MetaCoq.Template.Ast]
map_predicate [section, in MetaCoq.Template.Ast]
map_map_subst_expand_lets [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
map_fix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
map_cofix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
map_const [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
map_subst_expand_lets_k [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_subst_expand_lets [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_expand_lets_subst_comm [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_subst_inst [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_idsn_spec [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_inst_idsn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_map_branch_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_map_predicate_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate_gen [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_proper [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_proper [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_id_spec [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_id_spec [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_eq_spec [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_eq_spec [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_branches_shift [abbreviation, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_shift_bcontext [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_shift_bbody [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_branch_shift [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_branch_shift [section, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_shift_puinst [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_shift_pcontext [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_shift_preturn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_shift_pparams [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift [section, in MetaCoq.PCUIC.PCUICSigmaCalculus]
map_typing_result [definition, in MetaCoq.SafeChecker.PCUICSafeRetyping]
map_trans_minductive_body [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_one_ind_body [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_constructor_body [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_expand_lets_to_extended_list_k_above [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_expand_lets_lift_cancel [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_option_out_check_one_cofix [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_option_out_check_one_fix [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_context_trans [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_map2 [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map_context_eqP_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_decl_eqP_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branches_k_map_branches_k [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branches_map_branches [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_k_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_proper [instance, in MetaCoq.PCUIC.PCUICAst]
map_branch_k_eq_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_eq_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_context_eq_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_decl_eq_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_id [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_k_map_branch [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_map_branch_k [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_k_map_branch_k_id [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_k_map_branch_k [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_map_branch [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_k_map_predicate [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_map_predicate_k [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_k_map_predicate_k [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_proper' [instance, in MetaCoq.PCUIC.PCUICAst]
map_predicate_proper [instance, in MetaCoq.PCUIC.PCUICAst]
map_predicate_k_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_context_id_spec_cond [lemma, in MetaCoq.PCUIC.PCUICAst]
map_context_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_decl_id_spec_cond [lemma, in MetaCoq.PCUIC.PCUICAst]
map_decl_id_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_k_eq_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_eq_spec [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_id [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_map_predicate [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branches_k [abbreviation, in MetaCoq.PCUIC.PCUICAst]
map_k_bcontext [lemma, in MetaCoq.PCUIC.PCUICAst]
map_k_bbody [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch_k [definition, in MetaCoq.PCUIC.PCUICAst]
map_branch_k [section, in MetaCoq.PCUIC.PCUICAst]
map_branches [definition, in MetaCoq.PCUIC.PCUICAst]
map_bcontext [lemma, in MetaCoq.PCUIC.PCUICAst]
map_bbody [lemma, in MetaCoq.PCUIC.PCUICAst]
map_branch [definition, in MetaCoq.PCUIC.PCUICAst]
map_branch [section, in MetaCoq.PCUIC.PCUICAst]
map_k_puinst [lemma, in MetaCoq.PCUIC.PCUICAst]
map_k_pcontext [lemma, in MetaCoq.PCUIC.PCUICAst]
map_k_preturn [lemma, in MetaCoq.PCUIC.PCUICAst]
map_k_pparams [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate_k [definition, in MetaCoq.PCUIC.PCUICAst]
map_predicate_k [section, in MetaCoq.PCUIC.PCUICAst]
map_puinst [lemma, in MetaCoq.PCUIC.PCUICAst]
map_pcontext [lemma, in MetaCoq.PCUIC.PCUICAst]
map_preturn [lemma, in MetaCoq.PCUIC.PCUICAst]
map_pparams [lemma, in MetaCoq.PCUIC.PCUICAst]
map_predicate [definition, in MetaCoq.PCUIC.PCUICAst]
map_predicate [section, in MetaCoq.PCUIC.PCUICAst]
map_erase_length [lemma, in MetaCoq.Erasure.ErasureFunction]
map_erase_irrel [lemma, in MetaCoq.Erasure.ErasureFunction]
map_erase [definition, in MetaCoq.Erasure.ErasureFunction]
map_context [definition, in MetaCoq.Erasure.EAst]
map_decl [definition, in MetaCoq.Erasure.EAst]
map_def [definition, in MetaCoq.Erasure.EAst]
map_def_ext [instance, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
map_vass_map_def_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
map_inst_idsn [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
map_constr_with_binders [definition, in MetaCoq.Template.Checker]
map_case_branch_with_binders [definition, in MetaCoq.Template.Checker]
map_predicate_with_binders [definition, in MetaCoq.Template.Checker]
map_context_with_binders [definition, in MetaCoq.Template.Checker]
map_non_nil [lemma, in MetaCoq.Erasure.ELiftSubst]
map_def_id_spec [lemma, in MetaCoq.Erasure.ELiftSubst]
map_def_eq_spec [lemma, in MetaCoq.Erasure.ELiftSubst]
map_subst_instance_to_extended_list_k [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
map_map2 [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
map_anon_fold_context_k [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
map_def_sig_nl [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
map_option_out_impl [lemma, in MetaCoq.Template.utils.MCOption]
map_option_out_length [lemma, in MetaCoq.Template.utils.MCOption]
map_option_out_map_option_map [lemma, in MetaCoq.Template.utils.MCOption]
map_option_out [definition, in MetaCoq.Template.utils.MCOption]
map_branches_k_map_branches_k [lemma, in MetaCoq.PCUIC.PCUICConversion]
map_pair [definition, in MetaCoq.Template.utils.MCProd]
map_subst_closedn [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
map_decl_closed_ext [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
map_subst_lift0_subst [lemma, in MetaCoq.PCUIC.PCUICSR]
map_expand_lets_to_extended_list [lemma, in MetaCoq.PCUIC.PCUICSR]
map_subst_instance_to_extended_list_k [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_app_simpl [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_subst_lift_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_ext [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_id_eq [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_id [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_lift_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_vass_map_def [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_lift0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
map_strip_repeat_box [lemma, in MetaCoq.Erasure.ERemoveParams]
map_repeat [lemma, in MetaCoq.Erasure.ERemoveParams]
map_map2 [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_fold_context_k [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_mutual_inductive_body' [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_one_inductive_body' [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_constructor_body' [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_vass_map_def [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
map_depth_hom [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
map_fix_rho_rename [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_fix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_cofix_subst' [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_cofix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_fix_rho_map [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_fix [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_terms_map [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_brs_map [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_brs_wf [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_br_map [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_br_gen [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_br_wf [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_terms [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_fix_rho [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
map_decl_anon [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
map_def_anon [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
map_subst_instance_to_extended_list_k [lemma, in MetaCoq.Template.UnivSubst]
map_reln_ext [lemma, in MetaCoq.PCUIC.PCUICContexts]
map_subst_app_decomp [lemma, in MetaCoq.PCUIC.PCUICContexts]
map_subst_app_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICContexts]
map_subst_instance_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICContexts]
map_optimize_repeat_box [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
map_repeat [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
map_vass_map_def [lemma, in MetaCoq.Template.LiftSubst]
map_non_nil [lemma, in MetaCoq.Template.LiftSubst]
map_branches_k_map_branches_k [lemma, in MetaCoq.Template.LiftSubst]
map_bcontext_redl [lemma, in MetaCoq.PCUIC.PCUICReduction]
map_inj [lemma, in MetaCoq.PCUIC.PCUICReduction]
map_decomp_recomp' [lemma, in MetaCoq.PCUIC.PCUICReduction]
map_decomp_recomp [lemma, in MetaCoq.PCUIC.PCUICReduction]
map_recomp_decomp' [lemma, in MetaCoq.PCUIC.PCUICReduction]
map_recomp_decomp [lemma, in MetaCoq.PCUIC.PCUICReduction]
map_subst_lift1 [lemma, in MetaCoq.PCUIC.PCUICSpine]
map_subst_extended_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
map_subst_extended_subst_lift_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICSpine]
map2 [definition, in MetaCoq.Template.utils.MCList]
Map2Bias [section, in MetaCoq.PCUIC.TemplateToPCUIC]
map2i [definition, in MetaCoq.Template.utils.MCList]
map2i_ext [lemma, in MetaCoq.Template.utils.MCList]
map2i_rec [definition, in MetaCoq.Template.utils.MCList]
map2_app [lemma, in MetaCoq.Template.utils.All_Forall]
map2_trans [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_eq [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map2_Proper [instance, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map2_map_map [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_alpha_eq [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_alpha [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
map2_length [lemma, in MetaCoq.Template.utils.MCList]
map2_mapi [lemma, in MetaCoq.Template.utils.MCList]
map2_ext [lemma, in MetaCoq.Template.utils.MCList]
map2_cst [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map2_set_binder_name_context_assumptions [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map2_trans [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map2_map_map [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
map2_trans [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map2_set_binder_name_eq [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map2_Proper [instance, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map2_map_map [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
map2_set_binder_name_context_assumptions [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
map2_length [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
map2_map2_bias_left [lemma, in MetaCoq.PCUIC.TemplateToPCUIC]
map2_bias_left_length [lemma, in MetaCoq.PCUIC.TemplateToPCUIC]
map2_bias_left [definition, in MetaCoq.PCUIC.TemplateToPCUIC]
map2_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
map2_map_left [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
map2_map [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
map2_set_binder_name_alpha_eq [lemma, in MetaCoq.PCUIC.PCUICCasesContexts]
map2_set_binder_name_expand_lets [lemma, in MetaCoq.PCUIC.PCUICSR]
map2_set_binder_name_map [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map2_map_r [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map2_set_binder_name_fold [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
map2_set_binder_name_alpha_eq [lemma, in MetaCoq.PCUIC.PCUICContexts]
map2_set_binder_name_alpha [lemma, in MetaCoq.PCUIC.PCUICContexts]
max_name_length_ge [lemma, in MetaCoq.SafeChecker.PCUICConsistency]
max_name_length [definition, in MetaCoq.SafeChecker.PCUICConsistency]
max:7 [binder, in MetaCoq.Template.utils.MCArith]
maybe_string_of_list [definition, in MetaCoq.Erasure.EAstUtils]
MCArith [library]
MCCompare [library]
MCEquality [library]
MCList [library]
MCMonadNotation [module, in MetaCoq.Template.monad_utils]
_ ;; _ (monad_scope) [notation, in MetaCoq.Template.monad_utils]
' _ <- _ ;; _ (monad_scope) [notation, in MetaCoq.Template.monad_utils]
_ <- _ ;; _ (monad_scope) [notation, in MetaCoq.Template.monad_utils]
mlet ' _ <- _ ;; _ (monad_scope) [notation, in MetaCoq.Template.monad_utils]
mlet _ <- _ ;; _ (monad_scope) [notation, in MetaCoq.Template.monad_utils]
_ =<< _ (monad_scope) [notation, in MetaCoq.Template.monad_utils]
_ >>= _ (monad_scope) [notation, in MetaCoq.Template.monad_utils]
MCOption [library]
MCPred [library]
MCPrelude [library]
MCProd [library]
MCReflect [library]
MCRelations [library]
MCSquash [library]
MCString [library]
MCUtils [library]
MC_ExtrOCamlZPosInt [library]
MC_ExtrOCamlNatInt [library]
MC_ExtrOCamlInt63 [library]
mdeclvar:712 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdeclvar:801 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdeclvar:950 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdeclvar:976 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl':111 [binder, in MetaCoq.Erasure.EDeps]
mdecl':125 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
mdecl':13 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl':143 [binder, in MetaCoq.Erasure.EDeps]
mdecl':208 [binder, in MetaCoq.Erasure.Extract]
mdecl':21 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl':213 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':214 [binder, in MetaCoq.Erasure.Extract]
mdecl':224 [binder, in MetaCoq.Erasure.Extract]
mdecl':307 [binder, in MetaCoq.Erasure.EArities]
mdecl':317 [binder, in MetaCoq.Erasure.EArities]
mdecl':346 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':358 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':41 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl':444 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':451 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':461 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':473 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':484 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':497 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':7 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl':752 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':832 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':839 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':848 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':868 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':92 [binder, in MetaCoq.Erasure.EDeps]
mdecl':99 [binder, in MetaCoq.Erasure.EDeps]
mdecl:1 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:1 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:10 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:10 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:10 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:10 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
mdecl:100 [binder, in MetaCoq.Erasure.EArities]
mdecl:100 [binder, in MetaCoq.Template.WfAst]
mdecl:1000 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:1008 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:102 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:1029 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:103 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:1036 [binder, in MetaCoq.Template.Typing]
mdecl:104 [binder, in MetaCoq.PCUIC.PCUICInversion]
mdecl:104 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:104 [binder, in MetaCoq.Template.TypingWf]
mdecl:1046 [binder, in MetaCoq.Template.Typing]
mdecl:105 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:1060 [binder, in MetaCoq.Template.Typing]
mdecl:107 [binder, in MetaCoq.Erasure.EDeps]
mdecl:107 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:1077 [binder, in MetaCoq.Template.Typing]
mdecl:1079 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:109 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:109 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:109 [binder, in MetaCoq.Template.TypingWf]
mdecl:11 [binder, in MetaCoq.Erasure.ESubstitution]
mdecl:11 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:11 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
mdecl:11 [binder, in MetaCoq.Erasure.ErasureFunction]
mdecl:110 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:110 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:1100 [binder, in MetaCoq.PCUIC.PCUICConversion]
mdecl:1107 [binder, in MetaCoq.PCUIC.PCUICConversion]
mdecl:112 [binder, in MetaCoq.PCUIC.PCUICInversion]
mdecl:113 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:114 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
mdecl:114 [binder, in MetaCoq.Erasure.EInlineProjections]
mdecl:114 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
mdecl:115 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:115 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:116 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:117 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:117 [binder, in MetaCoq.Template.TypingWf]
mdecl:118 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mdecl:119 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
mdecl:12 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:12 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:12 [binder, in MetaCoq.Erasure.EExtends]
mdecl:120 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
mdecl:121 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:123 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:123 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mdecl:123 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
mdecl:123 [binder, in MetaCoq.Erasure.Prelim]
mdecl:124 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:124 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:124 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:127 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
mdecl:1270 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mdecl:1286 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:129 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:129 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:13 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:13 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:13 [binder, in MetaCoq.Examples.add_constructor]
mdecl:130 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:130 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:131 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:131 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mdecl:131 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:131 [binder, in MetaCoq.Template.WcbvEval]
mdecl:132 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:133 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:1336 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:134 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:135 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:138 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:139 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:139 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:139 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:139 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:14 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:14 [binder, in MetaCoq.Erasure.ErasureFunction]
mdecl:14 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
mdecl:141 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:141 [binder, in MetaCoq.Erasure.EDeps]
mdecl:141 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:141 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:142 [binder, in MetaCoq.PCUIC.PCUICInversion]
mdecl:143 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:143 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:144 [binder, in MetaCoq.Erasure.ErasureProperties]
mdecl:145 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
mdecl:145 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
mdecl:145 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:146 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mdecl:147 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:147 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:147 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:150 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:150 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mdecl:150 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:151 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:151 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:151 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mdecl:151 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
mdecl:153 [binder, in MetaCoq.PCUIC.PCUICInversion]
mdecl:155 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:156 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mdecl:158 [binder, in MetaCoq.Template.TypingWf]
mdecl:159 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
mdecl:161 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:162 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:163 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:163 [binder, in MetaCoq.Template.WcbvEval]
mdecl:164 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:164 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:164 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:164 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:165 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:165 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:165 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:165 [binder, in MetaCoq.Template.Typing]
mdecl:165 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:166 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:166 [binder, in MetaCoq.Template.TypingWf]
mdecl:167 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:168 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:169 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:169 [binder, in MetaCoq.Template.TypingWf]
mdecl:17 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:17 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:17 [binder, in MetaCoq.Erasure.EExtends]
mdecl:172 [binder, in MetaCoq.Template.TypingWf]
mdecl:173 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:175 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:177 [binder, in MetaCoq.Template.TypingWf]
mdecl:178 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:178 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:179 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:18 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:18 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:180 [binder, in MetaCoq.PCUIC.PCUICArities]
mdecl:180 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:181 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mdecl:181 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:181 [binder, in MetaCoq.Template.TypingWf]
mdecl:182 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:182 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:182 [binder, in MetaCoq.Template.WcbvEval]
mdecl:183 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:183 [binder, in MetaCoq.Template.Typing]
mdecl:184 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:185 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:187 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:187 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:188 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:188 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:188 [binder, in MetaCoq.Template.TypingWf]
mdecl:189 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:19 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:190 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:190 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:190 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:191 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mdecl:191 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:192 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:193 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:193 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:194 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:194 [binder, in MetaCoq.PCUIC.PCUICArities]
mdecl:194 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:194 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:197 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:198 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:198 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:2 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:20 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:20 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:20 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
mdecl:20 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:20 [binder, in MetaCoq.Erasure.EEnvMap]
mdecl:200 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:201 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:202 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:204 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:204 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:205 [binder, in MetaCoq.Erasure.Extract]
mdecl:206 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:207 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:208 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:209 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:21 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mdecl:210 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:210 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:210 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:212 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:212 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:212 [binder, in MetaCoq.Erasure.Extract]
mdecl:212 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:213 [binder, in MetaCoq.Template.TypingWf]
mdecl:214 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:214 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:215 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:216 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:217 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:218 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:218 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:219 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:219 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:22 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
mdecl:22 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:220 [binder, in MetaCoq.Erasure.Extract]
mdecl:222 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:223 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:224 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:225 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:225 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:225 [binder, in MetaCoq.Template.WcbvEval]
mdecl:225 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:226 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:226 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:227 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:231 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:232 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:232 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:233 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:233 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mdecl:2353 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mdecl:236 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:238 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:238 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:238 [binder, in MetaCoq.Template.TypingWf]
mdecl:239 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:239 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:240 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:243 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:244 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:245 [binder, in MetaCoq.Template.EtaExpand]
mdecl:248 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:248 [binder, in MetaCoq.Template.WcbvEval]
mdecl:25 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:251 [binder, in MetaCoq.Template.EtaExpand]
mdecl:252 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:256 [binder, in MetaCoq.Template.EtaExpand]
mdecl:257 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:258 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
mdecl:259 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:259 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:26 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mdecl:262 [binder, in MetaCoq.Template.Typing]
mdecl:263 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
mdecl:267 [binder, in MetaCoq.Erasure.EWcbvEval]
mdecl:27 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:271 [binder, in MetaCoq.Template.TypingWf]
mdecl:278 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:28 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
mdecl:28 [binder, in MetaCoq.Erasure.ErasureCorrectness]
mdecl:28 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
mdecl:28 [binder, in MetaCoq.Erasure.EEnvMap]
mdecl:281 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:281 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:283 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:288 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:291 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:294 [binder, in MetaCoq.Template.TypingWf]
mdecl:296 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:299 [binder, in MetaCoq.Template.TypingWf]
mdecl:30 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:301 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:301 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:305 [binder, in MetaCoq.Erasure.EArities]
mdecl:305 [binder, in MetaCoq.Template.TypingWf]
mdecl:309 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:31 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:312 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:312 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:314 [binder, in MetaCoq.Erasure.EArities]
mdecl:315 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:316 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:317 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
mdecl:323 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:323 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:323 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:327 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:328 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:329 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:33 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:332 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:332 [binder, in MetaCoq.Template.Ast]
mdecl:332 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:334 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:337 [binder, in MetaCoq.Erasure.EArities]
mdecl:34 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mdecl:340 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:341 [binder, in MetaCoq.Template.Ast]
mdecl:341 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:343 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:344 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:344 [binder, in MetaCoq.Template.Typing]
mdecl:344 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:345 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:346 [binder, in MetaCoq.Template.Ast]
mdecl:348 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:349 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:35 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:352 [binder, in MetaCoq.Template.Ast]
mdecl:356 [binder, in MetaCoq.Template.Ast]
mdecl:359 [binder, in MetaCoq.Template.Ast]
mdecl:359 [binder, in MetaCoq.Erasure.ERemoveParams]
mdecl:36 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:362 [binder, in MetaCoq.Template.Typing]
mdecl:365 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:365 [binder, in MetaCoq.Template.Ast]
mdecl:37 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
mdecl:37 [binder, in MetaCoq.Template.WfAst]
mdecl:37 [binder, in MetaCoq.Erasure.EEnvMap]
mdecl:370 [binder, in MetaCoq.Template.Ast]
mdecl:371 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:378 [binder, in MetaCoq.Template.Ast]
mdecl:38 [binder, in MetaCoq.PCUIC.PCUICArities]
mdecl:38 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:384 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:384 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:384 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:384 [binder, in MetaCoq.Template.Ast]
mdecl:385 [binder, in MetaCoq.Erasure.ERemoveParams]
mdecl:39 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:39 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:390 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:390 [binder, in MetaCoq.Erasure.ERemoveParams]
mdecl:395 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:397 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:399 [binder, in MetaCoq.Template.Ast]
mdecl:4 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:4 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:40 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:40 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:40 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:40 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:401 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:401 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:404 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:406 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:406 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:407 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:409 [binder, in MetaCoq.Template.EtaExpand]
mdecl:409 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:41 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:41 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
mdecl:41 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:410 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:413 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:414 [binder, in MetaCoq.Erasure.ERemoveParams]
mdecl:417 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:417 [binder, in MetaCoq.Erasure.ERemoveParams]
mdecl:419 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:42 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:42 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
mdecl:42 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:42 [binder, in MetaCoq.PCUIC.PCUICContexts]
mdecl:420 [binder, in MetaCoq.Template.EtaExpand]
mdecl:420 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:420 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:425 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:425 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:427 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:428 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:43 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:43 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:43 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
mdecl:432 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:439 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:44 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:44 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:44 [binder, in MetaCoq.Erasure.EEnvMap]
mdecl:440 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:441 [binder, in MetaCoq.PCUIC.PCUICProgress]
mdecl:446 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:449 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:45 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:45 [binder, in MetaCoq.Template.WcbvEval]
mdecl:45 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:454 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:457 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:459 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:467 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:468 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:47 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:47 [binder, in MetaCoq.Erasure.EWellformed]
mdecl:47 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:47 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:473 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:473 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:477 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:488 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:490 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:50 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:50 [binder, in MetaCoq.Erasure.EEnvMap]
mdecl:50 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:50 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
mdecl:50 [binder, in MetaCoq.PCUIC.PCUICContexts]
mdecl:501 [binder, in MetaCoq.Template.EtaExpand]
mdecl:51 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:51 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:510 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:52 [binder, in MetaCoq.Template.WfAst]
mdecl:52 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:52 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
mdecl:52 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:533 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:535 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:537 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:539 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:54 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:542 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:543 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:546 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:549 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:55 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:55 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:55 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:55 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:553 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:556 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:557 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:559 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:561 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:564 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:567 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:57 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:572 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:574 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:574 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:574 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:578 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:58 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
mdecl:58 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:58 [binder, in MetaCoq.PCUIC.PCUICContexts]
mdecl:58 [binder, in MetaCoq.Erasure.EGenericMapEnv]
mdecl:581 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:584 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:586 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:59 [binder, in MetaCoq.Erasure.EEnvMap]
mdecl:590 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:597 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:6 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
mdecl:6 [binder, in MetaCoq.Template.Typing]
mdecl:6 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:60 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:60 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:61 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:61 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:611 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:617 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:622 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:626 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:626 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:634 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:638 [binder, in MetaCoq.Template.Typing]
mdecl:64 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:64 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:641 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:642 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:644 [binder, in MetaCoq.Template.Typing]
mdecl:645 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:648 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:649 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:65 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:65 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:65 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:652 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:654 [binder, in MetaCoq.Template.Typing]
mdecl:659 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:66 [binder, in MetaCoq.Template.EtaExpand]
mdecl:66 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:66 [binder, in MetaCoq.Erasure.EArities]
mdecl:66 [binder, in MetaCoq.PCUIC.PCUICValidity]
mdecl:666 [binder, in MetaCoq.Template.Typing]
mdecl:668 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:669 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:67 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:670 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:672 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:673 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:68 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:680 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:682 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:69 [binder, in MetaCoq.Template.EtaExpand]
mdecl:69 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:69 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:69 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:69 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:698 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:698 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:70 [binder, in MetaCoq.PCUIC.PCUICElimination]
mdecl:702 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:708 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:71 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:71 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:71 [binder, in MetaCoq.Template.WcbvEval]
mdecl:713 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:716 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:72 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:72 [binder, in MetaCoq.Template.EtaExpand]
mdecl:72 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:726 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:728 [binder, in MetaCoq.PCUIC.PCUICSR]
mdecl:73 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:736 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:743 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:75 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:75 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:75 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:750 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:76 [binder, in MetaCoq.Erasure.EAst]
mdecl:768 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:77 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:77 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:770 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:773 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:773 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:78 [binder, in MetaCoq.PCUIC.PCUICInductives]
mdecl:791 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:794 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:80 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:80 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:806 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:819 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:823 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:829 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:83 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:83 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:830 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:835 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:84 [binder, in MetaCoq.Erasure.Prelim]
mdecl:844 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:85 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:856 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:86 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:864 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:866 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:88 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:880 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:882 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:89 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:89 [binder, in MetaCoq.Erasure.EDeps]
mdecl:89 [binder, in MetaCoq.Template.WcbvEval]
mdecl:891 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:897 [binder, in MetaCoq.PCUIC.PCUICTyping]
mdecl:9 [binder, in MetaCoq.Erasure.EInlineProjections]
mdecl:9 [binder, in MetaCoq.Template.EnvironmentTyping]
mdecl:90 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:90 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:901 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:907 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:91 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:914 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:92 [binder, in MetaCoq.Erasure.Prelim]
mdecl:922 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:925 [binder, in MetaCoq.Erasure.ErasureFunction]
mdecl:929 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:939 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:939 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:945 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:947 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:948 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:95 [binder, in MetaCoq.Template.Typing]
mdecl:957 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:96 [binder, in MetaCoq.Erasure.EGlobalEnv]
mdecl:96 [binder, in MetaCoq.Template.TypingWf]
mdecl:962 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:963 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:969 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:97 [binder, in MetaCoq.Erasure.EDeps]
mdecl:97 [binder, in MetaCoq.PCUIC.PCUICInversion]
mdecl:97 [binder, in MetaCoq.Erasure.Prelim]
mdecl:975 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:979 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:98 [binder, in MetaCoq.Erasure.ESubstitution]
mdecl:988 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:991 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
md:1023 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
md:17 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
md:28 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
md:51 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
Measure [section, in MetaCoq.SafeChecker.PCUICSafeReduce]
metacoq_tour [library]
metacoq_tour_prelude [library]
meta_conv_all [lemma, in MetaCoq.PCUIC.PCUICTyping]
meta_conv_term [lemma, in MetaCoq.PCUIC.PCUICTyping]
meta_conv [lemma, in MetaCoq.PCUIC.PCUICTyping]
ME:19 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
ME:71 [binder, in MetaCoq.Template.monad_utils]
mFix [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfixctx:125 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:585 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:608 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:617 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:622 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:629 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:639 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixi:1050 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfixi:1055 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfixi:1121 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfixi:1126 [binder, in MetaCoq.PCUIC.PCUICReduction]
mFixMfixMismatch [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfixpoint [definition, in MetaCoq.Template.BasicAst]
mfixpoint [definition, in MetaCoq.Erasure.EAst]
mfixpoint_size [definition, in MetaCoq.Examples.tauto]
mfixpoint_size [definition, in MetaCoq.PCUIC.utils.PCUICSize]
mfixpoint_depth_nth_error [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfixpoint_depth_In [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfixpoint_depth [abbreviation, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfixpoint_depth_gen [definition, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mFixRargMismatch [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix_hole_context [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix_hole [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mFix_mfix [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix'':734 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix'':739 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix'':756 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix'':761 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':10 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
mfix':100 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix':101 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix':1012 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':1017 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':103 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix':1038 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':1046 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':1062 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':107 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix':1083 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':1088 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':11 [binder, in MetaCoq.PCUIC.PCUICCSubst]
mfix':11 [binder, in MetaCoq.Erasure.ELiftSubst]
mfix':11 [binder, in MetaCoq.Template.WcbvEval]
mfix':11 [binder, in MetaCoq.PCUIC.PCUICToTemplate]
mfix':11 [binder, in MetaCoq.Erasure.ECSubst]
mfix':1109 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':1117 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix':112 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix':127 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix':13 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':131 [binder, in MetaCoq.Template.TermEquality]
mfix':131 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix':133 [binder, in MetaCoq.Erasure.Extract]
mfix':136 [binder, in MetaCoq.Template.TermEquality]
mfix':142 [binder, in MetaCoq.Erasure.Extract]
mfix':143 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix':150 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix':153 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix':157 [binder, in MetaCoq.Template.Checker]
mfix':159 [binder, in MetaCoq.Template.Checker]
mfix':163 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix':166 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix':166 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':171 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':172 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix':174 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix':175 [binder, in MetaCoq.PCUIC.PCUICEquality]
mfix':176 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':18 [binder, in MetaCoq.Erasure.EInlineProjections]
mfix':180 [binder, in MetaCoq.PCUIC.PCUICEquality]
mfix':181 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':183 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix':185 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix':19 [binder, in MetaCoq.Erasure.EInlineProjections]
mfix':1945 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':20 [binder, in MetaCoq.Erasure.ELiftSubst]
mfix':200 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':201 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':205 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':2126 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':2140 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':219 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':22 [binder, in MetaCoq.Erasure.ELiftSubst]
mfix':224 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':227 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix':228 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix':229 [binder, in MetaCoq.Template.Ast]
mfix':229 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':231 [binder, in MetaCoq.Template.Ast]
mfix':234 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':239 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':241 [binder, in MetaCoq.Template.Ast]
mfix':243 [binder, in MetaCoq.Template.Ast]
mfix':263 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':267 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix':268 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix':273 [binder, in MetaCoq.Template.Ast]
mfix':274 [binder, in MetaCoq.Template.Ast]
mfix':277 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':30 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':31 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':317 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':324 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':33 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':35 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
mfix':374 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix':404 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':408 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix':417 [binder, in MetaCoq.Erasure.ErasureFunction]
mfix':419 [binder, in MetaCoq.Erasure.ErasureFunction]
mfix':42 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':425 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':43 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
mfix':44 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
mfix':474 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':476 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':480 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':49 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mfix':497 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix':505 [binder, in MetaCoq.Template.Typing]
mfix':51 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':514 [binder, in MetaCoq.Template.Typing]
mfix':524 [binder, in MetaCoq.Template.Typing]
mfix':53 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mfix':541 [binder, in MetaCoq.Template.Typing]
mfix':550 [binder, in MetaCoq.Template.Typing]
mfix':560 [binder, in MetaCoq.Template.Typing]
mfix':571 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':575 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':589 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix':6 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':60 [binder, in MetaCoq.Erasure.Extract]
mfix':60 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':609 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix':618 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix':65 [binder, in MetaCoq.Erasure.Extract]
mfix':677 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':687 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':694 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':7 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
mfix':702 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':708 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':715 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':721 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':730 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':74 [binder, in MetaCoq.Translations.param_cheap_packed]
mfix':76 [binder, in MetaCoq.Translations.param_cheap_packed]
mfix':768 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':774 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix':8 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
mfix':8 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
mfix':86 [binder, in MetaCoq.Template.AstUtils]
mfix':87 [binder, in MetaCoq.Template.AstUtils]
mfix':9 [binder, in MetaCoq.PCUIC.PCUICExpandLets]
mfix':9 [binder, in MetaCoq.PCUIC.PCUICCSubst]
mfix':9 [binder, in MetaCoq.Erasure.ELiftSubst]
mfix':9 [binder, in MetaCoq.Template.WcbvEval]
mfix':9 [binder, in MetaCoq.Erasure.ECSubst]
mfix':92 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix':94 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':98 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix':99 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':991 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:101 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1055 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:111 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1125 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1140 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1151 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:121 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:128 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:135 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:142 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:202 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:204 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:215 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:216 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:224 [binder, in MetaCoq.Template.Typing]
mfix0:228 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:229 [binder, in MetaCoq.Template.Typing]
mfix0:234 [binder, in MetaCoq.Template.Typing]
mfix0:239 [binder, in MetaCoq.Template.Typing]
mfix0:260 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:274 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:276 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:280 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:294 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:300 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:306 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:312 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix0:382 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:395 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:401 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:410 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:417 [binder, in MetaCoq.Template.Typing]
mfix0:422 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:423 [binder, in MetaCoq.Template.Typing]
mfix0:429 [binder, in MetaCoq.Template.Typing]
mfix0:435 [binder, in MetaCoq.Template.Typing]
mfix0:473 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:474 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix0:475 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:480 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix0:481 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:486 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix0:492 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix0:494 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix0:79 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:90 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1':101 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix1':121 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix1':1517 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1':1776 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:1028 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1030 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:105 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1056 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:112 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1126 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1141 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1152 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:117 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix1:122 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:129 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:136 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:143 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:1513 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:16 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:170 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix1:1766 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:1772 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:184 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix1:203 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:205 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:216 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:217 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:225 [binder, in MetaCoq.Template.Typing]
mfix1:229 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:23 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:230 [binder, in MetaCoq.Template.Typing]
mfix1:235 [binder, in MetaCoq.Template.Typing]
mfix1:240 [binder, in MetaCoq.Template.Typing]
mfix1:261 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:275 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:276 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix1:277 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:281 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:282 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix1:295 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:301 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:307 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:313 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix1:32 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:383 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:396 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:402 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:409 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix1:411 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:418 [binder, in MetaCoq.Template.Typing]
mfix1:423 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:424 [binder, in MetaCoq.Template.Typing]
mfix1:430 [binder, in MetaCoq.Template.Typing]
mfix1:436 [binder, in MetaCoq.Template.Typing]
mfix1:474 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:475 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:476 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:480 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix1:481 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:482 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:487 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:493 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:495 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix1:502 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix1:55 [binder, in MetaCoq.Erasure.Prelim]
mfix1:6 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix1:66 [binder, in MetaCoq.Erasure.Prelim]
mfix1:84 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:91 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:97 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix2':102 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix2':122 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix2':1518 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2':1777 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:118 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix2:1514 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:1767 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:1773 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:407 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix2:478 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix2:500 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix2:98 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix:10 [binder, in MetaCoq.Erasure.Erasure]
mfix:100 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:100 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:101 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:1010 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:1014 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:1015 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:1017 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:102 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:102 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:102 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:1020 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:1021 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:1024 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:103 [binder, in MetaCoq.Template.WcbvEval]
mfix:103 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:1036 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:104 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:104 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:1045 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:105 [binder, in MetaCoq.Template.Typing]
mfix:105 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:105 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix:106 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
mfix:1060 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:107 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:1081 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:1086 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:1087 [binder, in MetaCoq.Template.Typing]
mfix:109 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:109 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix:109 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:1095 [binder, in MetaCoq.Template.Typing]
mfix:11 [binder, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
mfix:110 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:1107 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:111 [binder, in MetaCoq.Template.WcbvEval]
mfix:1116 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:1116 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:1119 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:112 [binder, in MetaCoq.Template.Typing]
mfix:112 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:116 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:116 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:117 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:118 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mfix:119 [binder, in MetaCoq.Template.Typing]
mfix:119 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:12 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:120 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:121 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix:121 [binder, in MetaCoq.Template.WcbvEval]
mfix:123 [binder, in MetaCoq.PCUIC.PCUICAst]
mfix:125 [binder, in MetaCoq.Erasure.EArities]
mfix:125 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix:126 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:127 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:127 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
mfix:127 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:128 [binder, in MetaCoq.Erasure.EGlobalEnv]
mfix:129 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix:129 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mfix:130 [binder, in MetaCoq.Template.EtaExpand]
mfix:130 [binder, in MetaCoq.Template.TermEquality]
mfix:130 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mfix:130 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:131 [binder, in MetaCoq.Erasure.Extract]
mfix:134 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:134 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mfix:135 [binder, in MetaCoq.Template.TermEquality]
mfix:135 [binder, in MetaCoq.Erasure.EGlobalEnv]
mfix:135 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix:136 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mfix:136 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix:137 [binder, in MetaCoq.Erasure.EGlobalEnv]
mfix:137 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix:138 [binder, in MetaCoq.Template.EtaExpand]
mfix:139 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mfix:139 [binder, in MetaCoq.Erasure.EGlobalEnv]
mfix:14 [binder, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
mfix:140 [binder, in MetaCoq.Erasure.Extract]
mfix:140 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:141 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix:141 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:1415 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:142 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:142 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:142 [binder, in MetaCoq.Erasure.ERemoveParams]
mfix:143 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:145 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:145 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mfix:145 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:146 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:147 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:147 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
mfix:148 [binder, in MetaCoq.Erasure.EGlobalEnv]
mfix:148 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:149 [binder, in MetaCoq.Erasure.EGlobalEnv]
mfix:15 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix:152 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:152 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:153 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:153 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:154 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:154 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:154 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mfix:155 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:155 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:158 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:159 [binder, in MetaCoq.PCUIC.PCUICInversion]
mfix:16 [binder, in MetaCoq.Template.Typing]
mfix:16 [binder, in MetaCoq.Template.WcbvEval]
mfix:160 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:167 [binder, in MetaCoq.PCUIC.PCUICInversion]
mfix:168 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:168 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:169 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:169 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:171 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:172 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:174 [binder, in MetaCoq.PCUIC.PCUICEquality]
mfix:174 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mfix:179 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:179 [binder, in MetaCoq.PCUIC.PCUICEquality]
mfix:18 [binder, in MetaCoq.Template.WcbvEval]
mfix:181 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:182 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:183 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:185 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:187 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mfix:187 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:188 [binder, in MetaCoq.Template.WcbvEval]
mfix:19 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:19 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:190 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:190 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:192 [binder, in MetaCoq.PCUIC.PCUICProgress]
mfix:1941 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:195 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:197 [binder, in MetaCoq.Template.WcbvEval]
mfix:198 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:200 [binder, in MetaCoq.PCUIC.PCUICProgress]
mfix:203 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mfix:204 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:204 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:205 [binder, in MetaCoq.Template.WcbvEval]
mfix:207 [binder, in MetaCoq.Template.Checker]
mfix:207 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:208 [binder, in MetaCoq.Template.EtaExpand]
mfix:209 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:21 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mfix:212 [binder, in MetaCoq.Template.Ast]
mfix:2123 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:2137 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:214 [binder, in MetaCoq.Template.Ast]
mfix:215 [binder, in MetaCoq.Template.WcbvEval]
mfix:217 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:218 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:22 [binder, in MetaCoq.Template.Normal]
mfix:22 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix:22 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:220 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:221 [binder, in MetaCoq.Template.EtaExpand]
mfix:222 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:223 [binder, in MetaCoq.Erasure.ErasureFunction]
mfix:225 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:227 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:227 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
mfix:227 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:228 [binder, in MetaCoq.Erasure.ErasureFunction]
mfix:228 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
mfix:229 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:23 [binder, in MetaCoq.Template.Typing]
mfix:231 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:231 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:232 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:233 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:237 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:238 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:24 [binder, in MetaCoq.Template.Normal]
mfix:240 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:242 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:242 [binder, in MetaCoq.Erasure.EEtaExpanded]
mfix:243 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:243 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:243 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:243 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:244 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:244 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:245 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:247 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:248 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:25 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
mfix:25 [binder, in MetaCoq.Erasure.ESpineView]
mfix:25 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mfix:250 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:250 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:251 [binder, in MetaCoq.Template.WcbvEval]
mfix:253 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:254 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:255 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:255 [binder, in MetaCoq.Template.WcbvEval]
mfix:257 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:258 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:26 [binder, in MetaCoq.Template.TypingWf]
mfix:264 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:266 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:266 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:267 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:27 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:27 [binder, in MetaCoq.Template.Typing]
mfix:27 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:27 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:27 [binder, in MetaCoq.Erasure.ESpineView]
mfix:27 [binder, in MetaCoq.Erasure.EWellformed]
mfix:27 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:271 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:273 [binder, in MetaCoq.Template.Typing]
mfix:273 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:274 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:275 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:276 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:276 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:279 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:28 [binder, in MetaCoq.Template.Typing]
mfix:28 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:28 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:281 [binder, in MetaCoq.Template.Typing]
mfix:282 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:286 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:287 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:289 [binder, in MetaCoq.Template.Typing]
mfix:289 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:29 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:29 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:290 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:292 [binder, in MetaCoq.Template.EtaExpand]
mfix:292 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:293 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:298 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:298 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:30 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
mfix:30 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:30 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:30 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
mfix:30 [binder, in MetaCoq.Erasure.ESpineView]
mfix:30 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:301 [binder, in MetaCoq.Template.EtaExpand]
mfix:301 [binder, in MetaCoq.Template.WcbvEval]
mfix:302 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:303 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mfix:305 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:308 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mfix:31 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix:316 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:32 [binder, in MetaCoq.Template.Typing]
mfix:32 [binder, in MetaCoq.Erasure.ESpineView]
mfix:32 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:323 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:323 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:324 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:327 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:33 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:33 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:33 [binder, in MetaCoq.Template.TypingWf]
mfix:330 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:330 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:330 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:330 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:331 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:332 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:332 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:333 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:335 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:336 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:336 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:337 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:338 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix:339 [binder, in MetaCoq.Erasure.EArities]
mfix:34 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
mfix:34 [binder, in MetaCoq.Erasure.EInlineProjections]
mfix:341 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix:342 [binder, in MetaCoq.PCUIC.PCUICProgress]
mfix:342 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:344 [binder, in MetaCoq.Erasure.EArities]
mfix:35 [binder, in MetaCoq.Erasure.EInlineProjections]
mfix:350 [binder, in MetaCoq.PCUIC.PCUICProgress]
mfix:351 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:353 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:357 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:358 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:36 [binder, in MetaCoq.Erasure.EInlineProjections]
mfix:36 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:36 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:36 [binder, in MetaCoq.PCUIC.PCUICReduction]
mfix:361 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:362 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix:363 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:364 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:366 [binder, in MetaCoq.PCUIC.PCUICProgress]
mfix:367 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:370 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:370 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix:371 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:372 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:372 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:373 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:375 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:376 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:377 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:378 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix:38 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:381 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:381 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:383 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:386 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:389 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:39 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:39 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:397 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:4 [binder, in MetaCoq.SafeChecker.Extraction]
mfix:40 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:40 [binder, in MetaCoq.Erasure.EInlineProjections]
mfix:407 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:407 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:419 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:42 [binder, in MetaCoq.Erasure.EWellformed]
mfix:426 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:427 [binder, in MetaCoq.Template.EtaExpand]
mfix:428 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:43 [binder, in MetaCoq.Template.WfAst]
mfix:433 [binder, in MetaCoq.Template.EtaExpand]
mfix:433 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:438 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:44 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:44 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:443 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:445 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:448 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:449 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:45 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:45 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:45 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:453 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:454 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:458 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:46 [binder, in MetaCoq.Template.WfAst]
mfix:46 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:463 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:469 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:472 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:473 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:477 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:479 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:479 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:48 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mfix:485 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:489 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:49 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:49 [binder, in MetaCoq.Erasure.Prelim]
mfix:493 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:494 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:5 [binder, in MetaCoq.PCUIC.PCUICSR]
mfix:5 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:50 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:500 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:500 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:503 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:504 [binder, in MetaCoq.Template.Typing]
mfix:505 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:51 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:51 [binder, in MetaCoq.Erasure.Prelim]
mfix:510 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:510 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:511 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:512 [binder, in MetaCoq.Template.Typing]
mfix:512 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:513 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:513 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:514 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:52 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:52 [binder, in MetaCoq.PCUIC.PCUICAlpha]
mfix:520 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:520 [binder, in MetaCoq.Template.Typing]
mfix:521 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:522 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:523 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:526 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:528 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:529 [binder, in MetaCoq.Template.Typing]
mfix:53 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mfix:532 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:535 [binder, in MetaCoq.Template.Typing]
mfix:536 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:540 [binder, in MetaCoq.Template.Typing]
mfix:548 [binder, in MetaCoq.Template.Typing]
mfix:556 [binder, in MetaCoq.Template.Typing]
mfix:565 [binder, in MetaCoq.Template.Typing]
mfix:569 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:57 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mfix:571 [binder, in MetaCoq.Template.Typing]
mfix:573 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:58 [binder, in MetaCoq.Erasure.Extract]
mfix:58 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:58 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:580 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:584 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:585 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:589 [binder, in MetaCoq.Template.Typing]
mfix:59 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:592 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:596 [binder, in MetaCoq.Template.Typing]
mfix:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:60 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:60 [binder, in MetaCoq.Erasure.Prelim]
mfix:606 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix:609 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:609 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
mfix:61 [binder, in MetaCoq.Template.Normal]
mfix:61 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mfix:62 [binder, in MetaCoq.Erasure.Prelim]
mfix:622 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:629 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:63 [binder, in MetaCoq.Erasure.Extract]
mfix:63 [binder, in MetaCoq.Template.Normal]
mfix:633 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:634 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:636 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:640 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:643 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:648 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:649 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:652 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:654 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:655 [binder, in MetaCoq.PCUIC.PCUICConfluence]
mfix:66 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:66 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
mfix:672 [binder, in MetaCoq.Template.Typing]
mfix:672 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:672 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:675 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:677 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:678 [binder, in MetaCoq.Template.Typing]
mfix:682 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:683 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:686 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:687 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:69 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:69 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:690 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:693 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:696 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:700 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:704 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:707 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:714 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:72 [binder, in MetaCoq.Erasure.Prelim]
mfix:720 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:729 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:74 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:76 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
mfix:76 [binder, in MetaCoq.Erasure.ErasureProperties]
mfix:767 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:77 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:773 [binder, in MetaCoq.PCUIC.PCUICConversion]
mfix:78 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:789 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:801 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:804 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:83 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:83 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:83 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:835 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:838 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:84 [binder, in MetaCoq.Erasure.EWellformed]
mfix:840 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:840 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:841 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:844 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:849 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:85 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:85 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:851 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:86 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
mfix:86 [binder, in MetaCoq.Erasure.EWellformed]
mfix:862 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:866 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:87 [binder, in MetaCoq.PCUIC.PCUICNormal]
mfix:87 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:88 [binder, in MetaCoq.Erasure.EWellformed]
mfix:88 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:89 [binder, in MetaCoq.SafeChecker.PCUICErrors]
mfix:907 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:91 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:915 [binder, in MetaCoq.PCUIC.PCUICTyping]
mfix:92 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:92 [binder, in MetaCoq.Erasure.EWellformed]
mfix:93 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:93 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:93 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:94 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mfix:94 [binder, in MetaCoq.Template.WcbvEval]
mfix:95 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
mfix:96 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:96 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:96 [binder, in MetaCoq.Erasure.EWcbvEval]
mfix:97 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
mfix:98 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:98 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:989 [binder, in MetaCoq.PCUIC.PCUICReduction]
mib':1439 [binder, in MetaCoq.Erasure.ErasureFunction]
mib':165 [binder, in MetaCoq.Erasure.Extract]
mib':178 [binder, in MetaCoq.Erasure.Extract]
mib':204 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mib':21 [binder, in MetaCoq.Erasure.ErasureCorrectness]
mib':792 [binder, in MetaCoq.Erasure.ErasureFunction]
mib':831 [binder, in MetaCoq.Erasure.ErasureFunction]
mib:100 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
mib:104 [binder, in MetaCoq.Template.Pretty]
mib:108 [binder, in MetaCoq.Template.Pretty]
mib:122 [binder, in MetaCoq.Template.Pretty]
mib:131 [binder, in MetaCoq.Template.AstUtils]
mib:164 [binder, in MetaCoq.Erasure.Extract]
mib:177 [binder, in MetaCoq.Erasure.Extract]
mib:20 [binder, in MetaCoq.Erasure.ErasureCorrectness]
mib:202 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mib:246 [binder, in MetaCoq.Erasure.Extract]
mib:354 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mib:676 [binder, in MetaCoq.Erasure.ErasureFunction]
mib:817 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
mib:830 [binder, in MetaCoq.Erasure.ErasureFunction]
mib:96 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
mie:111 [binder, in MetaCoq.Template.Pretty]
mie:115 [binder, in MetaCoq.Template.Pretty]
mie:125 [binder, in MetaCoq.Template.Pretty]
mie:130 [binder, in MetaCoq.Template.Pretty]
mind_body_to_entry [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mind_entry_private [projection, in MetaCoq.Template.Ast]
mind_entry_variance [projection, in MetaCoq.Template.Ast]
mind_entry_template [projection, in MetaCoq.Template.Ast]
mind_entry_universes [projection, in MetaCoq.Template.Ast]
mind_entry_inds [projection, in MetaCoq.Template.Ast]
mind_entry_params [projection, in MetaCoq.Template.Ast]
mind_entry_finite [projection, in MetaCoq.Template.Ast]
mind_entry_record [projection, in MetaCoq.Template.Ast]
mind_entry_lc [projection, in MetaCoq.Template.Ast]
mind_entry_consnames [projection, in MetaCoq.Template.Ast]
mind_entry_arity [projection, in MetaCoq.Template.Ast]
mind_entry_typename [projection, in MetaCoq.Template.Ast]
mind_entry_private [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_universes [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_inds [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_params [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_finite [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_record [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_lc [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_consnames [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_template [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_arity [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_typename [projection, in MetaCoq.PCUIC.PCUICAst]
mind_entry_private [projection, in MetaCoq.Erasure.EAst]
mind_entry_inds [projection, in MetaCoq.Erasure.EAst]
mind_entry_params [projection, in MetaCoq.Erasure.EAst]
mind_entry_finite [projection, in MetaCoq.Erasure.EAst]
mind_entry_record [projection, in MetaCoq.Erasure.EAst]
mind_entry_lc [projection, in MetaCoq.Erasure.EAst]
mind_entry_consnames [projection, in MetaCoq.Erasure.EAst]
mind_entry_template [projection, in MetaCoq.Erasure.EAst]
mind_entry_arity [projection, in MetaCoq.Erasure.EAst]
mind_entry_typename [projection, in MetaCoq.Erasure.EAst]
mind_body_to_entry [definition, in MetaCoq.Template.AstUtils]
mind':152 [binder, in MetaCoq.Erasure.EDeps]
mind:10 [binder, in MetaCoq.Template.Typing]
mind:101 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mind:1029 [binder, in MetaCoq.Erasure.ErasureFunction]
mind:109 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:11 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mind:11 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:11 [binder, in MetaCoq.PCUIC.PCUICProgram]
mind:118 [binder, in MetaCoq.Template.AstUtils]
mind:120 [binder, in MetaCoq.Template.EtaExpand]
mind:126 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
mind:1335 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mind:135 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mind:1362 [binder, in MetaCoq.Erasure.ErasureFunction]
mind:1380 [binder, in MetaCoq.Erasure.ErasureFunction]
mind:14 [binder, in MetaCoq.Erasure.EArities]
mind:14 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mind:1402 [binder, in MetaCoq.Erasure.ErasureFunction]
mind:144 [binder, in MetaCoq.Template.EtaExpand]
mind:149 [binder, in MetaCoq.Erasure.EDeps]
mind:159 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:16 [binder, in MetaCoq.PCUIC.PCUICInductives]
mind:160 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mind:164 [binder, in MetaCoq.Template.TypingWf]
mind:179 [binder, in MetaCoq.PCUIC.PCUICElimination]
mind:18 [binder, in MetaCoq.Examples.add_constructor]
mind:187 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:189 [binder, in MetaCoq.PCUIC.PCUICElimination]
mind:19 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:194 [binder, in MetaCoq.Template.EtaExpand]
mind:20 [binder, in MetaCoq.Template.TermEquality]
mind:203 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mind:204 [binder, in MetaCoq.PCUIC.PCUICElimination]
mind:208 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mind:21 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:211 [binder, in MetaCoq.PCUIC.PCUICElimination]
mind:212 [binder, in MetaCoq.Erasure.EEtaExpanded]
mind:213 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mind:222 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
mind:229 [binder, in MetaCoq.Template.EtaExpand]
mind:23 [binder, in MetaCoq.Template.TemplateMonad.Core]
mind:248 [binder, in MetaCoq.Erasure.EEtaExpanded]
mind:25 [binder, in MetaCoq.Template.EnvironmentTyping]
mind:27 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
mind:270 [binder, in MetaCoq.Erasure.EEtaExpanded]
mind:277 [binder, in MetaCoq.Erasure.EEtaExpanded]
mind:283 [binder, in MetaCoq.Template.EtaExpand]
mind:293 [binder, in MetaCoq.Template.TypingWf]
mind:379 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mind:386 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mind:389 [binder, in MetaCoq.Erasure.ERemoveParams]
mind:44 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:45 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
mind:46 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
mind:477 [binder, in MetaCoq.PCUIC.PCUICProgress]
mind:485 [binder, in MetaCoq.PCUIC.PCUICProgress]
mind:5 [binder, in MetaCoq.Template.EnvironmentTyping]
mind:50 [binder, in MetaCoq.Translations.param_original]
mind:54 [binder, in MetaCoq.Translations.param_binary]
mind:55 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:56 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mind:562 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mind:565 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mind:579 [binder, in MetaCoq.Template.EnvironmentTyping]
mind:58 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
mind:591 [binder, in MetaCoq.Template.EnvironmentTyping]
mind:598 [binder, in MetaCoq.Template.EnvironmentTyping]
mind:60 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
mind:625 [binder, in MetaCoq.Template.EnvironmentTyping]
mind:647 [binder, in MetaCoq.Template.EnvironmentTyping]
mind:65 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:70 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:72 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
mind:8 [binder, in MetaCoq.PCUIC.PCUICTyping]
mind:80 [binder, in MetaCoq.Translations.param_cheap_packed]
mind:82 [binder, in MetaCoq.Translations.param_binary]
mind:822 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:828 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:84 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:85 [binder, in MetaCoq.Translations.param_original]
mind:881 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:9 [binder, in MetaCoq.PCUIC.PCUICInductives]
mind:9 [binder, in MetaCoq.Erasure.EGlobalEnv]
mind:900 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:91 [binder, in MetaCoq.Translations.times_bool_fun]
mind:968 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
MiniHoTT [library]
MiniHoTT_paths [library]
mkApp [definition, in MetaCoq.Template.Ast]
mkApp [definition, in MetaCoq.Erasure.EAst]
mkAppBox [definition, in MetaCoq.Erasure.Extract]
mkAppBox_repeat [lemma, in MetaCoq.Erasure.Prelim]
mkAppMkApps [lemma, in MetaCoq.Template.AstUtils]
mkApps [definition, in MetaCoq.Template.Ast]
mkApps [definition, in MetaCoq.PCUIC.PCUICAst]
mkApps [definition, in MetaCoq.Erasure.EAst]
MkAppsInd [module, in MetaCoq.Erasure.EInduction]
MkAppsInd.case [definition, in MetaCoq.Erasure.EInduction]
MkAppsInd.inspect [definition, in MetaCoq.Erasure.EInduction]
MkAppsInd.MkApps_case [section, in MetaCoq.Erasure.EInduction]
MkAppsInd.MkApps_rec [section, in MetaCoq.Erasure.EInduction]
MkAppsInd.rec [definition, in MetaCoq.Erasure.EInduction]
mkApps_tRel [lemma, in MetaCoq.Template.EtaExpand]
mkApps_nonempty [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_nisApp [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_elim [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_elim_rec [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_intro [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_spec [inductive, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_decompose [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_decompose_app [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_inj [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_right [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_left [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_inv [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_head [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_Fix_spec [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_notApp_inj [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_nApp_inj [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_inj [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_discr [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_tApp_inj [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_app [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app_rec [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_tApp [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
mkApps_Prod_nil [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
mkApps_trans_wf [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mkApps_app [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mkApps_morphism [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mkApps_ind_typing_spine [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
mkApps_snoc [lemma, in MetaCoq.PCUIC.PCUICNormal]
mkApps_tApp [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
mkApps_tsize [lemma, in MetaCoq.Examples.tauto]
mkApps_decompose_app [definition, in MetaCoq.PCUIC.Syntax.PCUICInduction]
mkApps_decompose_app_rec [definition, in MetaCoq.PCUIC.Syntax.PCUICInduction]
mkApps_eq [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_elim [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_elim_rec [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_intro [constructor, in MetaCoq.Erasure.EAstUtils]
mkApps_spec [inductive, in MetaCoq.Erasure.EAstUtils]
mkApps_eq_right [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_head_inj [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_eq_inj [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_eq_decompose_app_rec [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_head_spine_decompose [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_head_spine [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_app [lemma, in MetaCoq.Erasure.EAstUtils]
mkApps_tApp [lemma, in MetaCoq.Template.TypingWf]
mkApps_tApp' [lemma, in MetaCoq.Template.TypingWf]
mkApps_ex [lemma, in MetaCoq.Template.LiftSubst]
mkApps_tRel [lemma, in MetaCoq.Template.LiftSubst]
mkApps_tApp [lemma, in MetaCoq.Template.LiftSubst]
mkApps_app [lemma, in MetaCoq.Template.AstUtils]
mkApps_nisApp [lemma, in MetaCoq.Template.AstUtils]
mkApps_tApp [lemma, in MetaCoq.Template.AstUtils]
mkApps_intro [constructor, in MetaCoq.Template.AstUtils]
mkApps_spec [inductive, in MetaCoq.Template.AstUtils]
mkApps_eq_inj [lemma, in MetaCoq.Template.AstUtils]
mkApps_mkApp [lemma, in MetaCoq.Template.AstUtils]
mkApps_context_hole [lemma, in MetaCoq.PCUIC.PCUICReduction]
mkApps_context [definition, in MetaCoq.PCUIC.PCUICReduction]
mkApps_snoc [lemma, in MetaCoq.Erasure.Prelim]
mkApp_tsize [lemma, in MetaCoq.Examples.tauto]
mkApp_mkApps [lemma, in MetaCoq.Template.TypingWf]
mkApp_ex [lemma, in MetaCoq.Template.TypingWf]
mkApp_ex_wf [lemma, in MetaCoq.Template.TypingWf]
mkApp_tApp [lemma, in MetaCoq.Template.AstUtils]
mkApp_mkApps [lemma, in MetaCoq.Template.AstUtils]
mkAssumArity [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
mkAssumArity_it_mkProd_or_LetIn [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
mkCase_old [definition, in MetaCoq.Template.AstUtils]
mkImpl [definition, in MetaCoq.Examples.demo]
mk_env_flags [definition, in MetaCoq.Erasure.EWcbvEval]
mm:109 [binder, in MetaCoq.Template.utils.MCRelations]
mm:111 [binder, in MetaCoq.Template.utils.MCRelations]
modpath [inductive, in MetaCoq.Template.Kernames]
ModPathComp [module, in MetaCoq.Template.Kernames]
ModPathComp.compare [definition, in MetaCoq.Template.Kernames]
ModPathComp.compare_trans [lemma, in MetaCoq.Template.Kernames]
ModPathComp.compare_sym [lemma, in MetaCoq.Template.Kernames]
ModPathComp.compare_eq [lemma, in MetaCoq.Template.Kernames]
ModPathComp.eq [definition, in MetaCoq.Template.Kernames]
ModPathComp.eq_univ [definition, in MetaCoq.Template.Kernames]
ModPathComp.mpbound_compare [definition, in MetaCoq.Template.Kernames]
ModPathComp.nat_compare_trans [lemma, in MetaCoq.Template.Kernames]
ModPathComp.nat_compare_sym [lemma, in MetaCoq.Template.Kernames]
ModPathComp.t [definition, in MetaCoq.Template.Kernames]
_ ?= _ [notation, in MetaCoq.Template.Kernames]
ModPathOT [module, in MetaCoq.Template.Kernames]
modpath_EqDec [instance, in MetaCoq.Template.Kernames]
modpath_eq_dec [definition, in MetaCoq.Template.Kernames]
Monad [record, in MetaCoq.Template.monad_utils]
MonadAllAll [section, in MetaCoq.Template.monad_utils]
MonadExc [record, in MetaCoq.Template.monad_utils]
MonadOperations [section, in MetaCoq.Template.monad_utils]
MonadOperations [section, in MetaCoq.Template.monad_utils]
monad_exc [instance, in MetaCoq.Translations.translation_utils]
monad_map_app_invs [lemma, in MetaCoq.SafeChecker.PCUICErrors]
monad_map_app [lemma, in MetaCoq.SafeChecker.PCUICErrors]
monad_map_length [lemma, in MetaCoq.SafeChecker.PCUICErrors]
monad_map_Forall2 [lemma, in MetaCoq.SafeChecker.PCUICErrors]
monad_map_All2 [lemma, in MetaCoq.SafeChecker.PCUICErrors]
monad_exc [instance, in MetaCoq.SafeChecker.PCUICErrors]
Monad_EnvCheck_wf_env_ext [instance, in MetaCoq.SafeChecker.SafeTemplateChecker]
monad_exc [instance, in MetaCoq.Template.Checker]
monad_All_All [definition, in MetaCoq.Template.monad_utils]
monad_Alli_nth [definition, in MetaCoq.Template.monad_utils]
monad_Alli_nth_gen [definition, in MetaCoq.Template.monad_utils]
monad_Alli_nth [section, in MetaCoq.Template.monad_utils]
monad_Alli_All [definition, in MetaCoq.Template.monad_utils]
monad_Alli [definition, in MetaCoq.Template.monad_utils]
monad_prod [definition, in MetaCoq.Template.monad_utils]
monad_All2 [definition, in MetaCoq.Template.monad_utils]
monad_All [definition, in MetaCoq.Template.monad_utils]
monad_iter [definition, in MetaCoq.Template.monad_utils]
monad_map2 [definition, in MetaCoq.Template.monad_utils]
monad_map_i [definition, in MetaCoq.Template.monad_utils]
monad_map_i_aux [definition, in MetaCoq.Template.monad_utils]
monad_fold_right [definition, in MetaCoq.Template.monad_utils]
monad_fold_left [definition, in MetaCoq.Template.monad_utils]
monad_map [definition, in MetaCoq.Template.monad_utils]
Monad_EnvCheck_X_env_ext_type [instance, in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_Alli_nth_forall [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_Alli_nth_gen_forall [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_lift_ext [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_All_All [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_mapi [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_mapi_rec [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
monad_utils [library]
Monomorphic_entry [constructor, in MetaCoq.Template.Universes]
Monomorphic_ctx [constructor, in MetaCoq.Template.Universes]
monomorphic_level_in_global_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_level_notin_levels_of_udecl [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_global_constraint_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_global_constraint [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_level_notin_AUContext [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorph_globref_term [definition, in MetaCoq.Translations.translation_utils]
MoreCongruenceLemmas [section, in MetaCoq.PCUIC.PCUICConversion]
motivepars:380 [binder, in MetaCoq.PCUIC.PCUICNormal]
motiveret:381 [binder, in MetaCoq.PCUIC.PCUICNormal]
motive:379 [binder, in MetaCoq.PCUIC.PCUICNormal]
motive:484 [binder, in MetaCoq.PCUIC.PCUICNormal]
motive:491 [binder, in MetaCoq.PCUIC.PCUICNormal]
motive:813 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
moveL_moveR_transport_V [definition, in MetaCoq.Translations.MiniHoTT]
moveL_moveR_transport_p [definition, in MetaCoq.Translations.MiniHoTT]
moveL_equiv_V [definition, in MetaCoq.Translations.MiniHoTT]
moveL_equiv_M [definition, in MetaCoq.Translations.MiniHoTT]
moveL_transport_V_1 [definition, in MetaCoq.Translations.MiniHoTT]
moveL_transport_p_V [definition, in MetaCoq.Translations.MiniHoTT]
moveL_transport_V_V [definition, in MetaCoq.Translations.MiniHoTT]
moveL_transport_p [definition, in MetaCoq.Translations.MiniHoTT]
moveL_transport_V [definition, in MetaCoq.Translations.MiniHoTT]
moveL_V1 [definition, in MetaCoq.Translations.MiniHoTT]
moveL_1V [definition, in MetaCoq.Translations.MiniHoTT]
moveL_M1 [definition, in MetaCoq.Translations.MiniHoTT]
moveL_1M [definition, in MetaCoq.Translations.MiniHoTT]
moveL_pV [definition, in MetaCoq.Translations.MiniHoTT]
moveL_Vp [definition, in MetaCoq.Translations.MiniHoTT]
moveL_pM [definition, in MetaCoq.Translations.MiniHoTT]
moveL_Mp [definition, in MetaCoq.Translations.MiniHoTT]
moveL_moveR_transport_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_moveR_transport_p [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_equiv_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_equiv_M [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_V_1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_p_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_V_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_p [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_transport_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_V1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_1V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_M1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_1M [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_pV [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_Vp [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_pM [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveL_Mp [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_moveL_transport_p [definition, in MetaCoq.Translations.MiniHoTT]
moveR_moveL_transport_V [definition, in MetaCoq.Translations.MiniHoTT]
moveR_equiv_V [definition, in MetaCoq.Translations.MiniHoTT]
moveR_equiv_M [definition, in MetaCoq.Translations.MiniHoTT]
moveR_transport_V_V [definition, in MetaCoq.Translations.MiniHoTT]
moveR_transport_p_V [definition, in MetaCoq.Translations.MiniHoTT]
moveR_transport_V [definition, in MetaCoq.Translations.MiniHoTT]
moveR_transport_p [definition, in MetaCoq.Translations.MiniHoTT]
moveR_V1 [definition, in MetaCoq.Translations.MiniHoTT]
moveR_1V [definition, in MetaCoq.Translations.MiniHoTT]
moveR_1M [definition, in MetaCoq.Translations.MiniHoTT]
moveR_M1 [definition, in MetaCoq.Translations.MiniHoTT]
moveR_pV [definition, in MetaCoq.Translations.MiniHoTT]
moveR_Vp [definition, in MetaCoq.Translations.MiniHoTT]
moveR_pM [definition, in MetaCoq.Translations.MiniHoTT]
moveR_Mp [definition, in MetaCoq.Translations.MiniHoTT]
moveR_moveL_transport_p [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_moveL_transport_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_equiv_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_equiv_M [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_V_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_p_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_transport_p [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_V1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_1V [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_1M [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_M1 [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_pV [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_Vp [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_pM [definition, in MetaCoq.Translations.MiniHoTT_paths]
moveR_Mp [definition, in MetaCoq.Translations.MiniHoTT_paths]
move_ws_term [definition, in MetaCoq.PCUIC.PCUICConfluence]
MPbound [constructor, in MetaCoq.Template.Kernames]
MPdot [constructor, in MetaCoq.Template.Kernames]
MPfile [constructor, in MetaCoq.Template.Kernames]
Mphi:512 [binder, in MetaCoq.Examples.tauto]
Mphi:523 [binder, in MetaCoq.Examples.tauto]
mp':21 [binder, in MetaCoq.Template.Kernames]
mp:10 [binder, in MetaCoq.Template.Kernames]
mp:105 [binder, in MetaCoq.Translations.translation_utils]
mp:153 [binder, in MetaCoq.Translations.translation_utils]
mp:20 [binder, in MetaCoq.Template.Kernames]
mp:48 [binder, in MetaCoq.Translations.param_original]
mp:52 [binder, in MetaCoq.Translations.param_binary]
mp:56 [binder, in MetaCoq.Translations.translation_utils]
mp:65 [binder, in MetaCoq.Translations.translation_utils]
mp:78 [binder, in MetaCoq.Translations.param_cheap_packed]
mp:8 [binder, in MetaCoq.Template.Kernames]
mp:80 [binder, in MetaCoq.Translations.param_binary]
mp:83 [binder, in MetaCoq.Translations.param_original]
mp:89 [binder, in MetaCoq.Translations.times_bool_fun]
Msem [definition, in MetaCoq.Examples.tauto]
Msg [constructor, in MetaCoq.SafeChecker.PCUICErrors]
msg:1 [binder, in MetaCoq.Translations.param_binary]
msg:1 [binder, in MetaCoq.Translations.standard_model]
msg:1 [binder, in MetaCoq.Translations.param_original]
msg:20 [binder, in MetaCoq.Template.TemplateMonad.Core]
msg:22 [binder, in MetaCoq.Template.TemplateMonad.Core]
mutual_inductive_entry [record, in MetaCoq.Template.Ast]
mutual_inductive_entry [record, in MetaCoq.PCUIC.PCUICAst]
mutual_inductive_body [record, in MetaCoq.Erasure.EAst]
mutual_inductive_entry [record, in MetaCoq.Erasure.EAst]
mut_pt_i [definition, in MetaCoq.Examples.demo]
mut_list_i [definition, in MetaCoq.Examples.demo]
mut_i [definition, in MetaCoq.Examples.demo]
my_None [constructor, in MetaCoq.Template.TemplateMonad.Common]
my_Some [constructor, in MetaCoq.Template.TemplateMonad.Common]
my_projT2 [projection, in MetaCoq.Template.TemplateMonad.Common]
my_projT1 [projection, in MetaCoq.Template.TemplateMonad.Common]
M':103 [binder, in MetaCoq.Template.monad_utils]
M':1032 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M':1045 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m':1219 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1231 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1247 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1257 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1264 [binder, in MetaCoq.Erasure.ErasureFunction]
m':1275 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M':129 [binder, in MetaCoq.Template.monad_utils]
m':1298 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M':135 [binder, in MetaCoq.Template.Typing]
M':137 [binder, in MetaCoq.Template.monad_utils]
M':139 [binder, in MetaCoq.Template.Typing]
M':144 [binder, in MetaCoq.Template.monad_utils]
M':202 [binder, in MetaCoq.PCUIC.PCUICNormal]
M':207 [binder, in MetaCoq.PCUIC.PCUICNormal]
M':216 [binder, in MetaCoq.PCUIC.PCUICReduction]
M':221 [binder, in MetaCoq.PCUIC.PCUICReduction]
m':24 [binder, in MetaCoq.Erasure.Extract]
M':250 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M':307 [binder, in MetaCoq.Template.Typing]
M':312 [binder, in MetaCoq.Template.Typing]
m':333 [binder, in MetaCoq.Template.EtaExpand]
M':375 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M':396 [binder, in MetaCoq.PCUIC.PCUICSR]
M':401 [binder, in MetaCoq.PCUIC.PCUICSR]
M':439 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M':52 [binder, in MetaCoq.PCUIC.PCUICReduction]
M':56 [binder, in MetaCoq.PCUIC.PCUICReduction]
m':584 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m':596 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m':608 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M':7 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
M':702 [binder, in MetaCoq.PCUIC.PCUICReduction]
m':79 [binder, in MetaCoq.Erasure.Extract]
M':839 [binder, in MetaCoq.PCUIC.PCUICReduction]
M0:253 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M0:285 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M0:30 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M0:444 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M0:488 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M0:845 [binder, in MetaCoq.PCUIC.PCUICReduction]
M0:865 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:102 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:103 [binder, in MetaCoq.PCUIC.PCUICConversion]
M1:107 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:109 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:115 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:13 [binder, in MetaCoq.Template.Reduction]
M1:18 [binder, in MetaCoq.Template.Reduction]
M1:196 [binder, in MetaCoq.Template.Typing]
M1:201 [binder, in MetaCoq.Template.Typing]
M1:203 [binder, in MetaCoq.Template.Typing]
M1:209 [binder, in MetaCoq.Template.Typing]
M1:213 [binder, in MetaCoq.Template.Typing]
M1:220 [binder, in MetaCoq.Template.Typing]
M1:221 [binder, in MetaCoq.Template.Typing]
M1:23 [binder, in MetaCoq.Template.Reduction]
M1:254 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M1:272 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:278 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:281 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:286 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M1:288 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:3 [binder, in MetaCoq.Template.Reduction]
M1:31 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M1:377 [binder, in MetaCoq.Template.Typing]
M1:383 [binder, in MetaCoq.Template.Typing]
M1:388 [binder, in MetaCoq.Template.Typing]
M1:395 [binder, in MetaCoq.Template.Typing]
M1:403 [binder, in MetaCoq.Template.Typing]
M1:411 [binder, in MetaCoq.Template.Typing]
M1:413 [binder, in MetaCoq.Template.Typing]
M1:445 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M1:452 [binder, in MetaCoq.PCUIC.PCUICSR]
M1:458 [binder, in MetaCoq.PCUIC.PCUICSR]
M1:461 [binder, in MetaCoq.PCUIC.PCUICSR]
M1:468 [binder, in MetaCoq.PCUIC.PCUICSR]
M1:489 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M1:73 [binder, in MetaCoq.PCUIC.PCUICConversion]
M1:77 [binder, in MetaCoq.PCUIC.PCUICConversion]
M1:8 [binder, in MetaCoq.Template.Reduction]
M1:81 [binder, in MetaCoq.PCUIC.PCUICConversion]
M1:846 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:859 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:866 [binder, in MetaCoq.PCUIC.PCUICReduction]
M1:96 [binder, in MetaCoq.PCUIC.PCUICConversion]
M2:10 [binder, in MetaCoq.Template.Reduction]
M2:104 [binder, in MetaCoq.PCUIC.PCUICConversion]
M2:104 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:105 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:110 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:113 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:15 [binder, in MetaCoq.Template.Reduction]
M2:198 [binder, in MetaCoq.Template.Typing]
M2:199 [binder, in MetaCoq.Template.Typing]
M2:20 [binder, in MetaCoq.Template.Reduction]
M2:204 [binder, in MetaCoq.Template.Typing]
M2:207 [binder, in MetaCoq.Template.Typing]
M2:215 [binder, in MetaCoq.Template.Typing]
M2:217 [binder, in MetaCoq.Template.Typing]
M2:223 [binder, in MetaCoq.Template.Typing]
M2:24 [binder, in MetaCoq.Template.Reduction]
M2:274 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:276 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:282 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:286 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:379 [binder, in MetaCoq.Template.Typing]
M2:381 [binder, in MetaCoq.Template.Typing]
M2:389 [binder, in MetaCoq.Template.Typing]
M2:393 [binder, in MetaCoq.Template.Typing]
M2:405 [binder, in MetaCoq.Template.Typing]
M2:408 [binder, in MetaCoq.Template.Typing]
M2:415 [binder, in MetaCoq.Template.Typing]
M2:454 [binder, in MetaCoq.PCUIC.PCUICSR]
M2:456 [binder, in MetaCoq.PCUIC.PCUICSR]
M2:462 [binder, in MetaCoq.PCUIC.PCUICSR]
M2:466 [binder, in MetaCoq.PCUIC.PCUICSR]
M2:5 [binder, in MetaCoq.Template.Reduction]
M2:74 [binder, in MetaCoq.PCUIC.PCUICConversion]
M2:78 [binder, in MetaCoq.PCUIC.PCUICConversion]
M2:82 [binder, in MetaCoq.PCUIC.PCUICConversion]
M2:860 [binder, in MetaCoq.PCUIC.PCUICReduction]
M2:97 [binder, in MetaCoq.PCUIC.PCUICConversion]
M3:83 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:1 [binder, in MetaCoq.Template.monad_utils]
m:10 [binder, in MetaCoq.Template.utils.wGraph]
m:10 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
m:10 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:100 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:1004 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:1006 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:101 [binder, in MetaCoq.Erasure.ELiftSubst]
m:1011 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:1015 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:102 [binder, in MetaCoq.Template.utils.MCRelations]
M:102 [binder, in MetaCoq.Template.monad_utils]
M:1020 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:1026 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m:103 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
M:1031 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m:104 [binder, in MetaCoq.Template.utils.MCRelations]
M:104 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:104 [binder, in MetaCoq.Template.Environment]
M:104 [binder, in MetaCoq.Template.LiftSubst]
M:1044 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m:105 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:107 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:108 [binder, in MetaCoq.Template.WfAst]
M:108 [binder, in MetaCoq.Erasure.ELiftSubst]
m:108 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
m:11 [binder, in MetaCoq.PCUIC.PCUICAlpha]
M:11 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
m:110 [binder, in MetaCoq.Template.WfAst]
m:1121 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m:1126 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:113 [binder, in MetaCoq.Erasure.ELiftSubst]
M:114 [binder, in MetaCoq.Template.LiftSubst]
m:1150 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
m:1153 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
M:116 [binder, in MetaCoq.Erasure.ELiftSubst]
m:1163 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
m:1166 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
M:117 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:1170 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
M:119 [binder, in MetaCoq.Template.monad_utils]
m:12 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
m:12 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
m:12 [binder, in MetaCoq.Template.Checker]
M:121 [binder, in MetaCoq.Erasure.ELiftSubst]
m:1218 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:1230 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:1246 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:125 [binder, in MetaCoq.Erasure.EInduction]
M:125 [binder, in MetaCoq.Erasure.ELiftSubst]
M:1255 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:1256 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:1258 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:1261 [binder, in MetaCoq.Erasure.ErasureFunction]
M:1261 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:1264 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:1274 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:128 [binder, in MetaCoq.Template.monad_utils]
m:129 [binder, in MetaCoq.Erasure.EInduction]
m:1297 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:13 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
m:13 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:132 [binder, in MetaCoq.Template.LiftSubst]
M:134 [binder, in MetaCoq.Template.Typing]
M:136 [binder, in MetaCoq.Template.monad_utils]
M:137 [binder, in MetaCoq.Erasure.ELiftSubst]
m:137 [binder, in MetaCoq.Template.Environment]
M:138 [binder, in MetaCoq.Template.Typing]
m:14 [binder, in MetaCoq.Template.utils.wGraph]
M:143 [binder, in MetaCoq.Template.monad_utils]
M:144 [binder, in MetaCoq.Erasure.ELiftSubst]
M:145 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
m:145 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:146 [binder, in MetaCoq.Template.monad_utils]
m:147 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
M:149 [binder, in MetaCoq.Template.monad_utils]
M:15 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:150 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:155 [binder, in MetaCoq.Template.EtaExpand]
m:156 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
m:16 [binder, in MetaCoq.Template.utils.MCArith]
M:160 [binder, in MetaCoq.Erasure.ELiftSubst]
M:162 [binder, in MetaCoq.Template.monad_utils]
m:169 [binder, in MetaCoq.Template.AstUtils]
m:17 [binder, in MetaCoq.Template.utils.wGraph]
M:171 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:176 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:177 [binder, in MetaCoq.Template.monad_utils]
m:178 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:18 [binder, in MetaCoq.Template.utils.MCArith]
M:18 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
M:18 [binder, in MetaCoq.Template.LiftSubst]
m:180 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:182 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:184 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:185 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M:187 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:19 [binder, in MetaCoq.Template.utils.MCArith]
m:190 [binder, in MetaCoq.Erasure.Extract]
m:190 [binder, in MetaCoq.SafeChecker.PCUICErrors]
M:198 [binder, in MetaCoq.Template.monad_utils]
m:2 [binder, in MetaCoq.Template.utils.wGraph]
M:20 [binder, in MetaCoq.Template.LiftSubst]
m:2035 [binder, in MetaCoq.Template.utils.All_Forall]
m:204 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
m:204 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:209 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
m:209 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
m:209 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:21 [binder, in MetaCoq.Translations.translation_utils]
m:21 [binder, in MetaCoq.Template.utils.wGraph]
M:21 [binder, in MetaCoq.Template.LiftSubst]
M:215 [binder, in MetaCoq.PCUIC.PCUICReduction]
M:22 [binder, in MetaCoq.PCUIC.PCUICSpine]
M:220 [binder, in MetaCoq.PCUIC.PCUICReduction]
m:221 [binder, in MetaCoq.Erasure.EInduction]
M:223 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
m:224 [binder, in MetaCoq.Erasure.EInduction]
m:229 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:23 [binder, in MetaCoq.Erasure.EInduction]
m:23 [binder, in MetaCoq.Erasure.Extract]
M:23 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:231 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
m:231 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
M:232 [binder, in MetaCoq.Template.TypingWf]
m:236 [binder, in MetaCoq.SafeChecker.PCUICErrors]
m:237 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:239 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:240 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
m:241 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:242 [binder, in MetaCoq.SafeChecker.PCUICErrors]
m:243 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:2432 [binder, in MetaCoq.Translations.MiniHoTT]
M:2440 [binder, in MetaCoq.Translations.MiniHoTT_paths]
M:249 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m:25 [binder, in MetaCoq.Template.utils.wGraph]
m:25 [binder, in MetaCoq.Template.monad_utils]
m:252 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:253 [binder, in MetaCoq.Template.Environment]
m:254 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:256 [binder, in MetaCoq.PCUIC.PCUICInductives]
m:256 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:258 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:26 [binder, in MetaCoq.Erasure.EInduction]
M:26 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:26 [binder, in MetaCoq.Template.LiftSubst]
m:261 [binder, in MetaCoq.SafeChecker.PCUICErrors]
M:262 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
m:263 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
m:266 [binder, in MetaCoq.Template.Environment]
M:267 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
m:269 [binder, in MetaCoq.SafeChecker.PCUICErrors]
M:269 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
m:27 [binder, in MetaCoq.Translations.translation_utils]
m:27 [binder, in MetaCoq.Template.utils.bytestring]
m:27 [binder, in MetaCoq.Template.Checker]
M:27 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:274 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
M:276 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
m:28 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:282 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:283 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
m:284 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:29 [binder, in MetaCoq.Template.Typing]
m:29 [binder, in MetaCoq.Template.utils.wGraph]
m:294 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:297 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:299 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:30 [binder, in MetaCoq.Template.monad_utils]
m:301 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:303 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
m:303 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:305 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
m:306 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
M:306 [binder, in MetaCoq.Template.Typing]
M:310 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
M:311 [binder, in MetaCoq.Template.Typing]
m:314 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
m:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
M:321 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
M:325 [binder, in MetaCoq.PCUIC.PCUICSR]
m:33 [binder, in MetaCoq.Template.utils.wGraph]
m:33 [binder, in MetaCoq.Template.Pretty]
m:331 [binder, in MetaCoq.Template.EtaExpand]
m:332 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
m:333 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
m:337 [binder, in MetaCoq.Template.EtaExpand]
m:34 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
m:34 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:342 [binder, in MetaCoq.Template.EtaExpand]
m:345 [binder, in MetaCoq.Template.EtaExpand]
m:35 [binder, in MetaCoq.Template.Induction]
M:356 [binder, in MetaCoq.PCUIC.PCUICReduction]
m:357 [binder, in MetaCoq.Template.Universes]
m:359 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
m:36 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
M:361 [binder, in MetaCoq.PCUIC.PCUICReduction]
m:363 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:368 [binder, in MetaCoq.Template.EtaExpand]
m:37 [binder, in MetaCoq.Template.Induction]
m:371 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
m:373 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
M:374 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
m:375 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
m:376 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
M:38 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:38 [binder, in MetaCoq.Template.LiftSubst]
m:387 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:39 [binder, in MetaCoq.Template.utils.wGraph]
m:391 [binder, in MetaCoq.Template.Checker]
M:395 [binder, in MetaCoq.PCUIC.PCUICSR]
M:4 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
m:4 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:400 [binder, in MetaCoq.PCUIC.PCUICSR]
m:402 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
m:405 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
m:408 [binder, in MetaCoq.Template.utils.MCList]
m:408 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
M:41 [binder, in MetaCoq.Template.monad_utils]
m:419 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
M:421 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
M:43 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:43 [binder, in MetaCoq.Template.LiftSubst]
M:438 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m:44 [binder, in MetaCoq.Template.Checker]
M:44 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:445 [binder, in MetaCoq.Template.Typing]
M:45 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:4563 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
m:4565 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
m:457 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:47 [binder, in MetaCoq.Template.utils.wGraph]
M:471 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M:477 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
m:477 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
M:48 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:483 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M:489 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M:495 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
m:50 [binder, in MetaCoq.Template.utils.wGraph]
m:50 [binder, in MetaCoq.Template.Checker]
m:501 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
M:51 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:51 [binder, in MetaCoq.PCUIC.PCUICReduction]
m:511 [binder, in MetaCoq.Template.utils.MCList]
M:524 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
m:53 [binder, in MetaCoq.Template.utils.wGraph]
M:530 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M:539 [binder, in MetaCoq.PCUIC.PCUICSpine]
m:54 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
M:54 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:54 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:546 [binder, in MetaCoq.PCUIC.PCUICSpine]
M:55 [binder, in MetaCoq.Template.LiftSubst]
M:55 [binder, in MetaCoq.PCUIC.PCUICReduction]
m:56 [binder, in MetaCoq.Template.utils.wGraph]
M:57 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:572 [binder, in MetaCoq.Template.common.uGraph]
m:575 [binder, in MetaCoq.Template.common.uGraph]
m:577 [binder, in MetaCoq.Template.common.uGraph]
m:579 [binder, in MetaCoq.Template.common.uGraph]
m:583 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m:59 [binder, in MetaCoq.Template.utils.wGraph]
m:590 [binder, in MetaCoq.Template.utils.wGraph]
m:592 [binder, in MetaCoq.Template.utils.wGraph]
m:595 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m:6 [binder, in MetaCoq.Template.utils.wGraph]
M:6 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
M:60 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:60 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:60 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:607 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:63 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:63 [binder, in MetaCoq.Template.LiftSubst]
M:632 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M:636 [binder, in MetaCoq.PCUIC.PCUICSR]
m:637 [binder, in MetaCoq.Template.utils.MCList]
m:64 [binder, in MetaCoq.Template.utils.wGraph]
M:64 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:64 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:640 [binder, in MetaCoq.Template.utils.MCList]
M:641 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
m:644 [binder, in MetaCoq.Template.utils.MCList]
M:65 [binder, in MetaCoq.Erasure.ELiftSubst]
M:650 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
M:67 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:67 [binder, in MetaCoq.Erasure.ELiftSubst]
m:68 [binder, in MetaCoq.Erasure.EDeps]
m:68 [binder, in MetaCoq.Template.utils.wGraph]
M:68 [binder, in MetaCoq.Erasure.ELiftSubst]
m:688 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m:689 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M:69 [binder, in MetaCoq.Template.monad_utils]
M:69 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:692 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:697 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:699 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M:701 [binder, in MetaCoq.PCUIC.PCUICReduction]
M:704 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:708 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
M:708 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m:71 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
M:71 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:714 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:716 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
m:72 [binder, in MetaCoq.Template.utils.wGraph]
M:72 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:722 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:726 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:73 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:73 [binder, in MetaCoq.Erasure.ELiftSubst]
M:732 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m:739 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:74 [binder, in MetaCoq.Template.BasicAst]
M:74 [binder, in MetaCoq.Template.LiftSubst]
m:74 [binder, in MetaCoq.Template.Induction]
M:740 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m:743 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:744 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
M:747 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:75 [binder, in MetaCoq.Erasure.ELiftSubst]
m:750 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:754 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:759 [binder, in MetaCoq.PCUIC.PCUICConfluence]
m:76 [binder, in MetaCoq.Template.utils.wGraph]
m:76 [binder, in MetaCoq.Template.Induction]
M:764 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:769 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:77 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:778 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
m:78 [binder, in MetaCoq.Erasure.Extract]
m:781 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
M:79 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:79 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:79 [binder, in MetaCoq.Template.LiftSubst]
m:80 [binder, in MetaCoq.Template.utils.wGraph]
M:80 [binder, in MetaCoq.Erasure.ELiftSubst]
M:81 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:82 [binder, in MetaCoq.Template.utils.wGraph]
M:82 [binder, in MetaCoq.Template.LiftSubst]
M:838 [binder, in MetaCoq.PCUIC.PCUICReduction]
m:84 [binder, in MetaCoq.Template.utils.wGraph]
M:85 [binder, in MetaCoq.Template.monad_utils]
M:851 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
M:854 [binder, in MetaCoq.PCUIC.PCUICReduction]
M:86 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:86 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:86 [binder, in MetaCoq.Template.utils.wGraph]
M:87 [binder, in MetaCoq.Template.LiftSubst]
m:89 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:894 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
M:895 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:9 [binder, in MetaCoq.Template.monad_utils]
M:90 [binder, in MetaCoq.Template.monad_utils]
M:901 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:908 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:91 [binder, in MetaCoq.Template.LiftSubst]
M:915 [binder, in MetaCoq.PCUIC.PCUICConversion]
M:92 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:922 [binder, in MetaCoq.PCUIC.PCUICConversion]
m:926 [binder, in MetaCoq.Erasure.ErasureFunction]
m:93 [binder, in MetaCoq.Template.EtaExpand]
M:93 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:95 [binder, in MetaCoq.Erasure.ELiftSubst]
M:973 [binder, in MetaCoq.PCUIC.PCUICConfluence]
M:98 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
m:998 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
| 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) |