| 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 | (827 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 | (366 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 | (82 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 | (221 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 | (57 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 | (55 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 | (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 | (19 entries) |
Global Index
B
base [library]E
env [library]env_mod.ins_O [constructor, in ins_O]
env_mod.ins_S [constructor, in ins_S]
env_mod.item_lift [definition, in item_lift]
env_mod.nth_sub_item_inf [lemma, in nth_sub_item_inf]
env_mod.gt_O [lemma, in gt_O]
env_mod.sub_in_env [inductive, in sub_in_env]
env_mod.trunc [inductive, in trunc]
env_mod.ins_item_lift_lt [lemma, in ins_item_lift_lt]
_ ↓ _ ∈ _ (Typ_scope) [notation, in :Typ_scope:x_'↓'_x_'∈'_x]
env_mod.nth_sub_sup [lemma, in nth_sub_sup]
env_mod [module, in env_mod]
env_mod.item_trunc [lemma, in item_trunc]
env_mod.item_hd [constructor, in item_hd]
env_mod.nth_sub_eq [lemma, in nth_sub_eq]
_ ↓ _ ⊂ _ (Typ_scope) [notation, in :Typ_scope:x_'↓'_x_'⊂'_x]
env_mod.ins_in_env [inductive, in ins_in_env]
env_mod.nth_sub_inf [lemma, in nth_sub_inf]
env_mod.fun_item [lemma, in fun_item]
env_mod.Env [definition, in Env]
env_mod.ins_item_ge [lemma, in ins_item_ge]
env_mod.ins_item_lt [lemma, in ins_item_lt]
env_mod.item_tl [constructor, in item_tl]
env_mod.item [inductive, in item]
env_mod.sub_O [constructor, in sub_O]
env_mod.sub_S [constructor, in sub_S]
env_mod.trunc_O [constructor, in trunc_O]
env_mod.trunc_S [constructor, in trunc_S]
F
final_mod [module, in final_mod]final_mod.FromPTSATR_to_PTSe_trans [lemma, in FromPTSATR_to_PTSe_trans]
final_mod.FromPTS_to_PTSATR [lemma, in FromPTS_to_PTSATR]
final_mod.strip_var_ [lemma, in strip_var_]
final_mod.PTSe_SR_trans [lemma, in PTSe_SR_trans]
final_mod.FromPTSATR_to_PTS [lemma, in FromPTSATR_to_PTS]
final_mod.strip_var [lemma, in strip_var]
final_mod.FromPTSATR_to_PTSe [lemma, in FromPTSATR_to_PTSe]
final_mod.PTSe_SR [lemma, in PTSe_SR]
final_mod.PTS_equiv_PTSe [lemma, in PTS_equiv_PTSe]
final_result [library]
f_typ2_mod.der_wf [inductive, in der_wf]
f_term_mod.lift0 [lemma, in lift0]
f_env_mod.ins_O [constructor, in ins_O]
β _ (F_scope) [notation, in :F_scope:'β'_x]
f_env_mod.ins_S [constructor, in ins_S]
f_typ_mod.wf [inductive, in wf]
f_typ_mod.cBeta [constructor, in cBeta]
f_typ_mod.cAppEq [constructor, in cAppEq]
f_typ2_mod.dcons [constructor, in dcons]
f_typ_mod.lcAbs [constructor, in lcAbs]
_ [ _ ←h _ ] (F_scope) [notation, in :F_scope:x_'['_x_'←h'_x_']']
f_term_mod.AppEq [constructor, in AppEq]
f_typ_mod.ltyp_induc [definition, in ltyp_induc]
f_typ_mod.is_type [definition, in is_type]
εc _ (F_scope) [notation, in :F_scope:'εc'_x]
f_env_mod.item_lift [definition, in item_lift]
f_typ_mod.cApp [constructor, in cApp]
f_term_mod.ProdEq [constructor, in ProdEq]
f_typ_mod.sub_trunc [lemma, in sub_trunc]
_ ↓ _ ∈ _ (F_scope) [notation, in :F_scope:x_'↓'_x_'∈'_x]
f_env_mod.nth_sub_item_inf [lemma, in nth_sub_item_inf]
f_term_mod.subst_travers [lemma, in subst_travers]
f_typ_mod.wf_item [lemma, in wf_item]
f_term_mod.lift_is_lift [lemma, in lift_is_lift]
f_typ2_mod.subst_mult_sort [lemma, in subst_mult_sort]
f_typ_mod.simple_wf [inductive, in simple_wf]
f_typ2_mod.msub_O [constructor, in msub_O]
f_typ2_mod.dAbsEq [constructor, in dAbsEq]
f_typ2_mod.subst_mult_prod [lemma, in subst_mult_prod]
f_typ2_mod.msub_S [constructor, in msub_S]
f_typ2_mod.erasure_injectivity_type [lemma, in erasure_injectivity_type]
f_typ2_mod.subst_mult_var_eq [lemma, in subst_mult_var_eq]
f_typ2_mod.der_typ [inductive, in der_typ]
f_typ2_mod.erasure_outer [definition, in erasure_outer]
f_typ_mod.simple2normal [lemma, in simple2normal]
f_typ_mod.gen_var [lemma, in gen_var]
_ ⊢ _ : _ : _ [notation, in ::x_'⊢'_x_':'_x_':'_x]
f_typ_mod.thinning [lemma, in thinning]
_ † (F_scope) [notation, in :F_scope:x_'†']
f_typ2_mod.dVar [constructor, in dVar]
f_typ2_mod.unique_der_ext [lemma, in unique_der_ext]
f_typ2_mod.erasure_injectivity_term_type [lemma, in erasure_injectivity_term_type]
f_term_mod.Var [constructor, in Var]
f_typ_mod.wf_item_lift [lemma, in wf_item_lift]
_ ⊢ _ : _ (F_scope) [notation, in :F_scope:x_'⊢'_x_':'_x]
f_term_mod.Sort [constructor, in Sort]
_ ⊢' _ : _ (F_scope) [notation, in :F_scope:x_'⊢'''_x_':'_x]
f_term_mod.Prod [constructor, in Prod]
f_env_mod.sub_in_env [inductive, in sub_in_env]
f_typ_mod.lcConv [constructor, in lcConv]
f_equiv_mod [module, in f_equiv_mod]
f_env_mod.trunc [inductive, in trunc]
f_typ2_mod.der_typ_ind' [definition, in der_typ_ind']
f_env_mod [module, in f_env_mod]
f_typ2_mod.equality_subst [lemma, in equality_subst]
f_equiv_mod.PTSl2PTSF [lemma, in PTSl2PTSF]
f_typ_mod.wf_ind' [definition, in wf_ind']
f_typ2_mod.subst_mult_trunc [lemma, in subst_mult_trunc]
f_env_mod.ins_item_lift_lt [lemma, in ins_item_lift_lt]
f_typ_mod [module, in f_typ_mod]
f_term_mod.erasure_lem1 [lemma, in erasure_lem1]
_ ↑h _ (F_scope) [notation, in :F_scope:x_'↑h'_x]
f_typ2_mod.erasure_lem2 [lemma, in erasure_lem2]
f_term_mod.erasure_lem3 [lemma, in erasure_lem3]
ρ _ (F_scope) [notation, in :F_scope:'ρ'_x]
f_typ_mod.weakening [lemma, in weakening]
f_env_mod.subst_trunc [lemma, in subst_trunc]
f_typ2_mod.unique_der [lemma, in unique_der]
f_typ2_mod.subst_mult_term [definition, in subst_mult_term]
f_typ_mod.thinning_n_h [lemma, in thinning_n_h]
f_typ2_mod.comp_sort [constructor, in comp_sort]
f_typ2_mod.dTrans [constructor, in dTrans]
f_typ_mod.cConv [constructor, in cConv]
f_typ2_mod.comp_prod [constructor, in comp_prod]
f_typ2_mod.subst_mult_eq [lemma, in subst_mult_eq]
ε _ (F_scope) [notation, in :F_scope:'ε'_x]
f_typ2_mod.dRefl [constructor, in dRefl]
f_typ2_mod.erasure_term_type [lemma, in erasure_term_type]
f_typ2_mod.subst_mult_var [lemma, in subst_mult_var]
f_term_mod.Term [inductive, in Term]
f_typ_mod.beta_type_l [lemma, in beta_type_l]
f_typ_mod.beta_type_r [lemma, in beta_type_r]
f_typ2_mod.node [constructor, in node]
f_typ_mod.normal_equiv_simple [lemma, in normal_equiv_simple]
f_env_mod.subst_trunc2 [lemma, in subst_trunc2]
ι _ (F_scope) [notation, in :F_scope:'ι'_x]
f_typ2_mod.dSym [constructor, in dSym]
f_typ_mod.substitution [lemma, in substitution]
f_typ2_mod.subst_typR [lemma, in subst_typR]
f_typ2_mod.context_conversion [lemma, in context_conversion]
f_term_mod.Sym [constructor, in Sym]
f_typ2_mod.dAppEq [constructor, in dAppEq]
f_typ2_mod [module, in f_typ2_mod]
f_typ2_mod.erasure_context [definition, in erasure_context]
f_typ_mod.lcApp [constructor, in lcApp]
f_term_mod.lift_lift [lemma, in lift_lift]
f_typ_mod.cVar [constructor, in cVar]
f_typ2_mod.der_sound [lemma, in der_sound]
_ ↓ _ ⊂ _ (F_scope) [notation, in :F_scope:x_'↓'_x_'⊂'_x]
! _ (F_scope) [notation, in :F_scope:'!'_x]
f_typ2_mod.dnil [constructor, in dnil]
f_typ2_mod.subst_wf [lemma, in subst_wf]
f_env_mod.nth_sub_sup [lemma, in nth_sub_sup]
f_typ2_mod.dIota [constructor, in dIota]
f_typ_mod.lwf_ind' [definition, in lwf_ind']
f_term_mod.lift_rec_h [definition, in lift_rec_h]
f_typ_mod.gen_conv [lemma, in gen_conv]
f_typ_mod.lcSort [constructor, in lcSort]
f_term_mod.Prf_ind' [definition, in Prf_ind']
f_typ_mod.lcProd [constructor, in lcProd]
f_env_mod.subst_item [lemma, in subst_item]
f_typ_mod.wf_cons [constructor, in wf_cons]
f_env_mod.item_trunc [lemma, in item_trunc]
f_typ2_mod.erasure_item_lift_rev [lemma, in erasure_item_lift_rev]
f_typ2_mod.dBeta [constructor, in dBeta]
f_typ2_mod.erasure_outer_not_conv [lemma, in erasure_outer_not_conv]
_ ⊣' (F_scope) [notation, in :F_scope:x_'⊣''']
_ ·h _ (F_scope) [notation, in :F_scope:x_'·h'_x]
f_typ2_mod.erasure [definition, in erasure]
f_typ2_mod.dAbs [constructor, in dAbs]
_ ↑ _ # _ (F_scope) [notation, in :F_scope:x_'↑'_x_'#'_x]
f_term_mod.subst_rec [definition, in subst_rec]
f_term_mod.Refl [constructor, in Refl]
f_typ2_mod.erasure_term [lemma, in erasure_term]
f_env_mod.item_hd [constructor, in item_hd]
f_typ2_mod.subst_mult_lift_sup [lemma, in subst_mult_lift_sup]
f_term_mod.Abs [constructor, in Abs]
_ ↑h _ # _ (F_scope) [notation, in :F_scope:x_'↑h'_x_'#'_x]
_ [ _ ← _ ] (F_scope) [notation, in :F_scope:x_'['_x_'←'_x_']']
_ ↑ _ (F_scope) [notation, in :F_scope:x_'↑'_x]
f_typ_mod.typh_ind' [definition, in typh_ind']
f_typ2_mod.subst_mult_var_P2 [lemma, in subst_mult_var_P2]
f_typ2_mod.erasure_item_lift [lemma, in erasure_item_lift]
f_typ_mod.equality_typing [lemma, in equality_typing]
f_typ2_mod.comparable [inductive, in comparable]
f_equiv_mod.PTSeq2PTSF [lemma, in PTSeq2PTSF]
f_term_mod.lift_is_lift_sublemma [lemma, in lift_is_lift_sublemma]
f_typ_mod.cSort [constructor, in cSort]
λ [ _ ] , _ (F_scope) [notation, in :F_scope:'λ'_'['_x_']'_','_x]
f_typ_mod.cProd [constructor, in cProd]
f_typ2_mod.der_h [inductive, in der_h]
f_typ2_mod.context_conversion_context [lemma, in context_conversion_context]
f_typ_mod.TypeCorrect [lemma, in TypeCorrect]
f_typ_mod.typ [inductive, in typ]
f_typ2_mod.der_wf_ind' [definition, in der_wf_ind']
f_typ_mod.equality_unique [lemma, in equality_unique]
f_typ_mod.cSym [constructor, in cSym]
f_typ2_mod.der_induc [definition, in der_induc]
f_env_mod.ins_in_env [inductive, in ins_in_env]
f_term_mod.Iota [constructor, in Iota]
f_typ_mod.typ_ind' [definition, in typ_ind']
f_typ_mod.thinning_h [lemma, in thinning_h]
f_typ2_mod.comp_refl [constructor, in comp_refl]
f_env_mod.nth_sub_inf [lemma, in nth_sub_inf]
f_typ_mod.thinning_n [lemma, in thinning_n]
f_term_mod.Term_induc [definition, in Term_induc]
f_typ2_mod.equality_subst_ext [lemma, in equality_subst_ext]
f_env_mod.fun_item [lemma, in fun_item]
f_env_mod.Env [definition, in Env]
_ [ ← _ ] (F_scope) [notation, in :F_scope:x_'['_'←'_x_']']
f_typ2_mod.subst_mult_abs [lemma, in subst_mult_abs]
f_typ_mod.lwf_cons [constructor, in lwf_cons]
f_env_mod.ins_item [lemma, in ins_item]
f_env_mod.ins_item_ge [lemma, in ins_item_ge]
f_typ2_mod.der_h_ind' [definition, in der_h_ind']
f_typ_mod.gen_la [lemma, in gen_la]
f_term_mod.Beta [constructor, in Beta]
f_typ_mod.typ_induc [definition, in typ_induc]
f_typ2_mod.erasure_equality2 [lemma, in erasure_equality2]
f_typ_mod.gen_sort [lemma, in gen_sort]
f_env_mod.trunc_trans [lemma, in trunc_trans]
f_typ_mod.lcAbsEq [constructor, in lcAbsEq]
f_typ_mod.lcVar [constructor, in lcVar]
f_typ2_mod.subst_mult_lift_inf [lemma, in subst_mult_lift_inf]
f_term_mod.substP1 [lemma, in substP1]
f_term_mod.substP2 [lemma, in substP2]
f_term_mod.substP3 [lemma, in substP3]
f_typ_mod.simple_typ [inductive, in simple_typ]
f_typ2_mod.comp_subst [lemma, in comp_subst]
f_term_mod.substP4 [lemma, in substP4]
f_typ_mod.cProdEq [constructor, in cProdEq]
⟨ _ , [ _ ] _ ⟩ (F_scope) [notation, in :F_scope:'⟨'_x_','_'['_x_']'_x_'⟩']
f_typ2_mod.subst_mult_wf [lemma, in subst_mult_wf]
f_typ2_mod.dConv [constructor, in dConv]
f_typ_mod.cAbs [constructor, in cAbs]
f_typ_mod.wf_nil [constructor, in wf_nil]
f_env_mod.trunc_inj [lemma, in trunc_inj]
f_typ2_mod.erasure_item [lemma, in erasure_item]
f_typ_mod.lcRefl [constructor, in lcRefl]
f_typ_mod.gen_pi [lemma, in gen_pi]
f_typ_mod.cAbsEq [constructor, in cAbsEq]
{ _ , [ _ ] _ } (F_scope) [notation, in :F_scope:'{'_x_','_'['_x_']'_x_'}']
_ · _ (F_scope) [notation, in :F_scope:x_'·'_x]
f_typ_mod.normal2simple [lemma, in normal2simple]
_ [ ←h _ ] (F_scope) [notation, in :F_scope:x_'['_'←h'_x_']']
f_term_mod.Prf [inductive, in Prf]
f_term_mod.lift_rec [definition, in lift_rec]
f_typ2_mod.subst_mult_env [inductive, in subst_mult_env]
f_term_mod.AbsEq [constructor, in AbsEq]
f_equiv_mod.PTSlequivPTSF [lemma, in PTSlequivPTSF]
f_env_mod.ins_item_lt [lemma, in ins_item_lt]
f_typ_mod.typ_h_short [definition, in typ_h_short]
f_env_mod.item_tl [constructor, in item_tl]
f_typ2_mod.erasure_erasure_outer [lemma, in erasure_erasure_outer]
_ • _ (F_scope) [notation, in :F_scope:x_'•'_x]
f_typ_mod.gen_app [lemma, in gen_app]
_ ⊢ _ : _ = _ (F_scope) [notation, in :F_scope:x_'⊢'_x_':'_x_'='_x]
f_term_mod.subst_rec_h [definition, in subst_rec_h]
f_typ2_mod.deriv [inductive, in deriv]
f_typ2_mod.dApp [constructor, in dApp]
_ ∽ _ (F_scope) [notation, in :F_scope:x_'∽'_x]
_ ⊣ (F_scope) [notation, in :F_scope:x_'⊣']
f_term_mod.Term_ind' [definition, in Term_ind']
f_typ_mod.simple_typ_h [inductive, in simple_typ_h]
f_term_mod.App [constructor, in App]
f_typ2_mod.subst_mult_cons [lemma, in subst_mult_cons]
f_typ_mod.conv_inj [lemma, in conv_inj]
f_equiv_mod.Prod_Injective [lemma, in Prod_Injective]
f_typ2_mod.subst_mult_conv [lemma, in subst_mult_conv]
_ ⊢' _ : _ = _ (F_scope) [notation, in :F_scope:x_'⊢'''_x_':'_x_'='_x]
Π ( _ ) , _ (F_scope) [notation, in :F_scope:'Π'_'('_x_')'_','_x]
f_typ_mod.typ_h [inductive, in typ_h]
f_typ2_mod.erasure_outer_typing [lemma, in erasure_outer_typing]
f_typ_mod.lwf_nil [constructor, in lwf_nil]
f_typ2_mod.erasure_injectivity_term_sort [lemma, in erasure_injectivity_term_sort]
f_term_mod [module, in f_term_mod]
f_typ2_mod.dProdEq [constructor, in dProdEq]
f_typ_mod.lcIota [constructor, in lcIota]
f_term_mod.inv_lift [lemma, in inv_lift]
f_typ_mod.lcTrans [constructor, in lcTrans]
f_typ_mod.cRefl [constructor, in cRefl]
f_env_mod.item [inductive, in item]
f_typ_mod.ltyp_ind' [definition, in ltyp_ind']
f_typ2_mod.der_complete [lemma, in der_complete]
f_env_mod.sub_O [constructor, in sub_O]
f_typ2_mod.erasure_equality [lemma, in erasure_equality]
f_env_mod.sub_S [constructor, in sub_S]
f_typ_mod.lcSym [constructor, in lcSym]
f_typ_mod.wf_typ [lemma, in wf_typ]
f_term_mod.liftP1 [lemma, in liftP1]
f_typ_mod.ltyph_ind' [definition, in ltyph_ind']
f_term_mod.liftP2 [lemma, in liftP2]
f_typ2_mod.type_comparable [lemma, in type_comparable]
f_term_mod.liftP3 [lemma, in liftP3]
f_typ_mod.has_type [definition, in has_type]
f_typ_mod.lcProdEq [constructor, in lcProdEq]
f_term_mod.Conv [constructor, in Conv]
f_typ2_mod.erasure_subst [lemma, in erasure_subst]
# _ (F_scope) [notation, in :F_scope:'#'_x]
f_typ2_mod.subst_typ [lemma, in subst_typ]
f_typ_mod.lcBeta [constructor, in lcBeta]
f_term_mod.lift_rec0 [lemma, in lift_rec0]
f_typ2_mod.subst_mult_prf [definition, in subst_mult_prf]
f_typ_mod.lcAppEq [constructor, in lcAppEq]
f_typ2_mod.erasure_injectivity_term [lemma, in erasure_injectivity_term]
f_typ_mod.semitype [definition, in semitype]
_ ⊢ _ = _ [notation, in ::x_'⊢'_x_'='_x]
f_typ_mod.cTrans [constructor, in cTrans]
f_term_mod.subst_is_lift [lemma, in subst_is_lift]
f_typ_mod.cIota [constructor, in cIota]
f_typ2_mod.subst_mult_typ [lemma, in subst_mult_typ]
f_env_mod.trunc_O [constructor, in trunc_O]
f_term_mod.Trans [constructor, in Trans]
f_env_mod.trunc_S [constructor, in trunc_S]
f_typ2_mod.dSort [constructor, in dSort]
f_typ2_mod.subst_eq [lemma, in subst_eq]
f_equiv_mod.PTSF2PTSl [lemma, in PTSF2PTSl]
f_typ2_mod.erasure_lift [lemma, in erasure_lift]
f_typ2_mod.dProd [constructor, in dProd]
f_typ2_mod.subst_mult_app [lemma, in subst_mult_app]
f_env_mod.ins_trunc [lemma, in ins_trunc]
f_typ2_mod.PTSF2PTS [lemma, in PTSF2PTS]
f_typ2 [library]
f_equivalence [library]
f_typ [library]
f_term [library]
f_env [library]
G
glue [library]glue_mod.L43_ [lemma, in L43_]
glue_mod.ErasedContextSwitch [lemma, in ErasedContextSwitch]
glue_mod [module, in glue_mod]
glue_mod.L33 [lemma, in L33]
glue_mod.ErasedTermConfluence [lemma, in ErasedTermConfluence]
glue_mod.weak_type_shape [lemma, in weak_type_shape]
glue_mod.L33' [lemma, in L33']
glue_mod.peq_not_Pi_sort [lemma, in peq_not_Pi_sort]
glue_mod.ErasedTypeConversion [lemma, in ErasedTypeConversion]
P
PTS_ATR_mod.typ_reds_ind' [definition, in typ_reds_ind']PTS_ATR_mod.wf [inductive, in wf]
PTS_ATR_mod.wf_from_peq [lemma, in wf_from_peq]
PTS_ATR_mod.env_conv_cons [lemma, in env_conv_cons]
PTS_ATR_mod.sub_trunc [lemma, in sub_trunc]
PTS_ATR_mod.c_step [constructor, in c_step]
PTS_ATR_mod.wf_item [lemma, in wf_item]
PTS_ATR_mod.ConvSort [lemma, in ConvSort]
PTS_ATR_mod.typ_sort [constructor, in typ_sort]
PTS_ATR_mod.OSDiamond [lemma, in OSDiamond]
PTS_ATR_mod.reds_refl_rt [lemma, in reds_refl_rt]
PTS_ATR_mod.SR [lemma, in SR]
_ ⊢ _ ▹▹ _ : _ (Typ_scope) [notation, in :Typ_scope:x_'⊢'_x_'▹▹'_x_':'_x]
PTS_ATR_mod.typ_peq_sym [lemma, in typ_peq_sym]
PTS_ATR_mod.reds_subst [lemma, in reds_subst]
PTS_ATR_mod.thinning [lemma, in thinning]
PTS_ATR_mod.typ_la [constructor, in typ_la]
PTS_ATR_mod.wf_item_lift [lemma, in wf_item_lift]
PTS_ATR_mod.typ_app [constructor, in typ_app]
PTS_ATR_mod.fun_item_lift [lemma, in fun_item_lift]
PTS_ATR_mod.typ_reds_trans2 [lemma, in typ_reds_trans2]
PTS_ATR_mod.env_red1 [inductive, in env_red1]
PTS_ATR_mod.typ_exp [constructor, in typ_exp]
PTS_ATR_mod.wf_ind' [definition, in wf_ind']
PTS_ATR_mod.conv_in_env_reds [lemma, in conv_in_env_reds]
PTS_ATR_mod.weakening [lemma, in weakening]
PTS_ATR_mod.wf_from_typ_reds [lemma, in wf_from_typ_reds]
PTS_ATR_mod.pgen_app [lemma, in pgen_app]
PTS_ATR_mod.red1_in_env [lemma, in red1_in_env]
PTS_ATR_mod.reds_App___ [lemma, in reds_App___]
PTS_ATR_mod.Sort_Reds [lemma, in Sort_Reds]
PTS_ATR_mod.reds_App_ [lemma, in reds_App_]
PTS_ATR_mod.typ_pi [constructor, in typ_pi]
PTS_ATR_mod.SR_trans [lemma, in SR_trans]
PTS_ATR_mod.r_refl [constructor, in r_refl]
PTS_ATR_mod.typ_reds_trans_ [lemma, in typ_reds_trans_]
PTS_ATR_mod.red1_next [constructor, in red1_next]
PTS_ATR_mod.peq_subst [lemma, in peq_subst]
PTS_ATR_mod.conv1_in_env [lemma, in conv1_in_env]
PTS_ATR_mod.red_refl_lt [lemma, in red_refl_lt]
PTS_ATR_mod.typ_pcompat [lemma, in typ_pcompat]
PTS_ATR_mod.PiInj [lemma, in PiInj]
PTS_ATR_mod.reds_subst_gen [lemma, in reds_subst_gen]
PTS_ATR_mod.conv_in_env_peq [lemma, in conv_in_env_peq]
PTS_ATR_mod.typ_reds_intro [constructor, in typ_reds_intro]
PTS_ATR_mod.typ_exp_trans [lemma, in typ_exp_trans]
PTS_ATR_mod.typ_reds_trans [constructor, in typ_reds_trans]
PTS_ATR_mod.c_trans [constructor, in c_trans]
PTS_ATR_mod.pgen_la [lemma, in pgen_la]
PTS_ATR_mod.peq_thinning [lemma, in peq_thinning]
PTS_ATR_mod.typ_reds_relocate [lemma, in typ_reds_relocate]
PTS_ATR_mod.reds_App__ [lemma, in reds_App__]
PTS_ATR_mod.typ_reds [inductive, in typ_reds]
PTS_ATR_mod.wf_from_typ [lemma, in wf_from_typ]
pts_sig.Rel [axiom, in Rel]
PTS_ATR_mod.c_refl [constructor, in c_refl]
PTS_ATR_mod.typ_wf [lemma, in typ_wf]
PTS_ATR_mod.red_refl_rt [lemma, in red_refl_rt]
PTS_ATR_mod.env_red_to_conv [lemma, in env_red_to_conv]
PTS_ATR_mod.env_red_cons [lemma, in env_red_cons]
pts_sig [module, in pts_sig]
PTS_ATR_mod.typ_reds_to_red_ [lemma, in typ_reds_to_red_]
PTS_ATR_mod.subst_gen [lemma, in subst_gen]
_ ⊢ _ ▹ _ : _ (Typ_scope) [notation, in :Typ_scope:x_'⊢'_x_'▹'_x_':'_x]
PTS_ATR_mod.pgen_pi [lemma, in pgen_pi]
PTS_ATR_mod.wf_cons [constructor, in wf_cons]
PTS_ATR_mod [module, in PTS_ATR_mod]
_ ⊣ (Typ_scope) [notation, in :Typ_scope:x_'⊣']
PTS_ATR_mod.typ_var [constructor, in typ_var]
PTS_ATR_mod.env_red [inductive, in env_red]
PTS_ATR_mod.relocate [lemma, in relocate]
PTS_ATR_mod.typ_peq_intro [constructor, in typ_peq_intro]
PTS_ATR_mod.typ_peq_trans [constructor, in typ_peq_trans]
PTS_ATR_mod.reds_Pi_ [lemma, in reds_Pi_]
PTS_ATR_mod.SubDiam [lemma, in SubDiam]
PTS_ATR_mod.pgen_var [lemma, in pgen_var]
PTS_ATR_mod.reds_La [lemma, in reds_La]
PTS_ATR_mod.ChurchRosser [lemma, in ChurchRosser]
PTS_ATR_mod.typ [inductive, in typ]
PTS_ATR_mod.typ_beta [constructor, in typ_beta]
PTS_ATR_mod.typ_ind' [definition, in typ_ind']
PTS_ATR_mod.SR_trans' [lemma, in SR_trans']
PTS_ATR_mod.thinning_n [lemma, in thinning_n]
PTS_ATR_mod.typ_ind2 [lemma, in typ_ind2]
PTS_ATR_mod.typ_peq_intro2 [constructor, in typ_peq_intro2]
PTS_ATR_mod.r_trans [constructor, in r_trans]
PTS_ATR_mod.La_Reds [lemma, in La_Reds]
PTS_ATR_mod.pgen_sort [lemma, in pgen_sort]
PTS_ATR_mod.c_sym [lemma, in c_sym]
PTS_ATR_mod.reds_Pi [lemma, in reds_Pi]
PTS_ATR_mod.typ_induc [definition, in typ_induc]
PTS_ATR_mod.env_conv1_wf [lemma, in env_conv1_wf]
PTS_ATR_mod.env_conv_wf [lemma, in env_conv_wf]
PTS_ATR_mod.thinning_reds_n [lemma, in thinning_reds_n]
PTS_ATR_mod.peq_thinning_n [lemma, in peq_thinning_n]
PTS_ATR_mod.typ_peq_to_red [lemma, in typ_peq_to_red]
PTS_ATR_mod.Confluence [lemma, in Confluence]
PTS_ATR_mod.red_in_env [lemma, in red_in_env]
PTS_ATR_mod.typ_red [constructor, in typ_red]
PTS_ATR_mod.env_red1_wf [lemma, in env_red1_wf]
PTS_ATR_mod.wf_nil [constructor, in wf_nil]
PTS_ATR_mod.conv_item [lemma, in conv_item]
pts_sig.Ax [axiom, in Ax]
PTS_ATR_mod.reds_typ_pcompat [lemma, in reds_typ_pcompat]
PTS_ATR_mod.red_in_env_reds [lemma, in red_in_env_reds]
PTS_ATR_mod.c1_sym [lemma, in c1_sym]
PTS_ATR_mod.env_conv [inductive, in env_conv]
PTS_ATR_mod.env_red1_to_conv1 [lemma, in env_red1_to_conv1]
PTS_ATR_mod.Pi_Reds [lemma, in Pi_Reds]
PTS_ATR_mod.thinning_reds [lemma, in thinning_reds]
PTS_ATR_mod.reds_App [lemma, in reds_App]
PTS_ATR_mod.conv1_intro [constructor, in conv1_intro]
PTS_ATR_mod.eq_subst_gen [lemma, in eq_subst_gen]
PTS_ATR_mod.typ_peq [inductive, in typ_peq]
PTS_ATR_mod.env_red_wf [lemma, in env_red_wf]
PTS_ATR_mod.red1_intro [constructor, in red1_intro]
PTS_ATR_mod.red_item [lemma, in red_item]
PTS_ATR_mod.conv_in_env [lemma, in conv_in_env]
PTS_ATR_mod.env_conv1 [inductive, in env_conv1]
PTS_ATR_mod.sub_in_env_item [lemma, in sub_in_env_item]
PTS_ATR_mod.r_step [constructor, in r_step]
PTS_ATR_mod.typ_red_trans [lemma, in typ_red_trans]
_ ⊢ _ ≡' _ (Typ_scope) [notation, in :Typ_scope:x_'⊢'_x_'≡'''_x]
PTS_ATR_mod.reds_refl_lt [lemma, in reds_refl_lt]
PTS_ATR_mod.conv1_next [constructor, in conv1_next]
PTS_ATR_mod.reds_to_conv [lemma, in reds_to_conv]
R
red [library]_ → _ (Typ_scope) [notation, in :Typ_scope:x_'→'_x]
red_mod.Betaps_to_Betas [lemma, in Betaps_to_Betas]
red_mod.Betaps_Beta_closure [lemma, in Betaps_Beta_closure]
red_mod.Betap_sort [constructor, in Betap_sort]
red_mod.Beta_head [constructor, in Beta_head]
red_mod.Betap_pi [constructor, in Betap_pi]
red_mod.Betas_Beta [constructor, in Betas_Beta]
red_mod.Betap_to_Betas [lemma, in Betap_to_Betas]
red_mod.Betaps [inductive, in Betaps]
red_mod.Betas_refl [constructor, in Betas_refl]
red_mod.Betap_refl [lemma, in Betap_refl]
red_mod.Betas_trans [constructor, in Betas_trans]
red_mod.Betaps_intro [constructor, in Betaps_intro]
red_mod.Betaps_trans [constructor, in Betaps_trans]
red_mod.Betaps_Betas_closure [lemma, in Betaps_Betas_closure]
red_mod.Betap_App [constructor, in Betap_App]
_ →' _ (Typ_scope) [notation, in :Typ_scope:x_'→'''_x]
red_mod.Beta_lam2 [constructor, in Beta_lam2]
red_mod.Betap_var [constructor, in Betap_var]
_ →→ _ (Typ_scope) [notation, in :Typ_scope:x_'→→'_x]
red_mod.Betas_La [lemma, in Betas_La]
red_mod.Betap [inductive, in Betap]
red_mod.Betas [inductive, in Betas]
red_mod.Beta_pi [constructor, in Beta_pi]
red_mod.Beta [inductive, in Beta]
red_mod [module, in red_mod]
red_mod.Betas_Pi [lemma, in Betas_Pi]
red_mod.Betap_head [constructor, in Betap_head]
red_mod.Beta_red1 [constructor, in Beta_red1]
red_mod.Beta_red2 [constructor, in Beta_red2]
red_mod.Beta_red3 [constructor, in Beta_red3]
red_mod.Beta_red4 [constructor, in Beta_red4]
red_mod.Betas_App [lemma, in Betas_App]
red_mod.Beta_pi2 [constructor, in Beta_pi2]
red_mod.Beta_lam [constructor, in Beta_lam]
_ →→' _ (Typ_scope) [notation, in :Typ_scope:x_'→→'''_x]
red_mod.Betap_lam [constructor, in Betap_lam]
S
strip [library]strip_mod [module, in strip_mod]
strip_mod.strip_env [definition, in strip_env]
strip_mod.strip_lift [lemma, in strip_lift]
strip_mod.strip_subst [lemma, in strip_subst]
strip_mod.strip [definition, in strip]
T
term [library]term_mod.lift0 [lemma, in lift0]
term_mod.Pi [constructor, in Pi]
term_mod.subst_travers [lemma, in subst_travers]
Π ( _ ) , _ (Typ_scope) [notation, in :Typ_scope:'Π'_'('_x_')'_','_x]
# _ (Typ_scope) [notation, in :Typ_scope:'#'_x]
term_mod.Var [constructor, in Var]
term_mod.Sort [constructor, in Sort]
term_sig.Sorts [axiom, in Sorts]
term_sig [module, in term_sig]
_ ↑ _ (Typ_scope) [notation, in :Typ_scope:x_'↑'_x]
term_mod.Term [inductive, in Term]
term_mod.lift_lift [lemma, in lift_lift]
term_mod.subst_rec [definition, in subst_rec]
term_mod.expand_term_with_subst [lemma, in expand_term_with_subst]
! _ (Typ_scope) [notation, in :Typ_scope:'!'_x]
_ [ ← _ ] (Typ_scope) [notation, in :Typ_scope:x_'['_'←'_x_']']
_ [ _ ← _ ] (Typ_scope) [notation, in :Typ_scope:x_'['_x_'←'_x_']']
term_mod [module, in term_mod]
term_mod.substP1 [lemma, in substP1]
term_mod.substP2 [lemma, in substP2]
term_mod.substP3 [lemma, in substP3]
term_mod.substP4 [lemma, in substP4]
_ ·( _ , _ ) _ (Typ_scope) [notation, in :Typ_scope:x_'·('_x_','_x_')'_x]
term_mod.lift_rec [definition, in lift_rec]
λ [ _ ] , _ (Typ_scope) [notation, in :Typ_scope:'λ'_'['_x_']'_','_x]
term_mod.App [constructor, in App]
_ ↑ _ # _ (Typ_scope) [notation, in :Typ_scope:x_'↑'_x_'#'_x]
term_mod.inv_lift [lemma, in inv_lift]
term_mod.liftP1 [lemma, in liftP1]
term_mod.liftP2 [lemma, in liftP2]
term_mod.liftP3 [lemma, in liftP3]
term_mod.lift_rec0 [lemma, in lift_rec0]
term_mod.La [constructor, in La]
Theory [module, in Theory]
Theory.PTS [module, in Theory.PTS]
Theory.PTSATR [module, in Theory.PTSATR]
Theory.PTSe [module, in Theory.PTSe]
typ_annot [library]
U
ut_term_mod.lift0 [lemma, in lift0]_ · _ (UT_scope) [notation, in :UT_scope:x_'·'_x]
ut_typ_eq_mod.cSymm [constructor, in cSymm]
ut_env_mod.ins_O [constructor, in ins_O]
ut_env_mod.ins_S [constructor, in ins_S]
ut_typ_eq_mod.wf [inductive, in wf]
ut_typ_mod.wf [inductive, in wf]
ut_sr_mod.Betas_env_nil2 [lemma, in Betas_env_nil2]
ut_typ_eq_mod.cBeta [constructor, in cBeta]
ut_typ_eq_mod.typ_eqm [inductive, in typ_eqm]
_ ⊣e (UT_scope) [notation, in :UT_scope:x_'⊣e']
ut_red_mod.Betac_confl [lemma, in Betac_confl]
ut_sr_mod.SubjectRed [lemma, in SubjectRed]
ut_red_mod.Betac_sym [constructor, in Betac_sym]
ut_env_mod.item_lift [definition, in item_lift]
ut_typ_eq_mod.cApp [constructor, in cApp]
ut_typ_mod.cApp [constructor, in cApp]
_ [ ← _ ] (UT_scope) [notation, in :UT_scope:x_'['_'←'_x_']']
ut_typ_mod.sub_trunc [lemma, in sub_trunc]
ut_red_mod.Betaps_Beta_closure [lemma, in Betaps_Beta_closure]
ut_env_mod.nth_sub_item_inf [lemma, in nth_sub_item_inf]
ut_term_mod.Pi [constructor, in Pi]
ut_term_mod.subst_travers [lemma, in subst_travers]
ut_red_mod.Betap_sort [constructor, in Betap_sort]
ut_typ_eq_mod.cTransm [constructor, in cTransm]
ut_typ_eq_mod.wf_item [lemma, in wf_item]
_ ⊣' (UT_scope) [notation, in :UT_scope:x_'⊣''']
ut_typ_mod.wf_item [lemma, in wf_item]
ut_red_mod.Beta_head [constructor, in Beta_head]
_ →→ _ (UT_scope) [notation, in :UT_scope:x_'→→'_x]
! _ (UT_scope) [notation, in :UT_scope:'!'_x]
ut_red_mod.Beta_lift [lemma, in Beta_lift]
_ ↑ _ (UT_scope) [notation, in :UT_scope:x_'↑'_x]
ut_typ_mod.gen_var [lemma, in gen_var]
ut_typ_eq_mod.wfm_ind' [definition, in wfm_ind']
ut_red_mod.Betas_subst2 [lemma, in Betas_subst2]
ut_sr_mod.Beta_env_sound [lemma, in Beta_env_sound]
ut_typ_eq_mod.cPi_eqm [constructor, in cPi_eqm]
ut_typ_eq_mod.thinning [lemma, in thinning]
ut_typ_mod.thinning [lemma, in thinning]
ut_sr_mod.Beta_env_cons [constructor, in Beta_env_cons]
ut_sr_mod.Betas_env_refl [constructor, in Betas_env_refl]
ut_red_mod.Betac_not_Pi_sort [lemma, in Betac_not_Pi_sort]
ut_term_mod.Var [constructor, in Var]
ut_typ_eq_mod.wf_item_lift [lemma, in wf_item_lift]
ut_typ_mod.wf_item_lift [lemma, in wf_item_lift]
ut_sr_mod.Betas_env_sound_up [lemma, in Betas_env_sound_up]
ut_env_mod.gt_O [lemma, in gt_O]
ut_term_mod.Sort [constructor, in Sort]
ut_red_mod.Betap_pi [constructor, in Betap_pi]
ut_env_mod.sub_in_env [inductive, in sub_in_env]
ut_typ_eq_mod.wf_typ_eq [lemma, in wf_typ_eq]
ut_env_mod.trunc [inductive, in trunc]
_ ⊢ _ : _ (UT_scope) [notation, in :UT_scope:x_'⊢'_x_':'_x]
ut_sr_mod.Betac_env_sym [constructor, in Betac_env_sym]
ut_typ_eq_mod.wf_ind' [definition, in wf_ind']
ut_typ_mod.wf_ind' [definition, in wf_ind']
ut_env_mod.ins_item_lift_lt [lemma, in ins_item_lift_lt]
ut_typ_eq_mod.cSortm [constructor, in cSortm]
ut_red_mod.Betap_subst [lemma, in Betap_subst]
Π ( _ ) , _ (UT_scope) [notation, in :UT_scope:'Π'_'('_x_')'_','_x]
ut_red_mod.Betac_refl [lemma, in Betac_refl]
ut_sr_mod.Beta_env_sound2 [lemma, in Beta_env_sound2]
ut_typ_eq_mod.cPi_eq [constructor, in cPi_eq]
ut_typ_eq_mod.weakening [lemma, in weakening]
ut_typ_eq_mod.cApp_eq [constructor, in cApp_eq]
ut_typ_mod.weakening [lemma, in weakening]
ut_red_mod.Betap_app [constructor, in Betap_app]
ut_red_mod.Betas_Beta [constructor, in Betas_Beta]
_ ⊣m (UT_scope) [notation, in :UT_scope:x_'⊣m']
ut_sr_mod.Betas_env_sound2 [lemma, in Betas_env_sound2]
ut_typ_eq_mod.cApp_eqm [constructor, in cApp_eqm]
_ →e _ (UT_scope) [notation, in :UT_scope:x_'→e'_x]
ut_typ_eq_mod.TypeCorrect_Refl [lemma, in TypeCorrect_Refl]
ut_typ_eq_mod.conv_in_env_var_lift [lemma, in conv_in_env_var_lift]
ut_typ_eq_mod.typ_eq_ind' [definition, in typ_eq_ind']
ut_sr_mod.Betas_env_hd [lemma, in Betas_env_hd]
ut_typ_eq_mod.right_reflexivity [lemma, in right_reflexivity]
ut_typ_eq_mod.typm_induc [definition, in typm_induc]
ut_red_mod.PiInj [lemma, in PiInj]
ut_sr_mod.Beta_env_sound_up [lemma, in Beta_env_sound_up]
ut_term_mod.Term [inductive, in Term]
ut_red_mod.Betaps [inductive, in Betaps]
ut_typ_eq_mod.thinning_eq_n [lemma, in thinning_eq_n]
ut_sr_mod.Betas_env_inv [lemma, in Betas_env_inv]
ut_sr_mod.Betas_env_trans [constructor, in Betas_env_trans]
ut_typ_eq_mod.substitution2 [lemma, in substitution2]
ut_typ_eq_mod.substitution [lemma, in substitution]
ut_typ_mod.substitution [lemma, in substitution]
ut_typ_eq_mod.cLa_eqm [constructor, in cLa_eqm]
ut_typ_mod.legacy_var [lemma, in legacy_var]
ut_sr_mod.Betac_env [inductive, in Betac_env]
ut_typ_eq_mod.cVarm [constructor, in cVarm]
ut_red_mod.conv_sort [lemma, in conv_sort]
ut_sr_mod.Betas_env [inductive, in Betas_env]
ut_typ_eq_mod.wfm_cons [constructor, in wfm_cons]
ut_typ_mod.lcApp [constructor, in lcApp]
ut_term_mod.lift_lift [lemma, in lift_lift]
ut_typ_eq_mod.cVar [constructor, in cVar]
ut_typ_mod.cVar [constructor, in cVar]
ut_red_mod.Betas_refl [constructor, in Betas_refl]
ut_red_mod.conv_to_var [lemma, in conv_to_var]
ut_typ_eq_mod.cLa_eq [constructor, in cLa_eq]
ut_red_mod.sub_diamond_Betaps [lemma, in sub_diamond_Betaps]
ut_env_mod.nth_sub_sup [lemma, in nth_sub_sup]
ut_red_mod.Betas_Pi_inv [lemma, in Betas_Pi_inv]
ut_typ_eq_mod.etyp_mtyp [lemma, in etyp_mtyp]
ut_red_mod.Betac_subst [lemma, in Betac_subst]
ut_red_mod.Betac_La [lemma, in Betac_La]
ut_red_mod.Betap_refl [lemma, in Betap_refl]
ut_typ_eq_mod.wgen_pi [lemma, in wgen_pi]
ut_red_mod.Betas_trans [constructor, in Betas_trans]
ut_typ_eq_mod.cSort_eq [constructor, in cSort_eq]
ut_typ_mod.lcSort [constructor, in lcSort]
ut_red_mod.Betas_S [lemma, in Betas_S]
ut_typ_mod.lcWeak [constructor, in lcWeak]
ut_red_mod.Betas_V [lemma, in Betas_V]
ut_red_mod.Betaps_trans [constructor, in Betaps_trans]
ut_typ_eq_mod.wfe_nil [constructor, in wfe_nil]
ut_typ_mod.wf_cons [constructor, in wf_cons]
ut_env_mod.item_trunc [lemma, in item_trunc]
ut_red_mod.Betaps_Betas_closure [lemma, in Betaps_Betas_closure]
_ ⊣ (UT_scope) [notation, in :UT_scope:x_'⊣']
_ →→' _ (UT_scope) [notation, in :UT_scope:x_'→→'''_x]
ut_typ_eq_mod.left_reflexivity [lemma, in left_reflexivity]
ut_typ_eq_mod.wfm [inductive, in wfm]
ut_sr_mod.Betas_env_nil [lemma, in Betas_env_nil]
ut_term_mod.subst_rec [definition, in subst_rec]
ut_env_mod.item_hd [constructor, in item_hd]
_ ↓ _ ∈ _ (UT_scope) [notation, in :UT_scope:x_'↓'_x_'∈'_x]
ut_typ_eq_mod.thinning_eq [lemma, in thinning_eq]
ut_sr_mod.Betas_typ_sound [lemma, in Betas_typ_sound]
ut_sr_mod.Betac_env_Betas [constructor, in Betac_env_Betas]
ut_red_mod.Betac_lift [lemma, in Betac_lift]
ut_red_mod.Beta_lam2 [constructor, in Beta_lam2]
_ ↑ _ # _ (UT_scope) [notation, in :UT_scope:x_'↑'_x_'#'_x]
ut_red_mod.Betac_Pi [lemma, in Betac_Pi]
ut_red_mod.conv_var [lemma, in conv_var]
ut_env_mod.nth_sub_eq [lemma, in nth_sub_eq]
ut_typ_eq_mod.cSort [constructor, in cSort]
ut_typ_mod.cSort [constructor, in cSort]
ut_typ_mod.legacy_extend [lemma, in legacy_extend]
ut_sr_mod.Betas_env_comp [lemma, in Betas_env_comp]
ut_red_mod.Betap_var [constructor, in Betap_var]
ut_typ_mod.legacy_wf [inductive, in legacy_wf]
ut_typ_eq_mod.TypeCorrect [lemma, in TypeCorrect]
ut_typ_mod.TypeCorrect [lemma, in TypeCorrect]
_ →' _ (UT_scope) [notation, in :UT_scope:x_'→'''_x]
_ →' _ (UT_scope) [notation, in :UT_scope:x_'→'''_x]
ut_red_mod.Betap_diamond [lemma, in Betap_diamond]
ut_typ_eq_mod.typ [inductive, in typ]
ut_typ_mod.typ [inductive, in typ]
ut_term_mod.expand_term_with_subst [lemma, in expand_term_with_subst]
ut_sr_mod.Betas_env_cons [lemma, in Betas_env_cons]
_ ⊢e _ : _ (UT_scope) [notation, in :UT_scope:x_'⊢e'_x_':'_x]
ut_red_mod.Betas_La [lemma, in Betas_La]
ut_typ_eq_mod.cSym [constructor, in cSym]
ut_env_mod.ins_in_env [inductive, in ins_in_env]
ut_typ_eq_mod.typ_ind' [definition, in typ_ind']
ut_typ_mod.typ_ind' [definition, in typ_ind']
_ ≡ _ (UT_scope) [notation, in :UT_scope:x_'≡'_x]
_ [ _ ← _ ] (UT_scope) [notation, in :UT_scope:x_'['_x_'←'_x_']']
ut_typ_eq_mod.thinning_n [lemma, in thinning_n]
ut_typ_mod.thinning_n [lemma, in thinning_n]
ut_env_mod.nth_sub_inf [lemma, in nth_sub_inf]
ut_red_mod.conv_to_sort [lemma, in conv_to_sort]
ut_red_mod.Betap_Beta_closure [lemma, in Betap_Beta_closure]
ut_typ_eq_mod.cLa [constructor, in cLa]
ut_typ_mod.cLa [constructor, in cLa]
ut_red_mod.Betac [inductive, in Betac]
ut_typ_eq_mod.cBetam [constructor, in cBetam]
_ ⊢m _ = _ : _ (UT_scope) [notation, in :UT_scope:x_'⊢m'_x_'='_x_':'_x]
ut_typ_eq_mod.Cnvm [constructor, in Cnvm]
# _ (UT_scope) [notation, in :UT_scope:'#'_x]
ut_env_mod.fun_item [lemma, in fun_item]
ut_env_mod.Env [definition, in Env]
ut_red_mod.Betas_Betap_closure [lemma, in Betas_Betap_closure]
ut_red_mod.Betac_Betas [constructor, in Betac_Betas]
ut_red_mod.Betap [inductive, in Betap]
ut_typ_mod.lwf_cons [constructor, in lwf_cons]
ut_red_mod.Betas [inductive, in Betas]
ut_env_mod.ins_item_ge [lemma, in ins_item_ge]
ut_red_mod.Beta_pi [constructor, in Beta_pi]
ut_typ_mod.gen_la [lemma, in gen_la]
ut_red_mod.Beta [inductive, in Beta]
ut_typ_eq_mod.conv_in_env_var2 [lemma, in conv_in_env_var2]
ut_typ_eq_mod.typ_induc [definition, in typ_induc]
ut_typ_mod.typ_induc [definition, in typ_induc]
ut_typ_eq_mod.conv_in_env_var3 [lemma, in conv_in_env_var3]
ut_typ_mod.gen_sort [lemma, in gen_sort]
ut_red_mod.Betas_Pi [lemma, in Betas_Pi]
ut_red_mod.Betas_lift [lemma, in Betas_lift]
ut_typ_eq_mod [module, in ut_typ_eq_mod]
ut_typ_mod.lcLa [constructor, in lcLa]
ut_sr_mod.Beta_env_hd [constructor, in Beta_env_hd]
ut_red_mod.Betap_head [constructor, in Betap_head]
ut_typ_mod.lcVar [constructor, in lcVar]
ut_red_mod.Betaps_refl [constructor, in Betaps_refl]
ut_red_mod.Beta_red1 [constructor, in Beta_red1]
ut_red_mod.Beta_red2 [constructor, in Beta_red2]
ut_term_mod.substP1 [lemma, in substP1]
ut_term_mod.substP2 [lemma, in substP2]
ut_typ_eq_mod.conv_in_env_var_lift2 [lemma, in conv_in_env_var_lift2]
ut_term_mod.substP3 [lemma, in substP3]
ut_typ_eq_mod.conv_in_env_var_lift3 [lemma, in conv_in_env_var_lift3]
ut_term_mod.substP4 [lemma, in substP4]
ut_red_mod.Betap_lift [lemma, in Betap_lift]
ut_typ_eq_mod.Cnv [constructor, in Cnv]
ut_typ_mod.Cnv [constructor, in Cnv]
ut_typ_eq_mod.cPi [constructor, in cPi]
ut_typ_mod.cPi [constructor, in cPi]
ut_typ_mod.wf_nil [constructor, in wf_nil]
ut_sr_mod [module, in ut_sr_mod]
ut_red_mod.Betas_diamond [lemma, in Betas_diamond]
ut_red_mod.Betas_Betaps_closure [lemma, in Betas_Betaps_closure]
ut_term_mod [module, in ut_term_mod]
ut_typ_mod.typ2legacy [lemma, in typ2legacy]
ut_typ_mod.gen_pi [lemma, in gen_pi]
ut_red_mod.Betac_subst2 [lemma, in Betac_subst2]
ut_typ_mod.lCnv [constructor, in lCnv]
ut_term_mod.lift_rec [definition, in lift_rec]
ut_red_mod.Betac_App [lemma, in Betac_App]
ut_typ_eq_mod.wfe_cons [constructor, in wfe_cons]
ut_env_mod.ins_item_lt [lemma, in ins_item_lt]
ut_typ_mod.lcPi [constructor, in lcPi]
_ ≡e _ (UT_scope) [notation, in :UT_scope:x_'≡e'_x]
ut_red_mod.Betas_App [lemma, in Betas_App]
ut_env_mod.item_tl [constructor, in item_tl]
ut_typ_mod.legacy2typ [lemma, in legacy2typ]
ut_typ_mod.gen_app [lemma, in gen_app]
ut_sr_mod.Betas_env_sound [lemma, in Betas_env_sound]
_ ⊢' _ : _ (UT_scope) [notation, in :UT_scope:x_'⊢'''_x_':'_x]
_ ↓ _ ⊂ _ (UT_scope) [notation, in :UT_scope:x_'↓'_x_'⊂'_x]
ut_term_mod.App [constructor, in App]
ut_sr_mod.Betac_env_trans [constructor, in Betac_env_trans]
ut_typ_mod.lwf_nil [constructor, in lwf_nil]
ut_red_mod.Betas_subst [lemma, in Betas_subst]
ut_red_mod.Beta_pi2 [constructor, in Beta_pi2]
ut_term_mod.inv_lift [lemma, in inv_lift]
ut_typ_mod.wf_ltyp [lemma, in wf_ltyp]
ut_typ_eq_mod.cRefl [lemma, in cRefl]
ut_env_mod.item [inductive, in item]
ut_env_mod [module, in ut_env_mod]
ut_typ_eq_mod.conv_in_env [lemma, in conv_in_env]
ut_env_mod.sub_O [constructor, in sub_O]
ut_typ_mod [module, in ut_typ_mod]
_ → _ (UT_scope) [notation, in :UT_scope:x_'→'_x]
ut_env_mod.sub_S [constructor, in sub_S]
ut_red_mod [module, in ut_red_mod]
ut_typ_eq_mod.wf_typ [lemma, in wf_typ]
ut_typ_mod.wf_typ [lemma, in wf_typ]
ut_red_mod.Beta_lam [constructor, in Beta_lam]
ut_typ_eq_mod.conv_in_env_aux_trunc [lemma, in conv_in_env_aux_trunc]
ut_term_mod.liftP1 [lemma, in liftP1]
ut_term_mod.liftP2 [lemma, in liftP2]
ut_term_mod.liftP3 [lemma, in liftP3]
ut_typ_eq_mod.Cnv_eq [constructor, in Cnv_eq]
λ [ _ ] , _ (UT_scope) [notation, in :UT_scope:'λ'_'['_x_']'_','_x]
ut_typ_eq_mod.typ_eqm_ind' [definition, in typ_eqm_ind']
ut_typ_eq_mod.mtyp_etyp [lemma, in mtyp_etyp]
ut_term_mod.lift_rec0 [lemma, in lift_rec0]
_ →→e _ (UT_scope) [notation, in :UT_scope:x_'→→e'_x]
ut_red_mod.Betaps_trans2 [lemma, in Betaps_trans2]
ut_red_mod.Betap_lam [constructor, in Betap_lam]
_ ⊢e _ = _ : _ (UT_scope) [notation, in :UT_scope:x_'⊢e'_x_'='_x_':'_x]
ut_typ_eq_mod.wfm_nil [constructor, in wfm_nil]
ut_typ_eq_mod.cTrans [constructor, in cTrans]
ut_typ_eq_mod.cVar_eq [constructor, in cVar_eq]
ut_typ_eq_mod.TypeCorrect_eq [lemma, in TypeCorrect_eq]
ut_env_mod.trunc_O [constructor, in trunc_O]
ut_sr_mod.Subject_Reduction [lemma, in Subject_Reduction]
ut_sr_mod.Beta_sound [lemma, in Beta_sound]
ut_env_mod.trunc_S [constructor, in trunc_S]
ut_typ_eq_mod.parallel_subst [lemma, in parallel_subst]
ut_term_mod.La [constructor, in La]
ut_typ_eq_mod.conv_in_env_var [lemma, in conv_in_env_var]
ut_red_mod.Betac_trans [constructor, in Betac_trans]
ut_red_mod.Beta_beta [lemma, in Beta_beta]
ut_sr_mod.Beta_env [inductive, in Beta_env]
ut_typ_eq_mod.typ_eq [inductive, in typ_eq]
ut_typ_mod.legacy_typ [inductive, in legacy_typ]
ut_sr_mod.Betas_env_Beta [constructor, in Betas_env_Beta]
ut_typ_eq_mod.FromPTSe_to_PTS [lemma, in FromPTSe_to_PTS]
ut_red_mod.diamond_Betaps [lemma, in diamond_Betaps]
ut_sr [library]
ut_red [library]
ut_typ [library]
ut_term [library]
ut_env [library]
ut_typ_eq [library]
V
Vars [definition, in Vars]Lemma Index
E
env_mod.nth_sub_item_inf [in nth_sub_item_inf]env_mod.gt_O [in gt_O]
env_mod.ins_item_lift_lt [in ins_item_lift_lt]
env_mod.nth_sub_sup [in nth_sub_sup]
env_mod.item_trunc [in item_trunc]
env_mod.nth_sub_eq [in nth_sub_eq]
env_mod.nth_sub_inf [in nth_sub_inf]
env_mod.fun_item [in fun_item]
env_mod.ins_item_ge [in ins_item_ge]
env_mod.ins_item_lt [in ins_item_lt]
F
final_mod.FromPTSATR_to_PTSe_trans [in FromPTSATR_to_PTSe_trans]final_mod.FromPTS_to_PTSATR [in FromPTS_to_PTSATR]
final_mod.strip_var_ [in strip_var_]
final_mod.PTSe_SR_trans [in PTSe_SR_trans]
final_mod.FromPTSATR_to_PTS [in FromPTSATR_to_PTS]
final_mod.strip_var [in strip_var]
final_mod.FromPTSATR_to_PTSe [in FromPTSATR_to_PTSe]
final_mod.PTSe_SR [in PTSe_SR]
final_mod.PTS_equiv_PTSe [in PTS_equiv_PTSe]
f_term_mod.lift0 [in lift0]
f_typ_mod.sub_trunc [in sub_trunc]
f_env_mod.nth_sub_item_inf [in nth_sub_item_inf]
f_term_mod.subst_travers [in subst_travers]
f_typ_mod.wf_item [in wf_item]
f_term_mod.lift_is_lift [in lift_is_lift]
f_typ2_mod.subst_mult_sort [in subst_mult_sort]
f_typ2_mod.subst_mult_prod [in subst_mult_prod]
f_typ2_mod.erasure_injectivity_type [in erasure_injectivity_type]
f_typ2_mod.subst_mult_var_eq [in subst_mult_var_eq]
f_typ_mod.simple2normal [in simple2normal]
f_typ_mod.gen_var [in gen_var]
f_typ_mod.thinning [in thinning]
f_typ2_mod.unique_der_ext [in unique_der_ext]
f_typ2_mod.erasure_injectivity_term_type [in erasure_injectivity_term_type]
f_typ_mod.wf_item_lift [in wf_item_lift]
f_typ2_mod.equality_subst [in equality_subst]
f_equiv_mod.PTSl2PTSF [in PTSl2PTSF]
f_typ2_mod.subst_mult_trunc [in subst_mult_trunc]
f_env_mod.ins_item_lift_lt [in ins_item_lift_lt]
f_term_mod.erasure_lem1 [in erasure_lem1]
f_typ2_mod.erasure_lem2 [in erasure_lem2]
f_term_mod.erasure_lem3 [in erasure_lem3]
f_typ_mod.weakening [in weakening]
f_env_mod.subst_trunc [in subst_trunc]
f_typ2_mod.unique_der [in unique_der]
f_typ_mod.thinning_n_h [in thinning_n_h]
f_typ2_mod.subst_mult_eq [in subst_mult_eq]
f_typ2_mod.erasure_term_type [in erasure_term_type]
f_typ2_mod.subst_mult_var [in subst_mult_var]
f_typ_mod.beta_type_l [in beta_type_l]
f_typ_mod.beta_type_r [in beta_type_r]
f_typ_mod.normal_equiv_simple [in normal_equiv_simple]
f_env_mod.subst_trunc2 [in subst_trunc2]
f_typ_mod.substitution [in substitution]
f_typ2_mod.subst_typR [in subst_typR]
f_typ2_mod.context_conversion [in context_conversion]
f_term_mod.lift_lift [in lift_lift]
f_typ2_mod.der_sound [in der_sound]
f_typ2_mod.subst_wf [in subst_wf]
f_env_mod.nth_sub_sup [in nth_sub_sup]
f_typ_mod.gen_conv [in gen_conv]
f_env_mod.subst_item [in subst_item]
f_env_mod.item_trunc [in item_trunc]
f_typ2_mod.erasure_item_lift_rev [in erasure_item_lift_rev]
f_typ2_mod.erasure_outer_not_conv [in erasure_outer_not_conv]
f_typ2_mod.erasure_term [in erasure_term]
f_typ2_mod.subst_mult_lift_sup [in subst_mult_lift_sup]
f_typ2_mod.subst_mult_var_P2 [in subst_mult_var_P2]
f_typ2_mod.erasure_item_lift [in erasure_item_lift]
f_typ_mod.equality_typing [in equality_typing]
f_equiv_mod.PTSeq2PTSF [in PTSeq2PTSF]
f_term_mod.lift_is_lift_sublemma [in lift_is_lift_sublemma]
f_typ2_mod.context_conversion_context [in context_conversion_context]
f_typ_mod.TypeCorrect [in TypeCorrect]
f_typ_mod.equality_unique [in equality_unique]
f_typ_mod.thinning_h [in thinning_h]
f_env_mod.nth_sub_inf [in nth_sub_inf]
f_typ_mod.thinning_n [in thinning_n]
f_typ2_mod.equality_subst_ext [in equality_subst_ext]
f_env_mod.fun_item [in fun_item]
f_typ2_mod.subst_mult_abs [in subst_mult_abs]
f_env_mod.ins_item [in ins_item]
f_env_mod.ins_item_ge [in ins_item_ge]
f_typ_mod.gen_la [in gen_la]
f_typ2_mod.erasure_equality2 [in erasure_equality2]
f_typ_mod.gen_sort [in gen_sort]
f_env_mod.trunc_trans [in trunc_trans]
f_typ2_mod.subst_mult_lift_inf [in subst_mult_lift_inf]
f_term_mod.substP1 [in substP1]
f_term_mod.substP2 [in substP2]
f_term_mod.substP3 [in substP3]
f_typ2_mod.comp_subst [in comp_subst]
f_term_mod.substP4 [in substP4]
f_typ2_mod.subst_mult_wf [in subst_mult_wf]
f_env_mod.trunc_inj [in trunc_inj]
f_typ2_mod.erasure_item [in erasure_item]
f_typ_mod.gen_pi [in gen_pi]
f_typ_mod.normal2simple [in normal2simple]
f_equiv_mod.PTSlequivPTSF [in PTSlequivPTSF]
f_env_mod.ins_item_lt [in ins_item_lt]
f_typ2_mod.erasure_erasure_outer [in erasure_erasure_outer]
f_typ_mod.gen_app [in gen_app]
f_typ2_mod.subst_mult_cons [in subst_mult_cons]
f_typ_mod.conv_inj [in conv_inj]
f_equiv_mod.Prod_Injective [in Prod_Injective]
f_typ2_mod.subst_mult_conv [in subst_mult_conv]
f_typ2_mod.erasure_outer_typing [in erasure_outer_typing]
f_typ2_mod.erasure_injectivity_term_sort [in erasure_injectivity_term_sort]
f_term_mod.inv_lift [in inv_lift]
f_typ2_mod.der_complete [in der_complete]
f_typ2_mod.erasure_equality [in erasure_equality]
f_typ_mod.wf_typ [in wf_typ]
f_term_mod.liftP1 [in liftP1]
f_term_mod.liftP2 [in liftP2]
f_typ2_mod.type_comparable [in type_comparable]
f_term_mod.liftP3 [in liftP3]
f_typ2_mod.erasure_subst [in erasure_subst]
f_typ2_mod.subst_typ [in subst_typ]
f_term_mod.lift_rec0 [in lift_rec0]
f_typ2_mod.erasure_injectivity_term [in erasure_injectivity_term]
f_term_mod.subst_is_lift [in subst_is_lift]
f_typ2_mod.subst_mult_typ [in subst_mult_typ]
f_typ2_mod.subst_eq [in subst_eq]
f_equiv_mod.PTSF2PTSl [in PTSF2PTSl]
f_typ2_mod.erasure_lift [in erasure_lift]
f_typ2_mod.subst_mult_app [in subst_mult_app]
f_env_mod.ins_trunc [in ins_trunc]
f_typ2_mod.PTSF2PTS [in PTSF2PTS]
G
glue_mod.L43_ [in L43_]glue_mod.ErasedContextSwitch [in ErasedContextSwitch]
glue_mod.L33 [in L33]
glue_mod.ErasedTermConfluence [in ErasedTermConfluence]
glue_mod.weak_type_shape [in weak_type_shape]
glue_mod.L33' [in L33']
glue_mod.peq_not_Pi_sort [in peq_not_Pi_sort]
glue_mod.ErasedTypeConversion [in ErasedTypeConversion]
P
PTS_ATR_mod.wf_from_peq [in wf_from_peq]PTS_ATR_mod.env_conv_cons [in env_conv_cons]
PTS_ATR_mod.sub_trunc [in sub_trunc]
PTS_ATR_mod.wf_item [in wf_item]
PTS_ATR_mod.ConvSort [in ConvSort]
PTS_ATR_mod.OSDiamond [in OSDiamond]
PTS_ATR_mod.reds_refl_rt [in reds_refl_rt]
PTS_ATR_mod.SR [in SR]
PTS_ATR_mod.typ_peq_sym [in typ_peq_sym]
PTS_ATR_mod.reds_subst [in reds_subst]
PTS_ATR_mod.thinning [in thinning]
PTS_ATR_mod.wf_item_lift [in wf_item_lift]
PTS_ATR_mod.fun_item_lift [in fun_item_lift]
PTS_ATR_mod.typ_reds_trans2 [in typ_reds_trans2]
PTS_ATR_mod.conv_in_env_reds [in conv_in_env_reds]
PTS_ATR_mod.weakening [in weakening]
PTS_ATR_mod.wf_from_typ_reds [in wf_from_typ_reds]
PTS_ATR_mod.pgen_app [in pgen_app]
PTS_ATR_mod.red1_in_env [in red1_in_env]
PTS_ATR_mod.reds_App___ [in reds_App___]
PTS_ATR_mod.Sort_Reds [in Sort_Reds]
PTS_ATR_mod.reds_App_ [in reds_App_]
PTS_ATR_mod.SR_trans [in SR_trans]
PTS_ATR_mod.typ_reds_trans_ [in typ_reds_trans_]
PTS_ATR_mod.peq_subst [in peq_subst]
PTS_ATR_mod.conv1_in_env [in conv1_in_env]
PTS_ATR_mod.red_refl_lt [in red_refl_lt]
PTS_ATR_mod.typ_pcompat [in typ_pcompat]
PTS_ATR_mod.PiInj [in PiInj]
PTS_ATR_mod.reds_subst_gen [in reds_subst_gen]
PTS_ATR_mod.conv_in_env_peq [in conv_in_env_peq]
PTS_ATR_mod.typ_exp_trans [in typ_exp_trans]
PTS_ATR_mod.pgen_la [in pgen_la]
PTS_ATR_mod.peq_thinning [in peq_thinning]
PTS_ATR_mod.typ_reds_relocate [in typ_reds_relocate]
PTS_ATR_mod.reds_App__ [in reds_App__]
PTS_ATR_mod.wf_from_typ [in wf_from_typ]
PTS_ATR_mod.typ_wf [in typ_wf]
PTS_ATR_mod.red_refl_rt [in red_refl_rt]
PTS_ATR_mod.env_red_to_conv [in env_red_to_conv]
PTS_ATR_mod.env_red_cons [in env_red_cons]
PTS_ATR_mod.typ_reds_to_red_ [in typ_reds_to_red_]
PTS_ATR_mod.subst_gen [in subst_gen]
PTS_ATR_mod.pgen_pi [in pgen_pi]
PTS_ATR_mod.relocate [in relocate]
PTS_ATR_mod.reds_Pi_ [in reds_Pi_]
PTS_ATR_mod.SubDiam [in SubDiam]
PTS_ATR_mod.pgen_var [in pgen_var]
PTS_ATR_mod.reds_La [in reds_La]
PTS_ATR_mod.ChurchRosser [in ChurchRosser]
PTS_ATR_mod.SR_trans' [in SR_trans']
PTS_ATR_mod.thinning_n [in thinning_n]
PTS_ATR_mod.typ_ind2 [in typ_ind2]
PTS_ATR_mod.La_Reds [in La_Reds]
PTS_ATR_mod.pgen_sort [in pgen_sort]
PTS_ATR_mod.c_sym [in c_sym]
PTS_ATR_mod.reds_Pi [in reds_Pi]
PTS_ATR_mod.env_conv1_wf [in env_conv1_wf]
PTS_ATR_mod.env_conv_wf [in env_conv_wf]
PTS_ATR_mod.thinning_reds_n [in thinning_reds_n]
PTS_ATR_mod.peq_thinning_n [in peq_thinning_n]
PTS_ATR_mod.typ_peq_to_red [in typ_peq_to_red]
PTS_ATR_mod.Confluence [in Confluence]
PTS_ATR_mod.red_in_env [in red_in_env]
PTS_ATR_mod.env_red1_wf [in env_red1_wf]
PTS_ATR_mod.conv_item [in conv_item]
PTS_ATR_mod.reds_typ_pcompat [in reds_typ_pcompat]
PTS_ATR_mod.red_in_env_reds [in red_in_env_reds]
PTS_ATR_mod.c1_sym [in c1_sym]
PTS_ATR_mod.env_red1_to_conv1 [in env_red1_to_conv1]
PTS_ATR_mod.Pi_Reds [in Pi_Reds]
PTS_ATR_mod.thinning_reds [in thinning_reds]
PTS_ATR_mod.reds_App [in reds_App]
PTS_ATR_mod.eq_subst_gen [in eq_subst_gen]
PTS_ATR_mod.env_red_wf [in env_red_wf]
PTS_ATR_mod.red_item [in red_item]
PTS_ATR_mod.conv_in_env [in conv_in_env]
PTS_ATR_mod.sub_in_env_item [in sub_in_env_item]
PTS_ATR_mod.typ_red_trans [in typ_red_trans]
PTS_ATR_mod.reds_refl_lt [in reds_refl_lt]
PTS_ATR_mod.reds_to_conv [in reds_to_conv]
R
red_mod.Betaps_to_Betas [in Betaps_to_Betas]red_mod.Betaps_Beta_closure [in Betaps_Beta_closure]
red_mod.Betap_to_Betas [in Betap_to_Betas]
red_mod.Betap_refl [in Betap_refl]
red_mod.Betaps_Betas_closure [in Betaps_Betas_closure]
red_mod.Betas_La [in Betas_La]
red_mod.Betas_Pi [in Betas_Pi]
red_mod.Betas_App [in Betas_App]
S
strip_mod.strip_lift [in strip_lift]strip_mod.strip_subst [in strip_subst]
T
term_mod.lift0 [in lift0]term_mod.subst_travers [in subst_travers]
term_mod.lift_lift [in lift_lift]
term_mod.expand_term_with_subst [in expand_term_with_subst]
term_mod.substP1 [in substP1]
term_mod.substP2 [in substP2]
term_mod.substP3 [in substP3]
term_mod.substP4 [in substP4]
term_mod.inv_lift [in inv_lift]
term_mod.liftP1 [in liftP1]
term_mod.liftP2 [in liftP2]
term_mod.liftP3 [in liftP3]
term_mod.lift_rec0 [in lift_rec0]
U
ut_term_mod.lift0 [in lift0]ut_sr_mod.Betas_env_nil2 [in Betas_env_nil2]
ut_red_mod.Betac_confl [in Betac_confl]
ut_sr_mod.SubjectRed [in SubjectRed]
ut_typ_mod.sub_trunc [in sub_trunc]
ut_red_mod.Betaps_Beta_closure [in Betaps_Beta_closure]
ut_env_mod.nth_sub_item_inf [in nth_sub_item_inf]
ut_term_mod.subst_travers [in subst_travers]
ut_typ_eq_mod.wf_item [in wf_item]
ut_typ_mod.wf_item [in wf_item]
ut_red_mod.Beta_lift [in Beta_lift]
ut_typ_mod.gen_var [in gen_var]
ut_red_mod.Betas_subst2 [in Betas_subst2]
ut_sr_mod.Beta_env_sound [in Beta_env_sound]
ut_typ_eq_mod.thinning [in thinning]
ut_typ_mod.thinning [in thinning]
ut_red_mod.Betac_not_Pi_sort [in Betac_not_Pi_sort]
ut_typ_eq_mod.wf_item_lift [in wf_item_lift]
ut_typ_mod.wf_item_lift [in wf_item_lift]
ut_sr_mod.Betas_env_sound_up [in Betas_env_sound_up]
ut_env_mod.gt_O [in gt_O]
ut_typ_eq_mod.wf_typ_eq [in wf_typ_eq]
ut_env_mod.ins_item_lift_lt [in ins_item_lift_lt]
ut_red_mod.Betap_subst [in Betap_subst]
ut_red_mod.Betac_refl [in Betac_refl]
ut_sr_mod.Beta_env_sound2 [in Beta_env_sound2]
ut_typ_eq_mod.weakening [in weakening]
ut_typ_mod.weakening [in weakening]
ut_sr_mod.Betas_env_sound2 [in Betas_env_sound2]
ut_typ_eq_mod.TypeCorrect_Refl [in TypeCorrect_Refl]
ut_typ_eq_mod.conv_in_env_var_lift [in conv_in_env_var_lift]
ut_sr_mod.Betas_env_hd [in Betas_env_hd]
ut_typ_eq_mod.right_reflexivity [in right_reflexivity]
ut_red_mod.PiInj [in PiInj]
ut_sr_mod.Beta_env_sound_up [in Beta_env_sound_up]
ut_typ_eq_mod.thinning_eq_n [in thinning_eq_n]
ut_sr_mod.Betas_env_inv [in Betas_env_inv]
ut_typ_eq_mod.substitution2 [in substitution2]
ut_typ_eq_mod.substitution [in substitution]
ut_typ_mod.substitution [in substitution]
ut_typ_mod.legacy_var [in legacy_var]
ut_red_mod.conv_sort [in conv_sort]
ut_term_mod.lift_lift [in lift_lift]
ut_red_mod.conv_to_var [in conv_to_var]
ut_red_mod.sub_diamond_Betaps [in sub_diamond_Betaps]
ut_env_mod.nth_sub_sup [in nth_sub_sup]
ut_red_mod.Betas_Pi_inv [in Betas_Pi_inv]
ut_typ_eq_mod.etyp_mtyp [in etyp_mtyp]
ut_red_mod.Betac_subst [in Betac_subst]
ut_red_mod.Betac_La [in Betac_La]
ut_red_mod.Betap_refl [in Betap_refl]
ut_typ_eq_mod.wgen_pi [in wgen_pi]
ut_red_mod.Betas_S [in Betas_S]
ut_red_mod.Betas_V [in Betas_V]
ut_env_mod.item_trunc [in item_trunc]
ut_red_mod.Betaps_Betas_closure [in Betaps_Betas_closure]
ut_typ_eq_mod.left_reflexivity [in left_reflexivity]
ut_sr_mod.Betas_env_nil [in Betas_env_nil]
ut_typ_eq_mod.thinning_eq [in thinning_eq]
ut_sr_mod.Betas_typ_sound [in Betas_typ_sound]
ut_red_mod.Betac_lift [in Betac_lift]
ut_red_mod.Betac_Pi [in Betac_Pi]
ut_red_mod.conv_var [in conv_var]
ut_env_mod.nth_sub_eq [in nth_sub_eq]
ut_typ_mod.legacy_extend [in legacy_extend]
ut_sr_mod.Betas_env_comp [in Betas_env_comp]
ut_typ_eq_mod.TypeCorrect [in TypeCorrect]
ut_typ_mod.TypeCorrect [in TypeCorrect]
ut_red_mod.Betap_diamond [in Betap_diamond]
ut_term_mod.expand_term_with_subst [in expand_term_with_subst]
ut_sr_mod.Betas_env_cons [in Betas_env_cons]
ut_red_mod.Betas_La [in Betas_La]
ut_typ_eq_mod.thinning_n [in thinning_n]
ut_typ_mod.thinning_n [in thinning_n]
ut_env_mod.nth_sub_inf [in nth_sub_inf]
ut_red_mod.conv_to_sort [in conv_to_sort]
ut_red_mod.Betap_Beta_closure [in Betap_Beta_closure]
ut_env_mod.fun_item [in fun_item]
ut_red_mod.Betas_Betap_closure [in Betas_Betap_closure]
ut_env_mod.ins_item_ge [in ins_item_ge]
ut_typ_mod.gen_la [in gen_la]
ut_typ_eq_mod.conv_in_env_var2 [in conv_in_env_var2]
ut_typ_eq_mod.conv_in_env_var3 [in conv_in_env_var3]
ut_typ_mod.gen_sort [in gen_sort]
ut_red_mod.Betas_Pi [in Betas_Pi]
ut_red_mod.Betas_lift [in Betas_lift]
ut_term_mod.substP1 [in substP1]
ut_term_mod.substP2 [in substP2]
ut_typ_eq_mod.conv_in_env_var_lift2 [in conv_in_env_var_lift2]
ut_term_mod.substP3 [in substP3]
ut_typ_eq_mod.conv_in_env_var_lift3 [in conv_in_env_var_lift3]
ut_term_mod.substP4 [in substP4]
ut_red_mod.Betap_lift [in Betap_lift]
ut_red_mod.Betas_diamond [in Betas_diamond]
ut_red_mod.Betas_Betaps_closure [in Betas_Betaps_closure]
ut_typ_mod.typ2legacy [in typ2legacy]
ut_typ_mod.gen_pi [in gen_pi]
ut_red_mod.Betac_subst2 [in Betac_subst2]
ut_red_mod.Betac_App [in Betac_App]
ut_env_mod.ins_item_lt [in ins_item_lt]
ut_red_mod.Betas_App [in Betas_App]
ut_typ_mod.legacy2typ [in legacy2typ]
ut_typ_mod.gen_app [in gen_app]
ut_sr_mod.Betas_env_sound [in Betas_env_sound]
ut_red_mod.Betas_subst [in Betas_subst]
ut_term_mod.inv_lift [in inv_lift]
ut_typ_mod.wf_ltyp [in wf_ltyp]
ut_typ_eq_mod.cRefl [in cRefl]
ut_typ_eq_mod.conv_in_env [in conv_in_env]
ut_typ_eq_mod.wf_typ [in wf_typ]
ut_typ_mod.wf_typ [in wf_typ]
ut_typ_eq_mod.conv_in_env_aux_trunc [in conv_in_env_aux_trunc]
ut_term_mod.liftP1 [in liftP1]
ut_term_mod.liftP2 [in liftP2]
ut_term_mod.liftP3 [in liftP3]
ut_typ_eq_mod.mtyp_etyp [in mtyp_etyp]
ut_term_mod.lift_rec0 [in lift_rec0]
ut_red_mod.Betaps_trans2 [in Betaps_trans2]
ut_typ_eq_mod.TypeCorrect_eq [in TypeCorrect_eq]
ut_sr_mod.Subject_Reduction [in Subject_Reduction]
ut_sr_mod.Beta_sound [in Beta_sound]
ut_typ_eq_mod.parallel_subst [in parallel_subst]
ut_typ_eq_mod.conv_in_env_var [in conv_in_env_var]
ut_red_mod.Beta_beta [in Beta_beta]
ut_typ_eq_mod.FromPTSe_to_PTS [in FromPTSe_to_PTS]
ut_red_mod.diamond_Betaps [in diamond_Betaps]
Notation Index
E
_ ↓ _ ∈ _ (Typ_scope) [in :Typ_scope:x_'↓'_x_'∈'_x]_ ↓ _ ⊂ _ (Typ_scope) [in :Typ_scope:x_'↓'_x_'⊂'_x]
F
β _ (F_scope) [in :F_scope:'β'_x]_ [ _ ←h _ ] (F_scope) [in :F_scope:x_'['_x_'←h'_x_']']
εc _ (F_scope) [in :F_scope:'εc'_x]
_ ↓ _ ∈ _ (F_scope) [in :F_scope:x_'↓'_x_'∈'_x]
_ ⊢ _ : _ : _ [in ::x_'⊢'_x_':'_x_':'_x]
_ † (F_scope) [in :F_scope:x_'†']
_ ⊢ _ : _ (F_scope) [in :F_scope:x_'⊢'_x_':'_x]
_ ⊢' _ : _ (F_scope) [in :F_scope:x_'⊢'''_x_':'_x]
_ ↑h _ (F_scope) [in :F_scope:x_'↑h'_x]
ρ _ (F_scope) [in :F_scope:'ρ'_x]
ε _ (F_scope) [in :F_scope:'ε'_x]
ι _ (F_scope) [in :F_scope:'ι'_x]
_ ↓ _ ⊂ _ (F_scope) [in :F_scope:x_'↓'_x_'⊂'_x]
! _ (F_scope) [in :F_scope:'!'_x]
_ ⊣' (F_scope) [in :F_scope:x_'⊣''']
_ ·h _ (F_scope) [in :F_scope:x_'·h'_x]
_ ↑ _ # _ (F_scope) [in :F_scope:x_'↑'_x_'#'_x]
_ ↑h _ # _ (F_scope) [in :F_scope:x_'↑h'_x_'#'_x]
_ [ _ ← _ ] (F_scope) [in :F_scope:x_'['_x_'←'_x_']']
_ ↑ _ (F_scope) [in :F_scope:x_'↑'_x]
λ [ _ ] , _ (F_scope) [in :F_scope:'λ'_'['_x_']'_','_x]
_ [ ← _ ] (F_scope) [in :F_scope:x_'['_'←'_x_']']
⟨ _ , [ _ ] _ ⟩ (F_scope) [in :F_scope:'⟨'_x_','_'['_x_']'_x_'⟩']
{ _ , [ _ ] _ } (F_scope) [in :F_scope:'{'_x_','_'['_x_']'_x_'}']
_ · _ (F_scope) [in :F_scope:x_'·'_x]
_ [ ←h _ ] (F_scope) [in :F_scope:x_'['_'←h'_x_']']
_ • _ (F_scope) [in :F_scope:x_'•'_x]
_ ⊢ _ : _ = _ (F_scope) [in :F_scope:x_'⊢'_x_':'_x_'='_x]
_ ∽ _ (F_scope) [in :F_scope:x_'∽'_x]
_ ⊣ (F_scope) [in :F_scope:x_'⊣']
_ ⊢' _ : _ = _ (F_scope) [in :F_scope:x_'⊢'''_x_':'_x_'='_x]
Π ( _ ) , _ (F_scope) [in :F_scope:'Π'_'('_x_')'_','_x]
# _ (F_scope) [in :F_scope:'#'_x]
_ ⊢ _ = _ [in ::x_'⊢'_x_'='_x]
P
_ ⊢ _ ▹▹ _ : _ (Typ_scope) [in :Typ_scope:x_'⊢'_x_'▹▹'_x_':'_x]_ ⊢ _ ▹ _ : _ (Typ_scope) [in :Typ_scope:x_'⊢'_x_'▹'_x_':'_x]
_ ⊣ (Typ_scope) [in :Typ_scope:x_'⊣']
_ ⊢ _ ≡' _ (Typ_scope) [in :Typ_scope:x_'⊢'_x_'≡'''_x]
R
_ → _ (Typ_scope) [in :Typ_scope:x_'→'_x]_ →' _ (Typ_scope) [in :Typ_scope:x_'→'''_x]
_ →→ _ (Typ_scope) [in :Typ_scope:x_'→→'_x]
_ →→' _ (Typ_scope) [in :Typ_scope:x_'→→'''_x]
T
Π ( _ ) , _ (Typ_scope) [in :Typ_scope:'Π'_'('_x_')'_','_x]# _ (Typ_scope) [in :Typ_scope:'#'_x]
_ ↑ _ (Typ_scope) [in :Typ_scope:x_'↑'_x]
! _ (Typ_scope) [in :Typ_scope:'!'_x]
_ [ ← _ ] (Typ_scope) [in :Typ_scope:x_'['_'←'_x_']']
_ [ _ ← _ ] (Typ_scope) [in :Typ_scope:x_'['_x_'←'_x_']']
_ ·( _ , _ ) _ (Typ_scope) [in :Typ_scope:x_'·('_x_','_x_')'_x]
λ [ _ ] , _ (Typ_scope) [in :Typ_scope:'λ'_'['_x_']'_','_x]
_ ↑ _ # _ (Typ_scope) [in :Typ_scope:x_'↑'_x_'#'_x]
U
_ · _ (UT_scope) [in :UT_scope:x_'·'_x]_ ⊣e (UT_scope) [in :UT_scope:x_'⊣e']
_ [ ← _ ] (UT_scope) [in :UT_scope:x_'['_'←'_x_']']
_ ⊣' (UT_scope) [in :UT_scope:x_'⊣''']
_ →→ _ (UT_scope) [in :UT_scope:x_'→→'_x]
! _ (UT_scope) [in :UT_scope:'!'_x]
_ ↑ _ (UT_scope) [in :UT_scope:x_'↑'_x]
_ ⊢ _ : _ (UT_scope) [in :UT_scope:x_'⊢'_x_':'_x]
Π ( _ ) , _ (UT_scope) [in :UT_scope:'Π'_'('_x_')'_','_x]
_ ⊣m (UT_scope) [in :UT_scope:x_'⊣m']
_ →e _ (UT_scope) [in :UT_scope:x_'→e'_x]
_ ⊣ (UT_scope) [in :UT_scope:x_'⊣']
_ →→' _ (UT_scope) [in :UT_scope:x_'→→'''_x]
_ ↓ _ ∈ _ (UT_scope) [in :UT_scope:x_'↓'_x_'∈'_x]
_ ↑ _ # _ (UT_scope) [in :UT_scope:x_'↑'_x_'#'_x]
_ →' _ (UT_scope) [in :UT_scope:x_'→'''_x]
_ →' _ (UT_scope) [in :UT_scope:x_'→'''_x]
_ ⊢e _ : _ (UT_scope) [in :UT_scope:x_'⊢e'_x_':'_x]
_ ≡ _ (UT_scope) [in :UT_scope:x_'≡'_x]
_ [ _ ← _ ] (UT_scope) [in :UT_scope:x_'['_x_'←'_x_']']
_ ⊢m _ = _ : _ (UT_scope) [in :UT_scope:x_'⊢m'_x_'='_x_':'_x]
# _ (UT_scope) [in :UT_scope:'#'_x]
_ ≡e _ (UT_scope) [in :UT_scope:x_'≡e'_x]
_ ⊢' _ : _ (UT_scope) [in :UT_scope:x_'⊢'''_x_':'_x]
_ ↓ _ ⊂ _ (UT_scope) [in :UT_scope:x_'↓'_x_'⊂'_x]
_ → _ (UT_scope) [in :UT_scope:x_'→'_x]
λ [ _ ] , _ (UT_scope) [in :UT_scope:'λ'_'['_x_']'_','_x]
_ →→e _ (UT_scope) [in :UT_scope:x_'→→e'_x]
_ ⊢e _ = _ : _ (UT_scope) [in :UT_scope:x_'⊢e'_x_'='_x_':'_x]
Constructor Index
E
env_mod.ins_O [in ins_O]env_mod.ins_S [in ins_S]
env_mod.item_hd [in item_hd]
env_mod.item_tl [in item_tl]
env_mod.sub_O [in sub_O]
env_mod.sub_S [in sub_S]
env_mod.trunc_O [in trunc_O]
env_mod.trunc_S [in trunc_S]
F
f_env_mod.ins_O [in ins_O]f_env_mod.ins_S [in ins_S]
f_typ_mod.cBeta [in cBeta]
f_typ_mod.cAppEq [in cAppEq]
f_typ2_mod.dcons [in dcons]
f_typ_mod.lcAbs [in lcAbs]
f_term_mod.AppEq [in AppEq]
f_typ_mod.cApp [in cApp]
f_term_mod.ProdEq [in ProdEq]
f_typ2_mod.msub_O [in msub_O]
f_typ2_mod.dAbsEq [in dAbsEq]
f_typ2_mod.msub_S [in msub_S]
f_typ2_mod.dVar [in dVar]
f_term_mod.Var [in Var]
f_term_mod.Sort [in Sort]
f_term_mod.Prod [in Prod]
f_typ_mod.lcConv [in lcConv]
f_typ2_mod.comp_sort [in comp_sort]
f_typ2_mod.dTrans [in dTrans]
f_typ_mod.cConv [in cConv]
f_typ2_mod.comp_prod [in comp_prod]
f_typ2_mod.dRefl [in dRefl]
f_typ2_mod.node [in node]
f_typ2_mod.dSym [in dSym]
f_term_mod.Sym [in Sym]
f_typ2_mod.dAppEq [in dAppEq]
f_typ_mod.lcApp [in lcApp]
f_typ_mod.cVar [in cVar]
f_typ2_mod.dnil [in dnil]
f_typ2_mod.dIota [in dIota]
f_typ_mod.lcSort [in lcSort]
f_typ_mod.lcProd [in lcProd]
f_typ_mod.wf_cons [in wf_cons]
f_typ2_mod.dBeta [in dBeta]
f_typ2_mod.dAbs [in dAbs]
f_term_mod.Refl [in Refl]
f_env_mod.item_hd [in item_hd]
f_term_mod.Abs [in Abs]
f_typ_mod.cSort [in cSort]
f_typ_mod.cProd [in cProd]
f_typ_mod.cSym [in cSym]
f_term_mod.Iota [in Iota]
f_typ2_mod.comp_refl [in comp_refl]
f_typ_mod.lwf_cons [in lwf_cons]
f_term_mod.Beta [in Beta]
f_typ_mod.lcAbsEq [in lcAbsEq]
f_typ_mod.lcVar [in lcVar]
f_typ_mod.cProdEq [in cProdEq]
f_typ2_mod.dConv [in dConv]
f_typ_mod.cAbs [in cAbs]
f_typ_mod.wf_nil [in wf_nil]
f_typ_mod.lcRefl [in lcRefl]
f_typ_mod.cAbsEq [in cAbsEq]
f_term_mod.AbsEq [in AbsEq]
f_env_mod.item_tl [in item_tl]
f_typ2_mod.dApp [in dApp]
f_term_mod.App [in App]
f_typ_mod.lwf_nil [in lwf_nil]
f_typ2_mod.dProdEq [in dProdEq]
f_typ_mod.lcIota [in lcIota]
f_typ_mod.lcTrans [in lcTrans]
f_typ_mod.cRefl [in cRefl]
f_env_mod.sub_O [in sub_O]
f_env_mod.sub_S [in sub_S]
f_typ_mod.lcSym [in lcSym]
f_typ_mod.lcProdEq [in lcProdEq]
f_term_mod.Conv [in Conv]
f_typ_mod.lcBeta [in lcBeta]
f_typ_mod.lcAppEq [in lcAppEq]
f_typ_mod.cTrans [in cTrans]
f_typ_mod.cIota [in cIota]
f_env_mod.trunc_O [in trunc_O]
f_term_mod.Trans [in Trans]
f_env_mod.trunc_S [in trunc_S]
f_typ2_mod.dSort [in dSort]
f_typ2_mod.dProd [in dProd]
P
PTS_ATR_mod.c_step [in c_step]PTS_ATR_mod.typ_sort [in typ_sort]
PTS_ATR_mod.typ_la [in typ_la]
PTS_ATR_mod.typ_app [in typ_app]
PTS_ATR_mod.typ_exp [in typ_exp]
PTS_ATR_mod.typ_pi [in typ_pi]
PTS_ATR_mod.r_refl [in r_refl]
PTS_ATR_mod.red1_next [in red1_next]
PTS_ATR_mod.typ_reds_intro [in typ_reds_intro]
PTS_ATR_mod.typ_reds_trans [in typ_reds_trans]
PTS_ATR_mod.c_trans [in c_trans]
PTS_ATR_mod.c_refl [in c_refl]
PTS_ATR_mod.wf_cons [in wf_cons]
PTS_ATR_mod.typ_var [in typ_var]
PTS_ATR_mod.typ_peq_intro [in typ_peq_intro]
PTS_ATR_mod.typ_peq_trans [in typ_peq_trans]
PTS_ATR_mod.typ_beta [in typ_beta]
PTS_ATR_mod.typ_peq_intro2 [in typ_peq_intro2]
PTS_ATR_mod.r_trans [in r_trans]
PTS_ATR_mod.typ_red [in typ_red]
PTS_ATR_mod.wf_nil [in wf_nil]
PTS_ATR_mod.conv1_intro [in conv1_intro]
PTS_ATR_mod.red1_intro [in red1_intro]
PTS_ATR_mod.r_step [in r_step]
PTS_ATR_mod.conv1_next [in conv1_next]
R
red_mod.Betap_sort [in Betap_sort]red_mod.Beta_head [in Beta_head]
red_mod.Betap_pi [in Betap_pi]
red_mod.Betas_Beta [in Betas_Beta]
red_mod.Betas_refl [in Betas_refl]
red_mod.Betas_trans [in Betas_trans]
red_mod.Betaps_intro [in Betaps_intro]
red_mod.Betaps_trans [in Betaps_trans]
red_mod.Betap_App [in Betap_App]
red_mod.Beta_lam2 [in Beta_lam2]
red_mod.Betap_var [in Betap_var]
red_mod.Beta_pi [in Beta_pi]
red_mod.Betap_head [in Betap_head]
red_mod.Beta_red1 [in Beta_red1]
red_mod.Beta_red2 [in Beta_red2]
red_mod.Beta_red3 [in Beta_red3]
red_mod.Beta_red4 [in Beta_red4]
red_mod.Beta_pi2 [in Beta_pi2]
red_mod.Beta_lam [in Beta_lam]
red_mod.Betap_lam [in Betap_lam]
T
term_mod.Pi [in Pi]term_mod.Var [in Var]
term_mod.Sort [in Sort]
term_mod.App [in App]
term_mod.La [in La]
U
ut_typ_eq_mod.cSymm [in cSymm]ut_env_mod.ins_O [in ins_O]
ut_env_mod.ins_S [in ins_S]
ut_typ_eq_mod.cBeta [in cBeta]
ut_red_mod.Betac_sym [in Betac_sym]
ut_typ_eq_mod.cApp [in cApp]
ut_typ_mod.cApp [in cApp]
ut_term_mod.Pi [in Pi]
ut_red_mod.Betap_sort [in Betap_sort]
ut_typ_eq_mod.cTransm [in cTransm]
ut_red_mod.Beta_head [in Beta_head]
ut_typ_eq_mod.cPi_eqm [in cPi_eqm]
ut_sr_mod.Beta_env_cons [in Beta_env_cons]
ut_sr_mod.Betas_env_refl [in Betas_env_refl]
ut_term_mod.Var [in Var]
ut_term_mod.Sort [in Sort]
ut_red_mod.Betap_pi [in Betap_pi]
ut_sr_mod.Betac_env_sym [in Betac_env_sym]
ut_typ_eq_mod.cSortm [in cSortm]
ut_typ_eq_mod.cPi_eq [in cPi_eq]
ut_typ_eq_mod.cApp_eq [in cApp_eq]
ut_red_mod.Betap_app [in Betap_app]
ut_red_mod.Betas_Beta [in Betas_Beta]
ut_typ_eq_mod.cApp_eqm [in cApp_eqm]
ut_sr_mod.Betas_env_trans [in Betas_env_trans]
ut_typ_eq_mod.cLa_eqm [in cLa_eqm]
ut_typ_eq_mod.cVarm [in cVarm]
ut_typ_eq_mod.wfm_cons [in wfm_cons]
ut_typ_mod.lcApp [in lcApp]
ut_typ_eq_mod.cVar [in cVar]
ut_typ_mod.cVar [in cVar]
ut_red_mod.Betas_refl [in Betas_refl]
ut_typ_eq_mod.cLa_eq [in cLa_eq]
ut_red_mod.Betas_trans [in Betas_trans]
ut_typ_eq_mod.cSort_eq [in cSort_eq]
ut_typ_mod.lcSort [in lcSort]
ut_typ_mod.lcWeak [in lcWeak]
ut_red_mod.Betaps_trans [in Betaps_trans]
ut_typ_eq_mod.wfe_nil [in wfe_nil]
ut_typ_mod.wf_cons [in wf_cons]
ut_env_mod.item_hd [in item_hd]
ut_sr_mod.Betac_env_Betas [in Betac_env_Betas]
ut_red_mod.Beta_lam2 [in Beta_lam2]
ut_typ_eq_mod.cSort [in cSort]
ut_typ_mod.cSort [in cSort]
ut_red_mod.Betap_var [in Betap_var]
ut_typ_eq_mod.cSym [in cSym]
ut_typ_eq_mod.cLa [in cLa]
ut_typ_mod.cLa [in cLa]
ut_typ_eq_mod.cBetam [in cBetam]
ut_typ_eq_mod.Cnvm [in Cnvm]
ut_red_mod.Betac_Betas [in Betac_Betas]
ut_typ_mod.lwf_cons [in lwf_cons]
ut_red_mod.Beta_pi [in Beta_pi]
ut_typ_mod.lcLa [in lcLa]
ut_sr_mod.Beta_env_hd [in Beta_env_hd]
ut_red_mod.Betap_head [in Betap_head]
ut_typ_mod.lcVar [in lcVar]
ut_red_mod.Betaps_refl [in Betaps_refl]
ut_red_mod.Beta_red1 [in Beta_red1]
ut_red_mod.Beta_red2 [in Beta_red2]
ut_typ_eq_mod.Cnv [in Cnv]
ut_typ_mod.Cnv [in Cnv]
ut_typ_eq_mod.cPi [in cPi]
ut_typ_mod.cPi [in cPi]
ut_typ_mod.wf_nil [in wf_nil]
ut_typ_mod.lCnv [in lCnv]
ut_typ_eq_mod.wfe_cons [in wfe_cons]
ut_typ_mod.lcPi [in lcPi]
ut_env_mod.item_tl [in item_tl]
ut_term_mod.App [in App]
ut_sr_mod.Betac_env_trans [in Betac_env_trans]
ut_typ_mod.lwf_nil [in lwf_nil]
ut_red_mod.Beta_pi2 [in Beta_pi2]
ut_env_mod.sub_O [in sub_O]
ut_env_mod.sub_S [in sub_S]
ut_red_mod.Beta_lam [in Beta_lam]
ut_typ_eq_mod.Cnv_eq [in Cnv_eq]
ut_red_mod.Betap_lam [in Betap_lam]
ut_typ_eq_mod.wfm_nil [in wfm_nil]
ut_typ_eq_mod.cTrans [in cTrans]
ut_typ_eq_mod.cVar_eq [in cVar_eq]
ut_env_mod.trunc_O [in trunc_O]
ut_env_mod.trunc_S [in trunc_S]
ut_term_mod.La [in La]
ut_red_mod.Betac_trans [in Betac_trans]
ut_sr_mod.Betas_env_Beta [in Betas_env_Beta]
Inductive Index
E
env_mod.sub_in_env [in sub_in_env]env_mod.trunc [in trunc]
env_mod.ins_in_env [in ins_in_env]
env_mod.item [in item]
F
f_typ2_mod.der_wf [in der_wf]f_typ_mod.wf [in wf]
f_typ_mod.simple_wf [in simple_wf]
f_typ2_mod.der_typ [in der_typ]
f_env_mod.sub_in_env [in sub_in_env]
f_env_mod.trunc [in trunc]
f_term_mod.Term [in Term]
f_typ2_mod.comparable [in comparable]
f_typ2_mod.der_h [in der_h]
f_typ_mod.typ [in typ]
f_env_mod.ins_in_env [in ins_in_env]
f_typ_mod.simple_typ [in simple_typ]
f_term_mod.Prf [in Prf]
f_typ2_mod.subst_mult_env [in subst_mult_env]
f_typ2_mod.deriv [in deriv]
f_typ_mod.simple_typ_h [in simple_typ_h]
f_typ_mod.typ_h [in typ_h]
f_env_mod.item [in item]
P
PTS_ATR_mod.wf [in wf]PTS_ATR_mod.env_red1 [in env_red1]
PTS_ATR_mod.typ_reds [in typ_reds]
PTS_ATR_mod.env_red [in env_red]
PTS_ATR_mod.typ [in typ]
PTS_ATR_mod.env_conv [in env_conv]
PTS_ATR_mod.typ_peq [in typ_peq]
PTS_ATR_mod.env_conv1 [in env_conv1]
R
red_mod.Betaps [in Betaps]red_mod.Betap [in Betap]
red_mod.Betas [in Betas]
red_mod.Beta [in Beta]
T
term_mod.Term [in Term]U
ut_typ_eq_mod.wf [in wf]ut_typ_mod.wf [in wf]
ut_typ_eq_mod.typ_eqm [in typ_eqm]
ut_env_mod.sub_in_env [in sub_in_env]
ut_env_mod.trunc [in trunc]
ut_term_mod.Term [in Term]
ut_red_mod.Betaps [in Betaps]
ut_sr_mod.Betac_env [in Betac_env]
ut_sr_mod.Betas_env [in Betas_env]
ut_typ_eq_mod.wfm [in wfm]
ut_typ_mod.legacy_wf [in legacy_wf]
ut_typ_eq_mod.typ [in typ]
ut_typ_mod.typ [in typ]
ut_env_mod.ins_in_env [in ins_in_env]
ut_red_mod.Betac [in Betac]
ut_red_mod.Betap [in Betap]
ut_red_mod.Betas [in Betas]
ut_red_mod.Beta [in Beta]
ut_env_mod.item [in item]
ut_sr_mod.Beta_env [in Beta_env]
ut_typ_eq_mod.typ_eq [in typ_eq]
ut_typ_mod.legacy_typ [in legacy_typ]
Definition Index
E
env_mod.item_lift [in item_lift]env_mod.Env [in Env]
F
f_typ_mod.ltyp_induc [in ltyp_induc]f_typ_mod.is_type [in is_type]
f_env_mod.item_lift [in item_lift]
f_typ2_mod.erasure_outer [in erasure_outer]
f_typ2_mod.der_typ_ind' [in der_typ_ind']
f_typ_mod.wf_ind' [in wf_ind']
f_typ2_mod.subst_mult_term [in subst_mult_term]
f_typ2_mod.erasure_context [in erasure_context]
f_typ_mod.lwf_ind' [in lwf_ind']
f_term_mod.lift_rec_h [in lift_rec_h]
f_term_mod.Prf_ind' [in Prf_ind']
f_typ2_mod.erasure [in erasure]
f_term_mod.subst_rec [in subst_rec]
f_typ_mod.typh_ind' [in typh_ind']
f_typ2_mod.der_wf_ind' [in der_wf_ind']
f_typ2_mod.der_induc [in der_induc]
f_typ_mod.typ_ind' [in typ_ind']
f_term_mod.Term_induc [in Term_induc]
f_env_mod.Env [in Env]
f_typ2_mod.der_h_ind' [in der_h_ind']
f_typ_mod.typ_induc [in typ_induc]
f_term_mod.lift_rec [in lift_rec]
f_typ_mod.typ_h_short [in typ_h_short]
f_term_mod.subst_rec_h [in subst_rec_h]
f_term_mod.Term_ind' [in Term_ind']
f_typ_mod.ltyp_ind' [in ltyp_ind']
f_typ_mod.ltyph_ind' [in ltyph_ind']
f_typ_mod.has_type [in has_type]
f_typ2_mod.subst_mult_prf [in subst_mult_prf]
f_typ_mod.semitype [in semitype]
P
PTS_ATR_mod.typ_reds_ind' [in typ_reds_ind']PTS_ATR_mod.wf_ind' [in wf_ind']
PTS_ATR_mod.typ_ind' [in typ_ind']
PTS_ATR_mod.typ_induc [in typ_induc]
S
strip_mod.strip_env [in strip_env]strip_mod.strip [in strip]
T
term_mod.subst_rec [in subst_rec]term_mod.lift_rec [in lift_rec]
U
ut_env_mod.item_lift [in item_lift]ut_typ_eq_mod.wfm_ind' [in wfm_ind']
ut_typ_eq_mod.wf_ind' [in wf_ind']
ut_typ_mod.wf_ind' [in wf_ind']
ut_typ_eq_mod.typ_eq_ind' [in typ_eq_ind']
ut_typ_eq_mod.typm_induc [in typm_induc]
ut_term_mod.subst_rec [in subst_rec]
ut_typ_eq_mod.typ_ind' [in typ_ind']
ut_typ_mod.typ_ind' [in typ_ind']
ut_env_mod.Env [in Env]
ut_typ_eq_mod.typ_induc [in typ_induc]
ut_typ_mod.typ_induc [in typ_induc]
ut_term_mod.lift_rec [in lift_rec]
ut_typ_eq_mod.typ_eqm_ind' [in typ_eqm_ind']
V
Vars [in Vars]Module Index
E
env_mod [in env_mod]F
final_mod [in final_mod]f_equiv_mod [in f_equiv_mod]
f_env_mod [in f_env_mod]
f_typ_mod [in f_typ_mod]
f_typ2_mod [in f_typ2_mod]
f_term_mod [in f_term_mod]
G
glue_mod [in glue_mod]P
pts_sig [in pts_sig]PTS_ATR_mod [in PTS_ATR_mod]
R
red_mod [in red_mod]S
strip_mod [in strip_mod]T
term_sig [in term_sig]term_mod [in term_mod]
Theory [in Theory]
Theory.PTS [in Theory.PTS]
Theory.PTSATR [in Theory.PTSATR]
Theory.PTSe [in Theory.PTSe]
U
ut_typ_eq_mod [in ut_typ_eq_mod]ut_sr_mod [in ut_sr_mod]
ut_term_mod [in ut_term_mod]
ut_env_mod [in ut_env_mod]
ut_typ_mod [in ut_typ_mod]
ut_red_mod [in ut_red_mod]
Axiom Index
P
pts_sig.Rel [in Rel]pts_sig.Ax [in Ax]
T
term_sig.Sorts [in Sorts]Library Index
B
baseE
envF
final_resultf_typ2
f_equivalence
f_typ
f_term
f_env
G
glueR
redS
stripT
termtyp_annot
U
ut_srut_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 | (827 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 | (366 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 | (82 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 | (221 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 | (57 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 | (55 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 | (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 | (19 entries) |
This page has been generated by coqdoc