| 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) |
U
ua [axiom, in MetaCoq.Translations.times_bool_fun]UA [definition, in MetaCoq.Translations.times_bool_fun]
UA [definition, in MetaCoq.Translations.times_bool_fun2]
UA_postcomposeequiv' [definition, in MetaCoq.Translations.times_bool_fun2]
UA_postcomposeequiv [definition, in MetaCoq.Translations.times_bool_fun2]
ua:11 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
ua:2 [binder, in MetaCoq.Template.UnivSubst]
ua:7 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
UContext [module, in MetaCoq.Template.Universes]
UContext.constraints [definition, in MetaCoq.Template.Universes]
UContext.dest [definition, in MetaCoq.Template.Universes]
UContext.empty [definition, in MetaCoq.Template.Universes]
UContext.instance [definition, in MetaCoq.Template.Universes]
UContext.make [definition, in MetaCoq.Template.Universes]
UContext.make' [definition, in MetaCoq.Template.Universes]
UContext.t [definition, in MetaCoq.Template.Universes]
uctx_of_udecl [definition, in MetaCoq.Template.common.uGraph]
uctx_invariants [definition, in MetaCoq.Template.common.uGraph]
uctx':12 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx':181 [binder, in MetaCoq.Template.common.uGraph]
uctx':4 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx':700 [binder, in MetaCoq.Template.common.uGraph]
uctx':708 [binder, in MetaCoq.Template.common.uGraph]
uctx':713 [binder, in MetaCoq.Template.common.uGraph]
uctx':78 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
uctx1:660 [binder, in MetaCoq.Template.common.uGraph]
uctx1:670 [binder, in MetaCoq.Template.common.uGraph]
uctx2:661 [binder, in MetaCoq.Template.common.uGraph]
uctx2:671 [binder, in MetaCoq.Template.common.uGraph]
uctx:156 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
uctx:157 [binder, in MetaCoq.Template.common.uGraph]
uctx:158 [binder, in MetaCoq.Template.common.uGraph]
uctx:159 [binder, in MetaCoq.Template.common.uGraph]
uctx:162 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:162 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:163 [binder, in MetaCoq.Template.common.uGraph]
uctx:164 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:166 [binder, in MetaCoq.Template.common.uGraph]
uctx:167 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:169 [binder, in MetaCoq.Template.common.uGraph]
uctx:172 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:180 [binder, in MetaCoq.Template.common.uGraph]
uctx:207 [binder, in MetaCoq.Template.common.uGraph]
uctx:210 [binder, in MetaCoq.Template.common.uGraph]
uctx:222 [binder, in MetaCoq.Template.common.uGraph]
uctx:236 [binder, in MetaCoq.Template.common.uGraph]
uctx:245 [binder, in MetaCoq.Template.common.uGraph]
uctx:247 [binder, in MetaCoq.Template.common.uGraph]
uctx:263 [binder, in MetaCoq.Template.common.uGraph]
uctx:3 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
uctx:433 [binder, in MetaCoq.Template.Universes]
uctx:439 [binder, in MetaCoq.Template.Checker]
uctx:441 [binder, in MetaCoq.Template.Universes]
uctx:45 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:471 [binder, in MetaCoq.Template.common.uGraph]
uctx:472 [binder, in MetaCoq.Template.common.uGraph]
uctx:474 [binder, in MetaCoq.Template.common.uGraph]
uctx:535 [binder, in MetaCoq.Template.common.uGraph]
uctx:548 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
uctx:615 [binder, in MetaCoq.Template.common.uGraph]
uctx:618 [binder, in MetaCoq.Template.common.uGraph]
uctx:674 [binder, in MetaCoq.Template.common.uGraph]
uctx:678 [binder, in MetaCoq.Template.common.uGraph]
uctx:681 [binder, in MetaCoq.Template.common.uGraph]
uctx:686 [binder, in MetaCoq.Template.common.uGraph]
uctx:689 [binder, in MetaCoq.Template.common.uGraph]
uctx:694 [binder, in MetaCoq.Template.common.uGraph]
uctx:698 [binder, in MetaCoq.Template.common.uGraph]
uctx:706 [binder, in MetaCoq.Template.common.uGraph]
uctx:712 [binder, in MetaCoq.Template.common.uGraph]
uctx:72 [binder, in MetaCoq.Template.Checker]
uctx:74 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
uctx:764 [binder, in MetaCoq.Template.Universes]
uctx:85 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:87 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:91 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:92 [binder, in MetaCoq.Template.EnvironmentTyping]
uctx:99 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
uc:102 [binder, in MetaCoq.Template.common.uGraph]
uc:103 [binder, in MetaCoq.Template.common.uGraph]
uc:110 [binder, in MetaCoq.Template.common.uGraph]
uc:112 [binder, in MetaCoq.Template.common.uGraph]
uc:89 [binder, in MetaCoq.Template.common.uGraph]
udecl [projection, in MetaCoq.SafeChecker.PCUICWfEnv]
udecl_prop_in_var_poly [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl':728 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl':733 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:1035 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:163 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:165 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
udecl:168 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:173 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:214 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:22 [binder, in MetaCoq.Erasure.ErasureCorrectness]
udecl:221 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:228 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:314 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:46 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:467 [binder, in MetaCoq.Template.EnvironmentTyping]
udecl:570 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:669 [binder, in MetaCoq.Template.EnvironmentTyping]
udecl:673 [binder, in MetaCoq.Template.common.uGraph]
udecl:681 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
udecl:727 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:732 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:77 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:78 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
udecl:862 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
udecl:901 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
udecl:92 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
udecl:977 [binder, in MetaCoq.Erasure.ErasureFunction]
uf:14 [binder, in MetaCoq.PCUIC.PCUICAst]
uf:23 [binder, in MetaCoq.Template.Ast]
uf:29 [binder, in MetaCoq.PCUIC.PCUICAst]
uf:65 [binder, in MetaCoq.Template.Ast]
uGraph [library]
uinst:8 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
uint_wB [definition, in MetaCoq.Template.BasicAst]
uint_size [definition, in MetaCoq.Template.BasicAst]
uint63_model [definition, in MetaCoq.Template.BasicAst]
uint63_to_model [definition, in MetaCoq.PCUIC.TemplateToPCUIC]
uint63_from_model [definition, in MetaCoq.PCUIC.PCUICToTemplate]
UIP [definition, in MetaCoq.Translations.times_bool_fun]
UIP [definition, in MetaCoq.Translations.param_generous_packed]
uip_bool [lemma, in MetaCoq.Template.utils.MCUtils]
uip_preservation [lemma, in MetaCoq.Translations.param_generous_packed]
ui':113 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ui':1235 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui':1243 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui':195 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ui':30 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
ui':371 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui':393 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui':400 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui':58 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ui:109 [binder, in MetaCoq.PCUIC.PCUICAst]
ui:111 [binder, in MetaCoq.PCUIC.PCUICAst]
ui:111 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ui:114 [binder, in MetaCoq.PCUIC.PCUICAst]
ui:1234 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui:1242 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui:163 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
ui:171 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
ui:189 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
ui:194 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ui:224 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
ui:301 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
ui:329 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
ui:368 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui:39 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
ui:390 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui:399 [binder, in MetaCoq.PCUIC.PCUICConversion]
ui:446 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
ui:48 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
ui:55 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
UnboundEvar [constructor, in MetaCoq.SafeChecker.PCUICErrors]
UnboundEvar [constructor, in MetaCoq.Template.Checker]
UnboundMeta [constructor, in MetaCoq.Template.Checker]
UnboundRel [constructor, in MetaCoq.SafeChecker.PCUICErrors]
UnboundRel [constructor, in MetaCoq.Template.Checker]
UnboundVar [constructor, in MetaCoq.SafeChecker.PCUICErrors]
UnboundVar [constructor, in MetaCoq.Template.Checker]
UndeclaredConstant [constructor, in MetaCoq.SafeChecker.PCUICErrors]
UndeclaredConstant [constructor, in MetaCoq.Template.Checker]
UndeclaredConstructor [constructor, in MetaCoq.SafeChecker.PCUICErrors]
UndeclaredConstructor [constructor, in MetaCoq.Template.Checker]
UndeclaredInductive [constructor, in MetaCoq.SafeChecker.PCUICErrors]
UndeclaredInductive [constructor, in MetaCoq.Template.Checker]
unfold [definition, in MetaCoq.Template.utils.MCList]
unfold [constructor, in MetaCoq.Template.TemplateMonad.Common]
unfold_length [lemma, in MetaCoq.Template.utils.MCList]
unfold_cofix [definition, in MetaCoq.Template.Typing]
unfold_fix [definition, in MetaCoq.Template.Typing]
unfold_cofix [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
unfold_fix [definition, in MetaCoq.PCUIC.Syntax.PCUICCases]
unfold_one_proj_None [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_proj_cored [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_proj [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case_None [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case_cored [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_constants [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_None [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_decompose [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_cored [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zippx [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zipp [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case [definition, in MetaCoq.Template.Checker]
unfold_one_fix [definition, in MetaCoq.Template.Checker]
unfold_cofix [definition, in MetaCoq.Erasure.EGlobalEnv]
unfold_fix [definition, in MetaCoq.Erasure.EGlobalEnv]
unfold_cofix_wf [lemma, in MetaCoq.Template.TypingWf]
unfold_fix_wf [lemma, in MetaCoq.Template.TypingWf]
unfold_cofix_type [lemma, in MetaCoq.Erasure.Prelim]
unf:210 [binder, in MetaCoq.Template.Checker]
unguarded:85 [binder, in MetaCoq.Erasure.EWcbvEval]
unguarded:93 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
unique_sorting_equality_propositional [lemma, in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop [lemma, in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_r [lemma, in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_l [lemma, in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop [lemma, in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_r [lemma, in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_l [lemma, in MetaCoq.PCUIC.PCUICElimination]
unit [record, in MetaCoq.Translations.MiniHoTT]
unit [record, in MetaCoq.Translations.MiniHoTT_paths]
Univ [section, in MetaCoq.Template.Universes]
univ [definition, in MetaCoq.Examples.typing_correctness]
univ [definition, in MetaCoq.Examples.metacoq_tour_prelude]
UnivConstraint [module, in MetaCoq.Template.Universes]
UnivConstraint.compare [definition, in MetaCoq.Template.Universes]
UnivConstraint.compare_spec [lemma, in MetaCoq.Template.Universes]
UnivConstraint.eq [definition, in MetaCoq.Template.Universes]
UnivConstraint.eq_leibniz [definition, in MetaCoq.Template.Universes]
UnivConstraint.eq_dec [lemma, in MetaCoq.Template.Universes]
UnivConstraint.eq_equiv [definition, in MetaCoq.Template.Universes]
UnivConstraint.lt [definition, in MetaCoq.Template.Universes]
UnivConstraint.lt_compat [lemma, in MetaCoq.Template.Universes]
UnivConstraint.lt_strorder [lemma, in MetaCoq.Template.Universes]
UnivConstraint.lt_Level1 [constructor, in MetaCoq.Template.Universes]
UnivConstraint.lt_Cstr [constructor, in MetaCoq.Template.Universes]
UnivConstraint.lt_Level2 [constructor, in MetaCoq.Template.Universes]
UnivConstraint.lt_ [inductive, in MetaCoq.Template.Universes]
UnivConstraint.make [definition, in MetaCoq.Template.Universes]
UnivConstraint.t [definition, in MetaCoq.Template.Universes]
Universe [module, in MetaCoq.Template.Universes]
UniverseClosedSubst [section, in MetaCoq.Template.Universes]
UniverseClosedSubst [section, in MetaCoq.PCUIC.PCUICInductiveInversion]
UniverseLemmas [section, in MetaCoq.Template.Universes]
Universes [library]
universes_entry_of_decl [definition, in MetaCoq.Template.Universes]
universes_entry [inductive, in MetaCoq.Template.Universes]
universes_decl [inductive, in MetaCoq.Template.Universes]
universes_graph [definition, in MetaCoq.Template.common.uGraph]
universe_sup_eq_universe [instance, in MetaCoq.Template.Universes]
Universe.add_list_to_exprs [definition, in MetaCoq.Template.Universes]
Universe.add_to_exprs [definition, in MetaCoq.Template.Universes]
Universe.eqb [definition, in MetaCoq.Template.Universes]
Universe.eqb_refl [lemma, in MetaCoq.Template.Universes]
Universe.eq_dec_univ [instance, in MetaCoq.Template.Universes]
Universe.from_kernel_repr [definition, in MetaCoq.Template.Universes]
Universe.get_is_level [definition, in MetaCoq.Template.Universes]
Universe.get_univ_exprs [definition, in MetaCoq.Template.Universes]
Universe.is_type_sort [definition, in MetaCoq.Template.Universes]
Universe.is_prop [definition, in MetaCoq.Template.Universes]
Universe.is_sprop [definition, in MetaCoq.Template.Universes]
Universe.is_level [definition, in MetaCoq.Template.Universes]
Universe.is_levels [definition, in MetaCoq.Template.Universes]
Universe.lProp [constructor, in MetaCoq.Template.Universes]
Universe.lSProp [constructor, in MetaCoq.Template.Universes]
Universe.lType [constructor, in MetaCoq.Template.Universes]
Universe.make [definition, in MetaCoq.Template.Universes]
Universe.make_inj [lemma, in MetaCoq.Template.Universes]
Universe.of_levels [definition, in MetaCoq.Template.Universes]
Universe.of_expr [definition, in MetaCoq.Template.Universes]
Universe.on_sort [definition, in MetaCoq.Template.Universes]
Universe.reflect_eq_universe [instance, in MetaCoq.Template.Universes]
Universe.sort_of_product [definition, in MetaCoq.Template.Universes]
Universe.sup [definition, in MetaCoq.Template.Universes]
Universe.super [definition, in MetaCoq.Template.Universes]
Universe.t [definition, in MetaCoq.Template.Universes]
Universe.to_cuniv [definition, in MetaCoq.Template.Universes]
Universe.type0 [definition, in MetaCoq.Template.Universes]
Universe.type1 [definition, in MetaCoq.Template.Universes]
Universe.t_ [inductive, in MetaCoq.Template.Universes]
Universe.val_make [lemma, in MetaCoq.Template.Universes]
UnivSubst [record, in MetaCoq.Template.Universes]
UnivSubst [inductive, in MetaCoq.Template.Universes]
UnivSubst [library]
univs':643 [binder, in MetaCoq.Template.EnvironmentTyping]
univs':73 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
univs:100 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:1013 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:1014 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:1015 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:102 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:1024 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:1034 [binder, in MetaCoq.PCUIC.PCUICConversion]
univs:104 [binder, in MetaCoq.Erasure.ErasureProperties]
univs:108 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
univs:11 [binder, in MetaCoq.Erasure.ErasureCorrectness]
univs:1101 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:1135 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1151 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1198 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1210 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1222 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1235 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1292 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1317 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1318 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:1334 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1349 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:1355 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1370 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1392 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1398 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:14 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:140 [binder, in MetaCoq.Template.Pretty]
univs:1417 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:142 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:149 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
univs:151 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
univs:1521 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:1539 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:163 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
univs:168 [binder, in MetaCoq.Erasure.Extract]
univs:17 [binder, in MetaCoq.Erasure.ErasureCorrectness]
univs:189 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
univs:2 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
univs:20 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:201 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:23 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
univs:231 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:235 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:235 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:239 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:243 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:247 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:25 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:25 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:263 [binder, in MetaCoq.Template.EtaExpand]
univs:27 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
univs:29 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:294 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
univs:300 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
univs:310 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
univs:319 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:32 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:39 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:39 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:4 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:41 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
univs:42 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:424 [binder, in MetaCoq.Template.Checker]
univs:431 [binder, in MetaCoq.Template.Checker]
univs:44 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:45 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:460 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:462 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:464 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:466 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:48 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:483 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:490 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:493 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:505 [binder, in MetaCoq.Template.EtaExpand]
univs:51 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
univs:511 [binder, in MetaCoq.Template.EtaExpand]
univs:517 [binder, in MetaCoq.Template.EtaExpand]
univs:525 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:531 [binder, in MetaCoq.Template.Typing]
univs:537 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:539 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:54 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:540 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:545 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:547 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:567 [binder, in MetaCoq.Template.Typing]
univs:58 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
univs:61 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:61 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
univs:639 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:64 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
univs:647 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:66 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:663 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:68 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
univs:71 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
univs:71 [binder, in MetaCoq.Template.TypingWf]
univs:72 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
univs:72 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
univs:720 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:73 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:74 [binder, in MetaCoq.Erasure.ErasureProperties]
univs:76 [binder, in MetaCoq.Translations.translation_utils]
univs:80 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:82 [binder, in MetaCoq.Template.EnvironmentTyping]
univs:86 [binder, in MetaCoq.Erasure.ErasureProperties]
univs:945 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:956 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:961 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:969 [binder, in MetaCoq.Erasure.ErasureFunction]
univs:97 [binder, in MetaCoq.Erasure.ErasureProperties]
univx:87 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
univy:91 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
univ_is_prop_make [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
univ_exprs_map_all [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
univ_epxrs_elements_map [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
univ_expr_set_in_elements [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
univ:160 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
unlift [definition, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
unlift_renaming [definition, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
unlift_opt_pred [definition, in MetaCoq.Template.Typing]
unlift_opt_pred [definition, in MetaCoq.PCUIC.PCUICTyping]
Unnamed_thm0 [definition, in MetaCoq.Examples.constructor_tac]
Unnamed_thm [definition, in MetaCoq.Examples.constructor_tac]
Unnamed_thm [definition, in MetaCoq.Translations.times_bool_fun2]
Unnamed_thm [definition, in MetaCoq.Translations.param_generous_packed]
unpack_sigma [definition, in MetaCoq.Translations.MiniHoTT]
unpack_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
UnsatisfiableConstraints [constructor, in MetaCoq.Template.Checker]
UnsatisfiedConstraints [constructor, in MetaCoq.SafeChecker.PCUICErrors]
UnsatisfiedConstraints [constructor, in MetaCoq.Template.Checker]
untyped_substitution_red [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_length [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_nth_error [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
untyped_cons_let_def [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
untyped_cons_let_ass [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
untyped_emptyslet [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet [inductive, in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_projs [lemma, in MetaCoq.PCUIC.PCUICInductives]
untyped_subslet_inds [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
untyped_subslet_inds [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_length [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_lift [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ass [lemma, in MetaCoq.PCUIC.PCUICConvCumInversion]
untyped_substitution_ws_cumul_pb_subst_conv' [lemma, in MetaCoq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb_subst_conv [lemma, in MetaCoq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
untyped_closed_red_subst [lemma, in MetaCoq.PCUIC.PCUICConversion]
untyped_subslet_def_tip [lemma, in MetaCoq.PCUIC.PCUICConversion]
untyped_subslet_extended_subst [lemma, in MetaCoq.PCUIC.PCUICContexts]
untyped_subslet_lift [lemma, in MetaCoq.PCUIC.PCUICContexts]
untyped_subslet_eq_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
untyped_subslet_skipn [lemma, in MetaCoq.PCUIC.PCUICSpine]
up [definition, in MetaCoq.Template.EtaExpand]
Up [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up [definition, in MetaCoq.Erasure.ELiftSubst]
up [definition, in MetaCoq.Template.LiftSubst]
upars:103 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
upars:395 [binder, in MetaCoq.Template.Ast]
Upn [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_subst_consn_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_subst_consn_ge [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_compose [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_Upn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_comp [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_S [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_1 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_Up [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren_r [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren_l [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_proper [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_eq [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_1_Up [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_0 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ext [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
upn_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Upn_ctxmap [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
UProp [constructor, in MetaCoq.Template.Universes]
upto_names_impl_leq_term [lemma, in MetaCoq.PCUIC.PCUICEquality]
upto_names_impl_eq_term [lemma, in MetaCoq.PCUIC.PCUICEquality]
upto_names_impl [lemma, in MetaCoq.PCUIC.PCUICEquality]
upto_names_trans [instance, in MetaCoq.PCUIC.PCUICEquality]
upto_names_sym [instance, in MetaCoq.PCUIC.PCUICEquality]
upto_names_ref [instance, in MetaCoq.PCUIC.PCUICEquality]
upto_names' [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
upto_names [definition, in MetaCoq.PCUIC.PCUICEquality]
upto_eq_impl [lemma, in MetaCoq.PCUIC.PCUICEquality]
upto_names_eq_term [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_leq_term [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_eq_term_upto_univ [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_eq_term_refl [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_conv_context [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_check_cofix [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_check_fix [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_destInd [lemma, in MetaCoq.PCUIC.PCUICAlpha]
upto_names_terms_refl [instance, in MetaCoq.PCUIC.PCUICAlpha]
Up_comp [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext_closed [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_up_assoc [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Up_Up_assoc [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_Upn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_Up [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
Up_ext [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_proper' [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_up [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext_cond [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
up_0 [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Up_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Up_ctxmap [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
urename_is_open_term [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urename_on_free_vars_shift [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urenaming [definition, in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
urenaming_strengthen [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
urenaming_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vdef [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vass [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_impl [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
USProp [constructor, in MetaCoq.Template.Universes]
usubst [definition, in MetaCoq.PCUIC.Syntax.PCUICInstDef]
usubst_well_subst [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
usubst_up_vdef [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_up_vass [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_app_up [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_app [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_Up' [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_Up [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_ext [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_on_free_vars_shift [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
us':24 [binder, in MetaCoq.Translations.param_original]
us':38 [binder, in MetaCoq.Translations.param_binary]
us:126 [binder, in MetaCoq.PCUIC.PCUICAst]
us:152 [binder, in MetaCoq.PCUIC.PCUICArities]
us:16 [binder, in MetaCoq.Erasure.EAst]
us:162 [binder, in MetaCoq.PCUIC.PCUICArities]
us:2 [binder, in MetaCoq.Translations.translation_utils]
us:217 [binder, in MetaCoq.Template.Ast]
us:439 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
us:453 [binder, in MetaCoq.Template.EnvironmentTyping]
us:482 [binder, in MetaCoq.PCUIC.PCUICNormal]
us:515 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
us:60 [binder, in MetaCoq.Translations.times_bool_fun]
utils [library]
UType [constructor, in MetaCoq.Template.Universes]
u'':106 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u'':99 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u'0:398 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u'0:419 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u'0:470 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u'0:491 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':101 [binder, in MetaCoq.Erasure.Extract]
u':104 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u':105 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
u':1058 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':1067 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':1079 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':1098 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':11 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u':110 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u':1105 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':111 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
u':117 [binder, in MetaCoq.Template.TermEquality]
u':117 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':118 [binder, in MetaCoq.Template.common.uGraph]
u':118 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u':12 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':12 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':122 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':122 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':123 [binder, in MetaCoq.Template.common.uGraph]
u':124 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u':126 [binder, in MetaCoq.Template.common.uGraph]
u':126 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':126 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':128 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':130 [binder, in MetaCoq.Template.common.uGraph]
u':130 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u':131 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':1326 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u':134 [binder, in MetaCoq.Template.common.uGraph]
u':134 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':136 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u':136 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':137 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':138 [binder, in MetaCoq.Template.common.uGraph]
u':139 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':139 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':14 [binder, in MetaCoq.Template.TermEquality]
u':141 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':142 [binder, in MetaCoq.Template.common.uGraph]
u':147 [binder, in MetaCoq.Template.common.uGraph]
u':149 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':15 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':151 [binder, in MetaCoq.Template.common.uGraph]
u':155 [binder, in MetaCoq.Template.common.uGraph]
u':157 [binder, in MetaCoq.PCUIC.PCUICArities]
u':157 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u':157 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':159 [binder, in MetaCoq.PCUIC.PCUICSR]
u':159 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':160 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u':161 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':163 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u':163 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':165 [binder, in MetaCoq.Erasure.EArities]
u':167 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u':17 [binder, in MetaCoq.PCUIC.PCUICSN]
u':171 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u':175 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U':176 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u':178 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u':18 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':182 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':185 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':186 [binder, in MetaCoq.Erasure.EArities]
u':19 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':192 [binder, in MetaCoq.Erasure.EArities]
u':197 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':199 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':208 [binder, in MetaCoq.Template.Universes]
u':210 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':212 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':216 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':22 [binder, in MetaCoq.Template.Checker]
u':222 [binder, in MetaCoq.PCUIC.PCUICElimination]
u':228 [binder, in MetaCoq.PCUIC.PCUICElimination]
u':229 [binder, in MetaCoq.Template.Universes]
u':229 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':230 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u':231 [binder, in MetaCoq.Template.Universes]
u':233 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':234 [binder, in MetaCoq.PCUIC.PCUICElimination]
u':235 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':235 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':238 [binder, in MetaCoq.Template.Universes]
u':239 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':24 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':240 [binder, in MetaCoq.PCUIC.PCUICElimination]
u':242 [binder, in MetaCoq.Template.Universes]
u':244 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u':246 [binder, in MetaCoq.PCUIC.PCUICElimination]
u':25 [binder, in MetaCoq.PCUIC.PCUICSN]
u':250 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u':252 [binder, in MetaCoq.PCUIC.PCUICElimination]
u':252 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':253 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':254 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':256 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u':258 [binder, in MetaCoq.PCUIC.PCUICElimination]
u':258 [binder, in MetaCoq.Erasure.EArities]
u':26 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
u':266 [binder, in MetaCoq.Erasure.EArities]
u':266 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':270 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':272 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':29 [binder, in MetaCoq.Translations.standard_model]
u':29 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':292 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':296 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':3 [binder, in MetaCoq.Template.TermEquality]
u':30 [binder, in MetaCoq.Translations.times_bool_fun]
u':30 [binder, in MetaCoq.PCUIC.PCUICSN]
u':302 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':31 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':310 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':312 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':316 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':320 [binder, in MetaCoq.Template.TypingWf]
U':321 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':323 [binder, in MetaCoq.Template.Checker]
u':324 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':328 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':330 [binder, in MetaCoq.Template.Universes]
u':332 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':34 [binder, in MetaCoq.Translations.times_bool_fun]
u':340 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':350 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':351 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':353 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':354 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':355 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':357 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':363 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':363 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':363 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':369 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':372 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':379 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u':381 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':389 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':39 [binder, in MetaCoq.PCUIC.PCUICSN]
u':39 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':390 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u':393 [binder, in MetaCoq.PCUIC.PCUICProgress]
u':394 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':396 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':396 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':40 [binder, in MetaCoq.Erasure.Extract]
u':417 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':429 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':43 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':43 [binder, in MetaCoq.Translations.param_cheap_packed]
u':44 [binder, in MetaCoq.Template.TermEquality]
u':44 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
u':445 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':45 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u':45 [binder, in MetaCoq.Translations.param_cheap_packed]
u':450 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':452 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':459 [binder, in MetaCoq.Template.common.uGraph]
u':46 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':462 [binder, in MetaCoq.Template.common.uGraph]
u':465 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':468 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':47 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u':47 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':47 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u':48 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':481 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':487 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':489 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':490 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':493 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':494 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':496 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':498 [binder, in MetaCoq.Template.Universes]
u':499 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':502 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':503 [binder, in MetaCoq.Template.Universes]
u':503 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':51 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
u':513 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':519 [binder, in MetaCoq.Template.EnvironmentTyping]
u':519 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u':52 [binder, in MetaCoq.PCUIC.PCUICSN]
u':52 [binder, in MetaCoq.Translations.param_generous_packed]
u':520 [binder, in MetaCoq.Template.Universes]
u':521 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':522 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':524 [binder, in MetaCoq.Template.Universes]
u':530 [binder, in MetaCoq.Template.EnvironmentTyping]
u':536 [binder, in MetaCoq.Template.Universes]
u':536 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u':537 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':539 [binder, in MetaCoq.Template.Universes]
u':54 [binder, in MetaCoq.Translations.param_generous_packed]
u':543 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u':545 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':546 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':548 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':550 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':557 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':56 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u':567 [binder, in MetaCoq.Template.Universes]
u':57 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':570 [binder, in MetaCoq.Template.Universes]
u':571 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u':573 [binder, in MetaCoq.Template.Universes]
u':578 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':592 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':60 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u':60 [binder, in MetaCoq.PCUIC.PCUICSN]
u':61 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
u':621 [binder, in MetaCoq.Template.Universes]
u':627 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u':634 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u':650 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u':652 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':654 [binder, in MetaCoq.PCUIC.PCUICReduction]
u':657 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u':660 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u':666 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u':670 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':672 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u':7 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':7 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
u':70 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':702 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':708 [binder, in MetaCoq.PCUIC.PCUICEquality]
u':714 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u':727 [binder, in MetaCoq.Template.Universes]
u':756 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u':77 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':77 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':77 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u':787 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u':79 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u':8 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u':8 [binder, in MetaCoq.Template.TermEquality]
u':801 [binder, in MetaCoq.PCUIC.PCUICConversion]
u':81 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u':81 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u':869 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u':87 [binder, in MetaCoq.Template.TermEquality]
u':87 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
u':90 [binder, in MetaCoq.Template.TermEquality]
u':93 [binder, in MetaCoq.Template.TermEquality]
u':93 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
u':93 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
u':962 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u':97 [binder, in MetaCoq.Template.TermEquality]
u':97 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u':988 [binder, in MetaCoq.Erasure.ErasureFunction]
u0:29 [binder, in MetaCoq.Translations.param_original]
u0:377 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1':582 [binder, in MetaCoq.Template.Universes]
u1:103 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:106 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:109 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:112 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:113 [binder, in MetaCoq.PCUIC.PCUICElimination]
u1:115 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:118 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:121 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:124 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:132 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u1:138 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:143 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u1:200 [binder, in MetaCoq.Erasure.EArities]
u1:204 [binder, in MetaCoq.Erasure.EArities]
u1:211 [binder, in MetaCoq.Template.Universes]
u1:254 [binder, in MetaCoq.Template.Universes]
u1:2798 [binder, in MetaCoq.Translations.MiniHoTT]
u1:2806 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u1:2810 [binder, in MetaCoq.Translations.MiniHoTT]
u1:2818 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u1:30 [binder, in MetaCoq.Translations.param_original]
u1:307 [binder, in MetaCoq.Template.Universes]
u1:332 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u1:338 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u1:345 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u1:4 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u1:410 [binder, in MetaCoq.Template.common.uGraph]
u1:424 [binder, in MetaCoq.Template.common.uGraph]
u1:426 [binder, in MetaCoq.Template.common.uGraph]
u1:430 [binder, in MetaCoq.Template.common.uGraph]
u1:4405 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u1:445 [binder, in MetaCoq.Template.common.uGraph]
u1:451 [binder, in MetaCoq.Template.common.uGraph]
u1:453 [binder, in MetaCoq.Template.common.uGraph]
u1:465 [binder, in MetaCoq.Template.common.uGraph]
u1:49 [binder, in MetaCoq.Translations.param_binary]
u1:490 [binder, in MetaCoq.Template.common.uGraph]
u1:492 [binder, in MetaCoq.Template.common.uGraph]
u1:494 [binder, in MetaCoq.Template.common.uGraph]
u1:496 [binder, in MetaCoq.Template.common.uGraph]
u1:501 [binder, in MetaCoq.PCUIC.PCUICEquality]
u1:527 [binder, in MetaCoq.Template.common.uGraph]
u1:527 [binder, in MetaCoq.PCUIC.PCUICEquality]
u1:529 [binder, in MetaCoq.Template.common.uGraph]
u1:531 [binder, in MetaCoq.Template.common.uGraph]
u1:533 [binder, in MetaCoq.Template.common.uGraph]
u1:537 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u1:542 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u1:570 [binder, in MetaCoq.PCUIC.PCUICConversion]
u1:575 [binder, in MetaCoq.Template.Universes]
u1:578 [binder, in MetaCoq.Template.Universes]
u1:581 [binder, in MetaCoq.Template.Universes]
u1:586 [binder, in MetaCoq.Template.Universes]
u1:61 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:66 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:74 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:81 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:813 [binder, in MetaCoq.PCUIC.PCUICConversion]
u1:85 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u1:854 [binder, in MetaCoq.PCUIC.PCUICConversion]
u2':584 [binder, in MetaCoq.Template.Universes]
u2:104 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:107 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:110 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:113 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:114 [binder, in MetaCoq.PCUIC.PCUICElimination]
u2:116 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:119 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:122 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:125 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:136 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u2:139 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:147 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u2:201 [binder, in MetaCoq.Erasure.EArities]
u2:205 [binder, in MetaCoq.Erasure.EArities]
u2:212 [binder, in MetaCoq.Template.Universes]
u2:255 [binder, in MetaCoq.Template.Universes]
u2:2801 [binder, in MetaCoq.Translations.MiniHoTT]
u2:2809 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u2:2812 [binder, in MetaCoq.Translations.MiniHoTT]
u2:2820 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u2:308 [binder, in MetaCoq.Template.Universes]
u2:333 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u2:339 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u2:346 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u2:411 [binder, in MetaCoq.Template.common.uGraph]
u2:425 [binder, in MetaCoq.Template.common.uGraph]
u2:427 [binder, in MetaCoq.Template.common.uGraph]
u2:431 [binder, in MetaCoq.Template.common.uGraph]
u2:4406 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u2:446 [binder, in MetaCoq.Template.common.uGraph]
u2:452 [binder, in MetaCoq.Template.common.uGraph]
u2:454 [binder, in MetaCoq.Template.common.uGraph]
u2:466 [binder, in MetaCoq.Template.common.uGraph]
u2:491 [binder, in MetaCoq.Template.common.uGraph]
u2:493 [binder, in MetaCoq.Template.common.uGraph]
u2:495 [binder, in MetaCoq.Template.common.uGraph]
u2:497 [binder, in MetaCoq.Template.common.uGraph]
u2:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u2:503 [binder, in MetaCoq.PCUIC.PCUICEquality]
u2:528 [binder, in MetaCoq.Template.common.uGraph]
u2:529 [binder, in MetaCoq.PCUIC.PCUICEquality]
u2:530 [binder, in MetaCoq.Template.common.uGraph]
u2:532 [binder, in MetaCoq.Template.common.uGraph]
u2:534 [binder, in MetaCoq.Template.common.uGraph]
u2:539 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u2:544 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u2:571 [binder, in MetaCoq.PCUIC.PCUICConversion]
u2:576 [binder, in MetaCoq.Template.Universes]
u2:579 [binder, in MetaCoq.Template.Universes]
u2:583 [binder, in MetaCoq.Template.Universes]
u2:591 [binder, in MetaCoq.Template.Universes]
u2:62 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:67 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:75 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:814 [binder, in MetaCoq.PCUIC.PCUICConversion]
u2:82 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:855 [binder, in MetaCoq.PCUIC.PCUICConversion]
u2:86 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:1 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
u:1 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:10 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:10 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:10 [binder, in MetaCoq.Template.WfAst]
u:10 [binder, in MetaCoq.Template.utils.MCEquality]
u:10 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:10 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:10 [binder, in MetaCoq.Template.UnivSubst]
u:10 [binder, in MetaCoq.Template.LiftSubst]
u:100 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:100 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:100 [binder, in MetaCoq.PCUIC.PCUICValidity]
u:101 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:101 [binder, in MetaCoq.Template.EnvironmentTyping]
u:101 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:101 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:101 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:1018 [binder, in MetaCoq.Translations.MiniHoTT]
u:102 [binder, in MetaCoq.PCUIC.PCUICInversion]
u:102 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:102 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:1026 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1026 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:1028 [binder, in MetaCoq.Template.Typing]
u:1029 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:103 [binder, in MetaCoq.Erasure.EArities]
u:103 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:103 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:103 [binder, in MetaCoq.Erasure.ErasureProperties]
u:1031 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1033 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:1035 [binder, in MetaCoq.Template.Typing]
u:1039 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:104 [binder, in MetaCoq.Template.Universes]
u:104 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:104 [binder, in MetaCoq.Template.EnvironmentTyping]
u:104 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
U:104 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:1045 [binder, in MetaCoq.Template.Typing]
u:1045 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:105 [binder, in MetaCoq.Erasure.Extract]
u:105 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
u:1055 [binder, in MetaCoq.Template.utils.All_Forall]
u:1057 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1057 [binder, in MetaCoq.Translations.MiniHoTT]
u:106 [binder, in MetaCoq.Template.Universes]
u:106 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:106 [binder, in MetaCoq.PCUIC.PCUICAst]
u:1062 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1065 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:1066 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1068 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:107 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:107 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:107 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:1072 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1076 [binder, in MetaCoq.Template.Typing]
u:1076 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:1078 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:108 [binder, in MetaCoq.Template.Universes]
u:108 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:109 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:109 [binder, in MetaCoq.Erasure.EInduction]
u:109 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:109 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1097 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1099 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:11 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:11 [binder, in MetaCoq.PCUIC.PCUICEquality]
U:11 [binder, in MetaCoq.PCUIC.PCUICInversion]
u:11 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
u:11 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:11 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:110 [binder, in MetaCoq.Erasure.EArities]
U:110 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:110 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
u:110 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:1101 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:1104 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1107 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:111 [binder, in MetaCoq.Template.Universes]
u:111 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:111 [binder, in MetaCoq.PCUIC.PCUICValidity]
U:111 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:111 [binder, in MetaCoq.Template.AstUtils]
u:1110 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:112 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:112 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:112 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:112 [binder, in MetaCoq.Erasure.ErasureProperties]
u:112 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:112 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:113 [binder, in MetaCoq.Template.Universes]
u:113 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:114 [binder, in MetaCoq.Template.EtaExpand]
u:114 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
u:1149 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:115 [binder, in MetaCoq.Template.Universes]
u:115 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:115 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
u:115 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:115 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:1153 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:1158 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:116 [binder, in MetaCoq.Template.EtaExpand]
u:116 [binder, in MetaCoq.Template.Universes]
u:116 [binder, in MetaCoq.Template.TermEquality]
u:116 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:116 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u:116 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:116 [binder, in MetaCoq.Erasure.EEtaExpanded]
u:1164 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:117 [binder, in MetaCoq.Template.Universes]
u:117 [binder, in MetaCoq.PCUIC.PCUICValidity]
u:117 [binder, in MetaCoq.Template.common.uGraph]
u:117 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:117 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:1187 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:119 [binder, in MetaCoq.Template.EtaExpand]
u:119 [binder, in MetaCoq.Template.Universes]
u:119 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:119 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
U:1191 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1191 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:1194 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:1195 [binder, in MetaCoq.PCUIC.PCUICConfluence]
U:1197 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1199 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:12 [binder, in MetaCoq.Erasure.EInduction]
u:12 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:12 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:12 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:120 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:120 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:120 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:1203 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:1207 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:121 [binder, in MetaCoq.Erasure.EArities]
u:121 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:121 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:1211 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:1215 [binder, in MetaCoq.PCUIC.PCUICReduction]
U:1216 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1219 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:122 [binder, in MetaCoq.Template.Universes]
u:122 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:122 [binder, in MetaCoq.Template.WfAst]
u:122 [binder, in MetaCoq.Template.common.uGraph]
u:122 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:122 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:122 [binder, in MetaCoq.Erasure.EEtaExpanded]
u:1225 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1227 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1230 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1231 [binder, in MetaCoq.PCUIC.PCUICConfluence]
U:1237 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1239 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:124 [binder, in MetaCoq.Template.Universes]
u:124 [binder, in MetaCoq.Translations.param_cheap_packed]
u:124 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:124 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:124 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
U:1243 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:1249 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:125 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:125 [binder, in MetaCoq.Template.WfAst]
u:125 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:125 [binder, in MetaCoq.Template.common.uGraph]
u:125 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:125 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:125 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:1252 [binder, in MetaCoq.PCUIC.PCUICConfluence]
U:1255 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1255 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:126 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:126 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:126 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:126 [binder, in MetaCoq.Erasure.Prelim]
u:1261 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
U:1263 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1265 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:127 [binder, in MetaCoq.Template.Universes]
u:127 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:127 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:127 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:1270 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1271 [binder, in MetaCoq.PCUIC.PCUICConfluence]
U:1277 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:128 [binder, in MetaCoq.Template.Typing]
u:128 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:128 [binder, in MetaCoq.PCUIC.PCUICInductives]
U:128 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:128 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:128 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:1283 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:1287 [binder, in MetaCoq.Template.Typing]
u:129 [binder, in MetaCoq.Template.Universes]
u:129 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:129 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:129 [binder, in MetaCoq.Template.common.uGraph]
u:129 [binder, in MetaCoq.Erasure.ELiftSubst]
u:1290 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:1299 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:13 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:13 [binder, in MetaCoq.Template.TermEquality]
u:13 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:13 [binder, in MetaCoq.Erasure.ErasureFunction]
u:13 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:13 [binder, in MetaCoq.Template.UnivSubst]
u:13 [binder, in MetaCoq.Template.LiftSubst]
u:130 [binder, in MetaCoq.Template.Universes]
u:130 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:130 [binder, in MetaCoq.Template.Typing]
u:130 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:130 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:130 [binder, in MetaCoq.Translations.param_cheap_packed]
u:130 [binder, in MetaCoq.Template.WcbvEval]
u:131 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:1317 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:132 [binder, in MetaCoq.Template.Universes]
u:132 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:1325 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:133 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:133 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:133 [binder, in MetaCoq.Template.common.uGraph]
u:133 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:133 [binder, in MetaCoq.Erasure.ELiftSubst]
u:133 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u:134 [binder, in MetaCoq.Template.Universes]
u:134 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
U:134 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:134 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:134 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:135 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:135 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:135 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:135 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:135 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:136 [binder, in MetaCoq.Template.Universes]
u:136 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:136 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:136 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:1360 [binder, in MetaCoq.Erasure.ErasureFunction]
u:137 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:137 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:137 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:137 [binder, in MetaCoq.Template.common.uGraph]
u:1374 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1378 [binder, in MetaCoq.Erasure.ErasureFunction]
u:138 [binder, in MetaCoq.Template.Universes]
U:138 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:138 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:138 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:138 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:1384 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1386 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
U:139 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:139 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:14 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:14 [binder, in MetaCoq.PCUIC.PCUICCSubst]
u:14 [binder, in MetaCoq.Erasure.ELiftSubst]
u:14 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
u:14 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:140 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:140 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:140 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:140 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:1400 [binder, in MetaCoq.Erasure.ErasureFunction]
u:1406 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:141 [binder, in MetaCoq.Template.Universes]
u:141 [binder, in MetaCoq.Erasure.EArities]
u:141 [binder, in MetaCoq.Template.WfAst]
u:141 [binder, in MetaCoq.Template.common.uGraph]
U:141 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
U:141 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:141 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:1413 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:1416 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:1424 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:143 [binder, in MetaCoq.Template.EtaExpand]
u:143 [binder, in MetaCoq.Template.Universes]
u:143 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:143 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:143 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:143 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:144 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:144 [binder, in MetaCoq.PCUIC.PCUICArities]
u:145 [binder, in MetaCoq.Erasure.EArities]
u:145 [binder, in MetaCoq.Template.WfAst]
u:145 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:145 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:146 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:146 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:146 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:146 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:146 [binder, in MetaCoq.Template.common.uGraph]
u:146 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:146 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:146 [binder, in MetaCoq.PCUIC.PCUICReduction]
U:147 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:147 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:147 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:149 [binder, in MetaCoq.Template.Universes]
u:149 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:149 [binder, in MetaCoq.Erasure.EArities]
u:149 [binder, in MetaCoq.PCUIC.PCUICArities]
u:149 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
U:149 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:1494 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:15 [binder, in MetaCoq.Template.EtaExpand]
u:15 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:15 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:15 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:15 [binder, in MetaCoq.Translations.sigma]
u:15 [binder, in MetaCoq.PCUIC.PCUICSN]
u:15 [binder, in MetaCoq.Erasure.ErasureProperties]
u:15 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:15 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:15 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:150 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:150 [binder, in MetaCoq.Template.WfAst]
U:150 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:150 [binder, in MetaCoq.Template.common.uGraph]
U:150 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:150 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:150 [binder, in MetaCoq.Template.AstUtils]
u:151 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:151 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:151 [binder, in MetaCoq.Template.AstUtils]
u:152 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:152 [binder, in MetaCoq.Template.Universes]
u:152 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:152 [binder, in MetaCoq.PCUIC.PCUICInversion]
u:1522 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:1528 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:153 [binder, in MetaCoq.Template.Universes]
u:153 [binder, in MetaCoq.Erasure.EArities]
u:153 [binder, in MetaCoq.Template.WfAst]
u:153 [binder, in MetaCoq.Template.TypingWf]
u:154 [binder, in MetaCoq.Template.Universes]
u:154 [binder, in MetaCoq.Template.common.uGraph]
u:155 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:155 [binder, in MetaCoq.Template.TermEquality]
u:155 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:156 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:156 [binder, in MetaCoq.PCUIC.PCUICArities]
u:156 [binder, in MetaCoq.Template.WfAst]
u:156 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:156 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:157 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:158 [binder, in MetaCoq.Erasure.EArities]
u:158 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:158 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
U:158 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:158 [binder, in MetaCoq.PCUIC.PCUICSR]
u:158 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:159 [binder, in MetaCoq.Template.Universes]
u:159 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:16 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:16 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:16 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
u:16 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:16 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:16 [binder, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
u:16 [binder, in MetaCoq.Template.UnivSubst]
u:16 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:160 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:160 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:160 [binder, in MetaCoq.Template.WcbvEval]
u:160 [binder, in MetaCoq.Template.AstUtils]
u:161 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:162 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:162 [binder, in MetaCoq.Erasure.EArities]
U:162 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:162 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:162 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:162 [binder, in MetaCoq.Template.LiftSubst]
u:162 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:1620 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:163 [binder, in MetaCoq.Template.Universes]
u:164 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:164 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
U:164 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:164 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:165 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:165 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:165 [binder, in MetaCoq.Template.TypingWf]
u:166 [binder, in MetaCoq.Template.Universes]
u:166 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:166 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:167 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:168 [binder, in MetaCoq.Template.WcbvEval]
u:168 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:168 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:169 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:169 [binder, in MetaCoq.Erasure.ERemoveParams]
u:17 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:17 [binder, in MetaCoq.Template.Normal]
u:17 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:17 [binder, in MetaCoq.PCUIC.PCUICCSubst]
u:17 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:17 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:17 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:171 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
U:171 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:172 [binder, in MetaCoq.Examples.tauto]
u:173 [binder, in MetaCoq.Template.Universes]
u:173 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:1734 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
U:174 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
U:174 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:174 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:174 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:174 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:175 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:175 [binder, in MetaCoq.Erasure.EArities]
u:175 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:176 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u:176 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:176 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:176 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:176 [binder, in MetaCoq.Template.TypingWf]
u:176 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:1762 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:177 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:177 [binder, in MetaCoq.PCUIC.PCUICAst]
u:178 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:178 [binder, in MetaCoq.Template.Checker]
u:178 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:178 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:1781 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:1786 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:179 [binder, in MetaCoq.PCUIC.PCUICArities]
u:179 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:179 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:1792 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:18 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:18 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
u:18 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:18 [binder, in MetaCoq.PCUIC.PCUICGeneration]
u:18 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:18 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:18 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:18 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:18 [binder, in MetaCoq.Erasure.ECSubst]
u:18 [binder, in MetaCoq.Template.UnivSubst]
u:18 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:180 [binder, in MetaCoq.Erasure.EArities]
u:180 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:180 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:180 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:180 [binder, in MetaCoq.Template.WcbvEval]
u:181 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:181 [binder, in MetaCoq.Template.Universes]
u:181 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:181 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:182 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
U:183 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:184 [binder, in MetaCoq.Template.TermEquality]
u:184 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u:184 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:184 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:185 [binder, in MetaCoq.Template.Universes]
u:185 [binder, in MetaCoq.Erasure.EArities]
u:185 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:185 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:185 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:186 [binder, in MetaCoq.Template.EtaExpand]
u:186 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:187 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:187 [binder, in MetaCoq.Template.TermEquality]
u:187 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:188 [binder, in MetaCoq.PCUIC.PCUICAst]
u:189 [binder, in MetaCoq.Template.EtaExpand]
u:189 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:19 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:19 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
u:19 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:19 [binder, in MetaCoq.Erasure.ErasureFunction]
u:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:19 [binder, in MetaCoq.Translations.MiniHoTT]
u:19 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:19 [binder, in MetaCoq.Template.AstUtils]
u:190 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:190 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:190 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:190 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:191 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:191 [binder, in MetaCoq.Erasure.EArities]
u:191 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:191 [binder, in MetaCoq.Template.Checker]
u:193 [binder, in MetaCoq.Template.EtaExpand]
u:194 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:194 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:194 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:194 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u:195 [binder, in MetaCoq.PCUIC.PCUICArities]
u:195 [binder, in MetaCoq.Template.TermEquality]
u:195 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
u:195 [binder, in MetaCoq.PCUIC.PCUICSR]
u:1952 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:196 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:196 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:197 [binder, in MetaCoq.Template.Universes]
u:197 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:198 [binder, in MetaCoq.Template.Universes]
u:198 [binder, in MetaCoq.Template.TermEquality]
u:198 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:199 [binder, in MetaCoq.PCUIC.PCUICArities]
u:2 [binder, in MetaCoq.Template.TermEquality]
u:2 [binder, in MetaCoq.Erasure.ErasureProperties]
u:20 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:20 [binder, in MetaCoq.Template.Normal]
u:20 [binder, in MetaCoq.PCUIC.PCUICSN]
u:20 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:20 [binder, in MetaCoq.Erasure.EAst]
u:20 [binder, in MetaCoq.Template.Checker]
u:20 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:20 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:20 [binder, in MetaCoq.Erasure.ECSubst]
u:200 [binder, in MetaCoq.Template.Ast]
u:201 [binder, in MetaCoq.Template.TermEquality]
u:201 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:201 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:201 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:202 [binder, in MetaCoq.Template.Ast]
u:202 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:202 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
u:202 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:203 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:203 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:203 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:204 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:205 [binder, in MetaCoq.PCUIC.PCUICArities]
u:205 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:205 [binder, in MetaCoq.Template.Ast]
u:206 [binder, in MetaCoq.Erasure.EInduction]
u:207 [binder, in MetaCoq.Template.Universes]
u:207 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:207 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:207 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:2078 [binder, in MetaCoq.Translations.MiniHoTT]
u:2086 [binder, in MetaCoq.Translations.MiniHoTT]
u:2086 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:209 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:209 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:209 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:209 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2094 [binder, in MetaCoq.Translations.MiniHoTT]
u:2094 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2101 [binder, in MetaCoq.Translations.MiniHoTT]
u:2102 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2108 [binder, in MetaCoq.Translations.MiniHoTT]
u:2109 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:211 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:211 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2116 [binder, in MetaCoq.Translations.MiniHoTT]
u:2116 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:212 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:2124 [binder, in MetaCoq.Translations.MiniHoTT]
u:2124 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:213 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:2131 [binder, in MetaCoq.Translations.MiniHoTT]
u:2132 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2138 [binder, in MetaCoq.Translations.MiniHoTT]
u:2139 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:214 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:214 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:2145 [binder, in MetaCoq.Translations.MiniHoTT]
u:2146 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:215 [binder, in MetaCoq.Template.Universes]
u:215 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:215 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2152 [binder, in MetaCoq.Translations.MiniHoTT]
u:2153 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2159 [binder, in MetaCoq.Translations.MiniHoTT]
u:216 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:2160 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2167 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:217 [binder, in MetaCoq.Template.Universes]
u:217 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:217 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:217 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u:218 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:219 [binder, in MetaCoq.Template.Universes]
u:219 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:219 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:219 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:22 [binder, in MetaCoq.Examples.typing_correctness]
u:22 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
u:22 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:22 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:22 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:22 [binder, in MetaCoq.Template.UnivSubst]
U:220 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:221 [binder, in MetaCoq.Template.Universes]
u:221 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:221 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:221 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:221 [binder, in MetaCoq.PCUIC.PCUICAst]
u:221 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:222 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:222 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:222 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:223 [binder, in MetaCoq.Template.Universes]
u:224 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:224 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:224 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:224 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
u:224 [binder, in MetaCoq.Template.WcbvEval]
U:224 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:225 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:225 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:226 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:227 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:227 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:227 [binder, in MetaCoq.Template.TermEquality]
u:228 [binder, in MetaCoq.Template.EtaExpand]
u:228 [binder, in MetaCoq.Template.Universes]
u:228 [binder, in MetaCoq.PCUIC.PCUICConversion]
U:228 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:229 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:229 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:23 [binder, in MetaCoq.Erasure.EArities]
u:23 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:23 [binder, in MetaCoq.Erasure.EDeps]
u:23 [binder, in MetaCoq.PCUIC.PCUICSN]
u:23 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:23 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:23 [binder, in MetaCoq.Erasure.ECSubst]
u:23 [binder, in MetaCoq.Template.Induction]
u:23 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:230 [binder, in MetaCoq.Template.Universes]
u:231 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:231 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:232 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:232 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:232 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:232 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:233 [binder, in MetaCoq.Template.Universes]
u:233 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:233 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:234 [binder, in MetaCoq.Template.Universes]
u:234 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:234 [binder, in MetaCoq.Erasure.EArities]
u:234 [binder, in MetaCoq.Template.Ast]
u:234 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:234 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:234 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:235 [binder, in MetaCoq.Template.Universes]
u:236 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:236 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:236 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:237 [binder, in MetaCoq.Template.Universes]
u:237 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:238 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
U:238 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:238 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:239 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:24 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:24 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:24 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
u:24 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:24 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:24 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:240 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:240 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:240 [binder, in MetaCoq.PCUIC.PCUICAst]
U:2403 [binder, in MetaCoq.Template.utils.All_Forall]
u:241 [binder, in MetaCoq.Template.Universes]
u:242 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:242 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:242 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:242 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:243 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:244 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
U:244 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:245 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:246 [binder, in MetaCoq.Template.Universes]
u:246 [binder, in MetaCoq.Template.Ast]
u:246 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:247 [binder, in MetaCoq.Template.WcbvEval]
u:247 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:248 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:248 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:248 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:25 [binder, in MetaCoq.Template.WfAst]
u:25 [binder, in MetaCoq.PCUIC.PCUICValidity]
u:25 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
u:25 [binder, in MetaCoq.Erasure.ELiftSubst]
u:25 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:25 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:25 [binder, in MetaCoq.Template.UnivSubst]
u:25 [binder, in MetaCoq.Template.Induction]
u:251 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:251 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:252 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:252 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:253 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:253 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:253 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:254 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:254 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:254 [binder, in MetaCoq.Template.WcbvEval]
u:255 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:255 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:255 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:256 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:257 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:257 [binder, in MetaCoq.Erasure.EArities]
U:257 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:257 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:258 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:258 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:259 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
U:259 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:26 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:26 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:26 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:26 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:26 [binder, in MetaCoq.Erasure.ECSubst]
u:261 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:261 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:261 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
U:262 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
U:262 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:263 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:2637 [binder, in MetaCoq.Translations.MiniHoTT]
U:264 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:264 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2640 [binder, in MetaCoq.Translations.MiniHoTT]
u:2645 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2647 [binder, in MetaCoq.Translations.MiniHoTT]
u:2648 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:265 [binder, in MetaCoq.Template.Universes]
u:265 [binder, in MetaCoq.Erasure.EArities]
u:265 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:2655 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2657 [binder, in MetaCoq.Translations.MiniHoTT]
u:266 [binder, in MetaCoq.Template.Typing]
u:266 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2660 [binder, in MetaCoq.Translations.MiniHoTT]
u:2665 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2666 [binder, in MetaCoq.Translations.MiniHoTT]
u:2668 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:267 [binder, in MetaCoq.Template.Ast]
u:267 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2672 [binder, in MetaCoq.Translations.MiniHoTT]
u:2674 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:268 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:268 [binder, in MetaCoq.Template.Universes]
u:268 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:268 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:268 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:268 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2680 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:269 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:27 [binder, in MetaCoq.Template.WfAst]
u:27 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:27 [binder, in MetaCoq.PCUIC.PCUICSN]
u:27 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:27 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:27 [binder, in MetaCoq.Template.UnivSubst]
u:27 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
u:270 [binder, in MetaCoq.Template.Universes]
U:270 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:270 [binder, in MetaCoq.PCUIC.PCUICAlpha]
U:270 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:270 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2700 [binder, in MetaCoq.Translations.MiniHoTT]
u:2705 [binder, in MetaCoq.Translations.MiniHoTT]
u:2708 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:271 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2711 [binder, in MetaCoq.Translations.MiniHoTT]
u:2713 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2717 [binder, in MetaCoq.Translations.MiniHoTT]
u:2719 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:272 [binder, in MetaCoq.Template.Universes]
u:272 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
U:272 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:272 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2724 [binder, in MetaCoq.Translations.MiniHoTT]
u:2725 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2729 [binder, in MetaCoq.Translations.MiniHoTT]
u:273 [binder, in MetaCoq.Erasure.EArities]
u:273 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:273 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2732 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2737 [binder, in MetaCoq.Translations.MiniHoTT]
u:2737 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:274 [binder, in MetaCoq.Template.Universes]
u:274 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:2743 [binder, in MetaCoq.Translations.MiniHoTT]
u:2745 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2749 [binder, in MetaCoq.Translations.MiniHoTT]
u:275 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:275 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2751 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2756 [binder, in MetaCoq.Translations.MiniHoTT]
u:2757 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:276 [binder, in MetaCoq.Template.Universes]
u:276 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:276 [binder, in MetaCoq.Template.common.uGraph]
u:276 [binder, in MetaCoq.PCUIC.PCUICAlpha]
U:276 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:2761 [binder, in MetaCoq.Translations.MiniHoTT]
u:2764 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2769 [binder, in MetaCoq.Translations.MiniHoTT]
u:2769 [binder, in MetaCoq.Translations.MiniHoTT_paths]
U:277 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:277 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:277 [binder, in MetaCoq.Template.common.uGraph]
u:2775 [binder, in MetaCoq.Translations.MiniHoTT]
u:2777 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:278 [binder, in MetaCoq.Template.Universes]
u:2780 [binder, in MetaCoq.Translations.MiniHoTT]
u:2783 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2784 [binder, in MetaCoq.Translations.MiniHoTT]
u:2788 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2789 [binder, in MetaCoq.Translations.MiniHoTT]
u:279 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:279 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:2792 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2797 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:28 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:28 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:28 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:28 [binder, in MetaCoq.Template.Induction]
U:280 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:281 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:281 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2818 [binder, in MetaCoq.Translations.MiniHoTT]
u:282 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:282 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:282 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:2821 [binder, in MetaCoq.Translations.MiniHoTT]
u:2826 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2828 [binder, in MetaCoq.Translations.MiniHoTT]
u:2829 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:283 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:283 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:2836 [binder, in MetaCoq.Translations.MiniHoTT_paths]
U:284 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:284 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:284 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:284 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:284 [binder, in MetaCoq.PCUIC.PCUICSR]
u:285 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:285 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:285 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:286 [binder, in MetaCoq.Template.Universes]
u:286 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:286 [binder, in MetaCoq.Template.Ast]
u:286 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:286 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:2860 [binder, in MetaCoq.Translations.MiniHoTT]
u:2868 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:2869 [binder, in MetaCoq.Translations.MiniHoTT]
u:287 [binder, in MetaCoq.Template.Checker]
u:2877 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:288 [binder, in MetaCoq.Template.EtaExpand]
u:288 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:289 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:289 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:289 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:289 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:29 [binder, in MetaCoq.Template.WfAst]
u:29 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
u:29 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:290 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:290 [binder, in MetaCoq.Template.Universes]
u:290 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:291 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:291 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:291 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:2919 [binder, in MetaCoq.Translations.MiniHoTT]
u:292 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:2927 [binder, in MetaCoq.Translations.MiniHoTT]
u:2927 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:293 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:293 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:293 [binder, in MetaCoq.Template.Ast]
u:2935 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:294 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:294 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:295 [binder, in MetaCoq.Template.Universes]
u:295 [binder, in MetaCoq.Erasure.EArities]
U:295 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:295 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:296 [binder, in MetaCoq.Template.Universes]
u:297 [binder, in MetaCoq.PCUIC.PCUICSR]
U:298 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:298 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:298 [binder, in MetaCoq.Template.Typing]
u:299 [binder, in MetaCoq.Template.Universes]
u:299 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:299 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:3 [binder, in MetaCoq.PCUIC.PCUICCSubst]
u:3 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
u:3 [binder, in MetaCoq.Template.WcbvEval]
u:3 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:3 [binder, in MetaCoq.Erasure.ECSubst]
u:3 [binder, in MetaCoq.Template.UnivSubst]
u:30 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
u:30 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:300 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:301 [binder, in MetaCoq.Erasure.EArities]
u:301 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
U:301 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:302 [binder, in MetaCoq.Template.Typing]
u:303 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:304 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:304 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:304 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:305 [binder, in MetaCoq.Template.Universes]
U:305 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:305 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:305 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:306 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:306 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:306 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:307 [binder, in MetaCoq.Template.Environment]
u:308 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:308 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:309 [binder, in MetaCoq.Template.Universes]
u:309 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:309 [binder, in MetaCoq.PCUIC.PCUICSR]
u:31 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:31 [binder, in MetaCoq.PCUIC.PCUICValidity]
u:31 [binder, in MetaCoq.Template.Normal]
u:31 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:31 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:31 [binder, in MetaCoq.Erasure.EAstUtils]
u:310 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:311 [binder, in MetaCoq.Template.Universes]
u:311 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:311 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:312 [binder, in MetaCoq.PCUIC.PCUICElimination]
U:312 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:312 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:312 [binder, in MetaCoq.Template.TypingWf]
u:312 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:313 [binder, in MetaCoq.Template.Universes]
u:314 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:314 [binder, in MetaCoq.Template.WcbvEval]
u:315 [binder, in MetaCoq.Template.Universes]
u:315 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:315 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:316 [binder, in MetaCoq.Template.TypingWf]
u:317 [binder, in MetaCoq.Template.Universes]
u:317 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:317 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:318 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:318 [binder, in MetaCoq.Template.TypingWf]
U:319 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:32 [binder, in MetaCoq.Template.WfAst]
u:32 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:32 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
u:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:32 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:32 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
u:320 [binder, in MetaCoq.Template.Universes]
U:320 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:320 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:321 [binder, in MetaCoq.Template.Checker]
u:321 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:322 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:322 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:322 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:323 [binder, in MetaCoq.Template.Universes]
u:323 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:323 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:323 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:324 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:325 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:325 [binder, in MetaCoq.Template.Universes]
u:325 [binder, in MetaCoq.Template.Ast]
u:325 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:325 [binder, in MetaCoq.Template.TypingWf]
U:326 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:327 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:327 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:328 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:328 [binder, in MetaCoq.Template.Ast]
u:328 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:329 [binder, in MetaCoq.Template.Universes]
u:329 [binder, in MetaCoq.Erasure.EArities]
u:329 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:33 [binder, in MetaCoq.Translations.times_bool_fun]
U:33 [binder, in MetaCoq.PCUIC.PCUICArities]
u:33 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:330 [binder, in MetaCoq.Erasure.ERemoveParams]
u:331 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:331 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:331 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:332 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:332 [binder, in MetaCoq.PCUIC.PCUICSR]
u:333 [binder, in MetaCoq.Template.common.uGraph]
u:333 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:335 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:336 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:336 [binder, in MetaCoq.Template.TypingWf]
u:338 [binder, in MetaCoq.Template.common.uGraph]
u:338 [binder, in MetaCoq.PCUIC.PCUICSR]
u:338 [binder, in MetaCoq.Template.TypingWf]
u:339 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:339 [binder, in MetaCoq.Template.common.uGraph]
u:339 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:339 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:34 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:34 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:34 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:34 [binder, in MetaCoq.Erasure.EAstUtils]
u:34 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:341 [binder, in MetaCoq.Template.Universes]
u:342 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:342 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:343 [binder, in MetaCoq.Template.Universes]
u:343 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:343 [binder, in MetaCoq.Template.common.uGraph]
u:344 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:345 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:346 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:346 [binder, in MetaCoq.Erasure.EWcbvEval]
u:347 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:347 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:349 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:349 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:35 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:35 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:35 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:350 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:350 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
U:351 [binder, in MetaCoq.Erasure.EArities]
u:351 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:351 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:351 [binder, in MetaCoq.Template.common.uGraph]
u:351 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:352 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:352 [binder, in MetaCoq.Template.TypingWf]
u:353 [binder, in MetaCoq.Template.common.uGraph]
u:353 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:353 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:354 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:354 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:355 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:355 [binder, in MetaCoq.Template.TypingWf]
u:356 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:356 [binder, in MetaCoq.PCUIC.PCUICSR]
u:356 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:356 [binder, in MetaCoq.Erasure.EWcbvEval]
u:36 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:36 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:36 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
u:360 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:360 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:362 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:363 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:364 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:364 [binder, in MetaCoq.Template.utils.wGraph]
u:365 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:366 [binder, in MetaCoq.Template.common.uGraph]
u:366 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:367 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:368 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:369 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
u:369 [binder, in MetaCoq.Template.utils.wGraph]
u:369 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:37 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:37 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:37 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:37 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:37 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:370 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:370 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:370 [binder, in MetaCoq.Translations.MiniHoTT]
u:371 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:372 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:373 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:375 [binder, in MetaCoq.PCUIC.PCUICProgress]
U:375 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:375 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:376 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:377 [binder, in MetaCoq.Translations.MiniHoTT]
u:378 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:378 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:379 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:379 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:379 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:379 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:38 [binder, in MetaCoq.Erasure.Extract]
u:38 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:38 [binder, in MetaCoq.PCUIC.PCUICSN]
u:38 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:38 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:380 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:380 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:382 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:383 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:383 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:384 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:384 [binder, in MetaCoq.Translations.MiniHoTT]
u:384 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:385 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:385 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:386 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:387 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:387 [binder, in MetaCoq.PCUIC.PCUICSR]
u:388 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:388 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:388 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:389 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:389 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:389 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:389 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:389 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:39 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:39 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:390 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
U:391 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:391 [binder, in MetaCoq.Translations.MiniHoTT]
u:391 [binder, in MetaCoq.PCUIC.PCUICSR]
u:392 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:392 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:393 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:393 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:394 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:394 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:395 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:395 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:396 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:397 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:398 [binder, in MetaCoq.Translations.MiniHoTT]
u:399 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
U:399 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:399 [binder, in MetaCoq.Template.common.uGraph]
u:399 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:4 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:40 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:40 [binder, in MetaCoq.PCUIC.PCUICArities]
u:40 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:40 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:40 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:40 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:40 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
u:40 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:401 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
U:402 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:403 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:404 [binder, in MetaCoq.PCUIC.PCUICProgress]
U:404 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:404 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:405 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:406 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:406 [binder, in MetaCoq.Translations.MiniHoTT]
u:406 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:406 [binder, in MetaCoq.Translations.MiniHoTT_paths]
U:407 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:408 [binder, in MetaCoq.Template.EtaExpand]
u:408 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:41 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:41 [binder, in MetaCoq.PCUIC.PCUICSN]
U:41 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:41 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:410 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:410 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:412 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:412 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:414 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
u:414 [binder, in MetaCoq.Translations.MiniHoTT]
u:414 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:414 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:414 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:415 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:417 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:417 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:418 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:418 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:419 [binder, in MetaCoq.Template.EtaExpand]
u:419 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:42 [binder, in MetaCoq.Erasure.Extract]
u:42 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:42 [binder, in MetaCoq.PCUIC.PCUICAlpha]
u:42 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:42 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:42 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:42 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:42 [binder, in MetaCoq.Template.TypingWf]
u:420 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:420 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:422 [binder, in MetaCoq.Translations.MiniHoTT]
u:422 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:423 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
U:427 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:427 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:428 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:428 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:429 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:429 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:43 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:43 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:43 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:43 [binder, in MetaCoq.Template.TermEquality]
u:43 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:43 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
u:43 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:43 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
u:43 [binder, in MetaCoq.Erasure.ELiftSubst]
u:43 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:43 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:430 [binder, in MetaCoq.Template.Universes]
u:430 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:431 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:431 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:431 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:432 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:433 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:434 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:435 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:436 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:437 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:44 [binder, in MetaCoq.PCUIC.PCUICElimination]
u:44 [binder, in MetaCoq.PCUIC.PCUICSN]
u:44 [binder, in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
u:444 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:444 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:444 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:446 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:447 [binder, in MetaCoq.Template.EnvironmentTyping]
u:447 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:447 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:448 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:449 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:449 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:45 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:45 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:45 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
u:45 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:45 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:45 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:450 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:451 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:451 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:451 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:454 [binder, in MetaCoq.Template.Typing]
u:455 [binder, in MetaCoq.Template.common.uGraph]
u:456 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:457 [binder, in MetaCoq.Template.Universes]
u:458 [binder, in MetaCoq.Template.common.uGraph]
u:459 [binder, in MetaCoq.Template.Typing]
u:459 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:46 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:46 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:46 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:46 [binder, in MetaCoq.Erasure.ELiftSubst]
u:46 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u:460 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:461 [binder, in MetaCoq.Template.common.uGraph]
u:461 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:463 [binder, in MetaCoq.Template.Universes]
u:463 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:463 [binder, in MetaCoq.Template.common.uGraph]
u:463 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:464 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:464 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:465 [binder, in MetaCoq.Template.Universes]
U:466 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:466 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:466 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:467 [binder, in MetaCoq.Template.Typing]
u:467 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:467 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:468 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:469 [binder, in MetaCoq.Template.Typing]
u:469 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:469 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:47 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:47 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:47 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:47 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:47 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:471 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:471 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:472 [binder, in MetaCoq.Template.Typing]
u:472 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:473 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:474 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:475 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:475 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
u:475 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:476 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:478 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:478 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:48 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:48 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:48 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:48 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:480 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:480 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:480 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:481 [binder, in MetaCoq.Template.common.uGraph]
u:481 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:483 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:484 [binder, in MetaCoq.Template.common.uGraph]
u:485 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:485 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:486 [binder, in MetaCoq.Template.Typing]
u:486 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:486 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:486 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:487 [binder, in MetaCoq.Template.common.uGraph]
u:487 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:487 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:488 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:488 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:489 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:489 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:49 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:49 [binder, in MetaCoq.Erasure.EArities]
u:49 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:49 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
u:49 [binder, in MetaCoq.Erasure.ELiftSubst]
u:49 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:490 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:492 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:492 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:493 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:493 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:495 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:495 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:497 [binder, in MetaCoq.Template.Universes]
u:498 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:499 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:5 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:5 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:5 [binder, in MetaCoq.Erasure.Extract]
u:5 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
u:5 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
u:50 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
u:50 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:50 [binder, in MetaCoq.PCUIC.PCUICSN]
u:50 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:501 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:501 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:502 [binder, in MetaCoq.Template.Universes]
u:502 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:505 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:506 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:507 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
u:509 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:51 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
U:51 [binder, in MetaCoq.PCUIC.PCUICValidity]
u:51 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:51 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:510 [binder, in MetaCoq.PCUIC.PCUICEquality]
U:511 [binder, in MetaCoq.PCUIC.PCUICSR]
u:512 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:513 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:513 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:514 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:517 [binder, in MetaCoq.PCUIC.PCUICSR]
u:517 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:518 [binder, in MetaCoq.Template.EnvironmentTyping]
u:519 [binder, in MetaCoq.Template.Universes]
u:519 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:52 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:52 [binder, in MetaCoq.Erasure.EArities]
u:52 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:52 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:520 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:521 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:522 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:522 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:523 [binder, in MetaCoq.Template.Universes]
u:524 [binder, in MetaCoq.Template.common.uGraph]
u:524 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
U:524 [binder, in MetaCoq.PCUIC.PCUICSR]
u:525 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:525 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:525 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:526 [binder, in MetaCoq.Template.common.uGraph]
u:527 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:527 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:53 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:53 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:53 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:53 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:53 [binder, in MetaCoq.Template.AstUtils]
u:530 [binder, in MetaCoq.Template.Typing]
u:531 [binder, in MetaCoq.Template.EnvironmentTyping]
U:531 [binder, in MetaCoq.PCUIC.PCUICSR]
u:532 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:534 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:535 [binder, in MetaCoq.Template.Universes]
u:535 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:536 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:537 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:538 [binder, in MetaCoq.Template.Universes]
U:538 [binder, in MetaCoq.PCUIC.PCUICSR]
u:538 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:539 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:54 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:54 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:54 [binder, in MetaCoq.Template.Checker]
u:54 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:540 [binder, in MetaCoq.Template.common.uGraph]
u:542 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:542 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:542 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:545 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:547 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:547 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:547 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:548 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:548 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:548 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:55 [binder, in MetaCoq.Translations.times_bool_fun]
u:55 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:55 [binder, in MetaCoq.PCUIC.PCUICNormal]
u:55 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:55 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:55 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:552 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:556 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:558 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:558 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:559 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:56 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:56 [binder, in MetaCoq.Template.Normal]
u:56 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
u:56 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:560 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:563 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:5642 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:5649 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:565 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:565 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:566 [binder, in MetaCoq.Template.Universes]
u:566 [binder, in MetaCoq.Template.Typing]
U:566 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:567 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:567 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:569 [binder, in MetaCoq.Template.Universes]
u:569 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:57 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:57 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
u:57 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:57 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:57 [binder, in MetaCoq.Template.Checker]
u:57 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:57 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:571 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:571 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:572 [binder, in MetaCoq.Template.Universes]
u:573 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:576 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:577 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:577 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:579 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:58 [binder, in MetaCoq.Erasure.EInduction]
u:58 [binder, in MetaCoq.Template.utils.ReflectEq]
u:58 [binder, in MetaCoq.PCUIC.PCUICSN]
u:58 [binder, in MetaCoq.Erasure.ErasureProperties]
u:580 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:584 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:586 [binder, in MetaCoq.Template.EnvironmentTyping]
u:587 [binder, in MetaCoq.PCUIC.PCUICSR]
u:588 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:59 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:59 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:59 [binder, in MetaCoq.Template.Normal]
u:59 [binder, in MetaCoq.Template.Checker]
u:591 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:591 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:592 [binder, in MetaCoq.PCUIC.PCUICSR]
u:596 [binder, in MetaCoq.PCUIC.PCUICSR]
u:596 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:6 [binder, in MetaCoq.PCUIC.PCUICElimination]
U:6 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:6 [binder, in MetaCoq.Template.utils.MCEquality]
u:6 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
u:6 [binder, in MetaCoq.Template.monad_utils]
u:6 [binder, in MetaCoq.Template.UnivSubst]
u:6 [binder, in MetaCoq.Translations.param_generous_packed]
u:60 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
u:60 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:60 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:60 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:60 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
u:601 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:604 [binder, in MetaCoq.PCUIC.PCUICSR]
u:606 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:609 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:61 [binder, in MetaCoq.Erasure.EInduction]
u:61 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:61 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:61 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:61 [binder, in MetaCoq.Template.Environment]
u:61 [binder, in MetaCoq.PCUIC.PCUICContexts]
u:610 [binder, in MetaCoq.PCUIC.PCUICSR]
u:611 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
U:612 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:613 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:617 [binder, in MetaCoq.Template.utils.wGraph]
u:619 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:62 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:62 [binder, in MetaCoq.PCUIC.PCUICSN]
u:62 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:62 [binder, in MetaCoq.Template.Pretty]
u:62 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
u:62 [binder, in MetaCoq.Template.Induction]
u:620 [binder, in MetaCoq.Template.Universes]
u:620 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
u:620 [binder, in MetaCoq.Template.utils.wGraph]
U:621 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
U:622 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:622 [binder, in MetaCoq.PCUIC.PCUICSR]
u:623 [binder, in MetaCoq.Template.Universes]
u:623 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:623 [binder, in MetaCoq.Template.utils.wGraph]
u:625 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:625 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:626 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:626 [binder, in MetaCoq.Template.utils.wGraph]
u:628 [binder, in MetaCoq.Template.Universes]
u:628 [binder, in MetaCoq.PCUIC.PCUICSR]
u:628 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:630 [binder, in MetaCoq.Template.utils.wGraph]
u:630 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:632 [binder, in MetaCoq.Template.Universes]
u:632 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:632 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:633 [binder, in MetaCoq.Template.Typing]
u:633 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:634 [binder, in MetaCoq.Template.utils.wGraph]
u:636 [binder, in MetaCoq.Template.Universes]
u:636 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:637 [binder, in MetaCoq.Template.Typing]
u:637 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:639 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:64 [binder, in MetaCoq.Erasure.EInduction]
u:64 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:64 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:64 [binder, in MetaCoq.Template.Induction]
u:642 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:643 [binder, in MetaCoq.Template.Typing]
u:644 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:644 [binder, in MetaCoq.Template.utils.wGraph]
u:647 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:648 [binder, in MetaCoq.Template.utils.wGraph]
u:648 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:649 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:65 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:65 [binder, in MetaCoq.Template.Checker]
u:65 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:650 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:651 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:653 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:653 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:654 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:656 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:657 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:659 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:66 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:66 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
U:66 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:660 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:661 [binder, in MetaCoq.Template.Universes]
u:662 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:663 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:663 [binder, in MetaCoq.Template.utils.wGraph]
u:664 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:665 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:665 [binder, in MetaCoq.Template.Typing]
u:665 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:666 [binder, in MetaCoq.Template.utils.wGraph]
u:668 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:668 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:669 [binder, in MetaCoq.Template.utils.wGraph]
u:67 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:67 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:67 [binder, in MetaCoq.Translations.param_original]
u:67 [binder, in MetaCoq.Template.Induction]
u:670 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:671 [binder, in MetaCoq.Template.Universes]
u:671 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:672 [binder, in MetaCoq.Template.utils.wGraph]
u:674 [binder, in MetaCoq.Template.utils.All_Forall]
u:674 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:674 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:674 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:675 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:677 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:678 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:678 [binder, in MetaCoq.Template.utils.wGraph]
u:679 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:679 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:68 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:68 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:68 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
u:68 [binder, in MetaCoq.Translations.param_cheap_packed]
u:68 [binder, in MetaCoq.Template.WcbvEval]
u:68 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:68 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
u:680 [binder, in MetaCoq.Template.EnvironmentTyping]
u:680 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:682 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:682 [binder, in MetaCoq.Template.utils.wGraph]
u:682 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:686 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:686 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:687 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:687 [binder, in MetaCoq.PCUIC.PCUICConfluence]
U:687 [binder, in MetaCoq.PCUIC.PCUICSR]
u:689 [binder, in MetaCoq.Template.EnvironmentTyping]
u:689 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:689 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:69 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:69 [binder, in MetaCoq.Erasure.EArities]
u:69 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:69 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:69 [binder, in MetaCoq.Template.Checker]
u:69 [binder, in MetaCoq.Translations.MiniHoTT]
u:69 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:692 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:692 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:694 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:696 [binder, in MetaCoq.Template.utils.wGraph]
u:696 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:698 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
U:699 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:699 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:7 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:7 [binder, in MetaCoq.Template.TermEquality]
u:7 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:7 [binder, in MetaCoq.Template.LiftSubst]
u:70 [binder, in MetaCoq.Template.Normal]
u:70 [binder, in MetaCoq.PCUIC.PCUICInversion]
u:70 [binder, in MetaCoq.Translations.param_original]
u:700 [binder, in MetaCoq.Template.utils.wGraph]
u:700 [binder, in MetaCoq.PCUIC.PCUICSR]
u:701 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:703 [binder, in MetaCoq.PCUIC.PCUICEquality]
U:704 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:705 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:707 [binder, in MetaCoq.PCUIC.PCUICEquality]
U:708 [binder, in MetaCoq.PCUIC.PCUICSR]
u:71 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:71 [binder, in MetaCoq.Translations.param_binary]
u:71 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:71 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:71 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
u:71 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:710 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:710 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:710 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:711 [binder, in MetaCoq.Template.Universes]
u:712 [binder, in MetaCoq.Translations.MiniHoTT]
u:714 [binder, in MetaCoq.Template.Universes]
u:716 [binder, in MetaCoq.Template.Universes]
U:716 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:716 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:719 [binder, in MetaCoq.Template.Universes]
U:719 [binder, in MetaCoq.Template.Typing]
u:72 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:720 [binder, in MetaCoq.Translations.MiniHoTT]
u:720 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:722 [binder, in MetaCoq.Template.Universes]
u:723 [binder, in MetaCoq.Template.Universes]
u:723 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:725 [binder, in MetaCoq.PCUIC.PCUICSR]
u:726 [binder, in MetaCoq.Template.Universes]
U:727 [binder, in MetaCoq.Template.EnvironmentTyping]
u:727 [binder, in MetaCoq.PCUIC.PCUICEquality]
u:727 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:728 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:729 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:729 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:73 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:73 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
U:73 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:73 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:730 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u:732 [binder, in MetaCoq.Template.Universes]
u:732 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:732 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:733 [binder, in MetaCoq.Template.Universes]
u:735 [binder, in MetaCoq.Template.Universes]
u:735 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:735 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u:736 [binder, in MetaCoq.Template.Universes]
u:737 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:738 [binder, in MetaCoq.Template.Universes]
U:738 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:74 [binder, in MetaCoq.Translations.param_binary]
u:74 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
u:74 [binder, in MetaCoq.Translations.MiniHoTT]
u:740 [binder, in MetaCoq.Template.Universes]
u:740 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:742 [binder, in MetaCoq.Template.Universes]
u:742 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:742 [binder, in MetaCoq.PCUIC.PCUICConversion]
U:743 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:744 [binder, in MetaCoq.Template.Universes]
u:744 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:744 [binder, in MetaCoq.Translations.MiniHoTT]
u:746 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:748 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:75 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
u:75 [binder, in MetaCoq.Erasure.ErasureProperties]
u:75 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:750 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:752 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:752 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:754 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:755 [binder, in MetaCoq.Template.Universes]
u:755 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:757 [binder, in MetaCoq.Template.Universes]
u:757 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:758 [binder, in MetaCoq.PCUIC.PCUICSR]
u:759 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:76 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:76 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:76 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
u:76 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:76 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
u:76 [binder, in MetaCoq.Template.WcbvEval]
u:76 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:76 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:76 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
U:761 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:762 [binder, in MetaCoq.Template.Universes]
u:762 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:762 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:763 [binder, in MetaCoq.Translations.MiniHoTT]
u:763 [binder, in MetaCoq.PCUIC.PCUICSR]
u:764 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:766 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:767 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:768 [binder, in MetaCoq.Template.Universes]
u:77 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:77 [binder, in MetaCoq.PCUIC.PCUICInversion]
u:77 [binder, in MetaCoq.Erasure.ErasureProperties]
u:77 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:77 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:770 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:770 [binder, in MetaCoq.PCUIC.PCUICSR]
u:771 [binder, in MetaCoq.Translations.MiniHoTT]
u:771 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:776 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:778 [binder, in MetaCoq.PCUIC.PCUICSR]
u:779 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:78 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:78 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:78 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:780 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
U:781 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:784 [binder, in MetaCoq.PCUIC.PCUICSR]
u:786 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:79 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:79 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
U:79 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
u:79 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:790 [binder, in MetaCoq.PCUIC.PCUICSR]
u:795 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:796 [binder, in MetaCoq.PCUIC.PCUICSR]
u:799 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:8 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:8 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
u:8 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
u:8 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:8 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:80 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:80 [binder, in MetaCoq.Erasure.EArities]
u:80 [binder, in MetaCoq.Erasure.EWellformed]
u:80 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:80 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:80 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
u:80 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:800 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:801 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:803 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:804 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:804 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:81 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:817 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:82 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:82 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:82 [binder, in MetaCoq.Template.Checker]
u:82 [binder, in MetaCoq.Translations.MiniHoTT_paths]
u:83 [binder, in MetaCoq.PCUIC.PCUICProgress]
u:83 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:83 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
U:83 [binder, in MetaCoq.PCUIC.PCUICArities]
u:83 [binder, in MetaCoq.Erasure.EWellformed]
u:83 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:830 [binder, in MetaCoq.PCUIC.PCUICSpine]
u:838 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:839 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:84 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:84 [binder, in MetaCoq.PCUIC.PCUICInductives]
u:84 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:841 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:842 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:843 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
u:845 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:848 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:85 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:85 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
u:85 [binder, in MetaCoq.Erasure.ErasureProperties]
u:85 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:85 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
u:851 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:854 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:855 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:857 [binder, in MetaCoq.Template.utils.All_Forall]
u:857 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:857 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:86 [binder, in MetaCoq.Template.TermEquality]
u:86 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:86 [binder, in MetaCoq.Template.WcbvEval]
u:86 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:86 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
u:863 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:865 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:866 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:868 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
u:87 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:87 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:87 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:872 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:879 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:88 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
u:88 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
u:88 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:88 [binder, in MetaCoq.Template.Checker]
u:883 [binder, in MetaCoq.PCUIC.PCUICConfluence]
U:883 [binder, in MetaCoq.PCUIC.PCUICSR]
u:889 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:89 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:89 [binder, in MetaCoq.Template.TermEquality]
u:89 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:896 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:897 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:897 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:9 [binder, in MetaCoq.Template.Typing]
u:9 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
u:90 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:90 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:90 [binder, in MetaCoq.PCUIC.PCUICInversion]
u:90 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:90 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:902 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:906 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:91 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:91 [binder, in MetaCoq.Erasure.EArities]
u:91 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
u:915 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:92 [binder, in MetaCoq.Template.WfAst]
u:92 [binder, in MetaCoq.Template.TermEquality]
u:92 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
u:92 [binder, in MetaCoq.PCUIC.PCUICConversion]
u:92 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
u:922 [binder, in MetaCoq.Template.Typing]
u:922 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:924 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:925 [binder, in MetaCoq.Template.Typing]
u:928 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:93 [binder, in MetaCoq.Template.EnvironmentTyping]
u:93 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:93 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
U:933 [binder, in MetaCoq.Template.Typing]
u:933 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:94 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
u:94 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:94 [binder, in MetaCoq.Template.WfAst]
u:94 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:94 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:95 [binder, in MetaCoq.PCUIC.PCUICInversion]
u:95 [binder, in MetaCoq.PCUIC.PCUICAst]
u:95 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
u:95 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:95 [binder, in MetaCoq.Template.LiftSubst]
u:955 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:96 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:96 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:96 [binder, in MetaCoq.Template.TermEquality]
u:96 [binder, in MetaCoq.SafeChecker.PCUICErrors]
u:96 [binder, in MetaCoq.Erasure.ErasureProperties]
u:96 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:961 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:961 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:97 [binder, in MetaCoq.Template.WfAst]
u:97 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
u:972 [binder, in MetaCoq.PCUIC.PCUICConfluence]
u:973 [binder, in MetaCoq.PCUIC.PCUICTyping]
u:975 [binder, in MetaCoq.Template.Typing]
u:975 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:978 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:98 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
u:98 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:98 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:98 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:981 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:984 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:984 [binder, in MetaCoq.PCUIC.PCUICReduction]
u:987 [binder, in MetaCoq.Erasure.ErasureFunction]
u:99 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:99 [binder, in MetaCoq.Template.Typing]
u:99 [binder, in MetaCoq.Erasure.Extract]
u:99 [binder, in MetaCoq.Template.LiftSubst]
U:999 [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) |