| 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
S [module, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]S [constructor, in MetaRocq.Examples.demo]
S [module, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
S [module, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
SafeTemplateChecker [library]
safe_nth [definition, in MetaRocq.Utils.MRList]
safe_hd [definition, in MetaRocq.Erasure.EUnboxing]
safe_erasure_config [definition, in MetaRocq.ErasurePlugin.Erasure]
same_lookup_ind_decl [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_typing_result [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_ind_comp [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_sort_comp [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod_comp [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_typing_result_comp [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_hnf [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_reduce_stack [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod_last [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [definition, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
same_cstr_info_eta [lemma, in MetaRocq.Template.EtaExpand]
same_cstr_info [definition, in MetaRocq.Template.EtaExpand]
sandwich [lemma, in MetaRocq.PCUIC.PCUICConfluence]
satisfies [definition, in MetaRocq.Common.Universes]
satisfies_subset [lemma, in MetaRocq.Common.Universes]
satisfies_union [lemma, in MetaRocq.Common.Universes]
satisfies_combine_valuations [lemma, in MetaRocq.Common.UniversesDec]
satisfies_declare_and_uniquify_levels_2_1 [lemma, in MetaRocq.Common.UniversesDec]
satisfies_declare_and_uniquify_and_combine_levels_2_0 [lemma, in MetaRocq.Common.UniversesDec]
satisfies_declare_and_uniquify_and_combine_levels_1_1 [lemma, in MetaRocq.Common.UniversesDec]
satisfies_declare_and_uniquify_and_combine_levels_1_0 [lemma, in MetaRocq.Common.UniversesDec]
satisfies_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies_subst_instance_ctr [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies_subsets [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies_equal_sets [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies0 [inductive, in MetaRocq.Common.Universes]
satisfies0_sind [definition, in MetaRocq.Common.Universes]
satisfies0_ind [definition, in MetaRocq.Common.Universes]
satisfies0_Eq [constructor, in MetaRocq.Common.Universes]
satisfies0_Lt [constructor, in MetaRocq.Common.Universes]
satisfies0_subst_instance_ctr [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
scons [constructor, in MetaRocq.Examples.demo]
SE [module, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
SE [module, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
sec [section, in MetaRocq.Erasure.EGenericGlobalMap]
sec [section, in MetaRocq.Erasure.EGenericMapEnv]
sec.axioms_efl [variable, in MetaRocq.Erasure.EGenericMapEnv]
sec.cstrs_efl [variable, in MetaRocq.Erasure.EGenericMapEnv]
sec.efl [variable, in MetaRocq.Erasure.EGenericGlobalMap]
sec.efl [variable, in MetaRocq.Erasure.EGenericMapEnv]
sec.efl' [variable, in MetaRocq.Erasure.EGenericGlobalMap]
sec.efl' [variable, in MetaRocq.Erasure.EGenericMapEnv]
sec.GenTransformId [section, in MetaRocq.Erasure.EGenericGlobalMap]
sec.GenTransformId.gid [variable, in MetaRocq.Erasure.EGenericGlobalMap]
sec.gen_transform [variable, in MetaRocq.Erasure.EGenericGlobalMap]
sec.gen_transform_wellformed [variable, in MetaRocq.Erasure.EGenericMapEnv]
sec.gen_transform [variable, in MetaRocq.Erasure.EGenericMapEnv]
sec.gt [variable, in MetaRocq.Erasure.EGenericGlobalMap]
sec.GTWF [variable, in MetaRocq.Erasure.EGenericGlobalMap]
sec.Pre [variable, in MetaRocq.Erasure.EGenericMapEnv]
sec.wellformed_gen_transform_extends [variable, in MetaRocq.Erasure.EGenericMapEnv]
sem [definition, in MetaRocq.Examples.tauto]
semGen [definition, in MetaRocq.Examples.tauto]
seq [record, in MetaRocq.Examples.tauto]
SEq [module, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
SEq [module, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
seq_size [definition, in MetaRocq.Examples.tauto]
set_pparams_two [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
set_pparams [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
set_preturn_two [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
set_preturn [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
set_pcontext_two [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
set_pcontext [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
set_used [definition, in MetaRocq.Erasure.Typed.Optimize]
set_preturn_two [definition, in MetaRocq.PCUIC.PCUICConversion]
set_puinst [definition, in MetaRocq.PCUIC.PCUICConversion]
set_array_value [definition, in MetaRocq.PCUIC.PCUICReduction]
set_array_type [definition, in MetaRocq.PCUIC.PCUICReduction]
set_array_default [definition, in MetaRocq.PCUIC.PCUICReduction]
Sfst_decompose_app_rec [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
shift [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftf [definition, in MetaRocq.PCUIC.PCUICAst]
shiftf [abbreviation, in MetaRocq.Template.Ast]
shiftf0 [lemma, in MetaRocq.PCUIC.PCUICAst]
shiftk [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftk_unfold [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftk_compose [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftk_shift_l [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftk_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftk_0 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftk_shift [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
shiftn [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftnP [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnPF_closedPT [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
shiftnPS [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnPSS [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_shiftn [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
shiftnP_mon [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
shiftnP_up [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
shiftnP_predU [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_substP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_strengthenP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_xpredT [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_closedP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_S [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_shiftn [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_add [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_ext [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnS [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_ext_cond [lemma, in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
shiftn_Upn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_ren_id [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_compose [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_lift_renaming [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_1_S [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_rshiftk [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_add [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_id [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_ext [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn_renaming_eq [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
shiftn_renaming [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
shiftn0 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shiftn1_renaming [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
shift_typing [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningTyp]
shift_subst_consn_tip [lemma, in MetaRocq.PCUIC.PCUICSpine]
shift_subst_consn_ge [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shift_subst_instance [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shift_Up_comm [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
shift_renaming [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
show [projection, in MetaRocq.Utils.Show]
Show [record, in MetaRocq.Utils.Show]
show [constructor, in MetaRocq.Utils.Show]
Show [inductive, in MetaRocq.Utils.Show]
Show [library]
show_pstring [instance, in MetaRocq.Utils.Show]
show_Z [instance, in MetaRocq.Utils.Show]
show_positive [instance, in MetaRocq.Utils.Show]
show_float [instance, in MetaRocq.Utils.Show]
show_specfloat [instance, in MetaRocq.Utils.Show]
show_sint [instance, in MetaRocq.Utils.Show]
show_uint [instance, in MetaRocq.Utils.Show]
show_list [instance, in MetaRocq.Utils.Show]
show_option [instance, in MetaRocq.Utils.Show]
show_sum [instance, in MetaRocq.Utils.Show]
show_pair [instance, in MetaRocq.Utils.Show]
show_bool [instance, in MetaRocq.Utils.Show]
show_string [instance, in MetaRocq.Utils.Show]
show_bytestring [instance, in MetaRocq.Utils.Show]
show_program [instance, in MetaRocq.PCUIC.utils.PCUICPretty]
show_env [instance, in MetaRocq.PCUIC.utils.PCUICPretty]
Sigma [section, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
sigma [library]
sigmaarg [abbreviation, in MetaRocq.SafeChecker.PCUICSafeReduce]
Sigma.cf [variable, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
sigP [record, in MetaRocq.Utils.MRPrelude]
simpl_map_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst' [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_rec [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift_ext [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_k [lemma, in MetaRocq.Template.LiftSubst]
simpl_subst [lemma, in MetaRocq.Template.LiftSubst]
simpl_subst_rec [lemma, in MetaRocq.Template.LiftSubst]
simpl_lift0 [lemma, in MetaRocq.Template.LiftSubst]
simpl_lift [lemma, in MetaRocq.Template.LiftSubst]
simpl_pred [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
simpl_type_Case [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
simpl_subst_k [lemma, in MetaRocq.Erasure.ELiftSubst]
simpl_subst [lemma, in MetaRocq.Erasure.ELiftSubst]
simpl_subst_rec [lemma, in MetaRocq.Erasure.ELiftSubst]
simpl_lift0 [lemma, in MetaRocq.Erasure.ELiftSubst]
simpl_lift [lemma, in MetaRocq.Erasure.ELiftSubst]
SingletonProp [definition, in MetaRocq.PCUIC.PCUICElimination]
singleton_elim [definition, in MetaRocq.Examples.metarocq_tour]
SisFixApp_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
six [definition, in MetaRocq.Examples.demo]
size [definition, in MetaRocq.Examples.tauto]
size [definition, in MetaRocq.PCUIC.utils.PCUICSize]
size [definition, in MetaRocq.Utils.All_Forall]
size [definition, in MetaRocq.Erasure.EInduction]
size_wf_local_app [lemma, in MetaRocq.PCUIC.PCUICTyping]
size_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICSize]
size_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
size_decompose_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
size_decompose_app_rec [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
size_final [lemma, in MetaRocq.Erasure.EWcbvEval]
size_mkApps_l [lemma, in MetaRocq.Erasure.EInduction]
size_mkApps_f [lemma, in MetaRocq.Erasure.EInduction]
size_mkApps [lemma, in MetaRocq.Erasure.EInduction]
skipn_nil_length [lemma, in MetaRocq.PCUIC.PCUICSR]
skipn_subst_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
skipn_ge [lemma, in MetaRocq.Erasure.EImplementBox]
skipn_all_app_eq [lemma, in MetaRocq.Utils.MRList]
skipn_nth_error [lemma, in MetaRocq.Utils.MRList]
skipn_skipn [lemma, in MetaRocq.Utils.MRList]
skipn_eq_cons [lemma, in MetaRocq.Utils.MRList]
skipn_firstn_skipn [lemma, in MetaRocq.Utils.MRList]
skipn_mapi_rec [lemma, in MetaRocq.Utils.MRList]
skipn_app_le [lemma, in MetaRocq.Utils.MRList]
skipn_all [lemma, in MetaRocq.Utils.MRList]
skipn_n_Sn [lemma, in MetaRocq.Utils.MRList]
skipn_0_eq [lemma, in MetaRocq.Utils.MRList]
skipn_0 [lemma, in MetaRocq.Utils.MRList]
skipn_all_app [lemma, in MetaRocq.Utils.MRList]
skipn_all2 [lemma, in MetaRocq.Utils.MRList]
skipn_S [lemma, in MetaRocq.Utils.MRList]
skipn_nil [lemma, in MetaRocq.Utils.MRList]
skipn_app_prefix [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
skipn_repeat [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
skipn_firstn_slice [lemma, in MetaRocq.Erasure.Typed.Utils]
skipn_subst [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
skipn_ge [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
skipn_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICInductives]
skipn_subst_instance [lemma, in MetaRocq.PCUIC.PCUICInductives]
skipn_lift_context [lemma, in MetaRocq.PCUIC.PCUICInductives]
skipn_projs [lemma, in MetaRocq.PCUIC.PCUICInductives]
SL [module, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
SL [module, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
SL [module, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
SL [module, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
smash_context_subst_context_let_expand [lemma, in MetaRocq.PCUIC.PCUICSR]
smash_assumption_context [lemma, in MetaRocq.Erasure.Prelim]
smash_context_app_ass [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
smash_context_app_def [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
smash_context_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
smash_context_app_expand [lemma, in MetaRocq.PCUIC.PCUICContexts]
smash_context_idempotent [lemma, in MetaRocq.PCUIC.PCUICContexts]
smash_assumption_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
smash_context_assumption_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
smash_context_subst_empty [lemma, in MetaRocq.PCUIC.PCUICContexts]
smash_context_acc [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
smash_telescope [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
smash_context_app_expand_acc [lemma, in MetaRocq.PCUIC.PCUICInductives]
smash_context_lift [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
snd_erase_pcuic_program [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
snd_pair [lemma, in MetaRocq.Utils.MRProd]
snd_eq [definition, in MetaRocq.Utils.MRProd]
snd_on_snd [lemma, in MetaRocq.Utils.MRProd]
snd' [projection, in MetaRocq.Examples.demo]
snoc [definition, in MetaRocq.Common.BasicAst]
snoc [definition, in MetaRocq.Erasure.EAst]
snocP [lemma, in MetaRocq.Utils.MRList]
snoc_view_sind [definition, in MetaRocq.Utils.MRList]
snoc_view_rec [definition, in MetaRocq.Utils.MRList]
snoc_view_ind [definition, in MetaRocq.Utils.MRList]
snoc_view_rect [definition, in MetaRocq.Utils.MRList]
snoc_view_snoc [constructor, in MetaRocq.Utils.MRList]
snoc_view_nil [constructor, in MetaRocq.Utils.MRList]
snoc_view [inductive, in MetaRocq.Utils.MRList]
snoc_app_context [lemma, in MetaRocq.Common.BasicAst]
SN_to_WN [lemma, in MetaRocq.PCUIC.PCUICNormalization]
Sn_plus_one_transparent [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
solve_discr_args [lemma, in MetaRocq.Erasure.EEtaExpanded]
some_inj [lemma, in MetaRocq.Utils.MROption]
sort [abbreviation, in MetaRocq.Common.Universes]
Sort [module, in MetaRocq.Common.Universes]
SortCompare [section, in MetaRocq.Common.Universes]
SortCompare.cf [variable, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas [section, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas.eq_sort [variable, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas.eq_universe [variable, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas.leq_sort [variable, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas.leq_sort_n [variable, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas.leq_universe_n [variable, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas.lt_sort [variable, in MetaRocq.Common.Universes]
SortCompare.GeneralLemmas.univ [variable, in MetaRocq.Common.Universes]
_ <= _ [notation, in MetaRocq.Common.Universes]
_ < _ [notation, in MetaRocq.Common.Universes]
_ <_ _ _ [notation, in MetaRocq.Common.Universes]
_ <= _ (univ_scope) [notation, in MetaRocq.Common.Universes]
_ < _ (univ_scope) [notation, in MetaRocq.Common.Universes]
_ <_ _ _ (univ_scope) [notation, in MetaRocq.Common.Universes]
SortMap [module, in MetaRocq.Common.Universes]
SortMapDecide [module, in MetaRocq.Common.Universes]
SortMapExtraFact [module, in MetaRocq.Common.Universes]
SortMapFact [module, in MetaRocq.Common.Universes]
sorts_local_ctx_Pclosed [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
sorts_local_ctx_All_local_env [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
sorts_local_ctx_All_local_assum_impl [lemma, in MetaRocq.PCUIC.PCUICElimination]
sorts_local_ctx_app [lemma, in MetaRocq.PCUIC.PCUICContexts]
sorts_local_ctx_instantiate [lemma, in MetaRocq.PCUIC.PCUICContexts]
sorts_local_ctx_wf_local [lemma, in MetaRocq.PCUIC.PCUICContexts]
sorts_local_ctx_wf_sorts [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
sorts_local_ctx_All_wf_decl [lemma, in MetaRocq.Template.TypingWf]
sort_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
sort_of_product_twice [lemma, in MetaRocq.Common.Universes]
sort_of_product_idem [lemma, in MetaRocq.Common.Universes]
sort_sprop_le_inv [lemma, in MetaRocq.Common.Universes]
sort_prop_le_inv [lemma, in MetaRocq.Common.Universes]
sort_le_sprop_inv [lemma, in MetaRocq.Common.Universes]
sort_le_prop_inv [lemma, in MetaRocq.Common.Universes]
sort_of_type [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
sort_of_type_irrel [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
sort_of_products [definition, in MetaRocq.PCUIC.PCUICArities]
sort_typing_spine [lemma, in MetaRocq.Erasure.EArities]
Sort.clt [definition, in MetaRocq.Common.Universes]
Sort.csort_of_product [definition, in MetaRocq.Common.Universes]
Sort.csup [definition, in MetaRocq.Common.Universes]
Sort.csuper [definition, in MetaRocq.Common.Universes]
Sort.eqb [definition, in MetaRocq.Common.Universes]
Sort.eq_dec_sort [instance, in MetaRocq.Common.Universes]
Sort.family [inductive, in MetaRocq.Common.Universes]
Sort.family_sind [definition, in MetaRocq.Common.Universes]
Sort.family_rec [definition, in MetaRocq.Common.Universes]
Sort.family_ind [definition, in MetaRocq.Common.Universes]
Sort.family_rect [definition, in MetaRocq.Common.Universes]
Sort.fProp [constructor, in MetaRocq.Common.Universes]
Sort.fSProp [constructor, in MetaRocq.Common.Universes]
Sort.fType [constructor, in MetaRocq.Common.Universes]
Sort.get_is_level [definition, in MetaRocq.Common.Universes]
Sort.is_type_sort [definition, in MetaRocq.Common.Universes]
Sort.is_sprop_propositional [lemma, in MetaRocq.Common.Universes]
Sort.is_prop_propositional [lemma, in MetaRocq.Common.Universes]
Sort.is_propositional [definition, in MetaRocq.Common.Universes]
Sort.is_prop [definition, in MetaRocq.Common.Universes]
Sort.is_sprop [definition, in MetaRocq.Common.Universes]
Sort.is_level [definition, in MetaRocq.Common.Universes]
Sort.is_levels [definition, in MetaRocq.Common.Universes]
Sort.lt [definition, in MetaRocq.Common.Universes]
Sort.ltPropSProp [constructor, in MetaRocq.Common.Universes]
Sort.ltPropType [constructor, in MetaRocq.Common.Universes]
Sort.ltSPropType [constructor, in MetaRocq.Common.Universes]
Sort.ltTypeType [constructor, in MetaRocq.Common.Universes]
Sort.lt__sind [definition, in MetaRocq.Common.Universes]
Sort.lt__ind [definition, in MetaRocq.Common.Universes]
Sort.lt_ [inductive, in MetaRocq.Common.Universes]
Sort.map [definition, in MetaRocq.Common.Universes]
Sort.of_levels [definition, in MetaRocq.Common.Universes]
Sort.on_sort [definition, in MetaRocq.Common.Universes]
Sort.OT [module, in MetaRocq.Common.Universes]
Sort.OTOrig [module, in MetaRocq.Common.Universes]
Sort.OT.compare [definition, in MetaRocq.Common.Universes]
Sort.OT.compare_spec [lemma, in MetaRocq.Common.Universes]
Sort.OT.eq [definition, in MetaRocq.Common.Universes]
Sort.OT.eq_dec [definition, in MetaRocq.Common.Universes]
Sort.OT.eq_equiv [definition, in MetaRocq.Common.Universes]
Sort.OT.lt [definition, in MetaRocq.Common.Universes]
Sort.OT.lt_compat [definition, in MetaRocq.Common.Universes]
Sort.OT.lt_strorder [instance, in MetaRocq.Common.Universes]
Sort.OT.t [definition, in MetaRocq.Common.Universes]
Sort.reflect_eq_sort [instance, in MetaRocq.Common.Universes]
Sort.sort_of_product [definition, in MetaRocq.Common.Universes]
Sort.sort_of_product_ [definition, in MetaRocq.Common.Universes]
Sort.sProp [constructor, in MetaRocq.Common.Universes]
Sort.sSProp [constructor, in MetaRocq.Common.Universes]
Sort.sType [constructor, in MetaRocq.Common.Universes]
Sort.sType_super [lemma, in MetaRocq.Common.Universes]
Sort.sType_super_ [lemma, in MetaRocq.Common.Universes]
Sort.sup [definition, in MetaRocq.Common.Universes]
Sort.super [definition, in MetaRocq.Common.Universes]
Sort.super_ [definition, in MetaRocq.Common.Universes]
Sort.sup_ [definition, in MetaRocq.Common.Universes]
Sort.t [definition, in MetaRocq.Common.Universes]
Sort.to_family_to_csort [lemma, in MetaRocq.Common.Universes]
Sort.to_csort [definition, in MetaRocq.Common.Universes]
Sort.to_family [definition, in MetaRocq.Common.Universes]
Sort.type0 [definition, in MetaRocq.Common.Universes]
Sort.type1 [definition, in MetaRocq.Common.Universes]
Sort.t__sind [definition, in MetaRocq.Common.Universes]
Sort.t__rec [definition, in MetaRocq.Common.Universes]
Sort.t__ind [definition, in MetaRocq.Common.Universes]
Sort.t__rect [definition, in MetaRocq.Common.Universes]
Sort.t_ [inductive, in MetaRocq.Common.Universes]
source_edge_of_level [lemma, in MetaRocq.Common.uGraph]
spcons [abbreviation, in MetaRocq.PCUIC.PCUICSpine]
SpecializeAllWays [library]
SpecializeBy [library]
SpecializeUnderBindersBy [library]
spec_map_succ [lemma, in MetaRocq.Common.Universes]
spine [definition, in MetaRocq.Erasure.EAstUtils]
Spines [section, in MetaRocq.PCUIC.PCUICClassification]
Spines.cf [variable, in MetaRocq.PCUIC.PCUICClassification]
Spines.wfΣ [variable, in MetaRocq.PCUIC.PCUICClassification]
Spines.Σ [variable, in MetaRocq.PCUIC.PCUICClassification]
spine_subst_wt_terms [lemma, in MetaRocq.PCUIC.PCUICSR]
spine_subst_inst_subst_term_k [lemma, in MetaRocq.PCUIC.PCUICSR]
spine_subst_inst_subst_k [lemma, in MetaRocq.PCUIC.PCUICSR]
spine_subst_inst_subst_term [lemma, in MetaRocq.PCUIC.PCUICSR]
spine_subst_inst_subst [lemma, in MetaRocq.PCUIC.PCUICSR]
spine_subst_vass' [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_vass [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_app [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_extended_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_cumul [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_smash [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_ctx_inst_sub [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_subst_to_extended_list_k_gen [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_subst_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_ctx_inst [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_is_closed_context_codom [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_is_closed_context [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_weakening [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_inst [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_smash_app_inv [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_app_inv [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_weaken [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_subst_first [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_conv [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_inj_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_eq [lemma, in MetaRocq.PCUIC.PCUICSpine]
spine_codom_wf [projection, in MetaRocq.PCUIC.PCUICSpine]
spine_dom_wf [projection, in MetaRocq.PCUIC.PCUICSpine]
spine_subst [record, in MetaRocq.PCUIC.PCUICSpine]
spine_subst_smash_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
spine_subst_wt [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
spine_subst_expand_lets [lemma, in MetaRocq.PCUIC.PCUICInductives]
spine_subst_smash_inv [lemma, in MetaRocq.PCUIC.PCUICInductives]
spine_subst_smash_inv [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
spine_subst_wt [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
spine_nApp [lemma, in MetaRocq.Erasure.EAstUtils]
spine_tApp [lemma, in MetaRocq.Erasure.EAstUtils]
spine_mkApps [lemma, in MetaRocq.Erasure.EAstUtils]
SplitInContext [library]
SplitPrefix [section, in MetaRocq.Utils.MRList]
SplitPrefix.A [variable, in MetaRocq.Utils.MRList]
Simp (ssripat_scope) [notation, in MetaRocq.Utils.MRList]
SplitSuffix [section, in MetaRocq.Utils.MRList]
SplitSuffix.A [variable, in MetaRocq.Utils.MRList]
split_suffix_maximal [lemma, in MetaRocq.Utils.MRList]
split_suffix_is_suffix [lemma, in MetaRocq.Utils.MRList]
split_suffix [definition, in MetaRocq.Utils.MRList]
split_prefix_maximal [lemma, in MetaRocq.Utils.MRList]
split_prefix_is_prefix [lemma, in MetaRocq.Utils.MRList]
split_prefix [definition, in MetaRocq.Utils.MRList]
split_at_firstn_skipn [lemma, in MetaRocq.Utils.MRList]
split_at_aux_firstn_skipn [lemma, in MetaRocq.Utils.MRList]
split_at [definition, in MetaRocq.Utils.MRList]
split_at_aux [definition, in MetaRocq.Utils.MRList]
split_closed_context [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
split_common_prefix [definition, in MetaRocq.Quotation.CommonUtils]
split_modpath [definition, in MetaRocq.Quotation.CommonUtils]
split_common_prefix_ls [definition, in MetaRocq.Quotation.CommonUtils]
split_app3 [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
split_nth [lemma, in MetaRocq.PCUIC.PCUICReduction]
spnil [abbreviation, in MetaRocq.PCUIC.PCUICSpine]
sProp [abbreviation, in MetaRocq.Common.Universes]
sprop_sort_eq [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
squash [record, in MetaRocq.Utils.MRSquash]
squash_isType_welltyped [lemma, in MetaRocq.SafeChecker.PCUICSafeRetyping]
sq_wf_pop_decl [lemma, in MetaRocq.Erasure.Typed.Erasure]
sq_red_transitivity [lemma, in MetaRocq.Erasure.Typed.Erasure]
sq_ws_cumul_pb [definition, in MetaRocq.PCUIC.PCUICConversion]
sq_wf_local_app [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
sq_wfl_nil [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
SRContext [section, in MetaRocq.PCUIC.PCUICSR]
SRContext.cf [variable, in MetaRocq.PCUIC.PCUICSR]
_ ⊢ _ ⇝1 _ (pcuic) [notation, in MetaRocq.PCUIC.PCUICSR]
sr_stmt [definition, in MetaRocq.PCUIC.PCUICSR]
sr_red1 [lemma, in MetaRocq.PCUIC.PCUICSR]
SR_red1 [definition, in MetaRocq.PCUIC.PCUICSR]
SS [constructor, in MetaRocq.Examples.demo]
sSProp [abbreviation, in MetaRocq.Common.Universes]
ST [module, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ST [module, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
st [projection, in MetaRocq.SafeChecker.PCUICSafeConversion]
ST [module, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
ST [module, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
stack [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
StackHeadError [constructor, in MetaRocq.SafeChecker.PCUICErrors]
StackMismatch [constructor, in MetaRocq.SafeChecker.PCUICErrors]
Stacks [section, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Stacks [section, in MetaRocq.PCUIC.PCUICReduction]
Stacks.Σ [variable, in MetaRocq.PCUIC.Syntax.PCUICPosition]
Stacks.Σ [variable, in MetaRocq.PCUIC.PCUICReduction]
StackTailError [constructor, in MetaRocq.SafeChecker.PCUICErrors]
stack_context_stack_cat [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_position_stack_cat [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_cat_appstack [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_position_appstack [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_pos [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_position_valid [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_position_atpos [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_position_cons [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_position [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_entry_choice [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_context_appstack [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_context [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_entry_context [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_entry [inductive, in MetaRocq.PCUIC.Syntax.PCUICPosition]
stack_context_decompose [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
stack_entry_context_mFix_mfix_bd [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
standard_model [library]
state [inductive, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR [inductive, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_Acc [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_sind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_ind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_Args_Fallback [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_Fallback_Term [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_Args_Term [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
stateR_Term_Reduction [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
state_sind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
state_rec [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
state_ind [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
state_rect [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
step_sound [lemma, in MetaRocq.Examples.tauto]
stk1 [projection, in MetaRocq.SafeChecker.PCUICSafeConversion]
stk2 [projection, in MetaRocq.SafeChecker.PCUICSafeConversion]
streamn [inductive, in MetaRocq.Examples.demo]
strengthening [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
strengthening_type [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
strengthenP [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
strengthenP_addn [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
strengthenP_proper [instance, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
strictest_checker_flags_strictest [lemma, in MetaRocq.Common.config]
strictest_checker_flags [definition, in MetaRocq.Common.config]
strictly_extends_decls_wf [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
strictly_extends_decls_extends_global_env [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
strictly_extends_decls_lookup [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
strictly_extends_decls_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
strictly_extends_lookups [lemma, in MetaRocq.ErasurePlugin.ETransform]
strictly_extends_decls_wf_local [definition, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
string [abbreviation, in MetaRocq.Utils.MRString]
string [abbreviation, in MetaRocq.Utils.bytestring]
String [module, in MetaRocq.Utils.bytestring]
StringOT [module, in MetaRocq.Utils.bytestring]
StringOTOrig [module, in MetaRocq.Utils.bytestring]
StringOT.compare [definition, in MetaRocq.Utils.bytestring]
StringOT.compare_trans [lemma, in MetaRocq.Utils.bytestring]
StringOT.compare_sym [lemma, in MetaRocq.Utils.bytestring]
StringOT.compare_lt [lemma, in MetaRocq.Utils.bytestring]
StringOT.compare_refl [lemma, in MetaRocq.Utils.bytestring]
StringOT.compare_eq [lemma, in MetaRocq.Utils.bytestring]
StringOT.compare_spec [lemma, in MetaRocq.Utils.bytestring]
StringOT.eq [definition, in MetaRocq.Utils.bytestring]
StringOT.eq_leibniz [definition, in MetaRocq.Utils.bytestring]
StringOT.eq_dec [definition, in MetaRocq.Utils.bytestring]
StringOT.eq_trans [lemma, in MetaRocq.Utils.bytestring]
StringOT.eq_sym [lemma, in MetaRocq.Utils.bytestring]
StringOT.eq_refl [lemma, in MetaRocq.Utils.bytestring]
StringOT.eq_equiv [definition, in MetaRocq.Utils.bytestring]
StringOT.lt [definition, in MetaRocq.Utils.bytestring]
StringOT.lt_compat [definition, in MetaRocq.Utils.bytestring]
StringOT.lt_strorder [instance, in MetaRocq.Utils.bytestring]
StringOT.lt_irreflexive [definition, in MetaRocq.Utils.bytestring]
StringOT.lt_transitive [instance, in MetaRocq.Utils.bytestring]
StringOT.lt_not_eq [lemma, in MetaRocq.Utils.bytestring]
StringOT.lt_trans [lemma, in MetaRocq.Utils.bytestring]
StringOT.reflect_eq_string [instance, in MetaRocq.Utils.bytestring]
StringOT.t [definition, in MetaRocq.Utils.bytestring]
string_of_universe_instance [definition, in MetaRocq.Common.Universes]
string_of_sort [definition, in MetaRocq.Common.Universes]
string_of_level_expr [definition, in MetaRocq.Common.Universes]
string_of_level [definition, in MetaRocq.Common.Universes]
string_of_term [definition, in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_term [definition, in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_def [definition, in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_branch [definition, in MetaRocq.Template.AstUtils]
string_of_term_tree.string_of_predicate [definition, in MetaRocq.Template.AstUtils]
_ ^ _ [notation, in MetaRocq.Template.AstUtils]
string_of_term_tree [module, in MetaRocq.Template.AstUtils]
string_of_pstring [definition, in MetaRocq.Utils.Show]
string_of_float [definition, in MetaRocq.Utils.Show]
string_of_prim_int [definition, in MetaRocq.Utils.Show]
string_of_specfloat [definition, in MetaRocq.Utils.Show]
string_of_option [definition, in MetaRocq.Utils.Show]
string_of_bool [definition, in MetaRocq.Utils.Show]
string_show [definition, in MetaRocq.Utils.Show]
string_compare_irrel [lemma, in MetaRocq.Common.Reflect]
string_of_env_error [definition, in MetaRocq.SafeChecker.PCUICErrors]
string_of_type_error [definition, in MetaRocq.SafeChecker.PCUICErrors]
string_of_conv_error [definition, in MetaRocq.SafeChecker.PCUICErrors]
string_of_conv_pb [definition, in MetaRocq.SafeChecker.PCUICErrors]
string_of_Z [definition, in MetaRocq.SafeChecker.PCUICErrors]
string_of_Z [definition, in MetaRocq.Utils.MRString]
string_of_positive [definition, in MetaRocq.Utils.MRString]
string_of_nat [definition, in MetaRocq.Utils.MRString]
string_of_uint [definition, in MetaRocq.Utils.MRString]
string_of_list [definition, in MetaRocq.Utils.MRString]
string_of_list_aux [definition, in MetaRocq.Utils.MRString]
string_of_term [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
string_of_aname [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
string_of_uint63_model [definition, in MetaRocq.Common.BasicAst]
string_of_def [definition, in MetaRocq.Common.BasicAst]
string_of_case_info [definition, in MetaRocq.Common.BasicAst]
string_of_relevance [definition, in MetaRocq.Common.BasicAst]
string_of_name [definition, in MetaRocq.Common.BasicAst]
string_of_predicate [definition, in MetaRocq.PCUIC.PCUICAst]
string_of_branch [definition, in MetaRocq.PCUIC.PCUICAst]
string_of_type_error [definition, in MetaRocq.Template.Checker]
string_of_gref [definition, in MetaRocq.Common.Kernames]
string_of_inductive [definition, in MetaRocq.Common.Kernames]
string_of_kername [definition, in MetaRocq.Common.Kernames]
string_of_modpath [definition, in MetaRocq.Common.Kernames]
string_of_dirpath [definition, in MetaRocq.Common.Kernames]
string_of_nat_inj [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
string_of_uint_inj [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
string_of_nat_empty [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
string_eqdec [instance, in MetaRocq.Utils.MRPrelude]
string_of_branch [definition, in MetaRocq.Template.Ast]
string_of_predicate [definition, in MetaRocq.Template.Ast]
string_of_prim [definition, in MetaRocq.Erasure.EPrimitive]
string_compare_eq [abbreviation, in MetaRocq.Utils.bytestring]
string_compare [abbreviation, in MetaRocq.Utils.bytestring]
string_of_prim [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
string_of_term [definition, in MetaRocq.Erasure.EAstUtils]
string_of_def [definition, in MetaRocq.Erasure.EAstUtils]
String.append [definition, in MetaRocq.Utils.bytestring]
String.compare [definition, in MetaRocq.Utils.bytestring]
String.concat [definition, in MetaRocq.Utils.bytestring]
String.contains [definition, in MetaRocq.Utils.bytestring]
String.EmptyString [constructor, in MetaRocq.Utils.bytestring]
String.eqb [definition, in MetaRocq.Utils.bytestring]
String.eqb_compare [lemma, in MetaRocq.Utils.bytestring]
String.index [definition, in MetaRocq.Utils.bytestring]
String.length [definition, in MetaRocq.Utils.bytestring]
String.of_string [definition, in MetaRocq.Utils.bytestring]
String.parse [definition, in MetaRocq.Utils.bytestring]
String.prefix [definition, in MetaRocq.Utils.bytestring]
String.print [definition, in MetaRocq.Utils.bytestring]
String.print_parse_inv [lemma, in MetaRocq.Utils.bytestring]
String.rev [definition, in MetaRocq.Utils.bytestring]
String.String [constructor, in MetaRocq.Utils.bytestring]
String.substring [definition, in MetaRocq.Utils.bytestring]
String.t [inductive, in MetaRocq.Utils.bytestring]
String.to_string [definition, in MetaRocq.Utils.bytestring]
String.t_sind [definition, in MetaRocq.Utils.bytestring]
String.t_rec [definition, in MetaRocq.Utils.bytestring]
String.t_ind [definition, in MetaRocq.Utils.bytestring]
String.t_rect [definition, in MetaRocq.Utils.bytestring]
_ ++ _ (bs_scope) [notation, in MetaRocq.Utils.bytestring]
String2pos [library]
strip [definition, in MetaRocq.Erasure.ERemoveParams]
strip [section, in MetaRocq.Erasure.ERemoveParams]
strip_outer_cast [definition, in MetaRocq.Template.AstUtils]
strip_casts [definition, in MetaRocq.Template.AstUtils]
strip_casts_mkApps [lemma, in MetaRocq.Template.LiftSubst]
strip_casts_mkApps_tApp [lemma, in MetaRocq.Template.LiftSubst]
strip_casts_lift [lemma, in MetaRocq.Template.LiftSubst]
strip_casts_mkApps_wf [lemma, in MetaRocq.Template.TypingWf]
strip_casts_mkApp_wf [lemma, in MetaRocq.Template.TypingWf]
strip_casts_mkApps_napp_wf [lemma, in MetaRocq.Template.TypingWf]
strip_casts_decompose_app [lemma, in MetaRocq.Template.TypingWf]
strip_program_expanded [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_env_expanded [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_expanded_decl [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_expanded_irrel [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_expanded [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_program_wf [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_env_wf [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_env_eq [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_extends_env [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_extends' [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_decl_extends [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_extends [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_env' [definition, in MetaRocq.Erasure.ERemoveParams]
strip_decl_wf [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_wellformed_decl_irrel [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_wellformed_irrel [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_wellformed [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_declared_constructor [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_eval [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_mkApps_etaexp [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isLazyApp [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isPrimApp [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isConstructApp [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isFixApp [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isFix [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isApp [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isBox [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_isLambda [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_tApp [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_program [definition, in MetaRocq.Erasure.ERemoveParams]
strip_env [definition, in MetaRocq.Erasure.ERemoveParams]
strip_decl [definition, in MetaRocq.Erasure.ERemoveParams]
strip_inductive_decl [definition, in MetaRocq.Erasure.ERemoveParams]
strip_constant_decl [definition, in MetaRocq.Erasure.ERemoveParams]
strip_nth [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_cunfold_cofix [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_cunfold_fix [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_cofix_subst [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_fix_subst [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_iota_red [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_substl [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_csubst [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_mkApps [lemma, in MetaRocq.Erasure.ERemoveParams]
strip_mkApps_nonnil [lemma, in MetaRocq.Erasure.ERemoveParams]
strip.Def [section, in MetaRocq.Erasure.ERemoveParams]
strip.Σ [variable, in MetaRocq.Erasure.ERemoveParams]
StrongerInstances [module, in MetaRocq.Quotation.ToPCUIC.Init]
StrongerInstances [module, in MetaRocq.Quotation.ToTemplate.Init]
strong_nat_ind [lemma, in MetaRocq.Utils.MRArith]
strong_substitutivity [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
stuck_fix_value_args [lemma, in MetaRocq.Erasure.EWcbvEval]
stuck_fix_value_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
stuck_fix_value_args [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
stuck_fix_value_inv [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
sType [abbreviation, in MetaRocq.Common.Universes]
subgoal [definition, in MetaRocq.Examples.tauto]
subgraph_proper [instance, in MetaRocq.Common.uGraph]
subject_reduction_ctx [lemma, in MetaRocq.PCUIC.PCUICSR]
subject_reduction_closed [lemma, in MetaRocq.PCUIC.PCUICSR]
subject_reduction1_closed [lemma, in MetaRocq.PCUIC.PCUICSR]
subject_reduction [lemma, in MetaRocq.PCUIC.PCUICSR]
subject_reduction1 [lemma, in MetaRocq.PCUIC.PCUICSR]
subject_reduction_eval [lemma, in MetaRocq.PCUIC.PCUICClassification]
subject_is_open_term [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
subject_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
submodule_inclusion [inductive, in MetaRocq.Quotation.ToPCUIC.Init]
submodule_inclusion [inductive, in MetaRocq.Quotation.ToTemplate.Init]
subrelations_eq_compare_extends [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrelations_compare_extends [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrelations_leq_extends [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrelations_extends [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrelation_compare_sort_eq_prop [instance, in MetaRocq.PCUIC.PCUICCumulProp]
subrel_extends_eq_le [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_le [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_eq [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_eq_pb [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_cmp [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_extends_cmp_universe [instance, in MetaRocq.PCUIC.PCUICWeakeningEnv]
subrel_config_impl_eq_le [instance, in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_le [instance, in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_eq [instance, in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_eq_pb [instance, in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_config_impl_cmp [instance, in MetaRocq.PCUIC.PCUICWeakeningConfig]
subrel_lt_le [instance, in MetaRocq.Utils.MRArith]
subrel_eq_le [instance, in MetaRocq.Utils.MRArith]
subrel_R_True [instance, in MetaRocq.PCUIC.PCUICCumulProp]
subs [inductive, in MetaRocq.PCUIC.PCUICSubstitution]
Subsingleton [definition, in MetaRocq.PCUIC.PCUICElimination]
Subsingleton_extends [lemma, in MetaRocq.Erasure.ESubstitution]
Subsingleton_cofix [lemma, in MetaRocq.Erasure.EArities]
subslet [inductive, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_cstr_branch_context [lemma, in MetaRocq.Erasure.Prelim]
subslet_cofix_subst [lemma, in MetaRocq.Erasure.Prelim]
subslet_fix_subst [lemma, in MetaRocq.Erasure.Prelim]
subslet_well_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_usubst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_untyped_subslet [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_nth_error_lt [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_length [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_nth_error [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_def_tip [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_ass_tip [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_def [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_sind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_rec [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_ind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_rect [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subslet_open_terms [lemma, in MetaRocq.PCUIC.PCUICSpine]
subslet_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICSpine]
subslet_cumul [lemma, in MetaRocq.PCUIC.PCUICSpine]
subslet_skipn [lemma, in MetaRocq.PCUIC.PCUICSpine]
subslet_app [lemma, in MetaRocq.PCUIC.PCUICSpine]
subslet_eq_context_alpha_dom [lemma, in MetaRocq.PCUIC.PCUICSpine]
subslet_eq_context_alpha [lemma, in MetaRocq.PCUIC.PCUICSpine]
subslet_projs_smash [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subslet_projs [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subslet_cofix [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subslet_open [lemma, in MetaRocq.PCUIC.PCUICConversion]
subslet_inds [lemma, in MetaRocq.PCUIC.PCUICArities]
subslet_app_inv [lemma, in MetaRocq.PCUIC.PCUICArities]
subslet_app_closed [lemma, in MetaRocq.PCUIC.PCUICArities]
subslet_inds_gen [lemma, in MetaRocq.PCUIC.PCUICArities]
subslet_extended_subst [lemma, in MetaRocq.PCUIC.PCUICContexts]
subslet_lift [lemma, in MetaRocq.PCUIC.PCUICContexts]
subslet_smash_context [lemma, in MetaRocq.PCUIC.PCUICInductives]
subslet_extended_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst [definition, in MetaRocq.PCUIC.PCUICAst]
subst [definition, in MetaRocq.Template.Ast]
subst [definition, in MetaRocq.Erasure.ELiftSubst]
SubstIdentity [section, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
SubstIdentity [section, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstIdentity.cf [variable, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
SubstIdentity.cf [variable, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstInstanceClosed [section, in MetaRocq.Common.Universes]
SubstInstanceClosed.Hcl [variable, in MetaRocq.Common.Universes]
SubstInstanceClosed.u [variable, in MetaRocq.Common.Universes]
substitution [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
SubstitutionLemmas [section, in MetaRocq.PCUIC.PCUICSubstitution]
SubstitutionLemmas.cf [variable, in MetaRocq.PCUIC.PCUICSubstitution]
SubstitutionLemmas.wfΣ [variable, in MetaRocq.PCUIC.PCUICSubstitution]
SubstitutionLemmas.Σ [variable, in MetaRocq.PCUIC.PCUICSubstitution]
substitutionT [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
substitution_ws_cumul_pb_subst_conv [lemma, in MetaRocq.PCUIC.PCUICSR]
substitution_conv [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_cumul [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_wt_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_let [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_wf_local [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_prop [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_cumul_let [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_cumul0 [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_untyped_cumul [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_red [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_untyped_red [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_untyped_let_red [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_let_red [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_red1 [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_check_one_cofix [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_check_one_fix [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution_ws_cumul_pb_vdef [lemma, in MetaRocq.PCUIC.PCUICSpine]
substitution_ws_cumul_pb_vass [lemma, in MetaRocq.PCUIC.PCUICSpine]
substitution_subslet [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
substitution_ws_cumul_ctx_pb_subst_conv [lemma, in MetaRocq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb_subst_conv [lemma, in MetaRocq.PCUIC.PCUICConversion]
substitution_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
substitution_ws_cumul_ctx_pb_red_subst [lemma, in MetaRocq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
substitution_let_pred1 [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
substitution_untyped_cumul_prop_cumul [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
substitution_red_terms_conv_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
substitution_untyped_cumul_prop_equiv [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
substitution_cumul_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
substitution_untyped_cumul_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
substitution_wf_local_rel [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
substitution0 [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
substitution0_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
substitution0_let_pred1 [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
substitution0_pred1 [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
substitution1_untyped_cumul_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
substl [definition, in MetaRocq.Erasure.ECSubst]
substl [definition, in MetaRocq.Template.WcbvEval]
substl [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
substlet_typable [lemma, in MetaRocq.Erasure.ESubstitution]
substl_csubst_comm [lemma, in MetaRocq.Erasure.ECSubst]
substl_subst [lemma, in MetaRocq.Erasure.ECSubst]
substl_csubst_comm [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
substl_subst [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
substl_rel [lemma, in MetaRocq.Erasure.EReorderCstrs]
substl_closed [lemma, in MetaRocq.Erasure.EReorderCstrs]
substl_rel [lemma, in MetaRocq.Erasure.EInlineProjections]
substl_closed [lemma, in MetaRocq.Erasure.EInlineProjections]
substl_csubst_comm [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
substl_subst [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
substP [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
substP_shiftnP [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
substP_shiftnP_gen [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
substP_shiftnP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
SubstUnivPreserved [record, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstUnivPreserved [inductive, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstUnivPreserving [record, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstUnivPreserving [inductive, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
substu_pres_eq [instance, in MetaRocq.PCUIC.PCUICSN]
substu_True_eq_univ_prop [instance, in MetaRocq.PCUIC.PCUICCumulProp]
substu_f_True [instance, in MetaRocq.PCUIC.PCUICCumulProp]
subst_telescope_comm [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
subst_telescope_comm_rec [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
subst_telescope_cons [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
subst_context_subst_context [lemma, in MetaRocq.PCUIC.PCUICSR]
subst_instance_nlctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
subst_leq_term [lemma, in MetaRocq.PCUIC.PCUICEquality]
subst_eq_term [lemma, in MetaRocq.PCUIC.PCUICEquality]
subst_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_context' [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_comm [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_extended_subst_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_snoc0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_decl0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_subst_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_simpl' [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_simpl [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_decomp [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_empty_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_empty [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_gt [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_lt [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_rec [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_app' [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_inst_case_context_wf [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_compare_context [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_compare_decl [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_compare_term [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_skipn [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_fn_eq [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_decompose_prod_assum_rec [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_cstr_concl_head [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_destArity [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_fix_context [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_mutual_inductive_body [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subst_declared_constant [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_wf_local [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_is_constructor [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_unfold_cofix [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_unfold_fix [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_iota_red [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_predicate [abbreviation, in MetaRocq.PCUIC.PCUICSubstitution]
subst_length [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_decl_closed [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subst_closedn [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
subst_instance_closedu [lemma, in MetaRocq.Common.Universes]
subst_instance_univ_closedu [lemma, in MetaRocq.Common.Universes]
subst_instance_level_expr_closedu [lemma, in MetaRocq.Common.Universes]
subst_instance_level_closedu [lemma, in MetaRocq.Common.Universes]
subst_instance_instance [instance, in MetaRocq.Common.Universes]
subst_instance_to_family [lemma, in MetaRocq.Common.Universes]
subst_instance_sort [instance, in MetaRocq.Common.Universes]
subst_instance_universe [instance, in MetaRocq.Common.Universes]
subst_instance_level_expr [instance, in MetaRocq.Common.Universes]
subst_instance_cstrs [instance, in MetaRocq.Common.Universes]
subst_instance_cstr [instance, in MetaRocq.Common.Universes]
subst_instance_level [instance, in MetaRocq.Common.Universes]
subst_instance [projection, in MetaRocq.Common.Universes]
subst_instance [constructor, in MetaRocq.Common.Universes]
subst_context_subst_telescope [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_context_rev_subst_telescope [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_context_lift_context_comm [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_map_lift_lift_context [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_extended_lift [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_lift1 [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_subst_context [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_ext_list_ext_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_extended_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_context_lift_id [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_context_telescope [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_lift_lift [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_app_context_gen [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_telescope_subst_context [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_instance_rev [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_telescope_length [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_app_telescope [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_telescope_app [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_telescope_empty [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_sorts_local_ctx [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_type_local_ctx [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst_instance_mfix [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
subst_csubst_comm [lemma, in MetaRocq.Erasure.ECSubst]
subst_cstr_concl_head [lemma, in MetaRocq.Template.EtaExpand]
subst_context_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
subst_context_subst_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
subst_it_mkProd_or_LetIn [lemma, in MetaRocq.Template.LiftSubst]
subst_app_simpl [lemma, in MetaRocq.Template.LiftSubst]
subst_app_decomp [lemma, in MetaRocq.Template.LiftSubst]
subst_empty [lemma, in MetaRocq.Template.LiftSubst]
subst_mkApps [lemma, in MetaRocq.Template.LiftSubst]
subst_rel_eq [lemma, in MetaRocq.Template.LiftSubst]
subst_rel_gt [lemma, in MetaRocq.Template.LiftSubst]
subst_rel_lt [lemma, in MetaRocq.Template.LiftSubst]
subst_rec [abbreviation, in MetaRocq.Template.LiftSubst]
subst_instance_ind_type_id [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_ind_sort_id [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_prim_val_tag [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_prim_type [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_ws_cumul_ctx_pb_rel [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_let_expand_closed_ctx_lift [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_let_expand_lift [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_let_expand_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_inds_smash_params [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_context_expand_lets_k [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_instance_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_instance_expand_lets [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_conv_closed [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_context_subst_context_comm [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_context_subst_context [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_instance_variance_cstrs [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_instance_cstrs_add [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
subst_rel0_lift_id [lemma, in MetaRocq.PCUIC.PCUICConversion]
subst_instance_ws_cumul_ctx_pb_rel [lemma, in MetaRocq.PCUIC.PCUICConversion]
subst_instance_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
subst_instance_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
subst_context_app0 [lemma, in MetaRocq.PCUIC.PCUICConversion]
subst_instance_extended_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_closedu [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_cons [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_nil [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_instance_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_list [instance, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_isLambda [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
subst_instance_isFix [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
subst_instance_isRel [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
subst_instance_isConstruct [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
subst_telescope_subst_instance [lemma, in MetaRocq.PCUIC.PCUICArities]
subst_context_let_expand_length [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand_lift_id [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_lift_above [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand_tInd [definition, in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand_mkApps [definition, in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand_tProd [definition, in MetaRocq.PCUIC.PCUICContexts]
subst_context_let_expand [definition, in MetaRocq.PCUIC.PCUICContexts]
subst_let_expand [definition, in MetaRocq.PCUIC.PCUICContexts]
subst_context_smash_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_sorts_local_ctx [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_type_local_ctx [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_instance_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICContexts]
subst_shift_comm [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_context_decompo [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_context_map_subst_expand_lets_k [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_context_map_subst_expand_lets [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_extended_subst [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_context_lift_id [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_reli_lift_id [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_compose_r [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_idsn_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_ids_rel_ren [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_eq [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_shiftn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_app [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_inst' [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_inst [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_fn_subst_consn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_inst_aux [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_0s_shifts [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_0_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_compose_assoc [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_ids_ren [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_compose [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons' [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_ren [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_subst_consn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_0 [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_idsn_consn_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_ids_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_lt [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_lt_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_ge [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_app [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons_gen [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_gen_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_gen [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_proper_ext [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_tip [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn_nil [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_consn [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_ids [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_compose_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_compose [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons_proper [instance, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_cons [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_fn [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst_case_branch_context [lemma, in MetaRocq.Erasure.ESubstitution]
subst_instance_constr [instance, in MetaRocq.PCUIC.PCUICAst]
subst_csubst_comm [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
subst_instance_level_var_instance [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
subst_instance_level_lift [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
subst_skipn' [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
subst_lift_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_context_subst [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_let_expand_k_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_let_expand_k_mkApps [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_let_expand_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_let_expand_k_0 [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_let_expand_k [definition, in MetaRocq.PCUIC.PCUICInductives]
subst_context_lift_context_cancel [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_context_lift_context [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_context_extended_subst_expand [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_id [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_projs_inst [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_instance_projs [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_inds_concl_head [lemma, in MetaRocq.PCUIC.PCUICInductives]
subst_instance_closedu [lemma, in MetaRocq.Template.UnivSubst]
subst_instance_subst [lemma, in MetaRocq.Template.UnivSubst]
subst_instance_length [lemma, in MetaRocq.Template.UnivSubst]
subst_instance_it_mkProd_or_LetIn [lemma, in MetaRocq.Template.UnivSubst]
subst_instance_mkApps [lemma, in MetaRocq.Template.UnivSubst]
subst_instance_lift [lemma, in MetaRocq.Template.UnivSubst]
subst_instance_cons [lemma, in MetaRocq.Template.UnivSubst]
subst_instance_id [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_abstract_instance_id [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_abs [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_id_mdecl [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_check_one_cofix [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_check_one_fix [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_smash [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_app [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_app_rec [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_prod_assum [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_destArity [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_ws_cumul_pb [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate_set_preturn [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate_set_pparams [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_branches [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_branch [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_predicate [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_branch_type [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_expand_lets_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_expand_lets [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_to_extended_list [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_predicate_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_branch_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_inds [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_lift_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_subst_telescope [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_subst_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstr_args [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_mutual_inductive_body [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_inductive_body [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_constructor_body [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_app_ctx [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_app [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_extended_subst [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_super [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_make'_make [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_make [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstrs_union [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_monom_cstr [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstrs_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstr_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ0_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_two [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_nat [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_prod [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_def [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_equal_inst_global_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_equal_inst_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_universe_make [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_universe_make' [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_sort_val' [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_universe_val' [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_val' [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_valuation [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_sort_val [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_universe_val [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_val [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_val [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_dearg_case [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
subst_dearg_lambdas [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
subst_dearg_single [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
subst_it_mkLambda_or_LetIn [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
subst_context [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
subst_instance_empty [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
subst_global_uctx_invariants [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
subst_telescope_subst_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
subst_id [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
subst_context0_inst_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
subst_context_inst_context [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
subst_instance_constr [instance, in MetaRocq.Template.Ast]
subst_app_simpl [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_app_decomp [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_closed [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_empty [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_mkApps [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_rel_eq [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_rel_gt [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_rel_lt [lemma, in MetaRocq.Erasure.ELiftSubst]
subst_rec [abbreviation, in MetaRocq.Erasure.ELiftSubst]
subst_csubst_comm [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
subst0 [abbreviation, in MetaRocq.PCUIC.PCUICAst]
subst0 [abbreviation, in MetaRocq.Template.Ast]
subst0 [abbreviation, in MetaRocq.Erasure.ELiftSubst]
subst0_context [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst0_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSpine]
subst0_inst [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
subst1 [definition, in MetaRocq.PCUIC.PCUICAst]
subst1 [definition, in MetaRocq.Template.Ast]
subst1 [definition, in MetaRocq.Erasure.ELiftSubst]
subst1_mkApps [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
subst1_inst [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
subst1_mkApps [lemma, in MetaRocq.Template.LiftSubst]
subst1_mkApps [lemma, in MetaRocq.Erasure.ELiftSubst]
subst10 [abbreviation, in MetaRocq.PCUIC.PCUICAst]
subst10 [abbreviation, in MetaRocq.Template.Ast]
subst10 [abbreviation, in MetaRocq.Erasure.ELiftSubst]
subst10_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
subs_usubst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subs_nth_error [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subs_nth_error_lt [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subs_nth_error_ge [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subs_length [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
subs_sind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subs_rec [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subs_ind [definition, in MetaRocq.PCUIC.PCUICSubstitution]
subs_rect [definition, in MetaRocq.PCUIC.PCUICSubstitution]
sub_app_arg [constructor, in MetaRocq.Erasure.Typed.Erasure]
sub_prod_cod [constructor, in MetaRocq.Erasure.Typed.Erasure]
sub_prod_dom [constructor, in MetaRocq.Erasure.Typed.Erasure]
sub_context_set_empty [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
sub_context_set_empty [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
sub_context_set_trans [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sub_context_set [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Success [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
succs_proper [lemma, in MetaRocq.Common.uGraph]
succ_inj [lemma, in MetaRocq.Common.Universes]
sum_deriv_lengths [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
sunny [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
sunny_annotate [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
sunny_subset [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
sup_idem [lemma, in MetaRocq.Common.Universes]
sup_comm [lemma, in MetaRocq.Common.Universes]
sup_subst_instance_univ [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sup_subst_instance_univ0 [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sup0_comm [lemma, in MetaRocq.Common.Universes]
swap [definition, in MetaRocq.Utils.MRProd]
Swf_fix [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
switch_off_box [definition, in MetaRocq.Erasure.EImplementBox]
switch_minus [lemma, in MetaRocq.Common.Universes]
switch_cstr_as_blocks [definition, in MetaRocq.Erasure.EConstructorsAsBlocks]
switch_constructor_as_block [definition, in MetaRocq.Erasure.EConstructorsAsBlocks]
switch_unguarded_fix [definition, in MetaRocq.Erasure.EWcbvEval]
switch_env_flags_to_named [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
switch_term_flags_to_named [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
switch_no_params [definition, in MetaRocq.Erasure.EInlineProjections]
switch_no_params [definition, in MetaRocq.Erasure.ERemoveParams]
sym_eq_univ_prop [instance, in MetaRocq.PCUIC.PCUICCumulProp]
| 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) |