| 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 | (602 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 | (298 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 | (151 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 | (46 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 | (42 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 | (21 entries) |
| Moduleid 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 | (24 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 | (3 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 | (17 entries) |
Global Index
B
base [library]C
CE [moduleid, in counter_ex]CE.Dom_ce [lemma, in counter_ex]
CE.D1 [definition, in counter_ex]
CE.D1_ok [lemma, in counter_ex]
CE.D1_typ [lemma, in counter_ex]
CE.D2 [definition, in counter_ex]
CE.D2_typ [lemma, in counter_ex]
CE.D2_ok [lemma, in counter_ex]
CE.PTSe_dont_have_PiInj [lemma, in counter_ex]
CE.PTSe_PiInj [definition, in counter_ex]
CE.ze_pi_eq [lemma, in counter_ex]
counter_ex [library]
E
env [library]env_mod.nth_sub_inf [lemma, in env]
env_mod.trunc [inductive, in env]
env_mod.fun_item [lemma, in env]
_ ↓ _ ⊂ _ (Typ_scope) [notation, in env]
env_mod.trunc_S [constructor, in env]
env_mod.nth_sub_sup [lemma, in env]
env_mod.item_trunc [lemma, in env]
env_mod.ins_S [constructor, in env]
env_mod.trunc_O [constructor, in env]
env_mod.ins_item_ge [lemma, in env]
env_mod.sub_O [constructor, in env]
env_mod.item_hd [constructor, in env]
env_mod.sub_S [constructor, in env]
env_mod.ins_item_lt [lemma, in env]
env_mod.item [inductive, in env]
env_mod.item_tl [constructor, in env]
env_mod.ins_in_env [inductive, in env]
env_mod.ins_item_lift_lt [lemma, in env]
env_mod.Env [definition, in env]
env_mod.nth_sub_item_inf [lemma, in env]
env_mod.item_lift [definition, in env]
env_mod [moduleid, in env]
env_mod.nth_sub_eq [lemma, in env]
env_mod.ins_O [constructor, in env]
_ ↓ _ ∈ _ (Typ_scope) [notation, in env]
env_mod.sub_in_env [inductive, in env]
env_mod.gt_O [lemma, in env]
F
final_mod.strip_var [lemma, in final_result]final_mod.PTSe_SR [lemma, in final_result]
final_mod.FromPTSATR_to_PTS [lemma, in final_result]
final_mod.strip_var_ [lemma, in final_result]
final_mod.FromPTSATR_to_PTSe_trans [lemma, in final_result]
final_mod.FromPTSATR_to_PTSe [lemma, in final_result]
final_mod.PTSe_SR_trans [lemma, in final_result]
final_mod.PTS_equiv_PTSe [lemma, in final_result]
final_mod.FromPTS_to_PTSATR [lemma, in final_result]
final_mod [moduleid, in final_result]
final_result [library]
G
glue [library]glue_mod.weak_type_shape [lemma, in glue]
glue_mod.ErasedTermConfluence [lemma, in glue]
glue_mod.ErasedContextSwitch [lemma, in glue]
glue_mod.L33' [lemma, in glue]
glue_mod.peq_not_Pi_sort [lemma, in glue]
glue_mod.L43_ [lemma, in glue]
glue_mod.ErasedTypeConversion [lemma, in glue]
glue_mod [moduleid, in glue]
glue_mod.L33 [lemma, in glue]
M
Mpts [moduleid, in counter_ex]Mpts.Ax [definition, in counter_ex]
Mpts.Ax0 [constructor, in counter_ex]
Mpts.Ax1 [constructor, in counter_ex]
Mpts.Ax2 [constructor, in counter_ex]
Mpts.Ax3 [constructor, in counter_ex]
Mpts.iAx [inductive, in counter_ex]
Mpts.iRel [inductive, in counter_ex]
Mpts.Rel [definition, in counter_ex]
Mpts.Rel0 [constructor, in counter_ex]
Mpts.Rel1 [constructor, in counter_ex]
Mpts.Rel2 [constructor, in counter_ex]
Mpts.Rel3 [constructor, in counter_ex]
Msorts [moduleid, in counter_ex]
Msorts.iSorts [inductive, in counter_ex]
Msorts.Sorts [definition, in counter_ex]
Msorts.U [constructor, in counter_ex]
Msorts.V [constructor, in counter_ex]
Msorts.V' [constructor, in counter_ex]
Msorts.W [constructor, in counter_ex]
Msorts.W' [constructor, in counter_ex]
P
PTS_ATR_mod.reds_Pi_ [lemma, in typ_annot]PTS_ATR_mod.typ_peq [inductive, in typ_annot]
PTS_ATR_mod.env_conv_wf [lemma, in typ_annot]
PTS_ATR_mod.env_conv1 [inductive, in typ_annot]
PTS_ATR_mod.reds_App___ [lemma, in typ_annot]
PTS_ATR_mod.typ_exp [constructor, in typ_annot]
PTS_ATR_mod.typ_pcompat [lemma, in typ_annot]
PTS_ATR_mod.red_in_env_reds [lemma, in typ_annot]
PTS_ATR_mod.typ_red_trans [lemma, in typ_annot]
PTS_ATR_mod.conv_in_env_peq [lemma, in typ_annot]
PTS_ATR_mod.reds_La [lemma, in typ_annot]
PTS_ATR_mod.reds_subst_gen [lemma, in typ_annot]
PTS_ATR_mod.sub_in_env_item [lemma, in typ_annot]
PTS_ATR_mod.red_item [lemma, in typ_annot]
PTS_ATR_mod.eq_subst_gen [lemma, in typ_annot]
PTS_ATR_mod.typ_exp_trans [lemma, in typ_annot]
PTS_ATR_mod.SR_trans [lemma, in typ_annot]
PTS_ATR_mod.relocate [lemma, in typ_annot]
PTS_ATR_mod.thinning_reds_n [lemma, in typ_annot]
PTS_ATR_mod.pgen_pi [lemma, in typ_annot]
PTS_ATR_mod.reds_App_ [lemma, in typ_annot]
PTS_ATR_mod.conv_in_env_reds [lemma, in typ_annot]
PTS_ATR_mod.wf_item [lemma, in typ_annot]
PTS_ATR_mod.env_red [inductive, in typ_annot]
PTS_ATR_mod.typ_reds_intro [constructor, in typ_annot]
PTS_ATR_mod.env_red_wf [lemma, in typ_annot]
PTS_ATR_mod.reds_subst [lemma, in typ_annot]
_ ⊣ (Typ_scope) [notation, in typ_annot]
PTS_ATR_mod.c_sym [lemma, in typ_annot]
PTS_ATR_mod.env_conv1_wf [lemma, in typ_annot]
PTS_ATR_mod.typ_pi [constructor, in typ_annot]
PTS_ATR_mod.peq_thinning [lemma, in typ_annot]
_ ⊢ _ ▹▹ _ : _ (Typ_scope) [notation, in typ_annot]
PTS_ATR_mod.typ_beta [constructor, in typ_annot]
PTS_ATR_mod.pgen_app [lemma, in typ_annot]
PTS_ATR_mod.env_red_to_conv [lemma, in typ_annot]
PTS_ATR_mod.r_trans [constructor, in typ_annot]
PTS_ATR_mod.typ_reds_trans_ [lemma, in typ_annot]
pts_sig.Rel [axiom, in base]
PTS_ATR_mod.typ_red [constructor, in typ_annot]
PTS_ATR_mod.typ_peq_intro2 [constructor, in typ_annot]
PTS_ATR_mod.r_step [constructor, in typ_annot]
PTS_ATR_mod.thinning_reds [lemma, in typ_annot]
PTS_ATR_mod.ChurchRosser [lemma, in typ_annot]
PTS_ATR_mod.typ_app [constructor, in typ_annot]
PTS_ATR_mod.fun_item_lift [lemma, in typ_annot]
PTS_ATR_mod.red_in_env [lemma, in typ_annot]
PTS_ATR_mod.typ_ind2 [lemma, in typ_annot]
PTS_ATR_mod.reds_App__ [lemma, in typ_annot]
PTS_ATR_mod.typ_reds [inductive, in typ_annot]
PTS_ATR_mod.typ_reds_relocate [lemma, in typ_annot]
PTS_ATR_mod [moduleid, in typ_annot]
PTS_ATR_mod.c1_sym [lemma, in typ_annot]
PTS_ATR_mod.c_step [constructor, in typ_annot]
PTS_ATR_mod.conv1_in_env [lemma, in typ_annot]
PTS_ATR_mod.reds_Pi [lemma, in typ_annot]
PTS_ATR_mod.OSDiamond [lemma, in typ_annot]
PTS_ATR_mod.env_red_cons [lemma, in typ_annot]
PTS_ATR_mod.typ_sort [constructor, in typ_annot]
PTS_ATR_mod.SR_trans' [lemma, in typ_annot]
PTS_ATR_mod.typ_reds_trans [constructor, in typ_annot]
PTS_ATR_mod.wf_from_peq [lemma, in typ_annot]
PTS_ATR_mod.c_refl [constructor, in typ_annot]
PTS_ATR_mod.wf_from_typ [lemma, in typ_annot]
PTS_ATR_mod.sub_trunc [lemma, in typ_annot]
PTS_ATR_mod.subst_gen [lemma, in typ_annot]
PTS_ATR_mod.env_conv_cons [lemma, in typ_annot]
PTS_ATR_mod.env_red1_to_conv1 [lemma, in typ_annot]
PTS_ATR_mod.red1_intro [constructor, in typ_annot]
PTS_ATR_mod.wf_nil [constructor, in typ_annot]
PTS_ATR_mod.ConvSort [lemma, in typ_annot]
PTS_ATR_mod.weakening [lemma, in typ_annot]
PTS_ATR_mod.pgen_la [lemma, in typ_annot]
PTS_ATR_mod.PiInj [lemma, in typ_annot]
pts_sig [moduleid, in base]
PTS_ATR_mod.reds_to_conv [lemma, in typ_annot]
PTS_ATR_mod.peq_thinning_n [lemma, in typ_annot]
PTS_ATR_mod.thinning [lemma, in typ_annot]
PTS_ATR_mod.typ [inductive, in typ_annot]
PTS_ATR_mod.red1_in_env [lemma, in typ_annot]
PTS_ATR_mod.SubDiam [lemma, in typ_annot]
PTS_ATR_mod.typ_peq_to_red [lemma, in typ_annot]
PTS_ATR_mod.conv1_intro [constructor, in typ_annot]
PTS_ATR_mod.thinning_n [lemma, in typ_annot]
PTS_ATR_mod.env_conv [inductive, in typ_annot]
PTS_ATR_mod.reds_refl_lt [lemma, in typ_annot]
PTS_ATR_mod.pgen_var [lemma, in typ_annot]
PTS_ATR_mod.env_red1_wf [lemma, in typ_annot]
PTS_ATR_mod.reds_App [lemma, in typ_annot]
PTS_ATR_mod.reds_typ_pcompat [lemma, in typ_annot]
PTS_ATR_mod.conv_item [lemma, in typ_annot]
PTS_ATR_mod.reds_refl_rt [lemma, in typ_annot]
PTS_ATR_mod.pgen_sort [lemma, in typ_annot]
PTS_ATR_mod.typ_reds_to_red_ [lemma, in typ_annot]
PTS_ATR_mod.wf_cons [constructor, in typ_annot]
PTS_ATR_mod.typ_peq_intro [constructor, in typ_annot]
pts_sig.Ax [axiom, in base]
PTS_ATR_mod.wf_from_typ_reds [lemma, in typ_annot]
PTS_ATR_mod.env_red1 [inductive, in typ_annot]
PTS_ATR_mod.Confluence [lemma, in typ_annot]
PTS_ATR_mod.red1_next [constructor, in typ_annot]
PTS_ATR_mod.SR [lemma, in typ_annot]
_ ⊢ _ ≡'__ (Typ_scope) [notation, in typ_annot]
PTS_ATR_mod.wf_item_lift [lemma, in typ_annot]
PTS_ATR_mod.typ_var [constructor, in typ_annot]
_ ⊢ _ ▹ _ : _ (Typ_scope) [notation, in typ_annot]
PTS_ATR_mod.c_trans [constructor, in typ_annot]
PTS_ATR_mod.Sort_Reds [lemma, in typ_annot]
PTS_ATR_mod.peq_subst [lemma, in typ_annot]
PTS_ATR_mod.r_refl [constructor, in typ_annot]
PTS_ATR_mod.red_refl_lt [lemma, in typ_annot]
PTS_ATR_mod.conv_in_env [lemma, in typ_annot]
PTS_ATR_mod.typ_la [constructor, in typ_annot]
PTS_ATR_mod.La_Reds [lemma, in typ_annot]
PTS_ATR_mod.red_refl_rt [lemma, in typ_annot]
PTS_ATR_mod.Pi_Reds [lemma, in typ_annot]
PTS_ATR_mod.typ_reds_trans2 [lemma, in typ_annot]
PTS_ATR_mod.conv1_next [constructor, in typ_annot]
PTS_ATR_mod.typ_peq_trans [constructor, in typ_annot]
PTS_ATR_mod.typ_wf [lemma, in typ_annot]
PTS_ATR_mod.typ_peq_sym [lemma, in typ_annot]
PTS_ATR_mod.wf [inductive, in typ_annot]
R
red [library]red_mod.Beta_pi2 [constructor, in red]
red_mod.Betaps [inductive, in red]
red_mod.Beta [inductive, in red]
red_mod.Betap_App [constructor, in red]
red_mod.Betas_refl [constructor, in red]
red_mod.Betap_sort [constructor, in red]
red_mod.Betap_head [constructor, in red]
red_mod.Betaps_Beta_closure [lemma, in red]
red_mod.Betap_var [constructor, in red]
red_mod.Betap_refl [lemma, in red]
red_mod.Betap_lam [constructor, in red]
red_mod.Beta_red3 [constructor, in red]
red_mod.Beta_lam [constructor, in red]
red_mod.Betas_Pi [lemma, in red]
_ → _ (Typ_scope) [notation, in red]
_ →→ _ (Typ_scope) [notation, in red]
red_mod.Betaps_Betas_closure [lemma, in red]
red_mod.Betas_trans [constructor, in red]
red_mod.Beta_pi [constructor, in red]
red_mod [moduleid, in red]
red_mod.Beta_head [constructor, in red]
red_mod.Betaps_trans [constructor, in red]
red_mod.Beta_red1 [constructor, in red]
red_mod.Betas [inductive, in red]
_ →→'__ (Typ_scope) [notation, in red]
red_mod.Betas_Beta [constructor, in red]
red_mod.Betap [inductive, in red]
red_mod.Betap_pi [constructor, in red]
_ →'__ (Typ_scope) [notation, in red]
red_mod.Beta_red2 [constructor, in red]
red_mod.Beta_red4 [constructor, in red]
red_mod.Betap_to_Betas [lemma, in red]
red_mod.Betas_La [lemma, in red]
red_mod.Betaps_intro [constructor, in red]
red_mod.Betas_App [lemma, in red]
red_mod.Beta_lam2 [constructor, in red]
red_mod.Betaps_to_Betas [lemma, in red]
S
strip [library]strip_mod.strip_env [definition, in strip]
strip_mod.strip_subst [lemma, in strip]
strip_mod [moduleid, in strip]
strip_mod.strip_lift [lemma, in strip]
strip_mod.strip [definition, in strip]
T
term [library]term_mod.subst_travers [lemma, in term]
term_mod.La [constructor, in term]
Π ( _ ) , _ (Typ_scope) [notation, in term]
_ ↑ _ # _ (Typ_scope) [notation, in term]
term_mod.lift0 [lemma, in term]
term_mod.lift_rec [definition, in term]
_ ↑ _ (Typ_scope) [notation, in term]
term_mod.Term [inductive, in term]
term_mod.Pi [constructor, in term]
term_mod.App [constructor, in term]
term_mod.lift_lift [lemma, in term]
term_mod.Var [constructor, in term]
λ [ _ ] , _ (Typ_scope) [notation, in term]
term_mod.liftP2 [lemma, in term]
_ [ _ ← _ ] (Typ_scope) [notation, in term]
term_mod.substP2 [lemma, in term]
term_mod.subst_rec [definition, in term]
term_sig [moduleid, in base]
term_mod.liftP1 [lemma, in term]
term_mod.substP4 [lemma, in term]
term_mod.expand_term_with_subst [lemma, in term]
term_mod.lift_rec0 [lemma, in term]
! _ (Typ_scope) [notation, in term]
term_mod.substP1 [lemma, in term]
term_mod.inv_lift [lemma, in term]
term_mod.Sort [constructor, in term]
term_mod [moduleid, in term]
_ [ ← _ ] (Typ_scope) [notation, in term]
term_mod.liftP3 [lemma, in term]
term_sig.Sorts [axiom, in base]
term_mod.substP3 [lemma, in term]
_ ·( _ , _ ) _ (Typ_scope) [notation, in term]
# _ (Typ_scope) [notation, in term]
Theory [moduleid, in final_result]
Theory.PTS [moduleid, in final_result]
Theory.PTSATR [moduleid, in final_result]
Theory.PTSe [moduleid, in final_result]
typ_annot [library]
U
ut_red_mod.Betac_confl [lemma, in ut_red]ut_typ_eq_mod.thinning_eq_n [lemma, in ut_typ_eq]
ut_red_mod.Betac_trans [constructor, in ut_red]
ut_typ_mod.thinning_n [lemma, in ut_typ]
ut_typ_eq_inj_mod.gen_pi [lemma, in ut_typ_eq_inj]
ut_red_mod.Betap_pi [constructor, in ut_red]
ut_term_mod.lift_lift [lemma, in ut_term]
ut_env_mod.ins_O [constructor, in ut_env]
ut_red_mod.Beta_lam2 [constructor, in ut_red]
_ · _ (UT_scope) [notation, in ut_term]
ut_sr_mod.Betas_env_trans [constructor, in ut_sr]
ut_red_mod [moduleid, in ut_red]
ut_typ_mod.cApp [constructor, in ut_typ]
ut_strengh_mod.Sigma [inductive, in ut_strengh]
ut_red_mod.Betaps_Betas_closure [lemma, in ut_red]
ut_red_mod.Betaps_trans2 [lemma, in ut_red]
ut_term_mod [moduleid, in ut_term]
ut_term_mod.substP4 [lemma, in ut_term]
ut_red_mod.Betaps_trans [constructor, in ut_red]
# _ (UT_scope) [notation, in ut_term]
ut_typ_mod.typ [inductive, in ut_typ]
ut_typ_eq_mod.FromPTSe_to_PTS [lemma, in ut_typ_eq]
ut_typ_eq_mod.cTrans [constructor, in ut_typ_eq]
ut_typ_mod.sub_trunc [lemma, in ut_typ]
ut_term_mod.lift0 [lemma, in ut_term]
ut_sr_mod.Beta_env_sound_up [lemma, in ut_sr]
ut_strengh_mod.Ts_Sigma_Shape [lemma, in ut_strengh]
_ → _ (UT_scope) [notation, in ut_red]
ut_red_mod.Beta_red2 [constructor, in ut_red]
ut_red_mod.Betap_diamond [lemma, in ut_red]
ut_red_mod.Beta_red1 [constructor, in ut_red]
ut_typ_eq_inj_mod.gen_la [lemma, in ut_typ_eq_inj]
ut_strengh_mod.Tx_ok [lemma, in ut_strengh]
ut_red_mod.diamond_Betaps [lemma, in ut_red]
ut_red_mod.Beta_lam [constructor, in ut_red]
ut_red_mod.Betac_La [lemma, in ut_red]
ut_term_mod.expand_term_with_subst [lemma, in ut_term]
ut_env_mod.nth_sub_eq [lemma, in ut_env]
ut_strengh_mod.Tv_intro [constructor, in ut_strengh]
ut_typ_eq_mod.TypeCorrect_Refl [lemma, in ut_typ_eq]
ut_red_mod.Betap_app [constructor, in ut_red]
ut_red_mod.Betap [inductive, in ut_red]
ut_red_mod.Betas_Betaps_closure [lemma, in ut_red]
ut_red_mod.conv_var [lemma, in ut_red]
ut_typ_eq_inj_mod.wPiInj [lemma, in ut_typ_eq_inj]
ut_env_mod.ins_item_lift_lt [lemma, in ut_env]
ut_typ_mod.wf_nil [constructor, in ut_typ]
ut_typ_eq_mod.wf_typ [lemma, in ut_typ_eq]
ut_typ_mod.gen_la [lemma, in ut_typ]
ut_typ_eq_mod.cApp_eq [constructor, in ut_typ_eq]
ut_typ_eq_mod.wfe_nil [constructor, in ut_typ_eq]
ut_typ_eq_mod.thinning_n [lemma, in ut_typ_eq]
ut_typ_eq_mod.conv_in_env_var_lift3 [lemma, in ut_typ_eq]
ut_typ_eq_mod.conv_in_env_aux_trunc [lemma, in ut_typ_eq]
ut_strengh_mod.Ts_intro [constructor, in ut_strengh]
ut_sr_mod.Beta_sound [lemma, in ut_sr]
ut_strengh_mod.L2 [lemma, in ut_strengh]
ut_red_mod.Betap_Beta_closure [lemma, in ut_red]
ut_red_mod.Betap_head [constructor, in ut_red]
ut_strengh_mod.env_subst_down [definition, in ut_strengh]
ut_typ_eq_inj_mod.weak_to_PTS [lemma, in ut_typ_eq_inj]
ut_strengh_mod.Beta_lift_inv [lemma, in ut_strengh]
ut_strengh_mod.Tv_lift [lemma, in ut_strengh]
ut_typ_mod.Cnv [constructor, in ut_typ]
ut_strengh_mod.Tels'_subst [lemma, in ut_strengh]
ut_env_mod.nth_sub_sup [lemma, in ut_env]
ut_strengh_mod.ins_in_env_Sigma [lemma, in ut_strengh]
ut_strengh_mod.In_Sigma_tool [lemma, in ut_strengh]
ut_strengh_mod.fun_item_lift [lemma, in ut_strengh]
ut_env_mod.item_trunc [lemma, in ut_env]
ut_term_mod.La [constructor, in ut_term]
ut_typ_eq_mod.cRefl [constructor, in ut_typ_eq]
ut_strengh_mod.Sigma_la [constructor, in ut_strengh]
ut_typ_eq_mod.cSym [constructor, in ut_typ_eq]
ut_term_mod.subst_travers [lemma, in ut_term]
ut_strengh_mod.Shape_of_Ts_Term [lemma, in ut_strengh]
ut_sr_mod.Beta_env_cons [constructor, in ut_sr]
ut_sr_mod.Betas_env_sound_up [lemma, in ut_sr]
ut_strengh_mod.Ts_lift [lemma, in ut_strengh]
ut_typ_eq_mod.conv_in_env_var_lift [lemma, in ut_typ_eq]
ut_strengh_mod.WeakStrenghthening [lemma, in ut_strengh]
ut_red_mod.Betac_refl [lemma, in ut_red]
ut_red_mod.Betas_refl [constructor, in ut_red]
ut_strengh_mod.Shape_of_Type_Ts [lemma, in ut_strengh]
ut_term_mod.App [constructor, in ut_term]
ut_typ_eq_mod.wfe_cons [constructor, in ut_typ_eq]
_ ⊣e (UT_scope) [notation, in ut_typ_eq]
ut_typ_eq_mod.cPi_eq [constructor, in ut_typ_eq]
_ ≡ _ (UT_scope) [notation, in ut_red]
ut_strengh_mod [moduleid, in ut_strengh]
ut_typ_eq_mod.conv_in_env_var_lift2 [lemma, in ut_typ_eq]
ut_strengh_mod.Sigma_pi [constructor, in ut_strengh]
ut_env_mod.nth_sub_inf [lemma, in ut_env]
ut_term_mod.lift_rec [definition, in ut_term]
ut_typ_eq_mod.thinning [lemma, in ut_typ_eq]
ut_typ_eq_mod.Cnv_eq [constructor, in ut_typ_eq]
ut_sr_mod.Beta_env_sound [lemma, in ut_sr]
ut_sr_mod.Betas_env_nil [lemma, in ut_sr]
ut_red_mod.Betac_Pi [lemma, in ut_red]
ut_term_mod.Pi [constructor, in ut_term]
ut_sr_mod.Betas_env_cons [lemma, in ut_sr]
ut_typ_eq_inj_mod.wconv_in_env [lemma, in ut_typ_eq_inj]
ut_red_mod.Betas_S [lemma, in ut_red]
ut_typ_mod.gen_var [lemma, in ut_typ]
ut_strengh_mod.Betas_env_length [lemma, in ut_strengh]
_ →'__ (UT_scope) [notation, in ut_red]
ut_typ_eq_inj_mod.wtyp_eq_sym [lemma, in ut_typ_eq_inj]
ut_env_mod.trunc_O [constructor, in ut_env]
ut_typ_eq_inj_mod.Cnv_eq_wtyp_eq [lemma, in ut_typ_eq_inj]
ut_typ_eq_mod.substitution2 [lemma, in ut_typ_eq]
ut_typ_eq_mod.thinning_eq [lemma, in ut_typ_eq]
ut_sr_mod [moduleid, in ut_sr]
ut_sr_mod.Betas_env_nil2 [lemma, in ut_sr]
ut_strengh_mod.Tels' [definition, in ut_strengh]
ut_typ_mod.substitution [lemma, in ut_typ]
ut_red_mod.Betac [inductive, in ut_red]
ut_typ_eq_inj_mod.gen_app [lemma, in ut_typ_eq_inj]
ut_sr_mod.Subject_Reduction [lemma, in ut_sr]
ut_typ_eq_mod.cApp [constructor, in ut_typ_eq]
Π ( _ ) , _ (UT_scope) [notation, in ut_term]
ut_red_mod.sub_diamond_Betaps [lemma, in ut_red]
ut_typ_eq_inj_mod.wtyp_eq_intro2 [constructor, in ut_typ_eq_inj]
_ ⊢ _ : _ (UT_scope) [notation, in ut_typ]
ut_typ_eq_mod.conv_in_env_var3 [lemma, in ut_typ_eq]
ut_typ_eq_inj_mod.wtyp_eq_subst [lemma, in ut_typ_eq_inj]
ut_typ_eq_mod.cPi [constructor, in ut_typ_eq]
ut_typ_mod.cPi [constructor, in ut_typ]
ut_typ_eq_mod.wgen_pi [lemma, in ut_typ_eq]
ut_red_mod.Betac_lift [lemma, in ut_red]
ut_strengh_mod.env_subst_down_rev [lemma, in ut_strengh]
ut_typ_eq_inj_mod.weak_to_PTSe [lemma, in ut_typ_eq_inj]
ut_typ_eq_mod.conv_in_env_var [lemma, in ut_typ_eq]
ut_red_mod.Betac_App [lemma, in ut_red]
ut_typ_eq_mod.wf [inductive, in ut_typ_eq]
ut_env_mod.trunc [inductive, in ut_env]
ut_typ_eq_mod.conv_in_env [lemma, in ut_typ_eq]
_ →e _ (UT_scope) [notation, in ut_sr]
_ [[ _ ← _ ]] [notation, in ut_strengh]
ut_typ_eq_mod.cSort [constructor, in ut_typ_eq]
ut_red_mod.Betas_diamond [lemma, in ut_red]
ut_env_mod.gt_O [lemma, in ut_env]
ut_strengh_mod.Strenghthening [lemma, in ut_strengh]
ut_red_mod.Beta_lift [lemma, in ut_red]
ut_sr_mod.Betac_env_trans [constructor, in ut_sr]
ut_strengh_mod.env_subst_tool [lemma, in ut_strengh]
ut_strengh_mod.Betas_lift_inv [lemma, in ut_strengh]
ut_sr_mod.Betas_env_refl [constructor, in ut_sr]
ut_red_mod.Betap_lift [lemma, in ut_red]
ut_red_mod.Betas_Beta [constructor, in ut_red]
ut_typ_mod.wf_typ [lemma, in ut_typ]
ut_red_mod.Betas_Pi [lemma, in ut_red]
ut_red_mod.Betap_sort [constructor, in ut_red]
ut_strengh_mod.Tv_app [constructor, in ut_strengh]
ut_typ_mod.cLa [constructor, in ut_typ]
ut_red_mod.Betaps [inductive, in ut_red]
_ ≡e _ (UT_scope) [notation, in ut_sr]
ut_red_mod.Betaps_Beta_closure [lemma, in ut_red]
_ [ _ ← _ ] (UT_scope) [notation, in ut_term]
ut_sr_mod.Betac_env_Betas [constructor, in ut_sr]
ut_sr_mod.Betas_env_sound [lemma, in ut_sr]
ut_env_mod.item_tl [constructor, in ut_env]
ut_env_mod [moduleid, in ut_env]
ut_typ_eq_mod.wf_item [lemma, in ut_typ_eq]
ut_env_mod.nth_sub_item_inf [lemma, in ut_env]
ut_strengh_mod.Tv [inductive, in ut_strengh]
ut_term_mod.substP1 [lemma, in ut_term]
ut_red_mod.Beta_pi2 [constructor, in ut_red]
ut_sr_mod.Betas_env [inductive, in ut_sr]
ut_env_mod.ins_S [constructor, in ut_env]
_ ⊢e _ = _ : _ (UT_scope) [notation, in ut_typ_eq]
ut_typ_eq_mod.substitution [lemma, in ut_typ_eq]
ut_strengh_mod.Ts_app [constructor, in ut_strengh]
_ ⊢e _ : _ (UT_scope) [notation, in ut_typ_eq]
ut_strengh_mod.Betas_not_Pi_to_Sort [lemma, in ut_strengh]
ut_typ_mod.wf_item_lift [lemma, in ut_typ]
ut_red_mod.Betap_var [constructor, in ut_red]
ut_term_mod.substP2 [lemma, in ut_term]
ut_term_mod.liftP2 [lemma, in ut_term]
ut_env_mod.sub_O [constructor, in ut_env]
_ ⊢e _ = _ (UT_scope) [notation, in ut_typ_eq_inj]
ut_strengh_mod.Tv_la [constructor, in ut_strengh]
ut_strengh_mod.Sigma_app [constructor, in ut_strengh]
ut_strengh_mod.Ts [inductive, in ut_strengh]
ut_sr_mod.Betas_env_Beta [constructor, in ut_sr]
ut_strengh_mod.Tels [definition, in ut_strengh]
ut_typ_eq_mod.cBeta [constructor, in ut_typ_eq]
ut_sr_mod.Betac_env [inductive, in ut_sr]
ut_typ_mod.gen_app [lemma, in ut_typ]
ut_red_mod.conv_to_var [lemma, in ut_red]
ut_term_mod.Var [constructor, in ut_term]
ut_env_mod.Env [definition, in ut_env]
ut_env_mod.ins_item_ge [lemma, in ut_env]
ut_typ_eq_mod.typ [inductive, in ut_typ_eq]
ut_red_mod.Beta_pi [constructor, in ut_red]
ut_strengh_mod.Ts_pi [constructor, in ut_strengh]
ut_typ_eq_mod.Cnv [constructor, in ut_typ_eq]
ut_red_mod.Betas_Betap_closure [lemma, in ut_red]
ut_red_mod.Betap_lam [constructor, in ut_red]
_ →'__ (UT_scope) [notation, in ut_red]
ut_env_mod.trunc_S [constructor, in ut_env]
_ ⊣ (UT_scope) [notation, in ut_typ]
ut_sr_mod.Beta_env [inductive, in ut_sr]
ut_typ_mod [moduleid, in ut_typ]
ut_strengh_mod.Shape_of_Type_Tv [lemma, in ut_strengh]
ut_sr_mod.SubjectRed [lemma, in ut_sr]
ut_typ_eq_mod [moduleid, in ut_typ_eq]
_ →→e _ (UT_scope) [notation, in ut_sr]
ut_red_mod.Betas_Pi_inv [lemma, in ut_red]
ut_red_mod.PiInj [lemma, in ut_red]
ut_red_mod.Betas_lift [lemma, in ut_red]
ut_strengh_mod.ins_in_env_wf [lemma, in ut_strengh]
ut_strengh_mod.Betas_Tels_inv [lemma, in ut_strengh]
ut_typ_eq_inj_mod.wtyp_eq_intro [constructor, in ut_typ_eq_inj]
ut_strengh_mod.sub_in_env_rev_append [lemma, in ut_strengh]
ut_strengh_mod.Tels_subst [lemma, in ut_strengh]
ut_term_mod.inv_lift [lemma, in ut_term]
ut_typ_mod.TypeCorrect [lemma, in ut_typ]
_ →→ _ (UT_scope) [notation, in ut_red]
ut_red_mod.Betac_sym [constructor, in ut_red]
ut_typ_eq_mod.conv_in_env_var2 [lemma, in ut_typ_eq]
ut_typ_eq_inj_mod.wtyp_eq [inductive, in ut_typ_eq_inj]
ut_typ_eq_inj_mod.Cnv_wtyp_eq [lemma, in ut_typ_eq_inj]
ut_typ_eq_mod.wf_item_lift [lemma, in ut_typ_eq]
ut_strengh_mod.Tels_tool [lemma, in ut_strengh]
ut_red_mod.Betap_refl [lemma, in ut_red]
ut_red_mod.Beta_head [constructor, in ut_red]
ut_env_mod.ins_in_env [inductive, in ut_env]
ut_strengh_mod.env_subst [definition, in ut_strengh]
ut_red_mod.Betas_La [lemma, in ut_red]
ut_typ_eq_mod.cLa_eq [constructor, in ut_typ_eq]
ut_env_mod.fun_item [lemma, in ut_env]
ut_red_mod.Betas_App [lemma, in ut_red]
ut_typ_eq_inj_mod.SRe [lemma, in ut_typ_eq_inj]
ut_env_mod.item_lift [definition, in ut_env]
_ ↓ _ ∈ _ (UT_scope) [notation, in ut_env]
ut_red_mod.conv_to_sort [lemma, in ut_red]
ut_red_mod.Betas_subst [lemma, in ut_red]
ut_typ_mod.wf [inductive, in ut_typ]
_ ↓ _ ⊂ _ (UT_scope) [notation, in ut_env]
ut_typ_eq_mod.wf_typ_eq [lemma, in ut_typ_eq]
ut_red_mod.Betac_Betas [constructor, in ut_red]
ut_strengh_mod.Betas_Tels [lemma, in ut_strengh]
ut_typ_eq_mod.typ_eq [inductive, in ut_typ_eq]
ut_sr_mod.Betas_env_comp [lemma, in ut_sr]
ut_term_mod.Sort [constructor, in ut_term]
_ ↑ _ (UT_scope) [notation, in ut_term]
ut_typ_eq_mod.cLa [constructor, in ut_typ_eq]
ut_typ_eq_mod.TypeCorrect_eq [lemma, in ut_typ_eq]
ut_typ_eq_inj_mod.wtyp_eq_trans [constructor, in ut_typ_eq_inj]
ut_sr_mod.Betas_env_hd [lemma, in ut_sr]
ut_typ_mod.gen_sort [lemma, in ut_typ]
ut_term_mod.liftP3 [lemma, in ut_term]
ut_term_mod.Term [inductive, in ut_term]
ut_env_mod.sub_in_env [inductive, in ut_env]
ut_typ_eq_mod.weakening [lemma, in ut_typ_eq]
ut_sr_mod.Betac_env_sym [constructor, in ut_sr]
λ [ _ ] , _ (UT_scope) [notation, in ut_term]
! _ (UT_scope) [notation, in ut_term]
ut_typ_eq_mod.TypeCorrect [lemma, in ut_typ_eq]
ut_strengh_mod.In_Sigma [lemma, in ut_strengh]
ut_sr_mod.Betas_env_sound2 [lemma, in ut_sr]
ut_red_mod.Betap_subst [lemma, in ut_red]
ut_sr_mod.Betas_typ_sound [lemma, in ut_sr]
ut_red_mod.Betas [inductive, in ut_red]
ut_red_mod.Beta_beta [lemma, in ut_red]
ut_typ_eq_inj_mod [moduleid, in ut_typ_eq_inj]
ut_env_mod.ins_item_lt [lemma, in ut_env]
ut_sr_mod.Betas_env_inv [lemma, in ut_sr]
ut_term_mod.lift_rec0 [lemma, in ut_term]
ut_sr_mod.Beta_env_hd [constructor, in ut_sr]
ut_typ_mod.thinning [lemma, in ut_typ]
ut_term_mod.substP3 [lemma, in ut_term]
ut_red_mod.Betac_not_Pi_sort [lemma, in ut_red]
ut_typ_eq_mod.cVar [constructor, in ut_typ_eq]
ut_strengh_mod.env_subst_down_sub_in_env [lemma, in ut_strengh]
ut_typ_mod.wf_item [lemma, in ut_typ]
ut_strengh_mod.L1 [lemma, in ut_strengh]
ut_env_mod.item [inductive, in ut_env]
ut_typ_eq_mod.right_reflexivity [lemma, in ut_typ_eq]
ut_red_mod.Betac_subst [lemma, in ut_red]
ut_strengh_mod.Beta_Tels_inv [lemma, in ut_strengh]
ut_red_mod.Betaps_refl [constructor, in ut_red]
ut_typ_mod.wf_cons [constructor, in ut_typ]
ut_typ_mod.weakening [lemma, in ut_typ]
ut_sr_mod.Beta_env_sound2 [lemma, in ut_sr]
ut_red_mod.Beta [inductive, in ut_red]
_ [ ← _ ] (UT_scope) [notation, in ut_term]
ut_strengh_mod.env_subst_down_app [lemma, in ut_strengh]
ut_typ_mod.gen_pi [lemma, in ut_typ]
ut_red_mod.Betas_V [lemma, in ut_red]
ut_strengh_mod.Sigma_sorts [constructor, in ut_strengh]
_ →→'__ (UT_scope) [notation, in ut_red]
ut_red_mod.Betas_subst2 [lemma, in ut_red]
ut_env_mod.sub_S [constructor, in ut_env]
ut_typ_mod.cVar [constructor, in ut_typ]
ut_env_mod.item_hd [constructor, in ut_env]
ut_typ_mod.cSort [constructor, in ut_typ]
ut_red_mod.Betac_subst2 [lemma, in ut_red]
ut_term_mod.liftP1 [lemma, in ut_term]
_ ↑ _ # _ (UT_scope) [notation, in ut_term]
ut_term_mod.subst_rec [definition, in ut_term]
ut_typ_eq_mod.left_reflexivity [lemma, in ut_typ_eq]
ut_red_mod.Betas_trans [constructor, in ut_red]
ut_red_mod.conv_sort [lemma, in ut_red]
ut_strengh_mod.Ts_la [constructor, in ut_strengh]
ut_sr [library]
ut_typ_eq_inj [library]
ut_strengh [library]
ut_red [library]
ut_typ [library]
ut_term [library]
ut_env [library]
ut_typ_eq [library]
V
Vars [definition, in base]Lemma Index
C
CE.Dom_ce [in counter_ex]CE.D1_ok [in counter_ex]
CE.D1_typ [in counter_ex]
CE.D2_typ [in counter_ex]
CE.D2_ok [in counter_ex]
CE.PTSe_dont_have_PiInj [in counter_ex]
CE.ze_pi_eq [in counter_ex]
E
env_mod.nth_sub_inf [in env]env_mod.fun_item [in env]
env_mod.nth_sub_sup [in env]
env_mod.item_trunc [in env]
env_mod.ins_item_ge [in env]
env_mod.ins_item_lt [in env]
env_mod.ins_item_lift_lt [in env]
env_mod.nth_sub_item_inf [in env]
env_mod.nth_sub_eq [in env]
env_mod.gt_O [in env]
F
final_mod.strip_var [in final_result]final_mod.PTSe_SR [in final_result]
final_mod.FromPTSATR_to_PTS [in final_result]
final_mod.strip_var_ [in final_result]
final_mod.FromPTSATR_to_PTSe_trans [in final_result]
final_mod.FromPTSATR_to_PTSe [in final_result]
final_mod.PTSe_SR_trans [in final_result]
final_mod.PTS_equiv_PTSe [in final_result]
final_mod.FromPTS_to_PTSATR [in final_result]
G
glue_mod.weak_type_shape [in glue]glue_mod.ErasedTermConfluence [in glue]
glue_mod.ErasedContextSwitch [in glue]
glue_mod.L33' [in glue]
glue_mod.peq_not_Pi_sort [in glue]
glue_mod.L43_ [in glue]
glue_mod.ErasedTypeConversion [in glue]
glue_mod.L33 [in glue]
P
PTS_ATR_mod.reds_Pi_ [in typ_annot]PTS_ATR_mod.env_conv_wf [in typ_annot]
PTS_ATR_mod.reds_App___ [in typ_annot]
PTS_ATR_mod.typ_pcompat [in typ_annot]
PTS_ATR_mod.red_in_env_reds [in typ_annot]
PTS_ATR_mod.typ_red_trans [in typ_annot]
PTS_ATR_mod.conv_in_env_peq [in typ_annot]
PTS_ATR_mod.reds_La [in typ_annot]
PTS_ATR_mod.reds_subst_gen [in typ_annot]
PTS_ATR_mod.sub_in_env_item [in typ_annot]
PTS_ATR_mod.red_item [in typ_annot]
PTS_ATR_mod.eq_subst_gen [in typ_annot]
PTS_ATR_mod.typ_exp_trans [in typ_annot]
PTS_ATR_mod.SR_trans [in typ_annot]
PTS_ATR_mod.relocate [in typ_annot]
PTS_ATR_mod.thinning_reds_n [in typ_annot]
PTS_ATR_mod.pgen_pi [in typ_annot]
PTS_ATR_mod.reds_App_ [in typ_annot]
PTS_ATR_mod.conv_in_env_reds [in typ_annot]
PTS_ATR_mod.wf_item [in typ_annot]
PTS_ATR_mod.env_red_wf [in typ_annot]
PTS_ATR_mod.reds_subst [in typ_annot]
PTS_ATR_mod.c_sym [in typ_annot]
PTS_ATR_mod.env_conv1_wf [in typ_annot]
PTS_ATR_mod.peq_thinning [in typ_annot]
PTS_ATR_mod.pgen_app [in typ_annot]
PTS_ATR_mod.env_red_to_conv [in typ_annot]
PTS_ATR_mod.typ_reds_trans_ [in typ_annot]
PTS_ATR_mod.thinning_reds [in typ_annot]
PTS_ATR_mod.ChurchRosser [in typ_annot]
PTS_ATR_mod.fun_item_lift [in typ_annot]
PTS_ATR_mod.red_in_env [in typ_annot]
PTS_ATR_mod.typ_ind2 [in typ_annot]
PTS_ATR_mod.reds_App__ [in typ_annot]
PTS_ATR_mod.typ_reds_relocate [in typ_annot]
PTS_ATR_mod.c1_sym [in typ_annot]
PTS_ATR_mod.conv1_in_env [in typ_annot]
PTS_ATR_mod.reds_Pi [in typ_annot]
PTS_ATR_mod.OSDiamond [in typ_annot]
PTS_ATR_mod.env_red_cons [in typ_annot]
PTS_ATR_mod.SR_trans' [in typ_annot]
PTS_ATR_mod.wf_from_peq [in typ_annot]
PTS_ATR_mod.wf_from_typ [in typ_annot]
PTS_ATR_mod.sub_trunc [in typ_annot]
PTS_ATR_mod.subst_gen [in typ_annot]
PTS_ATR_mod.env_conv_cons [in typ_annot]
PTS_ATR_mod.env_red1_to_conv1 [in typ_annot]
PTS_ATR_mod.ConvSort [in typ_annot]
PTS_ATR_mod.weakening [in typ_annot]
PTS_ATR_mod.pgen_la [in typ_annot]
PTS_ATR_mod.PiInj [in typ_annot]
PTS_ATR_mod.reds_to_conv [in typ_annot]
PTS_ATR_mod.peq_thinning_n [in typ_annot]
PTS_ATR_mod.thinning [in typ_annot]
PTS_ATR_mod.red1_in_env [in typ_annot]
PTS_ATR_mod.SubDiam [in typ_annot]
PTS_ATR_mod.typ_peq_to_red [in typ_annot]
PTS_ATR_mod.thinning_n [in typ_annot]
PTS_ATR_mod.reds_refl_lt [in typ_annot]
PTS_ATR_mod.pgen_var [in typ_annot]
PTS_ATR_mod.env_red1_wf [in typ_annot]
PTS_ATR_mod.reds_App [in typ_annot]
PTS_ATR_mod.reds_typ_pcompat [in typ_annot]
PTS_ATR_mod.conv_item [in typ_annot]
PTS_ATR_mod.reds_refl_rt [in typ_annot]
PTS_ATR_mod.pgen_sort [in typ_annot]
PTS_ATR_mod.typ_reds_to_red_ [in typ_annot]
PTS_ATR_mod.wf_from_typ_reds [in typ_annot]
PTS_ATR_mod.Confluence [in typ_annot]
PTS_ATR_mod.SR [in typ_annot]
PTS_ATR_mod.wf_item_lift [in typ_annot]
PTS_ATR_mod.Sort_Reds [in typ_annot]
PTS_ATR_mod.peq_subst [in typ_annot]
PTS_ATR_mod.red_refl_lt [in typ_annot]
PTS_ATR_mod.conv_in_env [in typ_annot]
PTS_ATR_mod.La_Reds [in typ_annot]
PTS_ATR_mod.red_refl_rt [in typ_annot]
PTS_ATR_mod.Pi_Reds [in typ_annot]
PTS_ATR_mod.typ_reds_trans2 [in typ_annot]
PTS_ATR_mod.typ_wf [in typ_annot]
PTS_ATR_mod.typ_peq_sym [in typ_annot]
R
red_mod.Betaps_Beta_closure [in red]red_mod.Betap_refl [in red]
red_mod.Betas_Pi [in red]
red_mod.Betaps_Betas_closure [in red]
red_mod.Betap_to_Betas [in red]
red_mod.Betas_La [in red]
red_mod.Betas_App [in red]
red_mod.Betaps_to_Betas [in red]
S
strip_mod.strip_subst [in strip]strip_mod.strip_lift [in strip]
T
term_mod.subst_travers [in term]term_mod.lift0 [in term]
term_mod.lift_lift [in term]
term_mod.liftP2 [in term]
term_mod.substP2 [in term]
term_mod.liftP1 [in term]
term_mod.substP4 [in term]
term_mod.expand_term_with_subst [in term]
term_mod.lift_rec0 [in term]
term_mod.substP1 [in term]
term_mod.inv_lift [in term]
term_mod.liftP3 [in term]
term_mod.substP3 [in term]
U
ut_red_mod.Betac_confl [in ut_red]ut_typ_eq_mod.thinning_eq_n [in ut_typ_eq]
ut_typ_mod.thinning_n [in ut_typ]
ut_typ_eq_inj_mod.gen_pi [in ut_typ_eq_inj]
ut_term_mod.lift_lift [in ut_term]
ut_red_mod.Betaps_Betas_closure [in ut_red]
ut_red_mod.Betaps_trans2 [in ut_red]
ut_term_mod.substP4 [in ut_term]
ut_typ_eq_mod.FromPTSe_to_PTS [in ut_typ_eq]
ut_typ_mod.sub_trunc [in ut_typ]
ut_term_mod.lift0 [in ut_term]
ut_sr_mod.Beta_env_sound_up [in ut_sr]
ut_strengh_mod.Ts_Sigma_Shape [in ut_strengh]
ut_red_mod.Betap_diamond [in ut_red]
ut_typ_eq_inj_mod.gen_la [in ut_typ_eq_inj]
ut_strengh_mod.Tx_ok [in ut_strengh]
ut_red_mod.diamond_Betaps [in ut_red]
ut_red_mod.Betac_La [in ut_red]
ut_term_mod.expand_term_with_subst [in ut_term]
ut_env_mod.nth_sub_eq [in ut_env]
ut_typ_eq_mod.TypeCorrect_Refl [in ut_typ_eq]
ut_red_mod.Betas_Betaps_closure [in ut_red]
ut_red_mod.conv_var [in ut_red]
ut_typ_eq_inj_mod.wPiInj [in ut_typ_eq_inj]
ut_env_mod.ins_item_lift_lt [in ut_env]
ut_typ_eq_mod.wf_typ [in ut_typ_eq]
ut_typ_mod.gen_la [in ut_typ]
ut_typ_eq_mod.thinning_n [in ut_typ_eq]
ut_typ_eq_mod.conv_in_env_var_lift3 [in ut_typ_eq]
ut_typ_eq_mod.conv_in_env_aux_trunc [in ut_typ_eq]
ut_sr_mod.Beta_sound [in ut_sr]
ut_strengh_mod.L2 [in ut_strengh]
ut_red_mod.Betap_Beta_closure [in ut_red]
ut_typ_eq_inj_mod.weak_to_PTS [in ut_typ_eq_inj]
ut_strengh_mod.Beta_lift_inv [in ut_strengh]
ut_strengh_mod.Tv_lift [in ut_strengh]
ut_strengh_mod.Tels'_subst [in ut_strengh]
ut_env_mod.nth_sub_sup [in ut_env]
ut_strengh_mod.ins_in_env_Sigma [in ut_strengh]
ut_strengh_mod.In_Sigma_tool [in ut_strengh]
ut_strengh_mod.fun_item_lift [in ut_strengh]
ut_env_mod.item_trunc [in ut_env]
ut_term_mod.subst_travers [in ut_term]
ut_strengh_mod.Shape_of_Ts_Term [in ut_strengh]
ut_sr_mod.Betas_env_sound_up [in ut_sr]
ut_strengh_mod.Ts_lift [in ut_strengh]
ut_typ_eq_mod.conv_in_env_var_lift [in ut_typ_eq]
ut_strengh_mod.WeakStrenghthening [in ut_strengh]
ut_red_mod.Betac_refl [in ut_red]
ut_strengh_mod.Shape_of_Type_Ts [in ut_strengh]
ut_typ_eq_mod.conv_in_env_var_lift2 [in ut_typ_eq]
ut_env_mod.nth_sub_inf [in ut_env]
ut_typ_eq_mod.thinning [in ut_typ_eq]
ut_sr_mod.Beta_env_sound [in ut_sr]
ut_sr_mod.Betas_env_nil [in ut_sr]
ut_red_mod.Betac_Pi [in ut_red]
ut_sr_mod.Betas_env_cons [in ut_sr]
ut_typ_eq_inj_mod.wconv_in_env [in ut_typ_eq_inj]
ut_red_mod.Betas_S [in ut_red]
ut_typ_mod.gen_var [in ut_typ]
ut_strengh_mod.Betas_env_length [in ut_strengh]
ut_typ_eq_inj_mod.wtyp_eq_sym [in ut_typ_eq_inj]
ut_typ_eq_inj_mod.Cnv_eq_wtyp_eq [in ut_typ_eq_inj]
ut_typ_eq_mod.substitution2 [in ut_typ_eq]
ut_typ_eq_mod.thinning_eq [in ut_typ_eq]
ut_sr_mod.Betas_env_nil2 [in ut_sr]
ut_typ_mod.substitution [in ut_typ]
ut_typ_eq_inj_mod.gen_app [in ut_typ_eq_inj]
ut_sr_mod.Subject_Reduction [in ut_sr]
ut_red_mod.sub_diamond_Betaps [in ut_red]
ut_typ_eq_mod.conv_in_env_var3 [in ut_typ_eq]
ut_typ_eq_inj_mod.wtyp_eq_subst [in ut_typ_eq_inj]
ut_typ_eq_mod.wgen_pi [in ut_typ_eq]
ut_red_mod.Betac_lift [in ut_red]
ut_strengh_mod.env_subst_down_rev [in ut_strengh]
ut_typ_eq_inj_mod.weak_to_PTSe [in ut_typ_eq_inj]
ut_typ_eq_mod.conv_in_env_var [in ut_typ_eq]
ut_red_mod.Betac_App [in ut_red]
ut_typ_eq_mod.conv_in_env [in ut_typ_eq]
ut_red_mod.Betas_diamond [in ut_red]
ut_env_mod.gt_O [in ut_env]
ut_strengh_mod.Strenghthening [in ut_strengh]
ut_red_mod.Beta_lift [in ut_red]
ut_strengh_mod.env_subst_tool [in ut_strengh]
ut_strengh_mod.Betas_lift_inv [in ut_strengh]
ut_red_mod.Betap_lift [in ut_red]
ut_typ_mod.wf_typ [in ut_typ]
ut_red_mod.Betas_Pi [in ut_red]
ut_red_mod.Betaps_Beta_closure [in ut_red]
ut_sr_mod.Betas_env_sound [in ut_sr]
ut_typ_eq_mod.wf_item [in ut_typ_eq]
ut_env_mod.nth_sub_item_inf [in ut_env]
ut_term_mod.substP1 [in ut_term]
ut_typ_eq_mod.substitution [in ut_typ_eq]
ut_strengh_mod.Betas_not_Pi_to_Sort [in ut_strengh]
ut_typ_mod.wf_item_lift [in ut_typ]
ut_term_mod.substP2 [in ut_term]
ut_term_mod.liftP2 [in ut_term]
ut_typ_mod.gen_app [in ut_typ]
ut_red_mod.conv_to_var [in ut_red]
ut_env_mod.ins_item_ge [in ut_env]
ut_red_mod.Betas_Betap_closure [in ut_red]
ut_strengh_mod.Shape_of_Type_Tv [in ut_strengh]
ut_sr_mod.SubjectRed [in ut_sr]
ut_red_mod.Betas_Pi_inv [in ut_red]
ut_red_mod.PiInj [in ut_red]
ut_red_mod.Betas_lift [in ut_red]
ut_strengh_mod.ins_in_env_wf [in ut_strengh]
ut_strengh_mod.Betas_Tels_inv [in ut_strengh]
ut_strengh_mod.sub_in_env_rev_append [in ut_strengh]
ut_strengh_mod.Tels_subst [in ut_strengh]
ut_term_mod.inv_lift [in ut_term]
ut_typ_mod.TypeCorrect [in ut_typ]
ut_typ_eq_mod.conv_in_env_var2 [in ut_typ_eq]
ut_typ_eq_inj_mod.Cnv_wtyp_eq [in ut_typ_eq_inj]
ut_typ_eq_mod.wf_item_lift [in ut_typ_eq]
ut_strengh_mod.Tels_tool [in ut_strengh]
ut_red_mod.Betap_refl [in ut_red]
ut_red_mod.Betas_La [in ut_red]
ut_env_mod.fun_item [in ut_env]
ut_red_mod.Betas_App [in ut_red]
ut_typ_eq_inj_mod.SRe [in ut_typ_eq_inj]
ut_red_mod.conv_to_sort [in ut_red]
ut_red_mod.Betas_subst [in ut_red]
ut_typ_eq_mod.wf_typ_eq [in ut_typ_eq]
ut_strengh_mod.Betas_Tels [in ut_strengh]
ut_sr_mod.Betas_env_comp [in ut_sr]
ut_typ_eq_mod.TypeCorrect_eq [in ut_typ_eq]
ut_sr_mod.Betas_env_hd [in ut_sr]
ut_typ_mod.gen_sort [in ut_typ]
ut_term_mod.liftP3 [in ut_term]
ut_typ_eq_mod.weakening [in ut_typ_eq]
ut_typ_eq_mod.TypeCorrect [in ut_typ_eq]
ut_strengh_mod.In_Sigma [in ut_strengh]
ut_sr_mod.Betas_env_sound2 [in ut_sr]
ut_red_mod.Betap_subst [in ut_red]
ut_sr_mod.Betas_typ_sound [in ut_sr]
ut_red_mod.Beta_beta [in ut_red]
ut_env_mod.ins_item_lt [in ut_env]
ut_sr_mod.Betas_env_inv [in ut_sr]
ut_term_mod.lift_rec0 [in ut_term]
ut_typ_mod.thinning [in ut_typ]
ut_term_mod.substP3 [in ut_term]
ut_red_mod.Betac_not_Pi_sort [in ut_red]
ut_strengh_mod.env_subst_down_sub_in_env [in ut_strengh]
ut_typ_mod.wf_item [in ut_typ]
ut_strengh_mod.L1 [in ut_strengh]
ut_typ_eq_mod.right_reflexivity [in ut_typ_eq]
ut_red_mod.Betac_subst [in ut_red]
ut_strengh_mod.Beta_Tels_inv [in ut_strengh]
ut_typ_mod.weakening [in ut_typ]
ut_sr_mod.Beta_env_sound2 [in ut_sr]
ut_strengh_mod.env_subst_down_app [in ut_strengh]
ut_typ_mod.gen_pi [in ut_typ]
ut_red_mod.Betas_V [in ut_red]
ut_red_mod.Betas_subst2 [in ut_red]
ut_red_mod.Betac_subst2 [in ut_red]
ut_term_mod.liftP1 [in ut_term]
ut_typ_eq_mod.left_reflexivity [in ut_typ_eq]
ut_red_mod.conv_sort [in ut_red]
Constructor Index
E
env_mod.trunc_S [in env]env_mod.ins_S [in env]
env_mod.trunc_O [in env]
env_mod.sub_O [in env]
env_mod.item_hd [in env]
env_mod.sub_S [in env]
env_mod.item_tl [in env]
env_mod.ins_O [in env]
M
Mpts.Ax0 [in counter_ex]Mpts.Ax1 [in counter_ex]
Mpts.Ax2 [in counter_ex]
Mpts.Ax3 [in counter_ex]
Mpts.Rel0 [in counter_ex]
Mpts.Rel1 [in counter_ex]
Mpts.Rel2 [in counter_ex]
Mpts.Rel3 [in counter_ex]
Msorts.U [in counter_ex]
Msorts.V [in counter_ex]
Msorts.V' [in counter_ex]
Msorts.W [in counter_ex]
Msorts.W' [in counter_ex]
P
PTS_ATR_mod.typ_exp [in typ_annot]PTS_ATR_mod.typ_reds_intro [in typ_annot]
PTS_ATR_mod.typ_pi [in typ_annot]
PTS_ATR_mod.typ_beta [in typ_annot]
PTS_ATR_mod.r_trans [in typ_annot]
PTS_ATR_mod.typ_red [in typ_annot]
PTS_ATR_mod.typ_peq_intro2 [in typ_annot]
PTS_ATR_mod.r_step [in typ_annot]
PTS_ATR_mod.typ_app [in typ_annot]
PTS_ATR_mod.c_step [in typ_annot]
PTS_ATR_mod.typ_sort [in typ_annot]
PTS_ATR_mod.typ_reds_trans [in typ_annot]
PTS_ATR_mod.c_refl [in typ_annot]
PTS_ATR_mod.red1_intro [in typ_annot]
PTS_ATR_mod.wf_nil [in typ_annot]
PTS_ATR_mod.conv1_intro [in typ_annot]
PTS_ATR_mod.wf_cons [in typ_annot]
PTS_ATR_mod.typ_peq_intro [in typ_annot]
PTS_ATR_mod.red1_next [in typ_annot]
PTS_ATR_mod.typ_var [in typ_annot]
PTS_ATR_mod.c_trans [in typ_annot]
PTS_ATR_mod.r_refl [in typ_annot]
PTS_ATR_mod.typ_la [in typ_annot]
PTS_ATR_mod.conv1_next [in typ_annot]
PTS_ATR_mod.typ_peq_trans [in typ_annot]
R
red_mod.Beta_pi2 [in red]red_mod.Betap_App [in red]
red_mod.Betas_refl [in red]
red_mod.Betap_sort [in red]
red_mod.Betap_head [in red]
red_mod.Betap_var [in red]
red_mod.Betap_lam [in red]
red_mod.Beta_red3 [in red]
red_mod.Beta_lam [in red]
red_mod.Betas_trans [in red]
red_mod.Beta_pi [in red]
red_mod.Beta_head [in red]
red_mod.Betaps_trans [in red]
red_mod.Beta_red1 [in red]
red_mod.Betas_Beta [in red]
red_mod.Betap_pi [in red]
red_mod.Beta_red2 [in red]
red_mod.Beta_red4 [in red]
red_mod.Betaps_intro [in red]
red_mod.Beta_lam2 [in red]
T
term_mod.La [in term]term_mod.Pi [in term]
term_mod.App [in term]
term_mod.Var [in term]
term_mod.Sort [in term]
U
ut_red_mod.Betac_trans [in ut_red]ut_red_mod.Betap_pi [in ut_red]
ut_env_mod.ins_O [in ut_env]
ut_red_mod.Beta_lam2 [in ut_red]
ut_sr_mod.Betas_env_trans [in ut_sr]
ut_typ_mod.cApp [in ut_typ]
ut_red_mod.Betaps_trans [in ut_red]
ut_typ_eq_mod.cTrans [in ut_typ_eq]
ut_red_mod.Beta_red2 [in ut_red]
ut_red_mod.Beta_red1 [in ut_red]
ut_red_mod.Beta_lam [in ut_red]
ut_strengh_mod.Tv_intro [in ut_strengh]
ut_red_mod.Betap_app [in ut_red]
ut_typ_mod.wf_nil [in ut_typ]
ut_typ_eq_mod.cApp_eq [in ut_typ_eq]
ut_typ_eq_mod.wfe_nil [in ut_typ_eq]
ut_strengh_mod.Ts_intro [in ut_strengh]
ut_red_mod.Betap_head [in ut_red]
ut_typ_mod.Cnv [in ut_typ]
ut_term_mod.La [in ut_term]
ut_typ_eq_mod.cRefl [in ut_typ_eq]
ut_strengh_mod.Sigma_la [in ut_strengh]
ut_typ_eq_mod.cSym [in ut_typ_eq]
ut_sr_mod.Beta_env_cons [in ut_sr]
ut_red_mod.Betas_refl [in ut_red]
ut_term_mod.App [in ut_term]
ut_typ_eq_mod.wfe_cons [in ut_typ_eq]
ut_typ_eq_mod.cPi_eq [in ut_typ_eq]
ut_strengh_mod.Sigma_pi [in ut_strengh]
ut_typ_eq_mod.Cnv_eq [in ut_typ_eq]
ut_term_mod.Pi [in ut_term]
ut_env_mod.trunc_O [in ut_env]
ut_typ_eq_mod.cApp [in ut_typ_eq]
ut_typ_eq_inj_mod.wtyp_eq_intro2 [in ut_typ_eq_inj]
ut_typ_eq_mod.cPi [in ut_typ_eq]
ut_typ_mod.cPi [in ut_typ]
ut_typ_eq_mod.cSort [in ut_typ_eq]
ut_sr_mod.Betac_env_trans [in ut_sr]
ut_sr_mod.Betas_env_refl [in ut_sr]
ut_red_mod.Betas_Beta [in ut_red]
ut_red_mod.Betap_sort [in ut_red]
ut_strengh_mod.Tv_app [in ut_strengh]
ut_typ_mod.cLa [in ut_typ]
ut_sr_mod.Betac_env_Betas [in ut_sr]
ut_env_mod.item_tl [in ut_env]
ut_red_mod.Beta_pi2 [in ut_red]
ut_env_mod.ins_S [in ut_env]
ut_strengh_mod.Ts_app [in ut_strengh]
ut_red_mod.Betap_var [in ut_red]
ut_env_mod.sub_O [in ut_env]
ut_strengh_mod.Tv_la [in ut_strengh]
ut_strengh_mod.Sigma_app [in ut_strengh]
ut_sr_mod.Betas_env_Beta [in ut_sr]
ut_typ_eq_mod.cBeta [in ut_typ_eq]
ut_term_mod.Var [in ut_term]
ut_red_mod.Beta_pi [in ut_red]
ut_strengh_mod.Ts_pi [in ut_strengh]
ut_typ_eq_mod.Cnv [in ut_typ_eq]
ut_red_mod.Betap_lam [in ut_red]
ut_env_mod.trunc_S [in ut_env]
ut_typ_eq_inj_mod.wtyp_eq_intro [in ut_typ_eq_inj]
ut_red_mod.Betac_sym [in ut_red]
ut_red_mod.Beta_head [in ut_red]
ut_typ_eq_mod.cLa_eq [in ut_typ_eq]
ut_red_mod.Betac_Betas [in ut_red]
ut_term_mod.Sort [in ut_term]
ut_typ_eq_mod.cLa [in ut_typ_eq]
ut_typ_eq_inj_mod.wtyp_eq_trans [in ut_typ_eq_inj]
ut_sr_mod.Betac_env_sym [in ut_sr]
ut_sr_mod.Beta_env_hd [in ut_sr]
ut_typ_eq_mod.cVar [in ut_typ_eq]
ut_red_mod.Betaps_refl [in ut_red]
ut_typ_mod.wf_cons [in ut_typ]
ut_strengh_mod.Sigma_sorts [in ut_strengh]
ut_env_mod.sub_S [in ut_env]
ut_typ_mod.cVar [in ut_typ]
ut_env_mod.item_hd [in ut_env]
ut_typ_mod.cSort [in ut_typ]
ut_red_mod.Betas_trans [in ut_red]
ut_strengh_mod.Ts_la [in ut_strengh]
Notation Index
E
_ ↓ _ ⊂ _ (Typ_scope) [in env]_ ↓ _ ∈ _ (Typ_scope) [in env]
P
_ ⊣ (Typ_scope) [in typ_annot]_ ⊢ _ ▹▹ _ : _ (Typ_scope) [in typ_annot]
_ ⊢ _ ≡'__ (Typ_scope) [in typ_annot]
_ ⊢ _ ▹ _ : _ (Typ_scope) [in typ_annot]
R
_ → _ (Typ_scope) [in red]_ →→ _ (Typ_scope) [in red]
_ →→'__ (Typ_scope) [in red]
_ →'__ (Typ_scope) [in red]
T
Π ( _ ) , _ (Typ_scope) [in term]_ ↑ _ # _ (Typ_scope) [in term]
_ ↑ _ (Typ_scope) [in term]
λ [ _ ] , _ (Typ_scope) [in term]
_ [ _ ← _ ] (Typ_scope) [in term]
! _ (Typ_scope) [in term]
_ [ ← _ ] (Typ_scope) [in term]
_ ·( _ , _ ) _ (Typ_scope) [in term]
# _ (Typ_scope) [in term]
U
_ · _ (UT_scope) [in ut_term]# _ (UT_scope) [in ut_term]
_ → _ (UT_scope) [in ut_red]
_ ⊣e (UT_scope) [in ut_typ_eq]
_ ≡ _ (UT_scope) [in ut_red]
_ →'__ (UT_scope) [in ut_red]
Π ( _ ) , _ (UT_scope) [in ut_term]
_ ⊢ _ : _ (UT_scope) [in ut_typ]
_ →e _ (UT_scope) [in ut_sr]
_ [[ _ ← _ ]] [in ut_strengh]
_ ≡e _ (UT_scope) [in ut_sr]
_ [ _ ← _ ] (UT_scope) [in ut_term]
_ ⊢e _ = _ : _ (UT_scope) [in ut_typ_eq]
_ ⊢e _ : _ (UT_scope) [in ut_typ_eq]
_ ⊢e _ = _ (UT_scope) [in ut_typ_eq_inj]
_ →'__ (UT_scope) [in ut_red]
_ ⊣ (UT_scope) [in ut_typ]
_ →→e _ (UT_scope) [in ut_sr]
_ →→ _ (UT_scope) [in ut_red]
_ ↓ _ ∈ _ (UT_scope) [in ut_env]
_ ↓ _ ⊂ _ (UT_scope) [in ut_env]
_ ↑ _ (UT_scope) [in ut_term]
λ [ _ ] , _ (UT_scope) [in ut_term]
! _ (UT_scope) [in ut_term]
_ [ ← _ ] (UT_scope) [in ut_term]
_ →→'__ (UT_scope) [in ut_red]
_ ↑ _ # _ (UT_scope) [in ut_term]
Inductive Index
E
env_mod.trunc [in env]env_mod.item [in env]
env_mod.ins_in_env [in env]
env_mod.sub_in_env [in env]
M
Mpts.iAx [in counter_ex]Mpts.iRel [in counter_ex]
Msorts.iSorts [in counter_ex]
P
PTS_ATR_mod.typ_peq [in typ_annot]PTS_ATR_mod.env_conv1 [in typ_annot]
PTS_ATR_mod.env_red [in typ_annot]
PTS_ATR_mod.typ_reds [in typ_annot]
PTS_ATR_mod.typ [in typ_annot]
PTS_ATR_mod.env_conv [in typ_annot]
PTS_ATR_mod.env_red1 [in typ_annot]
PTS_ATR_mod.wf [in typ_annot]
R
red_mod.Betaps [in red]red_mod.Beta [in red]
red_mod.Betas [in red]
red_mod.Betap [in red]
T
term_mod.Term [in term]U
ut_strengh_mod.Sigma [in ut_strengh]ut_typ_mod.typ [in ut_typ]
ut_red_mod.Betap [in ut_red]
ut_red_mod.Betac [in ut_red]
ut_typ_eq_mod.wf [in ut_typ_eq]
ut_env_mod.trunc [in ut_env]
ut_red_mod.Betaps [in ut_red]
ut_strengh_mod.Tv [in ut_strengh]
ut_sr_mod.Betas_env [in ut_sr]
ut_strengh_mod.Ts [in ut_strengh]
ut_sr_mod.Betac_env [in ut_sr]
ut_typ_eq_mod.typ [in ut_typ_eq]
ut_sr_mod.Beta_env [in ut_sr]
ut_typ_eq_inj_mod.wtyp_eq [in ut_typ_eq_inj]
ut_env_mod.ins_in_env [in ut_env]
ut_typ_mod.wf [in ut_typ]
ut_typ_eq_mod.typ_eq [in ut_typ_eq]
ut_term_mod.Term [in ut_term]
ut_env_mod.sub_in_env [in ut_env]
ut_red_mod.Betas [in ut_red]
ut_env_mod.item [in ut_env]
ut_red_mod.Beta [in ut_red]
Definition Index
C
CE.D1 [in counter_ex]CE.D2 [in counter_ex]
CE.PTSe_PiInj [in counter_ex]
E
env_mod.Env [in env]env_mod.item_lift [in env]
M
Mpts.Ax [in counter_ex]Mpts.Rel [in counter_ex]
Msorts.Sorts [in counter_ex]
S
strip_mod.strip_env [in strip]strip_mod.strip [in strip]
T
term_mod.lift_rec [in term]term_mod.subst_rec [in term]
U
ut_strengh_mod.env_subst_down [in ut_strengh]ut_term_mod.lift_rec [in ut_term]
ut_strengh_mod.Tels' [in ut_strengh]
ut_strengh_mod.Tels [in ut_strengh]
ut_env_mod.Env [in ut_env]
ut_strengh_mod.env_subst [in ut_strengh]
ut_env_mod.item_lift [in ut_env]
ut_term_mod.subst_rec [in ut_term]
V
Vars [in base]Moduleid Index
C
CE [in counter_ex]E
env_mod [in env]F
final_mod [in final_result]G
glue_mod [in glue]M
Mpts [in counter_ex]Msorts [in counter_ex]
P
PTS_ATR_mod [in typ_annot]pts_sig [in base]
R
red_mod [in red]S
strip_mod [in strip]T
term_sig [in base]term_mod [in term]
Theory [in final_result]
Theory.PTS [in final_result]
Theory.PTSATR [in final_result]
Theory.PTSe [in final_result]
U
ut_red_mod [in ut_red]ut_term_mod [in ut_term]
ut_strengh_mod [in ut_strengh]
ut_sr_mod [in ut_sr]
ut_env_mod [in ut_env]
ut_typ_mod [in ut_typ]
ut_typ_eq_mod [in ut_typ_eq]
ut_typ_eq_inj_mod [in ut_typ_eq_inj]
Axiom Index
P
pts_sig.Rel [in base]pts_sig.Ax [in base]
T
term_sig.Sorts [in base]Library Index
B
baseC
counter_exE
envF
final_resultG
glueR
redS
stripT
termtyp_annot
U
ut_srut_typ_eq_inj
ut_strengh
ut_red
ut_typ
ut_term
ut_env
ut_typ_eq
| 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 | (602 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 | (298 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 | (151 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 | (46 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 | (42 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 | (21 entries) |
| Moduleid 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 | (24 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 | (3 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 | (17 entries) |
This page has been generated by coqdoc