| 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) |
K
kelim:319 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]kelim:620 [binder, in MetaCoq.Template.EnvironmentTyping]
kelim:75 [binder, in MetaCoq.Erasure.EPretty]
kelim:929 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Kername [module, in MetaCoq.Template.Kernames]
kername [definition, in MetaCoq.Template.Kernames]
KernameComp [module, in MetaCoq.Template.Kernames]
KernameComp.compare [definition, in MetaCoq.Template.Kernames]
KernameComp.compare_trans [lemma, in MetaCoq.Template.Kernames]
KernameComp.compare_sym [lemma, in MetaCoq.Template.Kernames]
KernameComp.eq [definition, in MetaCoq.Template.Kernames]
KernameComp.eq_equiv [lemma, in MetaCoq.Template.Kernames]
KernameComp.t [definition, in MetaCoq.Template.Kernames]
_ ?= _ [notation, in MetaCoq.Template.Kernames]
KernameMap [module, in MetaCoq.Template.Kernames]
KernameMapFact [module, in MetaCoq.Template.Kernames]
Kernames [library]
KernameSet [module, in MetaCoq.Template.Kernames]
KernameSetFact [module, in MetaCoq.Template.Kernames]
KernameSetProp [module, in MetaCoq.Template.Kernames]
kername_of_string [definition, in MetaCoq.Examples.typing_correctness]
kername_of_qualid [definition, in MetaCoq.Examples.demo]
kername_of_string [definition, in MetaCoq.Examples.metacoq_tour_prelude]
Kername.compare_eq [lemma, in MetaCoq.Template.Kernames]
Kername.compare_spec [definition, in MetaCoq.Template.Kernames]
Kername.eqb [definition, in MetaCoq.Template.Kernames]
Kername.eq_dec [definition, in MetaCoq.Template.Kernames]
Kername.lt [definition, in MetaCoq.Template.Kernames]
Kername.lt_compat [lemma, in MetaCoq.Template.Kernames]
Kername.lt_strorder [instance, in MetaCoq.Template.Kernames]
Kername.OT [module, in MetaCoq.Template.Kernames]
Kername.reflect_kername [instance, in MetaCoq.Template.Kernames]
keys:50 [binder, in MetaCoq.Template.utils.bytestring]
kind:166 [binder, in MetaCoq.Template.EtaExpand]
kind:185 [binder, in MetaCoq.Template.Ast]
kind:99 [binder, in MetaCoq.Template.EtaExpand]
knset_in_fold_left [lemma, in MetaCoq.Template.Kernames]
kn_fresh [projection, in MetaCoq.SafeChecker.PCUICWfEnv]
kn':11 [binder, in MetaCoq.Template.EnvMap]
kn':13 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn':15 [binder, in MetaCoq.Template.EnvMap]
kn':18 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn':29 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn':42 [binder, in MetaCoq.Template.Kernames]
kn':51 [binder, in MetaCoq.Translations.param_original]
kn':55 [binder, in MetaCoq.Translations.param_binary]
kn':55 [binder, in MetaCoq.Translations.param_original]
kn':56 [binder, in MetaCoq.Template.Kernames]
kn':59 [binder, in MetaCoq.Translations.param_binary]
kn':86 [binder, in MetaCoq.Translations.param_cheap_packed]
kn':886 [binder, in MetaCoq.Erasure.ErasureFunction]
kn':891 [binder, in MetaCoq.Erasure.ErasureFunction]
kn':895 [binder, in MetaCoq.Erasure.ErasureFunction]
kn':898 [binder, in MetaCoq.Erasure.ErasureFunction]
kn':904 [binder, in MetaCoq.Erasure.ErasureFunction]
kn':92 [binder, in MetaCoq.Translations.param_cheap_packed]
kn':95 [binder, in MetaCoq.Translations.times_bool_fun]
kn':99 [binder, in MetaCoq.Translations.times_bool_fun]
kn:10 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn:10 [binder, in MetaCoq.Template.EnvMap]
kn:1022 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:103 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
kn:1037 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:104 [binder, in MetaCoq.Erasure.Extract]
kn:1068 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
kn:108 [binder, in MetaCoq.Erasure.Extract]
kn:108 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
kn:11 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
kn:11 [binder, in MetaCoq.Erasure.EEnvMap]
kn:111 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
kn:112 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
kn:114 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
kn:116 [binder, in MetaCoq.Template.TypingWf]
kn:117 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:119 [binder, in MetaCoq.Erasure.ErasureProperties]
kn:124 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
kn:1260 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:13 [binder, in MetaCoq.Erasure.ErasureCorrectness]
kn:13 [binder, in MetaCoq.Template.Kernames]
kn:13 [binder, in MetaCoq.Erasure.EEnvMap]
kn:130 [binder, in MetaCoq.Erasure.EDeps]
kn:139 [binder, in MetaCoq.Erasure.ErasureProperties]
kn:14 [binder, in MetaCoq.Template.EnvMap]
kn:140 [binder, in MetaCoq.Translations.translation_utils]
kn:140 [binder, in MetaCoq.Erasure.ErasureProperties]
kn:141 [binder, in MetaCoq.Erasure.ErasureProperties]
kn:1425 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:1442 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:1455 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:146 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
kn:146 [binder, in MetaCoq.Erasure.EWellformed]
kn:147 [binder, in MetaCoq.Erasure.EDeps]
kn:148 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
kn:1484 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:15 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn:151 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:152 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
kn:156 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:156 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
kn:158 [binder, in MetaCoq.Erasure.ERemoveParams]
kn:16 [binder, in MetaCoq.Erasure.ESpineView]
kn:160 [binder, in MetaCoq.Erasure.ERemoveParams]
kn:161 [binder, in MetaCoq.Erasure.EEtaExpanded]
kn:167 [binder, in MetaCoq.Template.Environment]
kn:168 [binder, in MetaCoq.Template.TypingWf]
kn:169 [binder, in MetaCoq.Erasure.EInlineProjections]
kn:17 [binder, in MetaCoq.Erasure.EEnvMap]
kn:171 [binder, in MetaCoq.Template.Environment]
kn:173 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:174 [binder, in MetaCoq.Erasure.Extract]
kn:175 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:179 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:179 [binder, in MetaCoq.Erasure.Extract]
kn:180 [binder, in MetaCoq.Erasure.EEtaExpanded]
kn:182 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:182 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
kn:19 [binder, in MetaCoq.Erasure.ErasureCorrectness]
kn:19 [binder, in MetaCoq.Erasure.EEnvMap]
kn:199 [binder, in MetaCoq.Erasure.Extract]
kn:212 [binder, in MetaCoq.Template.TypingWf]
kn:220 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:23 [binder, in MetaCoq.Template.EnvironmentTyping]
kn:23 [binder, in MetaCoq.Erasure.EEnvMap]
kn:232 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:25 [binder, in MetaCoq.Erasure.EEnvMap]
kn:25 [binder, in MetaCoq.Erasure.EExtends]
kn:26 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:26 [binder, in MetaCoq.Erasure.EGenericMapEnv]
kn:27 [binder, in MetaCoq.Template.EnvMap]
kn:31 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:31 [binder, in MetaCoq.Erasure.EGenericMapEnv]
kn:32 [binder, in MetaCoq.Erasure.EEnvMap]
kn:33 [binder, in MetaCoq.Erasure.EGenericMapEnv]
kn:34 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:34 [binder, in MetaCoq.Template.EnvironmentTyping]
kn:34 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:34 [binder, in MetaCoq.Examples.demo]
kn:341 [binder, in MetaCoq.Erasure.EWcbvEval]
kn:35 [binder, in MetaCoq.Erasure.EGenericMapEnv]
kn:366 [binder, in MetaCoq.PCUIC.PCUICNormal]
kn:37 [binder, in MetaCoq.Template.EnvironmentTyping]
kn:37 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:37 [binder, in MetaCoq.Erasure.EExtends]
kn:38 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
kn:4 [binder, in MetaCoq.Erasure.EInlineProjections]
kn:4 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
kn:40 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:40 [binder, in MetaCoq.Examples.demo]
kn:40 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
kn:406 [binder, in MetaCoq.Erasure.ERemoveParams]
kn:408 [binder, in MetaCoq.Erasure.EWcbvEval]
kn:41 [binder, in MetaCoq.Erasure.Extract]
kn:41 [binder, in MetaCoq.Template.Kernames]
kn:41 [binder, in MetaCoq.Erasure.EEnvMap]
kn:412 [binder, in MetaCoq.Template.Checker]
kn:415 [binder, in MetaCoq.Erasure.EWcbvEval]
kn:42 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:426 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
kn:43 [binder, in MetaCoq.Erasure.Extract]
kn:43 [binder, in MetaCoq.Erasure.EEnvMap]
kn:446 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
kn:448 [binder, in MetaCoq.Erasure.EWcbvEval]
kn:46 [binder, in MetaCoq.Erasure.EEnvMap]
kn:47 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
kn:48 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:481 [binder, in MetaCoq.Template.EtaExpand]
kn:485 [binder, in MetaCoq.Template.EtaExpand]
kn:489 [binder, in MetaCoq.Template.EtaExpand]
kn:49 [binder, in MetaCoq.Translations.param_original]
kn:492 [binder, in MetaCoq.Template.EtaExpand]
kn:494 [binder, in MetaCoq.Template.EtaExpand]
kn:5 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
kn:509 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
kn:53 [binder, in MetaCoq.Translations.param_binary]
kn:53 [binder, in MetaCoq.Erasure.EEnvMap]
kn:542 [binder, in MetaCoq.Template.EtaExpand]
kn:55 [binder, in MetaCoq.Template.Kernames]
kn:56 [binder, in MetaCoq.Erasure.EWellformed]
kn:57 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
kn:59 [binder, in MetaCoq.Template.Kernames]
kn:61 [binder, in MetaCoq.Template.Kernames]
kn:61 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:61 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
kn:62 [binder, in MetaCoq.Erasure.EEnvMap]
kn:64 [binder, in MetaCoq.Template.EnvMap]
kn:657 [binder, in MetaCoq.Template.EnvironmentTyping]
kn:667 [binder, in MetaCoq.Template.EnvironmentTyping]
kn:67 [binder, in MetaCoq.Erasure.EPretty]
kn:69 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:693 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:7 [binder, in MetaCoq.Template.TypingWf]
kn:70 [binder, in MetaCoq.Erasure.EInlineProjections]
kn:75 [binder, in MetaCoq.Erasure.EInlineProjections]
kn:78 [binder, in MetaCoq.Erasure.EInlineProjections]
kn:79 [binder, in MetaCoq.Translations.param_cheap_packed]
kn:8 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
kn:8 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
kn:81 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:81 [binder, in MetaCoq.Translations.param_binary]
kn:81 [binder, in MetaCoq.Erasure.EDeps]
kn:81 [binder, in MetaCoq.Erasure.EInlineProjections]
kn:826 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:83 [binder, in MetaCoq.Erasure.EPretty]
kn:835 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:84 [binder, in MetaCoq.Translations.param_original]
kn:850 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:863 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:87 [binder, in MetaCoq.Erasure.EGenericMapEnv]
kn:877 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:879 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:88 [binder, in MetaCoq.Erasure.EGlobalEnv]
kn:885 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:888 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:890 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:894 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:897 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:9 [binder, in MetaCoq.Erasure.EEnvMap]
kn:90 [binder, in MetaCoq.Translations.times_bool_fun]
kn:903 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:95 [binder, in MetaCoq.Translations.translation_utils]
kn:973 [binder, in MetaCoq.Erasure.ErasureFunction]
kn:999 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
kproj [definition, in MetaCoq.Translations.standard_model]
k':10 [binder, in MetaCoq.PCUIC.PCUICCSubst]
k':10 [binder, in MetaCoq.Erasure.ELiftSubst]
k':10 [binder, in MetaCoq.Template.WcbvEval]
k':10 [binder, in MetaCoq.Erasure.ECSubst]
k':101 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
k':105 [binder, in MetaCoq.PCUIC.PCUICContexts]
k':107 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':111 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k':115 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':12 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k':1205 [binder, in MetaCoq.PCUIC.PCUICConversion]
k':121 [binder, in MetaCoq.Template.LiftSubst]
k':129 [binder, in MetaCoq.Template.LiftSubst]
k':1325 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k':140 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':149 [binder, in MetaCoq.Template.utils.MCList]
k':151 [binder, in MetaCoq.Erasure.ELiftSubst]
k':153 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':156 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':16 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k':16 [binder, in MetaCoq.Erasure.EReflect]
k':164 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':168 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':171 [binder, in MetaCoq.PCUIC.PCUICAst]
k':173 [binder, in MetaCoq.PCUIC.PCUICAst]
k':176 [binder, in MetaCoq.Erasure.ELiftSubst]
k':180 [binder, in MetaCoq.Erasure.ELiftSubst]
k':182 [binder, in MetaCoq.PCUIC.PCUICAst]
k':183 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':184 [binder, in MetaCoq.PCUIC.PCUICAst]
k':186 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k':186 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k':19 [binder, in MetaCoq.Template.Kernames]
k':19 [binder, in MetaCoq.Erasure.ELiftSubst]
k':190 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':192 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k':195 [binder, in MetaCoq.PCUIC.PCUICAst]
k':196 [binder, in MetaCoq.PCUIC.PCUICAst]
k':197 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':199 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k':204 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k':204 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':208 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k':208 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':208 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':21 [binder, in MetaCoq.Erasure.ELiftSubst]
k':212 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k':215 [binder, in MetaCoq.PCUIC.PCUICAst]
k':216 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k':219 [binder, in MetaCoq.PCUIC.PCUICAst]
k':220 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k':220 [binder, in MetaCoq.PCUIC.PCUICAst]
k':225 [binder, in MetaCoq.Template.Ast]
k':228 [binder, in MetaCoq.Template.Ast]
k':230 [binder, in MetaCoq.Template.Ast]
k':233 [binder, in MetaCoq.PCUIC.PCUICInductives]
k':237 [binder, in MetaCoq.Template.Ast]
k':239 [binder, in MetaCoq.PCUIC.PCUICInductives]
k':240 [binder, in MetaCoq.Template.Ast]
k':242 [binder, in MetaCoq.Template.BasicAst]
k':242 [binder, in MetaCoq.Template.Ast]
k':243 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':246 [binder, in MetaCoq.Template.BasicAst]
k':247 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':250 [binder, in MetaCoq.PCUIC.PCUICInductives]
k':251 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k':251 [binder, in MetaCoq.Template.Ast]
k':254 [binder, in MetaCoq.Template.Ast]
k':255 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k':255 [binder, in MetaCoq.Template.Ast]
k':26 [binder, in MetaCoq.Template.Environment]
k':261 [binder, in MetaCoq.Template.Ast]
k':265 [binder, in MetaCoq.Template.Ast]
k':266 [binder, in MetaCoq.Template.Ast]
k':27 [binder, in MetaCoq.PCUIC.PCUICAst]
k':280 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':29 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k':29 [binder, in MetaCoq.Erasure.EWellformed]
k':297 [binder, in MetaCoq.PCUIC.PCUICAst]
k':30 [binder, in MetaCoq.Template.Environment]
k':32 [binder, in MetaCoq.Erasure.ELiftSubst]
k':33 [binder, in MetaCoq.Erasure.ELiftSubst]
k':33 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k':339 [binder, in MetaCoq.PCUIC.PCUICAst]
k':361 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k':364 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k':369 [binder, in MetaCoq.PCUIC.PCUICAst]
k':375 [binder, in MetaCoq.PCUIC.PCUICAst]
k':38 [binder, in MetaCoq.Template.Environment]
k':406 [binder, in MetaCoq.Template.EtaExpand]
k':417 [binder, in MetaCoq.PCUIC.PCUICAst]
k':44 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
k':459 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k':464 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k':49 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':50 [binder, in MetaCoq.Template.Environment]
k':504 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k':510 [binder, in MetaCoq.PCUIC.PCUICAst]
k':513 [binder, in MetaCoq.Template.Typing]
k':519 [binder, in MetaCoq.PCUIC.PCUICAst]
k':52 [binder, in MetaCoq.Template.EnvMap]
k':523 [binder, in MetaCoq.Template.Typing]
k':526 [binder, in MetaCoq.PCUIC.PCUICAst]
k':53 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':532 [binder, in MetaCoq.Template.utils.All_Forall]
k':537 [binder, in MetaCoq.Template.utils.All_Forall]
k':549 [binder, in MetaCoq.Template.Typing]
k':559 [binder, in MetaCoq.Template.Typing]
k':582 [binder, in MetaCoq.PCUIC.PCUICAst]
k':59 [binder, in MetaCoq.Template.Environment]
k':596 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k':6 [binder, in MetaCoq.Template.WcbvEval]
k':6 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':60 [binder, in MetaCoq.Template.EnvMap]
k':60 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':604 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k':63 [binder, in MetaCoq.Template.Ast]
k':639 [binder, in MetaCoq.PCUIC.PCUICSpine]
k':64 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':644 [binder, in MetaCoq.PCUIC.PCUICSpine]
k':66 [binder, in MetaCoq.Erasure.EWellformed]
k':673 [binder, in MetaCoq.PCUIC.PCUICSpine]
k':68 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':69 [binder, in MetaCoq.Erasure.EWellformed]
k':73 [binder, in MetaCoq.Erasure.EWellformed]
k':73 [binder, in MetaCoq.Translations.param_cheap_packed]
k':74 [binder, in MetaCoq.Template.TypingWf]
k':75 [binder, in MetaCoq.Translations.param_cheap_packed]
k':76 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k':8 [binder, in MetaCoq.PCUIC.PCUICCSubst]
k':8 [binder, in MetaCoq.Erasure.ELiftSubst]
k':8 [binder, in MetaCoq.Template.WcbvEval]
k':8 [binder, in MetaCoq.Erasure.ECSubst]
k':915 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k':96 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:1 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:1 [binder, in MetaCoq.Template.LiftSubst]
k:100 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
k:100 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:100 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:100 [binder, in MetaCoq.Template.Environment]
k:100 [binder, in MetaCoq.Template.LiftSubst]
k:1000 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:1007 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:101 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:101 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:101 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:102 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:1022 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:103 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:103 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:104 [binder, in MetaCoq.Erasure.ESubstitution]
k:104 [binder, in MetaCoq.PCUIC.PCUICElimination]
k:104 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:104 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:105 [binder, in MetaCoq.Erasure.ELiftSubst]
k:105 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:106 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:106 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:106 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:107 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:108 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
k:108 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:108 [binder, in MetaCoq.PCUIC.PCUICAst]
k:108 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:108 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:109 [binder, in MetaCoq.Erasure.Extract]
k:109 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:11 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
k:11 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:11 [binder, in MetaCoq.Erasure.EReflect]
k:110 [binder, in MetaCoq.PCUIC.PCUICAlpha]
k:111 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
k:111 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:111 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:112 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:112 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:112 [binder, in MetaCoq.Erasure.ELiftSubst]
k:112 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1120 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:113 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:1134 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:114 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:114 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:114 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:114 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:114 [binder, in MetaCoq.Erasure.ERemoveParams]
k:115 [binder, in MetaCoq.Erasure.ELiftSubst]
k:115 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:115 [binder, in MetaCoq.Template.LiftSubst]
k:1164 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:1166 [binder, in MetaCoq.Template.utils.wGraph]
k:117 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:117 [binder, in MetaCoq.Template.LiftSubst]
k:1172 [binder, in MetaCoq.Translations.MiniHoTT]
k:1179 [binder, in MetaCoq.Template.utils.wGraph]
k:118 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:118 [binder, in MetaCoq.Erasure.EInlineProjections]
k:118 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:118 [binder, in MetaCoq.Erasure.ERemoveParams]
k:1180 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:1183 [binder, in MetaCoq.Translations.MiniHoTT]
k:119 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:119 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:119 [binder, in MetaCoq.Template.LiftSubst]
k:1191 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:12 [binder, in MetaCoq.Template.WfAst]
k:12 [binder, in MetaCoq.Erasure.EDeps]
k:12 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
k:12 [binder, in MetaCoq.Template.LiftSubst]
k:120 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:120 [binder, in MetaCoq.Erasure.ELiftSubst]
k:1203 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:1205 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:121 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:122 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:122 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:123 [binder, in MetaCoq.Template.LiftSubst]
k:124 [binder, in MetaCoq.Erasure.EInlineProjections]
k:124 [binder, in MetaCoq.Erasure.ELiftSubst]
k:1241 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:125 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
k:125 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
k:125 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:125 [binder, in MetaCoq.PCUIC.PCUICSR]
k:126 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:126 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:126 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1265 [binder, in MetaCoq.PCUIC.PCUICConfluence]
k:127 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:1274 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:1275 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:1276 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:1276 [binder, in MetaCoq.PCUIC.PCUICConfluence]
k:1277 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:128 [binder, in MetaCoq.Template.WfAst]
k:128 [binder, in MetaCoq.Erasure.ELiftSubst]
k:128 [binder, in MetaCoq.Erasure.ERemoveParams]
k:128 [binder, in MetaCoq.Template.LiftSubst]
k:129 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:129 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:129 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:129 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
k:1297 [binder, in MetaCoq.Template.utils.All_Forall]
k:13 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:13 [binder, in MetaCoq.PCUIC.PCUICCSubst]
k:13 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:13 [binder, in MetaCoq.Erasure.ELiftSubst]
k:130 [binder, in MetaCoq.Erasure.ELiftSubst]
k:130 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
k:130 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:130 [binder, in MetaCoq.Template.TypingWf]
k:131 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:132 [binder, in MetaCoq.Template.WfAst]
k:1324 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:133 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:133 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:133 [binder, in MetaCoq.Erasure.EEtaExpanded]
k:133 [binder, in MetaCoq.Template.LiftSubst]
k:134 [binder, in MetaCoq.Erasure.ELiftSubst]
k:134 [binder, in MetaCoq.PCUIC.PCUICSR]
k:134 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1346 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:135 [binder, in MetaCoq.Template.WfAst]
k:135 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:136 [binder, in MetaCoq.Erasure.EDeps]
k:136 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:136 [binder, in MetaCoq.Template.Ast]
k:136 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:1361 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:137 [binder, in MetaCoq.Template.WfAst]
k:137 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
k:1376 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:1377 [binder, in MetaCoq.Template.utils.All_Forall]
k:138 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:138 [binder, in MetaCoq.Template.LiftSubst]
k:139 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:139 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:14 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:14 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
k:14 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:140 [binder, in MetaCoq.Template.WfAst]
k:140 [binder, in MetaCoq.Erasure.EDeps]
k:140 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:141 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:142 [binder, in MetaCoq.PCUIC.PCUICSR]
k:142 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:143 [binder, in MetaCoq.Template.TypingWf]
k:143 [binder, in MetaCoq.Template.LiftSubst]
k:144 [binder, in MetaCoq.Template.WfAst]
k:144 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:144 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
k:144 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:144 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:145 [binder, in MetaCoq.Erasure.ELiftSubst]
k:146 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:146 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:146 [binder, in MetaCoq.Translations.param_cheap_packed]
k:146 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:146 [binder, in MetaCoq.Template.LiftSubst]
k:147 [binder, in MetaCoq.Erasure.ELiftSubst]
k:147 [binder, in MetaCoq.Template.TypingWf]
k:148 [binder, in MetaCoq.Template.utils.MCList]
k:148 [binder, in MetaCoq.Erasure.EDeps]
k:148 [binder, in MetaCoq.Translations.param_cheap_packed]
k:149 [binder, in MetaCoq.Erasure.ELiftSubst]
k:15 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:15 [binder, in MetaCoq.Template.utils.wGraph]
k:15 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:150 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:150 [binder, in MetaCoq.Template.Ast]
k:150 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:150 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:150 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1502 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:151 [binder, in MetaCoq.Template.TypingWf]
k:151 [binder, in MetaCoq.Template.LiftSubst]
k:1511 [binder, in MetaCoq.Translations.MiniHoTT]
k:1519 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:152 [binder, in MetaCoq.Erasure.ELiftSubst]
k:152 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:152 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1523 [binder, in MetaCoq.Translations.MiniHoTT]
k:153 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:153 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:1531 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:154 [binder, in MetaCoq.Template.Ast]
k:154 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:155 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:155 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:155 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:156 [binder, in MetaCoq.Template.utils.MCList]
k:156 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:157 [binder, in MetaCoq.Erasure.ELiftSubst]
k:158 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:158 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:158 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:159 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:159 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:159 [binder, in MetaCoq.Template.LiftSubst]
k:16 [binder, in MetaCoq.Template.Kernames]
k:16 [binder, in MetaCoq.PCUIC.PCUICCSubst]
k:16 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
k:160 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:160 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:161 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:161 [binder, in MetaCoq.Erasure.ELiftSubst]
k:162 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:163 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:163 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:165 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:165 [binder, in MetaCoq.PCUIC.PCUICAst]
k:165 [binder, in MetaCoq.Erasure.ELiftSubst]
k:166 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:166 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1666 [binder, in MetaCoq.Translations.MiniHoTT]
k:167 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
k:1672 [binder, in MetaCoq.Translations.MiniHoTT]
k:1674 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:168 [binder, in MetaCoq.Template.utils.MCList]
k:168 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:168 [binder, in MetaCoq.Erasure.EEtaExpanded]
k:1680 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:169 [binder, in MetaCoq.Erasure.ELiftSubst]
k:17 [binder, in MetaCoq.Erasure.EDeps]
k:17 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:17 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:17 [binder, in MetaCoq.Erasure.ECSubst]
k:170 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
k:170 [binder, in MetaCoq.Template.utils.MCList]
k:170 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:170 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:170 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:171 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:171 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:171 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:172 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:172 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:172 [binder, in MetaCoq.Erasure.ELiftSubst]
k:174 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:174 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:174 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:175 [binder, in MetaCoq.Template.Universes]
k:175 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:175 [binder, in MetaCoq.Erasure.ELiftSubst]
k:175 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:176 [binder, in MetaCoq.PCUIC.PCUICAst]
k:177 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:177 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:178 [binder, in MetaCoq.Template.utils.MCList]
k:178 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:178 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:179 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:179 [binder, in MetaCoq.Erasure.ELiftSubst]
k:179 [binder, in MetaCoq.PCUIC.PCUICSR]
k:179 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:179 [binder, in MetaCoq.Template.LiftSubst]
k:18 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
k:18 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:18 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
k:180 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
k:180 [binder, in MetaCoq.Examples.tauto]
k:181 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:181 [binder, in MetaCoq.Template.monad_utils]
k:181 [binder, in MetaCoq.PCUIC.PCUICSR]
k:181 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:182 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:182 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:183 [binder, in MetaCoq.Template.Universes]
k:183 [binder, in MetaCoq.Erasure.ELiftSubst]
k:183 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:184 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:185 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:185 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:186 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:187 [binder, in MetaCoq.Template.Universes]
k:187 [binder, in MetaCoq.PCUIC.PCUICAst]
k:187 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:188 [binder, in MetaCoq.Examples.tauto]
k:189 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:189 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
k:189 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:189 [binder, in MetaCoq.PCUIC.PCUICAst]
k:189 [binder, in MetaCoq.Examples.tauto]
k:19 [binder, in MetaCoq.Template.LiftSubst]
k:190 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:190 [binder, in MetaCoq.Examples.tauto]
k:190 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:191 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:192 [binder, in MetaCoq.Examples.tauto]
k:193 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:193 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:194 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:195 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:195 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:196 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:197 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:198 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:199 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:199 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:2 [binder, in MetaCoq.PCUIC.PCUICCSubst]
k:2 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:2 [binder, in MetaCoq.Erasure.ELiftSubst]
k:2 [binder, in MetaCoq.Template.EnvMap]
k:2 [binder, in MetaCoq.Template.WcbvEval]
k:2 [binder, in MetaCoq.Translations.standard_model]
k:2 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:2 [binder, in MetaCoq.Erasure.ECSubst]
k:20 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:201 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:202 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:202 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:203 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:204 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:204 [binder, in MetaCoq.Template.Environment]
k:206 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:206 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:206 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:206 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:207 [binder, in MetaCoq.PCUIC.PCUICArities]
k:207 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:209 [binder, in MetaCoq.Template.BasicAst]
k:21 [binder, in MetaCoq.Template.Environment]
k:21 [binder, in MetaCoq.Template.UnivSubst]
k:21 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:210 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:210 [binder, in MetaCoq.PCUIC.PCUICAst]
k:210 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:211 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:214 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:214 [binder, in MetaCoq.Template.Typing]
k:214 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
k:215 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:216 [binder, in MetaCoq.Template.utils.MCList]
k:217 [binder, in MetaCoq.PCUIC.PCUICAst]
k:2179 [binder, in MetaCoq.Template.utils.All_Forall]
k:218 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:218 [binder, in MetaCoq.Template.Typing]
k:218 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:218 [binder, in MetaCoq.Template.Environment]
k:2188 [binder, in MetaCoq.Template.utils.All_Forall]
k:219 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:22 [binder, in MetaCoq.Erasure.EDeps]
k:22 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
k:22 [binder, in MetaCoq.Erasure.ECSubst]
k:22 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
k:22 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
k:220 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:221 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:221 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:221 [binder, in MetaCoq.Template.Ast]
k:222 [binder, in MetaCoq.Template.BasicAst]
k:222 [binder, in MetaCoq.Template.Typing]
k:222 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:224 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:225 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:227 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:228 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:228 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:229 [binder, in MetaCoq.PCUIC.PCUICAst]
k:23 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:23 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:23 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
k:23 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:23 [binder, in MetaCoq.Template.LiftSubst]
k:230 [binder, in MetaCoq.Template.Environment]
k:232 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:232 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:232 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:233 [binder, in MetaCoq.Template.Ast]
k:233 [binder, in MetaCoq.Template.Environment]
k:235 [binder, in MetaCoq.Template.TypingWf]
k:2355 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:2356 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:2357 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:2358 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
k:237 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:238 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:238 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:24 [binder, in MetaCoq.Template.EtaExpand]
k:24 [binder, in MetaCoq.Erasure.EInlineProjections]
k:24 [binder, in MetaCoq.Erasure.ELiftSubst]
k:24 [binder, in MetaCoq.Template.Environment]
k:24 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:24 [binder, in MetaCoq.Template.UnivSubst]
k:240 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:242 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:242 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:245 [binder, in MetaCoq.Template.Ast]
k:246 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:246 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:247 [binder, in MetaCoq.Template.Ast]
k:249 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:25 [binder, in MetaCoq.Template.TermEquality]
k:25 [binder, in MetaCoq.Erasure.ECSubst]
k:25 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
k:250 [binder, in MetaCoq.Template.BasicAst]
k:2501 [binder, in MetaCoq.Translations.MiniHoTT]
k:2509 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:251 [binder, in MetaCoq.Template.BasicAst]
k:253 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:256 [binder, in MetaCoq.Template.Ast]
k:2570 [binder, in MetaCoq.Translations.MiniHoTT]
k:2575 [binder, in MetaCoq.Translations.MiniHoTT]
k:2578 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:258 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:2583 [binder, in MetaCoq.Translations.MiniHoTT_paths]
k:259 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:26 [binder, in MetaCoq.Template.WfAst]
k:26 [binder, in MetaCoq.Erasure.EInlineProjections]
k:26 [binder, in MetaCoq.PCUIC.PCUICAst]
k:26 [binder, in MetaCoq.Erasure.EWellformed]
k:26 [binder, in MetaCoq.Erasure.ELiftSubst]
k:26 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
k:26 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:261 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:261 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:262 [binder, in MetaCoq.Template.BasicAst]
k:263 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:263 [binder, in MetaCoq.Template.Ast]
k:265 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:266 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:268 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:268 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:269 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:27 [binder, in MetaCoq.Erasure.EDeps]
k:27 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:27 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
k:27 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:27 [binder, in MetaCoq.Erasure.EEtaExpanded]
k:271 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:272 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:273 [binder, in MetaCoq.Template.Environment]
k:274 [binder, in MetaCoq.PCUIC.PCUICAst]
k:275 [binder, in MetaCoq.Template.Ast]
k:276 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:276 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:276 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:278 [binder, in MetaCoq.Template.Environment]
k:278 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:28 [binder, in MetaCoq.Template.Environment]
k:28 [binder, in MetaCoq.Erasure.ECSubst]
k:28 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
k:281 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:283 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:284 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:285 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:287 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:29 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
k:29 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:290 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:291 [binder, in MetaCoq.PCUIC.PCUICConfluence]
k:292 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:294 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:296 [binder, in MetaCoq.PCUIC.PCUICAst]
k:296 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:298 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:299 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:299 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:299 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:30 [binder, in MetaCoq.Template.EnvironmentTyping]
k:30 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:30 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:30 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
k:301 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:301 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:302 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:302 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:302 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:303 [binder, in MetaCoq.Template.utils.MCList]
k:303 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:304 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:305 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:307 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:307 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:308 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:308 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:308 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:31 [binder, in MetaCoq.Template.WfAst]
k:31 [binder, in MetaCoq.PCUIC.PCUICAst]
k:31 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
k:31 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
k:310 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:310 [binder, in MetaCoq.Template.Environment]
k:311 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:313 [binder, in MetaCoq.Template.Environment]
k:314 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:314 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:315 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:316 [binder, in MetaCoq.Template.utils.MCList]
k:317 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:318 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:32 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:32 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:32 [binder, in MetaCoq.Erasure.ECSubst]
k:320 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:321 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:324 [binder, in MetaCoq.Template.utils.MCList]
k:324 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:325 [binder, in MetaCoq.Template.utils.MCList]
k:325 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:326 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:326 [binder, in MetaCoq.PCUIC.PCUICAst]
k:327 [binder, in MetaCoq.Erasure.EWcbvEval]
k:329 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:33 [binder, in MetaCoq.PCUIC.PCUICAst]
k:33 [binder, in MetaCoq.Erasure.EWellformed]
k:33 [binder, in MetaCoq.Template.Environment]
k:33 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
k:330 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
k:330 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
k:331 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:331 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:334 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:336 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:338 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
k:338 [binder, in MetaCoq.PCUIC.PCUICAst]
k:338 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:34 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:34 [binder, in MetaCoq.Erasure.ELiftSubst]
k:34 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
k:34 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
k:340 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:341 [binder, in MetaCoq.Template.common.uGraph]
k:343 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:344 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:345 [binder, in MetaCoq.Template.utils.MCList]
k:345 [binder, in MetaCoq.Template.common.uGraph]
k:346 [binder, in MetaCoq.Template.utils.MCList]
k:346 [binder, in MetaCoq.PCUIC.PCUICAst]
k:347 [binder, in MetaCoq.Template.EtaExpand]
k:348 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:348 [binder, in MetaCoq.PCUIC.PCUICAst]
k:35 [binder, in MetaCoq.PCUIC.PCUICAst]
k:35 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
k:35 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:35 [binder, in MetaCoq.Template.LiftSubst]
k:350 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:351 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:352 [binder, in MetaCoq.Template.utils.MCList]
k:352 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:352 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:353 [binder, in MetaCoq.PCUIC.PCUICAst]
k:355 [binder, in MetaCoq.PCUIC.PCUICAst]
k:357 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:358 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:359 [binder, in MetaCoq.Template.BasicAst]
k:359 [binder, in MetaCoq.Template.utils.MCList]
k:36 [binder, in MetaCoq.Erasure.ESubstitution]
k:36 [binder, in MetaCoq.Template.Environment]
k:36 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:36 [binder, in MetaCoq.Erasure.ECSubst]
k:360 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:365 [binder, in MetaCoq.Template.utils.MCList]
k:365 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:367 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:367 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
k:368 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:368 [binder, in MetaCoq.PCUIC.PCUICAst]
k:369 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:37 [binder, in MetaCoq.PCUIC.PCUICAst]
k:37 [binder, in MetaCoq.Erasure.ELiftSubst]
k:37 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:37 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
k:371 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
k:373 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:374 [binder, in MetaCoq.PCUIC.PCUICAst]
k:375 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:375 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
k:377 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:38 [binder, in MetaCoq.Erasure.ESubstitution]
k:38 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:38 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:38 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
k:380 [binder, in MetaCoq.PCUIC.PCUICAst]
k:382 [binder, in MetaCoq.Template.utils.wGraph]
k:382 [binder, in MetaCoq.PCUIC.PCUICAst]
K:383 [binder, in MetaCoq.Template.common.uGraph]
k:384 [binder, in MetaCoq.Erasure.ERemoveParams]
k:385 [binder, in MetaCoq.PCUIC.PCUICAst]
K:386 [binder, in MetaCoq.Template.common.uGraph]
k:387 [binder, in MetaCoq.PCUIC.PCUICAst]
k:39 [binder, in MetaCoq.PCUIC.PCUICAst]
k:39 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:39 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
K:390 [binder, in MetaCoq.Template.common.uGraph]
k:391 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:392 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
K:393 [binder, in MetaCoq.Template.common.uGraph]
k:394 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:396 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:398 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:4 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:4 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:4 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:4 [binder, in MetaCoq.Template.EnvMap]
k:4 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:4 [binder, in MetaCoq.Template.LiftSubst]
k:40 [binder, in MetaCoq.Template.Environment]
k:40 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:40 [binder, in MetaCoq.Erasure.ECSubst]
k:40 [binder, in MetaCoq.Template.LiftSubst]
k:400 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:401 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:403 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
k:404 [binder, in MetaCoq.Template.EtaExpand]
k:404 [binder, in MetaCoq.Template.Typing]
k:405 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:406 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:409 [binder, in MetaCoq.Template.Typing]
k:41 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:41 [binder, in MetaCoq.Erasure.EWellformed]
k:41 [binder, in MetaCoq.Erasure.ELiftSubst]
k:411 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:412 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:414 [binder, in MetaCoq.Template.Typing]
k:414 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:416 [binder, in MetaCoq.PCUIC.PCUICAst]
k:419 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:42 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:42 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
k:420 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:425 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:425 [binder, in MetaCoq.PCUIC.PCUICAst]
k:429 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:43 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:43 [binder, in MetaCoq.Erasure.ECSubst]
k:43 [binder, in MetaCoq.Translations.param_original]
k:430 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:433 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
k:434 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:435 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:436 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:436 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:438 [binder, in MetaCoq.Template.utils.MCList]
k:44 [binder, in MetaCoq.Template.WfAst]
k:44 [binder, in MetaCoq.Erasure.Extract]
k:44 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:44 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:44 [binder, in MetaCoq.Translations.param_original]
k:44 [binder, in MetaCoq.Template.LiftSubst]
k:442 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:442 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:442 [binder, in MetaCoq.PCUIC.PCUICAst]
k:45 [binder, in MetaCoq.Erasure.ELiftSubst]
k:451 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
k:453 [binder, in MetaCoq.PCUIC.PCUICAst]
k:458 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:459 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:46 [binder, in MetaCoq.PCUIC.PCUICAst]
k:46 [binder, in MetaCoq.Template.EnvMap]
k:46 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:46 [binder, in MetaCoq.Erasure.ECSubst]
k:465 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:47 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:47 [binder, in MetaCoq.Template.WfAst]
k:47 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:47 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
k:47 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:473 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:476 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:477 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:479 [binder, in MetaCoq.Template.EnvironmentTyping]
k:479 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:48 [binder, in MetaCoq.Erasure.ELiftSubst]
k:48 [binder, in MetaCoq.Template.EnvMap]
k:48 [binder, in MetaCoq.Template.Environment]
k:48 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:48 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:481 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:482 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:483 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:484 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:486 [binder, in MetaCoq.PCUIC.PCUICNormal]
k:486 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:489 [binder, in MetaCoq.PCUIC.PCUICAst]
k:49 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:492 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:495 [binder, in MetaCoq.PCUIC.PCUICAst]
k:498 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:499 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:499 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:50 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:50 [binder, in MetaCoq.PCUIC.PCUICAst]
k:50 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:50 [binder, in MetaCoq.Template.LiftSubst]
k:500 [binder, in MetaCoq.Template.utils.All_Forall]
k:500 [binder, in MetaCoq.PCUIC.PCUICAst]
k:502 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:503 [binder, in MetaCoq.PCUIC.PCUICAst]
k:504 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:506 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:507 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:509 [binder, in MetaCoq.PCUIC.PCUICAst]
k:51 [binder, in MetaCoq.Template.EnvMap]
k:51 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
k:510 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:510 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:511 [binder, in MetaCoq.Template.utils.All_Forall]
k:512 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:514 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:514 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:517 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:518 [binder, in MetaCoq.PCUIC.PCUICAst]
k:519 [binder, in MetaCoq.Template.utils.All_Forall]
k:519 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:52 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:52 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:522 [binder, in MetaCoq.Template.Typing]
k:522 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:525 [binder, in MetaCoq.Template.utils.All_Forall]
k:525 [binder, in MetaCoq.PCUIC.PCUICAst]
k:527 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:529 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:529 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:53 [binder, in MetaCoq.Template.Environment]
k:530 [binder, in MetaCoq.Template.utils.All_Forall]
k:531 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:531 [binder, in MetaCoq.PCUIC.PCUICAst]
k:532 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:533 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:534 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:535 [binder, in MetaCoq.Template.utils.All_Forall]
k:536 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:54 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
k:540 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:542 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:545 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:548 [binder, in MetaCoq.PCUIC.PCUICAst]
k:55 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:55 [binder, in MetaCoq.PCUIC.PCUICSR]
k:55 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:550 [binder, in MetaCoq.Template.utils.All_Forall]
k:550 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:553 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:554 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:554 [binder, in MetaCoq.PCUIC.PCUICAst]
k:556 [binder, in MetaCoq.Template.utils.All_Forall]
k:558 [binder, in MetaCoq.Template.Typing]
k:56 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:56 [binder, in MetaCoq.Template.EnvMap]
k:562 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:563 [binder, in MetaCoq.Template.utils.All_Forall]
k:564 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:565 [binder, in MetaCoq.Template.utils.All_Forall]
k:565 [binder, in MetaCoq.Template.utils.MCList]
k:566 [binder, in MetaCoq.Template.utils.wGraph]
k:568 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:57 [binder, in MetaCoq.PCUIC.PCUICValidity]
k:57 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:57 [binder, in MetaCoq.Template.Environment]
k:57 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:570 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:572 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:574 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:576 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:576 [binder, in MetaCoq.PCUIC.PCUICAst]
k:577 [binder, in MetaCoq.Template.utils.MCList]
k:577 [binder, in MetaCoq.PCUIC.PCUICSR]
k:578 [binder, in MetaCoq.PCUIC.PCUICSR]
k:579 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:580 [binder, in MetaCoq.Template.common.uGraph]
k:580 [binder, in MetaCoq.PCUIC.PCUICAst]
k:580 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:581 [binder, in MetaCoq.Template.EnvironmentTyping]
k:582 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:585 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:585 [binder, in MetaCoq.PCUIC.PCUICAst]
k:587 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:59 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:59 [binder, in MetaCoq.Template.EnvMap]
k:59 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:594 [binder, in MetaCoq.Template.EnvironmentTyping]
k:595 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:599 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:60 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:60 [binder, in MetaCoq.Translations.param_original]
k:60 [binder, in MetaCoq.Template.LiftSubst]
k:600 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:600 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:603 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:603 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:604 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:605 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:606 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:609 [binder, in MetaCoq.Template.Typing]
k:61 [binder, in MetaCoq.Erasure.EWellformed]
k:61 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
k:61 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:610 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:612 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:614 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
K:615 [binder, in MetaCoq.Template.utils.wGraph]
k:62 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
k:62 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:62 [binder, in MetaCoq.Translations.param_original]
k:620 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:627 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:63 [binder, in MetaCoq.Template.TermEquality]
k:63 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
k:63 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:63 [binder, in MetaCoq.Erasure.EGenericMapEnv]
k:635 [binder, in MetaCoq.PCUIC.PCUICConversion]
k:637 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:637 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:64 [binder, in MetaCoq.Translations.param_binary]
k:64 [binder, in MetaCoq.Erasure.EWellformed]
k:640 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:640 [binder, in MetaCoq.PCUIC.PCUICSpine]
K:641 [binder, in MetaCoq.Template.utils.wGraph]
K:642 [binder, in MetaCoq.Template.utils.wGraph]
k:643 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:643 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:647 [binder, in MetaCoq.PCUIC.PCUICSR]
k:647 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:65 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:65 [binder, in MetaCoq.Template.utils.wGraph]
k:65 [binder, in MetaCoq.PCUIC.PCUICAst]
k:651 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:654 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:66 [binder, in MetaCoq.Translations.param_binary]
k:66 [binder, in MetaCoq.Erasure.ELiftSubst]
k:662 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
K:662 [binder, in MetaCoq.Template.utils.wGraph]
k:662 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:665 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:668 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:67 [binder, in MetaCoq.Template.Ast]
k:67 [binder, in MetaCoq.Translations.param_cheap_packed]
k:67 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:672 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:674 [binder, in MetaCoq.PCUIC.PCUICSR]
k:68 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:68 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:68 [binder, in MetaCoq.PCUIC.PCUICAlpha]
k:68 [binder, in MetaCoq.Erasure.EWellformed]
k:68 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:680 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:689 [binder, in MetaCoq.Template.utils.MCList]
k:689 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:69 [binder, in MetaCoq.Template.Ast]
k:69 [binder, in MetaCoq.PCUIC.PCUICAlpha]
k:69 [binder, in MetaCoq.Template.EnvMap]
k:692 [binder, in MetaCoq.PCUIC.PCUICSpine]
K:693 [binder, in MetaCoq.Template.utils.wGraph]
K:694 [binder, in MetaCoq.Template.utils.wGraph]
k:7 [binder, in MetaCoq.Translations.param_binary]
k:7 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:7 [binder, in MetaCoq.Template.EnvMap]
k:70 [binder, in MetaCoq.Template.TermEquality]
k:70 [binder, in MetaCoq.Erasure.ELiftSubst]
k:71 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:71 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:71 [binder, in MetaCoq.Template.Ast]
k:71 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:71 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:71 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:71 [binder, in MetaCoq.Template.LiftSubst]
K:710 [binder, in MetaCoq.Template.utils.wGraph]
K:711 [binder, in MetaCoq.Template.utils.wGraph]
k:718 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:718 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:72 [binder, in MetaCoq.Erasure.EWellformed]
k:72 [binder, in MetaCoq.Template.TypingWf]
k:721 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:722 [binder, in MetaCoq.PCUIC.PCUICEquality]
k:728 [binder, in MetaCoq.Template.Universes]
k:73 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:73 [binder, in MetaCoq.Template.Ast]
k:74 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:74 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:746 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:75 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:75 [binder, in MetaCoq.Template.Ast]
k:76 [binder, in MetaCoq.Erasure.EWellformed]
k:76 [binder, in MetaCoq.Template.Checker]
k:76 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:76 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:77 [binder, in MetaCoq.Erasure.ELiftSubst]
k:77 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:770 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:779 [binder, in MetaCoq.PCUIC.PCUICSpine]
k:78 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:78 [binder, in MetaCoq.Template.utils.All_Forall]
k:78 [binder, in MetaCoq.Template.LiftSubst]
k:785 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:79 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:79 [binder, in MetaCoq.Template.Ast]
k:79 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:79 [binder, in MetaCoq.Erasure.EWellformed]
k:79 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
k:79 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:79 [binder, in MetaCoq.Template.TypingWf]
k:80 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:80 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:80 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:804 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:809 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:81 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:81 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:81 [binder, in MetaCoq.Template.Checker]
k:81 [binder, in MetaCoq.Erasure.ELiftSubst]
k:81 [binder, in MetaCoq.Template.LiftSubst]
k:819 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:82 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:82 [binder, in MetaCoq.Erasure.EWellformed]
k:829 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
k:83 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:83 [binder, in MetaCoq.PCUIC.PCUICAst]
k:83 [binder, in MetaCoq.Erasure.ELiftSubst]
k:837 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
k:839 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:84 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:84 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:84 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:842 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:844 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:85 [binder, in MetaCoq.PCUIC.PCUICAst]
k:856 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
k:86 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:86 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:86 [binder, in MetaCoq.Template.LiftSubst]
k:860 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:869 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:87 [binder, in MetaCoq.PCUIC.PCUICAst]
k:87 [binder, in MetaCoq.Template.Checker]
k:88 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:88 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:88 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:89 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:894 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:9 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
k:9 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
k:9 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:9 [binder, in MetaCoq.Template.UnivSubst]
k:9 [binder, in MetaCoq.Template.LiftSubst]
k:90 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:90 [binder, in MetaCoq.Erasure.ELiftSubst]
k:90 [binder, in MetaCoq.Template.Environment]
k:90 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:90 [binder, in MetaCoq.Template.LiftSubst]
k:902 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:909 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:909 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:91 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:91 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:914 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:919 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:92 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:92 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:92 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:92 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:926 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:928 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:93 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
k:93 [binder, in MetaCoq.Erasure.ELiftSubst]
k:932 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:94 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:94 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:94 [binder, in MetaCoq.Template.LiftSubst]
k:947 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:95 [binder, in MetaCoq.Template.TermEquality]
k:95 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:95 [binder, in MetaCoq.Template.Environment]
k:96 [binder, in MetaCoq.PCUIC.PCUICInductives]
k:96 [binder, in MetaCoq.Template.LiftSubst]
k:963 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:97 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:97 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:974 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:98 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
k:98 [binder, in MetaCoq.PCUIC.PCUICContexts]
k:981 [binder, in MetaCoq.Template.Typing]
k:988 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:99 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
k:99 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:99 [binder, in MetaCoq.Erasure.ELiftSubst]
k:991 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:992 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:993 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:994 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:995 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:996 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:997 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:998 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
k:999 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
| 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) |