| 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) |
I (lemma)
identity_typing [in MetaCoq.Examples.typing_correctness]idsn_spec [in MetaCoq.PCUIC.PCUICSigmaCalculus]
idsn_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
idsn_length [in MetaCoq.PCUIC.PCUICSigmaCalculus]
id_nth_spec [in MetaCoq.PCUIC.PCUICSigmaCalculus]
id_id [in MetaCoq.PCUIC.PCUICAst]
iff_is_true_eq_bool [in MetaCoq.Template.utils.MCUtils]
iff_ex [in MetaCoq.Template.utils.MCUtils]
iff_forall [in MetaCoq.Template.utils.MCUtils]
iff_reflect [in MetaCoq.SafeChecker.PCUICSafeConversion]
if_true_false [in MetaCoq.Template.utils.MCUtils]
IHup [in MetaCoq.PCUIC.PCUICInductives]
impredicative_product [in MetaCoq.Template.Universes]
impredicative_cuniv_product [in MetaCoq.Template.Universes]
InA_In_eq [in MetaCoq.Template.utils.MCList]
includes_deps_fold [in MetaCoq.Erasure.ErasureFunction]
includes_deps_union [in MetaCoq.Erasure.ErasureFunction]
incl_cs_refl [in MetaCoq.Template.Universes]
incl_cs_refl [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
incl_cs_refl [in MetaCoq.Erasure.ErasureFunction]
inds_nth_error [in MetaCoq.Erasure.EArities]
inds_spec [in MetaCoq.Template.Ast]
inds_length [in MetaCoq.Template.Ast]
inds_nth_error [in MetaCoq.PCUIC.PCUICInductiveInversion]
inds_is_open_terms [in MetaCoq.PCUIC.PCUICInductiveInversion]
inds_spec [in MetaCoq.PCUIC.Syntax.PCUICCases]
inds_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
inductive_cumulative_indices [in MetaCoq.PCUIC.PCUICInductiveInversion]
inductive_cumulative_indices_smash [in MetaCoq.SafeChecker.PCUICSafeRetyping]
ind_predicate_context_length [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind_predicate_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
infering_prod_on_free_vars [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
infering_on_free_vars [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
infering_ind_infering [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_ind_ind' [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_ind_ind [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_prod_infering [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_prod_prod' [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_prod_prod [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_sort_infering [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_sort_sort [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_checking [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_unique' [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_unique [in MetaCoq.PCUIC.Bidirectional.BDUnique]
infering_ind_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
infering_prod_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
infering_sort_isType [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
infering_sort_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
infering_typing [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
infer_irrel [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_as_sort_irrel [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
infer_as_prod_irrel [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Informative_extends [in MetaCoq.Erasure.ESubstitution]
Informative_cofix [in MetaCoq.Erasure.EArities]
init_graph_invariants [in MetaCoq.Template.common.uGraph]
inspect_nth_error_rename [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
instantiated_typing_spine_firstorder_spine [in MetaCoq.PCUIC.PCUICFirstorder]
instantiate_params_substP [in MetaCoq.Template.Typing]
instantiate_inds [in MetaCoq.PCUIC.PCUICInductives]
instantiate_wf_subslet [in MetaCoq.PCUIC.PCUICInductiveInversion]
instantiate_subslet [in MetaCoq.PCUIC.PCUICInductiveInversion]
instantiate_minductive [in MetaCoq.PCUIC.PCUICContexts]
inst_convSpec [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
inst_cumulSpec [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
inst_case_branch_context_inst [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
inst_case_predicate_context_inst [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
inst_context_on_free_vars [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
inst_case_branch_context_eq [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
inst_case_predicate_context_eq [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
inst_case_predicate_context_alpha_eq [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst_is_constructor [in MetaCoq.PCUIC.PCUICParallelReduction]
inst_extended_subst_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_rename_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_rename_assoc_n [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_mkApps [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_cofix [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_fix [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_letin [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_prod [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_lam [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_app [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_ext [in MetaCoq.PCUIC.PCUICSigmaCalculus]
inst_case_branch_context_rename [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
inst_case_predicate_context_rename [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
inst_case_predicate_context_eq [in MetaCoq.PCUIC.PCUICAlpha]
inst_case_branch_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
inst_case_predicate_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
inst_case_context_assumptions [in MetaCoq.PCUIC.Syntax.PCUICCases]
inst_case_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
inst_case_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICConvCumInversion]
inst_context_telescope [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_telescope_cons [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_telescope_upn0 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_subst_telescope [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_cumul_decls [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_conv_decls [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_cumul [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_conv [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_is_open_term [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_on_free_vars [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_ext_cond [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_set_preturn [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_set_pparams [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_unfold_cofix [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_unfold_fix [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_iota_red [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_extended_subst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_wf_cofixpoint [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_wf_fixpoint [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_check_one_cofix [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_check_one_fix [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_smash_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_app_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_decompose_prod_assum [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_type [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_context_gen [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_cstr_branch_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_inst_case_context_wf [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_inst_case_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_set_binder_name [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_inds [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_lift [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_lift [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_closed_extended_subst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_closedn_terms [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_cstr_args [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_closed_constructor_body [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_closed_decl [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_wf_branches [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_wf_branch [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_wf_predicate [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_case_predicate_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_subst_k [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_subst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_to_extended_list [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_reln [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_mkLambda_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_preturn [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_predicate_pcontext [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_fix_context_up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_fix_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_destArity [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_wf_local [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_closedn_ctx [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_decl_closed [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_ext_closed [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_closed0 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_subst0 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_mkApps [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_length [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_alt [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_context_snoc [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_case_branch_context_eq [in MetaCoq.PCUIC.PCUICCasesContexts]
inst_case_predicate_context_eq [in MetaCoq.PCUIC.PCUICCasesContexts]
inst_case_branch_context_eq [in MetaCoq.PCUIC.PCUICSR]
inst_case_branch_context_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_predicate_context_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_case_context_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst_closed [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
inst_ctxmap_up [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
inst_ctxmap [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
into_ws_cumul_pb_terms [in MetaCoq.PCUIC.PCUICInductiveInversion]
into_ws_cumul_ctx_pb_rel [in MetaCoq.PCUIC.PCUICInductiveInversion]
into_ws_cumul [in MetaCoq.PCUIC.PCUICInversion]
into_ws_cumul_pb_terms_Algo [in MetaCoq.SafeChecker.PCUICSafeRetyping]
into_wt_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_decls [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
into_ws_cumul_pb [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
into_red_terms [in MetaCoq.PCUIC.PCUICConvCumInversion]
into_closed_red [in MetaCoq.PCUIC.PCUICConversion]
into_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICContextConversion]
into_closed_red_ctx [in MetaCoq.PCUIC.PCUICSR]
introP [in MetaCoq.Template.utils.ReflectEq]
introT [in MetaCoq.Template.utils.MCReflect]
inversion_mkApps [in MetaCoq.PCUIC.PCUICProgress]
inversion_mkApps [in MetaCoq.PCUIC.PCUICValidity]
inversion_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICInversion]
inversion_CoFix [in MetaCoq.PCUIC.PCUICInversion]
inversion_Fix [in MetaCoq.PCUIC.PCUICInversion]
inversion_Proj [in MetaCoq.PCUIC.PCUICInversion]
inversion_Case [in MetaCoq.PCUIC.PCUICInversion]
inversion_Construct [in MetaCoq.PCUIC.PCUICInversion]
inversion_Ind [in MetaCoq.PCUIC.PCUICInversion]
inversion_Const [in MetaCoq.PCUIC.PCUICInversion]
inversion_App_size [in MetaCoq.PCUIC.PCUICInversion]
inversion_App [in MetaCoq.PCUIC.PCUICInversion]
inversion_LetIn [in MetaCoq.PCUIC.PCUICInversion]
inversion_Lambda [in MetaCoq.PCUIC.PCUICInversion]
inversion_Prod_size [in MetaCoq.PCUIC.PCUICInversion]
inversion_Prod [in MetaCoq.PCUIC.PCUICInversion]
inversion_Sort [in MetaCoq.PCUIC.PCUICInversion]
inversion_Evar [in MetaCoq.PCUIC.PCUICInversion]
inversion_Var [in MetaCoq.PCUIC.PCUICInversion]
inversion_Rel [in MetaCoq.PCUIC.PCUICInversion]
inversion_Rel [in MetaCoq.Examples.tauto]
inversion_it_mkProd_or_LetIn [in MetaCoq.SafeChecker.PCUICSafeChecker]
inversion_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICSpine]
inversion_mkApps_direct [in MetaCoq.PCUIC.PCUICSpine]
invert_it_Ind_eq_prod [in MetaCoq.Erasure.EArities]
invert_cumul_arity_l [in MetaCoq.PCUIC.PCUICArities]
invert_red1_letin [in MetaCoq.PCUIC.PCUICInductives]
invert_type_mkApps_ind [in MetaCoq.PCUIC.PCUICInductives]
invert_red_mkApps_tRel [in MetaCoq.PCUIC.PCUICInductiveInversion]
invert_Proj_Construct [in MetaCoq.PCUIC.PCUICInductiveInversion]
invert_Case_Construct [in MetaCoq.PCUIC.PCUICInductiveInversion]
invert_cumul_it_mkProd_or_LetIn_Sort_Ind [in MetaCoq.PCUIC.PCUICFirstorder]
invert_type_mkApps_tProd [in MetaCoq.SafeChecker.PCUICSafeConversion]
invert_red_lambda [in MetaCoq.PCUIC.PCUICConversion]
invert_cumul_ind_sort [in MetaCoq.PCUIC.PCUICConversion]
invert_cumul_sort_ind [in MetaCoq.PCUIC.PCUICConversion]
invert_cumul_ind_ind [in MetaCoq.PCUIC.PCUICConversion]
invert_cumul_ind_prod [in MetaCoq.PCUIC.PCUICConversion]
invert_cumul_prod_ind [in MetaCoq.PCUIC.PCUICConversion]
invert_red_mkApps_tInd [in MetaCoq.PCUIC.PCUICConversion]
invert_cumul_arity_l [in MetaCoq.PCUIC.PCUICConversion]
invert_cumul_arity_r [in MetaCoq.PCUIC.PCUICConversion]
invert_red_sort [in MetaCoq.PCUIC.PCUICConversion]
invert_red_prod [in MetaCoq.PCUIC.PCUICConversion]
invert_red_letin [in MetaCoq.PCUIC.PCUICConversion]
invert_fix_ind [in MetaCoq.PCUIC.PCUICCanonicity]
invert_ind_ind [in MetaCoq.PCUIC.PCUICCanonicity]
invert_cumul_arity_r_gen [in MetaCoq.PCUIC.PCUICCanonicity]
invert_cumul_arity_l_gen [in MetaCoq.PCUIC.PCUICCanonicity]
inv_opt_monad [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
inv_on_free_vars_decl [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
inv_opt_monad [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
inv_stuck_cofixes [in MetaCoq.SafeChecker.PCUICSafeConversion]
inv_stuck_fixes [in MetaCoq.SafeChecker.PCUICSafeConversion]
inv_reduced_body_proj [in MetaCoq.SafeChecker.PCUICSafeConversion]
inv_reduced_discriminees_case [in MetaCoq.SafeChecker.PCUICSafeConversion]
inv_wf_local [in MetaCoq.SafeChecker.PCUICTypeChecker]
In_map [in MetaCoq.PCUIC.PCUICElimination]
in_global_levels [in MetaCoq.PCUIC.PCUICWeakeningEnv]
In_Forall [in MetaCoq.Template.utils.All_Forall]
In_All [in MetaCoq.Template.utils.All_Forall]
In_size [in MetaCoq.Template.utils.MCList]
In_unfold_inj [in MetaCoq.Template.utils.MCList]
In_unfold_var [in MetaCoq.PCUIC.PCUICWfUniverses]
in_subst_instance [in MetaCoq.PCUIC.PCUICWfUniverses]
In_Level_global_ext_poly [in MetaCoq.PCUIC.PCUICWfUniverses]
In_lift_constraints [in MetaCoq.PCUIC.PCUICInductiveInversion]
in_global_ext_subst_abs_level [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
in_var_global_ext [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance_cstrs' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_subst_instance_cstrs [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
In_list_depth [in MetaCoq.PCUIC.Syntax.PCUICDepth]
In_Var_global_ext_poly [in MetaCoq.SafeChecker.PCUICSafeChecker]
In_unfold_inj [in MetaCoq.SafeChecker.PCUICSafeChecker]
iota_red_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
irred_equal [in MetaCoq.PCUIC.PCUICProgress]
isAppProd_isProd [in MetaCoq.PCUIC.PCUICSafeLemmata]
isAppProd_mkApps [in MetaCoq.PCUIC.PCUICSafeLemmata]
isApp_false_nApp [in MetaCoq.PCUIC.utils.PCUICAstUtils]
isApp_mkApps [in MetaCoq.PCUIC.utils.PCUICAstUtils]
isApp_mkApps [in MetaCoq.Erasure.ERemoveParams]
isArityHead_mkApps [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
isArity_mkApps [in MetaCoq.Erasure.EArities]
isArity_ind_type [in MetaCoq.Erasure.EArities]
isArity_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICArities]
isArity_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isArity_red [in MetaCoq.SafeChecker.PCUICSafeReduce]
isArity_mkAssumArity [in MetaCoq.SafeChecker.PCUICSafeReduce]
isArity_red1 [in MetaCoq.PCUIC.PCUICConversion]
isArity_subst [in MetaCoq.PCUIC.PCUICConversion]
isArity_ind [in MetaCoq.PCUIC.PCUICCanonicity]
isArity_typing_spine [in MetaCoq.PCUIC.PCUICCanonicity]
isArity_subst [in MetaCoq.PCUIC.PCUICCanonicity]
isBox_optimize [in MetaCoq.Erasure.EInlineProjections]
isBox_lift [in MetaCoq.Erasure.ELiftSubst]
isBox_mkApps_Construct [in MetaCoq.Erasure.ERemoveParams]
isBox_mkApps' [in MetaCoq.Erasure.ERemoveParams]
isBox_csubst [in MetaCoq.Erasure.ECSubst]
isBox_mkApps [in MetaCoq.Erasure.EWcbvEval]
isBox_optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
isConstructApp_mkApps [in MetaCoq.PCUIC.PCUICWcbvEval]
isConstructApp_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
isConstructApp_mkApps [in MetaCoq.Template.WcbvEval]
isConstructApp_mkApps [in MetaCoq.Erasure.EAstUtils]
isConstruct_app_eq_term_r [in MetaCoq.PCUIC.PCUICEquality]
isConstruct_app_eq_term_l [in MetaCoq.PCUIC.PCUICEquality]
isConstruct_erase [in MetaCoq.Erasure.ErasureFunction]
isConstruct_app_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
isConstruct_app_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
isConstruct_app_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
isConstruct_app_pred1 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
isconv_term_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_term_sound [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_sound [in MetaCoq.SafeChecker.PCUICSafeConversion]
isErasable_red [in MetaCoq.Erasure.EArities]
isErasable_unfold_cofix [in MetaCoq.Erasure.EArities]
isErasable_Propositional [in MetaCoq.Erasure.EArities]
isErasable_any_type [in MetaCoq.Erasure.EArities]
isErasable_Proof [in MetaCoq.Erasure.EArities]
isErasable_subst_instance [in MetaCoq.Erasure.ErasureProperties]
isErasable_irrel_global_env [in MetaCoq.Erasure.ErasureFunction]
isEtaExpFix_env_isEtaExp_env [in MetaCoq.Erasure.EEtaExpanded]
isEtaExpFix_isEtaExp [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_iota_red' [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_closedn [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_tApp_eval [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_tFix [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_FixApp [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_fixapp_mon [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_lookup [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_extends_decl [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_extends [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_app_extends [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_lookup_ext [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_tApp' [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_expanded [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_app_expanded [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_tApp [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_cunfold_cofix [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_cunfold_fix [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_cofix_subst [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_iota_red [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_fixsubstl [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_substl [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_closed [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps_intro [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_Constructor [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_mkApps_nonnil [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_app_mon [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_env_expanded_global_env [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_expanded [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_app_expanded [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_lookup [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_extends_decl [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_extends [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_app_extends [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_lookup_ext [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_cunfold_cofix [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_cunfold_fix [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_cofix_subst [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_fix_subst [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_iota_red [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_substl [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_mkApps_intro [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_app_mon [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_tApp [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_mkApps_intro_notConstruct [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_mkApps [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_Constructor [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_mkApps_napp [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_mkApps_nonnil [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_mkApps [in MetaCoq.Erasure.ERemoveParams]
isFixApp_mkApps [in MetaCoq.PCUIC.PCUICWcbvEval]
isFixApp_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
isFixApp_mkApps [in MetaCoq.Template.WcbvEval]
isFixApp_trans [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
isFixApp_mkApps [in MetaCoq.PCUIC.PCUICConversion]
isFixApp_mkApps [in MetaCoq.Erasure.EAstUtils]
isFixLambda_app_mkApps' [in MetaCoq.PCUIC.Syntax.PCUICViews]
isFixLambda_app_mkApps [in MetaCoq.PCUIC.Syntax.PCUICViews]
isFixLambda_app_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
isFix_mkApps [in MetaCoq.Erasure.EEtaExpandedFix]
isFix_mkApps [in MetaCoq.Erasure.EInlineProjections]
isFix_mkApps_Construct [in MetaCoq.Erasure.ERemoveParams]
isFix_mkApps' [in MetaCoq.Erasure.ERemoveParams]
isFix_mkApps [in MetaCoq.Erasure.EGenericMapEnv]
isFix_mkApps [in MetaCoq.Erasure.EOptimizePropDiscr]
isIndConstructApp_mkApps [in MetaCoq.PCUIC.PCUICConvCumInversion]
isLambda_eta_expand [in MetaCoq.Template.EtaExpand]
isLambda_unlift [in MetaCoq.Template.EtaExpand]
isLambda_isApp [in MetaCoq.Template.WfAst]
isLambda_optimize [in MetaCoq.Erasure.EInlineProjections]
isLambda_red1 [in MetaCoq.PCUIC.PCUICInductiveInversion]
isLambda_eq_term_r [in MetaCoq.PCUIC.PCUICEquality]
isLambda_eq_term_l [in MetaCoq.PCUIC.PCUICEquality]
isLambda_inv [in MetaCoq.PCUIC.PCUICAst]
isLambda_subst_instance [in MetaCoq.Erasure.ErasureProperties]
isLambda_inv [in MetaCoq.Erasure.ErasureFunction]
isLambda_subst [in MetaCoq.Erasure.ELiftSubst]
isLambda_lift [in MetaCoq.Erasure.ELiftSubst]
isLambda_mkApps [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
isLambda_subst [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
isLambda_lift [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
isLambda_mkApps_Construct [in MetaCoq.Erasure.ERemoveParams]
isLambda_mkApps' [in MetaCoq.Erasure.ERemoveParams]
isLambda_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
isLambda_csubst [in MetaCoq.Erasure.ECSubst]
isLambda_mkApps [in MetaCoq.Erasure.EWcbvEval]
isLambda_optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
isLambda_subst [in MetaCoq.Template.LiftSubst]
isLambda_lift [in MetaCoq.Template.LiftSubst]
isProdmkApps [in MetaCoq.PCUIC.PCUICSafeLemmata]
isPropositional_propositional_cstr [in MetaCoq.Erasure.EArities]
isPropositional_propositional [in MetaCoq.Erasure.EArities]
isred_full_nobeta [in MetaCoq.SafeChecker.PCUICSafeConversion]
isSortmkApps [in MetaCoq.PCUIC.PCUICSafeLemmata]
isStackApp_false_appstack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
isStuckfix_nApp [in MetaCoq.PCUIC.PCUICWcbvEval]
isStuckfix_nApp [in MetaCoq.Template.WcbvEval]
isStuckfix_nApp [in MetaCoq.Erasure.EWcbvEval]
isType_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICElimination]
isType_wt [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
isType_closed_red_refl [in MetaCoq.Erasure.EArities]
isType_red [in MetaCoq.Erasure.EArities]
isType_isErasable [in MetaCoq.Erasure.EArities]
isType_weaken [in MetaCoq.PCUIC.PCUICArities]
isType_it_mkProd_or_LetIn_wf_local [in MetaCoq.PCUIC.PCUICArities]
isType_substitution_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICArities]
isType_apply [in MetaCoq.PCUIC.PCUICArities]
isType_tLetIn_dom [in MetaCoq.PCUIC.PCUICArities]
isType_tLetIn_red [in MetaCoq.PCUIC.PCUICArities]
isType_subst_gen [in MetaCoq.PCUIC.PCUICArities]
isType_subst [in MetaCoq.PCUIC.PCUICArities]
isType_tProd [in MetaCoq.PCUIC.PCUICArities]
isType_Sort [in MetaCoq.PCUIC.PCUICArities]
isType_wf_universes [in MetaCoq.PCUIC.PCUICWfUniverses]
isType_closed [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
isType_mkApps_Ind_inv_spine [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
isType_substitution [in MetaCoq.PCUIC.PCUICSubstitution]
isType_closedPT [in MetaCoq.PCUIC.PCUICSubstitution]
isType_wf_local [in MetaCoq.PCUIC.PCUICSubstitution]
isType_case_predicate [in MetaCoq.PCUIC.PCUICInductives]
isType_mkApps_Ind_inv' [in MetaCoq.PCUIC.PCUICInductives]
isType_mkApps_Ind_inv [in MetaCoq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_smash [in MetaCoq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_subst [in MetaCoq.PCUIC.PCUICInductives]
isType_it_mkProd_or_LetIn_inv [in MetaCoq.PCUIC.PCUICInductives]
isType_mkApps_Ind [in MetaCoq.PCUIC.PCUICInductives]
isType_intro [in MetaCoq.PCUIC.PCUICInductives]
isType_weakening [in MetaCoq.PCUIC.PCUICValidity]
isType_subst_instance_decl [in MetaCoq.PCUIC.PCUICValidity]
isType_Sort_inv [in MetaCoq.PCUIC.PCUICValidity]
isType_extends [in MetaCoq.PCUIC.PCUICValidity]
isType_weaken [in MetaCoq.PCUIC.PCUICValidity]
isType_weaken_full [in MetaCoq.PCUIC.PCUICValidity]
isType_all_rels_subst_lift [in MetaCoq.PCUIC.PCUICInductiveInversion]
isType_subst_all_rels [in MetaCoq.PCUIC.PCUICInductiveInversion]
isType_is_open_term [in MetaCoq.PCUIC.PCUICInductiveInversion]
isType_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICInductiveInversion]
isType_mkApps_Ind_smash [in MetaCoq.PCUIC.PCUICInductiveInversion]
isType_on_ctx_free_vars [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
isType_on_free_vars [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
isType_alpha_ctx [in MetaCoq.PCUIC.PCUICAlpha]
isType_alpha [in MetaCoq.PCUIC.PCUICAlpha]
isType_eq_context_conversion [in MetaCoq.PCUIC.PCUICAlpha]
isType_context_conversion [in MetaCoq.PCUIC.PCUICFirstorder]
isType_wt [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
isType_subst_instance_id [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isType_subst_instance_decl [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
isType_ws_cumul_pb_refl [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
isType_open [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
isType_lift [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
isType_tLetIn [in MetaCoq.PCUIC.PCUICSR]
isType_red [in MetaCoq.PCUIC.PCUICSR]
isType_red1 [in MetaCoq.PCUIC.PCUICSR]
isType_mkApps_Ind_proj_inv [in MetaCoq.PCUIC.PCUICSR]
isType_subst_extended_subst [in MetaCoq.PCUIC.PCUICSR]
isType_expand_lets [in MetaCoq.PCUIC.PCUICSR]
isType_subst_arities [in MetaCoq.PCUIC.PCUICSR]
isType_weaken [in MetaCoq.PCUIC.PCUICSR]
isType_mkApps_inv [in MetaCoq.SafeChecker.PCUICSafeChecker]
isType_it_mkProd_or_LetIn_inv [in MetaCoq.SafeChecker.PCUICSafeChecker]
isType_it_mkProd [in MetaCoq.Erasure.EOptimizePropDiscr]
isType_tSort [in MetaCoq.Erasure.EOptimizePropDiscr]
isType_it_mkProd_or_LetIn_app [in MetaCoq.PCUIC.PCUICSpine]
isType_infering_sort [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
isType_mkApps_Ind_smash_inv [in MetaCoq.SafeChecker.PCUICTypeChecker]
isType_mkApps_Ind_smash [in MetaCoq.SafeChecker.PCUICTypeChecker]
isWfArity_prod_inv [in MetaCoq.Erasure.EArities]
isWfArity_subst_instance_decl [in MetaCoq.PCUIC.PCUICValidity]
isWfArity_alpha [in MetaCoq.PCUIC.PCUICAlpha]
isWfArity_sort [in MetaCoq.PCUIC.PCUICPrincipality]
isWfArity_red [in MetaCoq.PCUIC.PCUICSR]
isWfArity_red1 [in MetaCoq.PCUIC.PCUICSR]
is_type_subst [in MetaCoq.Erasure.ESubstitution]
Is_type_weakening [in MetaCoq.Erasure.ESubstitution]
Is_proof_extends [in MetaCoq.Erasure.ESubstitution]
Is_type_extends [in MetaCoq.Erasure.ESubstitution]
is_graph_of_uctx_levels [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
is_sprop_gt [in MetaCoq.Template.Universes]
is_prop_gt [in MetaCoq.Template.Universes]
is_sprop_sort_prod [in MetaCoq.Template.Universes]
is_prop_sort_prod [in MetaCoq.Template.Universes]
is_type_sup_r [in MetaCoq.Template.Universes]
is_sprop_sup_iff [in MetaCoq.Template.Universes]
is_prop_sup [in MetaCoq.Template.Universes]
is_prop_or_sprop_sort_sup_prop [in MetaCoq.Template.Universes]
is_prop_sort_sup_prop [in MetaCoq.Template.Universes]
is_prop_or_sprop_sort_sup [in MetaCoq.Template.Universes]
is_prop_sort_sup' [in MetaCoq.Template.Universes]
is_prop_sort_sup [in MetaCoq.Template.Universes]
is_not_prop_and_is_not_sprop [in MetaCoq.Template.Universes]
is_prop_and_is_sprop_val_false [in MetaCoq.Template.Universes]
is_sprop_val [in MetaCoq.Template.Universes]
is_prop_val [in MetaCoq.Template.Universes]
Is_proof_mkApps_tConstruct [in MetaCoq.PCUIC.PCUICElimination]
is_propositional_subst_instance [in MetaCoq.PCUIC.PCUICElimination]
is_ind_app_head_mkApps [in MetaCoq.PCUIC.utils.PCUICAstUtils]
Is_proof_app [in MetaCoq.Erasure.EArities]
Is_proof_ind [in MetaCoq.Erasure.EArities]
is_propositional_lower [in MetaCoq.Erasure.EArities]
is_propositional_bottom' [in MetaCoq.Erasure.EArities]
is_propositional_bottom [in MetaCoq.Erasure.EArities]
Is_proof_ty [in MetaCoq.Erasure.EArities]
Is_type_eval_inv [in MetaCoq.Erasure.EArities]
Is_type_eval [in MetaCoq.Erasure.EArities]
Is_type_red [in MetaCoq.Erasure.EArities]
Is_type_lambda [in MetaCoq.Erasure.EArities]
is_propositional_sort_prod [in MetaCoq.Erasure.EArities]
Is_type_app [in MetaCoq.Erasure.EArities]
is_prefix_rev_is_suffix [in MetaCoq.Template.utils.MCList]
is_suffix_is_prefix_rev [in MetaCoq.Template.utils.MCList]
is_prefix_cons_inv [in MetaCoq.Template.utils.MCList]
is_prefix_cons [in MetaCoq.Template.utils.MCList]
is_prefix_nil [in MetaCoq.Template.utils.MCList]
is_closed_ctx_closed [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
is_open_term_closed [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
is_propositional_cstr_optimize [in MetaCoq.Erasure.EInlineProjections]
is_propositional_optimize [in MetaCoq.Erasure.EInlineProjections]
is_closed_context_expand_let [in MetaCoq.PCUIC.PCUICInductives]
is_closed_context_weaken [in MetaCoq.PCUIC.PCUICInductiveInversion]
is_closed_subst_inst [in MetaCoq.PCUIC.PCUICInductiveInversion]
is_closed_context_weaken [in MetaCoq.PCUIC.PCUICCumulProp]
is_prop_subst_instance_level [in MetaCoq.PCUIC.PCUICCumulProp]
is_closed_context_snoc_inv [in MetaCoq.PCUIC.PCUICCumulProp]
is_sprop_prod [in MetaCoq.PCUIC.PCUICCumulProp]
is_prop_prod [in MetaCoq.PCUIC.PCUICCumulProp]
is_sprop_superE [in MetaCoq.PCUIC.PCUICCumulProp]
is_prop_superE [in MetaCoq.PCUIC.PCUICCumulProp]
is_sprop_bottom [in MetaCoq.PCUIC.PCUICCumulProp]
is_prop_bottom [in MetaCoq.PCUIC.PCUICCumulProp]
is_constructor_app_false [in MetaCoq.PCUIC.PCUICNormal]
is_consistent_spec2 [in MetaCoq.Template.common.uGraph]
is_graph_of_uctx_add [in MetaCoq.Template.common.uGraph]
is_graph_of_uctx_levels [in MetaCoq.Template.common.uGraph]
is_lt_spec [in MetaCoq.Template.common.uGraph]
is_consistent_spec [in MetaCoq.Template.common.uGraph]
is_closed_context_app_right [in MetaCoq.PCUIC.PCUICAlpha]
is_closed_context_app_left [in MetaCoq.PCUIC.PCUICAlpha]
is_closed_context_cstr_branch_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
is_closed_context_subst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
is_assumption_context_spec [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
is_constructor_prefix [in MetaCoq.PCUIC.Syntax.PCUICCases]
is_constructor_app_ge [in MetaCoq.PCUIC.Syntax.PCUICCases]
Is_type_conv_context [in MetaCoq.Erasure.ErasureProperties]
is_ConstructApp_erases [in MetaCoq.Erasure.ErasureProperties]
is_FixApp_erases [in MetaCoq.Erasure.ErasureProperties]
is_erasableb_irrel_global_env [in MetaCoq.Erasure.ErasureFunction]
is_arity_irrel [in MetaCoq.Erasure.ErasureFunction]
is_erasableb_irrel [in MetaCoq.Erasure.ErasureFunction]
is_erasableP [in MetaCoq.Erasure.ErasureFunction]
is_arityP [in MetaCoq.Erasure.ErasureFunction]
Is_conv_to_Arity_red [in MetaCoq.SafeChecker.PCUICSafeReduce]
is_constructor_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
is_leaf_sound [in MetaCoq.Examples.tauto]
is_nil [in MetaCoq.Template.WcbvEval]
is_open_term_subst_instance [in MetaCoq.PCUIC.PCUICConversion]
is_closed_context_subst_instance [in MetaCoq.PCUIC.PCUICConversion]
is_open_term_lift [in MetaCoq.PCUIC.PCUICConversion]
is_closed_context_lift [in MetaCoq.PCUIC.PCUICConversion]
is_open_fix_onone2 [in MetaCoq.PCUIC.PCUICConversion]
is_open_fix_or_cofix [in MetaCoq.PCUIC.PCUICConversion]
is_open_brs_OnOne2 [in MetaCoq.PCUIC.PCUICConversion]
is_open_case_set_preturn [in MetaCoq.PCUIC.PCUICConversion]
is_open_case_set_pparams [in MetaCoq.PCUIC.PCUICConversion]
is_open_case_split [in MetaCoq.PCUIC.PCUICConversion]
Is_conv_to_Arity_inv [in MetaCoq.PCUIC.PCUICConversion]
is_open_term_subst [in MetaCoq.PCUIC.PCUICConversion]
is_open_term_subst_gen [in MetaCoq.PCUIC.PCUICConversion]
is_closed_subst_context [in MetaCoq.PCUIC.PCUICConversion]
Is_conv_to_Arity_ind [in MetaCoq.PCUIC.PCUICCanonicity]
is_closed_context_cumul_app [in MetaCoq.PCUIC.PCUICContextConversion]
is_open_term_snoc [in MetaCoq.PCUIC.PCUICSR]
is_closed_context_set_binder_name [in MetaCoq.PCUIC.PCUICSR]
is_propositional_cstr_strip [in MetaCoq.Erasure.ERemoveParams]
is_propositional_strip [in MetaCoq.Erasure.ERemoveParams]
is_box_tApp [in MetaCoq.Erasure.EAstUtils]
is_box_mkApps [in MetaCoq.Erasure.EAstUtils]
is_allowed_elimination_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_prop_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_sprop_subst_instance_univ [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_prop_subst_instance_univ [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_constructor_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
is_constructor_pred1 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
is_propositional_cstr_gen_transform [in MetaCoq.Erasure.EGenericMapEnv]
is_propositional_gen_transform [in MetaCoq.Erasure.EGenericMapEnv]
is_propositional_cstr_optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
is_propositional_optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
is_box_inv [in MetaCoq.Erasure.EOptimizePropDiscr]
is_ind_app_head_mkApps [in MetaCoq.Template.AstUtils]
is_empty_app [in MetaCoq.Template.AstUtils]
is_closed_context_smash_end [in MetaCoq.PCUIC.PCUICSpine]
is_allowed_elimination_monotone [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
is_assumption_context_spec [in MetaCoq.Erasure.Prelim]
it_mkLambda_or_LetIn_app [in MetaCoq.PCUIC.utils.PCUICAstUtils]
it_mkLambda_or_LetIn_app [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
it_mkLambda_or_LetIn_inj [in MetaCoq.PCUIC.PCUICSafeLemmata]
it_mkLambda_or_LetIn_welltyped [in MetaCoq.PCUIC.PCUICSafeLemmata]
it_mkProd_red_Arity [in MetaCoq.Erasure.EArities]
it_mkProd_arity [in MetaCoq.Erasure.EArities]
it_mkProd_isArity [in MetaCoq.Erasure.EArities]
it_mkProd_or_LetIn_wf_local [in MetaCoq.PCUIC.PCUICArities]
it_mkProd_or_LetIn_inj [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
it_mkProd_or_LetIn_inj [in MetaCoq.Template.TypingWf]
| 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) |