| 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) |
C (lemma)
case_branch_context_assumptions [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]Case_Construct_ind_eq [in MetaCoq.PCUIC.PCUICSafeLemmata]
case_branch_context_assumptions [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
case_brs_forallb_map_spec [in MetaCoq.Template.Ast]
case_brs_map_k_spec [in MetaCoq.Template.Ast]
case_brs_map_spec [in MetaCoq.Template.Ast]
case_predicate_context_alpha [in MetaCoq.PCUIC.PCUICInductiveInversion]
case_branch_type_eq_context_gen_2 [in MetaCoq.PCUIC.PCUICAlpha]
case_branch_type_eq_context_gen_1 [in MetaCoq.PCUIC.PCUICAlpha]
case_branch_type_equiv [in MetaCoq.PCUIC.PCUICAlpha]
case_branch_context_equiv [in MetaCoq.PCUIC.PCUICAlpha]
case_predicate_context_equiv [in MetaCoq.PCUIC.PCUICAlpha]
case_branch_type_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branches_contexts_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branch_context_assumptions [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branch_context_length_args [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branch_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_predicate_context_length_indices [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_predicate_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_branch_type_fst [in MetaCoq.PCUIC.Syntax.PCUICCases]
case_brs_forallb_map_spec [in MetaCoq.PCUIC.PCUICAst]
case_brs_map_k_spec [in MetaCoq.PCUIC.PCUICAst]
case_brs_map_spec_cond [in MetaCoq.PCUIC.PCUICAst]
case_brs_map_spec [in MetaCoq.PCUIC.PCUICAst]
case_conv_preds_inv [in MetaCoq.SafeChecker.PCUICSafeConversion]
case_conv_brs_inv [in MetaCoq.SafeChecker.PCUICSafeConversion]
checking_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
check_constraints_complete [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
check_constraints_spec [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
check_ind_sorts_is_propositional [in MetaCoq.PCUIC.PCUICElimination]
check_eqb_universe_complete [in MetaCoq.Template.common.uGraph]
check_eqb_universe_spec' [in MetaCoq.Template.common.uGraph]
check_leqb_universe_complete [in MetaCoq.Template.common.uGraph]
check_leqb_universe_spec' [in MetaCoq.Template.common.uGraph]
check_constraints_complete [in MetaCoq.Template.common.uGraph]
check_constraints_spec [in MetaCoq.Template.common.uGraph]
check_gc_constraints_complete [in MetaCoq.Template.common.uGraph]
check_gc_constraint_complete [in MetaCoq.Template.common.uGraph]
check_eqb_levelalg_complete [in MetaCoq.Template.common.uGraph]
check_eqb_levelalg_spec' [in MetaCoq.Template.common.uGraph]
check_leqb_levelalg_complete [in MetaCoq.Template.common.uGraph]
check_leqb_levelalg_spec' [in MetaCoq.Template.common.uGraph]
check_eqb_universe_spec [in MetaCoq.Template.common.uGraph]
check_eqb_universe_refl [in MetaCoq.Template.common.uGraph]
check_gc_constraints_spec [in MetaCoq.Template.common.uGraph]
check_gc_constraint_spec [in MetaCoq.Template.common.uGraph]
check_eqb_levelalg_spec [in MetaCoq.Template.common.uGraph]
check_leqb_levelalg_spec [in MetaCoq.Template.common.uGraph]
check_recursivity_kind_inj [in MetaCoq.PCUIC.PCUICCanonicity]
check_constructors_smallerP [in MetaCoq.SafeChecker.PCUICSafeChecker]
chop_n_app [in MetaCoq.Template.utils.MCList]
chop_map [in MetaCoq.Template.utils.MCList]
chop_all [in MetaCoq.Erasure.EConstructorsAsBlocks]
chop_eq [in MetaCoq.Erasure.EConstructorsAsBlocks]
chop_firstn_skipn [in MetaCoq.Erasure.EConstructorsAsBlocks]
chop_firstn_skipn [in MetaCoq.SafeChecker.PCUICTypeChecker]
closedn_ctx_lift_inv [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
closedn_mkApps [in MetaCoq.Erasure.EEtaExpandedFix]
closedn_ctx_on_free_vars_shift [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_ctx_on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_expand'' [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedn_expand' [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedn_expand [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedn_zip [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedn_fill_hole [in MetaCoq.PCUIC.Syntax.PCUICPosition]
closedn_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
closedn_ctx_on_free_vars [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
closedn_ctx_cstr_branch_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closedn_ctx_expand_lets [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closedn_subst [in MetaCoq.Erasure.ELiftSubst]
closedn_subst_eq [in MetaCoq.Erasure.ELiftSubst]
closedn_lift [in MetaCoq.Erasure.ELiftSubst]
closedn_mkApps [in MetaCoq.PCUIC.PCUICCanonicity]
closedn_to_extended_list [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_to_extended_list_k [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_to_extended_list_k_up [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_expand_lets_eq [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_expand_lets [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_upwards [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_expand_lets [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_extended_subst [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_extended_subst_gen [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_subst [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_lift [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_decl [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_mapi_rec_ext [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_smash_context [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_spec [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_subst_instance_context [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_it_mkProd_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_mkLambda_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_mkProd_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_tip [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_subst_instance [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_subst0 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_subst [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_subst_eq' [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_subst_eq [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_mkApps [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_lift_inv [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_lift [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_app [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_cons [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closedn_expand_lets [in MetaCoq.PCUIC.PCUICSR]
closedn_mkApps [in MetaCoq.Erasure.ERemoveParams]
closedn_All_local_closed [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
closedn_All_local_env [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
closedn_ctx_alpha [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
closedn_mkApps [in MetaCoq.Erasure.EWcbvEval]
closedn_ctx_snoc [in MetaCoq.PCUIC.PCUICContexts]
closedP_xpredT [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_shiftnP_impl [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_shiftnP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_mon [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
closedP_shiftnP_eq [in MetaCoq.PCUIC.PCUICSR]
closedu_subst_instance [in MetaCoq.Template.Universes]
closedu_subst_instance_univ [in MetaCoq.Template.Universes]
closedu_subst_instance_level_expr [in MetaCoq.Template.Universes]
closedu_subst_instance_level [in MetaCoq.Template.Universes]
closedu_inds [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_to_extended_list_k [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_reln [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_smash_context [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_smash_context_gen [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_expand_lets_ctx [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_extended_subst [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_lift_context [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_subst_context [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_subst [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_lift [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_abstract_instance [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_mkApps [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_compare_decls [in MetaCoq.PCUIC.PCUICWfUniverses]
closedu_subst_instance_cstrs_lift [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_cstrs_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_lift [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_expr_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_lift [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
closedu_subst_instance [in MetaCoq.Template.UnivSubst]
closed_ind_predicate_context [in MetaCoq.PCUIC.PCUICWfUniverses]
closed_cstr_branch_context_npars [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
closed_cstr_branch_context [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
closed_ctx_on_ctx_free_vars [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
closed_wf_local [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
closed_arities_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
closed_ind_predicate_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
closed_unfold_cofix [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_unfold_cofix_cunfold_eq [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_unfold_fix_cunfold_eq [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_cofix_substl_subst_eq [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_fix_substl_subst_eq [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_unfold_fix [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_arg [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_iota [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_def [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_beta [in MetaCoq.PCUIC.PCUICWcbvEval]
closed_tele_subst [in MetaCoq.PCUIC.PCUICSubstitution]
closed_ctx_subst [in MetaCoq.PCUIC.PCUICSubstitution]
closed_iota_red [in MetaCoq.Erasure.EInlineProjections]
closed_transform_blocks [in MetaCoq.Erasure.EConstructorsAsBlocks]
closed_ctx_on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closed_decl_on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closed_on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closed_on_free_vars_none [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
closed_red_mkApps [in MetaCoq.PCUIC.PCUICInductiveInversion]
closed_red_upto_conv_ctx_prop [in MetaCoq.PCUIC.PCUICCumulProp]
closed_red1_upto_conv_ctx_prop [in MetaCoq.PCUIC.PCUICCumulProp]
closed_fake_params [in MetaCoq.PCUIC.PCUICNormal]
closed_csubst [in MetaCoq.PCUIC.PCUICCSubst]
closed_subst [in MetaCoq.PCUIC.PCUICCSubst]
closed_ctx_lift [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
closed_inst_case_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
closed_ctx_is_closed_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
closed_context_conversion [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_cumulativity [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_conv_conv [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_cumul_cumul [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
closed_red1_red [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
closed_red_open_right [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
closed_red1_open_right [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
closed_subst_up_vdef [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_subst_up_vass [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_subst_app_up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_subst_app [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_subst_Up' [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_subst_Up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_subst_ext [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_ctx_args [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_tele_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
closed_red_zipp [in MetaCoq.SafeChecker.PCUICSafeConversion]
closed_red_mkApps_tConst_axiom [in MetaCoq.SafeChecker.PCUICSafeConversion]
closed_upwards [in MetaCoq.Erasure.ELiftSubst]
closed_nlctx [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
closed_nl [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
closed_ctx_IH [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
closed_red_rel_all [in MetaCoq.PCUIC.PCUICConversion]
closed_red_subst [in MetaCoq.PCUIC.PCUICConversion]
closed_red1_mkApps_left [in MetaCoq.PCUIC.PCUICConversion]
closed_red_terms_open_right [in MetaCoq.PCUIC.PCUICConversion]
closed_red_terms_open_left [in MetaCoq.PCUIC.PCUICConversion]
closed_red_prod_codom [in MetaCoq.PCUIC.PCUICConversion]
closed_red_prod [in MetaCoq.PCUIC.PCUICConversion]
closed_red_letin_body [in MetaCoq.PCUIC.PCUICConversion]
closed_red_letin [in MetaCoq.PCUIC.PCUICConversion]
closed_red_untyped_substitution0 [in MetaCoq.PCUIC.PCUICConversion]
closed_red_untyped_substitution [in MetaCoq.PCUIC.PCUICConversion]
closed_red_red_subst0 [in MetaCoq.PCUIC.PCUICConversion]
closed_red_red_subst [in MetaCoq.PCUIC.PCUICConversion]
closed_red_clos [in MetaCoq.PCUIC.PCUICConversion]
closed_red_ctx_refl [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_refl [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_eq_context_upto_r [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_eq_context_upto_l [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_confluence [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_red_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_compare_term_r [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_compare_term_l [in MetaCoq.PCUIC.PCUICContextConversion]
closed_red_ctx_red_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
closed_ind_closed_cstrs [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_inds [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_ind_predicate_context [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_ctx_decl [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_ctx_expand_lets [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_declared_ind [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_smash_context_unfold [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_smash_context_gen [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_subst_context [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_map_subst_instance [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_ctx_lift [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_decl_upwards [in MetaCoq.PCUIC.Syntax.PCUICClosed]
closed_red1_case_branch_type [in MetaCoq.PCUIC.PCUICSR]
closed_red1_mkApps_left [in MetaCoq.PCUIC.PCUICSR]
closed_red1_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICSR]
closed_red1_ws_cumul_pb [in MetaCoq.PCUIC.PCUICSR]
closed_red1_eq_context_upto_names [in MetaCoq.PCUIC.PCUICSR]
closed_red1_ind [in MetaCoq.PCUIC.PCUICSR]
closed_upwards [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
closed_strip [in MetaCoq.Erasure.ERemoveParams]
closed_substl [in MetaCoq.Erasure.ECSubst]
closed_csubst [in MetaCoq.Erasure.ECSubst]
closed_subst [in MetaCoq.Erasure.ECSubst]
closed_cstr_branch_context_gen [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
closed_cunfold_cofix [in MetaCoq.Erasure.EWcbvEval]
closed_cunfold_fix [in MetaCoq.Erasure.EWcbvEval]
closed_cofix_subst [in MetaCoq.Erasure.EWcbvEval]
closed_fix_subst [in MetaCoq.Erasure.EWcbvEval]
closed_unfold_cofix_cunfold_eq [in MetaCoq.Erasure.EWcbvEval]
closed_cofix_substl_subst_eq [in MetaCoq.Erasure.EWcbvEval]
closed_unfold_fix_cunfold_eq [in MetaCoq.Erasure.EWcbvEval]
closed_fix_substl_subst_eq [in MetaCoq.Erasure.EWcbvEval]
closed_iota_red [in MetaCoq.Erasure.EOptimizePropDiscr]
closed_optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
closed_upwards [in MetaCoq.Template.LiftSubst]
closed_subst_map_lift [in MetaCoq.PCUIC.PCUICSpine]
closed_ctx_subst [in MetaCoq.PCUIC.PCUICSpine]
closed_k_ctx_subst [in MetaCoq.PCUIC.PCUICSpine]
clos_t_rt_equiv [in MetaCoq.Template.utils.MCRelations]
clos_t_rt_incl [in MetaCoq.Template.utils.MCRelations]
clos_rt_t_incl [in MetaCoq.Template.utils.MCRelations]
clos_refl_trans_prod_r [in MetaCoq.Template.utils.MCRelations]
clos_refl_trans_prod_l [in MetaCoq.Template.utils.MCRelations]
clos_rt_disjunction_right [in MetaCoq.Template.utils.MCRelations]
clos_rt_disjunction_left [in MetaCoq.Template.utils.MCRelations]
clos_t_rt [in MetaCoq.Template.utils.MCRelations]
clos_rt_red1_red1_rel_alpha [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_to_1n [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_red1_alpha_out' [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_red1_alpha_out [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_red1_eq_context_upto_names [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_red1 [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_ws_red1 [in MetaCoq.PCUIC.PCUICConfluence]
clos_red_rel_out_inv [in MetaCoq.PCUIC.PCUICConfluence]
clos_red_rel_out [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_out [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_red1_ctx_eq_length [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_prod_r [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_prod_l_sigma [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_rt_ctx [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_ctx_rt_ctx_red1_rel [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_length [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_on_free_vars [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_prod_r [in MetaCoq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_prod_l [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_disjunction_right [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_disjunction_left [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_OnOne2_local_env_ctx_incl [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_proper [in MetaCoq.PCUIC.PCUICConfluence]
clos_rt_OnOne2_local_env_incl [in MetaCoq.PCUIC.PCUICConfluence]
cmp_universe_subset [in MetaCoq.Template.Universes]
cofix_subst_length [in MetaCoq.Template.Typing]
cofix_subst_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
cofix_subst_length [in MetaCoq.Erasure.EGlobalEnv]
cofix_subst_instance_subst [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cofix_subst_nth [in MetaCoq.Erasure.Prelim]
combine_map_id [in MetaCoq.Template.utils.MCList]
common_typing [in MetaCoq.PCUIC.PCUICPrincipality]
commutes_disj_joinable [in MetaCoq.PCUIC.PCUICConfluence]
commutes_diamonds_diamond [in MetaCoq.PCUIC.PCUICConfluence]
commut_lift_subst [in MetaCoq.Erasure.ELiftSubst]
commut_lift_subst_rec [in MetaCoq.Erasure.ELiftSubst]
commut_lift_subst [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
commut_lift_subst_rec [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
commut_lift_subst [in MetaCoq.Template.LiftSubst]
commut_lift_subst_rec [in MetaCoq.Template.LiftSubst]
CompareSpec_Proper [in MetaCoq.Template.utils.MCCompare]
compare_cont_trans [in MetaCoq.Template.utils.MCCompare]
compare_cont_CompOpp [in MetaCoq.Template.utils.MCCompare]
compare_decls_eq_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
compare_decls_conv [in MetaCoq.PCUIC.PCUICSafeLemmata]
compare_eq_refl [in MetaCoq.Template.utils.ByteCompareSpec]
compare_spec [in MetaCoq.Template.utils.ByteCompareSpec]
compare_eq [in MetaCoq.Template.utils.ByteCompareSpec]
compare_opp [in MetaCoq.Template.utils.ByteCompareSpec]
compare_equiv [in MetaCoq.Template.utils.ByteCompareSpec]
compare_context_subset [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_decl_subset [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_term_subset [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_decl_map [in MetaCoq.PCUIC.PCUICEquality]
compare_decl_impl_ondecl [in MetaCoq.PCUIC.PCUICEquality]
compare_decls_impl [in MetaCoq.PCUIC.PCUICEquality]
compare_universe_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
compare_global_instance_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
compare_universe_instance_variance_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
compare_universe_variance_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
compare_universeb_make_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
compare_universeb_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
compare_term_mkApps_r_inv [in MetaCoq.PCUIC.PCUICConversion]
compare_term_mkApps_l_inv [in MetaCoq.PCUIC.PCUICConversion]
compare_term_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_global_instance_refl [in MetaCoq.SafeChecker.PCUICEqualityDec]
compose_map_decl [in MetaCoq.Template.BasicAst]
compose_map_def [in MetaCoq.Template.BasicAst]
compose_ren [in MetaCoq.PCUIC.PCUICSigmaCalculus]
compose_ids_l [in MetaCoq.PCUIC.PCUICSigmaCalculus]
compose_ids_r [in MetaCoq.PCUIC.PCUICSigmaCalculus]
compose_map_def [in MetaCoq.Erasure.ELiftSubst]
compose_on_snd [in MetaCoq.Template.utils.MCProd]
concat_Vp_inverse2 [in MetaCoq.Translations.MiniHoTT]
concat_pV_inverse2 [in MetaCoq.Translations.MiniHoTT]
concat_p1_1 [in MetaCoq.Translations.MiniHoTT]
concat_1p_1 [in MetaCoq.Translations.MiniHoTT]
concat_Vp_inverse2 [in MetaCoq.Translations.MiniHoTT_paths]
concat_pV_inverse2 [in MetaCoq.Translations.MiniHoTT_paths]
concat_p1_1 [in MetaCoq.Translations.MiniHoTT_paths]
concat_1p_1 [in MetaCoq.Translations.MiniHoTT_paths]
concat2_ap_ap [in MetaCoq.Translations.MiniHoTT]
concat2_ap_ap [in MetaCoq.Translations.MiniHoTT_paths]
confluent_union [in MetaCoq.PCUIC.PCUICConfluence]
consistency_preservation [in MetaCoq.Translations.param_generous_packed]
consistent_extension_on_union [in MetaCoq.Template.Universes]
consistent_extension_on_empty [in MetaCoq.Template.Universes]
consistent_instance_ext_wf [in MetaCoq.PCUIC.PCUICWfUniverses]
consistent_instance_valid [in MetaCoq.PCUIC.PCUICInductiveInversion]
consistent_instance_poly_length [in MetaCoq.PCUIC.PCUICInductiveInversion]
consistent_ext_on_full_ext [in MetaCoq.Template.common.uGraph]
consistent_ext_on_full_ext0 [in MetaCoq.Template.common.uGraph]
consistent_instance_ext_wf [in MetaCoq.SafeChecker.PCUICSafeConversion]
consistent_instance_ext_subst_abs_inds [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs_univ [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_abstract_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_valid_constraints [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans_polymorphic_cases [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans_polymorphic_case_aux [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_declared [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_extension_on_global [in MetaCoq.SafeChecker.PCUICSafeChecker]
consistent_instance_wf_universe [in MetaCoq.SafeChecker.PCUICEqualityDec]
ConstraintSetsUIP.ok_irrel [in MetaCoq.Template.Reflect]
ConstraintType.compare_spec [in MetaCoq.Template.Universes]
ConstraintType.eq_dec [in MetaCoq.Template.Universes]
constraint_lt_irrel [in MetaCoq.Template.Reflect]
constraint_type_lt_level_irrel [in MetaCoq.Template.Reflect]
constructor_isprop_pars_decl_constructor [in MetaCoq.Erasure.EInlineProjections]
constructor_isprop_pars_decl_inductive [in MetaCoq.Erasure.EInlineProjections]
constructor_isprop_pars_decl_params [in MetaCoq.Erasure.EConstructorsAsBlocks]
constructor_cumulative_indices [in MetaCoq.PCUIC.PCUICInductiveInversion]
constructor_isprop_pars_inductive_pars [in MetaCoq.Erasure.ERemoveParams]
constructor_isprop_pars_decl_lookup [in MetaCoq.Erasure.ERemoveParams]
constructor_isprop_pars_decl_constructor [in MetaCoq.Erasure.EGenericMapEnv]
constructor_isprop_pars_decl_inductive [in MetaCoq.Erasure.EGenericMapEnv]
constructor_isprop_pars_decl_inductive [in MetaCoq.Erasure.EOptimizePropDiscr]
construct_cofix_discr_match [in MetaCoq.PCUIC.Syntax.PCUICViews]
Construct_Ind_ind_eq' [in MetaCoq.PCUIC.PCUICInductiveInversion]
Construct_Ind_ind_eq [in MetaCoq.PCUIC.PCUICInductiveInversion]
construct_cofix_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cons_prefix [in MetaCoq.Template.utils.MCList]
contextual_closure_red [in MetaCoq.PCUIC.PCUICReduction]
context_assumptions_lift [in MetaCoq.Template.EtaExpand]
context_assumptions_lift' [in MetaCoq.Template.EtaExpand]
context_assumptions_fold_context_k_defs [in MetaCoq.Template.EtaExpand]
context_pres_let_bodies_red [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
context_pres_let_bodies_red1 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
context_assumptions_expand_lets_ctx [in MetaCoq.PCUIC.utils.PCUICAstUtils]
context_assumptions_smash_context [in MetaCoq.PCUIC.utils.PCUICAstUtils]
context_assumptions_map2_set_binder_name [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
context_assumptions_map [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
context_assumptions_map [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
context_subst_to_extended_list_k [in MetaCoq.PCUIC.PCUICInductives]
context_conversion_cumul_prop [in MetaCoq.PCUIC.PCUICCumulProp]
context_position_valid [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_position_atpos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
context_assumptions_context [in MetaCoq.PCUIC.PCUICSigmaCalculus]
context_cumulativity_spec [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
context_assumptions_set_binder_name [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
context_assumptions_map [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
context_conversion [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
context_cumulativity [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
context_cumulativity_prop [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
context_assumptions_mapi_context [in MetaCoq.PCUIC.PCUICAst]
context_position_nlctx [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
context_cumulativity_app [in MetaCoq.PCUIC.PCUICContextConversion]
context_cumulativity_wf_app [in MetaCoq.PCUIC.PCUICContextConversion]
context_assumptions_bound [in MetaCoq.PCUIC.PCUICSR]
context_assumptions_expand_lets_k_ctx [in MetaCoq.PCUIC.PCUICSR]
context_assumptions_subst [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
context_subst_app [in MetaCoq.PCUIC.PCUICContextSubst]
context_subst_fun' [in MetaCoq.PCUIC.PCUICContextSubst]
context_subst_fun [in MetaCoq.PCUIC.PCUICContextSubst]
context_subst_length2 [in MetaCoq.PCUIC.PCUICContextSubst]
context_subst_assumptions_length [in MetaCoq.PCUIC.PCUICContextSubst]
context_subst_length [in MetaCoq.PCUIC.PCUICContextSubst]
context_depth_inst_case_context [in MetaCoq.PCUIC.Syntax.PCUICDepth]
context_assumptions_fake_params [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash_context'' [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash_context' [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_fold_context_term [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
context_subst_extended_subst [in MetaCoq.PCUIC.PCUICContexts]
context_subst_lift [in MetaCoq.PCUIC.PCUICContexts]
context_assumptions_subst [in MetaCoq.PCUIC.PCUICSpine]
context_assumptions_lift [in MetaCoq.PCUIC.PCUICSpine]
context_subst_subst_extended_subst [in MetaCoq.PCUIC.PCUICSpine]
context_assumptions_rev [in MetaCoq.PCUIC.PCUICSpine]
context_assumptions_subst_telescope [in MetaCoq.PCUIC.PCUICSpine]
context_subst_subst [in MetaCoq.PCUIC.PCUICSpine]
context_subst_app_inv [in MetaCoq.PCUIC.PCUICSpine]
context_cumulativity_wt_decl [in MetaCoq.SafeChecker.PCUICTypeChecker]
context_cumulativity_welltyped [in MetaCoq.SafeChecker.PCUICTypeChecker]
contr_equiv [in MetaCoq.Translations.MiniHoTT]
contr_equiv [in MetaCoq.Translations.MiniHoTT_paths]
convSpec_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
convSpec_convAlgo_curry [in MetaCoq.PCUIC.PCUICConversion]
convSpec_convAlgo [in MetaCoq.PCUIC.PCUICConversion]
convSpec_cumulSpec [in MetaCoq.PCUIC.PCUICConversion]
convSpec_renameP [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
convSpec0_ind_all [in MetaCoq.PCUIC.PCUICCumulativitySpec]
conv_alt_red [in MetaCoq.PCUIC.PCUICCumulativity]
conv_cumul_inv [in MetaCoq.PCUIC.PCUICCumulativity]
conv_cumul [in MetaCoq.PCUIC.PCUICCumulativity]
conv_cumul2 [in MetaCoq.PCUIC.PCUICCumulativity]
conv_cum_zipp [in MetaCoq.PCUIC.PCUICSafeLemmata]
conv_alt_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICSafeLemmata]
conv_alt_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICSafeLemmata]
conv_to_arity_cumul [in MetaCoq.Erasure.EArities]
conv_refl' [in MetaCoq.Template.Typing]
conv_decls_fix_context [in MetaCoq.PCUIC.PCUICInductiveInversion]
conv_decls_fix_context_gen [in MetaCoq.PCUIC.PCUICInductiveInversion]
conv_eq_ctx [in MetaCoq.PCUIC.PCUICInductiveInversion]
conv_ctx_prop_app [in MetaCoq.PCUIC.PCUICCumulProp]
conv_ctx_prop_refl [in MetaCoq.PCUIC.PCUICCumulProp]
conv_cumul_prop [in MetaCoq.PCUIC.PCUICCumulProp]
conv_sort_inv [in MetaCoq.PCUIC.PCUICCumulProp]
conv_decorate_hetero [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
conv_decorate [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
conv_ctx_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
conv_decls_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
conv_context_wf_local_app [in MetaCoq.Erasure.ErasureProperties]
conv_cum_tProj_inv [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_cum_tCoFix_inv [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_cum_tFix_inv [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_cum_tCase_inv [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_cum_mkApps_inv [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_conv_cum_r [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_conv_cum_l [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_cum_alt [in MetaCoq.PCUIC.PCUICConvCumInversion]
conv_arity_Is_conv_to_Arity [in MetaCoq.SafeChecker.PCUICSafeReduce]
conv_cum_red_inv [in MetaCoq.SafeChecker.PCUICSafeConversion]
conv_cum_red_conv_inv [in MetaCoq.SafeChecker.PCUICSafeConversion]
conv_context_decl [in MetaCoq.SafeChecker.PCUICSafeConversion]
conv_inds [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_Lambda [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_red_conv_iff [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_red_iff [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_red_conv_inv [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_red_inv [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_red_conv [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_red [in MetaCoq.PCUIC.PCUICConversion]
conv_cum_conv_ctx [in MetaCoq.PCUIC.PCUICConversion]
conv_red_conv [in MetaCoq.PCUIC.PCUICConversion]
conv_Prod_inv [in MetaCoq.PCUIC.PCUICConversion]
conv_context_app_same [in MetaCoq.PCUIC.PCUICContextConversion]
conv_cumul_context [in MetaCoq.PCUIC.PCUICContextConversion]
conv_alt_red_ctx_inv [in MetaCoq.PCUIC.PCUICContextConversion]
conv_alt_red_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
conv_eq_context_upto_leq_inv [in MetaCoq.PCUIC.PCUICContextConversion]
conv_leq_context_upto [in MetaCoq.PCUIC.PCUICContextConversion]
conv_eq_context_upto [in MetaCoq.PCUIC.PCUICContextConversion]
conv_ctx_set_binder_name [in MetaCoq.PCUIC.PCUICSR]
conv_refl' [in MetaCoq.PCUIC.PCUICSR]
conv_context_rel_to_extended_list [in MetaCoq.PCUIC.PCUICSR]
conv_context_rel_reln [in MetaCoq.PCUIC.PCUICSR]
conv_context_smash_end [in MetaCoq.PCUIC.PCUICSR]
conv_renameP [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
conv_context_smash [in MetaCoq.PCUIC.PCUICContexts]
conv_infer_ind [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_prod [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_sort [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
conv_check [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
conv_context_app [in MetaCoq.Erasure.Prelim]
conv_decls_irrel_sec [in MetaCoq.SafeChecker.PCUICTypeChecker]
cored_zipc [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_red_cored [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_const [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_red [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_proj [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_case [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_red_trans [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_trans' [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_welltyped [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICSafeLemmata]
cored_redp [in MetaCoq.SafeChecker.PCUICWfReduction]
cored_cored' [in MetaCoq.PCUIC.PCUICSN]
cored_eq_context_upto [in MetaCoq.PCUIC.PCUICSN]
cored_eq_term_upto [in MetaCoq.PCUIC.PCUICSN]
cored_eq_context_upto_names [in MetaCoq.PCUIC.PCUICSN]
cored_upto [in MetaCoq.PCUIC.PCUICSN]
cored_alt [in MetaCoq.PCUIC.PCUICSN]
cored_welltyped [in MetaCoq.SafeChecker.PCUICSafeReduce]
cored'_postpone [in MetaCoq.PCUIC.PCUICSN]
correct_valuation_of_labelling_satisfies [in MetaCoq.Template.common.uGraph]
correct_labelling_of_valuation_satisfies_iff [in MetaCoq.Template.common.uGraph]
cstr_branch_context_assumptions [in MetaCoq.PCUIC.PCUICProgress]
cstr_branch_context_assumptions [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cstr_branch_context_assumptions [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cstr_branch_context_assumptions [in MetaCoq.PCUIC.Syntax.PCUICCases]
cstr_branch_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
cstr_branch_context_length [in MetaCoq.Template.TypingWf]
csubst_mkApps [in MetaCoq.Erasure.EEtaExpandedFix]
csubst_mkApps [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
csubst_closed [in MetaCoq.Erasure.ECSubst]
csubst_mkApps [in MetaCoq.Erasure.ECSubst]
csubst_closed [in MetaCoq.Erasure.EOptimizePropDiscr]
csubst_mkApps [in MetaCoq.Erasure.EOptimizePropDiscr]
CS_For_all_add [in MetaCoq.Template.Universes]
CS_For_all_union [in MetaCoq.Template.Universes]
CS_union_empty [in MetaCoq.Template.Universes]
cs_subset_trans [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctxmap_fix_subst [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctxmap_cofix_subst [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctxmap_ext [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx_inst_closed [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ctx_inst_app_weak [in MetaCoq.PCUIC.PCUICInductiveInversion]
ctx_inst_eq_context [in MetaCoq.PCUIC.PCUICAlpha]
ctx_inst_impl [in MetaCoq.PCUIC.PCUICAlpha]
ctx_inst_wt [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx_inst_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx_length_rev_ind [in MetaCoq.PCUIC.Syntax.PCUICInduction]
ctx_length_ind [in MetaCoq.PCUIC.Syntax.PCUICInduction]
ctx_inst_merge' [in MetaCoq.PCUIC.PCUICSR]
ctx_inst_merge [in MetaCoq.PCUIC.PCUICSR]
ctx_inst_wt [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctx_inst_smash [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctx_inst_bd_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
ctx_inst_impl [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
ctx_inst_eq_context [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_open_terms [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_smash [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_smash_acc [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_cumul [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_sub_subst [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_sub_to_extended_list_k [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_spine_subst [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_ass [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_def [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_app_sub [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_sub_eq [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_app_inv [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_app [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_subst_length [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_sub_spec [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_weaken [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_subst [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_length [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_inst [in MetaCoq.PCUIC.PCUICSpine]
ctx_inst_typing_bd [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_app_impl [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_length [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_on_universes [in MetaCoq.SafeChecker.PCUICEqualityDec]
ctx_inst_wt [in MetaCoq.SafeChecker.PCUICTypeChecker]
cumulAlgo_cumulSpec [in MetaCoq.PCUIC.PCUICConversion]
cumulSpec_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
cumulSpec_typed_cumulAlgo [in MetaCoq.PCUIC.PCUICConversion]
cumulSpec_cumulAlgo_curry [in MetaCoq.PCUIC.PCUICConversion]
cumulSpec_cumulAlgo [in MetaCoq.PCUIC.PCUICConversion]
cumulSpec_renameP [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
cumulSpec0_ind_all [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cumul_sprop2 [in MetaCoq.PCUIC.PCUICElimination]
cumul_sprop1 [in MetaCoq.PCUIC.PCUICElimination]
cumul_prop2 [in MetaCoq.PCUIC.PCUICElimination]
cumul_prop1 [in MetaCoq.PCUIC.PCUICElimination]
cumul_sprop_inv [in MetaCoq.PCUIC.PCUICElimination]
cumul_prop_inv [in MetaCoq.PCUIC.PCUICElimination]
cumul_App_l [in MetaCoq.PCUIC.PCUICCumulativity]
cumul_alt [in MetaCoq.PCUIC.PCUICCumulativity]
cumul_decorate [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cumul_prop2' [in MetaCoq.Erasure.EArities]
cumul_prop1' [in MetaCoq.Erasure.EArities]
cumul_propositional [in MetaCoq.Erasure.EArities]
cumul_sprop2 [in MetaCoq.Erasure.EArities]
cumul_sprop1 [in MetaCoq.Erasure.EArities]
cumul_prop2 [in MetaCoq.Erasure.EArities]
cumul_prop1 [in MetaCoq.Erasure.EArities]
cumul_refl' [in MetaCoq.Template.Typing]
cumul_ctx_relSpec_Algo [in MetaCoq.PCUIC.PCUICInductiveInversion]
cumul_prop_is_open [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_mkApps_Ind_inv [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_mkApps [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_tLetIn [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_tProd [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_subst_instance [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_subst_instance_instance [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_args [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_prod_inv [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_conv_r [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_conv_l [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_cum_r [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_cum_l [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_trans [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_sym [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_sprop_props [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_props [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_prop_alt [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_cumul_prop [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_ind_confluence [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_sort_confluence [in MetaCoq.PCUIC.PCUICCumulProp]
cumul_decorate_hetero [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cumul_type_irrelevance [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cumul_context_Spec_Algo [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cumul_decorate [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cumul_decls_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
cumul_context_Algo_Spec [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cumul_Prod_inv [in MetaCoq.PCUIC.PCUICConversion]
cumul_mkApps [in MetaCoq.PCUIC.PCUICConversion]
cumul_it_mkProd_or_LetIn_smash [in MetaCoq.PCUIC.PCUICCanonicity]
cumul_context_app_same [in MetaCoq.PCUIC.PCUICContextConversion]
cumul_alt_red_ctx_inv [in MetaCoq.PCUIC.PCUICContextConversion]
cumul_alt_red_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
cumul_eq_context_upto [in MetaCoq.PCUIC.PCUICContextConversion]
cumul_leq_context_upto [in MetaCoq.PCUIC.PCUICContextConversion]
cumul_trans_red_leqterm [in MetaCoq.PCUIC.PCUICContextConversion]
cumul_red_ctx_inv [in MetaCoq.PCUIC.PCUICContextConversion]
cumul_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cumul_renameP [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cumul_ctx_rel_close' [in MetaCoq.SafeChecker.PCUICSafeChecker]
cumul_Sort_Prod_discr [in MetaCoq.Erasure.Prelim]
cumul_ctx_rel_cons [in MetaCoq.SafeChecker.PCUICTypeChecker]
cumul_decls_irrel_sec [in MetaCoq.SafeChecker.PCUICTypeChecker]
cuniv_sup_mon [in MetaCoq.Template.Universes]
cuniv_uprop_le_inv [in MetaCoq.Template.Universes]
cuniv_le_usprop_inv [in MetaCoq.Template.Universes]
cuniv_le_uprop_inv [in MetaCoq.Template.Universes]
cuniv_sup_not_uproplevel [in MetaCoq.Template.Universes]
cuniv_sup_comm [in MetaCoq.Template.Universes]
| 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) |