| 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) |
O
O [constructor, in MetaCoq.Examples.demo]oargs:418 [binder, in MetaCoq.Erasure.EWcbvEval]
obpack [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
obseq:17 [binder, in MetaCoq.Template.Transform]
occ_betweenP [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
odd [definition, in MetaCoq.Examples.demo]
odd':44 [binder, in MetaCoq.Examples.add_constructor]
odd':46 [binder, in MetaCoq.Examples.add_constructor]
of_global_env_cons [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
of_global_env_cons [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
oi [definition, in MetaCoq.PCUIC.PCUICInductives]
oib [definition, in MetaCoq.PCUIC.PCUICInductives]
oib':158 [binder, in MetaCoq.Erasure.Extract]
oib:101 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
oib:1010 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
oib:109 [binder, in MetaCoq.Template.Pretty]
oib:130 [binder, in MetaCoq.Template.AstUtils]
oib:140 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
oib:157 [binder, in MetaCoq.Erasure.Extract]
oib:170 [binder, in MetaCoq.Template.TypingWf]
oib:187 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
oib:260 [binder, in MetaCoq.Template.Environment]
oib:264 [binder, in MetaCoq.Template.Environment]
oib:270 [binder, in MetaCoq.Template.Environment]
oib:350 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
oib:39 [binder, in MetaCoq.Template.Pretty]
oib:670 [binder, in MetaCoq.Erasure.ErasureFunction]
oib:818 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
oib:928 [binder, in MetaCoq.Erasure.ErasureFunction]
oib:930 [binder, in MetaCoq.Erasure.ErasureFunction]
oie:116 [binder, in MetaCoq.Template.Pretty]
oind:167 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
oind:56 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
oind:73 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
onarities:1008 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
OnConstructor [section, in MetaCoq.PCUIC.PCUICInductiveInversion]
OnConstructorExt [section, in MetaCoq.PCUIC.PCUICInductiveInversion]
oncstrs:991 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
oncs:836 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
oncs:889 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
oncs:910 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
oncs:912 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
onctx [abbreviation, in MetaCoq.Template.BasicAst]
onctxP [lemma, in MetaCoq.Template.BasicAst]
onctx_k [definition, in MetaCoq.Template.BasicAst]
onctx_All_fold [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
onctx_rel_pred1_refl' [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
onctx_rel_pred1_refl [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
onctx_eq_ctx_impl [lemma, in MetaCoq.PCUIC.PCUICEquality]
onctx_eq_ctx_trans [lemma, in MetaCoq.PCUIC.PCUICEquality]
onctx_eq_ctx_sym [lemma, in MetaCoq.PCUIC.PCUICEquality]
onctx_eq_ctx [lemma, in MetaCoq.PCUIC.PCUICEquality]
onctx_k_P [lemma, in MetaCoq.PCUIC.PCUICAst]
onctx_k_shift [lemma, in MetaCoq.PCUIC.PCUICAst]
onctx_k_rev [lemma, in MetaCoq.PCUIC.PCUICAst]
onctx_test [lemma, in MetaCoq.PCUIC.PCUICAst]
onctx_rel [definition, in MetaCoq.PCUIC.Syntax.PCUICInduction]
onctx_rel [definition, in MetaCoq.PCUIC.Syntax.PCUICDepth]
onctx_fold_context_term [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
onc:1239 [binder, in MetaCoq.Erasure.ErasureFunction]
onc:912 [binder, in MetaCoq.Erasure.ErasureFunction]
onc:919 [binder, in MetaCoq.Erasure.ErasureFunction]
ondecl [definition, in MetaCoq.Template.BasicAst]
ondeclP [lemma, in MetaCoq.Template.BasicAst]
ondecl_on_free_vars_decl [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
ondecl_map [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ondecl':775 [binder, in MetaCoq.Erasure.ErasureFunction]
ondecl:774 [binder, in MetaCoq.Erasure.ErasureFunction]
onec:890 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
ones [definition, in MetaCoq.Examples.demo]
one_inductive_entry [record, in MetaCoq.Template.Ast]
one_inductive_entry [record, in MetaCoq.PCUIC.PCUICAst]
one_inductive_body [record, in MetaCoq.Erasure.EAst]
one_inductive_entry [record, in MetaCoq.Erasure.EAst]
one_pt_i [definition, in MetaCoq.Examples.demo]
one_list_i [definition, in MetaCoq.Examples.demo]
one_i2 [definition, in MetaCoq.Examples.demo]
one_i [definition, in MetaCoq.Examples.demo]
OnFreeVars [section, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pcheck [variable, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pind [variable, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pinfer [variable, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Pprod [variable, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.Psort [variable, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.PΓ [variable, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
OnFreeVars.PΓ_rel [variable, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
onfvs_app [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
onib:100 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
onib:125 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
onib:142 [binder, in MetaCoq.PCUIC.PCUICElimination]
onib:175 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
onindices:996 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
OnInductives [section, in MetaCoq.PCUIC.PCUICInductives]
OnInductives [section, in MetaCoq.PCUIC.PCUICInductives]
OnInductives [section, in MetaCoq.Erasure.ErasureFunction]
oni:874 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
OnOne_local_2 [section, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2 [inductive, in MetaCoq.Template.utils.All_Forall]
OnOne2All [inductive, in MetaCoq.Template.utils.All_Forall]
OnOne2All_All3 [lemma, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
OnOne2All_All3 [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_nth_error_impl [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_impl_All_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_nth_error_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_nth_error [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_impl [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_split [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_impl_exist_and_All_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_impl_exist_and_All [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_ind_l [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_exist [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_sym [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_map_all [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_map [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_mapP [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_length2 [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_length [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_app [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_All2_mix_left [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_All_mix_left [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2All_tl [constructor, in MetaCoq.Template.utils.All_Forall]
OnOne2All_hd [constructor, in MetaCoq.Template.utils.All_Forall]
OnOne2All_map2_map_all [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
OnOne2All_map2 [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
OnOne2All_map2_map_all [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2All_All2_All2 [lemma, in MetaCoq.Template.TypingWf]
OnOne2All_on_Trel_eq_red_redl [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2All_red_redl [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2All2i_OnOne2All [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
OnOne2All2i_OnOne2All [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2i [inductive, in MetaCoq.Template.utils.All_Forall]
OnOne2i_nth_error_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_nth_error [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_impl [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_split [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_impl_exist_and_All_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_impl_exist_and_All [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_ind_l [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_exist [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_sym [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_map [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_mapP [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_length [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_app_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_app [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_All_mix_left [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2i_tl [constructor, in MetaCoq.Template.utils.All_Forall]
OnOne2i_hd [constructor, in MetaCoq.Template.utils.All_Forall]
OnOne2_All_All [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_All2_All2 [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_impl_All_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_nth_error_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_nth_error [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_impl [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_split [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_impl_exist_and_All_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_impl_exist_and_All [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_ind_l [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_exist [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_sym [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_map [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_mapP [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_length [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_app_r [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_app [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_All_mix_left [lemma, in MetaCoq.Template.utils.All_Forall]
OnOne2_tl [constructor, in MetaCoq.Template.utils.All_Forall]
OnOne2_hd [constructor, in MetaCoq.Template.utils.All_Forall]
OnOne2_map2 [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
OnOne2_local_env_impl_test [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_test_context_k [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_mapi_context [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_map_context [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_map [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_ondecl_impl [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_impl [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env_length [instance, in MetaCoq.PCUIC.utils.PCUICOnOne]
onone2_localenv_cons_tl [constructor, in MetaCoq.PCUIC.utils.PCUICOnOne]
onone2_localenv_def [constructor, in MetaCoq.PCUIC.utils.PCUICOnOne]
onone2_localenv_cons_abs [constructor, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_local_env [inductive, in MetaCoq.PCUIC.utils.PCUICOnOne]
OnOne2_All_All2 [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_All_OnOne2 [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_All2i_All2 [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
OnOne2_local_env_pred1_ctx_over [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_pars_pred1_ctx_over [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_disj [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_local_env_All2_fold [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_local_env_exist' [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_exist' [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_local_env_apply_dep [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_local_env_apply [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_sigma [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_apply_All [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_apply [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_prod_assoc [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_prod [lemma, in MetaCoq.PCUIC.PCUICConfluence]
OnOne2_local_env_forget_types [lemma, in MetaCoq.PCUIC.PCUICSR]
OnOne2_All2i_All2i [lemma, in MetaCoq.PCUIC.PCUICSR]
OnOne2_All2_All2 [lemma, in MetaCoq.PCUIC.PCUICSR]
OnOne2_local_env_All2_fold [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
OnOne2_All_All [lemma, in MetaCoq.Template.TypingWf]
OnOne2_All2 [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2_prod_inv_refl_r [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2_prod_inv [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2_context_redl [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2_on_Trel_eq_red_redl [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2_on_Trel_eq_unit [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2_red_redl [lemma, in MetaCoq.PCUIC.PCUICReduction]
OnOne2_ctx_inst [lemma, in MetaCoq.PCUIC.PCUICSpine]
onprojs:994 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
onsorts:995 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
OnSubterm [section, in MetaCoq.Erasure.EWcbvEvalEtaInd]
OnUdecl [section, in MetaCoq.SafeChecker.PCUICSafeChecker]
onud:978 [binder, in MetaCoq.Erasure.ErasureFunction]
onu:82 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
onu:91 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
onu:970 [binder, in MetaCoq.Erasure.ErasureFunction]
on_free_vars_type [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_branch_type [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_subst0 [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_subst [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_branch_context [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_case_predicate_context [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_ctx_tip [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_ctx_free_vars_strengthenP [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_free_vars_rename [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
on_global_univ_init_env [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
on_udecl_mono [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
on_snd_eq_id_spec [lemma, in MetaCoq.Template.BasicAst]
on_udecl_on_udecl_prop [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
on_udecl_prop [definition, in MetaCoq.PCUIC.PCUICWeakeningEnv]
on_Trel_eq [abbreviation, in MetaCoq.Template.utils.MCRelations]
on_Trel [definition, in MetaCoq.Template.utils.MCRelations]
on_rel [definition, in MetaCoq.Template.utils.MCRelations]
on_fst [definition, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
on_minductive_wf_params [lemma, in MetaCoq.PCUIC.PCUICArities]
on_ctx_universes [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
on_decl_universes [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
on_universes_subst [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
on_universes_lift [lemma, in MetaCoq.PCUIC.PCUICWfUniverses]
on_universes [definition, in MetaCoq.PCUIC.PCUICWfUniverses]
on_global_decl_wf [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
on_global_env_impl [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
on_pair [definition, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
on_wf_local_decl [definition, in MetaCoq.Template.Typing]
on_ctx_free_vars_snoc [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
on_constructor_closed [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
on_constructor_closed_arities [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
on_cofix [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_fix [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_proj [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_case [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_app [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_letin [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_lambda [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_evar [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_atom [constructor, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_subterms [inductive, in MetaCoq.Erasure.EWcbvEvalEtaInd]
on_one_decl_test_decl [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
on_one_decl_test_impl [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
on_one_decl_mapi_context [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
on_one_decl_map [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
on_one_decl_map_na [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
on_one_decl_impl [lemma, in MetaCoq.PCUIC.utils.PCUICOnOne]
on_one_decl [definition, in MetaCoq.PCUIC.utils.PCUICOnOne]
on_free_vars_all_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_def [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_ass [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_fix_context_weak [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_fix_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_inst_case_context_weak [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_inst_case_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snocS [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc_def [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc_ass [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_closedP_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_closedP [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_any_xpredT [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_All_fold [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context_xpredT [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_smash [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_snoc [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_lift_context0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_lift_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_vdef [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_vass [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_snoc [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_inst_case_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_fix_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_extend [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars_xpredT [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_on_ctx_free_vars [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_tip [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_concat [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_unfold_cofix [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_cofix_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_unfold_fix [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_fix_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_to_extended_list [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_map2_cstr_args [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_subst_instance [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_map [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms_inds [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_expand_lets_k [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_extended_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_implP [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_k [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_all_term [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_all_term [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_mkApps [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift0_above [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift0 [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_proper_pointwise [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars_proper [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_ctx_free_vars [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst1 [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst_gen [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_terms [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_lift [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx_proper [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ctx [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_proper_pointwise [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl_proper [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_decl [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_subst_instance [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_proper_pointwise [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_proper [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars_ext [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_free_vars [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
on_projections_decl [lemma, in MetaCoq.PCUIC.PCUICInductives]
on_inductive_sort_inst [lemma, in MetaCoq.PCUIC.PCUICInductives]
on_inductive_sort [lemma, in MetaCoq.PCUIC.PCUICInductives]
on_inductive_inst [lemma, in MetaCoq.PCUIC.PCUICInductives]
on_minductive_wf_params_indices_inst [lemma, in MetaCoq.PCUIC.PCUICInductives]
on_minductive_wf_params_indices [lemma, in MetaCoq.PCUIC.PCUICInductives]
on_constructor_closed_indices [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_udecl_prop_poly_bounded [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_projections_indices [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_constructor_inst_pars_indices [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_constructor_inst [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_constructor_inst_wf_args [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_constructor_subst [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_constructor_wf_args [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
on_contexts_subst_ctx [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_over_firstn_skipn [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_over_pred1_ctx [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_rename_context [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_fold_context_k [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_context_k [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_over_refl [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_mapi_inv [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_mapi [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_app_inv_left [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_over_app [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_app_inv [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_app_ex [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_app' [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_impl_ind [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_impl [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_length [abbreviation, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_app [abbreviation, in MetaCoq.PCUIC.PCUICParallelReduction]
on_contexts_over [abbreviation, in MetaCoq.PCUIC.PCUICParallelReduction]
on_decls_over [abbreviation, in MetaCoq.PCUIC.PCUICParallelReduction]
on_inl [definition, in MetaCoq.Template.common.uGraph]
on_free_vars_ctx_inst_case_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
on_free_vars_rename [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
on_subterm [definition, in MetaCoq.SafeChecker.PCUICSafeRetyping]
on_free_vars_ind_predicate_context [lemma, in MetaCoq.SafeChecker.PCUICSafeRetyping]
on_free_vars_ctx_All_fold_over [lemma, in MetaCoq.PCUIC.PCUICAlpha]
on_global_decl_d [projection, in MetaCoq.SafeChecker.PCUICWfEnv]
on_udecl_udecl [projection, in MetaCoq.SafeChecker.PCUICWfEnv]
on_global_decls_dec [record, in MetaCoq.SafeChecker.PCUICWfEnv]
on_free_vars_projs [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_mon [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_terms_proper [instance, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_case_predicate_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_expand_lets_k [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_subst_k [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_mfix [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ind_params [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_cstr_branch_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ind_predicate_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_k_eq [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_fst [definition, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_ctx_trans [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_decl_trans_on_free_vars_decl [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
on_free_vars_decl_lift_impl [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
on_free_vars_decl_lift [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
on_edge:875 [binder, in MetaCoq.Template.utils.wGraph]
on_global_decls_prefix [lemma, in MetaCoq.Erasure.ErasureFunction]
on_global_env_ind [lemma, in MetaCoq.Erasure.ErasureFunction]
on_minductive_wf_params_indices_inst_weaken [lemma, in MetaCoq.Erasure.ErasureFunction]
on_minductive_wf_params_weaken [lemma, in MetaCoq.Erasure.ErasureFunction]
on_ctx_free_vars_xpredT [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_prod_inv [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_prod [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctxs [definition, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_ctx_free_vars_app [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_decls [definition, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_ctx_inst_case_context_nil [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_up [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_free_vars_rename_S [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
on_cond:255 [binder, in MetaCoq.Template.Checker]
on_hyps_sound [lemma, in MetaCoq.Examples.tauto]
on_hyp_sound [lemma, in MetaCoq.Examples.tauto]
on_hyps_size [lemma, in MetaCoq.Examples.tauto]
on_hyp_size [lemma, in MetaCoq.Examples.tauto]
on_hyps [definition, in MetaCoq.Examples.tauto]
on_hyp [definition, in MetaCoq.Examples.tauto]
on_snd_eq_id_spec [lemma, in MetaCoq.Erasure.ELiftSubst]
on_Some_or_None [definition, in MetaCoq.Template.utils.MCOption]
on_SomeP [lemma, in MetaCoq.Template.utils.MCOption]
on_Some [definition, in MetaCoq.Template.utils.MCOption]
on_some [definition, in MetaCoq.Template.utils.MCOption]
on_free_vars_any_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
on_free_vars_ctx_fix_context_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
on_ctx_free_vars_fix_context_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
on_free_vars_ctx_inst_case_context_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
on_ctx_free_vars_inst_case_context_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
on_free_vars_ctx_closed_xpredT [lemma, in MetaCoq.PCUIC.PCUICConfluence]
on_one_decl_compare_decl [lemma, in MetaCoq.PCUIC.PCUICConfluence]
on_free_vars_ctx_inst_case_context_xpred0 [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_free_vars_ctx_snoc_def_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_free_vars_ctx_snoc_ass_inv [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_free_vars_subst [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_free_vars_shiftnP_S [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_fvs_letin [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_fvs_lambda [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_fvs_prod [lemma, in MetaCoq.PCUIC.PCUICConversion]
on_wf_local_decl [definition, in MetaCoq.PCUIC.PCUICTyping]
on_local_decl_glob [definition, in MetaCoq.PCUIC.PCUICTyping]
on_pi2 [definition, in MetaCoq.Template.utils.MCProd]
on_snd_eq_spec [lemma, in MetaCoq.Template.utils.MCProd]
on_snd_on_snd [lemma, in MetaCoq.Template.utils.MCProd]
on_snd [definition, in MetaCoq.Template.utils.MCProd]
on_free_vars_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
on_free_vars_decl_eq [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
on_local_decl [definition, in MetaCoq.PCUIC.PCUICContextConversion]
on_local_decl [definition, in MetaCoq.PCUIC.Syntax.PCUICInduction]
on_free_vars_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICSR]
on_free_vars_ctx_tip [lemma, in MetaCoq.PCUIC.PCUICSR]
on_constructor_closed_indices_inst [lemma, in MetaCoq.PCUIC.PCUICSR]
on_free_vars_closedn [lemma, in MetaCoq.PCUIC.PCUICSR]
on_constructor_wf_arities_pars_args [lemma, in MetaCoq.PCUIC.PCUICSR]
on_constructor_closed_indices [lemma, in MetaCoq.PCUIC.PCUICSR]
on_free_vars_ctx_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICSR]
on_constructor_wf_args [lemma, in MetaCoq.PCUIC.PCUICSR]
on_free_vars_ctx_onctx_k [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
on_ctx_free_vars_xpredT_skipn [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
on_ctx_free_vars_xpredT_snoc [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
on_free_vars_subst_consn [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
on_udecl_poly_bounded [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
on_ctx_free_vars_fold [definition, in MetaCoq.PCUIC.PCUICContextReduction]
on_ctx_free_vars_cons [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
on_inst_case_context [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
on_option [definition, in MetaCoq.Template.TypingWf]
on_global_inductive_wf_bodies [lemma, in MetaCoq.Template.TypingWf]
on_inductive_wf_params [lemma, in MetaCoq.Template.TypingWf]
on_global_inductive_wf_params [lemma, in MetaCoq.Template.TypingWf]
on_global_decls_extends_not_fresh [lemma, in MetaCoq.Template.TypingWf]
on_global_env_impl [lemma, in MetaCoq.Template.TypingWf]
on_global_decl_impl [lemma, in MetaCoq.Template.TypingWf]
on_declared_projection [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_constructor [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_inductive [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_minductive [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_declared_constant [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
on_universes_true [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
opaque:10 [binder, in MetaCoq.Template.TemplateMonad.Core]
opaque:36 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
opaque:9 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
open_decl_proj [definition, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
open_decl [definition, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
open_term [abbreviation, in MetaCoq.PCUIC.PCUICConfluence]
open_context [abbreviation, in MetaCoq.PCUIC.PCUICContextConversion]
opta:15 [binder, in MetaCoq.Template.utils.MCOption]
optimize [definition, in MetaCoq.Erasure.EInlineProjections]
optimize [section, in MetaCoq.Erasure.EInlineProjections]
optimize [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize [section, in MetaCoq.Erasure.EOptimizePropDiscr]
optimized_abstract_env_impl [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_ext_impl [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_prop [instance, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_ext_prop [instance, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_struct [instance, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimized_abstract_env_ext_struct [instance, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optimize_program_expanded [definition, in MetaCoq.Erasure.EInlineProjections]
optimize_program_wf [definition, in MetaCoq.Erasure.EInlineProjections]
optimize_program [definition, in MetaCoq.Erasure.EInlineProjections]
optimize_env_wf [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_decl_wf [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_wellformed_decl_irrel [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_wellformed_irrel [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_wellformed [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_env_expanded [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_env_eq [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_env_extends' [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_expanded_decl_irrel [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_expanded_decl [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_expanded_irrel [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_expanded [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_correct [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_env' [definition, in MetaCoq.Erasure.EInlineProjections]
optimize_env [definition, in MetaCoq.Erasure.EInlineProjections]
optimize_decl [definition, in MetaCoq.Erasure.EInlineProjections]
optimize_constant_decl [definition, in MetaCoq.Erasure.EInlineProjections]
optimize_cunfold_cofix [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_cunfold_fix [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_cofix_subst [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_fix_subst [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_iota_red [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_substl [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_csubst [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_mkApps [lemma, in MetaCoq.Erasure.EInlineProjections]
optimize_prop_discr_optimization [definition, in MetaCoq.Erasure.ETransform]
optimize_program_expanded [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_program_wf [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_program [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env_wf [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_decl_wf [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_wellformed_decl_irrel [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_wellformed_irrel [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_wellformed [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env_expanded [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env_eq [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env_extends' [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_expanded_decl_irrel [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_expanded_decl [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_expanded_irrel [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_expanded [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_correct [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env' [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_env [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_decl [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_constant_decl [definition, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_nth [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_cunfold_cofix [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_cunfold_fix [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_cofix_subst [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_fix_subst [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_iota_red [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_substl [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_csubst [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optimize_mkApps [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
optim_make_wf_env_ext [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
optim_pop [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
option_map_decl_type_map_decl [lemma, in MetaCoq.Template.BasicAst]
option_map_decl_body_map_decl [lemma, in MetaCoq.Template.BasicAst]
option_UIP [instance, in MetaCoq.PCUIC.PCUICWcbvEval]
option_is_none [definition, in MetaCoq.Erasure.Extract]
option_edge_of_level [definition, in MetaCoq.Template.common.uGraph]
option_map_Some [lemma, in MetaCoq.Template.utils.MCOption]
option_map_id [lemma, in MetaCoq.Template.utils.MCOption]
option_map_proper [instance, in MetaCoq.Template.utils.MCOption]
option_map_ext [lemma, in MetaCoq.Template.utils.MCOption]
option_map_two [lemma, in MetaCoq.Template.utils.MCOption]
option_default_ext [lemma, in MetaCoq.Template.utils.MCOption]
option_default [definition, in MetaCoq.Template.utils.MCOption]
option_get [definition, in MetaCoq.Template.utils.MCOption]
option_monad_exc [instance, in MetaCoq.Template.monad_utils]
option_monad [instance, in MetaCoq.Template.monad_utils]
option_instance [inductive, in MetaCoq.Template.TemplateMonad.Common]
opt_bool_to_bool [definition, in MetaCoq.Template.Checker]
opt_wcbv_flags [definition, in MetaCoq.Erasure.EWcbvEval]
Or [constructor, in MetaCoq.Examples.tauto]
orPL [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
orPL [lemma, in MetaCoq.Template.utils.MCPred]
orPR [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
orPR [lemma, in MetaCoq.Template.utils.MCPred]
orP_Proper [instance, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
orP_Proper [instance, in MetaCoq.Template.utils.MCPred]
other_adj [lemma, in MetaCoq.Translations.MiniHoTT]
other_adj [lemma, in MetaCoq.Translations.MiniHoTT_paths]
OT_byte.eq_dec [definition, in MetaCoq.Template.utils.bytestring]
OT_byte.compare [definition, in MetaCoq.Template.utils.bytestring]
OT_byte.lt_not_eq [lemma, in MetaCoq.Template.utils.bytestring]
OT_byte.lt_trans [lemma, in MetaCoq.Template.utils.bytestring]
OT_byte.eq_trans [lemma, in MetaCoq.Template.utils.bytestring]
OT_byte.eq_sym [lemma, in MetaCoq.Template.utils.bytestring]
OT_byte.eq_refl [lemma, in MetaCoq.Template.utils.bytestring]
OT_byte.lt [definition, in MetaCoq.Template.utils.bytestring]
OT_byte.eq [definition, in MetaCoq.Template.utils.bytestring]
OT_byte.t [definition, in MetaCoq.Template.utils.bytestring]
OT_byte [module, in MetaCoq.Template.utils.bytestring]
o':101 [binder, in MetaCoq.Template.Reflect]
o':108 [binder, in MetaCoq.Template.utils.MCOption]
o':51 [binder, in MetaCoq.Template.Transform]
o':91 [binder, in MetaCoq.Template.Reflect]
o:100 [binder, in MetaCoq.Template.Reflect]
o:104 [binder, in MetaCoq.Template.utils.MCOption]
o:107 [binder, in MetaCoq.Template.utils.MCOption]
o:2 [binder, in MetaCoq.Erasure.EWellformed]
o:204 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:215 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
o:218 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:236 [binder, in MetaCoq.Erasure.Extract]
o:244 [binder, in MetaCoq.Template.TypingWf]
o:262 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:276 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:3 [binder, in MetaCoq.Translations.param_binary]
o:30 [binder, in MetaCoq.Template.utils.MCOption]
o:31 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
o:403 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:424 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:472 [binder, in MetaCoq.Template.EnvironmentTyping]
o:475 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:496 [binder, in MetaCoq.PCUIC.PCUICConfluence]
o:50 [binder, in MetaCoq.Template.Transform]
o:7 [binder, in MetaCoq.Template.utils.MCOption]
o:76 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
o:79 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
o:89 [binder, in MetaCoq.Template.utils.MCOption]
o:90 [binder, in MetaCoq.Template.Reflect]
| 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) |