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