| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75519 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (245 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61331 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6913 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (269 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (443 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (296 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |
S
S [module, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]S [module, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
S [module, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
S [constructor, in MetaCoq.Examples.demo]
SafeTemplateChecker [library]
safe_nth [definition, in MetaCoq.Template.utils.MCList]
same_lookup_ind_decl [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_typing_result [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_ind_comp [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_sort_comp [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod_comp [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_typing_result_comp [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_hnf [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_reduce_stack [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod_last [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_prod [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
same_principal_type [definition, in MetaCoq.Erasure.ErasureFunction]
sandwich [lemma, in MetaCoq.PCUIC.PCUICConfluence]
satisfies [definition, in MetaCoq.Template.Universes]
satisfies_subset [lemma, in MetaCoq.Template.Universes]
satisfies_union [lemma, in MetaCoq.Template.Universes]
satisfies_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies_subst_instance_ctr [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies_subsets [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies_equal_sets [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
satisfies0 [inductive, in MetaCoq.Template.Universes]
satisfies0_Eq [constructor, in MetaCoq.Template.Universes]
satisfies0_Lt [constructor, in MetaCoq.Template.Universes]
satisfies0_subst_instance_ctr [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
scons [constructor, in MetaCoq.Examples.demo]
scrut_ty:127 [binder, in MetaCoq.PCUIC.PCUICInversion]
sc:793 [binder, in MetaCoq.PCUIC.PCUICConfluence]
SE [module, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
SE [module, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
sec [section, in MetaCoq.Erasure.EGenericMapEnv]
Sect [definition, in MetaCoq.Translations.MiniHoTT]
Sect [definition, in MetaCoq.Translations.MiniHoTT_paths]
sec.axioms_efl [variable, in MetaCoq.Erasure.EGenericMapEnv]
sec.cstrs_efl [variable, in MetaCoq.Erasure.EGenericMapEnv]
sec.efl [variable, in MetaCoq.Erasure.EGenericMapEnv]
sec.efl' [variable, in MetaCoq.Erasure.EGenericMapEnv]
sec.gen_transform_wellformed [variable, in MetaCoq.Erasure.EGenericMapEnv]
sec.gen_transform [variable, in MetaCoq.Erasure.EGenericMapEnv]
sec.Pre [variable, in MetaCoq.Erasure.EGenericMapEnv]
sec.wellformed_gen_transform_extends [variable, in MetaCoq.Erasure.EGenericMapEnv]
sem [definition, in MetaCoq.Examples.tauto]
semGen [definition, in MetaCoq.Examples.tauto]
sep:14 [binder, in MetaCoq.Template.utils.MCString]
sep:141 [binder, in MetaCoq.Template.utils.bytestring]
sep:152 [binder, in MetaCoq.Template.utils.bytestring]
sep:154 [binder, in MetaCoq.Template.utils.bytestring]
sep:3 [binder, in MetaCoq.Template.utils.MCString]
sep:66 [binder, in MetaCoq.Template.utils.bytestring]
SEq [module, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
seq [record, in MetaCoq.Examples.tauto]
SEq [module, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
seq_size [definition, in MetaCoq.Examples.tauto]
set_pparams_two [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
set_pparams [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
set_preturn_two [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
set_preturn [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
set_pcontext_two [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
set_pcontext [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
set_preturn_two [definition, in MetaCoq.PCUIC.PCUICConversion]
set_puinst [definition, in MetaCoq.PCUIC.PCUICConversion]
se:432 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:495 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:532 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:544 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:546 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:639 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Sfst_decompose_app_rec [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
sg:100 [binder, in MetaCoq.Examples.tauto]
sg:49 [binder, in MetaCoq.Examples.tauto]
sg:94 [binder, in MetaCoq.Examples.tauto]
sg:97 [binder, in MetaCoq.Examples.tauto]
shift [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftf [abbreviation, in MetaCoq.Template.Ast]
shiftf [definition, in MetaCoq.PCUIC.PCUICAst]
shiftf0 [lemma, in MetaCoq.PCUIC.PCUICAst]
shiftk [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_shift [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
shiftk_unfold [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_compose [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_shift_l [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftk_0 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftnP [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnPF_closedPT [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
shiftnPS [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnPSS [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_shiftn [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
shiftnP_predU [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_substP [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_strengthenP [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_xpredT [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_closedP [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_S [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_shiftn [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_add [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_ext [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnP_mon [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
shiftnP_up [lemma, in MetaCoq.PCUIC.PCUICConvCumInversion]
shiftnP0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
shiftnS [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_Upn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_ren_id [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_compose [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_lift_renaming [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_1_S [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_rshiftk [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_add [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_id [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_ext [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn_ext_cond [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
shiftn_renaming_eq [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shiftn_renaming [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shiftn0 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn0:133 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shiftn1_renaming [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shift_subst_consn_ge [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift_subst_instance [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift_Up_comm [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift_typing [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
shift_renaming [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
shift_subst_consn_tip [lemma, in MetaCoq.PCUIC.PCUICSpine]
shift':152 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift':51 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift':62 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:125 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:137 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:151 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:164 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:178 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:19 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:50 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:61 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:68 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:74 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:81 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:84 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:9 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
short:102 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
short:106 [binder, in MetaCoq.Template.Pretty]
short:112 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
short:113 [binder, in MetaCoq.Template.Pretty]
short:115 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
short:121 [binder, in MetaCoq.Template.Pretty]
short:127 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
short:129 [binder, in MetaCoq.Template.Pretty]
short:130 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
short:134 [binder, in MetaCoq.Template.Pretty]
short:144 [binder, in MetaCoq.Template.Pretty]
short:148 [binder, in MetaCoq.Template.Pretty]
short:153 [binder, in MetaCoq.Template.Pretty]
short:156 [binder, in MetaCoq.Template.Pretty]
short:160 [binder, in MetaCoq.Template.Pretty]
short:163 [binder, in MetaCoq.Template.Pretty]
short:98 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
sigma [record, in MetaCoq.Translations.sigma]
Sigma [section, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
sigma [library]
sigmaarg [abbreviation, in MetaCoq.SafeChecker.PCUICSafeReduce]
sigT [record, in MetaCoq.Translations.MiniHoTT]
sigT [record, in MetaCoq.Translations.MiniHoTT_paths]
sigT_ind [definition, in MetaCoq.Translations.MiniHoTT_paths]
simpl_type_Case [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
simpl_pred [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
simpl_subst_k [lemma, in MetaCoq.Erasure.ELiftSubst]
simpl_subst [lemma, in MetaCoq.Erasure.ELiftSubst]
simpl_subst_rec [lemma, in MetaCoq.Erasure.ELiftSubst]
simpl_lift0 [lemma, in MetaCoq.Erasure.ELiftSubst]
simpl_lift [lemma, in MetaCoq.Erasure.ELiftSubst]
simpl_map_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst' [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_k [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_rec [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift_ext [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
simpl_subst_k [lemma, in MetaCoq.Template.LiftSubst]
simpl_subst [lemma, in MetaCoq.Template.LiftSubst]
simpl_subst_rec [lemma, in MetaCoq.Template.LiftSubst]
simpl_lift0 [lemma, in MetaCoq.Template.LiftSubst]
simpl_lift [lemma, in MetaCoq.Template.LiftSubst]
SingletonProp [definition, in MetaCoq.PCUIC.PCUICElimination]
singleton_elim [definition, in MetaCoq.Examples.metacoq_tour]
singleton:92 [binder, in MetaCoq.Template.common.uGraph]
SisFixApp_mkApps [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
six [definition, in MetaCoq.Examples.demo]
size [definition, in MetaCoq.Erasure.EInduction]
size [definition, in MetaCoq.Template.utils.All_Forall]
size [definition, in MetaCoq.Examples.tauto]
size [definition, in MetaCoq.PCUIC.utils.PCUICSize]
sizeA:557 [binder, in MetaCoq.Template.utils.MCList]
sizeB:559 [binder, in MetaCoq.Template.utils.MCList]
size_mkApps_l [lemma, in MetaCoq.Erasure.EInduction]
size_mkApps_f [lemma, in MetaCoq.Erasure.EInduction]
size_mkApps [lemma, in MetaCoq.Erasure.EInduction]
size_wf_local_app [lemma, in MetaCoq.PCUIC.PCUICTyping]
size_mkApps [lemma, in MetaCoq.PCUIC.utils.PCUICSize]
size_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
size_decompose_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
size_decompose_app_rec [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
size_final [lemma, in MetaCoq.Erasure.EWcbvEval]
size:1 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
size:11 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
size:127 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
size:132 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
size:145 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
size:156 [binder, in MetaCoq.Examples.tauto]
size:158 [binder, in MetaCoq.Examples.tauto]
size:160 [binder, in MetaCoq.Examples.tauto]
size:162 [binder, in MetaCoq.Examples.tauto]
size:164 [binder, in MetaCoq.Examples.tauto]
size:166 [binder, in MetaCoq.Examples.tauto]
size:3 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
size:5 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
size:548 [binder, in MetaCoq.Template.utils.MCList]
size:588 [binder, in MetaCoq.Template.utils.MCList]
size:7 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
size:9 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
size:901 [binder, in MetaCoq.Template.utils.MCList]
skipn_all_app_eq [lemma, in MetaCoq.Template.utils.MCList]
skipn_nth_error [lemma, in MetaCoq.Template.utils.MCList]
skipn_skipn [lemma, in MetaCoq.Template.utils.MCList]
skipn_eq_cons [lemma, in MetaCoq.Template.utils.MCList]
skipn_firstn_skipn [lemma, in MetaCoq.Template.utils.MCList]
skipn_map_length [lemma, in MetaCoq.Template.utils.MCList]
skipn_mapi_rec [lemma, in MetaCoq.Template.utils.MCList]
skipn_app_le [lemma, in MetaCoq.Template.utils.MCList]
skipn_all [lemma, in MetaCoq.Template.utils.MCList]
skipn_n_Sn [lemma, in MetaCoq.Template.utils.MCList]
skipn_0_eq [lemma, in MetaCoq.Template.utils.MCList]
skipn_0 [lemma, in MetaCoq.Template.utils.MCList]
skipn_all_app [lemma, in MetaCoq.Template.utils.MCList]
skipn_all2 [lemma, in MetaCoq.Template.utils.MCList]
skipn_length [lemma, in MetaCoq.Template.utils.MCList]
skipn_S [lemma, in MetaCoq.Template.utils.MCList]
skipn_nil [lemma, in MetaCoq.Template.utils.MCList]
skipn_ge [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
skipn_expand_lets_ctx [lemma, in MetaCoq.PCUIC.PCUICInductives]
skipn_subst_instance [lemma, in MetaCoq.PCUIC.PCUICInductives]
skipn_lift_context [lemma, in MetaCoq.PCUIC.PCUICInductives]
skipn_projs [lemma, in MetaCoq.PCUIC.PCUICInductives]
skipn_subst [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
skipn_map_length [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
skipn_nil_length [lemma, in MetaCoq.PCUIC.PCUICSR]
skipn_subst_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
SL [module, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
SL [module, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
SL [module, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
SL [module, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
sl:50 [binder, in MetaCoq.Examples.tauto]
sl:51 [binder, in MetaCoq.Examples.tauto]
smaller:169 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
smash_context_app_expand_acc [lemma, in MetaCoq.PCUIC.PCUICInductives]
smash_context_acc [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
smash_context_lift [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
smash_context_app_ass [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
smash_context_app_def [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
smash_context_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
smash_context_subst_context_let_expand [lemma, in MetaCoq.PCUIC.PCUICSR]
smash_telescope [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
smash_context_app_expand [lemma, in MetaCoq.PCUIC.PCUICContexts]
smash_context_idempotent [lemma, in MetaCoq.PCUIC.PCUICContexts]
smash_assumption_context [lemma, in MetaCoq.PCUIC.PCUICContexts]
smash_context_assumption_context [lemma, in MetaCoq.PCUIC.PCUICContexts]
smash_context_subst_empty [lemma, in MetaCoq.PCUIC.PCUICContexts]
smash_assumption_context [lemma, in MetaCoq.Erasure.Prelim]
snd_eq [definition, in MetaCoq.Template.utils.MCProd]
snd_on_snd [lemma, in MetaCoq.Template.utils.MCProd]
snd' [projection, in MetaCoq.Examples.demo]
snoc [definition, in MetaCoq.Template.BasicAst]
snoc [definition, in MetaCoq.Erasure.EAst]
snoc_app_context [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
soft:42 [binder, in MetaCoq.PCUIC.utils.PCUICPrimitive]
solve_discr_args [lemma, in MetaCoq.Erasure.EEtaExpanded]
some_inj [lemma, in MetaCoq.Template.utils.MCOption]
Sort [constructor, in MetaCoq.Template.BasicAst]
sorting_size:404 [binder, in MetaCoq.Template.EnvironmentTyping]
sorting:201 [binder, in MetaCoq.Template.EnvironmentTyping]
sorting:212 [binder, in MetaCoq.Template.EnvironmentTyping]
sorting:252 [binder, in MetaCoq.Template.EnvironmentTyping]
sorting:289 [binder, in MetaCoq.Template.EnvironmentTyping]
sorting:361 [binder, in MetaCoq.Template.EnvironmentTyping]
sorting:394 [binder, in MetaCoq.Template.EnvironmentTyping]
sorts_local_ctx_All_local_assum_impl [lemma, in MetaCoq.PCUIC.PCUICElimination]
sorts_local_ctx_Pclosed [lemma, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
sorts_local_ctx_All_local_env [lemma, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
sorts_local_ctx_wf_sorts [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
sorts_local_ctx_instantiate [lemma, in MetaCoq.PCUIC.PCUICContexts]
sorts_local_ctx_wf_local [lemma, in MetaCoq.PCUIC.PCUICContexts]
sorts:147 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
sort_cons [constructor, in MetaCoq.PCUIC.Bidirectional.BDTyping]
sort_of_product_twice [lemma, in MetaCoq.Template.Universes]
sort_of_product_idem [lemma, in MetaCoq.Template.Universes]
sort_of_type_irrel [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
sort_typing_spine [lemma, in MetaCoq.Erasure.EArities]
sort_of_products [definition, in MetaCoq.PCUIC.PCUICArities]
sort_of_type [definition, in MetaCoq.SafeChecker.PCUICSafeRetyping]
source_edge_of_level [lemma, in MetaCoq.Template.common.uGraph]
spcons [abbreviation, in MetaCoq.PCUIC.PCUICSpine]
spec_map_succ [lemma, in MetaCoq.Template.Universes]
spine [definition, in MetaCoq.Erasure.EAstUtils]
Spines [section, in MetaCoq.PCUIC.PCUICCanonicity]
spine_subst_wt [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
spine_subst_expand_lets [lemma, in MetaCoq.PCUIC.PCUICInductives]
spine_subst_smash_inv [lemma, in MetaCoq.PCUIC.PCUICInductives]
spine_subst_smash_inv [lemma, in MetaCoq.SafeChecker.PCUICSafeRetyping]
spine_subst_wt [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
spine_subst_wt_terms [lemma, in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst_term_k [lemma, in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst_k [lemma, in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst_term [lemma, in MetaCoq.PCUIC.PCUICSR]
spine_subst_inst_subst [lemma, in MetaCoq.PCUIC.PCUICSR]
spine_nApp [lemma, in MetaCoq.Erasure.EAstUtils]
spine_tApp [lemma, in MetaCoq.Erasure.EAstUtils]
spine_mkApps [lemma, in MetaCoq.Erasure.EAstUtils]
spine_subst_app [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_extended_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_cumul [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_smash [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_ctx_inst_sub [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst_to_extended_list_k_gen [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_ctx_inst [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_is_closed_context_codom [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_is_closed_context [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_weakening [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_inst [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_smash_app_inv [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_app_inv [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_weaken [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst_first [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_conv [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_inj_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_eq [lemma, in MetaCoq.PCUIC.PCUICSpine]
spine_codom_wf [projection, in MetaCoq.PCUIC.PCUICSpine]
spine_dom_wf [projection, in MetaCoq.PCUIC.PCUICSpine]
spine_subst [record, in MetaCoq.PCUIC.PCUICSpine]
spine_subst_smash_inv [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
SplitPrefix [section, in MetaCoq.Template.utils.MCList]
Simp (ssripat_scope) [notation, in MetaCoq.Template.utils.MCList]
SplitSuffix [section, in MetaCoq.Template.utils.MCList]
split_suffix_maximal [lemma, in MetaCoq.Template.utils.MCList]
split_suffix_is_suffix [lemma, in MetaCoq.Template.utils.MCList]
split_suffix [definition, in MetaCoq.Template.utils.MCList]
split_prefix_maximal [lemma, in MetaCoq.Template.utils.MCList]
split_prefix_is_prefix [lemma, in MetaCoq.Template.utils.MCList]
split_prefix [definition, in MetaCoq.Template.utils.MCList]
split_at_firstn_skipn [lemma, in MetaCoq.Template.utils.MCList]
split_at_aux_firstn_skipn [lemma, in MetaCoq.Template.utils.MCList]
split_at [definition, in MetaCoq.Template.utils.MCList]
split_at_aux [definition, in MetaCoq.Template.utils.MCList]
split_app3 [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
split_closed_context [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
split_nth [lemma, in MetaCoq.PCUIC.PCUICReduction]
spnil [abbreviation, in MetaCoq.PCUIC.PCUICSpine]
sproperty:261 [binder, in MetaCoq.Template.EnvironmentTyping]
sproperty:295 [binder, in MetaCoq.Template.EnvironmentTyping]
sprop_sort_eq [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
sp':595 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sP:24 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
sP:30 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
sP:51 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
sp:562 [binder, in MetaCoq.PCUIC.PCUICSpine]
sp:578 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sP:59 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
sp:593 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sp:617 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sp:625 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
squash [record, in MetaCoq.Template.utils.MCSquash]
squash_isType_welltyped [lemma, in MetaCoq.SafeChecker.PCUICSafeRetyping]
sq_ws_cumul_pb [definition, in MetaCoq.PCUIC.PCUICConversion]
sq_wf_local_app [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
sq_wfl_nil [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
SRContext [section, in MetaCoq.PCUIC.PCUICSR]
_ ⊢ _ ⇝1 _ (pcuic) [notation, in MetaCoq.PCUIC.PCUICSR]
sr_stmt [definition, in MetaCoq.PCUIC.PCUICSR]
sr_red1 [lemma, in MetaCoq.PCUIC.PCUICSR]
SR_red1 [definition, in MetaCoq.PCUIC.PCUICSR]
SS [constructor, in MetaCoq.Examples.demo]
ssize:370 [binder, in MetaCoq.Template.EnvironmentTyping]
ss':352 [binder, in MetaCoq.Template.utils.wGraph]
ST [module, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ST [module, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ST [module, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
st [projection, in MetaCoq.SafeChecker.PCUICSafeConversion]
ST [module, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
stack [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
StackHeadError [constructor, in MetaCoq.SafeChecker.PCUICErrors]
StackMismatch [constructor, in MetaCoq.SafeChecker.PCUICErrors]
Stacks [section, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Stacks [section, in MetaCoq.PCUIC.PCUICReduction]
StackTailError [constructor, in MetaCoq.SafeChecker.PCUICErrors]
stack_context_decompose [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
stack_context_stack_cat [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_stack_cat [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_cat_appstack [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_appstack [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_pos [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_valid [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_atpos [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position_cons [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_position [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_entry_choice [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_context_appstack [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_context [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_entry_context [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_entry [inductive, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack_entry_context_mFix_mfix_bd [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
stack:435 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack:98 [binder, in MetaCoq.Template.Checker]
standard_model [library]
start:480 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
start:49 [binder, in MetaCoq.Template.utils.bytestring]
state [inductive, in MetaCoq.SafeChecker.PCUICSafeConversion]
stateR [inductive, in MetaCoq.SafeChecker.PCUICSafeConversion]
stateR_Acc [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
stateR_Args_Fallback [constructor, in MetaCoq.SafeChecker.PCUICSafeConversion]
stateR_Fallback_Term [constructor, in MetaCoq.SafeChecker.PCUICSafeConversion]
stateR_Args_Term [constructor, in MetaCoq.SafeChecker.PCUICSafeConversion]
stateR_Term_Reduction [constructor, in MetaCoq.SafeChecker.PCUICSafeConversion]
step_sound [lemma, in MetaCoq.Examples.tauto]
stk1 [projection, in MetaCoq.SafeChecker.PCUICSafeConversion]
stk2 [projection, in MetaCoq.SafeChecker.PCUICSafeConversion]
streamn [inductive, in MetaCoq.Examples.demo]
strengthening [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
strengthenP [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
strengthenP_addn [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
strengthenP_proper [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
string [abbreviation, in MetaCoq.Template.utils.bytestring]
String [module, in MetaCoq.Template.utils.bytestring]
string [abbreviation, in MetaCoq.Template.utils.MCString]
StringOT [module, in MetaCoq.Template.utils.bytestring]
StringOT.compare [definition, in MetaCoq.Template.utils.bytestring]
StringOT.compare_trans [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.compare_sym [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.compare_lt [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.compare_refl [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.compare_eq [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.compare_spec [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.eq [definition, in MetaCoq.Template.utils.bytestring]
StringOT.eq_leibniz [definition, in MetaCoq.Template.utils.bytestring]
StringOT.eq_dec [definition, in MetaCoq.Template.utils.bytestring]
StringOT.eq_trans [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.eq_sym [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.eq_refl [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.eq_equiv [definition, in MetaCoq.Template.utils.bytestring]
StringOT.lt [definition, in MetaCoq.Template.utils.bytestring]
StringOT.lt_compat [definition, in MetaCoq.Template.utils.bytestring]
StringOT.lt_strorder [instance, in MetaCoq.Template.utils.bytestring]
StringOT.lt_irreflexive [definition, in MetaCoq.Template.utils.bytestring]
StringOT.lt_transitive [instance, in MetaCoq.Template.utils.bytestring]
StringOT.lt_not_eq [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.lt_trans [lemma, in MetaCoq.Template.utils.bytestring]
StringOT.reflect_eq_string [instance, in MetaCoq.Template.utils.bytestring]
StringOT.t [definition, in MetaCoq.Template.utils.bytestring]
string_of_universe_instance [definition, in MetaCoq.Template.Universes]
string_of_sort [definition, in MetaCoq.Template.Universes]
string_of_level_expr [definition, in MetaCoq.Template.Universes]
string_of_level [definition, in MetaCoq.Template.Universes]
string_of_float64_model [definition, in MetaCoq.Template.BasicAst]
string_of_uint63_model [definition, in MetaCoq.Template.BasicAst]
string_of_def [definition, in MetaCoq.Template.BasicAst]
string_of_case_info [definition, in MetaCoq.Template.BasicAst]
string_of_relevance [definition, in MetaCoq.Template.BasicAst]
string_of_name [definition, in MetaCoq.Template.BasicAst]
string_of_term [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
string_of_aname [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
string_compare_eq [abbreviation, in MetaCoq.Template.utils.bytestring]
string_compare [abbreviation, in MetaCoq.Template.utils.bytestring]
string_of_branch [definition, in MetaCoq.Template.Ast]
string_of_predicate [definition, in MetaCoq.Template.Ast]
string_of_Z [definition, in MetaCoq.Template.utils.MCString]
string_of_positive [definition, in MetaCoq.Template.utils.MCString]
string_of_nat [definition, in MetaCoq.Template.utils.MCString]
string_of_uint [definition, in MetaCoq.Template.utils.MCString]
string_of_list [definition, in MetaCoq.Template.utils.MCString]
string_of_list_aux [definition, in MetaCoq.Template.utils.MCString]
string_of_gref [definition, in MetaCoq.Template.Kernames]
string_of_inductive [definition, in MetaCoq.Template.Kernames]
string_of_kername [definition, in MetaCoq.Template.Kernames]
string_of_modpath [definition, in MetaCoq.Template.Kernames]
string_of_dirpath [definition, in MetaCoq.Template.Kernames]
string_repeat_length [lemma, in MetaCoq.SafeChecker.PCUICConsistency]
string_repeat [definition, in MetaCoq.SafeChecker.PCUICConsistency]
string_of_type_error [definition, in MetaCoq.SafeChecker.PCUICErrors]
string_of_conv_error [definition, in MetaCoq.SafeChecker.PCUICErrors]
string_of_conv_pb [definition, in MetaCoq.SafeChecker.PCUICErrors]
string_of_Z [definition, in MetaCoq.SafeChecker.PCUICErrors]
string_of_predicate [definition, in MetaCoq.PCUIC.PCUICAst]
string_of_branch [definition, in MetaCoq.PCUIC.PCUICAst]
string_of_type_error [definition, in MetaCoq.Template.Checker]
string_compare_irrel [lemma, in MetaCoq.Template.Reflect]
string_of_term [definition, in MetaCoq.Erasure.EAstUtils]
string_of_def [definition, in MetaCoq.Erasure.EAstUtils]
string_of_prim [definition, in MetaCoq.PCUIC.utils.PCUICPrimitive]
string_of_float64_model [definition, in MetaCoq.PCUIC.utils.PCUICPrimitive]
string_eqdec [instance, in MetaCoq.Template.utils.MCPrelude]
string_of_term [definition, in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_term [definition, in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_def [definition, in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_branch [definition, in MetaCoq.Template.AstUtils]
string_of_term_tree.string_of_predicate [definition, in MetaCoq.Template.AstUtils]
_ ^ _ [notation, in MetaCoq.Template.AstUtils]
string_of_term_tree [module, in MetaCoq.Template.AstUtils]
string_of_float [definition, in MetaCoq.Template.AstUtils]
string_of_prim_int [definition, in MetaCoq.Template.AstUtils]
String.append [definition, in MetaCoq.Template.utils.bytestring]
String.compare [definition, in MetaCoq.Template.utils.bytestring]
String.concat [definition, in MetaCoq.Template.utils.bytestring]
String.contains [definition, in MetaCoq.Template.utils.bytestring]
String.EmptyString [constructor, in MetaCoq.Template.utils.bytestring]
String.eqb [definition, in MetaCoq.Template.utils.bytestring]
String.eqb_compare [lemma, in MetaCoq.Template.utils.bytestring]
String.index [definition, in MetaCoq.Template.utils.bytestring]
String.length [definition, in MetaCoq.Template.utils.bytestring]
String.of_string [definition, in MetaCoq.Template.utils.bytestring]
String.parse [definition, in MetaCoq.Template.utils.bytestring]
String.prefix [definition, in MetaCoq.Template.utils.bytestring]
String.print [definition, in MetaCoq.Template.utils.bytestring]
String.print_parse_inv [lemma, in MetaCoq.Template.utils.bytestring]
String.rev [definition, in MetaCoq.Template.utils.bytestring]
String.String [constructor, in MetaCoq.Template.utils.bytestring]
String.substring [definition, in MetaCoq.Template.utils.bytestring]
String.t [inductive, in MetaCoq.Template.utils.bytestring]
String.to_string [definition, in MetaCoq.Template.utils.bytestring]
_ ++ _ (bs_scope) [notation, in MetaCoq.Template.utils.bytestring]
strip [definition, in MetaCoq.Erasure.ERemoveParams]
strip [section, in MetaCoq.Erasure.ERemoveParams]
strip_program_expanded [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_env_expanded [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_expanded_decl [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_expanded_irrel [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_expanded [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_program_wf [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_env_wf [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_env_eq [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_extends' [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_decl_extends [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_extends [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_env' [definition, in MetaCoq.Erasure.ERemoveParams]
strip_decl_wf [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_wellformed_decl_irrel [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_wellformed_irrel [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_wellformed [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_declared_constructor [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_eval [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_mkApps_etaexp [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_isConstructApp [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_isFixApp [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_isFix [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_isApp [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_isBox [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_isLambda [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_tApp [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_program [definition, in MetaCoq.Erasure.ERemoveParams]
strip_env [definition, in MetaCoq.Erasure.ERemoveParams]
strip_decl [definition, in MetaCoq.Erasure.ERemoveParams]
strip_inductive_decl [definition, in MetaCoq.Erasure.ERemoveParams]
strip_constant_decl [definition, in MetaCoq.Erasure.ERemoveParams]
strip_nth [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_cunfold_cofix [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_cunfold_fix [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_cofix_subst [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_fix_subst [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_iota_red [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_substl [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_csubst [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_mkApps [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_mkApps_nonnil [lemma, in MetaCoq.Erasure.ERemoveParams]
strip_casts_mkApps_wf [lemma, in MetaCoq.Template.TypingWf]
strip_casts_mkApp_wf [lemma, in MetaCoq.Template.TypingWf]
strip_casts_mkApps_napp_wf [lemma, in MetaCoq.Template.TypingWf]
strip_casts_decompose_app [lemma, in MetaCoq.Template.TypingWf]
strip_casts_mkApps [lemma, in MetaCoq.Template.LiftSubst]
strip_casts_mkApps_tApp [lemma, in MetaCoq.Template.LiftSubst]
strip_casts_lift [lemma, in MetaCoq.Template.LiftSubst]
strip_outer_cast [definition, in MetaCoq.Template.AstUtils]
strip_casts [definition, in MetaCoq.Template.AstUtils]
strip.Def [section, in MetaCoq.Erasure.ERemoveParams]
strong_nat_ind [lemma, in MetaCoq.Template.utils.MCArith]
strong_substitutivity [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
stuck_fix_value_args [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
stuck_fix_value_inv [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
stuck_fix_value_args [lemma, in MetaCoq.Erasure.EWcbvEval]
stuck_fix_value_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
subgoal [definition, in MetaCoq.Examples.tauto]
subgraph_proper [instance, in MetaCoq.Template.common.uGraph]
subject_is_open_term [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
subject_closed [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
subject_reduction_eval [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
subject_reduction_ctx [lemma, in MetaCoq.PCUIC.PCUICSR]
subject_reduction_closed [lemma, in MetaCoq.PCUIC.PCUICSR]
subject_reduction1_closed [lemma, in MetaCoq.PCUIC.PCUICSR]
subject_reduction [lemma, in MetaCoq.PCUIC.PCUICSR]
subject_reduction1 [lemma, in MetaCoq.PCUIC.PCUICSR]
subrelations_eq_compare_extends [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelations_compare_extends [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelations_leq_extends [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelations_extends [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrelation_leq_universe_eq_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
subrelation_eq_universe_eq_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
subrel_extends_eq_le [instance, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrel_extends_le [instance, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrel_extends_eq [instance, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrel_extends_eq_pb [instance, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subrel_extends_cmp [instance, in MetaCoq.PCUIC.PCUICWeakeningEnv]
subs [inductive, in MetaCoq.PCUIC.PCUICSubstitution]
subslet [inductive, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_inds [lemma, in MetaCoq.PCUIC.PCUICArities]
subslet_app_inv [lemma, in MetaCoq.PCUIC.PCUICArities]
subslet_app_closed [lemma, in MetaCoq.PCUIC.PCUICArities]
subslet_inds_gen [lemma, in MetaCoq.PCUIC.PCUICArities]
subslet_well_subst [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_usubst [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_untyped_subslet [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_nth_error_lt [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_length [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_nth_error [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_def_tip [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_ass_tip [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_def [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subslet_smash_context [lemma, in MetaCoq.PCUIC.PCUICInductives]
subslet_extended_subst [lemma, in MetaCoq.PCUIC.PCUICInductives]
subslet_projs_smash [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subslet_projs [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subslet_cofix [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subslet_open [lemma, in MetaCoq.PCUIC.PCUICConversion]
subslet_extended_subst [lemma, in MetaCoq.PCUIC.PCUICContexts]
subslet_lift [lemma, in MetaCoq.PCUIC.PCUICContexts]
subslet_open_terms [lemma, in MetaCoq.PCUIC.PCUICSpine]
subslet_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICSpine]
subslet_cumul [lemma, in MetaCoq.PCUIC.PCUICSpine]
subslet_skipn [lemma, in MetaCoq.PCUIC.PCUICSpine]
subslet_app [lemma, in MetaCoq.PCUIC.PCUICSpine]
subslet_eq_context_alpha_dom [lemma, in MetaCoq.PCUIC.PCUICSpine]
subslet_eq_context_alpha [lemma, in MetaCoq.PCUIC.PCUICSpine]
subslet_cstr_branch_context [lemma, in MetaCoq.Erasure.Prelim]
subslet_cofix_subst [lemma, in MetaCoq.Erasure.Prelim]
subslet_fix_subst [lemma, in MetaCoq.Erasure.Prelim]
subst [definition, in MetaCoq.Template.Ast]
subst [definition, in MetaCoq.PCUIC.PCUICAst]
subst [definition, in MetaCoq.Erasure.ELiftSubst]
SubstIdentity [section, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
SubstIdentity [section, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstInstanceClosed [section, in MetaCoq.Template.Universes]
substitution [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
SubstitutionLemmas [section, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_conv [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_cumul [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_wt_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_let [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_wf_local [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_prop [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_cumul_let [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_cumul0 [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_untyped_cumul [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_red [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_untyped_red [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_untyped_let_red [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_let_red [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_red1 [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_check_one_cofix [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_check_one_fix [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution_subslet [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
substitution_untyped_cumul_prop_cumul [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
substitution_red_terms_conv_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
substitution_untyped_cumul_prop_equiv [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
substitution_cumul_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
substitution_untyped_cumul_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
substitution_let_pred1 [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
substitution_ws_cumul_ctx_pb_subst_conv [lemma, in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb_subst_conv [lemma, in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_ctx_pb_red_subst [lemma, in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
substitution_ws_cumul_pb_subst_conv [lemma, in MetaCoq.PCUIC.PCUICSR]
substitution_ws_cumul_pb_vdef [lemma, in MetaCoq.PCUIC.PCUICSpine]
substitution_ws_cumul_pb_vass [lemma, in MetaCoq.PCUIC.PCUICSpine]
substitution_wf_local_rel [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
substitution0 [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
substitution0_let_pred1 [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
substitution0_pred1 [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
substitution0_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
substitution1_untyped_cumul_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
substl [definition, in MetaCoq.PCUIC.PCUICWcbvEval]
substl [definition, in MetaCoq.Template.WcbvEval]
substl [definition, in MetaCoq.Erasure.ECSubst]
substlet_typable [lemma, in MetaCoq.Erasure.ESubstitution]
substl_rel [lemma, in MetaCoq.Erasure.EInlineProjections]
substl_closed [lemma, in MetaCoq.Erasure.EInlineProjections]
substl_csubst_comm [lemma, in MetaCoq.Erasure.ECSubst]
substl_subst [lemma, in MetaCoq.Erasure.ECSubst]
substl_csubst_comm [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
substl_subst [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
substP [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
substP_shiftnP [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
substP_shiftnP_gen [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
substP_shiftnP [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
SubstUnivPreserved [record, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstUnivPreserved [inductive, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstUnivPreserving [record, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
SubstUnivPreserving [inductive, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
substuniv_eq_univ_prop [instance, in MetaCoq.PCUIC.PCUICCumulProp]
substu_pres_eq [instance, in MetaCoq.PCUIC.PCUICSN]
subst_cstr_concl_head [lemma, in MetaCoq.Template.EtaExpand]
subst_case_branch_context [lemma, in MetaCoq.Erasure.ESubstitution]
subst_instance_closedu [lemma, in MetaCoq.Template.Universes]
subst_instance_univ_closedu [lemma, in MetaCoq.Template.Universes]
subst_instance_level_expr_closedu [lemma, in MetaCoq.Template.Universes]
subst_instance_level_closedu [lemma, in MetaCoq.Template.Universes]
subst_instance_instance [instance, in MetaCoq.Template.Universes]
subst_instance_univ [instance, in MetaCoq.Template.Universes]
subst_instance_univ0 [instance, in MetaCoq.Template.Universes]
subst_instance_level_expr [instance, in MetaCoq.Template.Universes]
subst_instance_cstrs [instance, in MetaCoq.Template.Universes]
subst_instance_cstr [instance, in MetaCoq.Template.Universes]
subst_instance_level [instance, in MetaCoq.Template.Universes]
subst_instance [projection, in MetaCoq.Template.Universes]
subst_instance [constructor, in MetaCoq.Template.Universes]
subst_app [definition, in MetaCoq.Translations.translation_utils]
subst_app [definition, in MetaCoq.Translations.times_bool_fun]
subst_telescope_subst_context [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
subst_telescope_subst_instance [lemma, in MetaCoq.PCUIC.PCUICArities]
subst_instance_empty [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
subst_context_app' [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_inst_case_context_wf [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_compare_context [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_compare_decl [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_compare_term [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_skipn [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_fn_eq [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_decompose_prod_assum_rec [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_cstr_concl_head [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_destArity [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_fix_context [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_mutual_inductive_body [definition, in MetaCoq.PCUIC.PCUICSubstitution]
subst_declared_constant [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_wf_local [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_is_constructor [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_unfold_cofix [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_unfold_fix [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_iota_red [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_predicate [abbreviation, in MetaCoq.PCUIC.PCUICSubstitution]
subst_length [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_decl_closed [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subst_instance_isLambda [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
subst_instance_isFix [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
subst_instance_isRel [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
subst_instance_isConstruct [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
subst_lift_subst [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_context_subst [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_k_lift [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_k_mkApps [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_k_0 [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_let_expand_k [definition, in MetaCoq.PCUIC.PCUICInductives]
subst_context_lift_context_cancel [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_context_lift_context [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_context_extended_subst_expand [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_id [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_projs_inst [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_instance_projs [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_inds_concl_head [lemma, in MetaCoq.PCUIC.PCUICInductives]
subst_instance_constr [instance, in MetaCoq.Template.Ast]
subst_let_expand_closed_ctx_lift [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_let_expand_lift [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_let_expand_app [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_inds_smash_params [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_context_expand_lets_k [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_expand_lets_ctx [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_expand_lets [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_conv_closed [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_context_subst_context_comm [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_context_subst_context [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_variance_cstrs [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_instance_cstrs_add [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
subst_skipn' [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
subst_leq_term [lemma, in MetaCoq.PCUIC.PCUICEquality]
subst_eq_term [lemma, in MetaCoq.PCUIC.PCUICEquality]
subst_shift_comm [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_decompo [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_map_subst_expand_lets_k [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_map_subst_expand_lets [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_extended_subst [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_lift_id [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_reli_lift_id [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_compose_r [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_idsn_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_ids_rel_ren [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_eq [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_shiftn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_app [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_inst' [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_inst [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_fn_subst_consn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_inst_aux [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_0s_shifts [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_0_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_compose_assoc [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_ids_ren [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_compose [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons' [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_ren [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_subst_consn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_0 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_idsn_consn_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_ids_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_lt_spec [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_ge [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_app [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons_gen [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_gen_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_gen [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_proper_ext [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_tip [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_subst_cons [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn_nil [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_consn [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_ids [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_compose_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_compose [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_cons [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_fn [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst_context_expand_lets_ctx [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
subst_context_subst_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
subst_instance_ind_type_id [lemma, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_ind_sort_id [lemma, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_ws_cumul_ctx_pb_rel [lemma, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
subst_instance_constr [instance, in MetaCoq.PCUIC.PCUICAst]
subst_id [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subst_context0_inst_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subst_context_inst_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subst_app_simpl [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_app_decomp [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_closed [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_empty [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_mkApps [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_rel_eq [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_rel_gt [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_rel_lt [lemma, in MetaCoq.Erasure.ELiftSubst]
subst_rec [abbreviation, in MetaCoq.Erasure.ELiftSubst]
subst_instance_extended_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_closedu [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_mkApps [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_cons [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_nil [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_instance_length [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_list [instance, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
subst_instance_nlctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
subst_instance_ws_cumul_ctx_pb_rel [lemma, in MetaCoq.PCUIC.PCUICConversion]
subst_instance_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
subst_instance_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
subst_context_app0 [lemma, in MetaCoq.PCUIC.PCUICConversion]
subst_closedn [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
subst_context_subst_context [lemma, in MetaCoq.PCUIC.PCUICSR]
subst_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_context' [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_comm [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_extended_subst_k [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_context_snoc0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_decl0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_subst_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_simpl' [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_simpl [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_app_decomp [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_empty_eq [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_empty [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_mkApps [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_eq [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_gt [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_rel_lt [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_rec [abbreviation, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst_telescope_comm [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
subst_telescope_comm_rec [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
subst_telescope_cons [lemma, in MetaCoq.PCUIC.PCUICContextSubst]
subst_instance_id [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_abstract_instance_id [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_abs [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_id_mdecl [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_check_one_cofix [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_check_one_fix [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_smash [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_app [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_app_rec [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_decompose_prod_assum [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_destArity [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_ws_cumul_pb [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate_set_preturn [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate_set_pparams [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_branches [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_branch [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_wf_predicate [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_branch_type [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_expand_lets_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_expand_lets [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_to_extended_list [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_predicate_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_case_branch_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_inds [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_lift_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_subst_telescope [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_subst_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstr_args [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_mutual_inductive_body [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_inductive_body [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_constructor_body [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_app_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_app [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_predicate [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_extended_subst [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_super [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_make'_make [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_make [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstrs_union [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_monom_cstr [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstrs_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_cstr_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_two_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ0_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_nat [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_prod [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_def [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_equal_inst_global_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_equal_inst_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_make [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_make' [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_val' [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ0_val' [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_val' [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_valuation [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ_val [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_univ0_val [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_expr_val [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_instance_level_val [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
subst_csubst_comm [lemma, in MetaCoq.Erasure.ECSubst]
subst_instance_closedu [lemma, in MetaCoq.Template.UnivSubst]
subst_instance_subst [lemma, in MetaCoq.Template.UnivSubst]
subst_instance_length [lemma, in MetaCoq.Template.UnivSubst]
subst_instance_it_mkProd_or_LetIn [lemma, in MetaCoq.Template.UnivSubst]
subst_instance_mkApps [lemma, in MetaCoq.Template.UnivSubst]
subst_instance_lift [lemma, in MetaCoq.Template.UnivSubst]
subst_instance_cons [lemma, in MetaCoq.Template.UnivSubst]
subst_instance_level_var_instance [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
subst_instance_level_lift [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
subst_context_let_expand_length [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_lift_id [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_lift_above [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_tInd [definition, in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_mkApps [definition, in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand_tProd [definition, in MetaCoq.PCUIC.PCUICContexts]
subst_context_let_expand [definition, in MetaCoq.PCUIC.PCUICContexts]
subst_let_expand [definition, in MetaCoq.PCUIC.PCUICContexts]
subst_context_smash_context [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_sorts_local_ctx [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_type_local_ctx [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_instance_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICContexts]
subst_csubst_comm [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
subst_it_mkProd_or_LetIn [lemma, in MetaCoq.Template.LiftSubst]
subst_app_simpl [lemma, in MetaCoq.Template.LiftSubst]
subst_app_decomp [lemma, in MetaCoq.Template.LiftSubst]
subst_empty [lemma, in MetaCoq.Template.LiftSubst]
subst_mkApps [lemma, in MetaCoq.Template.LiftSubst]
subst_rel_eq [lemma, in MetaCoq.Template.LiftSubst]
subst_rel_gt [lemma, in MetaCoq.Template.LiftSubst]
subst_rel_lt [lemma, in MetaCoq.Template.LiftSubst]
subst_rec [abbreviation, in MetaCoq.Template.LiftSubst]
subst_context_subst_telescope [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_context_rev_subst_telescope [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_context_lift_context_comm [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_map_lift_lift_context [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_extended_lift [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_lift1 [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_subst_context [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_ext_list_ext_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_extended_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_context_lift_id [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_rel0_lift_id [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_context_telescope [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_lift_lift [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_app_context_gen [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_subst_context [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_instance_rev [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_length [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_app_telescope [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_app [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_telescope_empty [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_sorts_local_ctx [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_type_local_ctx [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst_global_uctx_invariants [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
subst0 [abbreviation, in MetaCoq.Template.Ast]
subst0 [abbreviation, in MetaCoq.PCUIC.PCUICAst]
subst0 [abbreviation, in MetaCoq.Erasure.ELiftSubst]
subst0_inst [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
subst0_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst0_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICSpine]
subst1 [definition, in MetaCoq.Template.Ast]
subst1 [definition, in MetaCoq.PCUIC.PCUICAst]
subst1 [definition, in MetaCoq.Erasure.ELiftSubst]
subst1_mkApps [lemma, in MetaCoq.Erasure.ELiftSubst]
subst1_mkApps [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
subst1_inst [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
subst1_mkApps [lemma, in MetaCoq.Template.LiftSubst]
subst10 [abbreviation, in MetaCoq.Template.Ast]
subst10 [abbreviation, in MetaCoq.PCUIC.PCUICAst]
subst10 [abbreviation, in MetaCoq.Erasure.ELiftSubst]
subst10_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
subs_usubst [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subs_nth_error [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subs_nth_error_lt [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subs_nth_error_ge [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
subs_length [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
sub_context_set_empty [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
sub_context_set_trans [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sub_context_set [definition, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sub_context_set_empty [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
sub:228 [binder, in MetaCoq.PCUIC.PCUICSpine]
sub:234 [binder, in MetaCoq.PCUIC.PCUICSpine]
sub:274 [binder, in MetaCoq.PCUIC.PCUICSpine]
sub:283 [binder, in MetaCoq.PCUIC.PCUICSpine]
sub:312 [binder, in MetaCoq.PCUIC.PCUICSpine]
sub:570 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
sub:580 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
sub:604 [binder, in MetaCoq.PCUIC.PCUICInductives]
Success [constructor, in MetaCoq.Translations.translation_utils]
Success [constructor, in MetaCoq.SafeChecker.PCUICSafeConversion]
succs_proper [lemma, in MetaCoq.Template.common.uGraph]
succ_inj [lemma, in MetaCoq.Template.Universes]
suffix [definition, in MetaCoq.Translations.param_binary]
suffix0 [definition, in MetaCoq.Translations.param_binary]
suffix:1444 [binder, in MetaCoq.Erasure.ErasureFunction]
suffix:1446 [binder, in MetaCoq.Erasure.ErasureFunction]
suffix:1450 [binder, in MetaCoq.Erasure.ErasureFunction]
suffix:1452 [binder, in MetaCoq.Erasure.ErasureFunction]
sup_idem [lemma, in MetaCoq.Template.Universes]
sup_comm [lemma, in MetaCoq.Template.Universes]
sup_subst_instance_univ [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sup_subst_instance_univ0 [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
sup0_assoc [lemma, in MetaCoq.Template.Universes]
sup0_idem [lemma, in MetaCoq.Template.Universes]
sup0_comm [lemma, in MetaCoq.Template.Universes]
swap [definition, in MetaCoq.Template.utils.MCProd]
Swf_fix [abbreviation, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
switch_minus [lemma, in MetaCoq.Template.Universes]
switch_no_params [definition, in MetaCoq.Erasure.EInlineProjections]
switch_constructor_as_block [definition, in MetaCoq.Erasure.EConstructorsAsBlocks]
switch_no_params [definition, in MetaCoq.Erasure.ERemoveParams]
switch_unguarded_fix [definition, in MetaCoq.Erasure.EWcbvEval]
symbol:12 [binder, in MetaCoq.Translations.param_original]
symbol:26 [binder, in MetaCoq.Translations.param_binary]
Symmetric [record, in MetaCoq.Translations.MiniHoTT]
Symmetric [inductive, in MetaCoq.Translations.MiniHoTT]
Symmetric [record, in MetaCoq.Translations.MiniHoTT_paths]
Symmetric [inductive, in MetaCoq.Translations.MiniHoTT_paths]
symmetric_equiv [instance, in MetaCoq.Translations.MiniHoTT]
symmetric_paths [instance, in MetaCoq.Translations.MiniHoTT]
symmetric_equiv [instance, in MetaCoq.Translations.MiniHoTT_paths]
symmetric_paths [instance, in MetaCoq.Translations.MiniHoTT_paths]
symmetry [projection, in MetaCoq.Translations.MiniHoTT]
symmetry [constructor, in MetaCoq.Translations.MiniHoTT]
symmetry [projection, in MetaCoq.Translations.MiniHoTT_paths]
symmetry [constructor, in MetaCoq.Translations.MiniHoTT_paths]
sym_eq_univ_prop [instance, in MetaCoq.PCUIC.PCUICCumulProp]
sym:109 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
sym:559 [binder, in MetaCoq.PCUIC.PCUICConfluence]
sym:67 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
s'':130 [binder, in MetaCoq.Template.utils.wGraph]
s'':146 [binder, in MetaCoq.Template.utils.wGraph]
s'':152 [binder, in MetaCoq.Template.utils.wGraph]
s'':156 [binder, in MetaCoq.Template.utils.wGraph]
s'':417 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s'0:840 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s'0:929 [binder, in MetaCoq.PCUIC.PCUICConversion]
s'0:988 [binder, in MetaCoq.PCUIC.PCUICConversion]
s'0:990 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':1007 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':101 [binder, in MetaCoq.Template.utils.wGraph]
s':1016 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':102 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':1025 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':1025 [binder, in MetaCoq.Template.utils.wGraph]
s':1033 [binder, in MetaCoq.Template.utils.wGraph]
s':107 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':110 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':111 [binder, in MetaCoq.PCUIC.PCUICContexts]
s':112 [binder, in MetaCoq.Erasure.ESubstitution]
s':1174 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':1186 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':119 [binder, in MetaCoq.Erasure.Prelim]
s':1195 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':120 [binder, in MetaCoq.Template.utils.wGraph]
S':126 [binder, in MetaCoq.PCUIC.PCUICArities]
s':126 [binder, in MetaCoq.PCUIC.PCUICSR]
s':127 [binder, in MetaCoq.PCUIC.PCUICEquality]
s':127 [binder, in MetaCoq.Template.utils.wGraph]
s':127 [binder, in MetaCoq.Template.TypingWf]
s':128 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':129 [binder, in MetaCoq.Template.utils.wGraph]
s':133 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':140 [binder, in MetaCoq.Template.utils.wGraph]
s':142 [binder, in MetaCoq.Erasure.ESubstitution]
s':142 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':145 [binder, in MetaCoq.Template.utils.wGraph]
s':149 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':151 [binder, in MetaCoq.Template.utils.wGraph]
s':155 [binder, in MetaCoq.Template.utils.wGraph]
s':158 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':159 [binder, in MetaCoq.Template.utils.wGraph]
s':160 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':165 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':171 [binder, in MetaCoq.PCUIC.PCUICArities]
s':179 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':187 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':192 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':206 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':208 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':210 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':235 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s':239 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':249 [binder, in MetaCoq.Erasure.EArities]
s':25 [binder, in MetaCoq.Template.Universes]
s':251 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':253 [binder, in MetaCoq.Template.utils.wGraph]
s':254 [binder, in MetaCoq.Erasure.EArities]
s':257 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':260 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':261 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':265 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':272 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':275 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':279 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':280 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':284 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':286 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':291 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s':292 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s':293 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':30 [binder, in MetaCoq.PCUIC.PCUICProgress]
s':300 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':301 [binder, in MetaCoq.Template.utils.wGraph]
s':306 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':307 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':307 [binder, in MetaCoq.Template.utils.wGraph]
s':311 [binder, in MetaCoq.Template.utils.wGraph]
s':319 [binder, in MetaCoq.Template.utils.wGraph]
s':322 [binder, in MetaCoq.Template.utils.wGraph]
s':326 [binder, in MetaCoq.Template.utils.wGraph]
s':329 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s':33 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':332 [binder, in MetaCoq.Template.utils.wGraph]
s':334 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s':334 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':34 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':346 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
s':347 [binder, in MetaCoq.Template.utils.wGraph]
s':35 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s':36 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
s':36 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':36 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s':360 [binder, in MetaCoq.PCUIC.PCUICInductives]
s':371 [binder, in MetaCoq.PCUIC.PCUICInductives]
s':383 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':386 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':39 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':397 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':400 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':403 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':405 [binder, in MetaCoq.Template.utils.wGraph]
s':406 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':408 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':410 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':410 [binder, in MetaCoq.Template.utils.wGraph]
s':413 [binder, in MetaCoq.Template.utils.wGraph]
s':414 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':416 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':423 [binder, in MetaCoq.Template.utils.wGraph]
s':43 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':443 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s':45 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
s':450 [binder, in MetaCoq.Template.utils.wGraph]
s':46 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s':467 [binder, in MetaCoq.PCUIC.PCUICNormal]
s':467 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':473 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s':48 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':482 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s':494 [binder, in MetaCoq.Template.utils.wGraph]
s':499 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
s':50 [binder, in MetaCoq.Template.Universes]
s':50 [binder, in MetaCoq.Template.Typing]
s':509 [binder, in MetaCoq.Template.Universes]
s':51 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':515 [binder, in MetaCoq.Template.Universes]
s':518 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s':52 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':529 [binder, in MetaCoq.Template.Universes]
s':54 [binder, in MetaCoq.PCUIC.PCUICProgress]
s':542 [binder, in MetaCoq.Template.common.uGraph]
s':544 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s':5634 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
S':568 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s':574 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
S':576 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s':58 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':583 [binder, in MetaCoq.PCUIC.PCUICInductives]
s':6 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':60 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s':600 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s':605 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s':62 [binder, in MetaCoq.Template.Typing]
s':62 [binder, in MetaCoq.Template.Reflect]
s':62 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':620 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s':634 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s':648 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':65 [binder, in MetaCoq.PCUIC.PCUICArities]
S':656 [binder, in MetaCoq.Template.common.uGraph]
s':66 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':67 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':685 [binder, in MetaCoq.Template.Universes]
s':685 [binder, in MetaCoq.PCUIC.PCUICSR]
s':73 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
s':742 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':752 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':765 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':77 [binder, in MetaCoq.Template.Typing]
s':77 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':772 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':779 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':795 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':796 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':80 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
s':80 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s':805 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':812 [binder, in MetaCoq.PCUIC.PCUICSpine]
s':827 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s':828 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s':829 [binder, in MetaCoq.Template.utils.wGraph]
s':83 [binder, in MetaCoq.Template.TermEquality]
s':83 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s':84 [binder, in MetaCoq.PCUIC.PCUICElimination]
s':862 [binder, in MetaCoq.Template.utils.wGraph]
s':92 [binder, in MetaCoq.Erasure.ESubstitution]
s':927 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':967 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':979 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':98 [binder, in MetaCoq.Template.utils.wGraph]
s':985 [binder, in MetaCoq.PCUIC.PCUICConversion]
s':997 [binder, in MetaCoq.PCUIC.PCUICConversion]
s0:102 [binder, in MetaCoq.Template.utils.wGraph]
s0:112 [binder, in MetaCoq.Template.utils.wGraph]
s0:171 [binder, in MetaCoq.PCUIC.PCUICElimination]
s0:175 [binder, in MetaCoq.PCUIC.PCUICElimination]
s0:385 [binder, in MetaCoq.Template.utils.wGraph]
s0:389 [binder, in MetaCoq.Template.utils.wGraph]
s0:395 [binder, in MetaCoq.Template.utils.wGraph]
s0:470 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s0:839 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s0:845 [binder, in MetaCoq.Template.utils.wGraph]
s0:849 [binder, in MetaCoq.Template.utils.wGraph]
s0:853 [binder, in MetaCoq.Template.utils.wGraph]
s0:928 [binder, in MetaCoq.PCUIC.PCUICConversion]
s0:987 [binder, in MetaCoq.PCUIC.PCUICConversion]
s0:989 [binder, in MetaCoq.PCUIC.PCUICConversion]
s1':655 [binder, in MetaCoq.Template.Universes]
s1:100 [binder, in MetaCoq.PCUIC.PCUICProgress]
s1:1000 [binder, in MetaCoq.Template.Typing]
s1:1010 [binder, in MetaCoq.Template.Typing]
s1:103 [binder, in MetaCoq.Template.utils.wGraph]
s1:103 [binder, in MetaCoq.PCUIC.PCUICTyping]
S1:105 [binder, in MetaCoq.Template.common.uGraph]
s1:1064 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s1:110 [binder, in MetaCoq.PCUIC.PCUICProgress]
s1:113 [binder, in MetaCoq.Template.utils.wGraph]
s1:116 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:130 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:148 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:148 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s1:151 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s1:162 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:194 [binder, in MetaCoq.Template.Universes]
s1:20 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s1:244 [binder, in MetaCoq.PCUIC.PCUICProgress]
s1:253 [binder, in MetaCoq.PCUIC.PCUICProgress]
s1:263 [binder, in MetaCoq.PCUIC.PCUICProgress]
s1:3 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s1:321 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s1:33 [binder, in MetaCoq.Template.utils.bytestring]
s1:345 [binder, in MetaCoq.Template.Universes]
s1:345 [binder, in MetaCoq.Template.Checker]
s1:356 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s1:386 [binder, in MetaCoq.Template.utils.wGraph]
s1:39 [binder, in MetaCoq.Template.utils.bytestring]
s1:392 [binder, in MetaCoq.Template.utils.wGraph]
s1:396 [binder, in MetaCoq.Template.utils.wGraph]
s1:42 [binder, in MetaCoq.PCUIC.PCUICInversion]
s1:449 [binder, in MetaCoq.Template.common.uGraph]
s1:466 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
s1:471 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s1:484 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:493 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:50 [binder, in MetaCoq.PCUIC.PCUICInversion]
s1:503 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:588 [binder, in MetaCoq.Template.Universes]
s1:590 [binder, in MetaCoq.Template.Universes]
s1:594 [binder, in MetaCoq.Template.Universes]
s1:615 [binder, in MetaCoq.Template.Typing]
s1:620 [binder, in MetaCoq.Template.Typing]
s1:626 [binder, in MetaCoq.Template.Typing]
s1:654 [binder, in MetaCoq.Template.Universes]
S1:657 [binder, in MetaCoq.Template.common.uGraph]
s1:666 [binder, in MetaCoq.Template.Universes]
s1:67 [binder, in MetaCoq.PCUIC.PCUICInversion]
s1:686 [binder, in MetaCoq.Template.Universes]
s1:690 [binder, in MetaCoq.Template.Universes]
s1:692 [binder, in MetaCoq.Template.Universes]
s1:694 [binder, in MetaCoq.Template.Universes]
s1:696 [binder, in MetaCoq.Template.Universes]
s1:702 [binder, in MetaCoq.Template.Universes]
s1:704 [binder, in MetaCoq.Template.Universes]
s1:706 [binder, in MetaCoq.Template.Universes]
s1:812 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:821 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:831 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:839 [binder, in MetaCoq.Template.utils.wGraph]
s1:842 [binder, in MetaCoq.Template.utils.wGraph]
s1:846 [binder, in MetaCoq.Template.utils.wGraph]
s1:850 [binder, in MetaCoq.Template.utils.wGraph]
s1:854 [binder, in MetaCoq.Template.utils.wGraph]
s1:91 [binder, in MetaCoq.PCUIC.PCUICProgress]
s1:92 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:97 [binder, in MetaCoq.PCUIC.PCUICTyping]
s1:991 [binder, in MetaCoq.Template.Typing]
s2':657 [binder, in MetaCoq.Template.Universes]
s2':786 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s2:104 [binder, in MetaCoq.Template.utils.wGraph]
S2:106 [binder, in MetaCoq.Template.common.uGraph]
s2:1065 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s2:114 [binder, in MetaCoq.Template.utils.wGraph]
s2:117 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:131 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:149 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:149 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s2:152 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s2:163 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:195 [binder, in MetaCoq.Template.Universes]
s2:21 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s2:245 [binder, in MetaCoq.PCUIC.PCUICProgress]
s2:322 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s2:34 [binder, in MetaCoq.Template.utils.bytestring]
s2:346 [binder, in MetaCoq.Template.Universes]
s2:346 [binder, in MetaCoq.Template.Checker]
s2:357 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s2:387 [binder, in MetaCoq.Template.utils.wGraph]
s2:393 [binder, in MetaCoq.Template.utils.wGraph]
s2:397 [binder, in MetaCoq.Template.utils.wGraph]
s2:4 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s2:40 [binder, in MetaCoq.Template.utils.bytestring]
s2:43 [binder, in MetaCoq.PCUIC.PCUICInversion]
s2:450 [binder, in MetaCoq.Template.common.uGraph]
s2:472 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s2:472 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
s2:485 [binder, in MetaCoq.PCUIC.PCUICTyping]
s2:51 [binder, in MetaCoq.PCUIC.PCUICInversion]
s2:587 [binder, in MetaCoq.Template.Universes]
s2:592 [binder, in MetaCoq.Template.Universes]
s2:595 [binder, in MetaCoq.Template.Universes]
s2:616 [binder, in MetaCoq.Template.Typing]
s2:656 [binder, in MetaCoq.Template.Universes]
S2:658 [binder, in MetaCoq.Template.common.uGraph]
s2:667 [binder, in MetaCoq.Template.Universes]
s2:687 [binder, in MetaCoq.Template.Universes]
s2:691 [binder, in MetaCoq.Template.Universes]
s2:693 [binder, in MetaCoq.Template.Universes]
s2:695 [binder, in MetaCoq.Template.Universes]
s2:697 [binder, in MetaCoq.Template.Universes]
s2:703 [binder, in MetaCoq.Template.Universes]
s2:705 [binder, in MetaCoq.Template.Universes]
s2:707 [binder, in MetaCoq.Template.Universes]
s2:785 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s2:813 [binder, in MetaCoq.PCUIC.PCUICTyping]
s2:840 [binder, in MetaCoq.Template.utils.wGraph]
s2:843 [binder, in MetaCoq.Template.utils.wGraph]
s2:847 [binder, in MetaCoq.Template.utils.wGraph]
s2:851 [binder, in MetaCoq.Template.utils.wGraph]
s2:855 [binder, in MetaCoq.Template.utils.wGraph]
s2:92 [binder, in MetaCoq.PCUIC.PCUICProgress]
s2:93 [binder, in MetaCoq.PCUIC.PCUICTyping]
s2:992 [binder, in MetaCoq.Template.Typing]
s3:473 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s3:668 [binder, in MetaCoq.Template.Universes]
s:1 [binder, in MetaCoq.Examples.typing_correctness]
s:1 [binder, in MetaCoq.Examples.metacoq_tour_prelude]
s:1 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:10 [binder, in MetaCoq.Translations.param_binary]
s:10 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:10 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
S:100 [binder, in MetaCoq.Template.utils.MCRelations]
s:100 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:100 [binder, in MetaCoq.Template.utils.wGraph]
s:1003 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1006 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
S:1008 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:101 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:1015 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:1016 [binder, in MetaCoq.Template.utils.wGraph]
s:102 [binder, in MetaCoq.Template.Universes]
s:1020 [binder, in MetaCoq.Template.Typing]
s:1021 [binder, in MetaCoq.Template.utils.wGraph]
s:1024 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:103 [binder, in MetaCoq.Erasure.ESubstitution]
s:103 [binder, in MetaCoq.Template.EnvironmentTyping]
s:103 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:103 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
S:104 [binder, in MetaCoq.Template.common.uGraph]
s:104 [binder, in MetaCoq.Examples.tauto]
s:105 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:105 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:105 [binder, in MetaCoq.Examples.tauto]
S:1054 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:106 [binder, in MetaCoq.Template.WfAst]
s:106 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:107 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:107 [binder, in MetaCoq.Examples.tauto]
s:1072 [binder, in MetaCoq.Template.utils.wGraph]
s:1074 [binder, in MetaCoq.Template.utils.wGraph]
s:1075 [binder, in MetaCoq.Template.utils.wGraph]
S:1077 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:108 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:108 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:1086 [binder, in MetaCoq.Template.utils.wGraph]
s:1089 [binder, in MetaCoq.Template.utils.wGraph]
s:109 [binder, in MetaCoq.Template.utils.wGraph]
s:109 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:109 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:1094 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1096 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1098 [binder, in MetaCoq.Template.utils.wGraph]
s:11 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:11 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:110 [binder, in MetaCoq.Erasure.ESubstitution]
s:110 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:110 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:110 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:110 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:110 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:1104 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1106 [binder, in MetaCoq.Template.Typing]
s:111 [binder, in MetaCoq.Erasure.EInduction]
s:1110 [binder, in MetaCoq.Template.utils.wGraph]
s:1119 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1120 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:1127 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:113 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:1136 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
S:114 [binder, in MetaCoq.PCUIC.PCUICArities]
s:114 [binder, in MetaCoq.PCUIC.PCUICSR]
s:114 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:114 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
s:114 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:117 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:1173 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:118 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:1185 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:119 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:119 [binder, in MetaCoq.Template.utils.wGraph]
s:119 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:1193 [binder, in MetaCoq.Translations.MiniHoTT]
s:1194 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:1196 [binder, in MetaCoq.Template.Typing]
s:1199 [binder, in MetaCoq.Template.Typing]
s:12 [binder, in MetaCoq.PCUIC.PCUICInversion]
s:12 [binder, in MetaCoq.Erasure.ELiftSubst]
s:12 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
s:12 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:12 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:120 [binder, in MetaCoq.PCUIC.PCUICProgress]
s:1201 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:1203 [binder, in MetaCoq.Translations.MiniHoTT]
s:1205 [binder, in MetaCoq.Template.Typing]
s:1208 [binder, in MetaCoq.Template.Typing]
S:121 [binder, in MetaCoq.PCUIC.PCUICArities]
s:121 [binder, in MetaCoq.Erasure.EInlineProjections]
s:121 [binder, in MetaCoq.PCUIC.PCUICSR]
s:1211 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:122 [binder, in MetaCoq.Erasure.EInduction]
s:1228 [binder, in MetaCoq.Template.Typing]
s:123 [binder, in MetaCoq.Erasure.EInlineProjections]
s:1231 [binder, in MetaCoq.Template.Typing]
s:1237 [binder, in MetaCoq.Template.Typing]
s:124 [binder, in MetaCoq.Erasure.ESubstitution]
s:124 [binder, in MetaCoq.PCUIC.PCUICSR]
s:1240 [binder, in MetaCoq.Template.Typing]
S:125 [binder, in MetaCoq.PCUIC.PCUICArities]
s:125 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:125 [binder, in MetaCoq.Template.TypingWf]
s:126 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:126 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:126 [binder, in MetaCoq.PCUIC.PCUICEquality]
s:126 [binder, in MetaCoq.Template.utils.wGraph]
s:126 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:1269 [binder, in MetaCoq.Translations.MiniHoTT]
s:127 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:127 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:1273 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:1277 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:128 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:128 [binder, in MetaCoq.Template.utils.wGraph]
s:129 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:129 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:129 [binder, in MetaCoq.Template.TypingWf]
s:1296 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1299 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:13 [binder, in MetaCoq.Erasure.EInduction]
s:130 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:130 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:130 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:130 [binder, in MetaCoq.Erasure.ERemoveParams]
s:1304 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:1309 [binder, in MetaCoq.Translations.MiniHoTT]
s:131 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
s:131 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:1311 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1317 [binder, in MetaCoq.Translations.MiniHoTT_paths]
S:132 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:132 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:132 [binder, in MetaCoq.PCUIC.PCUICSR]
s:132 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:133 [binder, in MetaCoq.PCUIC.PCUICElimination]
S:133 [binder, in MetaCoq.PCUIC.PCUICArities]
s:133 [binder, in MetaCoq.Template.utils.wGraph]
s:133 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:1330 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:134 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:134 [binder, in MetaCoq.Translations.MiniHoTT]
s:1344 [binder, in MetaCoq.Translations.MiniHoTT]
s:1345 [binder, in MetaCoq.Translations.MiniHoTT]
s:135 [binder, in MetaCoq.Erasure.ESubstitution]
s:135 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:135 [binder, in MetaCoq.Erasure.EEtaExpanded]
s:1352 [binder, in MetaCoq.Translations.MiniHoTT]
s:1352 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:1353 [binder, in MetaCoq.Translations.MiniHoTT]
s:1353 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:136 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:136 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:136 [binder, in MetaCoq.Template.utils.wGraph]
s:1360 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:1361 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:137 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
S:137 [binder, in MetaCoq.PCUIC.PCUICArities]
s:139 [binder, in MetaCoq.Template.utils.wGraph]
s:139 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:139 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:1394 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
s:14 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:14 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:140 [binder, in MetaCoq.Erasure.ESubstitution]
s:140 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:140 [binder, in MetaCoq.PCUIC.PCUICSR]
S:141 [binder, in MetaCoq.PCUIC.PCUICArities]
s:142 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:142 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:143 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:143 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:144 [binder, in MetaCoq.Template.utils.wGraph]
s:145 [binder, in MetaCoq.Template.LiftSubst]
s:146 [binder, in MetaCoq.PCUIC.PCUICArities]
s:147 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
s:148 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
s:148 [binder, in MetaCoq.Template.utils.wGraph]
s:148 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:149 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:150 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:150 [binder, in MetaCoq.Template.utils.wGraph]
s:150 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:151 [binder, in MetaCoq.PCUIC.PCUICArities]
s:151 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
s:151 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:152 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:153 [binder, in MetaCoq.PCUIC.PCUICArities]
s:154 [binder, in MetaCoq.Template.utils.wGraph]
s:154 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:1547 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
s:155 [binder, in MetaCoq.Template.utils.bytestring]
s:156 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:156 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:157 [binder, in MetaCoq.PCUIC.PCUICAlpha]
s:157 [binder, in MetaCoq.Erasure.ErasureFunction]
s:157 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:158 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:158 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:158 [binder, in MetaCoq.Template.utils.wGraph]
s:159 [binder, in MetaCoq.Template.utils.bytestring]
s:159 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:159 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:159 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:16 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:16 [binder, in MetaCoq.Erasure.EDeps]
s:16 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:16 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:160 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:161 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:162 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:163 [binder, in MetaCoq.Template.EtaExpand]
s:163 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:164 [binder, in MetaCoq.PCUIC.PCUICArities]
s:164 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:166 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:167 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:168 [binder, in MetaCoq.PCUIC.PCUICAlpha]
s:168 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:169 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:17 [binder, in MetaCoq.Template.utils.MCString]
s:17 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:170 [binder, in MetaCoq.PCUIC.PCUICArities]
s:170 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:170 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:170 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
s:171 [binder, in MetaCoq.Erasure.ELiftSubst]
s:171 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:171 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:172 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:173 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:1737 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
s:1745 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
s:1747 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
s:175 [binder, in MetaCoq.PCUIC.PCUICAst]
s:175 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:175 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:176 [binder, in MetaCoq.PCUIC.PCUICNormal]
s:176 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:177 [binder, in MetaCoq.PCUIC.PCUICArities]
s:177 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:178 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
s:178 [binder, in MetaCoq.Erasure.ELiftSubst]
s:179 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:18 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
s:181 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:182 [binder, in MetaCoq.Erasure.ELiftSubst]
s:183 [binder, in MetaCoq.Template.Ast]
s:183 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:184 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:184 [binder, in MetaCoq.PCUIC.PCUICSR]
s:186 [binder, in MetaCoq.PCUIC.PCUICArities]
s:186 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:186 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:188 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:188 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s:19 [binder, in MetaCoq.PCUIC.PCUICValidity]
s:19 [binder, in MetaCoq.PCUIC.PCUICNormal]
s:19 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:19 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
s:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:19 [binder, in MetaCoq.Erasure.ECSubst]
s:190 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:191 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:192 [binder, in MetaCoq.Template.Universes]
s:192 [binder, in MetaCoq.PCUIC.PCUICArities]
s:192 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:193 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:193 [binder, in MetaCoq.SafeChecker.PCUICErrors]
s:194 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:194 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:195 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:196 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:197 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:201 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:201 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:202 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:205 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:205 [binder, in MetaCoq.Template.EnvironmentTyping]
s:205 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:205 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:206 [binder, in MetaCoq.PCUIC.PCUICArities]
s:207 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:207 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:208 [binder, in MetaCoq.Erasure.EInduction]
s:208 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:209 [binder, in MetaCoq.Template.EnvironmentTyping]
s:209 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:21 [binder, in MetaCoq.Erasure.EInduction]
s:21 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:211 [binder, in MetaCoq.PCUIC.PCUICProgress]
s:211 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:212 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:213 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:215 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:216 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s:216 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:218 [binder, in MetaCoq.Erasure.EInduction]
s:22 [binder, in MetaCoq.Template.Universes]
s:22 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:22 [binder, in MetaCoq.Template.EnvMap]
s:22 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:22 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:22 [binder, in MetaCoq.PCUIC.utils.PCUICPrimitive]
s:22 [binder, in MetaCoq.Template.Induction]
s:222 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
S:2229 [binder, in MetaCoq.Template.utils.All_Forall]
s:224 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:226 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:227 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:227 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:227 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:228 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s:229 [binder, in MetaCoq.Template.EnvironmentTyping]
s:23 [binder, in MetaCoq.Template.utils.bytestring]
s:23 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:230 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:232 [binder, in MetaCoq.Template.Ast]
s:232 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:233 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:234 [binder, in MetaCoq.Template.common.uGraph]
s:235 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:236 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:236 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:237 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:238 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:24 [binder, in MetaCoq.Template.Universes]
s:24 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:24 [binder, in MetaCoq.PCUIC.utils.PCUICPrimitive]
s:24 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:240 [binder, in MetaCoq.Template.EnvironmentTyping]
s:241 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:242 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:244 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:248 [binder, in MetaCoq.Erasure.EArities]
s:25 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:25 [binder, in MetaCoq.Examples.tauto]
s:250 [binder, in MetaCoq.Template.utils.wGraph]
s:250 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:252 [binder, in MetaCoq.Template.utils.wGraph]
s:253 [binder, in MetaCoq.Erasure.EArities]
s:253 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:255 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:256 [binder, in MetaCoq.Erasure.EArities]
s:256 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:256 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:257 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:257 [binder, in MetaCoq.Template.utils.wGraph]
s:259 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:259 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:26 [binder, in MetaCoq.Template.Universes]
s:26 [binder, in MetaCoq.Erasure.EDeps]
s:26 [binder, in MetaCoq.Examples.tauto]
s:260 [binder, in MetaCoq.Template.Universes]
s:260 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:261 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:261 [binder, in MetaCoq.PCUIC.PCUICAlpha]
s:262 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:262 [binder, in MetaCoq.Erasure.EArities]
s:263 [binder, in MetaCoq.Template.utils.wGraph]
s:263 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:264 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:264 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:267 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:268 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:268 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:269 [binder, in MetaCoq.Template.utils.wGraph]
s:269 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:27 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
S:27 [binder, in MetaCoq.Template.utils.MCRelations]
s:27 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:27 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:27 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:27 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:271 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:2721 [binder, in MetaCoq.Translations.MiniHoTT]
s:2729 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:273 [binder, in MetaCoq.PCUIC.PCUICProgress]
s:273 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:274 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:275 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:2753 [binder, in MetaCoq.Translations.MiniHoTT]
s:2761 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:278 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:279 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:28 [binder, in MetaCoq.Template.utils.bytestring]
s:280 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:282 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:282 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:283 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:285 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:285 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:2875 [binder, in MetaCoq.Translations.MiniHoTT]
s:2883 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:29 [binder, in MetaCoq.Erasure.EInlineProjections]
s:29 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
s:290 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:290 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:291 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:292 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:294 [binder, in MetaCoq.Template.EnvironmentTyping]
s:295 [binder, in MetaCoq.Template.utils.wGraph]
s:297 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:298 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:299 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:3 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
s:30 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:30 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s:30 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
s:30 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:30 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
s:30 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:30 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:30 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
s:300 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:301 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:302 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:305 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:306 [binder, in MetaCoq.PCUIC.PCUICElimination]
s:306 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:308 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:309 [binder, in MetaCoq.Template.Environment]
s:31 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:31 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
s:31 [binder, in MetaCoq.Erasure.EDeps]
s:31 [binder, in MetaCoq.Erasure.Prelim]
s:313 [binder, in MetaCoq.Template.utils.wGraph]
s:313 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:313 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:314 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:314 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:318 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:32 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:32 [binder, in MetaCoq.Template.Checker]
s:320 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:321 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:321 [binder, in MetaCoq.Template.utils.wGraph]
s:323 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:324 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:325 [binder, in MetaCoq.Template.utils.wGraph]
s:328 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:328 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:33 [binder, in MetaCoq.Erasure.EDeps]
s:33 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:33 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
s:33 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:33 [binder, in MetaCoq.Template.Induction]
s:331 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:331 [binder, in MetaCoq.Template.utils.wGraph]
s:333 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:333 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:335 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:34 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s:34 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s:340 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:341 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:342 [binder, in MetaCoq.Template.Universes]
s:342 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:343 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:344 [binder, in MetaCoq.Template.Universes]
s:345 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
s:346 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:346 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:346 [binder, in MetaCoq.Template.utils.wGraph]
s:348 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
s:348 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:35 [binder, in MetaCoq.Template.TemplateMonad.Core]
s:35 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:35 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:35 [binder, in MetaCoq.PCUIC.PCUICInversion]
s:35 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
s:35 [binder, in MetaCoq.Template.Environment]
s:35 [binder, in MetaCoq.PCUIC.PCUICSR]
s:35 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:351 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:354 [binder, in MetaCoq.Template.utils.wGraph]
s:357 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:359 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:360 [binder, in MetaCoq.Template.utils.wGraph]
s:361 [binder, in MetaCoq.PCUIC.PCUICProgress]
s:362 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:362 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:365 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:365 [binder, in MetaCoq.Template.utils.wGraph]
s:366 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:367 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:369 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:37 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:370 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:370 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:371 [binder, in MetaCoq.Template.utils.wGraph]
s:375 [binder, in MetaCoq.Template.utils.wGraph]
s:376 [binder, in MetaCoq.Template.EtaExpand]
s:376 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:379 [binder, in MetaCoq.Template.utils.wGraph]
S:38 [binder, in MetaCoq.Template.utils.MCRelations]
s:38 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:38 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:38 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:381 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:381 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:382 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:385 [binder, in MetaCoq.Template.EnvironmentTyping]
s:385 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:387 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:39 [binder, in MetaCoq.Template.Typing]
s:39 [binder, in MetaCoq.Template.Environment]
s:39 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
s:390 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:391 [binder, in MetaCoq.PCUIC.PCUICNormal]
s:393 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:394 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:396 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:399 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:399 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:4 [binder, in MetaCoq.PCUIC.PCUICArities]
s:4 [binder, in MetaCoq.Examples.typing_correctness]
s:4 [binder, in MetaCoq.Examples.metacoq_tour_prelude]
s:400 [binder, in MetaCoq.Template.utils.wGraph]
s:402 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:403 [binder, in MetaCoq.Template.EnvironmentTyping]
s:405 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:407 [binder, in MetaCoq.Template.Universes]
s:407 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:408 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:409 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
S:41 [binder, in MetaCoq.Template.utils.MCRelations]
s:41 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:413 [binder, in MetaCoq.Template.EtaExpand]
s:413 [binder, in MetaCoq.Template.Universes]
s:413 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:415 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:418 [binder, in MetaCoq.Template.utils.wGraph]
s:418 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:42 [binder, in MetaCoq.PCUIC.PCUICValidity]
s:42 [binder, in MetaCoq.Template.Environment]
s:421 [binder, in MetaCoq.PCUIC.PCUICProgress]
s:423 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:424 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:425 [binder, in MetaCoq.Template.utils.MCList]
s:426 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:427 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:427 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:428 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:43 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
s:430 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:430 [binder, in MetaCoq.Template.utils.wGraph]
s:431 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:433 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:435 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:437 [binder, in MetaCoq.Template.Universes]
S:44 [binder, in MetaCoq.Template.utils.MCRelations]
s:44 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:44 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
s:440 [binder, in MetaCoq.Template.utils.wGraph]
s:441 [binder, in MetaCoq.Template.utils.wGraph]
s:441 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:449 [binder, in MetaCoq.Template.utils.wGraph]
s:45 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:45 [binder, in MetaCoq.Examples.tauto]
s:45 [binder, in MetaCoq.Template.Environment]
s:45 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:45 [binder, in MetaCoq.Template.Induction]
s:450 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s:453 [binder, in MetaCoq.Template.utils.wGraph]
s:458 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:46 [binder, in MetaCoq.Template.Typing]
s:46 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:46 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:461 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:461 [binder, in MetaCoq.Template.utils.wGraph]
s:466 [binder, in MetaCoq.PCUIC.PCUICNormal]
s:466 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:466 [binder, in MetaCoq.Template.utils.wGraph]
S:47 [binder, in MetaCoq.Template.utils.MCRelations]
s:47 [binder, in MetaCoq.Template.Normal]
s:47 [binder, in MetaCoq.Template.Environment]
s:470 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:471 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:472 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:474 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:475 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:476 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:48 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
s:48 [binder, in MetaCoq.Examples.tauto]
s:480 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:481 [binder, in MetaCoq.Template.utils.wGraph]
s:482 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:484 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:485 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:488 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:49 [binder, in MetaCoq.PCUIC.PCUICProgress]
s:49 [binder, in MetaCoq.Template.Universes]
s:490 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:490 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:493 [binder, in MetaCoq.Template.utils.wGraph]
s:494 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:497 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:497 [binder, in MetaCoq.Template.utils.wGraph]
s:498 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
s:498 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:5 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:5 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:5 [binder, in MetaCoq.Template.Transform]
s:5 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:50 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:50 [binder, in MetaCoq.Template.AstUtils]
s:50 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:501 [binder, in MetaCoq.Template.utils.wGraph]
s:504 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:508 [binder, in MetaCoq.Template.Universes]
s:508 [binder, in MetaCoq.Template.utils.wGraph]
s:508 [binder, in MetaCoq.Examples.tauto]
s:508 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:509 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:51 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
s:51 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:51 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:511 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:514 [binder, in MetaCoq.Template.Universes]
s:514 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:517 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:52 [binder, in MetaCoq.Examples.tauto]
s:52 [binder, in MetaCoq.Template.Environment]
s:520 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:521 [binder, in MetaCoq.Template.Typing]
s:523 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:523 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:524 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:528 [binder, in MetaCoq.Template.Universes]
s:529 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:531 [binder, in MetaCoq.Template.utils.wGraph]
s:534 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:535 [binder, in MetaCoq.Template.utils.wGraph]
s:536 [binder, in MetaCoq.Translations.MiniHoTT]
s:54 [binder, in MetaCoq.Template.Universes]
s:54 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:541 [binder, in MetaCoq.Template.common.uGraph]
s:543 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:543 [binder, in MetaCoq.Template.utils.wGraph]
s:544 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:546 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:548 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:548 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:5482 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s:549 [binder, in MetaCoq.PCUIC.PCUICSR]
s:549 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
S:55 [binder, in MetaCoq.Template.utils.MCRelations]
s:55 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:550 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:551 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:551 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:555 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:555 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:556 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:556 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:557 [binder, in MetaCoq.Template.Typing]
s:557 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:558 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:558 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:558 [binder, in MetaCoq.Translations.MiniHoTT]
s:559 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:56 [binder, in MetaCoq.PCUIC.PCUICValidity]
s:56 [binder, in MetaCoq.Template.Environment]
s:56 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:560 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:5608 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s:562 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:564 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:566 [binder, in MetaCoq.Translations.MiniHoTT_paths]
S:567 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:567 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:569 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:569 [binder, in MetaCoq.Translations.MiniHoTT]
s:57 [binder, in MetaCoq.Template.Typing]
s:57 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:57 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:571 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:573 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
S:575 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:577 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:577 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:579 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:58 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:58 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:580 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:580 [binder, in MetaCoq.Translations.MiniHoTT]
s:581 [binder, in MetaCoq.Template.utils.wGraph]
s:583 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:584 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:586 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:587 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:587 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:587 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:588 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:59 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
s:59 [binder, in MetaCoq.PCUIC.PCUICInversion]
s:59 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:590 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:594 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:596 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:597 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:598 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:598 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:598 [binder, in MetaCoq.Translations.MiniHoTT]
s:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
s:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:6 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:6 [binder, in MetaCoq.Template.Induction]
s:60 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
s:60 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:60 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s:602 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:603 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:603 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:604 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:606 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:606 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:607 [binder, in MetaCoq.Template.Typing]
s:607 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:608 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:61 [binder, in MetaCoq.Template.Reflect]
s:61 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:61 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:61 [binder, in MetaCoq.Template.Induction]
s:611 [binder, in MetaCoq.Template.Typing]
s:613 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:616 [binder, in MetaCoq.Translations.MiniHoTT]
s:619 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:62 [binder, in MetaCoq.Examples.tauto]
s:62 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:62 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:621 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:624 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:626 [binder, in MetaCoq.PCUIC.PCUICInductives]
S:629 [binder, in MetaCoq.Template.utils.wGraph]
s:63 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:630 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:631 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:632 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:633 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
S:633 [binder, in MetaCoq.Template.utils.wGraph]
s:638 [binder, in MetaCoq.Template.Universes]
s:638 [binder, in MetaCoq.Template.common.uGraph]
s:64 [binder, in MetaCoq.PCUIC.PCUICInductives]
s:640 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:642 [binder, in MetaCoq.Template.Universes]
s:643 [binder, in MetaCoq.Template.Universes]
S:643 [binder, in MetaCoq.Template.utils.wGraph]
s:646 [binder, in MetaCoq.PCUIC.PCUICSpine]
S:647 [binder, in MetaCoq.Template.utils.wGraph]
s:649 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:649 [binder, in MetaCoq.Template.common.uGraph]
S:65 [binder, in MetaCoq.Template.utils.MCRelations]
s:65 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:65 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:651 [binder, in MetaCoq.Template.Universes]
S:655 [binder, in MetaCoq.Template.common.uGraph]
s:657 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:659 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:66 [binder, in MetaCoq.Template.Typing]
s:66 [binder, in MetaCoq.Examples.tauto]
s:66 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:66 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:660 [binder, in MetaCoq.Template.EnvironmentTyping]
s:661 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:663 [binder, in MetaCoq.Template.Universes]
s:663 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:664 [binder, in MetaCoq.Template.Universes]
s:665 [binder, in MetaCoq.Template.Universes]
s:669 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:67 [binder, in MetaCoq.Template.utils.bytestring]
s:67 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
s:67 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
s:672 [binder, in MetaCoq.Template.Universes]
s:673 [binder, in MetaCoq.PCUIC.PCUICSR]
s:674 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:676 [binder, in MetaCoq.Template.Typing]
s:676 [binder, in MetaCoq.PCUIC.PCUICSpine]
S:677 [binder, in MetaCoq.Template.utils.wGraph]
s:679 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:68 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:680 [binder, in MetaCoq.PCUIC.PCUICSpine]
S:681 [binder, in MetaCoq.Template.utils.wGraph]
s:682 [binder, in MetaCoq.Template.Typing]
s:684 [binder, in MetaCoq.Template.Universes]
s:684 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:684 [binder, in MetaCoq.PCUIC.PCUICSR]
s:685 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:687 [binder, in MetaCoq.Template.Typing]
s:69 [binder, in MetaCoq.Template.TermEquality]
s:691 [binder, in MetaCoq.PCUIC.PCUICSR]
s:694 [binder, in MetaCoq.Template.Typing]
S:695 [binder, in MetaCoq.Template.utils.wGraph]
S:699 [binder, in MetaCoq.Template.utils.wGraph]
s:7 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
s:7 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:70 [binder, in MetaCoq.Examples.tauto]
s:70 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:708 [binder, in MetaCoq.Template.Typing]
s:71 [binder, in MetaCoq.Erasure.EWellformed]
s:71 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:71 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:710 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:712 [binder, in MetaCoq.Template.utils.wGraph]
s:714 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:717 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:717 [binder, in MetaCoq.PCUIC.PCUICEquality]
s:719 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:72 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
s:72 [binder, in MetaCoq.Template.Induction]
s:720 [binder, in MetaCoq.Template.Typing]
s:720 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:723 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:73 [binder, in MetaCoq.PCUIC.PCUICArities]
s:73 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:731 [binder, in MetaCoq.Template.Universes]
s:736 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:74 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
s:741 [binder, in MetaCoq.Template.Universes]
s:741 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:748 [binder, in MetaCoq.Template.Universes]
s:749 [binder, in MetaCoq.Template.utils.wGraph]
s:75 [binder, in MetaCoq.Template.Typing]
s:75 [binder, in MetaCoq.Template.WfAst]
s:75 [binder, in MetaCoq.Erasure.EWellformed]
s:75 [binder, in MetaCoq.PCUIC.PCUICContexts]
s:751 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:752 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:756 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:761 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:764 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:765 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:766 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:769 [binder, in MetaCoq.PCUIC.PCUICSpine]
S:77 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
s:771 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:778 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:778 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:78 [binder, in MetaCoq.Erasure.ESubstitution]
s:78 [binder, in MetaCoq.PCUIC.PCUICArities]
s:784 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:787 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
S:789 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:79 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
s:79 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
s:79 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
S:792 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:794 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:795 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:8 [binder, in MetaCoq.Template.Normal]
s:80 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:800 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s:804 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:808 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:81 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:81 [binder, in MetaCoq.Erasure.ESubstitution]
s:81 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:81 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:81 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
s:811 [binder, in MetaCoq.PCUIC.PCUICSpine]
S:814 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:82 [binder, in MetaCoq.PCUIC.PCUICElimination]
S:82 [binder, in MetaCoq.Template.utils.MCRelations]
s:82 [binder, in MetaCoq.Template.TermEquality]
s:822 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:825 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:826 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
s:827 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:828 [binder, in MetaCoq.Template.utils.wGraph]
s:829 [binder, in MetaCoq.PCUIC.PCUICSR]
s:83 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
s:83 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:834 [binder, in MetaCoq.Template.utils.wGraph]
s:84 [binder, in MetaCoq.PCUIC.PCUICInversion]
s:84 [binder, in MetaCoq.Template.Environment]
s:841 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:842 [binder, in MetaCoq.PCUIC.PCUICTyping]
S:85 [binder, in MetaCoq.Template.utils.MCRelations]
s:854 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:857 [binder, in MetaCoq.Template.utils.wGraph]
s:866 [binder, in MetaCoq.Template.utils.wGraph]
s:87 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:875 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:88 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:883 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:888 [binder, in MetaCoq.Translations.MiniHoTT]
s:889 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:893 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:893 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:894 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:895 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:896 [binder, in MetaCoq.Translations.MiniHoTT_paths]
s:899 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
s:9 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:900 [binder, in MetaCoq.Template.utils.wGraph]
s:900 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:903 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:907 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:91 [binder, in MetaCoq.Erasure.ESubstitution]
s:91 [binder, in MetaCoq.Template.WfAst]
s:914 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:919 [binder, in MetaCoq.Template.utils.wGraph]
s:92 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:926 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:926 [binder, in MetaCoq.PCUIC.PCUICTyping]
s:927 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:927 [binder, in MetaCoq.Template.utils.wGraph]
s:93 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:939 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:94 [binder, in MetaCoq.PCUIC.PCUICSpine]
s:942 [binder, in MetaCoq.Template.Typing]
s:943 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
s:945 [binder, in MetaCoq.Template.utils.wGraph]
S:946 [binder, in MetaCoq.PCUIC.PCUICReduction]
s:95 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:95 [binder, in MetaCoq.Examples.tauto]
S:950 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:966 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:968 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:97 [binder, in MetaCoq.Template.EtaExpand]
s:97 [binder, in MetaCoq.Template.utils.wGraph]
s:970 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
s:978 [binder, in MetaCoq.PCUIC.PCUICConversion]
s:979 [binder, in MetaCoq.Template.utils.wGraph]
s:98 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
s:98 [binder, in MetaCoq.Examples.tauto]
s:983 [binder, in MetaCoq.Template.Typing]
s:983 [binder, in MetaCoq.Template.utils.wGraph]
s:984 [binder, in MetaCoq.PCUIC.PCUICConversion]
S:987 [binder, in MetaCoq.PCUIC.PCUICConfluence]
S:989 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:99 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
S:991 [binder, in MetaCoq.PCUIC.PCUICConfluence]
S:993 [binder, in MetaCoq.PCUIC.PCUICConfluence]
s:996 [binder, in MetaCoq.PCUIC.PCUICConversion]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75519 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (245 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61331 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6913 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (269 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (443 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (296 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |