| 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) |
L
labelling_of_valuation [definition, in MetaCoq.Template.common.uGraph]lam [constructor, in MetaCoq.Examples.add_constructor]
LambdaNotConvertibleAnn [constructor, in MetaCoq.SafeChecker.PCUICErrors]
LambdaNotConvertibleTypes [constructor, in MetaCoq.SafeChecker.PCUICErrors]
Lambda_bd [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Lambda_ty [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Lambda_conv_cum_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
lam_tm [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
lam_ty [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
last_nonempty_eq [lemma, in MetaCoq.Template.utils.MCList]
last_app [lemma, in MetaCoq.Template.utils.MCList]
last_inv [lemma, in MetaCoq.Template.utils.MCList]
lazy [constructor, in MetaCoq.Template.TemplateMonad.Common]
leA:100 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leA:140 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leA:17 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leA:3 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leA:39 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leA:46 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leA:58 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leA:75 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
leA:98 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
leb_spec_Set [lemma, in MetaCoq.Template.utils.MCArith]
leb_S [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
leb_spect [lemma, in MetaCoq.PCUIC.PCUICFirstorder]
leB:106 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leB:107 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
leB:142 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leB:23 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leB:40 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leB:47 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leB:5 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leB:64 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
leB:84 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
left_dlexmod [constructor, in MetaCoq.PCUIC.utils.PCUICUtils]
left_lex [constructor, in MetaCoq.PCUIC.utils.PCUICUtils]
Lemmata [section, in MetaCoq.PCUIC.PCUICSafeLemmata]
len [projection, in MetaCoq.PCUIC.PCUICAst]
len [constructor, in MetaCoq.PCUIC.PCUICAst]
lengths [definition, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
lengths [definition, in MetaCoq.PCUIC.Syntax.PCUICTactics]
length_nil [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
length_of [abbreviation, in MetaCoq.PCUIC.PCUICAst]
lenm_eq [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
len:1004 [binder, in MetaCoq.Template.utils.All_Forall]
leqb_levelalg_n:512 [binder, in MetaCoq.Template.Universes]
leqb_universe_n_ [definition, in MetaCoq.Template.Universes]
leqb_univ_expr_n_spec' [lemma, in MetaCoq.Template.common.uGraph]
leqb_universe [definition, in MetaCoq.Template.common.uGraph]
leqb_levelalg_n_spec [lemma, in MetaCoq.Template.common.uGraph]
leqb_levelalg_n_spec0 [lemma, in MetaCoq.Template.common.uGraph]
leqb_levelalg_n [definition, in MetaCoq.Template.common.uGraph]
leqb_expr_univ_n_spec [lemma, in MetaCoq.Template.common.uGraph]
leqb_expr_univ_n_spec0 [lemma, in MetaCoq.Template.common.uGraph]
leqb_expr_univ_n [definition, in MetaCoq.Template.common.uGraph]
leqb_expr_n_spec [lemma, in MetaCoq.Template.common.uGraph]
leqb_expr_n_spec0 [lemma, in MetaCoq.Template.common.uGraph]
leqb_expr_n [definition, in MetaCoq.Template.common.uGraph]
leqb_level_n_spec [lemma, in MetaCoq.Template.common.uGraph]
leqb_level_n_spec0 [lemma, in MetaCoq.Template.common.uGraph]
leqb_level_n [definition, in MetaCoq.Template.common.uGraph]
leqb_term [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
leqb_term_spec [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
leqb_term [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
leqb:285 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leqb:316 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leqty:239 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
lequ:12 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:121 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:132 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:150 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:171 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:178 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:188 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:202 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:21 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:224 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:31 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:37 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:62 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:69 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq_prop_is_prop_sprop [lemma, in MetaCoq.Template.Universes]
leq_sprop_sprop [lemma, in MetaCoq.Template.Universes]
leq_prop_prop [lemma, in MetaCoq.Template.Universes]
leq_universe_sprop_l [lemma, in MetaCoq.Template.Universes]
leq_universe_prop_no_prop_sub_type [lemma, in MetaCoq.Template.Universes]
leq_universe_sprop_r [lemma, in MetaCoq.Template.Universes]
leq_universe_prop_r [lemma, in MetaCoq.Template.Universes]
leq_universe_props [lemma, in MetaCoq.Template.Universes]
leq_universe_super [lemma, in MetaCoq.Template.Universes]
leq_universe_product_mon [lemma, in MetaCoq.Template.Universes]
leq_universe_subset [lemma, in MetaCoq.Template.Universes]
leq_universe_refl' [definition, in MetaCoq.Template.Universes]
leq_universe_partial_order [instance, in MetaCoq.Template.Universes]
leq_universe_antisym [instance, in MetaCoq.Template.Universes]
leq_universe_preorder [instance, in MetaCoq.Template.Universes]
leq_levelalg_partial_order [instance, in MetaCoq.Template.Universes]
leq_levelalg_antisym [instance, in MetaCoq.Template.Universes]
leq_levelalg_preorder [instance, in MetaCoq.Template.Universes]
leq_universe_product [lemma, in MetaCoq.Template.Universes]
leq_universe_sup_r [lemma, in MetaCoq.Template.Universes]
leq_universe_sup_l [lemma, in MetaCoq.Template.Universes]
leq_levelalg_sup0_mon [lemma, in MetaCoq.Template.Universes]
leq_levelalg_sup0_r [lemma, in MetaCoq.Template.Universes]
leq_levelalg_sup0_l [lemma, in MetaCoq.Template.Universes]
leq_universe_trans [instance, in MetaCoq.Template.Universes]
leq_universe_n_trans [instance, in MetaCoq.Template.Universes]
leq_levelalg_n_trans [instance, in MetaCoq.Template.Universes]
leq_universe_refl [instance, in MetaCoq.Template.Universes]
leq_levelalg_n_refl [instance, in MetaCoq.Template.Universes]
leq_universe_leq_universe_n [lemma, in MetaCoq.Template.Universes]
leq_levelalg_leq_levelalg_n [lemma, in MetaCoq.Template.Universes]
leq_universe [definition, in MetaCoq.Template.Universes]
leq_levelalg [definition, in MetaCoq.Template.Universes]
leq_universe_n [definition, in MetaCoq.Template.Universes]
leq_levelalg_n:505 [binder, in MetaCoq.Template.Universes]
leq_universe_n_ [definition, in MetaCoq.Template.Universes]
leq_levelalg_n [definition, in MetaCoq.Template.Universes]
leq_cuniverse_antisym [instance, in MetaCoq.Template.Universes]
leq_cuniverse_preorder [instance, in MetaCoq.Template.Universes]
leq_cuniverse_trans [instance, in MetaCoq.Template.Universes]
leq_cuniverse_n_trans [instance, in MetaCoq.Template.Universes]
leq_cuniverse_refl [instance, in MetaCoq.Template.Universes]
leq_cuniv_of_product_mon [lemma, in MetaCoq.Template.Universes]
leq_cuniverse [definition, in MetaCoq.Template.Universes]
leq_cuniverse_n [definition, in MetaCoq.Template.Universes]
leq_term_sprop_sorted_r [lemma, in MetaCoq.PCUIC.PCUICElimination]
leq_term_propositional_sorted_l [lemma, in MetaCoq.PCUIC.PCUICElimination]
leq_term_sprop_sorted_l [lemma, in MetaCoq.PCUIC.PCUICElimination]
leq_term_prop_sorted_r [lemma, in MetaCoq.PCUIC.PCUICElimination]
leq_term_prop_sorted_l [lemma, in MetaCoq.PCUIC.PCUICElimination]
leq_universe_propositional_l [lemma, in MetaCoq.PCUIC.PCUICElimination]
leq_term_mkApps [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
leq_term_App [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
leq_term_leq_term_napp [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
leq_term_ext [definition, in MetaCoq.PCUIC.PCUICCumulativity]
leq_universe_propositional_l [lemma, in MetaCoq.Erasure.EArities]
leq_universe_propositional_r [lemma, in MetaCoq.Erasure.EArities]
leq_term_propopositional_sorted_r [lemma, in MetaCoq.Erasure.EArities]
leq_term_propositional_sorted_l [lemma, in MetaCoq.Erasure.EArities]
leq_universe_sort_of_products_mon [lemma, in MetaCoq.PCUIC.PCUICArities]
leq_term_nocast [definition, in MetaCoq.Template.Typing]
leq_term_App [lemma, in MetaCoq.Template.TermEquality]
leq_term_mkApps [lemma, in MetaCoq.Template.TermEquality]
leq_term_refl [lemma, in MetaCoq.Template.TermEquality]
leq_term [abbreviation, in MetaCoq.Template.TermEquality]
leq_term:46 [binder, in MetaCoq.Template.TermEquality]
leq_term_subset [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
leq_term_napp [abbreviation, in MetaCoq.PCUIC.PCUICCumulProp]
leq_term_eq_term_prop_impl [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
leq_universe_prop_spec [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
leq_levelalg_vertices [lemma, in MetaCoq.Template.common.uGraph]
leq_levelalg_vertices1 [lemma, in MetaCoq.Template.common.uGraph]
leq_levelalg_vertices0 [lemma, in MetaCoq.Template.common.uGraph]
leq_term_leq_term_napp [lemma, in MetaCoq.PCUIC.PCUICEquality]
leq_term_partial_order [instance, in MetaCoq.PCUIC.PCUICEquality]
leq_term_antisym [instance, in MetaCoq.PCUIC.PCUICEquality]
leq_term_preorder [instance, in MetaCoq.PCUIC.PCUICEquality]
leq_context_preord [instance, in MetaCoq.PCUIC.PCUICEquality]
leq_context [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
leq_decl [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
leq_term [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
leq_term:110 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:108 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:106 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:104 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:102 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:100 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:94 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:84 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term':76 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:74 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term':71 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:69 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term':67 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:65 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term:49 [binder, in MetaCoq.PCUIC.PCUICEquality]
leq_term_propositional_sorted_l [lemma, in MetaCoq.Erasure.ErasureFunction]
leq_term [definition, in MetaCoq.Template.Checker]
leq_term_napp [abbreviation, in MetaCoq.PCUIC.PCUICPrincipality]
leq_term_empty_leq_term [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
leq_term_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_universe_subst_instance [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_universe_SubstUnivPreserving [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_context_cumul_context [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
leq_universe_sort_of_products [lemma, in MetaCoq.PCUIC.PCUICSpine]
leq_universeP [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq0_levelalg_n [definition, in MetaCoq.Template.Universes]
leq0_level_n_complete [lemma, in MetaCoq.Template.common.uGraph]
leq0_level_n [definition, in MetaCoq.Template.common.uGraph]
leq:101 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:107 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:113 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:1235 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:1236 [binder, in MetaCoq.PCUIC.PCUICConfluence]
leq:127 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:128 [binder, in MetaCoq.SafeChecker.PCUICErrors]
leq:139 [binder, in MetaCoq.SafeChecker.PCUICErrors]
leq:139 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:151 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:157 [binder, in MetaCoq.SafeChecker.PCUICErrors]
leq:161 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:2077 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2100 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2112 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2121 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2135 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:214 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:222 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:228 [binder, in MetaCoq.Template.Checker]
leq:235 [binder, in MetaCoq.Template.Checker]
leq:237 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:247 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
leq:253 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2552 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2559 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:273 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:278 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:283 [binder, in MetaCoq.PCUIC.PCUICConfluence]
leq:326 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:352 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:370 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:375 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:380 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:4414 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:4566 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:510 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:517 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:52 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:523 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:5233 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:529 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:536 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:549 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:55 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:5655 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5666 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5677 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5687 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5699 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5707 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:59 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:648 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:654 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:66 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:663 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:669 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:677 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:690 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:696 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:708 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:72 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:8 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:824 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:826 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:85 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:877 [binder, in MetaCoq.PCUIC.PCUICConversion]
leq:92 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:94 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:99 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
leterm:380 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
letin_red_body [constructor, in MetaCoq.Template.Typing]
letin_red_ty [constructor, in MetaCoq.Template.Typing]
letin_red_def [constructor, in MetaCoq.Template.Typing]
LetIn_in [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
LetIn_ty [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
LetIn_bd [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
letin_red_body [constructor, in MetaCoq.PCUIC.PCUICReduction]
letin_red_ty [constructor, in MetaCoq.PCUIC.PCUICReduction]
letin_red_def [constructor, in MetaCoq.PCUIC.PCUICReduction]
lets_in_constructor_types [projection, in MetaCoq.Template.config]
lets:821 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
let_expansion_obseq [definition, in MetaCoq.PCUIC.PCUICTransform]
let_in [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
let_ty [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
let_bd [constructor, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Level [module, in MetaCoq.Template.Universes]
LevelAlgExpr [module, in MetaCoq.Template.Universes]
LevelAlgExpr.eq_dec_univ0 [instance, in MetaCoq.Template.Universes]
LevelAlgExpr.Evaluable [instance, in MetaCoq.Template.Universes]
LevelAlgExpr.exprs [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.get_is_level [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.is_level [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.is_levels [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.levelexprset_reflect [instance, in MetaCoq.Template.Universes]
LevelAlgExpr.make [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.make' [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.succ [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.sup [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.t [definition, in MetaCoq.Template.Universes]
LevelAlgExpr.val_make' [lemma, in MetaCoq.Template.Universes]
LevelAlgExpr.val_make [lemma, in MetaCoq.Template.Universes]
levelalg_get_is_level_correct [lemma, in MetaCoq.Template.Universes]
LevelExpr [module, in MetaCoq.Template.Universes]
LevelExprSet [module, in MetaCoq.Template.Universes]
LevelExprSetFact [module, in MetaCoq.Template.Universes]
LevelExprSetProp [module, in MetaCoq.Template.Universes]
levelexprset_eq_dec [instance, in MetaCoq.Template.Universes]
levelexprset_reflect [instance, in MetaCoq.Template.Universes]
LevelExprSet_For_all [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
LevelExpr.compare [definition, in MetaCoq.Template.Universes]
LevelExpr.compare_spec [definition, in MetaCoq.Template.Universes]
LevelExpr.eq [definition, in MetaCoq.Template.Universes]
LevelExpr.eq_leibniz [definition, in MetaCoq.Template.Universes]
LevelExpr.eq_dec [definition, in MetaCoq.Template.Universes]
LevelExpr.eq_equiv [definition, in MetaCoq.Template.Universes]
LevelExpr.Evaluable [instance, in MetaCoq.Template.Universes]
LevelExpr.from_kernel_repr [definition, in MetaCoq.Template.Universes]
LevelExpr.get_noprop [definition, in MetaCoq.Template.Universes]
LevelExpr.get_level [definition, in MetaCoq.Template.Universes]
LevelExpr.is_level [definition, in MetaCoq.Template.Universes]
LevelExpr.lt [definition, in MetaCoq.Template.Universes]
LevelExpr.ltLevelExpr1 [constructor, in MetaCoq.Template.Universes]
LevelExpr.ltLevelExpr2 [constructor, in MetaCoq.Template.Universes]
LevelExpr.lt_compat [definition, in MetaCoq.Template.Universes]
LevelExpr.lt_strorder [instance, in MetaCoq.Template.Universes]
LevelExpr.lt_ [inductive, in MetaCoq.Template.Universes]
LevelExpr.make [definition, in MetaCoq.Template.Universes]
LevelExpr.reflect_t [instance, in MetaCoq.Template.Universes]
LevelExpr.set [definition, in MetaCoq.Template.Universes]
LevelExpr.succ [definition, in MetaCoq.Template.Universes]
LevelExpr.t [definition, in MetaCoq.Template.Universes]
LevelExpr.to_kernel_repr [definition, in MetaCoq.Template.Universes]
LevelExpr.type1 [definition, in MetaCoq.Template.Universes]
LevelExpr.val_make_npl [lemma, in MetaCoq.Template.Universes]
LevelExpr.val_make [lemma, in MetaCoq.Template.Universes]
LevelIn_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
LevelSet [module, in MetaCoq.Template.Universes]
LevelSetDecide [module, in MetaCoq.Template.Universes]
LevelSetFact [module, in MetaCoq.Template.Universes]
LevelSetMoreFacts [section, in MetaCoq.Template.Universes]
LevelSetProp [module, in MetaCoq.Template.Universes]
LevelSetsUIP [module, in MetaCoq.Template.Reflect]
LevelSetsUIP.eqb_LevelSet [definition, in MetaCoq.Template.Reflect]
LevelSetsUIP.levels_tree_reflect [instance, in MetaCoq.Template.Reflect]
LevelSetsUIP.levels_tree_rect [definition, in MetaCoq.Template.Reflect]
LevelSetsUIP.levels_tree_eqb [definition, in MetaCoq.Template.Reflect]
LevelSetsUIP.ok_irrel [lemma, in MetaCoq.Template.Reflect]
LevelSetsUIP.reflect_LevelSet [instance, in MetaCoq.Template.Reflect]
LevelSet_union_empty [lemma, in MetaCoq.Template.Universes]
LevelSet_In_fold_right_add [lemma, in MetaCoq.Template.Universes]
LevelSet_mem_union [definition, in MetaCoq.Template.Universes]
LevelSet_pair_In [lemma, in MetaCoq.Template.Universes]
LevelSet_pair [definition, in MetaCoq.Template.Universes]
levelset_for_all_eq [lemma, in MetaCoq.Template.common.uGraph]
LevelSet_in_union_global [lemma, in MetaCoq.PCUIC.PCUICGlobalEnv]
levels_of_udecl [definition, in MetaCoq.Template.Universes]
levels_univ_gc_declared_declared [lemma, in MetaCoq.Template.common.uGraph]
levels_gc_declared_declared [lemma, in MetaCoq.Template.common.uGraph]
levels_global_ext_constraint [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_global_constraint [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_global_levels_declared [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
levels1:611 [binder, in MetaCoq.Template.common.uGraph]
levels2:612 [binder, in MetaCoq.Template.common.uGraph]
levels:1 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
levels:1019 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
levels:200 [binder, in MetaCoq.SafeChecker.PCUICErrors]
levels:401 [binder, in MetaCoq.Template.Universes]
levels:404 [binder, in MetaCoq.Template.Universes]
levels:468 [binder, in MetaCoq.Template.EnvironmentTyping]
levels:520 [binder, in MetaCoq.Template.common.uGraph]
levels:537 [binder, in MetaCoq.Template.common.uGraph]
levels:665 [binder, in MetaCoq.Template.common.uGraph]
levels:671 [binder, in MetaCoq.Template.EnvironmentTyping]
levels:79 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
levels:80 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
level_var_instance_length [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
level_gc_declared_declared [lemma, in MetaCoq.Template.common.uGraph]
level_mem [definition, in MetaCoq.SafeChecker.PCUICWfEnv]
level_lt_ind_dep [definition, in MetaCoq.Template.Reflect]
Level.compare [definition, in MetaCoq.Template.Universes]
Level.compare_spec [definition, in MetaCoq.Template.Universes]
Level.eq [definition, in MetaCoq.Template.Universes]
Level.eqb [definition, in MetaCoq.Template.Universes]
Level.eqb_spec [lemma, in MetaCoq.Template.Universes]
Level.eqb_refl [instance, in MetaCoq.Template.Universes]
Level.eq_dec [definition, in MetaCoq.Template.Universes]
Level.eq_leibniz [definition, in MetaCoq.Template.Universes]
Level.eq_level [definition, in MetaCoq.Template.Universes]
Level.eq_equiv [definition, in MetaCoq.Template.Universes]
Level.Evaluable [instance, in MetaCoq.Template.Universes]
Level.is_var [definition, in MetaCoq.Template.Universes]
Level.is_set [definition, in MetaCoq.Template.Universes]
Level.Level [constructor, in MetaCoq.Template.Universes]
Level.lt [definition, in MetaCoq.Template.Universes]
Level.ltLevelLevel [constructor, in MetaCoq.Template.Universes]
Level.ltLevelVar [constructor, in MetaCoq.Template.Universes]
Level.ltSetLevel [constructor, in MetaCoq.Template.Universes]
Level.ltSetVar [constructor, in MetaCoq.Template.Universes]
Level.ltVarVar [constructor, in MetaCoq.Template.Universes]
Level.lt_compat [definition, in MetaCoq.Template.Universes]
Level.lt_strorder [definition, in MetaCoq.Template.Universes]
Level.lt_ [inductive, in MetaCoq.Template.Universes]
Level.lzero [constructor, in MetaCoq.Template.Universes]
Level.reflect_level [instance, in MetaCoq.Template.Universes]
Level.t [definition, in MetaCoq.Template.Universes]
Level.t_ [inductive, in MetaCoq.Template.Universes]
Level.Var [constructor, in MetaCoq.Template.Universes]
lexprod [definition, in MetaCoq.PCUIC.utils.PCUICUtils]
le_irrel [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
le_ind_prop [definition, in MetaCoq.Template.Reflect]
le':758 [binder, in MetaCoq.PCUIC.PCUICSpine]
le:114 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:120 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:1232 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:126 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:16 [binder, in MetaCoq.PCUIC.PCUICInversion]
le:172 [binder, in MetaCoq.SafeChecker.PCUICErrors]
le:191 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
le:199 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
le:203 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
le:270 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
le:346 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
le:354 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
le:359 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
le:362 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
le:365 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
le:382 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
le:393 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
le:393 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
le:402 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
le:406 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
le:463 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
le:505 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:52 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
le:54 [binder, in MetaCoq.PCUIC.PCUICArities]
le:55 [binder, in MetaCoq.PCUIC.PCUICArities]
le:569 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
le:583 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
le:611 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
le:627 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
le:63 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:679 [binder, in MetaCoq.PCUIC.PCUICSR]
le:69 [binder, in MetaCoq.PCUIC.PCUICSR]
le:745 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:749 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:751 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:756 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:77 [binder, in MetaCoq.PCUIC.PCUICSR]
le:82 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
le:85 [binder, in MetaCoq.PCUIC.PCUICAlpha]
le:90 [binder, in MetaCoq.PCUIC.PCUICAlpha]
le:92 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
le:939 [binder, in MetaCoq.PCUIC.PCUICConversion]
le:944 [binder, in MetaCoq.PCUIC.PCUICConversion]
le:947 [binder, in MetaCoq.PCUIC.PCUICConversion]
le:95 [binder, in MetaCoq.PCUIC.PCUICAlpha]
le:953 [binder, in MetaCoq.PCUIC.PCUICConversion]
lH:159 [binder, in MetaCoq.Translations.param_cheap_packed]
liat [abbreviation, in MetaCoq.PCUIC.PCUICValidity]
LibHypsNaming [library]
lift [definition, in MetaCoq.Template.Ast]
lift [definition, in MetaCoq.PCUIC.PCUICAst]
lift [definition, in MetaCoq.Erasure.ELiftSubst]
liftP_ctx [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
liftP_ctx_ind [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
LiftSubst [library]
lift_ctx [definition, in MetaCoq.Template.EtaExpand]
lift_unlift_context [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift_term [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
lift_isLambda [lemma, in MetaCoq.Erasure.ESubstitution]
lift_inst_case_branch_context [lemma, in MetaCoq.Erasure.ESubstitution]
lift_isApp [lemma, in MetaCoq.Template.WfAst]
lift_to_wf_list [lemma, in MetaCoq.Template.WfAst]
lift_to_list [lemma, in MetaCoq.Template.WfAst]
lift_context_subst [lemma, in MetaCoq.PCUIC.PCUICInductives]
lift_context_expand_lets_ctx [lemma, in MetaCoq.PCUIC.PCUICInductives]
lift_context_subst_context_let_expand [lemma, in MetaCoq.PCUIC.PCUICInductives]
lift_context_lift_context [lemma, in MetaCoq.PCUIC.PCUICInductives]
lift_instance_length [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
lift_iota_red [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
lift_rename' [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
lift_leq_term [lemma, in MetaCoq.PCUIC.PCUICEquality]
lift_eq_term [lemma, in MetaCoq.PCUIC.PCUICEquality]
lift_compare_context [lemma, in MetaCoq.PCUIC.PCUICEquality]
lift_compare_decls [lemma, in MetaCoq.PCUIC.PCUICEquality]
lift_compare_term [lemma, in MetaCoq.PCUIC.PCUICEquality]
lift_renaming_0 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_rename [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_renaming_0_rshift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_renaming_spec [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_renaming [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_fix_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_mutual_inductive_body [definition, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_context_lift_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_expand_lets_k [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
lift_closed [lemma, in MetaCoq.Erasure.ELiftSubst]
lift_mkApps [lemma, in MetaCoq.Erasure.ELiftSubst]
lift_isApp [lemma, in MetaCoq.Erasure.ELiftSubst]
lift_rel_alt [lemma, in MetaCoq.Erasure.ELiftSubst]
lift_rel_lt [lemma, in MetaCoq.Erasure.ELiftSubst]
lift_rel_ge [lemma, in MetaCoq.Erasure.ELiftSubst]
lift_declared_constant [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
lift_to_pred [lemma, in MetaCoq.PCUIC.PCUICConfluence]
lift_to_ws_red [lemma, in MetaCoq.PCUIC.PCUICConfluence]
lift_ws [definition, in MetaCoq.PCUIC.PCUICConfluence]
lift_context_add [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
lift_decl_closed [lemma, in MetaCoq.PCUIC.Syntax.PCUICClosed]
lift_extended_subst' [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_extended_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_alt [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc0 [definition, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_length [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_decl0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_to_extended_list_k [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_closed [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_mkApps [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_isApp [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_lt [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_ge [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc [lemma, in MetaCoq.Template.TypingWf]
lift_context_snoc0 [definition, in MetaCoq.Template.TypingWf]
lift_to_extended_list_k [lemma, in MetaCoq.Template.LiftSubst]
lift_closed [lemma, in MetaCoq.Template.LiftSubst]
lift_mkApps [lemma, in MetaCoq.Template.LiftSubst]
lift_rel_lt [lemma, in MetaCoq.Template.LiftSubst]
lift_rel_ge [lemma, in MetaCoq.Template.LiftSubst]
lift_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICSpine]
lift_context0_app [lemma, in MetaCoq.PCUIC.PCUICSpine]
lift_context_subst_context [lemma, in MetaCoq.PCUIC.PCUICSpine]
lift0 [abbreviation, in MetaCoq.Template.Ast]
lift0 [abbreviation, in MetaCoq.PCUIC.PCUICAst]
lift0 [abbreviation, in MetaCoq.Erasure.ELiftSubst]
lift0_rename [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift0_open [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
lift0_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
lift0_p [lemma, in MetaCoq.Erasure.ELiftSubst]
lift0_id [lemma, in MetaCoq.Erasure.ELiftSubst]
lift0_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift0_p [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift0_id [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift0_inst_id [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
lift0_p [lemma, in MetaCoq.Template.LiftSubst]
lift0_id [lemma, in MetaCoq.Template.LiftSubst]
ListOrderedType [module, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_trans [lemma, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_lt_lt [lemma, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_sym [lemma, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_refl [lemma, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_eq [lemma, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_spec [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eq [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eqb [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eqb_dec [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eq_dec [instance, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eq_leibniz [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eq_equiv [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt [definition, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt_compat [instance, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt_strorder [instance, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt_cons_cons_tl [constructor, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt_cons_cons_hd [constructor, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt_nil_cons [constructor, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt_ [inductive, in MetaCoq.Template.utils.MCCompare]
ListOrderedType.t [definition, in MetaCoq.Template.utils.MCCompare]
ListSize [section, in MetaCoq.Template.utils.MCList]
ListSizeMap [section, in MetaCoq.Template.utils.MCList]
list_size_map_hom [lemma, in MetaCoq.Template.utils.MCList]
list_size_map_le [lemma, in MetaCoq.Template.utils.MCList]
list_size_mapi_le [lemma, in MetaCoq.Template.utils.MCList]
list_size_mapi_rec_le [lemma, in MetaCoq.Template.utils.MCList]
list_size_map_eq [lemma, in MetaCoq.Template.utils.MCList]
list_size_mapi_eq [lemma, in MetaCoq.Template.utils.MCList]
list_size_mapi_rec_eq [lemma, in MetaCoq.Template.utils.MCList]
list_size_map [lemma, in MetaCoq.Template.utils.MCList]
list_size_length [lemma, in MetaCoq.Template.utils.MCList]
list_size_rev [lemma, in MetaCoq.Template.utils.MCList]
list_size_app [lemma, in MetaCoq.Template.utils.MCList]
list_size [definition, in MetaCoq.Template.utils.MCList]
list_rect_rev [lemma, in MetaCoq.Template.utils.MCList]
list_ind_rev [lemma, in MetaCoq.Template.utils.MCList]
list_size_length [lemma, in MetaCoq.Examples.tauto]
list_length_rev_ind [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
list_size_rev [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
list_size_mapi_context_hom [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
list_depth_mapi_rec_le [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_depth_rev [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_depth_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_depth [abbreviation, in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_depth_gen [definition, in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_length_ind [lemma, in MetaCoq.Template.LiftSubst]
list_map_swap_eq' [lemma, in MetaCoq.PCUIC.PCUICReduction]
list_map_swap_eq [lemma, in MetaCoq.PCUIC.PCUICReduction]
list_split_eq [lemma, in MetaCoq.PCUIC.PCUICReduction]
list_context [inductive, in MetaCoq.PCUIC.PCUICReduction]
LI:100 [binder, in MetaCoq.Translations.times_bool_fun]
LI:101 [binder, in MetaCoq.Translations.times_bool_fun]
lls:111 [binder, in MetaCoq.Examples.tauto]
lls:120 [binder, in MetaCoq.Examples.tauto]
lls:77 [binder, in MetaCoq.Examples.tauto]
ll:164 [binder, in MetaCoq.PCUIC.PCUICConfluence]
ll:165 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Loader [library]
Loader [library]
Loader [library]
LocalAssum [constructor, in MetaCoq.PCUIC.PCUICAst]
LocalAssum [constructor, in MetaCoq.Erasure.EAst]
localassum_cons_def [constructor, in MetaCoq.PCUIC.PCUICElimination]
localassum_cons_abs [constructor, in MetaCoq.PCUIC.PCUICElimination]
localassum_nil [constructor, in MetaCoq.PCUIC.PCUICElimination]
LocalDef [constructor, in MetaCoq.PCUIC.PCUICAst]
LocalDef [constructor, in MetaCoq.Erasure.EAst]
locality [inductive, in MetaCoq.Template.TemplateMonad.Common]
local_entry [inductive, in MetaCoq.PCUIC.PCUICAst]
local_entry [inductive, in MetaCoq.Erasure.EAst]
local_env_telescope [lemma, in MetaCoq.PCUIC.PCUICConfluence]
local_env_telescope [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
lookup [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
Lookup [module, in MetaCoq.Template.EnvironmentTyping]
Lookups [section, in MetaCoq.Template.Checker]
Lookups [section, in MetaCoq.Erasure.EGlobalEnv]
lookups [section, in MetaCoq.PCUIC.utils.PCUICPretty]
LookupSig [module, in MetaCoq.Template.EnvironmentTyping]
lookup_lookup_global_env_None [lemma, in MetaCoq.Template.EtaExpand]
lookup_global_env_lookup [lemma, in MetaCoq.Template.EtaExpand]
lookup_lookup_global_env [lemma, in MetaCoq.Template.EtaExpand]
lookup_global_env [definition, in MetaCoq.Template.EtaExpand]
lookup_lookup_env [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
lookup_tsl_table' [definition, in MetaCoq.Translations.translation_utils]
lookup_tsl_table [definition, in MetaCoq.Translations.translation_utils]
lookup_env_cons_fresh [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
lookup_env_cons [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
lookup_env_nil [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
lookup_env_Some_fresh [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
lookup_global_Some_fresh [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
lookup_inductive_pars_constructor_pars_args [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
lookup_ind_decl [definition, in MetaCoq.Erasure.EPretty]
lookup_inductive_None [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
lookup_wf_local_decl [definition, in MetaCoq.Template.Typing]
lookup_wf_local [definition, in MetaCoq.Template.Typing]
lookup_on_global_env [lemma, in MetaCoq.Template.Typing]
lookup_projection_optimize [lemma, in MetaCoq.Erasure.EInlineProjections]
lookup_constructor_optimize [lemma, in MetaCoq.Erasure.EInlineProjections]
lookup_env_optimize [lemma, in MetaCoq.Erasure.EInlineProjections]
lookup_env_optimize_env_None [lemma, in MetaCoq.Erasure.EInlineProjections]
lookup_env_map_snd [lemma, in MetaCoq.Erasure.EInlineProjections]
lookup_env_optimize_env_Some [lemma, in MetaCoq.Erasure.EInlineProjections]
lookup_inductive_wellformed [lemma, in MetaCoq.Erasure.EInlineProjections]
lookup_constructor [definition, in MetaCoq.Template.TermEquality]
lookup_inductive [definition, in MetaCoq.Template.TermEquality]
lookup_minductive [definition, in MetaCoq.Template.TermEquality]
lookup_constructor_transform_blocks [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
lookup_env_transform_blocks [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
lookup_constructor_pars_args_spec [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
lookup_ind_decl_complete [lemma, in MetaCoq.SafeChecker.PCUICSafeRetyping]
lookup_ind_decl [definition, in MetaCoq.SafeChecker.PCUICSafeRetyping]
lookup_inductive_declared [lemma, in MetaCoq.PCUIC.Syntax.PCUICCases]
lookup_projection_lookup_constructor [lemma, in MetaCoq.Erasure.ErasureProperties]
lookup_constant [definition, in MetaCoq.Erasure.ErasureProperties]
lookup_erase_global [lemma, in MetaCoq.Erasure.ErasureFunction]
lookup_env_erase [lemma, in MetaCoq.Erasure.ErasureFunction]
lookup_env_cons_disc [lemma, in MetaCoq.Erasure.ErasureFunction]
lookup_env_ext [lemma, in MetaCoq.Erasure.ErasureFunction]
lookup_env_wellformed [lemma, in MetaCoq.Erasure.EWellformed]
lookup_env [definition, in MetaCoq.Template.Checker]
lookup_constructor_type_cstrs [definition, in MetaCoq.Template.Checker]
lookup_constructor_type [definition, in MetaCoq.Template.Checker]
lookup_constructor_decl [definition, in MetaCoq.Template.Checker]
lookup_ind_type_cstrs [definition, in MetaCoq.Template.Checker]
lookup_ind_type [definition, in MetaCoq.Template.Checker]
lookup_ind_decl [definition, in MetaCoq.Template.Checker]
lookup_constant_type_cstrs [definition, in MetaCoq.Template.Checker]
lookup_constant_type [definition, in MetaCoq.Template.Checker]
lookup_env_nlg [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
lookup_wf_local_decl [definition, in MetaCoq.PCUIC.PCUICTyping]
lookup_wf_local [definition, in MetaCoq.PCUIC.PCUICTyping]
lookup_on_global_env [lemma, in MetaCoq.PCUIC.PCUICTyping]
lookup_env_Some_fresh [lemma, in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor_pars_args_cstr_arity [lemma, in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor_lookup_inductive [lemma, in MetaCoq.Erasure.EGlobalEnv]
lookup_projection_lookup_constructor [lemma, in MetaCoq.Erasure.EGlobalEnv]
lookup_projection [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor_pars_args [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_inductive_pars [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_inductive [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_minductive [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_constant [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_env [definition, in MetaCoq.Erasure.EGlobalEnv]
lookup_env_In [lemma, in MetaCoq.Erasure.EExtends]
lookup_minductive_declared_inductive [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_minductive_declared_minductive [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_inductive_pars_spec [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_constructor_lookup_inductive_pars [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_inductive_pars_is_prop_and_pars [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_constructor_strip [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_env_strip [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_inductive_pars_constructor_pars_args [lemma, in MetaCoq.Erasure.ERemoveParams]
lookup_env_closed [lemma, in MetaCoq.Erasure.EWcbvEval]
lookup_ind_decl [definition, in MetaCoq.Template.Pretty]
lookup_env_extends [lemma, in MetaCoq.Template.TypingWf]
lookup_projection_gen_transform [lemma, in MetaCoq.Erasure.EGenericMapEnv]
lookup_constructor_gen_transform [lemma, in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_gen_transform [lemma, in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_None [lemma, in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_map_snd [lemma, in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_Some [lemma, in MetaCoq.Erasure.EGenericMapEnv]
lookup_constructor_optimize [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_optimize [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_optimize_env_None [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_map_snd [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_optimize_env_Some [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_inductive [definition, in MetaCoq.Template.AstUtils]
lookup_minductive [definition, in MetaCoq.Template.AstUtils]
lookup_mind_decl [definition, in MetaCoq.Template.AstUtils]
lookup_ind_decl [definition, in MetaCoq.PCUIC.utils.PCUICPretty]
lookup_ind_decl [definition, in MetaCoq.SafeChecker.PCUICTypeChecker]
Lookup.consistent_instance_length [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.consistent_instance_ext [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.consistent_instance [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_projection_lookup [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constructor_lookup [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_inductive_lookup [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_minductive_lookup [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constant_lookup [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_projection [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constructor [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_inductive [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_minductive [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constant [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_levels_InSet [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_uctx [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_constraints [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_levels [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_uctx [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_constraints [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_levels_memSet [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_levels_InSet [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.global_levels [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_projection_declared [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constructor_declared [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_inductive_declared [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_minductive_declared [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constant_declared [lemma, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_projection [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constructor [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_inductive [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_minductive [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constant [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.on_udecl_decl [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.universes_decl_of_decl [definition, in MetaCoq.Template.EnvironmentTyping]
Lookup.wf_universe [definition, in MetaCoq.Template.EnvironmentTyping]
lookup:20 [binder, in MetaCoq.PCUIC.PCUICTyping]
lookup:27 [binder, in MetaCoq.PCUIC.PCUICTyping]
lookup:35 [binder, in MetaCoq.PCUIC.PCUICTyping]
LS [module, in MetaCoq.Template.Universes]
LSet_in_global_bounded [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
LSet_in_poly_bounded [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
lsp_proper [instance, in MetaCoq.Template.common.uGraph]
lsp_expr [definition, in MetaCoq.Template.common.uGraph]
ls0:114 [binder, in MetaCoq.Examples.tauto]
ls0:123 [binder, in MetaCoq.Examples.tauto]
ls:108 [binder, in MetaCoq.Examples.tauto]
ls:117 [binder, in MetaCoq.Examples.tauto]
ls:126 [binder, in MetaCoq.Examples.tauto]
ls:129 [binder, in MetaCoq.Examples.tauto]
ls:138 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ls:54 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
ls:73 [binder, in MetaCoq.Examples.tauto]
ls:93 [binder, in MetaCoq.Examples.tauto]
ls:96 [binder, in MetaCoq.Examples.tauto]
ls:99 [binder, in MetaCoq.Examples.tauto]
lt [definition, in MetaCoq.Template.utils.ByteCompareSpec]
lt_universe_str_order [instance, in MetaCoq.Template.Universes]
lt_levelalg_str_order [instance, in MetaCoq.Template.Universes]
lt_universe_trans [instance, in MetaCoq.Template.Universes]
lt_universe [definition, in MetaCoq.Template.Universes]
lt_levelalg [definition, in MetaCoq.Template.Universes]
lt_cuniverse_str_order [instance, in MetaCoq.Template.Universes]
lt_cuniverse_trans [instance, in MetaCoq.Template.Universes]
lt_cuniverse [definition, in MetaCoq.Template.Universes]
lt_not_eq [lemma, in MetaCoq.Template.utils.ByteCompareSpec]
lt_trans [lemma, in MetaCoq.Template.utils.ByteCompareSpec]
lt_level_irrel [lemma, in MetaCoq.Template.Reflect]
lt:316 [binder, in MetaCoq.Template.common.uGraph]
lt:321 [binder, in MetaCoq.Template.common.uGraph]
lt:331 [binder, in MetaCoq.Template.common.uGraph]
lt:363 [binder, in MetaCoq.Template.common.uGraph]
lt:397 [binder, in MetaCoq.Template.common.uGraph]
lt:402 [binder, in MetaCoq.Template.common.uGraph]
lt:409 [binder, in MetaCoq.Template.common.uGraph]
lt:416 [binder, in MetaCoq.Template.common.uGraph]
lt:485 [binder, in MetaCoq.Template.common.uGraph]
lu':32 [binder, in MetaCoq.Translations.standard_model]
lvls:439 [binder, in MetaCoq.Template.Universes]
lvs:154 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
lvs:90 [binder, in MetaCoq.Template.EnvironmentTyping]
lx:1187 [binder, in MetaCoq.PCUIC.PCUICReduction]
lzero [abbreviation, in MetaCoq.Template.common.uGraph]
l'x:1188 [binder, in MetaCoq.PCUIC.PCUICReduction]
l''':1850 [binder, in MetaCoq.Template.utils.All_Forall]
l''':2574 [binder, in MetaCoq.Template.utils.All_Forall]
l'':1177 [binder, in MetaCoq.PCUIC.PCUICReduction]
l'':14 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':16 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':18 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':1845 [binder, in MetaCoq.Template.utils.All_Forall]
l'':19 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
l'':20 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':21 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
l'':2232 [binder, in MetaCoq.Template.utils.All_Forall]
l'':2246 [binder, in MetaCoq.Template.utils.All_Forall]
l'':2485 [binder, in MetaCoq.Template.utils.All_Forall]
l'':2498 [binder, in MetaCoq.Template.utils.All_Forall]
l'':2573 [binder, in MetaCoq.Template.utils.All_Forall]
l'':2586 [binder, in MetaCoq.Template.utils.All_Forall]
l'':2597 [binder, in MetaCoq.Template.utils.All_Forall]
l'':280 [binder, in MetaCoq.Template.utils.MCList]
l'':419 [binder, in MetaCoq.PCUIC.PCUICNormal]
l'':44 [binder, in MetaCoq.Template.utils.All_Forall]
l'':509 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l'':520 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l'':558 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l'':753 [binder, in MetaCoq.PCUIC.PCUICReduction]
l'':814 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l'':923 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':10 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
l':10 [binder, in MetaCoq.Erasure.EAstUtils]
l':101 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':101 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':1010 [binder, in MetaCoq.Template.utils.All_Forall]
l':1012 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':1014 [binder, in MetaCoq.Template.utils.All_Forall]
l':103 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
l':1051 [binder, in MetaCoq.Template.utils.All_Forall]
l':1051 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l':106 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':1063 [binder, in MetaCoq.Template.utils.All_Forall]
l':107 [binder, in MetaCoq.Template.utils.All_Forall]
l':1071 [binder, in MetaCoq.Template.utils.All_Forall]
L':108 [binder, in MetaCoq.Translations.times_bool_fun]
l':1081 [binder, in MetaCoq.Template.utils.All_Forall]
L':109 [binder, in MetaCoq.Translations.times_bool_fun]
l':1093 [binder, in MetaCoq.Template.utils.All_Forall]
l':110 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':1102 [binder, in MetaCoq.Template.utils.All_Forall]
l':1111 [binder, in MetaCoq.Template.utils.All_Forall]
l':1116 [binder, in MetaCoq.Template.utils.All_Forall]
l':1116 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':112 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
l':1122 [binder, in MetaCoq.Template.utils.All_Forall]
l':1131 [binder, in MetaCoq.Template.utils.All_Forall]
l':1140 [binder, in MetaCoq.Template.utils.All_Forall]
l':1146 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':1149 [binder, in MetaCoq.Template.utils.All_Forall]
l':1158 [binder, in MetaCoq.Template.utils.All_Forall]
l':1159 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':1167 [binder, in MetaCoq.Template.utils.All_Forall]
l':1176 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':118 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':1184 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':121 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':1215 [binder, in MetaCoq.Template.utils.All_Forall]
l':123 [binder, in MetaCoq.Template.utils.All_Forall]
l':1237 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':124 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
l':1245 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':125 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
L':126 [binder, in MetaCoq.Translations.times_bool_fun]
l':126 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l':1268 [binder, in MetaCoq.Template.Typing]
L':127 [binder, in MetaCoq.Translations.times_bool_fun]
l':1273 [binder, in MetaCoq.Template.utils.All_Forall]
l':1279 [binder, in MetaCoq.Template.Typing]
l':1281 [binder, in MetaCoq.Template.utils.All_Forall]
l':129 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l':129 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':131 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':134 [binder, in MetaCoq.PCUIC.PCUICContexts]
l':1356 [binder, in MetaCoq.Template.utils.All_Forall]
l':137 [binder, in MetaCoq.Template.LiftSubst]
l':138 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1391 [binder, in MetaCoq.Template.utils.All_Forall]
l':1398 [binder, in MetaCoq.Template.utils.All_Forall]
l':1408 [binder, in MetaCoq.Template.utils.All_Forall]
l':141 [binder, in MetaCoq.Template.TypingWf]
l':1416 [binder, in MetaCoq.Template.utils.All_Forall]
l':142 [binder, in MetaCoq.Template.LiftSubst]
l':1421 [binder, in MetaCoq.Template.utils.All_Forall]
l':1425 [binder, in MetaCoq.Template.utils.All_Forall]
l':143 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1436 [binder, in MetaCoq.Template.utils.All_Forall]
l':1443 [binder, in MetaCoq.Template.utils.All_Forall]
l':1448 [binder, in MetaCoq.Template.utils.All_Forall]
l':1455 [binder, in MetaCoq.Template.utils.All_Forall]
l':1490 [binder, in MetaCoq.Template.utils.All_Forall]
l':15 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
l':15 [binder, in MetaCoq.Erasure.EAstUtils]
l':1505 [binder, in MetaCoq.Template.utils.All_Forall]
l':1522 [binder, in MetaCoq.Template.utils.All_Forall]
l':1528 [binder, in MetaCoq.Template.utils.All_Forall]
l':1535 [binder, in MetaCoq.Template.utils.All_Forall]
l':1543 [binder, in MetaCoq.Template.utils.All_Forall]
l':1550 [binder, in MetaCoq.Template.utils.All_Forall]
l':1556 [binder, in MetaCoq.Template.utils.All_Forall]
l':1565 [binder, in MetaCoq.Template.utils.All_Forall]
l':1580 [binder, in MetaCoq.Template.utils.All_Forall]
l':1603 [binder, in MetaCoq.Template.utils.All_Forall]
l':161 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1614 [binder, in MetaCoq.Template.utils.All_Forall]
l':1623 [binder, in MetaCoq.Template.utils.All_Forall]
l':1631 [binder, in MetaCoq.Template.utils.All_Forall]
l':1639 [binder, in MetaCoq.Template.utils.All_Forall]
l':164 [binder, in MetaCoq.Erasure.EDeps]
l':164 [binder, in MetaCoq.Erasure.ELiftSubst]
l':1647 [binder, in MetaCoq.Template.utils.All_Forall]
l':165 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1654 [binder, in MetaCoq.Template.utils.All_Forall]
l':1662 [binder, in MetaCoq.Template.utils.All_Forall]
l':167 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':1670 [binder, in MetaCoq.Template.utils.All_Forall]
l':1678 [binder, in MetaCoq.Template.utils.All_Forall]
l':168 [binder, in MetaCoq.Erasure.ELiftSubst]
l':1686 [binder, in MetaCoq.Template.utils.All_Forall]
l':169 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1695 [binder, in MetaCoq.Template.utils.All_Forall]
l':17 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
l':17 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
l':17 [binder, in MetaCoq.Erasure.EAstUtils]
l':1718 [binder, in MetaCoq.Template.utils.All_Forall]
l':1730 [binder, in MetaCoq.Template.utils.All_Forall]
l':1738 [binder, in MetaCoq.Template.utils.All_Forall]
l':1743 [binder, in MetaCoq.Template.utils.All_Forall]
l':1755 [binder, in MetaCoq.Template.utils.All_Forall]
l':1770 [binder, in MetaCoq.Template.utils.All_Forall]
l':1778 [binder, in MetaCoq.Template.utils.All_Forall]
l':1785 [binder, in MetaCoq.Template.utils.All_Forall]
l':1792 [binder, in MetaCoq.Template.utils.All_Forall]
l':18 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
l':1804 [binder, in MetaCoq.Template.utils.All_Forall]
l':1812 [binder, in MetaCoq.Template.utils.All_Forall]
l':1824 [binder, in MetaCoq.Template.utils.All_Forall]
l':1829 [binder, in MetaCoq.Template.utils.All_Forall]
l':1833 [binder, in MetaCoq.Template.utils.All_Forall]
l':1844 [binder, in MetaCoq.Template.utils.All_Forall]
l':1854 [binder, in MetaCoq.Template.utils.All_Forall]
l':186 [binder, in MetaCoq.Template.utils.All_Forall]
l':1862 [binder, in MetaCoq.Template.utils.All_Forall]
l':1869 [binder, in MetaCoq.Template.utils.All_Forall]
l':19 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
l':191 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':1918 [binder, in MetaCoq.Template.utils.All_Forall]
l':193 [binder, in MetaCoq.Template.utils.All_Forall]
l':1942 [binder, in MetaCoq.Template.utils.All_Forall]
l':196 [binder, in MetaCoq.Template.Environment]
l':1960 [binder, in MetaCoq.Template.utils.All_Forall]
l':1976 [binder, in MetaCoq.Template.utils.All_Forall]
l':1981 [binder, in MetaCoq.Template.utils.All_Forall]
l':1994 [binder, in MetaCoq.Template.utils.All_Forall]
l':200 [binder, in MetaCoq.Template.utils.All_Forall]
l':2007 [binder, in MetaCoq.Template.utils.All_Forall]
l':2013 [binder, in MetaCoq.Template.utils.All_Forall]
l':2021 [binder, in MetaCoq.Template.utils.All_Forall]
l':2028 [binder, in MetaCoq.Template.utils.All_Forall]
l':203 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':2034 [binder, in MetaCoq.Template.utils.All_Forall]
l':204 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2040 [binder, in MetaCoq.Template.utils.All_Forall]
l':2059 [binder, in MetaCoq.Template.utils.All_Forall]
l':2064 [binder, in MetaCoq.Template.utils.All_Forall]
l':207 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2073 [binder, in MetaCoq.Template.utils.All_Forall]
l':2083 [binder, in MetaCoq.Template.utils.All_Forall]
l':209 [binder, in MetaCoq.Template.utils.All_Forall]
l':2090 [binder, in MetaCoq.Template.utils.All_Forall]
l':2098 [binder, in MetaCoq.Template.utils.All_Forall]
l':2105 [binder, in MetaCoq.Template.utils.All_Forall]
l':211 [binder, in MetaCoq.PCUIC.PCUICNormal]
l':2112 [binder, in MetaCoq.Template.utils.All_Forall]
l':212 [binder, in MetaCoq.Template.Typing]
l':213 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':214 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':2140 [binder, in MetaCoq.Template.utils.All_Forall]
l':2151 [binder, in MetaCoq.Template.utils.All_Forall]
l':2160 [binder, in MetaCoq.Template.utils.All_Forall]
l':2168 [binder, in MetaCoq.Template.utils.All_Forall]
l':217 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2176 [binder, in MetaCoq.Template.utils.All_Forall]
l':2185 [binder, in MetaCoq.Template.utils.All_Forall]
l':22 [binder, in MetaCoq.Template.utils.All_Forall]
l':22 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':22 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l':220 [binder, in MetaCoq.Template.utils.All_Forall]
l':220 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':223 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':2231 [binder, in MetaCoq.Template.utils.All_Forall]
l':224 [binder, in MetaCoq.Template.TypingWf]
l':2245 [binder, in MetaCoq.Template.utils.All_Forall]
l':23 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':231 [binder, in MetaCoq.Template.utils.All_Forall]
l':235 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2364 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
l':240 [binder, in MetaCoq.Template.utils.MCList]
l':242 [binder, in MetaCoq.Template.utils.All_Forall]
l':243 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':243 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':2448 [binder, in MetaCoq.Template.utils.All_Forall]
l':2457 [binder, in MetaCoq.Template.utils.All_Forall]
l':248 [binder, in MetaCoq.Template.TermEquality]
l':2484 [binder, in MetaCoq.Template.utils.All_Forall]
l':249 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l':2497 [binder, in MetaCoq.Template.utils.All_Forall]
l':25 [binder, in MetaCoq.Template.AstUtils]
l':250 [binder, in MetaCoq.Template.utils.All_Forall]
l':253 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':255 [binder, in MetaCoq.Template.TermEquality]
l':2572 [binder, in MetaCoq.Template.utils.All_Forall]
l':258 [binder, in MetaCoq.Template.utils.All_Forall]
l':258 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':2585 [binder, in MetaCoq.Template.utils.All_Forall]
l':2596 [binder, in MetaCoq.Template.utils.All_Forall]
l':26 [binder, in MetaCoq.Erasure.Extract]
l':260 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
l':262 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l':264 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':266 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':266 [binder, in MetaCoq.Template.TypingWf]
l':267 [binder, in MetaCoq.Template.utils.All_Forall]
l':269 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l':270 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':277 [binder, in MetaCoq.Template.utils.All_Forall]
l':277 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':279 [binder, in MetaCoq.Template.utils.MCList]
l':280 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':282 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':283 [binder, in MetaCoq.Template.utils.MCList]
l':284 [binder, in MetaCoq.Erasure.EWcbvEval]
l':286 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
l':287 [binder, in MetaCoq.Template.utils.All_Forall]
l':287 [binder, in MetaCoq.Template.WcbvEval]
l':288 [binder, in MetaCoq.Erasure.ERemoveParams]
l':290 [binder, in MetaCoq.Erasure.ERemoveParams]
l':291 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l':291 [binder, in MetaCoq.Template.WcbvEval]
l':292 [binder, in MetaCoq.Erasure.ERemoveParams]
l':292 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':293 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':294 [binder, in MetaCoq.Template.common.uGraph]
l':294 [binder, in MetaCoq.Erasure.ERemoveParams]
l':294 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l':296 [binder, in MetaCoq.Erasure.ERemoveParams]
l':297 [binder, in MetaCoq.Template.common.uGraph]
l':298 [binder, in MetaCoq.Erasure.ERemoveParams]
l':30 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
L':30 [binder, in MetaCoq.Erasure.ErasureProperties]
l':301 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':301 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':302 [binder, in MetaCoq.Template.common.uGraph]
l':307 [binder, in MetaCoq.Template.common.uGraph]
l':310 [binder, in MetaCoq.Template.common.uGraph]
l':312 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':313 [binder, in MetaCoq.Template.common.uGraph]
l':314 [binder, in MetaCoq.Template.utils.All_Forall]
l':316 [binder, in MetaCoq.PCUIC.PCUICSR]
l':318 [binder, in MetaCoq.Template.utils.All_Forall]
l':318 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':32 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':32 [binder, in MetaCoq.Erasure.EAstUtils]
l':320 [binder, in MetaCoq.Template.WcbvEval]
l':328 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':331 [binder, in MetaCoq.Template.utils.MCList]
l':332 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':335 [binder, in MetaCoq.Template.utils.All_Forall]
l':337 [binder, in MetaCoq.Template.utils.MCList]
l':34 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':343 [binder, in MetaCoq.Template.utils.All_Forall]
l':344 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':346 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':349 [binder, in MetaCoq.Template.TypingWf]
l':35 [binder, in MetaCoq.Template.Universes]
l':350 [binder, in MetaCoq.Template.utils.All_Forall]
l':354 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':358 [binder, in MetaCoq.Template.utils.All_Forall]
l':358 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':358 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
L':36 [binder, in MetaCoq.Erasure.ErasureProperties]
l':36 [binder, in MetaCoq.Template.AstUtils]
l':361 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':363 [binder, in MetaCoq.Template.utils.All_Forall]
l':364 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':365 [binder, in MetaCoq.PCUIC.PCUICNormal]
l':366 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l':372 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':374 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':377 [binder, in MetaCoq.Template.utils.All_Forall]
l':377 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':379 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l':379 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':380 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':384 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':385 [binder, in MetaCoq.Template.utils.MCList]
l':386 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l':389 [binder, in MetaCoq.Template.utils.All_Forall]
l':389 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l':39 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':392 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':394 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':399 [binder, in MetaCoq.Template.utils.All_Forall]
l':399 [binder, in MetaCoq.Template.Typing]
l':4 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
l':402 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':402 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':402 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l':407 [binder, in MetaCoq.Template.utils.All_Forall]
l':41 [binder, in MetaCoq.Template.utils.MCList]
l':41 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':412 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':412 [binder, in MetaCoq.Erasure.ErasureFunction]
l':412 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l':416 [binder, in MetaCoq.Template.utils.All_Forall]
l':418 [binder, in MetaCoq.PCUIC.PCUICNormal]
l':42 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l':424 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
l':426 [binder, in MetaCoq.Template.utils.All_Forall]
l':428 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':43 [binder, in MetaCoq.Template.utils.All_Forall]
l':430 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':433 [binder, in MetaCoq.Template.utils.MCList]
l':44 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
l':44 [binder, in MetaCoq.Erasure.Prelim]
l':451 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l':453 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
L':46 [binder, in MetaCoq.Erasure.ErasureProperties]
l':46 [binder, in MetaCoq.Template.AstUtils]
l':463 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':47 [binder, in MetaCoq.Template.TypingWf]
l':472 [binder, in MetaCoq.Template.Universes]
l':472 [binder, in MetaCoq.PCUIC.PCUICSR]
l':475 [binder, in MetaCoq.Template.Universes]
l':481 [binder, in MetaCoq.Template.utils.MCList]
l':486 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l':49 [binder, in MetaCoq.Template.monad_utils]
l':496 [binder, in MetaCoq.Template.utils.MCList]
l':496 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l':497 [binder, in MetaCoq.Template.utils.All_Forall]
l':50 [binder, in MetaCoq.Erasure.EInduction]
l':50 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':50 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l':500 [binder, in MetaCoq.Template.common.uGraph]
l':506 [binder, in MetaCoq.Template.common.uGraph]
l':508 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':51 [binder, in MetaCoq.Template.utils.MCList]
l':51 [binder, in MetaCoq.PCUIC.PCUICSR]
l':51 [binder, in MetaCoq.Erasure.EAstUtils]
l':514 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':518 [binder, in MetaCoq.Template.utils.MCList]
l':519 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':522 [binder, in MetaCoq.Template.utils.MCList]
l':523 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':528 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':538 [binder, in MetaCoq.Template.utils.MCList]
l':538 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':54 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l':541 [binder, in MetaCoq.Template.utils.All_Forall]
l':544 [binder, in MetaCoq.Template.utils.MCList]
l':546 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':553 [binder, in MetaCoq.Template.utils.MCList]
l':554 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l':557 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':56 [binder, in MetaCoq.Erasure.EAstUtils]
l':564 [binder, in MetaCoq.Template.common.uGraph]
l':569 [binder, in MetaCoq.Template.common.uGraph]
l':57 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':571 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':579 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':581 [binder, in MetaCoq.Template.utils.All_Forall]
l':585 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':59 [binder, in MetaCoq.Erasure.EInduction]
L':59 [binder, in MetaCoq.Erasure.EArities]
l':590 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':591 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l':592 [binder, in MetaCoq.Template.utils.All_Forall]
l':592 [binder, in MetaCoq.Template.common.uGraph]
l':592 [binder, in MetaCoq.PCUIC.PCUICConversion]
l':594 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':597 [binder, in MetaCoq.Template.utils.All_Forall]
l':597 [binder, in MetaCoq.Template.common.uGraph]
l':6 [binder, in MetaCoq.Template.utils.MCList]
l':6 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
l':60 [binder, in MetaCoq.Erasure.EArities]
l':60 [binder, in MetaCoq.Template.monad_utils]
l':60 [binder, in MetaCoq.Erasure.EAstUtils]
l':601 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':602 [binder, in MetaCoq.Template.utils.All_Forall]
l':607 [binder, in MetaCoq.Template.utils.MCList]
l':608 [binder, in MetaCoq.Template.utils.All_Forall]
l':613 [binder, in MetaCoq.Template.utils.All_Forall]
l':620 [binder, in MetaCoq.Template.utils.All_Forall]
l':623 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':629 [binder, in MetaCoq.Template.utils.All_Forall]
l':63 [binder, in MetaCoq.Erasure.EAstUtils]
l':634 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':639 [binder, in MetaCoq.Template.utils.All_Forall]
l':642 [binder, in MetaCoq.Template.utils.All_Forall]
l':646 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':65 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':655 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
L':66 [binder, in MetaCoq.Translations.times_bool_fun]
l':668 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
L':67 [binder, in MetaCoq.Translations.times_bool_fun]
l':67 [binder, in MetaCoq.Template.utils.ReflectEq]
l':67 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
l':67 [binder, in MetaCoq.Template.monad_utils]
l':671 [binder, in MetaCoq.Template.utils.All_Forall]
l':671 [binder, in MetaCoq.PCUIC.PCUICEquality]
l':680 [binder, in MetaCoq.Template.utils.All_Forall]
l':685 [binder, in MetaCoq.Template.utils.All_Forall]
l':689 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':69 [binder, in MetaCoq.Template.Reflect]
l':692 [binder, in MetaCoq.Template.utils.All_Forall]
l':693 [binder, in MetaCoq.Template.utils.MCList]
l':697 [binder, in MetaCoq.Template.utils.MCList]
l':699 [binder, in MetaCoq.Template.Universes]
l':699 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':7 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
l':701 [binder, in MetaCoq.Template.Universes]
l':701 [binder, in MetaCoq.Template.utils.All_Forall]
l':71 [binder, in MetaCoq.Template.utils.MCOption]
l':712 [binder, in MetaCoq.Template.utils.MCList]
l':727 [binder, in MetaCoq.Template.utils.MCList]
l':727 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':73 [binder, in MetaCoq.Template.Reflect]
l':739 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':740 [binder, in MetaCoq.Template.utils.MCList]
l':742 [binder, in MetaCoq.Template.utils.All_Forall]
l':747 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':750 [binder, in MetaCoq.Template.utils.MCList]
l':752 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':756 [binder, in MetaCoq.Template.utils.All_Forall]
l':756 [binder, in MetaCoq.Template.utils.MCList]
l':757 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':761 [binder, in MetaCoq.Template.utils.MCList]
l':762 [binder, in MetaCoq.Template.utils.All_Forall]
l':762 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':766 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':768 [binder, in MetaCoq.Template.utils.All_Forall]
l':77 [binder, in MetaCoq.Template.Reflect]
l':77 [binder, in MetaCoq.Template.utils.MCOption]
l':77 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':776 [binder, in MetaCoq.Template.utils.All_Forall]
l':777 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':78 [binder, in MetaCoq.Template.monad_utils]
l':78 [binder, in MetaCoq.Erasure.EAstUtils]
l':783 [binder, in MetaCoq.Template.utils.All_Forall]
l':786 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':79 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l':792 [binder, in MetaCoq.Template.utils.All_Forall]
l':792 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':799 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':802 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':803 [binder, in MetaCoq.Template.utils.All_Forall]
l':807 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':81 [binder, in MetaCoq.Template.Universes]
l':81 [binder, in MetaCoq.Erasure.Extract]
l':81 [binder, in MetaCoq.Template.Reflect]
l':812 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':813 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l':815 [binder, in MetaCoq.Template.utils.All_Forall]
l':816 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':819 [binder, in MetaCoq.Template.utils.All_Forall]
l':821 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l':822 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':824 [binder, in MetaCoq.Template.utils.MCList]
l':824 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':833 [binder, in MetaCoq.Template.utils.MCList]
l':833 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':84 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l':849 [binder, in MetaCoq.Template.utils.MCList]
l':85 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
l':853 [binder, in MetaCoq.Template.utils.All_Forall]
l':86 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':86 [binder, in MetaCoq.Template.utils.All_Forall]
l':864 [binder, in MetaCoq.Template.utils.All_Forall]
l':870 [binder, in MetaCoq.Template.utils.All_Forall]
l':878 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':879 [binder, in MetaCoq.Template.utils.All_Forall]
l':88 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':887 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':90 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':905 [binder, in MetaCoq.Template.utils.All_Forall]
l':908 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':915 [binder, in MetaCoq.Template.utils.All_Forall]
l':92 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l':922 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':927 [binder, in MetaCoq.Template.utils.MCList]
l':929 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':932 [binder, in MetaCoq.Template.utils.All_Forall]
l':938 [binder, in MetaCoq.Template.utils.All_Forall]
l':939 [binder, in MetaCoq.PCUIC.PCUICTyping]
l':945 [binder, in MetaCoq.Template.utils.All_Forall]
l':945 [binder, in MetaCoq.PCUIC.PCUICTyping]
l':954 [binder, in MetaCoq.Template.utils.All_Forall]
l':962 [binder, in MetaCoq.PCUIC.PCUICReduction]
l':964 [binder, in MetaCoq.Template.utils.All_Forall]
l':97 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l':973 [binder, in MetaCoq.Template.utils.All_Forall]
l':983 [binder, in MetaCoq.Template.utils.All_Forall]
l':995 [binder, in MetaCoq.Template.utils.All_Forall]
l0':1999 [binder, in MetaCoq.Template.utils.All_Forall]
l0':2606 [binder, in MetaCoq.Template.utils.All_Forall]
l0':593 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l0:1485 [binder, in MetaCoq.Template.utils.All_Forall]
l0:1494 [binder, in MetaCoq.Template.utils.All_Forall]
l0:1500 [binder, in MetaCoq.Template.utils.All_Forall]
l0:1509 [binder, in MetaCoq.Template.utils.All_Forall]
l0:1998 [binder, in MetaCoq.Template.utils.All_Forall]
l0:2605 [binder, in MetaCoq.Template.utils.All_Forall]
l0:592 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l0:69 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
l1'':817 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l1':1516 [binder, in MetaCoq.Template.utils.All_Forall]
l1':2001 [binder, in MetaCoq.Template.utils.All_Forall]
l1':2608 [binder, in MetaCoq.Template.utils.All_Forall]
l1':382 [binder, in MetaCoq.Template.Universes]
l1':393 [binder, in MetaCoq.Template.Universes]
l1':816 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l1:1019 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1034 [binder, in MetaCoq.Template.utils.All_Forall]
l1:111 [binder, in MetaCoq.Template.monad_utils]
l1:115 [binder, in MetaCoq.Template.utils.MCList]
l1:1186 [binder, in MetaCoq.Template.utils.wGraph]
l1:122 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
l1:1229 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1238 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1249 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1262 [binder, in MetaCoq.Template.utils.All_Forall]
l1:133 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:144 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:1461 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1472 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1477 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1514 [binder, in MetaCoq.Template.utils.All_Forall]
l1:153 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:1570 [binder, in MetaCoq.Template.utils.All_Forall]
l1:16 [binder, in MetaCoq.Template.Universes]
l1:1711 [binder, in MetaCoq.Template.utils.All_Forall]
L1:1760 [binder, in MetaCoq.Template.utils.All_Forall]
l1:1950 [binder, in MetaCoq.Template.utils.All_Forall]
l1:197 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:2000 [binder, in MetaCoq.Template.utils.All_Forall]
l1:2048 [binder, in MetaCoq.Template.utils.All_Forall]
l1:222 [binder, in MetaCoq.PCUIC.PCUICSR]
l1:231 [binder, in MetaCoq.Template.Checker]
l1:235 [binder, in MetaCoq.PCUIC.PCUICSR]
l1:238 [binder, in MetaCoq.Template.Checker]
l1:249 [binder, in MetaCoq.Template.Checker]
l1:2607 [binder, in MetaCoq.Template.utils.All_Forall]
l1:280 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:287 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:294 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:299 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:3 [binder, in MetaCoq.Template.Reflect]
l1:306 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l1:32 [binder, in MetaCoq.Template.utils.MCCompare]
l1:32 [binder, in MetaCoq.Template.Universes]
l1:335 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l1:34 [binder, in MetaCoq.Template.utils.MCCompare]
L1:340 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L1:343 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l1:36 [binder, in MetaCoq.Template.Universes]
l1:367 [binder, in MetaCoq.Template.Universes]
l1:372 [binder, in MetaCoq.Template.Universes]
l1:376 [binder, in MetaCoq.Template.Universes]
l1:38 [binder, in MetaCoq.Template.utils.MCCompare]
l1:381 [binder, in MetaCoq.Template.Universes]
l1:389 [binder, in MetaCoq.Template.Universes]
l1:395 [binder, in MetaCoq.Template.utils.MCList]
l1:403 [binder, in MetaCoq.Template.common.uGraph]
L1:41 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l1:412 [binder, in MetaCoq.Template.utils.MCList]
l1:417 [binder, in MetaCoq.Template.common.uGraph]
l1:42 [binder, in MetaCoq.Template.Universes]
L1:42 [binder, in MetaCoq.Erasure.ErasureProperties]
l1:424 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l1:432 [binder, in MetaCoq.Template.common.uGraph]
l1:4400 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
l1:4418 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
l1:447 [binder, in MetaCoq.Template.common.uGraph]
l1:502 [binder, in MetaCoq.PCUIC.PCUICEquality]
l1:527 [binder, in MetaCoq.Template.utils.MCList]
l1:528 [binder, in MetaCoq.PCUIC.PCUICEquality]
l1:551 [binder, in MetaCoq.Template.common.uGraph]
l1:57 [binder, in MetaCoq.Template.Universes]
l1:645 [binder, in MetaCoq.Template.utils.All_Forall]
l1:657 [binder, in MetaCoq.Template.utils.All_Forall]
l1:67 [binder, in MetaCoq.Template.utils.MCCompare]
l1:687 [binder, in MetaCoq.Template.utils.MCList]
l1:7 [binder, in MetaCoq.Template.Reflect]
l1:705 [binder, in MetaCoq.Template.utils.All_Forall]
l1:717 [binder, in MetaCoq.Template.utils.All_Forall]
l1:721 [binder, in MetaCoq.PCUIC.PCUICReduction]
l1:776 [binder, in MetaCoq.Template.Universes]
l1:789 [binder, in MetaCoq.Template.utils.MCList]
l1:815 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l1:820 [binder, in MetaCoq.Template.utils.MCList]
l1:822 [binder, in MetaCoq.Template.utils.MCList]
l1:823 [binder, in MetaCoq.Template.utils.All_Forall]
l1:827 [binder, in MetaCoq.Template.utils.MCList]
l1:837 [binder, in MetaCoq.Template.utils.All_Forall]
l1:838 [binder, in MetaCoq.Template.utils.MCList]
l1:843 [binder, in MetaCoq.Template.utils.MCList]
l1:845 [binder, in MetaCoq.Template.utils.MCList]
l1:847 [binder, in MetaCoq.Template.utils.MCList]
l1:85 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l1:850 [binder, in MetaCoq.Template.utils.MCList]
l1:852 [binder, in MetaCoq.Template.utils.MCList]
l1:854 [binder, in MetaCoq.Template.utils.MCList]
l1:90 [binder, in MetaCoq.Template.Universes]
l2':1517 [binder, in MetaCoq.Template.utils.All_Forall]
l2':375 [binder, in MetaCoq.Template.Universes]
l2':380 [binder, in MetaCoq.Template.Universes]
l2':386 [binder, in MetaCoq.Template.Universes]
l2':391 [binder, in MetaCoq.Template.Universes]
L2':44 [binder, in MetaCoq.Erasure.ErasureProperties]
l2:1020 [binder, in MetaCoq.Template.utils.All_Forall]
l2:1035 [binder, in MetaCoq.Template.utils.All_Forall]
l2:112 [binder, in MetaCoq.Template.monad_utils]
l2:116 [binder, in MetaCoq.Template.utils.MCList]
l2:1187 [binder, in MetaCoq.Template.utils.wGraph]
l2:123 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
l2:1250 [binder, in MetaCoq.Template.utils.All_Forall]
l2:1263 [binder, in MetaCoq.Template.utils.All_Forall]
l2:137 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l2:1462 [binder, in MetaCoq.Template.utils.All_Forall]
l2:1473 [binder, in MetaCoq.Template.utils.All_Forall]
l2:1478 [binder, in MetaCoq.Template.utils.All_Forall]
l2:148 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l2:1515 [binder, in MetaCoq.Template.utils.All_Forall]
l2:156 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l2:1571 [binder, in MetaCoq.Template.utils.All_Forall]
l2:17 [binder, in MetaCoq.Template.Universes]
l2:1712 [binder, in MetaCoq.Template.utils.All_Forall]
L2:1761 [binder, in MetaCoq.Template.utils.All_Forall]
l2:195 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l2:1951 [binder, in MetaCoq.Template.utils.All_Forall]
l2:2049 [binder, in MetaCoq.Template.utils.All_Forall]
l2:223 [binder, in MetaCoq.PCUIC.PCUICSR]
l2:233 [binder, in MetaCoq.Template.Checker]
l2:236 [binder, in MetaCoq.PCUIC.PCUICSR]
l2:240 [binder, in MetaCoq.Template.Checker]
l2:250 [binder, in MetaCoq.Template.Checker]
l2:300 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l2:307 [binder, in MetaCoq.SafeChecker.PCUICErrors]
l2:33 [binder, in MetaCoq.Template.utils.MCCompare]
l2:33 [binder, in MetaCoq.Template.Universes]
l2:336 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
L2:341 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L2:344 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l2:35 [binder, in MetaCoq.Template.utils.MCCompare]
l2:369 [binder, in MetaCoq.Template.Universes]
l2:37 [binder, in MetaCoq.Template.Universes]
l2:374 [binder, in MetaCoq.Template.Universes]
l2:379 [binder, in MetaCoq.Template.Universes]
l2:385 [binder, in MetaCoq.Template.Universes]
l2:387 [binder, in MetaCoq.Template.Universes]
l2:39 [binder, in MetaCoq.Template.utils.MCCompare]
l2:396 [binder, in MetaCoq.Template.utils.MCList]
l2:4 [binder, in MetaCoq.Template.Reflect]
l2:404 [binder, in MetaCoq.Template.common.uGraph]
l2:413 [binder, in MetaCoq.Template.utils.MCList]
l2:418 [binder, in MetaCoq.Template.common.uGraph]
L2:42 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l2:425 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l2:43 [binder, in MetaCoq.Template.Universes]
L2:43 [binder, in MetaCoq.Erasure.ErasureProperties]
l2:433 [binder, in MetaCoq.Template.common.uGraph]
l2:4423 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
l2:448 [binder, in MetaCoq.Template.common.uGraph]
l2:504 [binder, in MetaCoq.PCUIC.PCUICEquality]
l2:528 [binder, in MetaCoq.Template.utils.MCList]
l2:530 [binder, in MetaCoq.PCUIC.PCUICEquality]
l2:552 [binder, in MetaCoq.Template.common.uGraph]
l2:58 [binder, in MetaCoq.Template.Universes]
l2:646 [binder, in MetaCoq.Template.utils.All_Forall]
l2:658 [binder, in MetaCoq.Template.utils.All_Forall]
l2:68 [binder, in MetaCoq.Template.utils.MCCompare]
l2:688 [binder, in MetaCoq.Template.utils.MCList]
l2:706 [binder, in MetaCoq.Template.utils.All_Forall]
l2:718 [binder, in MetaCoq.Template.utils.All_Forall]
l2:722 [binder, in MetaCoq.PCUIC.PCUICReduction]
l2:774 [binder, in MetaCoq.Template.Universes]
l2:790 [binder, in MetaCoq.Template.utils.MCList]
l2:8 [binder, in MetaCoq.Template.Reflect]
l2:821 [binder, in MetaCoq.Template.utils.MCList]
l2:823 [binder, in MetaCoq.Template.utils.MCList]
l2:824 [binder, in MetaCoq.Template.utils.All_Forall]
l2:828 [binder, in MetaCoq.Template.utils.MCList]
l2:838 [binder, in MetaCoq.Template.utils.All_Forall]
l2:839 [binder, in MetaCoq.Template.utils.MCList]
l2:84 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l2:844 [binder, in MetaCoq.Template.utils.MCList]
l2:846 [binder, in MetaCoq.Template.utils.MCList]
l2:848 [binder, in MetaCoq.Template.utils.MCList]
l2:851 [binder, in MetaCoq.Template.utils.MCList]
l2:853 [binder, in MetaCoq.Template.utils.MCList]
l2:855 [binder, in MetaCoq.Template.utils.MCList]
l2:91 [binder, in MetaCoq.Template.Universes]
l3:1021 [binder, in MetaCoq.Template.utils.All_Forall]
l3:1036 [binder, in MetaCoq.Template.utils.All_Forall]
l3:1713 [binder, in MetaCoq.Template.utils.All_Forall]
l3:224 [binder, in MetaCoq.PCUIC.PCUICSR]
l3:237 [binder, in MetaCoq.PCUIC.PCUICSR]
l3:337 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l3:426 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l3:647 [binder, in MetaCoq.Template.utils.All_Forall]
l3:659 [binder, in MetaCoq.Template.utils.All_Forall]
l3:707 [binder, in MetaCoq.Template.utils.All_Forall]
l3:825 [binder, in MetaCoq.Template.utils.All_Forall]
l3:839 [binder, in MetaCoq.Template.utils.All_Forall]
l4:1030 [binder, in MetaCoq.Template.utils.All_Forall]
l4:1045 [binder, in MetaCoq.Template.utils.All_Forall]
l4:655 [binder, in MetaCoq.Template.utils.All_Forall]
l4:667 [binder, in MetaCoq.Template.utils.All_Forall]
l4:834 [binder, in MetaCoq.Template.utils.All_Forall]
l4:848 [binder, in MetaCoq.Template.utils.All_Forall]
l:10 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
l:10 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
l:100 [binder, in MetaCoq.Template.utils.All_Forall]
l:100 [binder, in MetaCoq.Template.utils.MCList]
L:100 [binder, in MetaCoq.Translations.param_cheap_packed]
l:100 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:100 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:1002 [binder, in MetaCoq.Template.utils.All_Forall]
L:1005 [binder, in MetaCoq.Template.utils.All_Forall]
l:1006 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1007 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1008 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1009 [binder, in MetaCoq.Template.utils.All_Forall]
l:1009 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:101 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:1011 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1013 [binder, in MetaCoq.Template.utils.All_Forall]
l:1017 [binder, in MetaCoq.Template.Typing]
l:102 [binder, in MetaCoq.Template.utils.MCList]
l:102 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
L:102 [binder, in MetaCoq.Translations.param_cheap_packed]
l:102 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:102 [binder, in MetaCoq.Template.LiftSubst]
l:1020 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:103 [binder, in MetaCoq.Template.WfAst]
l:103 [binder, in MetaCoq.Erasure.EAstUtils]
l:1032 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1033 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1034 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1035 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:105 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:105 [binder, in MetaCoq.Template.EnvironmentTyping]
l:105 [binder, in MetaCoq.Erasure.EAstUtils]
l:105 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:1050 [binder, in MetaCoq.Template.utils.All_Forall]
l:1050 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:106 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
L:106 [binder, in MetaCoq.Translations.times_bool_fun]
l:106 [binder, in MetaCoq.Template.utils.All_Forall]
l:106 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:106 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:1062 [binder, in MetaCoq.Template.utils.All_Forall]
L:107 [binder, in MetaCoq.Translations.times_bool_fun]
l:107 [binder, in MetaCoq.Template.utils.MCList]
l:107 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
l:107 [binder, in MetaCoq.Erasure.ELiftSubst]
l:107 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
l:1070 [binder, in MetaCoq.Template.utils.All_Forall]
l:1075 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1077 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1078 [binder, in MetaCoq.Template.utils.wGraph]
l:1078 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1079 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:108 [binder, in MetaCoq.Template.utils.MCList]
L:108 [binder, in MetaCoq.Translations.param_cheap_packed]
l:1080 [binder, in MetaCoq.Template.utils.All_Forall]
l:1080 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1081 [binder, in MetaCoq.Template.utils.wGraph]
l:1084 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1086 [binder, in MetaCoq.Erasure.ErasureFunction]
l:109 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:1091 [binder, in MetaCoq.Erasure.ErasureFunction]
l:1092 [binder, in MetaCoq.Template.utils.All_Forall]
l:1095 [binder, in MetaCoq.Erasure.ErasureFunction]
l:1099 [binder, in MetaCoq.Erasure.ErasureFunction]
l:11 [binder, in MetaCoq.Template.Universes]
l:11 [binder, in MetaCoq.Erasure.EArities]
l:11 [binder, in MetaCoq.Template.utils.MCList]
l:11 [binder, in MetaCoq.Template.Typing]
l:11 [binder, in MetaCoq.Template.utils.MCString]
l:11 [binder, in MetaCoq.Template.utils.wGraph]
l:11 [binder, in MetaCoq.Examples.add_constructor]
l:110 [binder, in MetaCoq.Template.Universes]
l:110 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
l:110 [binder, in MetaCoq.Template.utils.MCList]
l:1101 [binder, in MetaCoq.Template.utils.All_Forall]
l:1103 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1104 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1105 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1106 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1107 [binder, in MetaCoq.Erasure.ErasureFunction]
l:1110 [binder, in MetaCoq.Template.utils.All_Forall]
l:1112 [binder, in MetaCoq.Erasure.ErasureFunction]
l:1115 [binder, in MetaCoq.Template.utils.All_Forall]
l:1115 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1116 [binder, in MetaCoq.Erasure.ErasureFunction]
l:112 [binder, in MetaCoq.Template.AstUtils]
l:1120 [binder, in MetaCoq.Erasure.ErasureFunction]
l:1121 [binder, in MetaCoq.Template.utils.All_Forall]
l:1130 [binder, in MetaCoq.Template.utils.All_Forall]
l:1139 [binder, in MetaCoq.Template.utils.All_Forall]
l:114 [binder, in MetaCoq.Template.utils.All_Forall]
l:1142 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1145 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1147 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1148 [binder, in MetaCoq.Template.utils.All_Forall]
l:115 [binder, in MetaCoq.Template.Checker]
l:1153 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1154 [binder, in MetaCoq.Template.utils.wGraph]
l:1154 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1155 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1156 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1157 [binder, in MetaCoq.Template.utils.All_Forall]
l:1158 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:116 [binder, in MetaCoq.Translations.param_binary]
l:116 [binder, in MetaCoq.Erasure.ERemoveParams]
l:1163 [binder, in MetaCoq.Template.utils.wGraph]
l:1166 [binder, in MetaCoq.Template.utils.All_Forall]
l:117 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1170 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1173 [binder, in MetaCoq.Template.utils.All_Forall]
l:1175 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1178 [binder, in MetaCoq.Template.utils.All_Forall]
l:118 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
l:118 [binder, in MetaCoq.Template.Ast]
l:1183 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:1185 [binder, in MetaCoq.Template.utils.All_Forall]
L:119 [binder, in MetaCoq.PCUIC.PCUICProgress]
l:119 [binder, in MetaCoq.Erasure.EInduction]
l:1192 [binder, in MetaCoq.Template.utils.All_Forall]
l:1199 [binder, in MetaCoq.Template.utils.All_Forall]
l:12 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
l:12 [binder, in MetaCoq.Erasure.EAstUtils]
l:12 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:12 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:120 [binder, in MetaCoq.Translations.param_binary]
l:120 [binder, in MetaCoq.Erasure.EEtaExpanded]
l:120 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1205 [binder, in MetaCoq.Template.utils.All_Forall]
l:1206 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:121 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
l:121 [binder, in MetaCoq.Erasure.EAstUtils]
l:1210 [binder, in MetaCoq.Template.utils.All_Forall]
l:1214 [binder, in MetaCoq.Template.utils.All_Forall]
l:1219 [binder, in MetaCoq.Template.utils.All_Forall]
l:122 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
l:122 [binder, in MetaCoq.Template.utils.All_Forall]
l:122 [binder, in MetaCoq.Template.utils.MCList]
l:123 [binder, in MetaCoq.Template.BasicAst]
l:123 [binder, in MetaCoq.Template.Ast]
l:123 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
l:123 [binder, in MetaCoq.Erasure.EGlobalEnv]
l:1236 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:124 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
L:124 [binder, in MetaCoq.Translations.times_bool_fun]
l:124 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:124 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1244 [binder, in MetaCoq.PCUIC.PCUICConversion]
L:125 [binder, in MetaCoq.Translations.times_bool_fun]
l:125 [binder, in MetaCoq.Template.utils.MCList]
l:125 [binder, in MetaCoq.Template.EnvironmentTyping]
l:125 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l:125 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
l:126 [binder, in MetaCoq.Translations.param_binary]
l:126 [binder, in MetaCoq.Template.Ast]
l:1260 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1264 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1267 [binder, in MetaCoq.Template.Typing]
l:127 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:127 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
l:1272 [binder, in MetaCoq.Template.utils.All_Forall]
l:1278 [binder, in MetaCoq.Template.Typing]
l:128 [binder, in MetaCoq.Template.utils.All_Forall]
l:128 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l:128 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:128 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:128 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
l:1280 [binder, in MetaCoq.Template.utils.All_Forall]
l:1284 [binder, in MetaCoq.Template.utils.All_Forall]
l:1286 [binder, in MetaCoq.Template.Typing]
l:1289 [binder, in MetaCoq.Template.utils.All_Forall]
l:1294 [binder, in MetaCoq.Template.utils.All_Forall]
l:13 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:13 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
l:13 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
l:13 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
l:13 [binder, in MetaCoq.Erasure.ESpineView]
l:13 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:130 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
L:130 [binder, in MetaCoq.Erasure.EArities]
l:130 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:130 [binder, in MetaCoq.Erasure.EGlobalEnv]
l:1300 [binder, in MetaCoq.Template.utils.All_Forall]
l:1301 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:1305 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1306 [binder, in MetaCoq.Template.utils.All_Forall]
l:131 [binder, in MetaCoq.Template.utils.MCList]
l:131 [binder, in MetaCoq.Template.EnvironmentTyping]
l:131 [binder, in MetaCoq.Erasure.EEtaExpanded]
l:1314 [binder, in MetaCoq.Template.utils.All_Forall]
l:132 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:132 [binder, in MetaCoq.Template.utils.MCList]
l:132 [binder, in MetaCoq.Erasure.ELiftSubst]
l:1321 [binder, in MetaCoq.Template.utils.All_Forall]
l:1329 [binder, in MetaCoq.Template.utils.All_Forall]
l:133 [binder, in MetaCoq.Template.utils.All_Forall]
L:133 [binder, in MetaCoq.Translations.param_cheap_packed]
l:133 [binder, in MetaCoq.PCUIC.PCUICContexts]
l:1334 [binder, in MetaCoq.Template.utils.All_Forall]
l:1339 [binder, in MetaCoq.Template.utils.All_Forall]
l:134 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:134 [binder, in MetaCoq.Template.utils.bytestring]
l:1345 [binder, in MetaCoq.Template.utils.All_Forall]
l:135 [binder, in MetaCoq.Template.utils.MCList]
l:1350 [binder, in MetaCoq.Template.utils.All_Forall]
l:1355 [binder, in MetaCoq.Template.utils.All_Forall]
L:1358 [binder, in MetaCoq.Template.utils.All_Forall]
l:136 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:136 [binder, in MetaCoq.Template.utils.MCList]
l:136 [binder, in MetaCoq.Erasure.ELiftSubst]
l:136 [binder, in MetaCoq.Template.LiftSubst]
l:1366 [binder, in MetaCoq.Template.utils.All_Forall]
l:137 [binder, in MetaCoq.Translations.times_bool_fun]
l:137 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:137 [binder, in MetaCoq.Template.Ast]
l:137 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1376 [binder, in MetaCoq.Template.utils.All_Forall]
l:138 [binder, in MetaCoq.Template.utils.All_Forall]
l:138 [binder, in MetaCoq.Template.utils.bytestring]
l:138 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:138 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
l:1383 [binder, in MetaCoq.Template.utils.All_Forall]
l:139 [binder, in MetaCoq.Translations.times_bool_fun]
L:139 [binder, in MetaCoq.Translations.param_cheap_packed]
l:1390 [binder, in MetaCoq.Template.utils.All_Forall]
l:1393 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1397 [binder, in MetaCoq.Template.utils.All_Forall]
l:14 [binder, in MetaCoq.Template.Universes]
l:14 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
l:14 [binder, in MetaCoq.Erasure.EAstUtils]
l:140 [binder, in MetaCoq.Template.TypingWf]
l:1401 [binder, in MetaCoq.Template.utils.All_Forall]
l:1407 [binder, in MetaCoq.Template.utils.All_Forall]
l:141 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:141 [binder, in MetaCoq.Template.utils.MCList]
l:141 [binder, in MetaCoq.Template.LiftSubst]
l:1415 [binder, in MetaCoq.Template.utils.All_Forall]
l:142 [binder, in MetaCoq.Template.utils.All_Forall]
l:142 [binder, in MetaCoq.Template.utils.bytestring]
l:142 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:1420 [binder, in MetaCoq.Template.utils.All_Forall]
l:1424 [binder, in MetaCoq.Template.utils.All_Forall]
l:143 [binder, in MetaCoq.Template.utils.bytestring]
l:143 [binder, in MetaCoq.Template.Ast]
l:1435 [binder, in MetaCoq.Template.utils.All_Forall]
l:144 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:1442 [binder, in MetaCoq.Template.utils.All_Forall]
l:1447 [binder, in MetaCoq.Template.utils.All_Forall]
l:145 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1454 [binder, in MetaCoq.Template.utils.All_Forall]
l:146 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:146 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:1469 [binder, in MetaCoq.Template.utils.All_Forall]
l:147 [binder, in MetaCoq.Template.Universes]
l:147 [binder, in MetaCoq.Template.utils.MCList]
l:147 [binder, in MetaCoq.Erasure.ERemoveParams]
l:148 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1484 [binder, in MetaCoq.Template.utils.All_Forall]
l:1489 [binder, in MetaCoq.Template.utils.All_Forall]
l:149 [binder, in MetaCoq.Template.utils.bytestring]
l:149 [binder, in MetaCoq.Template.WcbvEval]
l:149 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
l:149 [binder, in MetaCoq.Template.LiftSubst]
l:1493 [binder, in MetaCoq.Template.utils.All_Forall]
l:1499 [binder, in MetaCoq.Template.utils.All_Forall]
l:15 [binder, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
l:15 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
l:15 [binder, in MetaCoq.Template.utils.MCString]
l:15 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:15 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:1504 [binder, in MetaCoq.Template.utils.All_Forall]
l:1508 [binder, in MetaCoq.Template.utils.All_Forall]
l:151 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:151 [binder, in MetaCoq.Template.Ast]
l:151 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
l:152 [binder, in MetaCoq.Template.utils.All_Forall]
l:152 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l:1521 [binder, in MetaCoq.Template.utils.All_Forall]
l:1527 [binder, in MetaCoq.Template.utils.All_Forall]
l:153 [binder, in MetaCoq.Template.utils.bytestring]
l:153 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:1534 [binder, in MetaCoq.Template.utils.All_Forall]
l:1542 [binder, in MetaCoq.Template.utils.All_Forall]
l:1549 [binder, in MetaCoq.Template.utils.All_Forall]
l:155 [binder, in MetaCoq.Template.utils.MCList]
l:155 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
l:155 [binder, in MetaCoq.Template.monad_utils]
l:1555 [binder, in MetaCoq.Template.utils.All_Forall]
l:156 [binder, in MetaCoq.PCUIC.PCUICElimination]
l:156 [binder, in MetaCoq.Template.utils.All_Forall]
l:1564 [binder, in MetaCoq.Template.utils.All_Forall]
l:157 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1574 [binder, in MetaCoq.Template.utils.All_Forall]
l:1579 [binder, in MetaCoq.Template.utils.All_Forall]
l:158 [binder, in MetaCoq.Template.Universes]
l:158 [binder, in MetaCoq.Translations.param_cheap_packed]
l:158 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:158 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:1585 [binder, in MetaCoq.Template.utils.All_Forall]
l:1589 [binder, in MetaCoq.Template.utils.All_Forall]
l:159 [binder, in MetaCoq.Examples.tauto]
l:1593 [binder, in MetaCoq.Template.utils.All_Forall]
l:1597 [binder, in MetaCoq.Template.utils.All_Forall]
l:16 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
l:16 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
l:160 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:160 [binder, in MetaCoq.Template.Ast]
l:1602 [binder, in MetaCoq.Template.utils.All_Forall]
l:161 [binder, in MetaCoq.Template.utils.All_Forall]
L:161 [binder, in MetaCoq.Erasure.EArities]
l:161 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
l:1613 [binder, in MetaCoq.Template.utils.All_Forall]
l:162 [binder, in MetaCoq.Template.utils.MCList]
l:1621 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1622 [binder, in MetaCoq.Template.utils.All_Forall]
l:163 [binder, in MetaCoq.Erasure.EDeps]
l:163 [binder, in MetaCoq.Examples.tauto]
l:163 [binder, in MetaCoq.Erasure.ELiftSubst]
l:163 [binder, in MetaCoq.Template.LiftSubst]
l:1630 [binder, in MetaCoq.Template.utils.All_Forall]
l:1638 [binder, in MetaCoq.Template.utils.All_Forall]
l:164 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:164 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:164 [binder, in MetaCoq.Template.AstUtils]
l:1646 [binder, in MetaCoq.Template.utils.All_Forall]
l:165 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
l:1653 [binder, in MetaCoq.Template.utils.All_Forall]
l:166 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:166 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:166 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:1661 [binder, in MetaCoq.Template.utils.All_Forall]
l:1669 [binder, in MetaCoq.Template.utils.All_Forall]
l:167 [binder, in MetaCoq.Template.utils.All_Forall]
l:167 [binder, in MetaCoq.Erasure.ELiftSubst]
l:1677 [binder, in MetaCoq.Template.utils.All_Forall]
l:168 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:168 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:168 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
l:1685 [binder, in MetaCoq.Template.utils.All_Forall]
l:169 [binder, in MetaCoq.Template.utils.MCList]
l:169 [binder, in MetaCoq.Template.monad_utils]
l:1694 [binder, in MetaCoq.Template.utils.All_Forall]
l:17 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
l:17 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
l:17 [binder, in MetaCoq.Template.AstUtils]
l:170 [binder, in MetaCoq.Template.Ast]
l:1717 [binder, in MetaCoq.Template.utils.All_Forall]
l:172 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:172 [binder, in MetaCoq.Template.utils.All_Forall]
l:1729 [binder, in MetaCoq.Template.utils.All_Forall]
l:1736 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1737 [binder, in MetaCoq.Template.utils.All_Forall]
l:174 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1742 [binder, in MetaCoq.Template.utils.All_Forall]
l:1743 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1744 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1746 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
l:175 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:175 [binder, in MetaCoq.Examples.tauto]
l:175 [binder, in MetaCoq.Template.LiftSubst]
l:1754 [binder, in MetaCoq.Template.utils.All_Forall]
l:176 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:176 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
l:1769 [binder, in MetaCoq.Template.utils.All_Forall]
l:177 [binder, in MetaCoq.Template.utils.All_Forall]
l:177 [binder, in MetaCoq.Template.utils.MCList]
l:177 [binder, in MetaCoq.Template.LiftSubst]
l:1777 [binder, in MetaCoq.Template.utils.All_Forall]
l:178 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
l:1784 [binder, in MetaCoq.Template.utils.All_Forall]
l:179 [binder, in MetaCoq.Template.BasicAst]
l:1791 [binder, in MetaCoq.Template.utils.All_Forall]
l:1798 [binder, in MetaCoq.Template.utils.All_Forall]
l:18 [binder, in MetaCoq.Template.Typing]
l:18 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
l:18 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:180 [binder, in MetaCoq.Template.monad_utils]
l:1803 [binder, in MetaCoq.Template.utils.All_Forall]
l:181 [binder, in MetaCoq.Template.utils.All_Forall]
l:1811 [binder, in MetaCoq.Template.utils.All_Forall]
l:1818 [binder, in MetaCoq.Template.utils.All_Forall]
l:182 [binder, in MetaCoq.Examples.tauto]
l:1823 [binder, in MetaCoq.Template.utils.All_Forall]
l:1828 [binder, in MetaCoq.Template.utils.All_Forall]
l:183 [binder, in MetaCoq.Template.common.uGraph]
l:1832 [binder, in MetaCoq.Template.utils.All_Forall]
l:184 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
l:184 [binder, in MetaCoq.Template.utils.MCList]
l:184 [binder, in MetaCoq.Examples.tauto]
l:184 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:184 [binder, in MetaCoq.Erasure.EWcbvEval]
l:1843 [binder, in MetaCoq.Template.utils.All_Forall]
l:185 [binder, in MetaCoq.Template.utils.All_Forall]
l:185 [binder, in MetaCoq.Template.Environment]
l:1853 [binder, in MetaCoq.Template.utils.All_Forall]
l:186 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
L:186 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:186 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:1861 [binder, in MetaCoq.Template.utils.All_Forall]
l:1868 [binder, in MetaCoq.Template.utils.All_Forall]
l:187 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
l:1876 [binder, in MetaCoq.Template.utils.All_Forall]
l:188 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
l:1883 [binder, in MetaCoq.Template.utils.All_Forall]
l:189 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:189 [binder, in MetaCoq.Template.utils.MCList]
l:1890 [binder, in MetaCoq.Template.utils.All_Forall]
l:1893 [binder, in MetaCoq.Template.utils.All_Forall]
l:1899 [binder, in MetaCoq.Template.utils.All_Forall]
l:19 [binder, in MetaCoq.Erasure.EInduction]
l:19 [binder, in MetaCoq.Erasure.EAstUtils]
l:190 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:1907 [binder, in MetaCoq.Template.utils.All_Forall]
l:191 [binder, in MetaCoq.Erasure.Extract]
l:191 [binder, in MetaCoq.Template.Environment]
L:191 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:1912 [binder, in MetaCoq.Template.utils.All_Forall]
l:1917 [binder, in MetaCoq.Template.utils.All_Forall]
l:192 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
l:192 [binder, in MetaCoq.Template.utils.All_Forall]
l:1922 [binder, in MetaCoq.Template.utils.All_Forall]
l:1927 [binder, in MetaCoq.Template.utils.All_Forall]
l:193 [binder, in MetaCoq.Template.monad_utils]
l:1932 [binder, in MetaCoq.Template.utils.All_Forall]
l:194 [binder, in MetaCoq.Template.common.uGraph]
l:1941 [binder, in MetaCoq.Template.utils.All_Forall]
l:195 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:195 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
l:195 [binder, in MetaCoq.Template.utils.MCList]
l:195 [binder, in MetaCoq.Template.Environment]
l:195 [binder, in MetaCoq.Erasure.EWcbvEval]
l:1959 [binder, in MetaCoq.Template.utils.All_Forall]
l:196 [binder, in MetaCoq.Erasure.EInduction]
L:196 [binder, in MetaCoq.Erasure.EArities]
l:196 [binder, in MetaCoq.Template.common.uGraph]
L:196 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:196 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:196 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:197 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
l:197 [binder, in MetaCoq.Template.common.uGraph]
l:197 [binder, in MetaCoq.Examples.tauto]
l:1975 [binder, in MetaCoq.Template.utils.All_Forall]
l:198 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
l:198 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:198 [binder, in MetaCoq.Template.Environment]
l:198 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1980 [binder, in MetaCoq.Template.utils.All_Forall]
l:199 [binder, in MetaCoq.Template.Universes]
l:199 [binder, in MetaCoq.Template.utils.All_Forall]
l:199 [binder, in MetaCoq.Template.utils.MCList]
l:1993 [binder, in MetaCoq.Template.utils.All_Forall]
l:2 [binder, in MetaCoq.Erasure.EAstUtils]
l:2 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:20 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:20 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
l:20 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:20 [binder, in MetaCoq.PCUIC.PCUICContexts]
l:20 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
l:200 [binder, in MetaCoq.Template.BasicAst]
l:2006 [binder, in MetaCoq.Template.utils.All_Forall]
l:201 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:201 [binder, in MetaCoq.Template.utils.MCList]
L:201 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:201 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:2012 [binder, in MetaCoq.Template.utils.All_Forall]
l:202 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:202 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:2020 [binder, in MetaCoq.Template.utils.All_Forall]
l:2027 [binder, in MetaCoq.Template.utils.All_Forall]
l:203 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:203 [binder, in MetaCoq.Template.utils.All_Forall]
l:203 [binder, in MetaCoq.Erasure.EWcbvEval]
l:2033 [binder, in MetaCoq.Template.utils.All_Forall]
l:2039 [binder, in MetaCoq.Template.utils.All_Forall]
l:204 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:204 [binder, in MetaCoq.Template.monad_utils]
l:204 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:204 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:2043 [binder, in MetaCoq.Template.utils.All_Forall]
l:2053 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
l:2054 [binder, in MetaCoq.Template.utils.All_Forall]
l:2058 [binder, in MetaCoq.Template.utils.All_Forall]
l:206 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:206 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
l:2063 [binder, in MetaCoq.Template.utils.All_Forall]
l:2072 [binder, in MetaCoq.Template.utils.All_Forall]
l:2078 [binder, in MetaCoq.Template.utils.All_Forall]
l:208 [binder, in MetaCoq.Template.utils.All_Forall]
l:208 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
l:2082 [binder, in MetaCoq.Template.utils.All_Forall]
l:2089 [binder, in MetaCoq.Template.utils.All_Forall]
l:209 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:209 [binder, in MetaCoq.Template.utils.MCList]
l:209 [binder, in MetaCoq.Template.Checker]
l:209 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:2097 [binder, in MetaCoq.Template.utils.All_Forall]
l:21 [binder, in MetaCoq.Template.utils.All_Forall]
l:21 [binder, in MetaCoq.Template.utils.MCList]
l:21 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
l:21 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:21 [binder, in MetaCoq.Erasure.EInlineProjections]
l:21 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l:21 [binder, in MetaCoq.Template.Induction]
l:21 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:210 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:210 [binder, in MetaCoq.Template.Environment]
L:210 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:2104 [binder, in MetaCoq.Template.utils.All_Forall]
l:211 [binder, in MetaCoq.Template.Typing]
l:2111 [binder, in MetaCoq.Template.utils.All_Forall]
l:2117 [binder, in MetaCoq.Template.utils.All_Forall]
l:212 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:212 [binder, in MetaCoq.Template.common.uGraph]
l:2121 [binder, in MetaCoq.Template.utils.All_Forall]
l:213 [binder, in MetaCoq.Erasure.ErasureFunction]
l:213 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:2139 [binder, in MetaCoq.Template.utils.All_Forall]
l:214 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
L:215 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:2150 [binder, in MetaCoq.Template.utils.All_Forall]
l:2159 [binder, in MetaCoq.Template.utils.All_Forall]
l:216 [binder, in MetaCoq.Erasure.EInduction]
l:216 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:2167 [binder, in MetaCoq.Template.utils.All_Forall]
l:217 [binder, in MetaCoq.Template.utils.MCList]
l:217 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:2175 [binder, in MetaCoq.Template.utils.All_Forall]
l:2184 [binder, in MetaCoq.Template.utils.All_Forall]
l:219 [binder, in MetaCoq.Template.utils.All_Forall]
l:219 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:2196 [binder, in MetaCoq.Template.utils.All_Forall]
l:22 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:22 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:22 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:22 [binder, in MetaCoq.Erasure.EAstUtils]
l:220 [binder, in MetaCoq.Template.common.uGraph]
l:2203 [binder, in MetaCoq.Template.utils.All_Forall]
l:221 [binder, in MetaCoq.Template.common.uGraph]
l:222 [binder, in MetaCoq.Template.utils.MCList]
l:222 [binder, in MetaCoq.Template.Checker]
l:222 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:223 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:223 [binder, in MetaCoq.Template.TypingWf]
l:2230 [binder, in MetaCoq.Template.utils.All_Forall]
l:224 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:224 [binder, in MetaCoq.Template.utils.MCList]
l:2244 [binder, in MetaCoq.Template.utils.All_Forall]
l:225 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:227 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:228 [binder, in MetaCoq.Template.utils.MCList]
l:228 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l:228 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:228 [binder, in MetaCoq.Template.Environment]
l:229 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:230 [binder, in MetaCoq.Template.utils.All_Forall]
l:232 [binder, in MetaCoq.Template.utils.MCList]
l:233 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:233 [binder, in MetaCoq.Template.common.uGraph]
l:234 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:234 [binder, in MetaCoq.Template.Environment]
l:235 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
l:235 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:235 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l:235 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:236 [binder, in MetaCoq.Template.utils.MCList]
l:236 [binder, in MetaCoq.Template.Environment]
l:2363 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
l:237 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:238 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:238 [binder, in MetaCoq.Template.common.uGraph]
l:239 [binder, in MetaCoq.Template.utils.MCList]
L:239 [binder, in MetaCoq.Erasure.EWcbvEval]
l:24 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:24 [binder, in MetaCoq.Erasure.EArities]
l:24 [binder, in MetaCoq.Template.AstUtils]
l:240 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:241 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:241 [binder, in MetaCoq.Template.utils.All_Forall]
l:241 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:241 [binder, in MetaCoq.PCUIC.PCUICAst]
l:242 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:242 [binder, in MetaCoq.Template.common.uGraph]
l:242 [binder, in MetaCoq.Template.utils.wGraph]
l:242 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:243 [binder, in MetaCoq.Template.common.uGraph]
l:244 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
L:244 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:2447 [binder, in MetaCoq.Template.utils.All_Forall]
l:245 [binder, in MetaCoq.Template.Universes]
l:2456 [binder, in MetaCoq.Template.utils.All_Forall]
l:246 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l:246 [binder, in MetaCoq.Template.TermEquality]
l:247 [binder, in MetaCoq.Template.utils.MCList]
l:247 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:247 [binder, in MetaCoq.Template.utils.wGraph]
l:2475 [binder, in MetaCoq.Template.utils.All_Forall]
l:248 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:248 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l:2483 [binder, in MetaCoq.Template.utils.All_Forall]
l:249 [binder, in MetaCoq.Template.utils.All_Forall]
L:249 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:2496 [binder, in MetaCoq.Template.utils.All_Forall]
l:25 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:25 [binder, in MetaCoq.Erasure.Extract]
l:25 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:251 [binder, in MetaCoq.Template.Typing]
l:2512 [binder, in MetaCoq.Template.utils.All_Forall]
l:252 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:252 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:253 [binder, in MetaCoq.Template.TermEquality]
L:254 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:254 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:2546 [binder, in MetaCoq.Template.utils.All_Forall]
l:255 [binder, in MetaCoq.Template.utils.MCList]
l:2557 [binder, in MetaCoq.Template.utils.All_Forall]
l:257 [binder, in MetaCoq.Template.utils.All_Forall]
l:257 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:2571 [binder, in MetaCoq.Template.utils.All_Forall]
l:258 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:2584 [binder, in MetaCoq.Template.utils.All_Forall]
l:259 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
L:259 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:259 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
l:2595 [binder, in MetaCoq.Template.utils.All_Forall]
l:26 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:26 [binder, in MetaCoq.Template.common.uGraph]
l:26 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
l:261 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:262 [binder, in MetaCoq.Template.Universes]
l:262 [binder, in MetaCoq.Template.utils.MCList]
l:263 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:265 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:265 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:265 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:265 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:265 [binder, in MetaCoq.Template.TypingWf]
l:266 [binder, in MetaCoq.Template.utils.All_Forall]
l:267 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L:268 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:268 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:269 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:269 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
L:27 [binder, in MetaCoq.Erasure.ErasureProperties]
l:27 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:270 [binder, in MetaCoq.Template.utils.MCList]
L:272 [binder, in MetaCoq.PCUIC.PCUICProgress]
l:272 [binder, in MetaCoq.Template.common.uGraph]
l:273 [binder, in MetaCoq.Template.common.uGraph]
l:273 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
L:273 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:274 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:275 [binder, in MetaCoq.Template.common.uGraph]
l:275 [binder, in MetaCoq.Template.WcbvEval]
l:276 [binder, in MetaCoq.Template.utils.All_Forall]
l:276 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:276 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:277 [binder, in MetaCoq.Template.WcbvEval]
l:278 [binder, in MetaCoq.Template.EtaExpand]
l:278 [binder, in MetaCoq.Template.utils.MCList]
l:279 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:28 [binder, in MetaCoq.Erasure.EArities]
l:28 [binder, in MetaCoq.Template.utils.MCList]
l:28 [binder, in MetaCoq.Template.common.uGraph]
l:28 [binder, in MetaCoq.Erasure.EAstUtils]
l:280 [binder, in MetaCoq.Template.Universes]
l:280 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:280 [binder, in MetaCoq.Template.common.uGraph]
l:281 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:282 [binder, in MetaCoq.Template.utils.MCList]
l:282 [binder, in MetaCoq.Template.common.uGraph]
l:283 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:283 [binder, in MetaCoq.Template.WcbvEval]
l:283 [binder, in MetaCoq.Erasure.EWcbvEval]
l:284 [binder, in MetaCoq.Template.Universes]
l:284 [binder, in MetaCoq.Template.common.uGraph]
l:285 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
l:286 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:286 [binder, in MetaCoq.Template.utils.All_Forall]
L:286 [binder, in MetaCoq.Template.common.uGraph]
l:286 [binder, in MetaCoq.Template.WcbvEval]
l:287 [binder, in MetaCoq.Template.Ast]
l:287 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
l:287 [binder, in MetaCoq.Template.common.uGraph]
l:287 [binder, in MetaCoq.Erasure.ERemoveParams]
l:288 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:288 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:289 [binder, in MetaCoq.Erasure.ERemoveParams]
l:29 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
l:29 [binder, in MetaCoq.Template.Normal]
l:29 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l:29 [binder, in MetaCoq.Erasure.EEtaExpanded]
l:29 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:29 [binder, in MetaCoq.Template.AstUtils]
l:290 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:290 [binder, in MetaCoq.Template.utils.MCList]
l:290 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
L:290 [binder, in MetaCoq.Template.common.uGraph]
l:290 [binder, in MetaCoq.Template.WcbvEval]
l:291 [binder, in MetaCoq.Template.common.uGraph]
l:291 [binder, in MetaCoq.Erasure.ERemoveParams]
l:291 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:292 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
l:292 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:293 [binder, in MetaCoq.Template.utils.All_Forall]
l:293 [binder, in MetaCoq.Template.common.uGraph]
l:293 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:293 [binder, in MetaCoq.Erasure.ERemoveParams]
l:293 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:293 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:295 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l:295 [binder, in MetaCoq.Erasure.ERemoveParams]
l:296 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:296 [binder, in MetaCoq.Template.utils.All_Forall]
l:296 [binder, in MetaCoq.Template.utils.MCList]
l:296 [binder, in MetaCoq.Template.common.uGraph]
l:297 [binder, in MetaCoq.Erasure.ERemoveParams]
l:297 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:298 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:299 [binder, in MetaCoq.Template.utils.All_Forall]
l:299 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:3 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
l:3 [binder, in MetaCoq.Template.utils.wGraph]
l:3 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:30 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:30 [binder, in MetaCoq.Template.utils.MCList]
l:30 [binder, in MetaCoq.Template.common.uGraph]
l:30 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
l:30 [binder, in MetaCoq.Erasure.EAstUtils]
l:30 [binder, in MetaCoq.Erasure.ECSubst]
l:300 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:300 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:300 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:301 [binder, in MetaCoq.Template.utils.MCList]
l:301 [binder, in MetaCoq.Template.common.uGraph]
l:302 [binder, in MetaCoq.Template.Universes]
l:302 [binder, in MetaCoq.Template.utils.All_Forall]
l:304 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:304 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:305 [binder, in MetaCoq.Template.utils.All_Forall]
l:305 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:306 [binder, in MetaCoq.Template.common.uGraph]
l:307 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:308 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:309 [binder, in MetaCoq.Template.utils.All_Forall]
l:309 [binder, in MetaCoq.Template.utils.MCList]
l:309 [binder, in MetaCoq.Template.common.uGraph]
l:309 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:309 [binder, in MetaCoq.Erasure.ERemoveParams]
l:309 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:31 [binder, in MetaCoq.Template.utils.All_Forall]
L:31 [binder, in MetaCoq.Erasure.EArities]
l:31 [binder, in MetaCoq.Template.TemplateMonad.Core]
l:31 [binder, in MetaCoq.Erasure.EWellformed]
l:31 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
l:31 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:311 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:311 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:311 [binder, in MetaCoq.Erasure.ERemoveParams]
l:311 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:312 [binder, in MetaCoq.Template.common.uGraph]
l:313 [binder, in MetaCoq.Template.utils.All_Forall]
l:313 [binder, in MetaCoq.Erasure.ERemoveParams]
l:314 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:315 [binder, in MetaCoq.Template.utils.MCList]
l:315 [binder, in MetaCoq.PCUIC.PCUICSR]
l:315 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:317 [binder, in MetaCoq.Template.utils.All_Forall]
l:317 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:317 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:317 [binder, in MetaCoq.Erasure.ERemoveParams]
l:317 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:319 [binder, in MetaCoq.Template.WcbvEval]
l:32 [binder, in MetaCoq.PCUIC.PCUICInversion]
l:32 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
l:32 [binder, in MetaCoq.Template.AstUtils]
l:32 [binder, in MetaCoq.Template.Induction]
l:320 [binder, in MetaCoq.Template.utils.All_Forall]
l:320 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:320 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:321 [binder, in MetaCoq.Erasure.ERemoveParams]
l:322 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:322 [binder, in MetaCoq.Template.utils.MCList]
l:323 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:324 [binder, in MetaCoq.Template.Universes]
l:324 [binder, in MetaCoq.Erasure.EWcbvEval]
l:325 [binder, in MetaCoq.Erasure.ERemoveParams]
l:326 [binder, in MetaCoq.Template.Ast]
l:326 [binder, in MetaCoq.Erasure.EWcbvEval]
l:327 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:327 [binder, in MetaCoq.Template.Checker]
l:328 [binder, in MetaCoq.Template.utils.All_Forall]
l:329 [binder, in MetaCoq.Template.Ast]
l:33 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:330 [binder, in MetaCoq.Template.utils.MCList]
l:331 [binder, in MetaCoq.Template.TypingWf]
l:331 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:334 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:334 [binder, in MetaCoq.Template.utils.All_Forall]
l:336 [binder, in MetaCoq.Template.utils.MCList]
l:34 [binder, in MetaCoq.Template.Universes]
l:34 [binder, in MetaCoq.Erasure.ECSubst]
l:34 [binder, in MetaCoq.Template.LiftSubst]
l:341 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:341 [binder, in MetaCoq.Template.TypingWf]
l:342 [binder, in MetaCoq.Template.utils.All_Forall]
l:343 [binder, in MetaCoq.Template.utils.MCList]
l:343 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:345 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:345 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:348 [binder, in MetaCoq.Template.TypingWf]
l:349 [binder, in MetaCoq.Template.utils.All_Forall]
l:349 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l:35 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
l:35 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
L:35 [binder, in MetaCoq.Erasure.ErasureProperties]
l:35 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
l:35 [binder, in MetaCoq.Template.monad_utils]
l:35 [binder, in MetaCoq.Erasure.EAstUtils]
l:35 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:35 [binder, in MetaCoq.Template.AstUtils]
l:351 [binder, in MetaCoq.Template.utils.MCList]
l:351 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
l:353 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:353 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:354 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:355 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:356 [binder, in MetaCoq.Template.common.uGraph]
l:357 [binder, in MetaCoq.Template.utils.All_Forall]
l:357 [binder, in MetaCoq.Template.utils.MCList]
l:357 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l:357 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:358 [binder, in MetaCoq.Erasure.EWcbvEval]
l:36 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:36 [binder, in MetaCoq.Erasure.Prelim]
l:360 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:360 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
l:361 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:361 [binder, in MetaCoq.Erasure.EWcbvEval]
l:362 [binder, in MetaCoq.Template.utils.All_Forall]
l:363 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:364 [binder, in MetaCoq.Template.utils.MCList]
l:364 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:364 [binder, in MetaCoq.Template.common.uGraph]
l:365 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l:369 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:370 [binder, in MetaCoq.Template.utils.MCList]
l:373 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:373 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:374 [binder, in MetaCoq.Template.EtaExpand]
l:375 [binder, in MetaCoq.Template.utils.MCList]
l:375 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:376 [binder, in MetaCoq.Template.utils.All_Forall]
l:376 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:376 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:378 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:379 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:379 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:38 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:38 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
l:38 [binder, in MetaCoq.Erasure.ESpineView]
L:38 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:38 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:38 [binder, in MetaCoq.Erasure.ECSubst]
l:380 [binder, in MetaCoq.Template.utils.MCList]
l:381 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:382 [binder, in MetaCoq.Template.EtaExpand]
l:383 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:384 [binder, in MetaCoq.Template.utils.MCList]
l:387 [binder, in MetaCoq.Template.EtaExpand]
l:388 [binder, in MetaCoq.Template.utils.All_Forall]
l:388 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:39 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:39 [binder, in MetaCoq.Erasure.Prelim]
l:390 [binder, in MetaCoq.Template.EtaExpand]
l:390 [binder, in MetaCoq.Template.utils.MCList]
l:391 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
L:391 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:391 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:393 [binder, in MetaCoq.Template.utils.MCList]
l:398 [binder, in MetaCoq.Template.utils.All_Forall]
l:398 [binder, in MetaCoq.Template.Typing]
l:4 [binder, in MetaCoq.Template.utils.MCList]
l:4 [binder, in MetaCoq.Template.TemplateCheckWf]
l:4 [binder, in MetaCoq.PCUIC.PCUICInductives]
l:4 [binder, in MetaCoq.Template.utils.MCString]
l:4 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
l:4 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:40 [binder, in MetaCoq.Template.utils.MCList]
l:40 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
L:40 [binder, in MetaCoq.Erasure.ErasureProperties]
l:40 [binder, in MetaCoq.Erasure.ESpineView]
l:40 [binder, in MetaCoq.Examples.tauto]
l:40 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:40 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:40 [binder, in MetaCoq.Template.AstUtils]
L:400 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:401 [binder, in MetaCoq.Template.utils.MCList]
l:401 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:401 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:401 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:404 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:405 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:405 [binder, in MetaCoq.Template.utils.MCList]
l:405 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:406 [binder, in MetaCoq.Template.utils.All_Forall]
l:407 [binder, in MetaCoq.Template.utils.MCList]
l:408 [binder, in MetaCoq.Template.common.uGraph]
l:41 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l:41 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:411 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:411 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L:412 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:415 [binder, in MetaCoq.Template.utils.All_Forall]
l:417 [binder, in MetaCoq.Template.utils.MCList]
l:417 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:419 [binder, in MetaCoq.Template.utils.MCList]
l:42 [binder, in MetaCoq.Template.utils.All_Forall]
l:42 [binder, in MetaCoq.Erasure.EGenericMapEnv]
l:421 [binder, in MetaCoq.Template.utils.MCList]
L:421 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:423 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
l:425 [binder, in MetaCoq.Template.utils.All_Forall]
l:427 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:427 [binder, in MetaCoq.Template.utils.wGraph]
l:429 [binder, in MetaCoq.Template.utils.MCList]
l:429 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:43 [binder, in MetaCoq.Erasure.EInduction]
l:43 [binder, in MetaCoq.Template.utils.MCOption]
l:43 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
l:43 [binder, in MetaCoq.Template.AstUtils]
l:430 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:432 [binder, in MetaCoq.Template.utils.All_Forall]
l:432 [binder, in MetaCoq.Template.utils.MCList]
l:432 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:432 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:434 [binder, in MetaCoq.PCUIC.PCUICAst]
l:437 [binder, in MetaCoq.Template.common.uGraph]
l:437 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:438 [binder, in MetaCoq.Template.utils.All_Forall]
l:438 [binder, in MetaCoq.PCUIC.PCUICAst]
l:439 [binder, in MetaCoq.Template.utils.MCList]
l:439 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:44 [binder, in MetaCoq.Template.WcbvEval]
L:44 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:44 [binder, in MetaCoq.Erasure.EAstUtils]
l:44 [binder, in MetaCoq.Template.Induction]
l:442 [binder, in MetaCoq.Template.utils.All_Forall]
l:442 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:443 [binder, in MetaCoq.PCUIC.PCUICAst]
l:444 [binder, in MetaCoq.Template.utils.MCList]
l:444 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:445 [binder, in MetaCoq.Template.utils.All_Forall]
l:445 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:446 [binder, in MetaCoq.Template.utils.MCList]
l:448 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:449 [binder, in MetaCoq.Template.utils.All_Forall]
l:449 [binder, in MetaCoq.Template.utils.MCList]
l:449 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:45 [binder, in MetaCoq.Erasure.EInduction]
l:45 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
l:45 [binder, in MetaCoq.Template.monad_utils]
l:45 [binder, in MetaCoq.Template.AstUtils]
l:452 [binder, in MetaCoq.Template.utils.MCList]
l:452 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:453 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:454 [binder, in MetaCoq.Template.utils.All_Forall]
l:454 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:454 [binder, in MetaCoq.PCUIC.PCUICAst]
l:455 [binder, in MetaCoq.Template.utils.MCList]
l:457 [binder, in MetaCoq.Template.utils.wGraph]
l:459 [binder, in MetaCoq.Template.utils.MCList]
l:459 [binder, in MetaCoq.Template.utils.wGraph]
l:46 [binder, in MetaCoq.Template.utils.bytestring]
l:46 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:46 [binder, in MetaCoq.Examples.tauto]
l:46 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:46 [binder, in MetaCoq.Template.TypingWf]
l:46 [binder, in MetaCoq.Erasure.Prelim]
l:461 [binder, in MetaCoq.PCUIC.PCUICAst]
l:462 [binder, in MetaCoq.Template.utils.All_Forall]
l:462 [binder, in MetaCoq.PCUIC.PCUICEquality]
L:463 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:465 [binder, in MetaCoq.Template.utils.MCList]
l:465 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:468 [binder, in MetaCoq.Template.utils.All_Forall]
l:468 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:469 [binder, in MetaCoq.Template.utils.wGraph]
l:47 [binder, in MetaCoq.Translations.translation_utils]
l:47 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:470 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:471 [binder, in MetaCoq.Template.Universes]
l:471 [binder, in MetaCoq.Template.utils.MCList]
l:471 [binder, in MetaCoq.Template.EnvironmentTyping]
l:471 [binder, in MetaCoq.PCUIC.PCUICSR]
l:472 [binder, in MetaCoq.Template.utils.All_Forall]
l:472 [binder, in MetaCoq.Erasure.ErasureFunction]
L:472 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:473 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:474 [binder, in MetaCoq.Template.Universes]
l:474 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:475 [binder, in MetaCoq.Template.utils.MCList]
l:475 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:476 [binder, in MetaCoq.Template.utils.All_Forall]
l:477 [binder, in MetaCoq.Erasure.ErasureFunction]
l:478 [binder, in MetaCoq.Template.utils.MCList]
l:478 [binder, in MetaCoq.Template.EnvironmentTyping]
l:478 [binder, in MetaCoq.Template.common.uGraph]
l:478 [binder, in MetaCoq.Template.utils.wGraph]
l:478 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:479 [binder, in MetaCoq.Template.utils.wGraph]
l:48 [binder, in MetaCoq.Template.utils.All_Forall]
l:48 [binder, in MetaCoq.Template.utils.MCOption]
l:48 [binder, in MetaCoq.Erasure.EAstUtils]
l:48 [binder, in MetaCoq.Template.LiftSubst]
l:48 [binder, in MetaCoq.Erasure.Prelim]
l:480 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:480 [binder, in MetaCoq.Template.utils.MCList]
l:480 [binder, in MetaCoq.Template.common.uGraph]
l:481 [binder, in MetaCoq.Erasure.ErasureFunction]
l:481 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:482 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:482 [binder, in MetaCoq.Template.common.uGraph]
l:482 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:483 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:483 [binder, in MetaCoq.Template.utils.All_Forall]
l:483 [binder, in MetaCoq.Template.utils.MCList]
L:484 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:485 [binder, in MetaCoq.Erasure.ErasureFunction]
l:485 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:486 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:487 [binder, in MetaCoq.Template.utils.MCList]
l:488 [binder, in MetaCoq.Template.utils.MCList]
l:489 [binder, in MetaCoq.Template.Universes]
l:489 [binder, in MetaCoq.Template.utils.All_Forall]
l:49 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
l:49 [binder, in MetaCoq.Erasure.ESpineView]
l:49 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:49 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:49 [binder, in MetaCoq.Template.AstUtils]
l:491 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:492 [binder, in MetaCoq.Template.utils.MCList]
l:493 [binder, in MetaCoq.Template.utils.MCList]
L:493 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:494 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:495 [binder, in MetaCoq.Template.utils.MCList]
l:495 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l:495 [binder, in MetaCoq.Erasure.ErasureFunction]
l:496 [binder, in MetaCoq.Template.utils.All_Forall]
l:499 [binder, in MetaCoq.Template.utils.MCList]
l:499 [binder, in MetaCoq.Template.common.uGraph]
l:5 [binder, in MetaCoq.Erasure.EInduction]
l:5 [binder, in MetaCoq.Template.utils.MCString]
l:5 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
l:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:5 [binder, in MetaCoq.Template.Induction]
l:50 [binder, in MetaCoq.Erasure.EArities]
l:50 [binder, in MetaCoq.Template.utils.MCList]
l:50 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:50 [binder, in MetaCoq.PCUIC.PCUICSR]
l:50 [binder, in MetaCoq.Erasure.EAstUtils]
l:501 [binder, in MetaCoq.Template.utils.All_Forall]
l:501 [binder, in MetaCoq.Erasure.ErasureFunction]
l:503 [binder, in MetaCoq.Template.EnvironmentTyping]
l:505 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:505 [binder, in MetaCoq.Template.common.uGraph]
l:506 [binder, in MetaCoq.Template.utils.All_Forall]
l:506 [binder, in MetaCoq.Template.EnvironmentTyping]
l:506 [binder, in MetaCoq.Erasure.ErasureFunction]
l:507 [binder, in MetaCoq.Template.utils.MCList]
l:507 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:51 [binder, in MetaCoq.Template.monad_utils]
l:51 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:511 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:511 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:511 [binder, in MetaCoq.Erasure.ErasureFunction]
l:512 [binder, in MetaCoq.Template.utils.All_Forall]
l:512 [binder, in MetaCoq.Template.utils.MCList]
l:514 [binder, in MetaCoq.Template.utils.MCList]
l:517 [binder, in MetaCoq.Template.utils.MCList]
l:518 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:52 [binder, in MetaCoq.Erasure.EInduction]
l:52 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:52 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:52 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:520 [binder, in MetaCoq.Template.utils.All_Forall]
l:520 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:521 [binder, in MetaCoq.Template.utils.MCList]
l:522 [binder, in MetaCoq.Erasure.ErasureFunction]
l:526 [binder, in MetaCoq.Template.utils.All_Forall]
l:527 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:528 [binder, in MetaCoq.Erasure.ErasureFunction]
l:53 [binder, in MetaCoq.Template.Universes]
l:53 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
l:53 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:53 [binder, in MetaCoq.PCUIC.PCUICGlobalEnv]
l:53 [binder, in MetaCoq.Template.TypingWf]
l:53 [binder, in MetaCoq.Template.LiftSubst]
l:530 [binder, in MetaCoq.Template.utils.MCList]
l:531 [binder, in MetaCoq.Template.utils.All_Forall]
l:533 [binder, in MetaCoq.Template.utils.MCList]
l:533 [binder, in MetaCoq.Erasure.ErasureFunction]
l:534 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:535 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:536 [binder, in MetaCoq.Template.utils.All_Forall]
l:536 [binder, in MetaCoq.Template.utils.MCList]
l:538 [binder, in MetaCoq.Erasure.ErasureFunction]
l:539 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:539 [binder, in MetaCoq.PCUIC.PCUICAst]
l:54 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
l:54 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
l:54 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:540 [binder, in MetaCoq.Template.utils.All_Forall]
l:543 [binder, in MetaCoq.Template.utils.MCList]
l:543 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:543 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:544 [binder, in MetaCoq.Template.utils.All_Forall]
l:549 [binder, in MetaCoq.Template.utils.MCList]
l:549 [binder, in MetaCoq.PCUIC.PCUICAst]
l:55 [binder, in MetaCoq.Erasure.EInduction]
l:55 [binder, in MetaCoq.Template.utils.All_Forall]
l:55 [binder, in MetaCoq.PCUIC.PCUICValidity]
l:55 [binder, in MetaCoq.Erasure.EAstUtils]
l:55 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
l:551 [binder, in MetaCoq.Template.utils.All_Forall]
l:552 [binder, in MetaCoq.Template.utils.MCList]
l:553 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
l:553 [binder, in MetaCoq.Template.common.uGraph]
l:554 [binder, in MetaCoq.Template.utils.MCList]
l:555 [binder, in MetaCoq.Template.utils.MCList]
l:555 [binder, in MetaCoq.PCUIC.PCUICInductives]
l:556 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:557 [binder, in MetaCoq.Template.utils.All_Forall]
l:557 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:558 [binder, in MetaCoq.Template.common.uGraph]
l:56 [binder, in MetaCoq.Template.utils.MCList]
l:56 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
l:56 [binder, in MetaCoq.Template.WcbvEval]
l:56 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:56 [binder, in MetaCoq.Template.monad_utils]
l:56 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:56 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:560 [binder, in MetaCoq.Erasure.ErasureFunction]
l:561 [binder, in MetaCoq.Template.utils.MCList]
l:561 [binder, in MetaCoq.PCUIC.PCUICAst]
l:562 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:563 [binder, in MetaCoq.Template.utils.MCList]
l:563 [binder, in MetaCoq.Template.common.uGraph]
l:564 [binder, in MetaCoq.Template.utils.All_Forall]
l:565 [binder, in MetaCoq.Erasure.ErasureFunction]
l:566 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:568 [binder, in MetaCoq.Template.utils.MCList]
l:568 [binder, in MetaCoq.Template.common.uGraph]
l:569 [binder, in MetaCoq.Erasure.ErasureFunction]
l:57 [binder, in MetaCoq.Erasure.EInduction]
l:57 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:570 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:572 [binder, in MetaCoq.Template.utils.MCList]
l:573 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:573 [binder, in MetaCoq.Erasure.ErasureFunction]
l:575 [binder, in MetaCoq.Template.utils.MCList]
l:576 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:578 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:578 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:58 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:58 [binder, in MetaCoq.Erasure.EAstUtils]
L:58 [binder, in MetaCoq.Erasure.Prelim]
l:580 [binder, in MetaCoq.Template.utils.All_Forall]
l:580 [binder, in MetaCoq.Template.utils.MCList]
l:580 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:581 [binder, in MetaCoq.Template.common.uGraph]
l:581 [binder, in MetaCoq.Erasure.ErasureFunction]
l:584 [binder, in MetaCoq.Template.utils.MCList]
l:584 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:586 [binder, in MetaCoq.Template.utils.All_Forall]
l:586 [binder, in MetaCoq.Template.common.uGraph]
l:586 [binder, in MetaCoq.Erasure.ErasureFunction]
l:587 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:587 [binder, in MetaCoq.Template.utils.wGraph]
l:589 [binder, in MetaCoq.Template.utils.MCList]
l:589 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:59 [binder, in MetaCoq.Template.utils.MCList]
l:59 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
l:59 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
L:59 [binder, in MetaCoq.Erasure.Prelim]
l:590 [binder, in MetaCoq.Erasure.ErasureFunction]
l:590 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:591 [binder, in MetaCoq.Template.utils.All_Forall]
l:591 [binder, in MetaCoq.Template.common.uGraph]
l:591 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:592 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:594 [binder, in MetaCoq.Template.utils.MCList]
l:594 [binder, in MetaCoq.Erasure.ErasureFunction]
l:596 [binder, in MetaCoq.Template.utils.All_Forall]
l:596 [binder, in MetaCoq.Template.common.uGraph]
l:597 [binder, in MetaCoq.Template.utils.MCList]
l:6 [binder, in MetaCoq.Template.utils.All_Forall]
l:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l:6 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
l:60 [binder, in MetaCoq.Template.utils.MCList]
l:60 [binder, in MetaCoq.Template.TypingWf]
l:60 [binder, in MetaCoq.Template.Induction]
l:600 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:601 [binder, in MetaCoq.Template.utils.All_Forall]
l:606 [binder, in MetaCoq.Template.utils.MCList]
l:607 [binder, in MetaCoq.Template.utils.All_Forall]
l:609 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:609 [binder, in MetaCoq.Erasure.ErasureFunction]
l:612 [binder, in MetaCoq.Template.utils.All_Forall]
l:614 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:614 [binder, in MetaCoq.Erasure.ErasureFunction]
l:617 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:618 [binder, in MetaCoq.Template.utils.MCList]
l:619 [binder, in MetaCoq.Template.utils.All_Forall]
l:62 [binder, in MetaCoq.Erasure.EInduction]
l:62 [binder, in MetaCoq.Template.utils.All_Forall]
l:62 [binder, in MetaCoq.Erasure.EAstUtils]
l:620 [binder, in MetaCoq.Erasure.ErasureFunction]
l:622 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:623 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:625 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:626 [binder, in MetaCoq.Erasure.ErasureFunction]
L:627 [binder, in MetaCoq.Template.utils.All_Forall]
l:628 [binder, in MetaCoq.Template.utils.All_Forall]
l:628 [binder, in MetaCoq.Template.common.uGraph]
l:629 [binder, in MetaCoq.Template.Typing]
l:63 [binder, in MetaCoq.Template.Kernames]
l:63 [binder, in MetaCoq.Template.monad_utils]
l:63 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
L:631 [binder, in MetaCoq.Template.utils.All_Forall]
l:632 [binder, in MetaCoq.Template.common.uGraph]
l:633 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:634 [binder, in MetaCoq.Template.utils.All_Forall]
L:636 [binder, in MetaCoq.Template.utils.All_Forall]
l:636 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:636 [binder, in MetaCoq.Erasure.ErasureFunction]
l:638 [binder, in MetaCoq.Template.utils.All_Forall]
l:64 [binder, in MetaCoq.Template.Universes]
l:64 [binder, in MetaCoq.Template.WfAst]
l:64 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:64 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:641 [binder, in MetaCoq.Template.utils.All_Forall]
l:641 [binder, in MetaCoq.Template.common.uGraph]
l:641 [binder, in MetaCoq.Erasure.ErasureFunction]
l:644 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:645 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:645 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:646 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:647 [binder, in MetaCoq.Erasure.ErasureFunction]
l:647 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:65 [binder, in MetaCoq.Template.Universes]
l:65 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
l:65 [binder, in MetaCoq.PCUIC.PCUICSR]
l:651 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
l:653 [binder, in MetaCoq.Erasure.ErasureFunction]
l:654 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:659 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:66 [binder, in MetaCoq.Erasure.EInduction]
l:66 [binder, in MetaCoq.Template.utils.ReflectEq]
l:66 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
l:66 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:66 [binder, in MetaCoq.Template.TypingWf]
l:66 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
l:660 [binder, in MetaCoq.Template.Universes]
l:660 [binder, in MetaCoq.PCUIC.PCUICSpine]
l:662 [binder, in MetaCoq.Template.utils.MCList]
l:662 [binder, in MetaCoq.PCUIC.PCUICSR]
l:664 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:667 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:668 [binder, in MetaCoq.Template.utils.MCList]
l:669 [binder, in MetaCoq.PCUIC.PCUICEquality]
l:669 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:67 [binder, in MetaCoq.Template.WfAst]
l:67 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
l:67 [binder, in MetaCoq.Erasure.EAstUtils]
l:670 [binder, in MetaCoq.Template.utils.All_Forall]
l:670 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:674 [binder, in MetaCoq.Template.utils.MCList]
l:674 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:675 [binder, in MetaCoq.PCUIC.PCUICSR]
l:675 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:677 [binder, in MetaCoq.Template.Universes]
l:678 [binder, in MetaCoq.Template.utils.MCList]
l:679 [binder, in MetaCoq.Template.utils.All_Forall]
l:68 [binder, in MetaCoq.Erasure.EInduction]
l:68 [binder, in MetaCoq.Template.utils.MCList]
l:68 [binder, in MetaCoq.Template.Normal]
l:68 [binder, in MetaCoq.Template.Reflect]
l:681 [binder, in MetaCoq.Template.Universes]
l:681 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:683 [binder, in MetaCoq.Template.Universes]
l:684 [binder, in MetaCoq.Template.utils.All_Forall]
l:688 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:689 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:69 [binder, in MetaCoq.Template.utils.All_Forall]
l:69 [binder, in MetaCoq.Template.utils.MCList]
l:69 [binder, in MetaCoq.Erasure.EDeps]
l:69 [binder, in MetaCoq.Template.utils.wGraph]
l:69 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:69 [binder, in MetaCoq.Template.LiftSubst]
L:69 [binder, in MetaCoq.Erasure.Prelim]
l:691 [binder, in MetaCoq.Template.utils.All_Forall]
l:691 [binder, in MetaCoq.Template.common.uGraph]
l:692 [binder, in MetaCoq.Template.utils.MCList]
l:696 [binder, in MetaCoq.Template.utils.MCList]
l:696 [binder, in MetaCoq.Template.common.uGraph]
l:698 [binder, in MetaCoq.Template.Universes]
l:698 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:698 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:7 [binder, in MetaCoq.Template.utils.wGraph]
l:70 [binder, in MetaCoq.Template.Universes]
l:70 [binder, in MetaCoq.Template.utils.MCOption]
l:70 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:70 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:70 [binder, in MetaCoq.Erasure.EAstUtils]
L:70 [binder, in MetaCoq.Erasure.Prelim]
l:700 [binder, in MetaCoq.Template.Universes]
l:700 [binder, in MetaCoq.Template.utils.All_Forall]
l:700 [binder, in MetaCoq.Template.utils.MCList]
l:702 [binder, in MetaCoq.Template.utils.MCList]
l:705 [binder, in MetaCoq.Template.utils.MCList]
l:706 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:71 [binder, in MetaCoq.Template.Induction]
l:711 [binder, in MetaCoq.Template.utils.MCList]
l:712 [binder, in MetaCoq.Template.Universes]
l:714 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:718 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:72 [binder, in MetaCoq.Erasure.EInduction]
l:72 [binder, in MetaCoq.Translations.times_bool_fun]
l:72 [binder, in MetaCoq.Template.utils.bytestring]
l:72 [binder, in MetaCoq.Template.Reflect]
l:72 [binder, in MetaCoq.Erasure.EAstUtils]
l:722 [binder, in MetaCoq.Erasure.ErasureFunction]
l:726 [binder, in MetaCoq.Template.utils.MCList]
l:726 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:728 [binder, in MetaCoq.Erasure.ErasureFunction]
l:729 [binder, in MetaCoq.Template.Universes]
l:73 [binder, in MetaCoq.Template.utils.wGraph]
l:73 [binder, in MetaCoq.Template.LiftSubst]
l:733 [binder, in MetaCoq.Erasure.ErasureFunction]
l:737 [binder, in MetaCoq.Template.Universes]
l:738 [binder, in MetaCoq.Erasure.ErasureFunction]
l:738 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:738 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:739 [binder, in MetaCoq.Template.utils.MCList]
l:74 [binder, in MetaCoq.Template.WfAst]
l:741 [binder, in MetaCoq.Template.utils.All_Forall]
l:742 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:746 [binder, in MetaCoq.Template.Universes]
l:746 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:749 [binder, in MetaCoq.Template.utils.All_Forall]
l:749 [binder, in MetaCoq.Template.utils.MCList]
l:749 [binder, in MetaCoq.Erasure.ErasureFunction]
l:75 [binder, in MetaCoq.Translations.times_bool_fun]
l:75 [binder, in MetaCoq.Template.utils.All_Forall]
l:75 [binder, in MetaCoq.Template.utils.MCList]
l:750 [binder, in MetaCoq.Template.Universes]
l:751 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:752 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:755 [binder, in MetaCoq.Template.utils.All_Forall]
l:755 [binder, in MetaCoq.Template.utils.MCList]
l:755 [binder, in MetaCoq.Erasure.ErasureFunction]
l:756 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:756 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:76 [binder, in MetaCoq.Template.Reflect]
l:76 [binder, in MetaCoq.Template.utils.MCOption]
l:76 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:760 [binder, in MetaCoq.Template.utils.MCList]
l:760 [binder, in MetaCoq.Erasure.ErasureFunction]
l:761 [binder, in MetaCoq.Template.utils.All_Forall]
l:761 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:765 [binder, in MetaCoq.Erasure.ErasureFunction]
l:765 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:766 [binder, in MetaCoq.Template.utils.MCList]
l:767 [binder, in MetaCoq.Template.utils.All_Forall]
l:767 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:77 [binder, in MetaCoq.Template.Universes]
l:77 [binder, in MetaCoq.Template.utils.MCList]
l:77 [binder, in MetaCoq.Template.utils.wGraph]
l:77 [binder, in MetaCoq.Template.monad_utils]
l:77 [binder, in MetaCoq.Erasure.EAstUtils]
l:775 [binder, in MetaCoq.Template.utils.All_Forall]
l:776 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:777 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:78 [binder, in MetaCoq.Erasure.EInduction]
l:78 [binder, in MetaCoq.PCUIC.PCUICAst]
l:78 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:78 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:780 [binder, in MetaCoq.Template.utils.MCList]
l:782 [binder, in MetaCoq.Template.utils.All_Forall]
l:785 [binder, in MetaCoq.Template.utils.wGraph]
l:785 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:789 [binder, in MetaCoq.Template.utils.wGraph]
l:79 [binder, in MetaCoq.Template.utils.MCList]
l:79 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
l:791 [binder, in MetaCoq.Template.utils.All_Forall]
l:791 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:792 [binder, in MetaCoq.Template.utils.wGraph]
l:798 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:798 [binder, in MetaCoq.Template.utils.wGraph]
l:8 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:8 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
L:8 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
l:8 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
l:80 [binder, in MetaCoq.Template.Universes]
l:80 [binder, in MetaCoq.Template.utils.All_Forall]
l:80 [binder, in MetaCoq.Erasure.Extract]
l:80 [binder, in MetaCoq.Template.Reflect]
l:80 [binder, in MetaCoq.Template.utils.MCOption]
L:800 [binder, in MetaCoq.Template.utils.All_Forall]
l:801 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:802 [binder, in MetaCoq.Template.utils.All_Forall]
l:804 [binder, in MetaCoq.Template.utils.wGraph]
L:805 [binder, in MetaCoq.Template.utils.All_Forall]
l:806 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:807 [binder, in MetaCoq.Template.utils.wGraph]
l:809 [binder, in MetaCoq.Template.utils.All_Forall]
l:81 [binder, in MetaCoq.Template.utils.MCList]
l:81 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
l:81 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
l:81 [binder, in MetaCoq.Erasure.EAstUtils]
L:811 [binder, in MetaCoq.Template.utils.All_Forall]
l:811 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:812 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l:812 [binder, in MetaCoq.Template.utils.wGraph]
l:814 [binder, in MetaCoq.Template.utils.All_Forall]
l:815 [binder, in MetaCoq.Template.utils.wGraph]
l:815 [binder, in MetaCoq.PCUIC.PCUICConversion]
l:815 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:818 [binder, in MetaCoq.Template.utils.All_Forall]
l:819 [binder, in MetaCoq.Template.utils.wGraph]
l:82 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:820 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
l:821 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:822 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:822 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:823 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:823 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
l:825 [binder, in MetaCoq.Template.utils.MCList]
l:825 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:826 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:826 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:827 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:828 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:829 [binder, in MetaCoq.Template.utils.MCList]
l:83 [binder, in MetaCoq.Template.utils.MCList]
l:83 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
l:83 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:83 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:830 [binder, in MetaCoq.Template.utils.MCList]
l:832 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:84 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:840 [binder, in MetaCoq.Template.utils.MCList]
l:846 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:849 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:85 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:85 [binder, in MetaCoq.Template.utils.All_Forall]
l:852 [binder, in MetaCoq.Template.utils.All_Forall]
l:852 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:855 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:855 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:856 [binder, in MetaCoq.Template.utils.MCList]
l:858 [binder, in MetaCoq.Template.utils.MCList]
l:858 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:859 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:86 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:86 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:863 [binder, in MetaCoq.Template.utils.All_Forall]
l:864 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:868 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:869 [binder, in MetaCoq.Template.utils.All_Forall]
l:87 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:87 [binder, in MetaCoq.Template.Typing]
l:872 [binder, in MetaCoq.Template.utils.MCList]
l:872 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
l:877 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:878 [binder, in MetaCoq.Template.utils.All_Forall]
l:878 [binder, in MetaCoq.Template.utils.MCList]
l:88 [binder, in MetaCoq.Template.utils.MCList]
l:88 [binder, in MetaCoq.Erasure.ELiftSubst]
l:88 [binder, in MetaCoq.Template.monad_utils]
l:88 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:884 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:886 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:887 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:888 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:889 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:89 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:89 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:890 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:892 [binder, in MetaCoq.Template.utils.MCList]
l:899 [binder, in MetaCoq.Template.utils.MCList]
l:9 [binder, in MetaCoq.Template.WfAst]
l:9 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:9 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
l:9 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
l:9 [binder, in MetaCoq.Erasure.EAstUtils]
l:9 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:9 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:9 [binder, in MetaCoq.Erasure.EWcbvEval]
l:90 [binder, in MetaCoq.Template.utils.MCList]
l:90 [binder, in MetaCoq.Template.WfAst]
l:903 [binder, in MetaCoq.Template.utils.MCList]
l:904 [binder, in MetaCoq.Template.utils.All_Forall]
l:907 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:908 [binder, in MetaCoq.Template.utils.MCList]
l:91 [binder, in MetaCoq.PCUIC.PCUICConfluence]
l:911 [binder, in MetaCoq.Template.utils.MCList]
l:914 [binder, in MetaCoq.Template.utils.All_Forall]
l:92 [binder, in MetaCoq.Template.utils.MCList]
l:92 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:921 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:924 [binder, in MetaCoq.Template.utils.All_Forall]
l:926 [binder, in MetaCoq.Template.utils.MCList]
l:928 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:93 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:93 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
L:93 [binder, in MetaCoq.PCUIC.PCUICNormal]
l:931 [binder, in MetaCoq.Template.utils.All_Forall]
l:937 [binder, in MetaCoq.Template.utils.All_Forall]
l:938 [binder, in MetaCoq.PCUIC.PCUICTyping]
l:94 [binder, in MetaCoq.Template.utils.MCList]
l:94 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
l:94 [binder, in MetaCoq.PCUIC.PCUICAst]
l:94 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:944 [binder, in MetaCoq.Template.utils.All_Forall]
l:944 [binder, in MetaCoq.PCUIC.PCUICTyping]
l:95 [binder, in MetaCoq.Template.Universes]
l:95 [binder, in MetaCoq.Template.EnvironmentTyping]
l:95 [binder, in MetaCoq.Template.monad_utils]
l:953 [binder, in MetaCoq.Template.utils.All_Forall]
l:96 [binder, in MetaCoq.Template.utils.MCList]
l:96 [binder, in MetaCoq.Erasure.EInlineProjections]
l:96 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
l:961 [binder, in MetaCoq.PCUIC.PCUICReduction]
l:963 [binder, in MetaCoq.Template.utils.All_Forall]
l:97 [binder, in MetaCoq.Template.Universes]
l:97 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:97 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:972 [binder, in MetaCoq.Template.utils.All_Forall]
l:972 [binder, in MetaCoq.PCUIC.PCUICTyping]
l:98 [binder, in MetaCoq.Template.LiftSubst]
l:982 [binder, in MetaCoq.Template.utils.All_Forall]
l:989 [binder, in MetaCoq.Template.utils.wGraph]
l:99 [binder, in MetaCoq.Erasure.EInduction]
l:99 [binder, in MetaCoq.Template.utils.MCList]
L:99 [binder, in MetaCoq.Translations.param_cheap_packed]
L:992 [binder, in MetaCoq.Template.utils.All_Forall]
l:994 [binder, in MetaCoq.Template.utils.All_Forall]
L:997 [binder, in MetaCoq.Template.utils.All_Forall]
lΔ:927 [binder, in MetaCoq.PCUIC.PCUICReduction]
| 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) |