| 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) |
S (lemma)
same_lookup_ind_decl [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]same_hnf [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_reduce_stack [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod_last [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
sandwich [in MetaCoq.PCUIC.PCUICConfluence]
satisfies_subset [in MetaCoq.Template.Universes]
satisfies_union [in MetaCoq.Template.Universes]
satisfies_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies_subst_instance_ctr [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies0_subst_instance_ctr [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Sfst_decompose_app_rec [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
shiftf0 [in MetaCoq.PCUIC.PCUICAst]
shiftk_shift [in MetaCoq.PCUIC.PCUICParallelReduction]
shiftk_unfold [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_compose [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_shift_l [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_0 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftnPF_closedPT [in MetaCoq.PCUIC.PCUICSubstitution]
shiftnPS [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnPSS [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_shiftn [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
shiftnP_substP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_strengthenP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_xpredT [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_closedP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_S [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_impl [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_shiftn [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_add [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_mon [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
shiftnP_up [in MetaCoq.PCUIC.PCUICConvCumInversion]
shiftnP0 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnS [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_Upn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_ren_id [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_compose [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_lift_renaming [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_1_S [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_rshiftk [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_add [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_id [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_ext [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_ext_cond [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
shiftn_renaming_eq [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shiftn_renaming [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shiftn0 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn1_renaming [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shift_subst_consn_ge [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift_subst_instance [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift_Up_comm [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift_typing [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
shift_renaming [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shift_subst_consn_tip [in MetaCoq.PCUIC.PCUICSpine]
simpl_type_Case [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
simpl_pred [in MetaCoq.PCUIC.PCUICParallelReduction]
simpl_subst_k [in MetaCoq.Erasure.ELiftSubst]
simpl_subst [in MetaCoq.Erasure.ELiftSubst]
simpl_subst_rec [in MetaCoq.Erasure.ELiftSubst]
simpl_lift0 [in MetaCoq.Erasure.ELiftSubst]
simpl_lift [in MetaCoq.Erasure.ELiftSubst]
simpl_map_lift [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst' [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_k [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_rec [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift_ext [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift0 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_k [in MetaCoq.Template.LiftSubst]
simpl_subst [in MetaCoq.Template.LiftSubst]
simpl_subst_rec [in MetaCoq.Template.LiftSubst]
simpl_lift0 [in MetaCoq.Template.LiftSubst]
simpl_lift [in MetaCoq.Template.LiftSubst]
SisFixApp_mkApps [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
size_mkApps_l [in MetaCoq.Erasure.EInduction]
size_mkApps_f [in MetaCoq.Erasure.EInduction]
size_mkApps [in MetaCoq.Erasure.EInduction]
size_wf_local_app [in MetaCoq.PCUIC.PCUICTyping]
size_mkApps [in MetaCoq.PCUIC.utils.PCUICSize]
size_lift [in MetaCoq.PCUIC.Syntax.PCUICInduction]
size_decompose_app [in MetaCoq.PCUIC.Syntax.PCUICInduction]
size_decompose_app_rec [in MetaCoq.PCUIC.Syntax.PCUICInduction]
size_final [in MetaCoq.Erasure.EWcbvEval]
skipn_all_app_eq [in MetaCoq.Template.utils.MCList]
skipn_nth_error [in MetaCoq.Template.utils.MCList]
skipn_skipn [in MetaCoq.Template.utils.MCList]
skipn_eq_cons [in MetaCoq.Template.utils.MCList]
skipn_firstn_skipn [in MetaCoq.Template.utils.MCList]
skipn_map_length [in MetaCoq.Template.utils.MCList]
skipn_mapi_rec [in MetaCoq.Template.utils.MCList]
skipn_app_le [in MetaCoq.Template.utils.MCList]
skipn_all [in MetaCoq.Template.utils.MCList]
skipn_n_Sn [in MetaCoq.Template.utils.MCList]
skipn_0_eq [in MetaCoq.Template.utils.MCList]
skipn_0 [in MetaCoq.Template.utils.MCList]
skipn_all_app [in MetaCoq.Template.utils.MCList]
skipn_all2 [in MetaCoq.Template.utils.MCList]
skipn_length [in MetaCoq.Template.utils.MCList]
skipn_S [in MetaCoq.Template.utils.MCList]
skipn_nil [in MetaCoq.Template.utils.MCList]
skipn_ge [in MetaCoq.Erasure.EConstructorsAsBlocks]
skipn_expand_lets_ctx [in MetaCoq.PCUIC.PCUICInductives]
skipn_subst_instance [in MetaCoq.PCUIC.PCUICInductives]
skipn_lift_context [in MetaCoq.PCUIC.PCUICInductives]
skipn_projs [in MetaCoq.PCUIC.PCUICInductives]
skipn_subst [in MetaCoq.PCUIC.PCUICSigmaCalculus]
skipn_map_length [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
skipn_nil_length [in MetaCoq.PCUIC.PCUICSR]
skipn_subst_context [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
smash_context_app_expand_acc [in MetaCoq.PCUIC.PCUICInductives]
smash_context_acc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
smash_context_lift [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
smash_context_app_ass [in MetaCoq.PCUIC.Syntax.PCUICClosed]
smash_context_app_def [in MetaCoq.PCUIC.Syntax.PCUICClosed]
smash_context_subst [in MetaCoq.PCUIC.Syntax.PCUICClosed]
smash_context_subst_context_let_expand [in MetaCoq.PCUIC.PCUICSR]
smash_context_app_expand [in MetaCoq.PCUIC.PCUICContexts]
smash_context_idempotent [in MetaCoq.PCUIC.PCUICContexts]
smash_assumption_context [in MetaCoq.PCUIC.PCUICContexts]
smash_context_assumption_context [in MetaCoq.PCUIC.PCUICContexts]
smash_context_subst_empty [in MetaCoq.PCUIC.PCUICContexts]
smash_assumption_context [in MetaCoq.Erasure.Prelim]
snd_on_snd [in MetaCoq.Template.utils.MCProd]
snoc_app_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
solve_discr_args [in MetaCoq.Erasure.EEtaExpanded]
some_inj [in MetaCoq.Template.utils.MCOption]
sorts_local_ctx_All_local_assum_impl [in MetaCoq.PCUIC.PCUICElimination]
sorts_local_ctx_Pclosed [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
sorts_local_ctx_All_local_env [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
sorts_local_ctx_wf_sorts [in MetaCoq.SafeChecker.PCUICSafeChecker]
sorts_local_ctx_instantiate [in MetaCoq.PCUIC.PCUICContexts]
sorts_local_ctx_wf_local [in MetaCoq.PCUIC.PCUICContexts]
sort_of_product_twice [in MetaCoq.Template.Universes]
sort_of_product_idem [in MetaCoq.Template.Universes]
sort_of_type_irrel [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
sort_typing_spine [in MetaCoq.Erasure.EArities]
source_edge_of_level [in MetaCoq.Template.common.uGraph]
spec_map_succ [in MetaCoq.Template.Universes]
spine_subst_wt [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
spine_subst_expand_lets [in MetaCoq.PCUIC.PCUICInductives]
spine_subst_smash_inv [in MetaCoq.PCUIC.PCUICInductives]
spine_subst_smash_inv [in MetaCoq.SafeChecker.PCUICSafeRetyping]
spine_subst_wt [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
spine_subst_wt_terms [in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst_term_k [in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst_k [in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst_term [in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst [in MetaCoq.PCUIC.PCUICSR]
spine_nApp [in MetaCoq.Erasure.EAstUtils]
spine_tApp [in MetaCoq.Erasure.EAstUtils]
spine_mkApps [in MetaCoq.Erasure.EAstUtils]
spine_subst_app [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_extended_subst [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_cumul [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_smash [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_ctx_inst_sub [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst_to_extended_list_k_gen [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst_to_extended_list_k [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_to_extended_list_k [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_ctx_inst [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_is_closed_context_codom [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_is_closed_context [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_weakening [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_inst [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_smash_app_inv [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_app_inv [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_weaken [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst_first [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_conv [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_inj_subst [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_eq [in MetaCoq.PCUIC.PCUICSpine]
spine_subst_smash_inv [in MetaCoq.SafeChecker.PCUICTypeChecker]
split_suffix_maximal [in MetaCoq.Template.utils.MCList]
split_suffix_is_suffix [in MetaCoq.Template.utils.MCList]
split_prefix_maximal [in MetaCoq.Template.utils.MCList]
split_prefix_is_prefix [in MetaCoq.Template.utils.MCList]
split_at_firstn_skipn [in MetaCoq.Template.utils.MCList]
split_at_aux_firstn_skipn [in MetaCoq.Template.utils.MCList]
split_app3 [in MetaCoq.PCUIC.PCUICParallelReduction]
split_closed_context [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
split_nth [in MetaCoq.PCUIC.PCUICReduction]
sprop_sort_eq [in MetaCoq.PCUIC.PCUICCumulProp]
squash_isType_welltyped [in MetaCoq.SafeChecker.PCUICSafeRetyping]
sq_wf_local_app [in MetaCoq.SafeChecker.PCUICTypeChecker]
sq_wfl_nil [in MetaCoq.SafeChecker.PCUICTypeChecker]
sr_red1 [in MetaCoq.PCUIC.PCUICSR]
stack_context_decompose [in MetaCoq.PCUIC.PCUICSafeLemmata]
stack_context_stack_cat [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_stack_cat [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_cat_appstack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_appstack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_valid [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_atpos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_cons [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_context_appstack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_entry_context_mFix_mfix_bd [in MetaCoq.SafeChecker.PCUICSafeConversion]
stateR_Acc [in MetaCoq.SafeChecker.PCUICSafeConversion]
step_sound [in MetaCoq.Examples.tauto]
strengthening [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
strengthenP_addn [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
StringOT.compare_trans [in MetaCoq.Template.utils.bytestring]
StringOT.compare_sym [in MetaCoq.Template.utils.bytestring]
StringOT.compare_lt [in MetaCoq.Template.utils.bytestring]
StringOT.compare_refl [in MetaCoq.Template.utils.bytestring]
StringOT.compare_eq [in MetaCoq.Template.utils.bytestring]
StringOT.compare_spec [in MetaCoq.Template.utils.bytestring]
StringOT.eq_trans [in MetaCoq.Template.utils.bytestring]
StringOT.eq_sym [in MetaCoq.Template.utils.bytestring]
StringOT.eq_refl [in MetaCoq.Template.utils.bytestring]
StringOT.lt_not_eq [in MetaCoq.Template.utils.bytestring]
StringOT.lt_trans [in MetaCoq.Template.utils.bytestring]
string_repeat_length [in MetaCoq.SafeChecker.PCUICConsistency]
string_compare_irrel [in MetaCoq.Template.Reflect]
String.eqb_compare [in MetaCoq.Template.utils.bytestring]
String.print_parse_inv [in MetaCoq.Template.utils.bytestring]
strip_program_expanded [in MetaCoq.Erasure.ERemoveParams]
strip_env_expanded [in MetaCoq.Erasure.ERemoveParams]
strip_expanded_decl [in MetaCoq.Erasure.ERemoveParams]
strip_expanded_irrel [in MetaCoq.Erasure.ERemoveParams]
strip_expanded [in MetaCoq.Erasure.ERemoveParams]
strip_program_wf [in MetaCoq.Erasure.ERemoveParams]
strip_env_wf [in MetaCoq.Erasure.ERemoveParams]
strip_env_eq [in MetaCoq.Erasure.ERemoveParams]
strip_extends' [in MetaCoq.Erasure.ERemoveParams]
strip_decl_extends [in MetaCoq.Erasure.ERemoveParams]
strip_extends [in MetaCoq.Erasure.ERemoveParams]
strip_decl_wf [in MetaCoq.Erasure.ERemoveParams]
strip_wellformed_decl_irrel [in MetaCoq.Erasure.ERemoveParams]
strip_wellformed_irrel [in MetaCoq.Erasure.ERemoveParams]
strip_wellformed [in MetaCoq.Erasure.ERemoveParams]
strip_declared_constructor [in MetaCoq.Erasure.ERemoveParams]
strip_eval [in MetaCoq.Erasure.ERemoveParams]
strip_mkApps_etaexp [in MetaCoq.Erasure.ERemoveParams]
strip_isConstructApp [in MetaCoq.Erasure.ERemoveParams]
strip_isFixApp [in MetaCoq.Erasure.ERemoveParams]
strip_isFix [in MetaCoq.Erasure.ERemoveParams]
strip_isApp [in MetaCoq.Erasure.ERemoveParams]
strip_isBox [in MetaCoq.Erasure.ERemoveParams]
strip_isLambda [in MetaCoq.Erasure.ERemoveParams]
strip_tApp [in MetaCoq.Erasure.ERemoveParams]
strip_nth [in MetaCoq.Erasure.ERemoveParams]
strip_cunfold_cofix [in MetaCoq.Erasure.ERemoveParams]
strip_cunfold_fix [in MetaCoq.Erasure.ERemoveParams]
strip_cofix_subst [in MetaCoq.Erasure.ERemoveParams]
strip_fix_subst [in MetaCoq.Erasure.ERemoveParams]
strip_iota_red [in MetaCoq.Erasure.ERemoveParams]
strip_substl [in MetaCoq.Erasure.ERemoveParams]
strip_csubst [in MetaCoq.Erasure.ERemoveParams]
strip_mkApps [in MetaCoq.Erasure.ERemoveParams]
strip_mkApps_nonnil [in MetaCoq.Erasure.ERemoveParams]
strip_casts_mkApps_wf [in MetaCoq.Template.TypingWf]
strip_casts_mkApp_wf [in MetaCoq.Template.TypingWf]
strip_casts_mkApps_napp_wf [in MetaCoq.Template.TypingWf]
strip_casts_decompose_app [in MetaCoq.Template.TypingWf]
strip_casts_mkApps [in MetaCoq.Template.LiftSubst]
strip_casts_mkApps_tApp [in MetaCoq.Template.LiftSubst]
strip_casts_lift [in MetaCoq.Template.LiftSubst]
strong_nat_ind [in MetaCoq.Template.utils.MCArith]
strong_substitutivity [in MetaCoq.PCUIC.PCUICParallelReduction]
stuck_fix_value_args [in MetaCoq.PCUIC.PCUICWcbvEval]
stuck_fix_value_inv [in MetaCoq.PCUIC.PCUICWcbvEval]
stuck_fix_value_args [in MetaCoq.Erasure.EWcbvEval]
stuck_fix_value_inv [in MetaCoq.Erasure.EWcbvEval]
subject_is_open_term [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
subject_closed [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
subject_reduction_eval [in MetaCoq.PCUIC.PCUICCanonicity]
subject_reduction_ctx [in MetaCoq.PCUIC.PCUICSR]
subject_reduction_closed [in MetaCoq.PCUIC.PCUICSR]
subject_reduction1_closed [in MetaCoq.PCUIC.PCUICSR]
subject_reduction [in MetaCoq.PCUIC.PCUICSR]
subject_reduction1 [in MetaCoq.PCUIC.PCUICSR]
subrelations_eq_compare_extends [in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelations_compare_extends [in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelations_leq_extends [in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelations_extends [in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelation_leq_universe_eq_prop [in MetaCoq.PCUIC.PCUICCumulProp]
subrelation_eq_universe_eq_prop [in MetaCoq.PCUIC.PCUICCumulProp]
subslet_inds [in MetaCoq.PCUIC.PCUICArities]
subslet_app_inv [in MetaCoq.PCUIC.PCUICArities]
subslet_app_closed [in MetaCoq.PCUIC.PCUICArities]
subslet_inds_gen [in MetaCoq.PCUIC.PCUICArities]
subslet_well_subst [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_usubst [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_untyped_subslet [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_nth_error_lt [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_length [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_nth_error [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_def_tip [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_ass_tip [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_def [in MetaCoq.PCUIC.PCUICSubstitution]
subslet_smash_context [in MetaCoq.PCUIC.PCUICInductives]
subslet_extended_subst [in MetaCoq.PCUIC.PCUICInductives]
subslet_projs_smash [in MetaCoq.PCUIC.PCUICInductiveInversion]
subslet_projs [in MetaCoq.PCUIC.PCUICInductiveInversion]
subslet_cofix [in MetaCoq.PCUIC.PCUICInductiveInversion]
subslet_open [in MetaCoq.PCUIC.PCUICConversion]
subslet_extended_subst [in MetaCoq.PCUIC.PCUICContexts]
subslet_lift [in MetaCoq.PCUIC.PCUICContexts]
subslet_open_terms [in MetaCoq.PCUIC.PCUICSpine]
subslet_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICSpine]
subslet_cumul [in MetaCoq.PCUIC.PCUICSpine]
subslet_skipn [in MetaCoq.PCUIC.PCUICSpine]
subslet_app [in MetaCoq.PCUIC.PCUICSpine]
subslet_eq_context_alpha_dom [in MetaCoq.PCUIC.PCUICSpine]
subslet_eq_context_alpha [in MetaCoq.PCUIC.PCUICSpine]
subslet_cstr_branch_context [in MetaCoq.Erasure.Prelim]
subslet_cofix_subst [in MetaCoq.Erasure.Prelim]
subslet_fix_subst [in MetaCoq.Erasure.Prelim]
substitution [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_conv [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_cumul [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_wt_cumul_pb [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_let [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_wf_local [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_prop [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_cumul_let [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_cumul0 [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_untyped_cumul [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_red [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_untyped_red [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_untyped_let_red [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_let_red [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_red1 [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_check_one_cofix [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_check_one_fix [in MetaCoq.PCUIC.PCUICSubstitution]
substitution_subslet [in MetaCoq.PCUIC.PCUICInductiveInversion]
substitution_untyped_cumul_prop_cumul [in MetaCoq.PCUIC.PCUICCumulProp]
substitution_red_terms_conv_prop [in MetaCoq.PCUIC.PCUICCumulProp]
substitution_untyped_cumul_prop_equiv [in MetaCoq.PCUIC.PCUICCumulProp]
substitution_cumul_prop [in MetaCoq.PCUIC.PCUICCumulProp]
substitution_untyped_cumul_prop [in MetaCoq.PCUIC.PCUICCumulProp]
substitution_let_pred1 [in MetaCoq.PCUIC.PCUICParallelReduction]
substitution_ws_cumul_ctx_pb_subst_conv [in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb_subst_conv [in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_ctx_pb_red_subst [in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb_subst_conv [in MetaCoq.PCUIC.PCUICSR]
substitution_ws_cumul_pb_vdef [in MetaCoq.PCUIC.PCUICSpine]
substitution_ws_cumul_pb_vass [in MetaCoq.PCUIC.PCUICSpine]
substitution_wf_local_rel [in MetaCoq.SafeChecker.PCUICTypeChecker]
substitution0 [in MetaCoq.PCUIC.PCUICSubstitution]
substitution0_let_pred1 [in MetaCoq.PCUIC.PCUICParallelReduction]
substitution0_pred1 [in MetaCoq.PCUIC.PCUICParallelReduction]
substitution0_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
substitution1_untyped_cumul_prop [in MetaCoq.PCUIC.PCUICCumulProp]
substlet_typable [in MetaCoq.Erasure.ESubstitution]
substl_rel [in MetaCoq.Erasure.EInlineProjections]
substl_closed [in MetaCoq.Erasure.EInlineProjections]
substl_csubst_comm [in MetaCoq.Erasure.ECSubst]
substl_subst [in MetaCoq.Erasure.ECSubst]
substl_csubst_comm [in MetaCoq.Erasure.EOptimizePropDiscr]
substl_subst [in MetaCoq.Erasure.EOptimizePropDiscr]
substP_shiftnP [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
substP_shiftnP_gen [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
substP_shiftnP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
subst_cstr_concl_head [in MetaCoq.Template.EtaExpand]
subst_case_branch_context [in MetaCoq.Erasure.ESubstitution]
subst_instance_closedu [in MetaCoq.Template.Universes]
subst_instance_univ_closedu [in MetaCoq.Template.Universes]
subst_instance_level_expr_closedu [in MetaCoq.Template.Universes]
subst_instance_level_closedu [in MetaCoq.Template.Universes]
subst_telescope_subst_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
subst_telescope_subst_instance [in MetaCoq.PCUIC.PCUICArities]
subst_instance_empty [in MetaCoq.PCUIC.PCUICWfUniverses]
subst_context_app' [in MetaCoq.PCUIC.PCUICSubstitution]
subst_inst_case_context_wf [in MetaCoq.PCUIC.PCUICSubstitution]
subst_compare_context [in MetaCoq.PCUIC.PCUICSubstitution]
subst_compare_decl [in MetaCoq.PCUIC.PCUICSubstitution]
subst_compare_term [in MetaCoq.PCUIC.PCUICSubstitution]
subst_skipn [in MetaCoq.PCUIC.PCUICSubstitution]
subst_fn_eq [in MetaCoq.PCUIC.PCUICSubstitution]
subst_decompose_prod_assum_rec [in MetaCoq.PCUIC.PCUICSubstitution]
subst_to_extended_list_k [in MetaCoq.PCUIC.PCUICSubstitution]
subst_cstr_concl_head [in MetaCoq.PCUIC.PCUICSubstitution]
subst_destArity [in MetaCoq.PCUIC.PCUICSubstitution]
subst_fix_context [in MetaCoq.PCUIC.PCUICSubstitution]
subst_declared_constant [in MetaCoq.PCUIC.PCUICSubstitution]
subst_wf_local [in MetaCoq.PCUIC.PCUICSubstitution]
subst_is_constructor [in MetaCoq.PCUIC.PCUICSubstitution]
subst_unfold_cofix [in MetaCoq.PCUIC.PCUICSubstitution]
subst_unfold_fix [in MetaCoq.PCUIC.PCUICSubstitution]
subst_iota_red [in MetaCoq.PCUIC.PCUICSubstitution]
subst_length [in MetaCoq.PCUIC.PCUICSubstitution]
subst_decl_closed [in MetaCoq.PCUIC.PCUICSubstitution]
subst_instance_isLambda [in MetaCoq.PCUIC.PCUICEtaExpand]
subst_instance_isFix [in MetaCoq.PCUIC.PCUICEtaExpand]
subst_instance_isRel [in MetaCoq.PCUIC.PCUICEtaExpand]
subst_instance_isConstruct [in MetaCoq.PCUIC.PCUICEtaExpand]
subst_lift_subst [in MetaCoq.PCUIC.PCUICInductives]
subst_context_subst [in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_k_lift [in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_k_mkApps [in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_k_0 [in MetaCoq.PCUIC.PCUICInductives]
subst_context_lift_context_cancel [in MetaCoq.PCUIC.PCUICInductives]
subst_context_lift_context [in MetaCoq.PCUIC.PCUICInductives]
subst_context_extended_subst_expand [in MetaCoq.PCUIC.PCUICInductives]
subst_id [in MetaCoq.PCUIC.PCUICInductives]
subst_projs_inst [in MetaCoq.PCUIC.PCUICInductives]
subst_instance_projs [in MetaCoq.PCUIC.PCUICInductives]
subst_inds_concl_head [in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_closed_ctx_lift [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_let_expand_lift [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_let_expand_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_inds_smash_params [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_context_expand_lets_k [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_expand_lets_ctx [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_expand_lets [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_conv_closed [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_context_subst_context_comm [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_context_subst_context [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_variance_cstrs [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_cstrs_add [in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_skipn' [in MetaCoq.PCUIC.PCUICParallelReduction]
subst_leq_term [in MetaCoq.PCUIC.PCUICEquality]
subst_eq_term [in MetaCoq.PCUIC.PCUICEquality]
subst_shift_comm [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_decompo [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_map_subst_expand_lets_k [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_map_subst_expand_lets [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_extended_subst [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_lift_id [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_reli_lift_id [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_compose_r [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_idsn_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_ids_rel_ren [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_eq [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_shiftn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_inst' [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_inst [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_fn_subst_consn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_inst_aux [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_0s_shifts [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_0_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_compose_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_ids_ren [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_compose [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons' [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_ren [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_subst_consn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_0 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_idsn_consn_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_ids_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_lt_spec [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_ge [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_app [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons_gen [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_tip [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_nil [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_ids [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_expand_lets_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
subst_context_subst_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
subst_instance_ind_type_id [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_ind_sort_id [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_ws_cumul_ctx_pb_rel [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_id [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subst_context0_inst_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subst_context_inst_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subst_app_simpl [in MetaCoq.Erasure.ELiftSubst]
subst_app_decomp [in MetaCoq.Erasure.ELiftSubst]
subst_closed [in MetaCoq.Erasure.ELiftSubst]
subst_empty [in MetaCoq.Erasure.ELiftSubst]
subst_mkApps [in MetaCoq.Erasure.ELiftSubst]
subst_rel_eq [in MetaCoq.Erasure.ELiftSubst]
subst_rel_gt [in MetaCoq.Erasure.ELiftSubst]
subst_rel_lt [in MetaCoq.Erasure.ELiftSubst]
subst_instance_extended_subst [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_closedu [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_subst [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_it_mkProd_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_mkApps [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_lift [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_cons [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_nil [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_instance_length [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_nlctx [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
subst_instance_ws_cumul_ctx_pb_rel [in MetaCoq.PCUIC.PCUICConversion]
subst_instance_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICConversion]
subst_instance_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
subst_context_app0 [in MetaCoq.PCUIC.PCUICConversion]
subst_closedn [in MetaCoq.PCUIC.Syntax.PCUICClosed]
subst_context_subst_context [in MetaCoq.PCUIC.PCUICSR]
subst_it_mkProd_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_context' [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_context [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_comm [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_extended_subst_k [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_app [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_snoc0 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_decl0 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_subst_lift [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_simpl' [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_simpl [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_decomp [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_empty_eq [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_empty [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_mkApps [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_eq [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_gt [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_lt [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_telescope_comm [in MetaCoq.PCUIC.PCUICContextSubst]
subst_telescope_comm_rec [in MetaCoq.PCUIC.PCUICContextSubst]
subst_telescope_cons [in MetaCoq.PCUIC.PCUICContextSubst]
subst_instance_id [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_abstract_instance_id [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_abs [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_id_mdecl [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_check_one_cofix [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_check_one_fix [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_smash [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_app [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_app_rec [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_prod_assum [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_destArity [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_ws_cumul_pb [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate_set_preturn [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate_set_pparams [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_branches [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_branch [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_predicate [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_branch_type [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_expand_lets_ctx [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_expand_lets [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_to_extended_list [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_predicate_context [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_branch_context [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_inds [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_lift_context [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_subst_telescope [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_subst_context [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstr_args [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_app_ctx [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_app [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_extended_subst [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_super [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_make'_make [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_make [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstrs_union [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_monom_cstr [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstrs_two [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstr_two [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two_context [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_two [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ0_two [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_two [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_two [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_equal_inst_global_inst [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_equal_inst_inst [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_make [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_make' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_val' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ0_val' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_val' [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_val [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ0_val [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_val [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_val [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_csubst_comm [in MetaCoq.Erasure.ECSubst]
subst_instance_closedu [in MetaCoq.Template.UnivSubst]
subst_instance_subst [in MetaCoq.Template.UnivSubst]
subst_instance_length [in MetaCoq.Template.UnivSubst]
subst_instance_it_mkProd_or_LetIn [in MetaCoq.Template.UnivSubst]
subst_instance_mkApps [in MetaCoq.Template.UnivSubst]
subst_instance_lift [in MetaCoq.Template.UnivSubst]
subst_instance_cons [in MetaCoq.Template.UnivSubst]
subst_instance_level_var_instance [in MetaCoq.SafeChecker.PCUICSafeChecker]
subst_instance_level_lift [in MetaCoq.SafeChecker.PCUICSafeChecker]
subst_context_let_expand_length [in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_lift_id [in MetaCoq.PCUIC.PCUICContexts]
subst_lift_above [in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICContexts]
subst_context_smash_context [in MetaCoq.PCUIC.PCUICContexts]
subst_sorts_local_ctx [in MetaCoq.PCUIC.PCUICContexts]
subst_type_local_ctx [in MetaCoq.PCUIC.PCUICContexts]
subst_instance_to_extended_list_k [in MetaCoq.PCUIC.PCUICContexts]
subst_csubst_comm [in MetaCoq.Erasure.EOptimizePropDiscr]
subst_it_mkProd_or_LetIn [in MetaCoq.Template.LiftSubst]
subst_app_simpl [in MetaCoq.Template.LiftSubst]
subst_app_decomp [in MetaCoq.Template.LiftSubst]
subst_empty [in MetaCoq.Template.LiftSubst]
subst_mkApps [in MetaCoq.Template.LiftSubst]
subst_rel_eq [in MetaCoq.Template.LiftSubst]
subst_rel_gt [in MetaCoq.Template.LiftSubst]
subst_rel_lt [in MetaCoq.Template.LiftSubst]
subst_context_subst_telescope [in MetaCoq.PCUIC.PCUICSpine]
subst_context_rev_subst_telescope [in MetaCoq.PCUIC.PCUICSpine]
subst_context_lift_context_comm [in MetaCoq.PCUIC.PCUICSpine]
subst_map_lift_lift_context [in MetaCoq.PCUIC.PCUICSpine]
subst_extended_lift [in MetaCoq.PCUIC.PCUICSpine]
subst_lift1 [in MetaCoq.PCUIC.PCUICSpine]
subst_subst_context [in MetaCoq.PCUIC.PCUICSpine]
subst_ext_list_ext_subst [in MetaCoq.PCUIC.PCUICSpine]
subst_extended_subst [in MetaCoq.PCUIC.PCUICSpine]
subst_context_lift_id [in MetaCoq.PCUIC.PCUICSpine]
subst_rel0_lift_id [in MetaCoq.PCUIC.PCUICSpine]
subst_context_telescope [in MetaCoq.PCUIC.PCUICSpine]
subst_lift_lift [in MetaCoq.PCUIC.PCUICSpine]
subst_app_context_gen [in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_subst_context [in MetaCoq.PCUIC.PCUICSpine]
subst_instance_rev [in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_length [in MetaCoq.PCUIC.PCUICSpine]
subst_app_telescope [in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_app [in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_empty [in MetaCoq.PCUIC.PCUICSpine]
subst_sorts_local_ctx [in MetaCoq.PCUIC.PCUICSpine]
subst_type_local_ctx [in MetaCoq.PCUIC.PCUICSpine]
subst_global_uctx_invariants [in MetaCoq.SafeChecker.PCUICTypeChecker]
subst0_inst [in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst0_context [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst0_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICSpine]
subst1_mkApps [in MetaCoq.Erasure.ELiftSubst]
subst1_mkApps [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst1_inst [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
subst1_mkApps [in MetaCoq.Template.LiftSubst]
subst10_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subs_usubst [in MetaCoq.PCUIC.PCUICSubstitution]
subs_nth_error [in MetaCoq.PCUIC.PCUICSubstitution]
subs_nth_error_lt [in MetaCoq.PCUIC.PCUICSubstitution]
subs_nth_error_ge [in MetaCoq.PCUIC.PCUICSubstitution]
subs_length [in MetaCoq.PCUIC.PCUICSubstitution]
sub_context_set_empty [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
sub_context_set_empty [in MetaCoq.SafeChecker.PCUICSafeChecker]
succs_proper [in MetaCoq.Template.common.uGraph]
succ_inj [in MetaCoq.Template.Universes]
sup_idem [in MetaCoq.Template.Universes]
sup_comm [in MetaCoq.Template.Universes]
sup_subst_instance_univ [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sup_subst_instance_univ0 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sup0_assoc [in MetaCoq.Template.Universes]
sup0_idem [in MetaCoq.Template.Universes]
sup0_comm [in MetaCoq.Template.Universes]
switch_minus [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) |