| 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 | _ | (1749 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (2 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
| 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 | _ | (858 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (21 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 | _ | (220 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 | _ | (54 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (15 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 | _ | (217 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 | _ | (79 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 | _ | (134 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (105 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 | _ | (42 entries) |
Global Index
A
abs [constructor, in deBruijn_Fsub_Iso]add [abbreviation, in Metatheory_Env]
all [constructor, in deBruijn_Fsub_Iso]
app [constructor, in deBruijn_Fsub_Iso]
appabs [constructor, in dB_Fsub_basic_Main]
apparg [constructor, in dB_Fsub_basic_Main]
appfun [constructor, in dB_Fsub_basic_Main]
apply_tuple [definition, in CoqUniquenessTac]
app_cons_not_nil [lemma, in CoqListFacts]
app_eq_cons [lemma, in CoqListFacts]
Arith_Max_extra [library]
arrow [constructor, in deBruijn_Fsub_Iso]
arrow [definition, in CoqUniquenessTac]
AssocList [library]
atm [abbreviation, in Tutorial_STLC_Iso]
atm [abbreviation, in LNameless_STLC_Iso]
ATOM [module, in MetatheoryAtom]
AtomDT [module, in MetatheoryAtom]
AtomDT.eq [definition, in MetatheoryAtom]
AtomDT.eq_dec [definition, in MetatheoryAtom]
AtomDT.eq_refl [definition, in MetatheoryAtom]
AtomDT.eq_sym [definition, in MetatheoryAtom]
AtomDT.eq_trans [definition, in MetatheoryAtom]
AtomDT.t [definition, in MetatheoryAtom]
AtomImpl [module, in MetatheoryAtom]
AtomImpl.atom [definition, in MetatheoryAtom]
AtomImpl.atom_fresh_for_list [lemma, in MetatheoryAtom]
AtomImpl.eq_atom_dec [definition, in MetatheoryAtom]
AtomImpl.max_lt_r [lemma, in MetatheoryAtom]
AtomImpl.nat_list_max [lemma, in MetatheoryAtom]
atoms [abbreviation, in MetatheoryAtom]
AtomSetDecide [module, in MetatheoryAtom]
AtomSetFacts [module, in MetatheoryAtom]
AtomSetImpl [module, in MetatheoryAtom]
AtomSetNotin [module, in MetatheoryAtom]
AtomSetProperties [module, in MetatheoryAtom]
ATOM.atom [axiom, in MetatheoryAtom]
ATOM.atom_fresh_for_list [axiom, in MetatheoryAtom]
ATOM.eq_atom_dec [axiom, in MetatheoryAtom]
atom_fresh [lemma, in MetatheoryAtom]
B
bfsubstRep_permutation [lemma, in LNameless_Meta_Env]bfsubstRep_permutation_core [lemma, in LNameless_Meta]
bfsubstRep_permutation_core_wf [lemma, in LNameless_Meta]
bfsubstRep_permutation_ind [lemma, in LNameless_Meta]
bfsubstRep_permutation_ind_wf [lemma, in LNameless_Meta]
bfsubstRep_permutation_var [lemma, in LNameless_Meta_Env]
bfsubstRep_permutation_var_wf [lemma, in LNameless_Meta]
bfsubstRep_permutation_var_wfT [lemma, in LNameless_Meta]
bfsubstRep_permutation_wf [lemma, in LNameless_Meta]
bfsubstRep_permutation_wfT [lemma, in LNameless_Meta]
bfsubstRep_var_intro [lemma, in LNameless_Meta]
bfsubst_permutation [lemma, in LNameless_Meta_Env]
bfsubst_permutation_core [lemma, in LNameless_Meta]
bfsubst_permutation_core_wf [lemma, in LNameless_Meta]
bfsubst_permutation_ind [lemma, in LNameless_Meta]
bfsubst_permutation_ind_wf [lemma, in LNameless_Meta]
bfsubst_permutation_var [lemma, in LNameless_Meta_Env]
bfsubst_permutation_var_wf [lemma, in LNameless_Meta]
bfsubst_permutation_var_wfT [lemma, in LNameless_Meta]
bfsubst_permutation_var_wfT_hetero [lemma, in LNameless_Meta]
bfsubst_permutation_wf [lemma, in LNameless_Meta]
bfsubst_permutation_wfT [lemma, in LNameless_Meta]
bfsubst_var_intro [lemma, in LNameless_Meta]
BIND [constructor, in DGP_Core]
bind [inductive, in LN_Fsub_basic_Definitions]
bind_sub [constructor, in LN_Fsub_basic_Definitions]
bind_typ [constructor, in LN_Fsub_basic_Definitions]
bsubst [definition, in LNameless_Meta]
bsubstitutionRep_hetero [lemma, in LNameless_Meta]
bsubstitutionRep_hetero_wf [lemma, in LNameless_Meta]
bsubstitutionRep_homo [lemma, in LNameless_Meta]
bsubstitutionRep_homo_wf [lemma, in LNameless_Meta]
bsubstitutionRep_var_twice [lemma, in LNameless_Meta]
bsubstitutionRep_var_twice_wf [lemma, in LNameless_Meta]
bsubstitution_hetero [lemma, in LNameless_Meta]
bsubstitution_hetero_wf [lemma, in LNameless_Meta]
bsubstitution_homo [lemma, in LNameless_Meta]
bsubstitution_homo_wf [lemma, in LNameless_Meta]
bsubstitution_var_twice [lemma, in LNameless_Meta]
bsubstitution_var_twice_wf [lemma, in LNameless_Meta]
bsubstRep [definition, in LNameless_Meta]
bsubstRep_hetero_core [lemma, in LNameless_Meta]
bsubstRep_homo_core [lemma, in LNameless_Meta]
bsubst_hetero_core [lemma, in LNameless_Meta]
bsubst_homo_core [lemma, in LNameless_Meta]
bsubst_size [lemma, in LNameless_Meta]
bsubst_sizeRep [lemma, in LNameless_Meta]
C
canonical_form_abs [lemma, in LN_Fsub_adv_Soundness]canonical_form_abs [lemma, in LN_Fsub_basic_Soundness]
canonical_form_tabs [lemma, in LN_Fsub_basic_Soundness]
canonical_form_tabs [lemma, in LN_Fsub_adv_Soundness]
CONST [constructor, in DGP_Core]
cons_eq_app [lemma, in CoqListFacts]
context_replacement [lemma, in dB_Fsub_basic_Main]
conv_bsubst [lemma, in LNameless_Meta]
conv_envT [lemma, in LNameless_Meta_Env]
conv_freevars_1 [lemma, in LNameless_Meta]
conv_freevars_2 [lemma, in LNameless_Meta]
conv_freevars_3 [lemma, in LNameless_Meta]
conv_freevars_4 [lemma, in LNameless_Meta]
conv_fsubst [lemma, in LNameless_Meta]
conv_wfT [lemma, in LNameless_Meta]
CoqEqDec [library]
CoqFSetDecide [library]
CoqFSetInterface [library]
CoqListFacts [library]
CoqUniquenessTac [library]
ctx [inductive, in dB_Fsub_basic_Main]
ctx_app [definition, in dB_Fsub_basic_Main]
c_apparg [constructor, in dB_Fsub_basic_Main]
c_appfun [constructor, in dB_Fsub_basic_Main]
c_hole [constructor, in dB_Fsub_basic_Main]
c_typefun [constructor, in dB_Fsub_basic_Main]
D
D [module, in AssocList]D [module, in FSetWeakNotin]
dBTemplate [module, in dB_Template]
dBTemplate.From_TEnv [definition, in dB_Template]
dBTemplate.From_To_TEnv [lemma, in dB_Template]
dBTemplate.From_Tshift [lemma, in dB_Template]
dBTemplate.From_Tsubst [lemma, in dB_Template]
dBTemplate.gTget_left [definition, in dB_Template]
dBTemplate.gTget_right [definition, in dB_Template]
dBTemplate.gTinsert_left [definition, in dB_Template]
dBTemplate.gTremove_right [definition, in dB_Template]
dBTemplate.gTwf_env [definition, in dB_Template]
dBTemplate.gTwf_env_Twf_env [lemma, in dB_Template]
dBTemplate.opt_From [definition, in dB_Template]
dBTemplate.opt_From_preserving_some [lemma, in dB_Template]
dBTemplate.opt_To [definition, in dB_Template]
dBTemplate.opt_To_preserving_eq [lemma, in dB_Template]
dBTemplate.opt_To_preserving_eq_rev [lemma, in dB_Template]
dBTemplate.opt_To_preserving_none [lemma, in dB_Template]
dBTemplate.opt_To_preserving_none_rev [lemma, in dB_Template]
dBTemplate.opt_To_preserving_some [lemma, in dB_Template]
dBTemplate.opt_To_preserving_some_rev [lemma, in dB_Template]
dBTemplate.TEnv [abbreviation, in dB_Template]
dBTemplate.Tinsert [definition, in dB_Template]
dBTemplate.Tinsert_S [lemma, in dB_Template]
dBTemplate.Tlth [definition, in dB_Template]
dBTemplate.To_From_TEnv [lemma, in dB_Template]
dBTemplate.To_TEnv [definition, in dB_Template]
dBTemplate.Tremove_right [definition, in dB_Template]
dBTemplate.Tremove_right_gTremove_right [lemma, in dB_Template]
dBTemplate.Tshift [definition, in dB_Template]
dBTemplate.Tshift_id [lemma, in dB_Template]
dBTemplate.Tsubst [definition, in dB_Template]
dBTemplate.Tsubst_id [lemma, in dB_Template]
dBTemplate.Twf_env [definition, in dB_Template]
dBTemplate.Twf_env_gTwf_env [lemma, in dB_Template]
dBTemplate.Twf_env_remove_right [lemma, in dB_Template]
dBTemplate.Twf_env_weaken [lemma, in dB_Template]
dBTemplate.Twf_typ [definition, in dB_Template]
dBTemplate.Twf_typ_eleft [lemma, in dB_Template]
dBTemplate.Twf_typ_insert_right [lemma, in dB_Template]
dBTemplate.Twf_typ_remove_right [lemma, in dB_Template]
dBTemplate.Twf_typ_strengthening_right [lemma, in dB_Template]
dBTemplate.Twf_typ_weakening_right [lemma, in dB_Template]
dBTemplate.Ysize [definition, in dB_Template]
dB_Fsub_basic_Main [library]
dB_Template [library]
dB_Template_Two_Sort [library]
deBruijn [module, in deBruijn_Meta]
deBruijn_Fsub_Iso [library]
deBruijn_Isomorphism [library]
deBruijn_Meta [library]
deBruijn_Meta_Env [library]
DecidableSorting [section, in CoqListFacts]
DecidableSorting.A [variable, in CoqListFacts]
DecidableSorting.leA [variable, in CoqListFacts]
DecidableSorting.leA_dec [variable, in CoqListFacts]
Decide [module, in CoqFSetDecide]
Dgp [module, in DGP_Core]
Dgp.Bind [constructor, in DGP_Core]
Dgp.Const [constructor, in DGP_Core]
Dgp.conv [definition, in DGP_Core]
Dgp.conv_id [lemma, in DGP_Core]
Dgp.conv_indep [lemma, in DGP_Core]
Dgp.conv_size [lemma, in DGP_Core]
Dgp.conv_Var [lemma, in DGP_Core]
Dgp.InL [constructor, in DGP_Core]
Dgp.InR [constructor, in DGP_Core]
Dgp.Interpret [inductive, in DGP_Core]
Dgp.InterpretRep [inductive, in DGP_Core]
Dgp.Pair [constructor, in DGP_Core]
Dgp.QQ [definition, in DGP_Core]
Dgp.Rec [constructor, in DGP_Core]
Dgp.Repr [constructor, in DGP_Core]
Dgp.size [definition, in DGP_Core]
Dgp.sizeRep [definition, in DGP_Core]
Dgp.Term [constructor, in DGP_Core]
Dgp.Unit [constructor, in DGP_Core]
Dgp.Var [constructor, in DGP_Core]
Dgp.VV [definition, in DGP_Core]
DGP_Core [library]
DisjUnionUsualDecidableType [module, in Metatheory_Var]
DisjUnionUsualDecidableType.eq [definition, in Metatheory_Var]
DisjUnionUsualDecidableType.eq_dec [definition, in Metatheory_Var]
DisjUnionUsualDecidableType.eq_refl [definition, in Metatheory_Var]
DisjUnionUsualDecidableType.eq_sym [definition, in Metatheory_Var]
DisjUnionUsualDecidableType.eq_trans [definition, in Metatheory_Var]
DisjUnionUsualDecidableType.t [definition, in Metatheory_Var]
dom_empty_env [lemma, in Metatheory_Env]
dom_map_1 [lemma, in Metatheory_Env]
dom_map_2 [lemma, in Metatheory_Env]
dom_map_3 [lemma, in Metatheory_Env]
dom_map_4 [lemma, in Metatheory_Env]
E
E [module, in CoqFSetInterface]E [module, in CoqFSetInterface]
E [module, in CoqFSetInterface]
elim_incl_app [lemma, in CoqListFacts]
elim_incl_cons [lemma, in CoqListFacts]
elim_not_In_app [lemma, in CoqListFacts]
elim_not_In_cons [lemma, in CoqListFacts]
empty [abbreviation, in Metatheory_Env]
empty_env [definition, in Metatheory_Env]
env [definition, in Metatheory_Env]
ENV [abbreviation, in deBruijn_Meta_Env]
Env [definition, in deBruijn_Meta_Env]
EnvImpl [module, in Metatheory_Env]
envT [inductive, in LNameless_Meta_Env]
envTRep [inductive, in LNameless_Meta_Env]
envTRep_dom_subset [lemma, in LNameless_Meta_Env]
envTRep_fv [lemma, in LNameless_Meta_Env]
envTrep_wfRep [lemma, in LNameless_Meta_Env]
envTRep_wfT [lemma, in LNameless_Meta_Env]
envT_dom_subset [lemma, in LNameless_Meta_Env]
envT_from_wf_env [lemma, in LNameless_Meta_Env]
envT_from_wf_env_left [lemma, in LNameless_Meta_Env]
envT_fv [lemma, in LNameless_Meta_Env]
envT_narrow [lemma, in LNameless_Meta_Env]
envT_narrowRep [lemma, in LNameless_Meta_Env]
envT_narrowRep_ [lemma, in LNameless_Meta_Env]
envT_narrow_ [lemma, in LNameless_Meta_Env]
envT_narrow_left [lemma, in LNameless_Meta_Env]
envT_narrow_right [lemma, in LNameless_Meta_Env]
envT_Tfv [lemma, in LN_Template_One_Sort]
envT_Tfv [lemma, in LN_Template_Two_Sort]
envT_weaken [lemma, in LNameless_Meta_Env]
envT_weakenRep [lemma, in LNameless_Meta_Env]
envT_weaken_left [lemma, in LNameless_Meta_Env]
envT_weaken_right [lemma, in LNameless_Meta_Env]
envT_wf [lemma, in LNameless_Meta_Env]
envT_wfT [lemma, in LNameless_Meta_Env]
env_Bind_hetero [constructor, in LNameless_Meta_Env]
env_Bind_homo [constructor, in LNameless_Meta_Env]
env_Bind_REC_hetero [constructor, in LNameless_Meta_Env]
env_Bind_REC_homo [constructor, in LNameless_Meta_Env]
env_Const [constructor, in LNameless_Meta_Env]
Env_Definitions [section, in Metatheory_Env]
Env_Definitions.A [variable, in Metatheory_Env]
env_fvar [constructor, in LNameless_Meta_Env]
env_InL [constructor, in LNameless_Meta_Env]
env_InR [constructor, in LNameless_Meta_Env]
env_Pair [constructor, in LNameless_Meta_Env]
env_Rec [constructor, in LNameless_Meta_Env]
env_Repr [constructor, in LNameless_Meta_Env]
env_subst [inductive, in dB_Fsub_basic_Main]
env_subst_get_left_ge [lemma, in dB_Fsub_basic_Main]
env_subst_get_left_lt [lemma, in dB_Fsub_basic_Main]
env_subst_get_right [lemma, in dB_Fsub_basic_Main]
env_subst_le [lemma, in dB_Fsub_basic_Main]
env_subst_minus_1 [lemma, in dB_Fsub_basic_Main]
env_subst_sub [lemma, in dB_Fsub_basic_Main]
env_subst_wf_env [lemma, in dB_Fsub_basic_Main]
env_subst_wf_typ [lemma, in dB_Fsub_basic_Main]
env_subst_wf_typ_0 [lemma, in dB_Fsub_basic_Main]
env_Term [constructor, in LNameless_Meta_Env]
env_Unit [constructor, in LNameless_Meta_Env]
env_Var [constructor, in LNameless_Meta_Env]
EqDec_atom [instance, in MetatheoryAtom]
EqDec_eq [record, in CoqEqDec]
EqDec_eq [inductive, in CoqEqDec]
EqDec_eq_of_EqDec [instance, in CoqEqDec]
eqlistA_unique [lemma, in CoqListFacts]
eqlist_eq [lemma, in CoqListFacts]
equiv_decidable [lemma, in CoqEqDec]
equiv_reflexive' [lemma, in CoqEqDec]
equiv_symmetric' [lemma, in CoqEqDec]
equiv_transitive' [lemma, in CoqEqDec]
eq_dec [projection, in CoqEqDec]
eq_dec [constructor, in CoqEqDec]
eq_pair_dec [lemma, in CoqUniquenessTac]
eq_unit_dec [lemma, in CoqUniquenessTac]
es_here [constructor, in dB_Fsub_basic_Main]
es_left [constructor, in dB_Fsub_basic_Main]
es_right [constructor, in dB_Fsub_basic_Main]
example_pick_fresh_use [lemma, in MetatheoryAtom]
extends [definition, in Metatheory_Env]
extendsRep_env [lemma, in LNameless_Meta_Env]
extends_app_L [lemma, in Metatheory_Env]
extends_app_R [lemma, in Metatheory_Env]
extends_env [lemma, in LNameless_Meta_Env]
extends_L [lemma, in Metatheory_Env]
extends_push [lemma, in Metatheory_Env]
extends_R [lemma, in Metatheory_Env]
extends_swap [lemma, in Metatheory_Env]
E_AppAbs [constructor, in dB_Fsub_basic_Main]
E_Ctx [constructor, in dB_Fsub_basic_Main]
E_TappTabs [constructor, in dB_Fsub_basic_Main]
F
F [module, in CoqFSetDecide]freevars [definition, in LNameless_Meta]
freevarsRep [definition, in LNameless_Meta]
freevarsRep_pass_binder [lemma, in LNameless_Meta]
freevars_pass_binder [lemma, in LNameless_Meta]
FSetDecideAuxiliary [module, in CoqFSetDecide]
FSetDecideTestCases [module, in CoqFSetDecide]
FSetExtra [library]
FSetLogicalFacts [module, in CoqFSetDecide]
FSetWeakNotin [library]
fsubst [definition, in LNameless_Meta]
fsubstitution [lemma, in LNameless_Meta]
fsubstitutionRep [lemma, in LNameless_Meta]
fsubstRep [definition, in LNameless_Meta]
fsubstRep_fresh [lemma, in LNameless_Meta_Env]
fsubstRep_no_occur [lemma, in LNameless_Meta]
fsubstRep_self [lemma, in LNameless_Meta]
fsubst_fresh [lemma, in LNameless_Meta_Env]
fsubst_no_occur [lemma, in LNameless_Meta]
fsubst_self [lemma, in LNameless_Meta]
fun_inj [definition, in deBruijn_Isomorphism]
fun_inj [definition, in LNameless_Isomorphism]
fun_value [lemma, in dB_Fsub_basic_Main]
FWellformed [module, in LN_Template]
FWellformed.envT_THfv [lemma, in LN_Template]
FWellformed.envT_Yfv [lemma, in LN_Template]
FWellformed.extends_TenvT [lemma, in LN_Template]
FWellformed.noRepr_YHenvT [lemma, in LN_Template]
FWellformed.notin_app_3 [lemma, in LN_Template]
FWellformed.TenvT [definition, in LN_Template]
FWellformed.TenvT_narrow [lemma, in LN_Template]
FWellformed.TenvT_narrow_left [lemma, in LN_Template]
FWellformed.TenvT_narrow_right [lemma, in LN_Template]
FWellformed.TenvT_weaken [lemma, in LN_Template]
FWellformed.TenvT_weaken_left [lemma, in LN_Template]
FWellformed.TenvT_weaken_right [lemma, in LN_Template]
FWellformed.THenvT [definition, in LN_Template]
FWellformed.THenvT_Thwf [lemma, in LN_Template]
FWellformed.THenvT_THwfT [lemma, in LN_Template]
FWellformed.uniq_from_Ywf_env [lemma, in LN_Template]
FWellformed.YenvT [definition, in LN_Template]
FWellformed.YenvT_Ywf [lemma, in LN_Template]
FWellformed.YenvT_YwfT [lemma, in LN_Template]
FWellformed.YHenvT [definition, in LN_Template]
FWellformed.YTenvT [definition, in LN_Template]
FWellformed.YTenvT_narrow [lemma, in LN_Template]
FWellformed.YTenvT_narrow_left [lemma, in LN_Template]
FWellformed.YTenvT_narrow_right [lemma, in LN_Template]
FWellformed.YTenvT_typ_var_indep [lemma, in LN_Template]
FWellformed.YTenvT_typ_var_strengthen [lemma, in LN_Template]
FWellformed.YTenvT_weaken [lemma, in LN_Template]
FWellformed.YTenvT_weaken_left [lemma, in LN_Template]
FWellformed.YTenvT_weaken_right [lemma, in LN_Template]
FWellformed.Ywf_env [definition, in LN_Template]
G
GenericVarSig [module, in Metatheory_Var]get_left [definition, in deBruijn_Meta_Env]
get_left_gt [lemma, in deBruijn_Meta_Env]
get_left_insert_left_ge [lemma, in deBruijn_Meta_Env]
get_left_insert_left_lt [lemma, in deBruijn_Meta_Env]
get_left_narrow_eq [lemma, in dB_Fsub_basic_Main]
get_left_narrow_ne [lemma, in dB_Fsub_basic_Main]
get_left_remove_right [lemma, in deBruijn_Meta_Env]
get_right [definition, in deBruijn_Meta_Env]
get_right_insert_left [lemma, in deBruijn_Meta_Env]
get_right_narrow [lemma, in dB_Fsub_basic_Main]
get_right_remove_right_ge [lemma, in deBruijn_Meta_Env]
get_right_remove_right_lt [lemma, in deBruijn_Meta_Env]
get_right_wf [lemma, in deBruijn_Meta_Env]
gTinsert_left_Tinsert_left [lemma, in dB_Template_Two_Sort]
gTTwf [definition, in LN_Template_Two_Sort]
gTTwf_basic [definition, in LN_Template_Two_Sort]
gTTwf_TTwf [lemma, in LN_Template_Two_Sort]
gTTwf_TTwf_basic [lemma, in LN_Template_Two_Sort]
GVar_to_Quant [module, in Metatheory_Var]
H
HO_wf [definition, in deBruijn_Meta_Env]HO_wfRep [definition, in deBruijn_Meta_Env]
HO_wfRep_extensionality [lemma, in deBruijn_Meta_Env]
HO_wfRep_insert_right [lemma, in deBruijn_Meta_Env]
HO_wfRep_left [lemma, in deBruijn_Meta_Env]
HO_wfRep_strengthening_right [lemma, in deBruijn_Meta_Env]
HO_wfRep_weaken [lemma, in deBruijn_Meta_Env]
HO_wfRep_weakening_left [lemma, in deBruijn_Meta_Env]
HO_wfRep_weakening_right [lemma, in deBruijn_Meta_Env]
HO_wfRep_weaken_lth [lemma, in deBruijn_Meta_Env]
HO_wfright_remove_right [lemma, in deBruijn_Meta_Env]
HO_wf_extensionality [lemma, in deBruijn_Meta_Env]
HO_wf_insert_right [lemma, in deBruijn_Meta_Env]
HO_wf_left [lemma, in deBruijn_Meta_Env]
HO_wf_remove_right [lemma, in deBruijn_Meta_Env]
HO_wf_strengthening_right [lemma, in deBruijn_Meta_Env]
HO_wf_weaken [lemma, in deBruijn_Meta_Env]
HO_wf_weakening_left [lemma, in deBruijn_Meta_Env]
HO_wf_weakening_right [lemma, in deBruijn_Meta_Env]
HO_wf_weaken_lth [lemma, in deBruijn_Meta_Env]
I
il_here [constructor, in deBruijn_Meta_Env]il_left [constructor, in deBruijn_Meta_Env]
il_right [constructor, in deBruijn_Meta_Env]
InA_iff_In [lemma, in CoqListFacts]
InA_In [lemma, in CoqListFacts]
incl_nil [lemma, in CoqListFacts]
Inf [abbreviation, in CoqListFacts]
insert [definition, in deBruijn_Meta_Env]
insert_left [inductive, in deBruijn_Meta_Env]
insert_left_HO_wf [lemma, in deBruijn_Meta_Env]
insert_left_HO_wfRep [lemma, in deBruijn_Meta_Env]
insert_left_lth [lemma, in deBruijn_Meta_Env]
insert_left_lth_1 [lemma, in deBruijn_Meta_Env]
insert_left_wf_env [lemma, in deBruijn_Meta_Env]
insert_S [lemma, in deBruijn_Meta_Env]
insert_T [lemma, in deBruijn_Meta_Env]
insert_T_ind [lemma, in deBruijn_Meta_Env]
In_atoms_dec [lemma, in Metatheory_Env]
In_atoms_dec [lemma, in LNameless_Meta_Env]
In_incl [lemma, in CoqListFacts]
In_map [lemma, in CoqListFacts]
Iso [definition, in LNameless_Isomorphism]
Iso [definition, in deBruijn_Isomorphism]
Iso_full [module, in LNameless_Isomorphism]
Iso_full [module, in deBruijn_Isomorphism]
Iso_full.From_To [axiom, in LNameless_Isomorphism]
Iso_full.From_To [axiom, in deBruijn_Isomorphism]
Iso_full.To_inj [axiom, in deBruijn_Isomorphism]
Iso_full.To_inj [axiom, in LNameless_Isomorphism]
Iso_nat [module, in LNameless_Isomorphism]
Iso_nat [module, in deBruijn_Isomorphism]
Iso_nat [module, in Tutorial_STLC_Iso]
Iso_nat.From [definition, in Tutorial_STLC_Iso]
Iso_nat.From [definition, in deBruijn_Isomorphism]
Iso_nat.From [definition, in LNameless_Isomorphism]
Iso_nat.RR [definition, in LNameless_Isomorphism]
Iso_nat.RR [definition, in deBruijn_Isomorphism]
Iso_nat.RR [definition, in Tutorial_STLC_Iso]
Iso_nat.To [definition, in LNameless_Isomorphism]
Iso_nat.To [definition, in deBruijn_Isomorphism]
Iso_nat.To [definition, in Tutorial_STLC_Iso]
Iso_nat.To_ [definition, in deBruijn_Isomorphism]
Iso_nat.To_ [definition, in LNameless_Isomorphism]
Iso_nat.To_ [definition, in Tutorial_STLC_Iso]
Iso_nat.To_From [lemma, in deBruijn_Isomorphism]
Iso_nat.To_From [lemma, in Tutorial_STLC_Iso]
Iso_nat.To_From [lemma, in LNameless_Isomorphism]
Iso_nat.TT [definition, in deBruijn_Isomorphism]
Iso_nat.TT [definition, in Tutorial_STLC_Iso]
Iso_nat.TT [definition, in LNameless_Isomorphism]
Iso_nat_REC [lemma, in deBruijn_Isomorphism]
Iso_nat_REC [lemma, in LNameless_Isomorphism]
Iso_partial [module, in deBruijn_Isomorphism]
Iso_partial [module, in LNameless_Isomorphism]
Iso_partial.From [axiom, in LNameless_Isomorphism]
Iso_partial.From [axiom, in deBruijn_Isomorphism]
Iso_partial.From_inj [axiom, in deBruijn_Isomorphism]
Iso_partial.From_inj [axiom, in LNameless_Isomorphism]
Iso_partial.ISO [definition, in deBruijn_Isomorphism]
Iso_partial.ISO [definition, in LNameless_Isomorphism]
Iso_partial.RR [axiom, in LNameless_Isomorphism]
Iso_partial.RR [axiom, in deBruijn_Isomorphism]
Iso_partial.To [axiom, in LNameless_Isomorphism]
Iso_partial.To [axiom, in deBruijn_Isomorphism]
Iso_partial.To_From [axiom, in deBruijn_Isomorphism]
Iso_partial.To_From [axiom, in LNameless_Isomorphism]
Iso_partial.TT [axiom, in deBruijn_Isomorphism]
Iso_partial.TT [axiom, in LNameless_Isomorphism]
Iso_trm [module, in LNameless_STLC_Iso]
Iso_trm [module, in Tutorial_STLC_Iso]
Iso_trm [module, in deBruijn_Fsub_Iso]
Iso_trm [module, in LNameless_Fsub_Iso]
Iso_trm.From [definition, in LNameless_Fsub_Iso]
Iso_trm.From [definition, in deBruijn_Fsub_Iso]
Iso_trm.From [definition, in LNameless_STLC_Iso]
Iso_trm.From [definition, in Tutorial_STLC_Iso]
Iso_trm.From_inj [lemma, in deBruijn_Fsub_Iso]
Iso_trm.From_inj [lemma, in LNameless_Fsub_Iso]
Iso_trm.From_inj [lemma, in Tutorial_STLC_Iso]
Iso_trm.From_inj [lemma, in LNameless_STLC_Iso]
Iso_trm.From_To [lemma, in deBruijn_Fsub_Iso]
Iso_trm.From_To [lemma, in Tutorial_STLC_Iso]
Iso_trm.From_To [lemma, in LNameless_Fsub_Iso]
Iso_trm.From_To [lemma, in LNameless_STLC_Iso]
Iso_trm.From_To_Rep [lemma, in LNameless_Fsub_Iso]
Iso_trm.From_To_Rep [lemma, in LNameless_STLC_Iso]
Iso_trm.From_To_Rep [lemma, in deBruijn_Fsub_Iso]
Iso_trm.From_To_Rep [lemma, in Tutorial_STLC_Iso]
Iso_trm.ISO [definition, in Tutorial_STLC_Iso]
Iso_trm.ISO [definition, in LNameless_Fsub_Iso]
Iso_trm.ISO [definition, in LNameless_STLC_Iso]
Iso_trm.ISO [definition, in deBruijn_Fsub_Iso]
Iso_trm.RR [definition, in Tutorial_STLC_Iso]
Iso_trm.RR [definition, in LNameless_STLC_Iso]
Iso_trm.RR [definition, in LNameless_Fsub_Iso]
Iso_trm.RR [definition, in deBruijn_Fsub_Iso]
Iso_trm.To [definition, in Tutorial_STLC_Iso]
Iso_trm.To [definition, in deBruijn_Fsub_Iso]
Iso_trm.To [definition, in LNameless_STLC_Iso]
Iso_trm.To [definition, in LNameless_Fsub_Iso]
Iso_trm.To_ [definition, in LNameless_Fsub_Iso]
Iso_trm.To_ [definition, in deBruijn_Fsub_Iso]
Iso_trm.To_ [definition, in LNameless_STLC_Iso]
Iso_trm.To_ [definition, in Tutorial_STLC_Iso]
Iso_trm.To_From [lemma, in deBruijn_Fsub_Iso]
Iso_trm.To_From [lemma, in LNameless_STLC_Iso]
Iso_trm.To_From [lemma, in Tutorial_STLC_Iso]
Iso_trm.To_From [lemma, in LNameless_Fsub_Iso]
Iso_trm.To_inj [lemma, in LNameless_STLC_Iso]
Iso_trm.To_inj [lemma, in Tutorial_STLC_Iso]
Iso_trm.To_inj [lemma, in deBruijn_Fsub_Iso]
Iso_trm.To_inj [lemma, in LNameless_Fsub_Iso]
Iso_trm.TT [definition, in LNameless_STLC_Iso]
Iso_trm.TT [definition, in Tutorial_STLC_Iso]
Iso_trm.TT [definition, in deBruijn_Fsub_Iso]
Iso_trm.TT [definition, in LNameless_Fsub_Iso]
Iso_typ [module, in Tutorial_STLC_Iso]
Iso_typ [module, in LNameless_Fsub_Iso]
Iso_typ [module, in LNameless_STLC_Iso]
Iso_typ [module, in deBruijn_Fsub_Iso]
Iso_typ.From [definition, in Tutorial_STLC_Iso]
Iso_typ.From [definition, in LNameless_STLC_Iso]
Iso_typ.From [definition, in LNameless_Fsub_Iso]
Iso_typ.From [definition, in deBruijn_Fsub_Iso]
Iso_typ.From_inj [lemma, in deBruijn_Fsub_Iso]
Iso_typ.From_inj [lemma, in LNameless_Fsub_Iso]
Iso_typ.From_inj [lemma, in LNameless_STLC_Iso]
Iso_typ.From_inj [lemma, in Tutorial_STLC_Iso]
Iso_typ.From_To [lemma, in deBruijn_Fsub_Iso]
Iso_typ.From_To [lemma, in LNameless_Fsub_Iso]
Iso_typ.From_To_Rep [lemma, in LNameless_Fsub_Iso]
Iso_typ.From_To_Rep [lemma, in deBruijn_Fsub_Iso]
Iso_typ.ISO [definition, in deBruijn_Fsub_Iso]
Iso_typ.ISO [definition, in LNameless_Fsub_Iso]
Iso_typ.ISO [definition, in LNameless_STLC_Iso]
Iso_typ.ISO [definition, in Tutorial_STLC_Iso]
Iso_typ.RR [definition, in Tutorial_STLC_Iso]
Iso_typ.RR [definition, in LNameless_STLC_Iso]
Iso_typ.RR [definition, in deBruijn_Fsub_Iso]
Iso_typ.RR [definition, in LNameless_Fsub_Iso]
Iso_typ.To [definition, in LNameless_STLC_Iso]
Iso_typ.To [definition, in LNameless_Fsub_Iso]
Iso_typ.To [definition, in deBruijn_Fsub_Iso]
Iso_typ.To [definition, in Tutorial_STLC_Iso]
Iso_typ.To_ [definition, in LNameless_STLC_Iso]
Iso_typ.To_ [definition, in deBruijn_Fsub_Iso]
Iso_typ.To_ [definition, in Tutorial_STLC_Iso]
Iso_typ.To_ [definition, in LNameless_Fsub_Iso]
Iso_typ.To_From [lemma, in LNameless_Fsub_Iso]
Iso_typ.To_From [lemma, in LNameless_STLC_Iso]
Iso_typ.To_From [lemma, in deBruijn_Fsub_Iso]
Iso_typ.To_From [lemma, in Tutorial_STLC_Iso]
Iso_typ.To_inj [lemma, in LNameless_Fsub_Iso]
Iso_typ.To_inj [lemma, in deBruijn_Fsub_Iso]
Iso_typ.TT [definition, in LNameless_STLC_Iso]
Iso_typ.TT [definition, in Tutorial_STLC_Iso]
Iso_typ.TT [definition, in LNameless_Fsub_Iso]
Iso_typ.TT [definition, in deBruijn_Fsub_Iso]
Iso_typ_REC [lemma, in LNameless_Fsub_Iso]
Iso_typ_REC [lemma, in LNameless_STLC_Iso]
Iso_typ_REC [lemma, in deBruijn_Fsub_Iso]
K
KeySetFacts [module, in AssocList]KeySetProperties [module, in AssocList]
L
lelistA_dec [lemma, in CoqListFacts]lelistA_unique [lemma, in CoqListFacts]
le_max_S_l [lemma, in Arith_Max_extra]
le_max_S_r [lemma, in Arith_Max_extra]
LibTactics [library]
list_rev [definition, in CoqUniquenessTac]
LNameless [module, in LNameless_Meta]
LNameless_Fsub_Iso [library]
LNameless_Isomorphism [library]
LNameless_Meta [library]
LNameless_Meta_Env [library]
LNameless_STLC_Iso [library]
LNTemplate [module, in LN_Template]
LNTemplate.env_fv [definition, in LN_Template]
LNTemplate.env_fv_no_occur [lemma, in LN_Template]
LNTemplate.From_Tbsubst [lemma, in LN_Template]
LNTemplate.From_Tbsubst_var [lemma, in LN_Template]
LNTemplate.From_Tfsubst [lemma, in LN_Template]
LNTemplate.From_Tfsubst_var [lemma, in LN_Template]
LNTemplate.gTwf [definition, in LN_Template]
LNTemplate.gTwf_basic [definition, in LN_Template]
LNTemplate.gTwf_from_Twf_basic [lemma, in LN_Template]
LNTemplate.gTwf_Twf [lemma, in LN_Template]
LNTemplate.gTwf_Twf_basic [lemma, in LN_Template]
LNTemplate.iso_env_map [lemma, in LN_Template]
LNTemplate.noRepr_Tbsubst [lemma, in LN_Template]
LNTemplate.noRepr_Tfsubst [lemma, in LN_Template]
LNTemplate.noRepr_Tfv [lemma, in LN_Template]
LNTemplate.noRepr_Twf [lemma, in LN_Template]
LNTemplate.noRepr_TwfT [lemma, in LN_Template]
LNTemplate.Tbfsubst_var_intro [lemma, in LN_Template]
LNTemplate.Tbsubst [definition, in LN_Template]
LNTemplate.Tbsubst_homo [lemma, in LN_Template]
LNTemplate.Tbsubst_homo_core [lemma, in LN_Template]
LNTemplate.Tbsubst_var_twice [lemma, in LN_Template]
LNTemplate.Tfsubst [definition, in LN_Template]
LNTemplate.Tfsubst_no_occur [lemma, in LN_Template]
LNTemplate.Tfsubst_self [lemma, in LN_Template]
LNTemplate.Tfv [definition, in LN_Template]
LNTemplate.Tfv_pass_binder [lemma, in LN_Template]
LNTemplate.Tfv_pass_binder_1 [lemma, in LN_Template]
LNTemplate.TSize [definition, in LN_Template]
LNTemplate.TSize_Tbsubst [lemma, in LN_Template]
LNTemplate.Twf [definition, in LN_Template]
LNTemplate.TwfT [definition, in LN_Template]
LNTemplate.TwfT_Twf [lemma, in LN_Template]
LNTemplate.Twf_basic [definition, in LN_Template]
LNTemplate.Twf_basic_from_gTwf [lemma, in LN_Template]
LNTemplate.Twf_basic_from_Twf [lemma, in LN_Template]
LNTemplate.Twf_from_Twf_basic [lemma, in LN_Template]
LNTemplate.Twf_gTwf [lemma, in LN_Template]
LNTemplate.Twf_gTwf_basic [lemma, in LN_Template]
LN_Fsub_adv_Definitions [library]
LN_Fsub_adv_Infrastructure [library]
LN_Fsub_adv_Soundness [library]
LN_Fsub_basic_Definitions [library]
LN_Fsub_basic_Infrastructure [library]
LN_Fsub_basic_Soundness [library]
LN_STLC_basic_Definitions [library]
LN_STLC_basic_Infrastructure [library]
LN_STLC_basic_Soundness [library]
LN_Template [library]
LN_Template_One_Sort [library]
LN_Template_Two_Sort [library]
local_preservation_app [lemma, in dB_Fsub_basic_Main]
local_preservation_tapp [lemma, in dB_Fsub_basic_Main]
local_progress [lemma, in dB_Fsub_basic_Main]
lth [definition, in deBruijn_Meta_Env]
lth_preserving [lemma, in deBruijn_Meta_Env]
lt_max_SS_l [lemma, in Arith_Max_extra]
lt_max_SS_r [lemma, in Arith_Max_extra]
lt_max_S_l [lemma, in Arith_Max_extra]
lt_max_S_r [lemma, in Arith_Max_extra]
lt_SS_max_l [lemma, in Arith_Max_extra]
lt_SS_max_r [lemma, in Arith_Max_extra]
lt_S_max_l [lemma, in Arith_Max_extra]
lt_S_max_r [lemma, in Arith_Max_extra]
M
M [module, in LN_Template]M [module, in LN_Template]
Make [module, in FSetExtra]
Make [module, in AssocList]
Make.alist_ind [lemma, in AssocList]
Make.app_assoc [lemma, in AssocList]
Make.app_assoc_map_push [lemma, in AssocList]
Make.app_eq_one [lemma, in AssocList]
Make.app_nil_1 [lemma, in AssocList]
Make.app_nil_2 [lemma, in AssocList]
Make.AssortedListProperties [section, in AssocList]
Make.AssortedListProperties.x [variable, in AssocList]
Make.AssortedListProperties.X [variable, in AssocList]
Make.AssortedListProperties.xs [variable, in AssocList]
Make.AssortedListProperties.ys [variable, in AssocList]
Make.AssortedListProperties.zs [variable, in AssocList]
Make.binds [definition, in AssocList]
Make.BindsDerived [section, in AssocList]
Make.BindsDerived.a [variable, in AssocList]
Make.BindsDerived.A [variable, in AssocList]
Make.BindsDerived.b [variable, in AssocList]
Make.BindsDerived.B [variable, in AssocList]
Make.BindsDerived.E [variable, in AssocList]
Make.BindsDerived.F [variable, in AssocList]
Make.BindsDerived.f [variable, in AssocList]
Make.BindsDerived.G [variable, in AssocList]
Make.BindsDerived.x [variable, in AssocList]
Make.BindsDerived.y [variable, in AssocList]
Make.BindsProperties [section, in AssocList]
Make.BindsProperties.A [variable, in AssocList]
Make.BindsProperties.a [variable, in AssocList]
Make.BindsProperties.B [variable, in AssocList]
Make.BindsProperties.b [variable, in AssocList]
Make.BindsProperties.E [variable, in AssocList]
Make.BindsProperties.f [variable, in AssocList]
Make.BindsProperties.F [variable, in AssocList]
Make.BindsProperties.G [variable, in AssocList]
Make.BindsProperties.x [variable, in AssocList]
Make.BindsProperties.y [variable, in AssocList]
Make.BindsProperties2 [section, in AssocList]
Make.BindsProperties2.a [variable, in AssocList]
Make.BindsProperties2.A [variable, in AssocList]
Make.BindsProperties2.B [variable, in AssocList]
Make.BindsProperties2.b [variable, in AssocList]
Make.BindsProperties2.E [variable, in AssocList]
Make.BindsProperties2.f [variable, in AssocList]
Make.BindsProperties2.F [variable, in AssocList]
Make.BindsProperties2.G [variable, in AssocList]
Make.BindsProperties2.x [variable, in AssocList]
Make.BindsProperties2.y [variable, in AssocList]
Make.binds_app_iff [lemma, in AssocList]
Make.binds_app_uniq_iff [lemma, in AssocList]
Make.binds_app_uniq_1 [lemma, in AssocList]
Make.binds_app_1 [lemma, in AssocList]
Make.binds_app_2 [lemma, in AssocList]
Make.binds_app_3 [lemma, in AssocList]
Make.binds_cons_iff [lemma, in AssocList]
Make.binds_cons_uniq_iff [lemma, in AssocList]
Make.binds_cons_uniq_1 [lemma, in AssocList]
Make.binds_cons_1 [lemma, in AssocList]
Make.binds_cons_2 [lemma, in AssocList]
Make.binds_cons_3 [lemma, in AssocList]
Make.binds_cons_4 [lemma, in AssocList]
Make.binds_dec [lemma, in AssocList]
Make.binds_dom_contradiction [lemma, in AssocList]
Make.binds_head [lemma, in AssocList]
Make.binds_In [lemma, in AssocList]
Make.binds_In_inv [lemma, in AssocList]
Make.binds_lookup [lemma, in AssocList]
Make.binds_lookup_dec [lemma, in AssocList]
Make.binds_map_1 [lemma, in AssocList]
Make.binds_map_2 [lemma, in AssocList]
Make.binds_mid_eq [lemma, in AssocList]
Make.binds_nil_iff [lemma, in AssocList]
Make.binds_one_iff [lemma, in AssocList]
Make.binds_one_1 [lemma, in AssocList]
Make.binds_one_2 [lemma, in AssocList]
Make.binds_one_3 [lemma, in AssocList]
Make.binds_remove_mid [lemma, in AssocList]
Make.binds_unique [lemma, in AssocList]
Make.binds_weaken [lemma, in AssocList]
Make.cons_app_assoc [lemma, in AssocList]
Make.cons_app_one [lemma, in AssocList]
Make.disjoint [definition, in AssocList]
Make.disjoint [definition, in FSetExtra]
Make.Disjoint [section, in AssocList]
Make.disjoint_app_l [lemma, in AssocList]
Make.disjoint_app_r [lemma, in AssocList]
Make.disjoint_app_1 [lemma, in AssocList]
Make.disjoint_app_2 [lemma, in AssocList]
Make.disjoint_app_3 [lemma, in AssocList]
Make.disjoint_cons_l [lemma, in AssocList]
Make.disjoint_cons_r [lemma, in AssocList]
Make.disjoint_cons_1 [lemma, in AssocList]
Make.disjoint_cons_2 [lemma, in AssocList]
Make.disjoint_cons_3 [lemma, in AssocList]
Make.disjoint_map_l [lemma, in AssocList]
Make.disjoint_map_r [lemma, in AssocList]
Make.disjoint_map_1 [lemma, in AssocList]
Make.disjoint_map_2 [lemma, in AssocList]
Make.disjoint_nil_1 [lemma, in AssocList]
Make.disjoint_one_l [lemma, in AssocList]
Make.disjoint_one_r [lemma, in AssocList]
Make.disjoint_one_1 [lemma, in AssocList]
Make.disjoint_one_2 [lemma, in AssocList]
Make.disjoint_sym [lemma, in AssocList]
Make.disjoint_sym_1 [lemma, in AssocList]
Make.dom [definition, in AssocList]
Make.dom_app [lemma, in AssocList]
Make.dom_cons [lemma, in AssocList]
Make.dom_map [lemma, in AssocList]
Make.dom_nil [lemma, in AssocList]
Make.dom_one [lemma, in AssocList]
Make.dom_push [lemma, in AssocList]
Make.eq_push_inv [lemma, in AssocList]
Make.fresh_app_l [lemma, in AssocList]
Make.fresh_app_r [lemma, in AssocList]
Make.fresh_list [definition, in FSetExtra]
Make.fresh_mid_head [lemma, in AssocList]
Make.fresh_mid_tail [lemma, in AssocList]
Make.get [definition, in AssocList]
Make.in_app_iff [lemma, in AssocList]
Make.in_nil_iff [lemma, in AssocList]
Make.in_one_iff [lemma, in AssocList]
Make.ListProperties [section, in AssocList]
Make.ListProperties.l [variable, in AssocList]
Make.ListProperties.l1 [variable, in AssocList]
Make.ListProperties.l2 [variable, in AssocList]
Make.ListProperties.l3 [variable, in AssocList]
Make.ListProperties.x [variable, in AssocList]
Make.ListProperties.X [variable, in AssocList]
Make.ListProperties.y [variable, in AssocList]
Make.map [definition, in AssocList]
Make.maps [definition, in AssocList]
Make.map_app [lemma, in AssocList]
Make.map_cons [lemma, in AssocList]
Make.map_nil [lemma, in AssocList]
Make.map_one [lemma, in AssocList]
Make.nil_neq_one_mid [lemma, in AssocList]
Make.notin [definition, in FSetExtra]
Make.one [definition, in AssocList]
Make.one_eq_app [lemma, in AssocList]
Make.one_mid_neq_nil [lemma, in AssocList]
Make.Properties [section, in AssocList]
Make.Properties.a [variable, in AssocList]
Make.Properties.A [variable, in AssocList]
Make.Properties.b [variable, in AssocList]
Make.Properties.B [variable, in AssocList]
Make.Properties.c [variable, in AssocList]
Make.Properties.E [variable, in AssocList]
Make.Properties.F [variable, in AssocList]
Make.Properties.f [variable, in AssocList]
Make.Properties.g [variable, in AssocList]
Make.Properties.G [variable, in AssocList]
Make.Properties.key [variable, in AssocList]
Make.Properties.x [variable, in AssocList]
Make.Properties.y [variable, in AssocList]
Make.uniq [inductive, in AssocList]
Make.UniqDerived [section, in AssocList]
Make.UniqDerived.A [variable, in AssocList]
Make.UniqDerived.a [variable, in AssocList]
Make.UniqDerived.b [variable, in AssocList]
Make.UniqDerived.E [variable, in AssocList]
Make.UniqDerived.F [variable, in AssocList]
Make.UniqDerived.G [variable, in AssocList]
Make.UniqDerived.x [variable, in AssocList]
Make.UniqDerived.y [variable, in AssocList]
Make.UniqProperties [section, in AssocList]
Make.UniqProperties.a [variable, in AssocList]
Make.UniqProperties.A [variable, in AssocList]
Make.UniqProperties.b [variable, in AssocList]
Make.UniqProperties.B [variable, in AssocList]
Make.UniqProperties.E [variable, in AssocList]
Make.UniqProperties.F [variable, in AssocList]
Make.UniqProperties.f [variable, in AssocList]
Make.UniqProperties.G [variable, in AssocList]
Make.UniqProperties.x [variable, in AssocList]
Make.uniq_app_iff [lemma, in AssocList]
Make.uniq_app_1 [lemma, in AssocList]
Make.uniq_app_2 [lemma, in AssocList]
Make.uniq_app_3 [lemma, in AssocList]
Make.uniq_app_4 [lemma, in AssocList]
Make.uniq_cons_iff [lemma, in AssocList]
Make.uniq_cons_1 [lemma, in AssocList]
Make.uniq_cons_2 [lemma, in AssocList]
Make.uniq_cons_3 [lemma, in AssocList]
Make.uniq_dom_only [lemma, in AssocList]
Make.uniq_dom_only_1 [lemma, in AssocList]
Make.uniq_insert_mid [lemma, in AssocList]
Make.uniq_map_app_1 [lemma, in AssocList]
Make.uniq_map_app_2 [lemma, in AssocList]
Make.uniq_map_iff [lemma, in AssocList]
Make.uniq_map_1 [lemma, in AssocList]
Make.uniq_map_2 [lemma, in AssocList]
Make.uniq_nil [constructor, in AssocList]
Make.uniq_one_1 [lemma, in AssocList]
Make.uniq_push [constructor, in AssocList]
Make.uniq_remove_mid [lemma, in AssocList]
Make.uniq_reorder_1 [lemma, in AssocList]
Make.uniq_reorder_2 [lemma, in AssocList]
Mapping_Env [section, in Metatheory_Env]
Mapping_Env.A [variable, in Metatheory_Env]
Mapping_Env.B [variable, in Metatheory_Env]
Mapping_Env.f [variable, in Metatheory_Env]
Mapping_Env.g [variable, in Metatheory_Env]
map_extends_1 [lemma, in Metatheory_Env]
map_extends_2 [lemma, in Metatheory_Env]
map_subst_tb_id [lemma, in LN_Fsub_basic_Infrastructure]
map_uniq_1 [lemma, in Metatheory_Env]
map_uniq_2 [lemma, in Metatheory_Env]
map_uniq_3 [lemma, in Metatheory_Env]
map_uniq_4 [lemma, in Metatheory_Env]
map_uniq_5 [lemma, in Metatheory_Env]
max_lt_1 [lemma, in Arith_Max_extra]
max_lt_2 [lemma, in Arith_Max_extra]
MetatheoryAtom [library]
Metatheory_Env [library]
Metatheory_Var [library]
modus_ponens [lemma, in LibTactics]
MT [module, in dB_Template_Two_Sort]
MT [module, in LN_Template_One_Sort]
MT [module, in LN_Template_Two_Sort]
MY [module, in LN_Template_One_Sort]
MY [module, in LN_Template_Two_Sort]
MY [module, in dB_Template_Two_Sort]
M_tt [module, in LN_Template_One_Sort]
M_tt [module, in dB_Template_Two_Sort]
M_tt [module, in LN_Template_Two_Sort]
M_ty [module, in dB_Template_Two_Sort]
M_ty [module, in LN_Template_Two_Sort]
M_yt [module, in LN_Template_Two_Sort]
M_yt [module, in dB_Template_Two_Sort]
M_yt [module, in LN_Template_One_Sort]
M_yy [module, in dB_Template_Two_Sort]
M_yy [module, in LN_Template_Two_Sort]
N
narrow [inductive, in dB_Fsub_basic_Main]narrowing_case [lemma, in dB_Fsub_basic_Main]
narrowing_prop [definition, in dB_Fsub_basic_Main]
NarrowTrans [section, in LN_Fsub_basic_Soundness]
NarrowTrans [section, in LN_Fsub_adv_Soundness]
narrow_extend_left [constructor, in dB_Fsub_basic_Main]
narrow_extend_right [constructor, in dB_Fsub_basic_Main]
narrow_wf_env [lemma, in dB_Fsub_basic_Main]
narrow_wf_typ [lemma, in dB_Fsub_basic_Main]
narrow_0 [constructor, in dB_Fsub_basic_Main]
Nat [module, in Variable_Sets]
nil_eq_app [lemma, in CoqListFacts]
noRepr [definition, in DGP_Core]
noRepr_bsubstRep_hetero [lemma, in LNameless_Meta_Env]
noRepr_bsubst_hetero [lemma, in LNameless_Meta_Env]
noRepr_envTRep_hetero [lemma, in LNameless_Meta_Env]
noRepr_envT_fsubst [lemma, in LNameless_Meta_Env]
noRepr_envT_fsubstRep [lemma, in LNameless_Meta_Env]
noRepr_envT_fsubstRep_ [lemma, in LNameless_Meta_Env]
noRepr_envT_fsubst_ [lemma, in LNameless_Meta_Env]
noRepr_envT_hetero [lemma, in LNameless_Meta_Env]
noRepr_freevarsRep_hetero [lemma, in LNameless_Meta_Env]
noRepr_freevars_hetero [lemma, in LNameless_Meta_Env]
noRepr_fsubstRep_hetero [lemma, in LNameless_Meta_Env]
noRepr_fsubst_hetero [lemma, in LNameless_Meta_Env]
noRepr_shiftRep_hetero [lemma, in deBruijn_Meta]
noRepr_shift_hetero [lemma, in deBruijn_Meta]
noRepr_shift_preserves_size [lemma, in deBruijn_Meta]
noRepr_shift_preserves_sizeRep [lemma, in deBruijn_Meta]
noRepr_shift_shift [lemma, in deBruijn_Meta]
noRepr_shift_shiftRep [lemma, in deBruijn_Meta]
noRepr_shift_substRep_1 [lemma, in deBruijn_Meta]
noRepr_shift_substRep_2 [lemma, in deBruijn_Meta]
noRepr_shift_subst_1 [lemma, in deBruijn_Meta]
noRepr_shift_subst_2 [lemma, in deBruijn_Meta]
noRepr_substRep_hetero [lemma, in deBruijn_Meta]
noRepr_subst_hetero [lemma, in deBruijn_Meta]
noRepr_subst_shift [lemma, in deBruijn_Meta]
noRepr_subst_shiftRep [lemma, in deBruijn_Meta]
noRepr_subst_subst [lemma, in deBruijn_Meta]
noRepr_subst_substRep [lemma, in deBruijn_Meta]
noRepr_THbfsubst_permutation_var [lemma, in LN_Template_Two_Sort]
noRepr_THbfsubst_permutation_var_1 [lemma, in LN_Template_Two_Sort]
noRepr_THbfsubst_permutation_var_1_wf [lemma, in LN_Template_Two_Sort]
noRepr_TTwfT_THfsubst [lemma, in LN_Template_Two_Sort]
noRepr_TTwf_THfsubst [lemma, in LN_Template_Two_Sort]
noRepr_wfRep_hetero [lemma, in LNameless_Meta_Env]
noRepr_wfTRep_hetero [lemma, in LNameless_Meta_Env]
noRepr_wfT_hetero [lemma, in LNameless_Meta_Env]
noRepr_wf_env_fsubst [lemma, in LNameless_Meta_Env]
noRepr_wf_hetero [lemma, in LNameless_Meta_Env]
noRepr_YenvT_Yfsubst [lemma, in LN_Template_Two_Sort]
noRepr_Yshift_preserves_Ysize [lemma, in dB_Template_Two_Sort]
noRepr_Yshift_Yshift [lemma, in dB_Template_Two_Sort]
noRepr_Yshift_Ysubst_1 [lemma, in dB_Template_Two_Sort]
noRepr_Yshift_Ysubst_2 [lemma, in dB_Template_Two_Sort]
noRepr_Ysubst_Yshift [lemma, in dB_Template_Two_Sort]
noRepr_Ysubst_Ysubst [lemma, in dB_Template_Two_Sort]
noRepr_YTenvT_Yfsubst [lemma, in LN_Template_Two_Sort]
noRepr_YTenvT_Yfsubst_left [lemma, in LN_Template_Two_Sort]
noRepr_YTwf_env_Yfsubst [lemma, in LN_Template_Two_Sort]
noRepr_YTwf_env_Yfsubst_left [lemma, in LN_Template_Two_Sort]
noRepr_Ywf_env_Yfsubst [lemma, in LN_Template_Two_Sort]
notin_app_1 [lemma, in Metatheory_Env]
notin_app_2 [lemma, in Metatheory_Env]
notin_cons_mid [lemma, in Metatheory_Env]
notin_extra [section, in Metatheory_Env]
Notin_fun [module, in FSetWeakNotin]
Notin_fun.Lemmas [section, in FSetWeakNotin]
Notin_fun.Lemmas.s [variable, in FSetWeakNotin]
Notin_fun.Lemmas.s' [variable, in FSetWeakNotin]
Notin_fun.Lemmas.x [variable, in FSetWeakNotin]
Notin_fun.Lemmas.y [variable, in FSetWeakNotin]
Notin_fun.notin_add_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_1' [lemma, in FSetWeakNotin]
Notin_fun.notin_add_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_empty_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_3' [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_1' [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_3 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_1 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_2 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_3 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_4 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_5 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_6 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_7 [lemma, in FSetWeakNotin]
notin_fv_wf [lemma, in LN_Fsub_basic_Infrastructure]
notin_neq [lemma, in LNameless_Meta_Env]
notin_neq [lemma, in Metatheory_Env]
not_In_app [lemma, in CoqListFacts]
not_In_cons [lemma, in CoqListFacts]
O
okt [inductive, in LN_Fsub_basic_Definitions]okt_empty [constructor, in LN_Fsub_basic_Definitions]
okt_narrow [lemma, in LN_Fsub_basic_Infrastructure]
okt_strengthen [lemma, in LN_Fsub_basic_Infrastructure]
okt_sub [constructor, in LN_Fsub_basic_Definitions]
okt_subst_tb [lemma, in LN_Fsub_basic_Infrastructure]
okt_typ [constructor, in LN_Fsub_basic_Definitions]
ok_from_okt [lemma, in LN_Fsub_basic_Infrastructure]
opt_map [definition, in deBruijn_Meta_Env]
opt_map_none [lemma, in deBruijn_Meta_Env]
opt_map_none_1 [lemma, in deBruijn_Meta_Env]
P
PLUS [constructor, in DGP_Core]preservation [definition, in LN_Fsub_basic_Definitions]
preservation [definition, in LN_Fsub_adv_Definitions]
preservation [definition, in LN_STLC_basic_Definitions]
preservation [lemma, in dB_Fsub_basic_Main]
preservation [definition, in Tutorial_STLC_Formalization]
preservation' [lemma, in dB_Fsub_basic_Main]
preservation_result [lemma, in LN_Fsub_basic_Soundness]
preservation_result [lemma, in LN_STLC_basic_Soundness]
preservation_result [lemma, in LN_Fsub_adv_Soundness]
PROD [constructor, in DGP_Core]
progress [definition, in LN_STLC_basic_Definitions]
progress [definition, in Tutorial_STLC_Formalization]
progress [lemma, in dB_Fsub_basic_Main]
progress [definition, in LN_Fsub_adv_Definitions]
progress [definition, in LN_Fsub_basic_Definitions]
progress' [lemma, in dB_Fsub_basic_Main]
progress_result [lemma, in LN_Fsub_basic_Soundness]
progress_result [lemma, in LN_Fsub_adv_Soundness]
progress_result [lemma, in LN_STLC_basic_Soundness]
PWellformed [module, in LN_Template]
PWellformed.envT_Tfv [lemma, in LN_Template]
PWellformed.extends_TenvT [lemma, in LN_Template]
PWellformed.Tbfsubst_permutation [lemma, in LN_Template]
PWellformed.Tbfsubst_permutation_var [lemma, in LN_Template]
PWellformed.TenvT [definition, in LN_Template]
PWellformed.TenvT_dom_subset [lemma, in LN_Template]
PWellformed.TenvT_narrow [lemma, in LN_Template]
PWellformed.TenvT_narrow_left [lemma, in LN_Template]
PWellformed.TenvT_narrow_right [lemma, in LN_Template]
PWellformed.TenvT_Twf [lemma, in LN_Template]
PWellformed.TenvT_TwfT [lemma, in LN_Template]
PWellformed.TenvT_weaken [lemma, in LN_Template]
PWellformed.TenvT_weaken_left [lemma, in LN_Template]
PWellformed.TenvT_weaken_right [lemma, in LN_Template]
PWellformed.Tfsubst_fresh [lemma, in LN_Template]
Q
QuantificationVarSig [module, in Metatheory_Var]R
REC [constructor, in DGP_Core]red [inductive, in LN_STLC_basic_Definitions]
red [inductive, in LN_Fsub_basic_Definitions]
red [inductive, in dB_Fsub_basic_Main]
red [inductive, in Tutorial_STLC_Formalization]
red [inductive, in LN_Fsub_adv_Definitions]
red' [inductive, in dB_Fsub_basic_Main]
red_abs [constructor, in LN_Fsub_adv_Definitions]
red_abs [constructor, in LN_Fsub_basic_Definitions]
red_app_1 [constructor, in LN_Fsub_adv_Definitions]
red_app_1 [constructor, in Tutorial_STLC_Formalization]
red_app_1 [constructor, in LN_STLC_basic_Definitions]
red_app_1 [constructor, in LN_Fsub_basic_Definitions]
red_app_2 [constructor, in LN_Fsub_adv_Definitions]
red_app_2 [constructor, in LN_Fsub_basic_Definitions]
red_app_2 [constructor, in Tutorial_STLC_Formalization]
red_app_2 [constructor, in LN_STLC_basic_Definitions]
red_beta [constructor, in LN_STLC_basic_Definitions]
red_beta [constructor, in Tutorial_STLC_Formalization]
red_regular [lemma, in LN_Fsub_basic_Infrastructure]
red_regular [lemma, in LN_Fsub_adv_Infrastructure]
red_regular [lemma, in LN_STLC_basic_Infrastructure]
red_tabs [constructor, in LN_Fsub_adv_Definitions]
red_tabs [constructor, in LN_Fsub_basic_Definitions]
red_tapp [constructor, in LN_Fsub_basic_Definitions]
red_tapp [constructor, in LN_Fsub_adv_Definitions]
remove [abbreviation, in Metatheory_Env]
remove_right [definition, in deBruijn_Meta_Env]
Rep [inductive, in DGP_Core]
REPR [constructor, in DGP_Core]
Rep_dec [lemma, in DGP_Core]
Rep_dec_or [lemma, in DGP_Core]
Rep_dec_unicity [lemma, in DGP_Core]
S
S [module, in CoqFSetInterface]SA_All [constructor, in dB_Fsub_basic_Main]
SA_Arrow [constructor, in dB_Fsub_basic_Main]
SA_Refl_TVar [constructor, in dB_Fsub_basic_Main]
SA_Top [constructor, in dB_Fsub_basic_Main]
SA_Trans_TVar [constructor, in dB_Fsub_basic_Main]
Sdep [module, in CoqFSetInterface]
Sdep.add [axiom, in CoqFSetInterface]
Sdep.Add [definition, in CoqFSetInterface]
Sdep.cardinal [axiom, in CoqFSetInterface]
Sdep.choose [axiom, in CoqFSetInterface]
Sdep.choose_equal [axiom, in CoqFSetInterface]
Sdep.compare [axiom, in CoqFSetInterface]
Sdep.diff [axiom, in CoqFSetInterface]
Sdep.elements [axiom, in CoqFSetInterface]
Sdep.elt [definition, in CoqFSetInterface]
Sdep.Empty [definition, in CoqFSetInterface]
Sdep.empty [axiom, in CoqFSetInterface]
Sdep.eq [definition, in CoqFSetInterface]
Sdep.Equal [definition, in CoqFSetInterface]
Sdep.equal [axiom, in CoqFSetInterface]
Sdep.eq_In [axiom, in CoqFSetInterface]
Sdep.eq_refl [axiom, in CoqFSetInterface]
Sdep.eq_sym [axiom, in CoqFSetInterface]
Sdep.eq_trans [axiom, in CoqFSetInterface]
Sdep.Exists [definition, in CoqFSetInterface]
Sdep.exists_ [axiom, in CoqFSetInterface]
Sdep.filter [axiom, in CoqFSetInterface]
Sdep.fold [axiom, in CoqFSetInterface]
Sdep.for_all [axiom, in CoqFSetInterface]
Sdep.For_all [definition, in CoqFSetInterface]
Sdep.In [axiom, in CoqFSetInterface]
Sdep.inter [axiom, in CoqFSetInterface]
Sdep.is_empty [axiom, in CoqFSetInterface]
Sdep.lt [axiom, in CoqFSetInterface]
Sdep.lt_not_eq [axiom, in CoqFSetInterface]
Sdep.lt_trans [axiom, in CoqFSetInterface]
Sdep.max_elt [axiom, in CoqFSetInterface]
Sdep.mem [axiom, in CoqFSetInterface]
Sdep.min_elt [axiom, in CoqFSetInterface]
Sdep.partition [axiom, in CoqFSetInterface]
Sdep.remove [axiom, in CoqFSetInterface]
Sdep.singleton [axiom, in CoqFSetInterface]
Sdep.subset [axiom, in CoqFSetInterface]
Sdep.Subset [definition, in CoqFSetInterface]
Sdep.t [axiom, in CoqFSetInterface]
Sdep.union [axiom, in CoqFSetInterface]
Sfun [module, in CoqFSetInterface]
Sfun.choose_3 [axiom, in CoqFSetInterface]
Sfun.compare [axiom, in CoqFSetInterface]
Sfun.elements_3 [axiom, in CoqFSetInterface]
Sfun.lt [axiom, in CoqFSetInterface]
Sfun.lt_not_eq [axiom, in CoqFSetInterface]
Sfun.lt_trans [axiom, in CoqFSetInterface]
Sfun.max_elt [axiom, in CoqFSetInterface]
Sfun.max_elt_1 [axiom, in CoqFSetInterface]
Sfun.max_elt_2 [axiom, in CoqFSetInterface]
Sfun.max_elt_3 [axiom, in CoqFSetInterface]
Sfun.min_elt [axiom, in CoqFSetInterface]
Sfun.min_elt_1 [axiom, in CoqFSetInterface]
Sfun.min_elt_2 [axiom, in CoqFSetInterface]
Sfun.min_elt_3 [axiom, in CoqFSetInterface]
Sfun.Spec [section, in CoqFSetInterface]
Sfun.Spec.s [variable, in CoqFSetInterface]
Sfun.Spec.s' [variable, in CoqFSetInterface]
Sfun.Spec.s'' [variable, in CoqFSetInterface]
Sfun.Spec.x [variable, in CoqFSetInterface]
Sfun.Spec.y [variable, in CoqFSetInterface]
shift [definition, in deBruijn_Meta]
shiftRep [definition, in deBruijn_Meta]
Single [module, in Variable_Sets]
singleton [abbreviation, in Metatheory_Env]
Single.eq_dec [definition, in Variable_Sets]
Single.t [definition, in Variable_Sets]
skip [axiom, in LibTactics]
Sort [abbreviation, in CoqListFacts]
SortedListEquality [section, in CoqListFacts]
SortedListEquality.A [variable, in CoqListFacts]
SortedListEquality.eqA_ltA [variable, in CoqListFacts]
SortedListEquality.ltA [variable, in CoqListFacts]
SortedListEquality.ltA_eqA [variable, in CoqListFacts]
SortedListEquality.ltA_not_eqA [variable, in CoqListFacts]
SortedListEquality.ltA_trans [variable, in CoqListFacts]
sort_dec [lemma, in CoqListFacts]
Sort_InA_eq [lemma, in CoqListFacts]
Sort_In_eq [lemma, in CoqListFacts]
sort_unique [lemma, in CoqListFacts]
sub [inductive, in LN_Fsub_basic_Definitions]
sub [inductive, in LN_Fsub_adv_Definitions]
sub [inductive, in dB_Fsub_basic_Main]
subst [definition, in deBruijn_Meta]
substRep [definition, in deBruijn_Meta]
subst_preserves_typing [lemma, in dB_Fsub_basic_Main]
subst_tb [definition, in LN_Fsub_basic_Infrastructure]
subst_typ_preserves_typing [lemma, in dB_Fsub_basic_Main]
subst_typ_preserves_typing_ind [lemma, in dB_Fsub_basic_Main]
sub_all [constructor, in LN_Fsub_basic_Definitions]
sub_all [constructor, in LN_Fsub_adv_Definitions]
sub_arrow [constructor, in LN_Fsub_adv_Definitions]
sub_arrow [constructor, in LN_Fsub_basic_Definitions]
sub_extensionality [lemma, in dB_Fsub_basic_Main]
sub_narrowing [lemma, in LN_Fsub_basic_Soundness]
sub_narrowing [lemma, in LN_Fsub_adv_Soundness]
sub_narrowing [lemma, in dB_Fsub_basic_Main]
sub_narrowing_aux [lemma, in LN_Fsub_adv_Soundness]
sub_narrowing_aux [lemma, in LN_Fsub_basic_Soundness]
sub_reflexivity [lemma, in LN_Fsub_adv_Soundness]
sub_reflexivity [lemma, in LN_Fsub_basic_Soundness]
sub_reflexivity [lemma, in dB_Fsub_basic_Main]
sub_refl_tvar [constructor, in LN_Fsub_basic_Definitions]
sub_refl_tvar [constructor, in LN_Fsub_adv_Definitions]
sub_regular [lemma, in LN_Fsub_basic_Infrastructure]
sub_regular [lemma, in LN_Fsub_adv_Infrastructure]
sub_strengthening [lemma, in LN_Fsub_basic_Soundness]
sub_strengthening [lemma, in LN_Fsub_adv_Soundness]
sub_strengthening_right [lemma, in dB_Fsub_basic_Main]
sub_through_subst_tt [lemma, in LN_Fsub_basic_Soundness]
sub_through_subst_tt [lemma, in LN_Fsub_adv_Soundness]
sub_top [constructor, in LN_Fsub_basic_Definitions]
sub_top [constructor, in LN_Fsub_adv_Definitions]
sub_transitivity [lemma, in LN_Fsub_adv_Soundness]
sub_transitivity [lemma, in dB_Fsub_basic_Main]
sub_transitivity [lemma, in LN_Fsub_basic_Soundness]
sub_trans_tvar [constructor, in LN_Fsub_adv_Definitions]
sub_trans_tvar [constructor, in LN_Fsub_basic_Definitions]
sub_typ_indep [lemma, in LN_Fsub_adv_Infrastructure]
sub_weakening [lemma, in LN_Fsub_basic_Soundness]
sub_weakening [lemma, in LN_Fsub_adv_Soundness]
sub_weakening_left [lemma, in dB_Fsub_basic_Main]
sub_weakening_left_ind [lemma, in dB_Fsub_basic_Main]
sub_weakening_right [lemma, in dB_Fsub_basic_Main]
sub_weakening_right_ind [lemma, in dB_Fsub_basic_Main]
sub_wf [lemma, in dB_Fsub_basic_Main]
S_plus_1 [lemma, in Arith_Max_extra]
T
tabs [constructor, in deBruijn_Fsub_Iso]tapp [constructor, in deBruijn_Fsub_Iso]
tapptabs [constructor, in dB_Fsub_basic_Main]
Tbfsubst_permutation [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_core [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_core [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_core_TTwf [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_core_TTwfT [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_core_wf [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_core_wf [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_ind [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_ind [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_ind_wf [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_ind_wf [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_var [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_var [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_var_TTwf [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_var_TTwfT [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_var_wf [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_var_wf [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_var_wfT [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_var_wfT [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_wf [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_wf [lemma, in LN_Template_Two_Sort]
Tbfsubst_permutation_wfT [lemma, in LN_Template_One_Sort]
Tbfsubst_permutation_wfT [lemma, in LN_Template_Two_Sort]
Tbsubst_homo_wf [lemma, in LN_Template_One_Sort]
Tbsubst_homo_wf [lemma, in LN_Template_Two_Sort]
Tbsubst_var_twice [definition, in LN_Template_Two_Sort]
Tbsubst_var_twice_wf [lemma, in LN_Template_One_Sort]
Tbsubst_var_twice_wf [lemma, in LN_Template_Two_Sort]
TenvT_dom_subset [lemma, in LN_Template_Two_Sort]
TenvT_dom_subset [lemma, in LN_Template_One_Sort]
TenvT_Twf [lemma, in LN_Template_One_Sort]
TenvT_Twf [lemma, in LN_Template_Two_Sort]
TenvT_TwfT [lemma, in LN_Template_Two_Sort]
TenvT_TwfT [lemma, in LN_Template_One_Sort]
term [inductive, in LN_Fsub_adv_Definitions]
term [inductive, in deBruijn_Fsub_Iso]
term [inductive, in LN_Fsub_basic_Definitions]
term_abs [constructor, in LN_Fsub_adv_Definitions]
term_abs [constructor, in LN_Fsub_basic_Definitions]
term_app [constructor, in LN_Fsub_adv_Definitions]
term_app [constructor, in LN_Fsub_basic_Definitions]
term_tabs [constructor, in LN_Fsub_basic_Definitions]
term_tabs [constructor, in LN_Fsub_adv_Definitions]
term_tapp [constructor, in LN_Fsub_basic_Definitions]
term_tapp [constructor, in LN_Fsub_adv_Definitions]
term_TTwf [lemma, in LN_Fsub_basic_Infrastructure]
term_TTwfT [lemma, in LN_Fsub_adv_Infrastructure]
term_var [constructor, in LN_Fsub_basic_Definitions]
term_var [constructor, in LN_Fsub_adv_Definitions]
Tfsubst_fresh [lemma, in LN_Template_One_Sort]
Tfsubst_fresh [lemma, in LN_Template_Two_Sort]
Tfsubst_Lemma [lemma, in LN_Template_Two_Sort]
Tfsubst_Lemma [lemma, in LN_Template_One_Sort]
Tget_left [definition, in dB_Template_Two_Sort]
Tget_left_gTget_left [lemma, in dB_Template_Two_Sort]
Tget_left_insert_left_ge [lemma, in dB_Template_Two_Sort]
Tget_left_insert_left_lt [lemma, in dB_Template_Two_Sort]
Tget_left_remove_right [lemma, in dB_Template_Two_Sort]
Tget_left_some_gt [lemma, in dB_Template_Two_Sort]
Tget_right [definition, in dB_Template_Two_Sort]
Tget_right_gTget_right [lemma, in dB_Template_Two_Sort]
Tget_right_insert_left [lemma, in dB_Template_Two_Sort]
Tget_right_remove_right_ge [lemma, in dB_Template_Two_Sort]
Tget_right_remove_right_lt [lemma, in dB_Template_Two_Sort]
Tget_right_wf [lemma, in dB_Template_Two_Sort]
THbfsubst_permutation [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_core [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_core_Ywf [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_ind [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_ind_Ywf [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_var [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_var_wf [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_var_wfT [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_wf [lemma, in LN_Template_Two_Sort]
THbfsubst_permutation_wfT [lemma, in LN_Template_Two_Sort]
THbsubst_hetero [lemma, in LN_Template_Two_Sort]
THbsubst_hetero_core_1 [lemma, in LN_Template_Two_Sort]
THbsubst_hetero_core_2 [lemma, in LN_Template_Two_Sort]
THbsubst_hetero_wf [lemma, in LN_Template_Two_Sort]
THbsubst_homo_wf [lemma, in LN_Template_Two_Sort]
THbsubst_var_twice [definition, in LN_Template_Two_Sort]
THbsubst_var_twice_wf [lemma, in LN_Template_Two_Sort]
THenvT_dom_subset [lemma, in LN_Template_Two_Sort]
THfsubst_fresh [lemma, in LN_Template_Two_Sort]
THfsubst_Lemma [lemma, in LN_Template_Two_Sort]
THwfT_Tbsubst [lemma, in LN_Template_Two_Sort]
THwfT_Tbsubst_1 [lemma, in LN_Template_Two_Sort]
THwfT_Tfsubst [lemma, in LN_Template_Two_Sort]
THwfT_THfsubst [lemma, in LN_Template_Two_Sort]
THwf_Tfsubst [lemma, in LN_Template_Two_Sort]
THwf_THfsubst [lemma, in LN_Template_Two_Sort]
Til_here [constructor, in dB_Template_Two_Sort]
Til_left [constructor, in dB_Template_Two_Sort]
Til_right [constructor, in dB_Template_Two_Sort]
Tinsert_left [inductive, in dB_Template_Two_Sort]
Tinsert_left_gTinsert_left [lemma, in dB_Template_Two_Sort]
Tinsert_left_length [lemma, in dB_Template_Two_Sort]
Tinsert_left_length_1 [lemma, in dB_Template_Two_Sort]
Tinsert_left_wf_env [lemma, in dB_Template_Two_Sort]
Tinsert_left_wf_typ [lemma, in dB_Template_Two_Sort]
Tinsert_T [lemma, in dB_Template_Two_Sort]
Tinsert_T_ind [lemma, in dB_Template_Two_Sort]
Tlth_preserving [lemma, in dB_Template_Two_Sort]
top [constructor, in deBruijn_Fsub_Iso]
transitivity_and_narrowing [lemma, in dB_Fsub_basic_Main]
transitivity_case [lemma, in dB_Fsub_basic_Main]
transitivity_on [definition, in LN_Fsub_basic_Soundness]
transitivity_on [definition, in LN_Fsub_adv_Soundness]
transitivity_prop [definition, in dB_Fsub_basic_Main]
trm [inductive, in Tutorial_STLC_Iso]
trm [inductive, in LNameless_Fsub_Iso]
trm [inductive, in LNameless_STLC_Iso]
trm [inductive, in Tutorial_STLC_Syntax]
trm_abs [constructor, in LNameless_Fsub_Iso]
trm_abs [constructor, in LNameless_STLC_Iso]
trm_abs [constructor, in Tutorial_STLC_Iso]
trm_abs [constructor, in Tutorial_STLC_Syntax]
trm_app [constructor, in Tutorial_STLC_Syntax]
trm_app [constructor, in LNameless_STLC_Iso]
trm_app [constructor, in LNameless_Fsub_Iso]
trm_app [constructor, in Tutorial_STLC_Iso]
trm_bvar [constructor, in LNameless_Fsub_Iso]
trm_bvar [constructor, in LNameless_STLC_Iso]
trm_bvar [constructor, in Tutorial_STLC_Syntax]
trm_bvar [constructor, in Tutorial_STLC_Iso]
trm_fvar [constructor, in Tutorial_STLC_Syntax]
trm_fvar [constructor, in Tutorial_STLC_Iso]
trm_fvar [constructor, in LNameless_Fsub_Iso]
trm_fvar [constructor, in LNameless_STLC_Iso]
trm_tabs [constructor, in LNameless_Fsub_Iso]
trm_tapp [constructor, in LNameless_Fsub_Iso]
trm_typ [lemma, in LNameless_Fsub_Iso]
trm_typ [lemma, in deBruijn_Fsub_Iso]
trm_typ [lemma, in LNameless_STLC_Iso]
tr_list_rev [definition, in CoqUniquenessTac]
tr_tuple_rev [definition, in CoqUniquenessTac]
TSize_Tbsubst [definition, in LN_Template_Two_Sort]
TSize_THbsubst [definition, in LN_Template_Two_Sort]
TTenvT [definition, in LN_Template_Two_Sort]
TTenvT_fv [lemma, in LN_Template_Two_Sort]
TTenvT_narrow [lemma, in LN_Template_Two_Sort]
TTenvT_narrow_left [lemma, in LN_Template_Two_Sort]
TTenvT_narrow_right [lemma, in LN_Template_Two_Sort]
TTenvT_Tfv [lemma, in LN_Template_Two_Sort]
TTenvT_THfv [lemma, in LN_Template_Two_Sort]
TTenvT_weaken [lemma, in LN_Template_Two_Sort]
TTenvT_weaken_left [lemma, in LN_Template_Two_Sort]
TTenvT_weaken_right [lemma, in LN_Template_Two_Sort]
TTwf [definition, in LN_Template_Two_Sort]
TTwfT [definition, in LN_Template_Two_Sort]
TTwfT_term [lemma, in LN_Fsub_adv_Infrastructure]
TTwfT_Tfsubst [lemma, in LN_Template_Two_Sort]
TTwfT_THfsubst [lemma, in LN_Template_Two_Sort]
TTwfT_THwf [lemma, in LN_Template_Two_Sort]
TTwfT_Twf [lemma, in LN_Template_Two_Sort]
TTwf_basic [definition, in LN_Template_Two_Sort]
TTwf_basic_from_TTwf [lemma, in LN_Template_Two_Sort]
TTwf_from_TTwf_basic [lemma, in LN_Template_Two_Sort]
TTwf_gTTwf [lemma, in LN_Template_Two_Sort]
TTwf_gTTwf_basic [lemma, in LN_Template_Two_Sort]
TTwf_term [lemma, in LN_Fsub_basic_Infrastructure]
TTwf_Tfsubst [lemma, in LN_Template_Two_Sort]
TTwf_THfsubst [lemma, in LN_Template_Two_Sort]
tuple [definition, in CoqUniquenessTac]
tuple_rev [definition, in CoqUniquenessTac]
Tutorial_STLC_Formalization [library]
Tutorial_STLC_Iso [library]
Tutorial_STLC_Syntax [library]
tvar [constructor, in deBruijn_Fsub_Iso]
TwfT_abs_inv [lemma, in LN_STLC_basic_Infrastructure]
TwfT_Tfsubst [lemma, in LN_Template_Two_Sort]
TwfT_Tfsubst [lemma, in LN_Template_One_Sort]
TwfT_THbsubst [lemma, in LN_Template_Two_Sort]
TwfT_THbsubst_1 [lemma, in LN_Template_Two_Sort]
TwfT_THfsubst [lemma, in LN_Template_Two_Sort]
twf_nil_top [lemma, in dB_Fsub_basic_Main]
Twf_Tfsubst [lemma, in LN_Template_Two_Sort]
Twf_Tfsubst [lemma, in LN_Template_One_Sort]
Twf_THfsubst [lemma, in LN_Template_Two_Sort]
Twf_typ_env_weaken [lemma, in dB_Template_Two_Sort]
Twf_typ_extensionality [lemma, in dB_Template_Two_Sort]
Twf_typ_weakening_left [lemma, in dB_Template_Two_Sort]
TwoNat [module, in Variable_Sets]
typ [inductive, in deBruijn_Fsub_Iso]
typ [inductive, in LNameless_Fsub_Iso]
typ [inductive, in Tutorial_STLC_Iso]
typ [inductive, in LNameless_STLC_Iso]
typ [inductive, in Tutorial_STLC_Syntax]
type [inductive, in LN_Fsub_basic_Definitions]
type [inductive, in LN_Fsub_adv_Definitions]
typefun [constructor, in dB_Fsub_basic_Main]
typefun_value [lemma, in dB_Fsub_basic_Main]
type_all [constructor, in LN_Fsub_adv_Definitions]
type_all [constructor, in LN_Fsub_basic_Definitions]
type_arrow [constructor, in LN_Fsub_basic_Definitions]
type_arrow [constructor, in LN_Fsub_adv_Definitions]
type_from_wft [lemma, in LN_Fsub_basic_Infrastructure]
type_top [constructor, in LN_Fsub_basic_Definitions]
type_top [constructor, in LN_Fsub_adv_Definitions]
type_var [constructor, in LN_Fsub_adv_Definitions]
type_var [constructor, in LN_Fsub_basic_Definitions]
type_Ywf [lemma, in LN_Fsub_basic_Infrastructure]
type_YwfT [lemma, in LN_Fsub_adv_Infrastructure]
typing [inductive, in Tutorial_STLC_Formalization]
typing [inductive, in LN_Fsub_adv_Definitions]
typing [inductive, in LN_Fsub_basic_Definitions]
typing [inductive, in LN_STLC_basic_Definitions]
typing [inductive, in dB_Fsub_basic_Main]
typing_abs [constructor, in LN_Fsub_adv_Definitions]
typing_abs [constructor, in LN_STLC_basic_Definitions]
typing_abs [constructor, in LN_Fsub_basic_Definitions]
typing_abs [constructor, in Tutorial_STLC_Formalization]
typing_app [constructor, in LN_Fsub_basic_Definitions]
typing_app [constructor, in LN_STLC_basic_Definitions]
typing_app [constructor, in LN_Fsub_adv_Definitions]
typing_app [constructor, in Tutorial_STLC_Formalization]
typing_inv_abs [lemma, in LN_Fsub_basic_Soundness]
typing_inv_abs [lemma, in LN_Fsub_adv_Soundness]
typing_inv_tabs [lemma, in LN_Fsub_basic_Soundness]
typing_inv_tabs [lemma, in LN_Fsub_adv_Soundness]
typing_narrowing [lemma, in LN_Fsub_adv_Soundness]
typing_narrowing [lemma, in dB_Fsub_basic_Main]
typing_narrowing [lemma, in LN_Fsub_basic_Soundness]
typing_narrowing_ind [lemma, in dB_Fsub_basic_Main]
typing_regular [lemma, in LN_Fsub_adv_Infrastructure]
typing_regular [lemma, in LN_Fsub_basic_Infrastructure]
typing_regular [lemma, in LN_STLC_basic_Infrastructure]
typing_sub [constructor, in LN_Fsub_adv_Definitions]
typing_sub [constructor, in LN_Fsub_basic_Definitions]
typing_subst [lemma, in LN_STLC_basic_Soundness]
typing_tabs [constructor, in LN_Fsub_adv_Definitions]
typing_tabs [constructor, in LN_Fsub_basic_Definitions]
typing_tapp [constructor, in LN_Fsub_adv_Definitions]
typing_tapp [constructor, in LN_Fsub_basic_Definitions]
typing_through_subst_ee [lemma, in LN_Fsub_basic_Soundness]
typing_through_subst_ee [lemma, in LN_Fsub_adv_Soundness]
typing_through_subst_te [lemma, in LN_Fsub_basic_Soundness]
typing_through_subst_te [lemma, in LN_Fsub_adv_Soundness]
typing_var [constructor, in LN_Fsub_basic_Definitions]
typing_var [constructor, in LN_Fsub_adv_Definitions]
typing_var [constructor, in LN_STLC_basic_Definitions]
typing_var [constructor, in Tutorial_STLC_Formalization]
typing_weaken [lemma, in LN_STLC_basic_Soundness]
typing_weakening [lemma, in LN_Fsub_basic_Soundness]
typing_weakening_left [lemma, in dB_Fsub_basic_Main]
typing_weakening_left_ind [lemma, in dB_Fsub_basic_Main]
typing_weakening_right [lemma, in dB_Fsub_basic_Main]
typing_weakening_right_ind [lemma, in dB_Fsub_basic_Main]
typing_weakening_sub [lemma, in LN_Fsub_adv_Soundness]
typing_weakening_typ [lemma, in LN_Fsub_adv_Soundness]
typing_wf [lemma, in dB_Fsub_basic_Main]
typ_all [constructor, in LNameless_Fsub_Iso]
typ_arrow [constructor, in Tutorial_STLC_Syntax]
typ_arrow [constructor, in LNameless_STLC_Iso]
typ_arrow [constructor, in LNameless_Fsub_Iso]
typ_arrow [constructor, in Tutorial_STLC_Iso]
typ_bvar [constructor, in LNameless_Fsub_Iso]
typ_fvar [constructor, in LNameless_Fsub_Iso]
typ_noRepr [lemma, in deBruijn_Fsub_Iso]
typ_noRepr [lemma, in LNameless_Fsub_Iso]
typ_noRepr [lemma, in LNameless_STLC_Iso]
typ_top [constructor, in LNameless_Fsub_Iso]
typ_var [constructor, in Tutorial_STLC_Syntax]
typ_var [constructor, in Tutorial_STLC_Iso]
typ_var [constructor, in LNameless_STLC_Iso]
T_Abs [constructor, in dB_Fsub_basic_Main]
t_abs_inversion [lemma, in dB_Fsub_basic_Main]
T_App [constructor, in dB_Fsub_basic_Main]
T_Sub [constructor, in dB_Fsub_basic_Main]
T_Tabs [constructor, in dB_Fsub_basic_Main]
t_tabs_inversion [lemma, in dB_Fsub_basic_Main]
T_Tapp [constructor, in dB_Fsub_basic_Main]
T_Var [constructor, in dB_Fsub_basic_Main]
U
union [abbreviation, in Metatheory_Env]Uniqueness_Of_SetoidList_Proofs [section, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.A [variable, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.list_eq_dec [variable, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R [variable, in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R_unique [variable, in CoqListFacts]
uniq_dom_only [lemma, in LNameless_Meta_Env]
uniq_from_wf_env [lemma, in LNameless_Meta_Env]
uniq_from_YTwf_env_1 [lemma, in LN_Template_Two_Sort]
uniq_from_YTwf_env_2 [lemma, in LN_Template_Two_Sort]
UNIT [constructor, in DGP_Core]
V
value [inductive, in Tutorial_STLC_Formalization]value [definition, in dB_Fsub_basic_Main]
value [inductive, in LN_STLC_basic_Definitions]
value [inductive, in LN_Fsub_adv_Definitions]
value [inductive, in LN_Fsub_basic_Definitions]
value_abs [constructor, in Tutorial_STLC_Formalization]
value_abs [constructor, in LN_STLC_basic_Definitions]
value_abs [constructor, in LN_Fsub_adv_Definitions]
value_abs [constructor, in LN_Fsub_basic_Definitions]
value_regular [lemma, in LN_STLC_basic_Infrastructure]
value_regular [lemma, in LN_Fsub_adv_Infrastructure]
value_regular [lemma, in LN_Fsub_basic_Infrastructure]
value_tabs [constructor, in LN_Fsub_basic_Definitions]
value_tabs [constructor, in LN_Fsub_adv_Definitions]
var [abbreviation, in LNameless_STLC_Iso]
var [abbreviation, in Tutorial_STLC_Iso]
var [constructor, in deBruijn_Fsub_Iso]
var [abbreviation, in LNameless_Fsub_Iso]
Variable_Sets [library]
W
WDecide [module, in CoqFSetDecide]WDecide_fun [module, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [inductive, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [inductive, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_4 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [lemma, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [lemma, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [lemma, in CoqFSetDecide]
wf [definition, in LNameless_Meta]
wfRep [definition, in LNameless_Meta]
wfRep_basic [definition, in LNameless_Meta]
wft [inductive, in LN_Fsub_adv_Definitions]
wfT [inductive, in LNameless_Meta]
wft [inductive, in LN_Fsub_basic_Definitions]
wfTRep [inductive, in LNameless_Meta]
wfTRep_wfRep [lemma, in LNameless_Meta]
wft_all [constructor, in LN_Fsub_basic_Definitions]
wft_all [constructor, in LN_Fsub_adv_Definitions]
wft_arrow [constructor, in LN_Fsub_basic_Definitions]
wft_arrow [constructor, in LN_Fsub_adv_Definitions]
wfT_bsubstRep_hetero [lemma, in LNameless_Meta]
wfT_bsubstRep_hetero_ [lemma, in LNameless_Meta]
wfT_bsubstRep_hetero_1 [lemma, in LNameless_Meta]
wfT_bsubst_hetero [lemma, in LNameless_Meta]
wfT_bsubst_hetero_ [lemma, in LNameless_Meta]
wfT_bsubst_hetero_1 [lemma, in LNameless_Meta]
wft_from_env_has_sub [lemma, in LN_Fsub_basic_Infrastructure]
wft_from_env_has_typ [lemma, in LN_Fsub_basic_Infrastructure]
wft_from_okt_sub [lemma, in LN_Fsub_basic_Infrastructure]
wft_from_okt_typ [lemma, in LN_Fsub_basic_Infrastructure]
wfT_fsubst [lemma, in LNameless_Meta]
wfT_fsubstRep [lemma, in LNameless_Meta]
wft_narrow [lemma, in LN_Fsub_basic_Infrastructure]
wft_open [lemma, in LN_Fsub_adv_Infrastructure]
wft_open [lemma, in LN_Fsub_basic_Infrastructure]
wft_strengthen [lemma, in LN_Fsub_basic_Infrastructure]
wft_subst_tb [lemma, in LN_Fsub_basic_Infrastructure]
wft_top [constructor, in LN_Fsub_basic_Definitions]
wft_top [constructor, in LN_Fsub_adv_Definitions]
wft_var [constructor, in LN_Fsub_adv_Definitions]
wft_var [constructor, in LN_Fsub_basic_Definitions]
wft_weaken [lemma, in LN_Fsub_basic_Infrastructure]
wft_weaken_right [lemma, in LN_Fsub_basic_Infrastructure]
wfT_wf [lemma, in LNameless_Meta]
wft_YTenvT [lemma, in LN_Fsub_adv_Infrastructure]
wf_basic [definition, in LNameless_Meta]
wf_Bind_hetero [constructor, in LNameless_Meta]
wf_Bind_homo [constructor, in LNameless_Meta]
wf_Bind_REC_hetero [constructor, in LNameless_Meta]
wf_Bind_REC_homo [constructor, in LNameless_Meta]
wf_Const [constructor, in LNameless_Meta]
wf_env [inductive, in LNameless_Meta_Env]
wf_env [definition, in deBruijn_Meta_Env]
wf_env_binds [lemma, in LNameless_Meta_Env]
wf_env_cons [constructor, in LNameless_Meta_Env]
wf_env_empty [constructor, in LNameless_Meta_Env]
wf_env_narrow [lemma, in LNameless_Meta_Env]
wf_env_narrow_left [lemma, in LNameless_Meta_Env]
wf_env_remove_right [lemma, in deBruijn_Meta_Env]
wf_from_wf_basic [lemma, in LNameless_Meta]
wf_fsubst [lemma, in LNameless_Meta]
wf_fsubstRep [lemma, in LNameless_Meta]
wf_fsubstRep_ [lemma, in LNameless_Meta]
wf_fsubst_ [lemma, in LNameless_Meta]
wf_fvar [constructor, in LNameless_Meta]
wf_InL [constructor, in LNameless_Meta]
wf_InR [constructor, in LNameless_Meta]
wf_Pair [constructor, in LNameless_Meta]
wf_parameter [lemma, in LNameless_Meta]
wf_Rec [constructor, in LNameless_Meta]
wf_Repr [constructor, in LNameless_Meta]
wf_term [definition, in dB_Fsub_basic_Main]
wf_Term [constructor, in LNameless_Meta]
wf_Unit [constructor, in LNameless_Meta]
wf_Var [constructor, in LNameless_Meta]
WS [module, in CoqFSetInterface]
WSfun [module, in FSetExtra]
WSfun [module, in CoqFSetInterface]
WSfun.add [axiom, in CoqFSetInterface]
WSfun.add_1 [axiom, in CoqFSetInterface]
WSfun.add_2 [axiom, in CoqFSetInterface]
WSfun.add_3 [axiom, in CoqFSetInterface]
WSfun.cardinal [axiom, in CoqFSetInterface]
WSfun.cardinal_1 [axiom, in CoqFSetInterface]
WSfun.choose [axiom, in CoqFSetInterface]
WSfun.choose_1 [axiom, in CoqFSetInterface]
WSfun.choose_2 [axiom, in CoqFSetInterface]
WSfun.diff [axiom, in CoqFSetInterface]
WSfun.diff_1 [axiom, in CoqFSetInterface]
WSfun.diff_2 [axiom, in CoqFSetInterface]
WSfun.diff_3 [axiom, in CoqFSetInterface]
WSfun.disjoint [definition, in FSetExtra]
WSfun.elements [axiom, in CoqFSetInterface]
WSfun.elements_1 [axiom, in CoqFSetInterface]
WSfun.elements_2 [axiom, in CoqFSetInterface]
WSfun.elements_3w [axiom, in CoqFSetInterface]
WSfun.elt [definition, in CoqFSetInterface]
WSfun.Empty [definition, in CoqFSetInterface]
WSfun.empty [axiom, in CoqFSetInterface]
WSfun.empty_1 [axiom, in CoqFSetInterface]
WSfun.eq [definition, in CoqFSetInterface]
WSfun.equal [axiom, in CoqFSetInterface]
WSfun.Equal [definition, in CoqFSetInterface]
WSfun.equal_1 [axiom, in CoqFSetInterface]
WSfun.equal_2 [axiom, in CoqFSetInterface]
WSfun.eq_dec [axiom, in CoqFSetInterface]
WSfun.eq_refl [axiom, in CoqFSetInterface]
WSfun.eq_sym [axiom, in CoqFSetInterface]
WSfun.eq_trans [axiom, in CoqFSetInterface]
WSfun.Exists [definition, in CoqFSetInterface]
WSfun.exists_ [axiom, in CoqFSetInterface]
WSfun.exists_1 [axiom, in CoqFSetInterface]
WSfun.exists_2 [axiom, in CoqFSetInterface]
WSfun.filter [axiom, in CoqFSetInterface]
WSfun.filter_1 [axiom, in CoqFSetInterface]
WSfun.filter_2 [axiom, in CoqFSetInterface]
WSfun.filter_3 [axiom, in CoqFSetInterface]
WSfun.fold [axiom, in CoqFSetInterface]
WSfun.fold_1 [axiom, in CoqFSetInterface]
WSfun.for_all [axiom, in CoqFSetInterface]
WSfun.For_all [definition, in CoqFSetInterface]
WSfun.for_all_1 [axiom, in CoqFSetInterface]
WSfun.for_all_2 [axiom, in CoqFSetInterface]
WSfun.fresh_list [definition, in FSetExtra]
WSfun.In [axiom, in CoqFSetInterface]
WSfun.inter [axiom, in CoqFSetInterface]
WSfun.inter_1 [axiom, in CoqFSetInterface]
WSfun.inter_2 [axiom, in CoqFSetInterface]
WSfun.inter_3 [axiom, in CoqFSetInterface]
WSfun.In_1 [axiom, in CoqFSetInterface]
WSfun.is_empty [axiom, in CoqFSetInterface]
WSfun.is_empty_1 [axiom, in CoqFSetInterface]
WSfun.is_empty_2 [axiom, in CoqFSetInterface]
WSfun.mem [axiom, in CoqFSetInterface]
WSfun.mem_1 [axiom, in CoqFSetInterface]
WSfun.mem_2 [axiom, in CoqFSetInterface]
WSfun.notin [definition, in FSetExtra]
WSfun.partition [axiom, in CoqFSetInterface]
WSfun.partition_1 [axiom, in CoqFSetInterface]
WSfun.partition_2 [axiom, in CoqFSetInterface]
WSfun.remove [axiom, in CoqFSetInterface]
WSfun.remove_1 [axiom, in CoqFSetInterface]
WSfun.remove_2 [axiom, in CoqFSetInterface]
WSfun.remove_3 [axiom, in CoqFSetInterface]
WSfun.singleton [axiom, in CoqFSetInterface]
WSfun.singleton_1 [axiom, in CoqFSetInterface]
WSfun.singleton_2 [axiom, in CoqFSetInterface]
WSfun.Spec [section, in CoqFSetInterface]
WSfun.Spec.Filter [section, in CoqFSetInterface]
WSfun.Spec.Filter.f [variable, in CoqFSetInterface]
WSfun.Spec.s [variable, in CoqFSetInterface]
WSfun.Spec.s' [variable, in CoqFSetInterface]
WSfun.Spec.s'' [variable, in CoqFSetInterface]
WSfun.Spec.x [variable, in CoqFSetInterface]
WSfun.Spec.y [variable, in CoqFSetInterface]
WSfun.subset [axiom, in CoqFSetInterface]
WSfun.Subset [definition, in CoqFSetInterface]
WSfun.subset_1 [axiom, in CoqFSetInterface]
WSfun.subset_2 [axiom, in CoqFSetInterface]
WSfun.t [axiom, in CoqFSetInterface]
WSfun.union [axiom, in CoqFSetInterface]
WSfun.union_1 [axiom, in CoqFSetInterface]
WSfun.union_2 [axiom, in CoqFSetInterface]
WSfun.union_3 [axiom, in CoqFSetInterface]
Y
Ybfsubst_permutation [lemma, in LN_Template_Two_Sort]Ybfsubst_permutation_core [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_core_Ywf [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_ind [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_ind_Ywf [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_var [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_var_wf [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_var_wfT [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_wf [lemma, in LN_Template_Two_Sort]
Ybfsubst_permutation_wfT [lemma, in LN_Template_Two_Sort]
Ybsubst_homo_wf [lemma, in LN_Template_Two_Sort]
Ybsubst_var_twice [definition, in LN_Template_Two_Sort]
Ybsubst_var_twice_wf [lemma, in LN_Template_Two_Sort]
YenvT_dom_subset [lemma, in LN_Template_Two_Sort]
YenvT_from_Ywf_env [lemma, in LN_Template_Two_Sort]
YenvT_from_Ywf_env_left [lemma, in LN_Template_Two_Sort]
Yfsubst_fresh [lemma, in LN_Template_Two_Sort]
Yfsubst_Lemma [lemma, in LN_Template_Two_Sort]
YHfsubst_Lemma [lemma, in LN_Template_Two_Sort]
YSize_Ybsubst [definition, in LN_Template_Two_Sort]
Ysubst_preserves_subtyping [lemma, in dB_Fsub_basic_Main]
YTenvT_all_inv [lemma, in LN_Fsub_adv_Infrastructure]
YTenvT_from_YTwf_env_1 [lemma, in LN_Template_Two_Sort]
YTenvT_from_YTwf_env_1_left [lemma, in LN_Template_Two_Sort]
YTenvT_from_YTwf_env_2 [lemma, in LN_Template_Two_Sort]
YTenvT_from_YTwf_env_2_left [lemma, in LN_Template_Two_Sort]
YTenvT_wft [lemma, in LN_Fsub_adv_Infrastructure]
YTenvT_Yfv [lemma, in LN_Template_Two_Sort]
YTenvT_YwfT [lemma, in LN_Template_Two_Sort]
YTwf_empty [constructor, in LN_Template_Two_Sort]
YTwf_env [inductive, in LN_Template_Two_Sort]
YTwf_env_binds_1 [lemma, in LN_Template_Two_Sort]
YTwf_env_binds_2 [lemma, in LN_Template_Two_Sort]
YTwf_env_fv_1 [lemma, in LN_Template_Two_Sort]
YTwf_env_fv_2 [lemma, in LN_Template_Two_Sort]
YTwf_env_map_subst_id_1 [lemma, in LN_Template_Two_Sort]
YTwf_env_map_subst_id_2 [lemma, in LN_Template_Two_Sort]
YTwf_env_map_subst_id_3 [lemma, in LN_Template_Two_Sort]
YTwf_env_narrow [lemma, in LN_Template_Two_Sort]
YTwf_env_strengthening [lemma, in LN_Template_Two_Sort]
YTwf_env_strengthening_left [lemma, in LN_Template_Two_Sort]
YTwf_env_strengthening_1 [lemma, in LN_Template_Two_Sort]
YTwf_sub [constructor, in LN_Template_Two_Sort]
YTwf_typ [constructor, in LN_Template_Two_Sort]
YwfT_all_inv [lemma, in LN_Fsub_adv_Infrastructure]
YwfT_arrow_inv [lemma, in LN_Fsub_adv_Infrastructure]
YwfT_type [lemma, in LN_Fsub_adv_Infrastructure]
YwfT_Yfsubst [lemma, in LN_Template_Two_Sort]
Ywf_basic_type [lemma, in LN_Fsub_basic_Infrastructure]
Ywf_env_binds [lemma, in LN_Template_Two_Sort]
Ywf_env_cons [lemma, in LN_Template_Two_Sort]
Ywf_env_from_YTwf_env [lemma, in LN_Template_Two_Sort]
Ywf_env_narrow [lemma, in LN_Template_Two_Sort]
Ywf_env_narrow_left [lemma, in LN_Template_Two_Sort]
Ywf_type [lemma, in LN_Fsub_basic_Infrastructure]
Ywf_Yfsubst [lemma, in LN_Template_Two_Sort]
Instance Index
E
EqDec_atom [in MetatheoryAtom]EqDec_eq_of_EqDec [in CoqEqDec]
Projection Index
E
eq_dec [in CoqEqDec]Record Index
E
EqDec_eq [in CoqEqDec]Lemma Index
A
app_cons_not_nil [in CoqListFacts]app_eq_cons [in CoqListFacts]
AtomImpl.atom_fresh_for_list [in MetatheoryAtom]
AtomImpl.max_lt_r [in MetatheoryAtom]
AtomImpl.nat_list_max [in MetatheoryAtom]
atom_fresh [in MetatheoryAtom]
B
bfsubstRep_permutation [in LNameless_Meta_Env]bfsubstRep_permutation_core [in LNameless_Meta]
bfsubstRep_permutation_core_wf [in LNameless_Meta]
bfsubstRep_permutation_ind [in LNameless_Meta]
bfsubstRep_permutation_ind_wf [in LNameless_Meta]
bfsubstRep_permutation_var [in LNameless_Meta_Env]
bfsubstRep_permutation_var_wf [in LNameless_Meta]
bfsubstRep_permutation_var_wfT [in LNameless_Meta]
bfsubstRep_permutation_wf [in LNameless_Meta]
bfsubstRep_permutation_wfT [in LNameless_Meta]
bfsubstRep_var_intro [in LNameless_Meta]
bfsubst_permutation [in LNameless_Meta_Env]
bfsubst_permutation_core [in LNameless_Meta]
bfsubst_permutation_core_wf [in LNameless_Meta]
bfsubst_permutation_ind [in LNameless_Meta]
bfsubst_permutation_ind_wf [in LNameless_Meta]
bfsubst_permutation_var [in LNameless_Meta_Env]
bfsubst_permutation_var_wf [in LNameless_Meta]
bfsubst_permutation_var_wfT [in LNameless_Meta]
bfsubst_permutation_var_wfT_hetero [in LNameless_Meta]
bfsubst_permutation_wf [in LNameless_Meta]
bfsubst_permutation_wfT [in LNameless_Meta]
bfsubst_var_intro [in LNameless_Meta]
bsubstitutionRep_hetero [in LNameless_Meta]
bsubstitutionRep_hetero_wf [in LNameless_Meta]
bsubstitutionRep_homo [in LNameless_Meta]
bsubstitutionRep_homo_wf [in LNameless_Meta]
bsubstitutionRep_var_twice [in LNameless_Meta]
bsubstitutionRep_var_twice_wf [in LNameless_Meta]
bsubstitution_hetero [in LNameless_Meta]
bsubstitution_hetero_wf [in LNameless_Meta]
bsubstitution_homo [in LNameless_Meta]
bsubstitution_homo_wf [in LNameless_Meta]
bsubstitution_var_twice [in LNameless_Meta]
bsubstitution_var_twice_wf [in LNameless_Meta]
bsubstRep_hetero_core [in LNameless_Meta]
bsubstRep_homo_core [in LNameless_Meta]
bsubst_hetero_core [in LNameless_Meta]
bsubst_homo_core [in LNameless_Meta]
bsubst_size [in LNameless_Meta]
bsubst_sizeRep [in LNameless_Meta]
C
canonical_form_abs [in LN_Fsub_adv_Soundness]canonical_form_abs [in LN_Fsub_basic_Soundness]
canonical_form_tabs [in LN_Fsub_basic_Soundness]
canonical_form_tabs [in LN_Fsub_adv_Soundness]
cons_eq_app [in CoqListFacts]
context_replacement [in dB_Fsub_basic_Main]
conv_bsubst [in LNameless_Meta]
conv_envT [in LNameless_Meta_Env]
conv_freevars_1 [in LNameless_Meta]
conv_freevars_2 [in LNameless_Meta]
conv_freevars_3 [in LNameless_Meta]
conv_freevars_4 [in LNameless_Meta]
conv_fsubst [in LNameless_Meta]
conv_wfT [in LNameless_Meta]
D
dBTemplate.From_To_TEnv [in dB_Template]dBTemplate.From_Tshift [in dB_Template]
dBTemplate.From_Tsubst [in dB_Template]
dBTemplate.gTwf_env_Twf_env [in dB_Template]
dBTemplate.opt_From_preserving_some [in dB_Template]
dBTemplate.opt_To_preserving_eq [in dB_Template]
dBTemplate.opt_To_preserving_eq_rev [in dB_Template]
dBTemplate.opt_To_preserving_none [in dB_Template]
dBTemplate.opt_To_preserving_none_rev [in dB_Template]
dBTemplate.opt_To_preserving_some [in dB_Template]
dBTemplate.opt_To_preserving_some_rev [in dB_Template]
dBTemplate.Tinsert_S [in dB_Template]
dBTemplate.To_From_TEnv [in dB_Template]
dBTemplate.Tremove_right_gTremove_right [in dB_Template]
dBTemplate.Tshift_id [in dB_Template]
dBTemplate.Tsubst_id [in dB_Template]
dBTemplate.Twf_env_gTwf_env [in dB_Template]
dBTemplate.Twf_env_remove_right [in dB_Template]
dBTemplate.Twf_env_weaken [in dB_Template]
dBTemplate.Twf_typ_eleft [in dB_Template]
dBTemplate.Twf_typ_insert_right [in dB_Template]
dBTemplate.Twf_typ_remove_right [in dB_Template]
dBTemplate.Twf_typ_strengthening_right [in dB_Template]
dBTemplate.Twf_typ_weakening_right [in dB_Template]
Dgp.conv_id [in DGP_Core]
Dgp.conv_indep [in DGP_Core]
Dgp.conv_size [in DGP_Core]
Dgp.conv_Var [in DGP_Core]
dom_empty_env [in Metatheory_Env]
dom_map_1 [in Metatheory_Env]
dom_map_2 [in Metatheory_Env]
dom_map_3 [in Metatheory_Env]
dom_map_4 [in Metatheory_Env]
E
elim_incl_app [in CoqListFacts]elim_incl_cons [in CoqListFacts]
elim_not_In_app [in CoqListFacts]
elim_not_In_cons [in CoqListFacts]
envTRep_dom_subset [in LNameless_Meta_Env]
envTRep_fv [in LNameless_Meta_Env]
envTrep_wfRep [in LNameless_Meta_Env]
envTRep_wfT [in LNameless_Meta_Env]
envT_dom_subset [in LNameless_Meta_Env]
envT_from_wf_env [in LNameless_Meta_Env]
envT_from_wf_env_left [in LNameless_Meta_Env]
envT_fv [in LNameless_Meta_Env]
envT_narrow [in LNameless_Meta_Env]
envT_narrowRep [in LNameless_Meta_Env]
envT_narrowRep_ [in LNameless_Meta_Env]
envT_narrow_ [in LNameless_Meta_Env]
envT_narrow_left [in LNameless_Meta_Env]
envT_narrow_right [in LNameless_Meta_Env]
envT_Tfv [in LN_Template_One_Sort]
envT_Tfv [in LN_Template_Two_Sort]
envT_weaken [in LNameless_Meta_Env]
envT_weakenRep [in LNameless_Meta_Env]
envT_weaken_left [in LNameless_Meta_Env]
envT_weaken_right [in LNameless_Meta_Env]
envT_wf [in LNameless_Meta_Env]
envT_wfT [in LNameless_Meta_Env]
env_subst_get_left_ge [in dB_Fsub_basic_Main]
env_subst_get_left_lt [in dB_Fsub_basic_Main]
env_subst_get_right [in dB_Fsub_basic_Main]
env_subst_le [in dB_Fsub_basic_Main]
env_subst_minus_1 [in dB_Fsub_basic_Main]
env_subst_sub [in dB_Fsub_basic_Main]
env_subst_wf_env [in dB_Fsub_basic_Main]
env_subst_wf_typ [in dB_Fsub_basic_Main]
env_subst_wf_typ_0 [in dB_Fsub_basic_Main]
eqlistA_unique [in CoqListFacts]
eqlist_eq [in CoqListFacts]
equiv_decidable [in CoqEqDec]
equiv_reflexive' [in CoqEqDec]
equiv_symmetric' [in CoqEqDec]
equiv_transitive' [in CoqEqDec]
eq_pair_dec [in CoqUniquenessTac]
eq_unit_dec [in CoqUniquenessTac]
example_pick_fresh_use [in MetatheoryAtom]
extendsRep_env [in LNameless_Meta_Env]
extends_app_L [in Metatheory_Env]
extends_app_R [in Metatheory_Env]
extends_env [in LNameless_Meta_Env]
extends_L [in Metatheory_Env]
extends_push [in Metatheory_Env]
extends_R [in Metatheory_Env]
extends_swap [in Metatheory_Env]
F
freevarsRep_pass_binder [in LNameless_Meta]freevars_pass_binder [in LNameless_Meta]
fsubstitution [in LNameless_Meta]
fsubstitutionRep [in LNameless_Meta]
fsubstRep_fresh [in LNameless_Meta_Env]
fsubstRep_no_occur [in LNameless_Meta]
fsubstRep_self [in LNameless_Meta]
fsubst_fresh [in LNameless_Meta_Env]
fsubst_no_occur [in LNameless_Meta]
fsubst_self [in LNameless_Meta]
fun_value [in dB_Fsub_basic_Main]
FWellformed.envT_THfv [in LN_Template]
FWellformed.envT_Yfv [in LN_Template]
FWellformed.extends_TenvT [in LN_Template]
FWellformed.noRepr_YHenvT [in LN_Template]
FWellformed.notin_app_3 [in LN_Template]
FWellformed.TenvT_narrow [in LN_Template]
FWellformed.TenvT_narrow_left [in LN_Template]
FWellformed.TenvT_narrow_right [in LN_Template]
FWellformed.TenvT_weaken [in LN_Template]
FWellformed.TenvT_weaken_left [in LN_Template]
FWellformed.TenvT_weaken_right [in LN_Template]
FWellformed.THenvT_Thwf [in LN_Template]
FWellformed.THenvT_THwfT [in LN_Template]
FWellformed.uniq_from_Ywf_env [in LN_Template]
FWellformed.YenvT_Ywf [in LN_Template]
FWellformed.YenvT_YwfT [in LN_Template]
FWellformed.YTenvT_narrow [in LN_Template]
FWellformed.YTenvT_narrow_left [in LN_Template]
FWellformed.YTenvT_narrow_right [in LN_Template]
FWellformed.YTenvT_typ_var_indep [in LN_Template]
FWellformed.YTenvT_typ_var_strengthen [in LN_Template]
FWellformed.YTenvT_weaken [in LN_Template]
FWellformed.YTenvT_weaken_left [in LN_Template]
FWellformed.YTenvT_weaken_right [in LN_Template]
G
get_left_gt [in deBruijn_Meta_Env]get_left_insert_left_ge [in deBruijn_Meta_Env]
get_left_insert_left_lt [in deBruijn_Meta_Env]
get_left_narrow_eq [in dB_Fsub_basic_Main]
get_left_narrow_ne [in dB_Fsub_basic_Main]
get_left_remove_right [in deBruijn_Meta_Env]
get_right_insert_left [in deBruijn_Meta_Env]
get_right_narrow [in dB_Fsub_basic_Main]
get_right_remove_right_ge [in deBruijn_Meta_Env]
get_right_remove_right_lt [in deBruijn_Meta_Env]
get_right_wf [in deBruijn_Meta_Env]
gTinsert_left_Tinsert_left [in dB_Template_Two_Sort]
gTTwf_TTwf [in LN_Template_Two_Sort]
gTTwf_TTwf_basic [in LN_Template_Two_Sort]
H
HO_wfRep_extensionality [in deBruijn_Meta_Env]HO_wfRep_insert_right [in deBruijn_Meta_Env]
HO_wfRep_left [in deBruijn_Meta_Env]
HO_wfRep_strengthening_right [in deBruijn_Meta_Env]
HO_wfRep_weaken [in deBruijn_Meta_Env]
HO_wfRep_weakening_left [in deBruijn_Meta_Env]
HO_wfRep_weakening_right [in deBruijn_Meta_Env]
HO_wfRep_weaken_lth [in deBruijn_Meta_Env]
HO_wfright_remove_right [in deBruijn_Meta_Env]
HO_wf_extensionality [in deBruijn_Meta_Env]
HO_wf_insert_right [in deBruijn_Meta_Env]
HO_wf_left [in deBruijn_Meta_Env]
HO_wf_remove_right [in deBruijn_Meta_Env]
HO_wf_strengthening_right [in deBruijn_Meta_Env]
HO_wf_weaken [in deBruijn_Meta_Env]
HO_wf_weakening_left [in deBruijn_Meta_Env]
HO_wf_weakening_right [in deBruijn_Meta_Env]
HO_wf_weaken_lth [in deBruijn_Meta_Env]
I
InA_iff_In [in CoqListFacts]InA_In [in CoqListFacts]
incl_nil [in CoqListFacts]
insert_left_HO_wf [in deBruijn_Meta_Env]
insert_left_HO_wfRep [in deBruijn_Meta_Env]
insert_left_lth [in deBruijn_Meta_Env]
insert_left_lth_1 [in deBruijn_Meta_Env]
insert_left_wf_env [in deBruijn_Meta_Env]
insert_S [in deBruijn_Meta_Env]
insert_T [in deBruijn_Meta_Env]
insert_T_ind [in deBruijn_Meta_Env]
In_atoms_dec [in Metatheory_Env]
In_atoms_dec [in LNameless_Meta_Env]
In_incl [in CoqListFacts]
In_map [in CoqListFacts]
Iso_nat.To_From [in deBruijn_Isomorphism]
Iso_nat.To_From [in Tutorial_STLC_Iso]
Iso_nat.To_From [in LNameless_Isomorphism]
Iso_nat_REC [in deBruijn_Isomorphism]
Iso_nat_REC [in LNameless_Isomorphism]
Iso_trm.From_inj [in deBruijn_Fsub_Iso]
Iso_trm.From_inj [in LNameless_Fsub_Iso]
Iso_trm.From_inj [in Tutorial_STLC_Iso]
Iso_trm.From_inj [in LNameless_STLC_Iso]
Iso_trm.From_To [in deBruijn_Fsub_Iso]
Iso_trm.From_To [in Tutorial_STLC_Iso]
Iso_trm.From_To [in LNameless_Fsub_Iso]
Iso_trm.From_To [in LNameless_STLC_Iso]
Iso_trm.From_To_Rep [in LNameless_Fsub_Iso]
Iso_trm.From_To_Rep [in LNameless_STLC_Iso]
Iso_trm.From_To_Rep [in deBruijn_Fsub_Iso]
Iso_trm.From_To_Rep [in Tutorial_STLC_Iso]
Iso_trm.To_From [in deBruijn_Fsub_Iso]
Iso_trm.To_From [in LNameless_STLC_Iso]
Iso_trm.To_From [in Tutorial_STLC_Iso]
Iso_trm.To_From [in LNameless_Fsub_Iso]
Iso_trm.To_inj [in LNameless_STLC_Iso]
Iso_trm.To_inj [in Tutorial_STLC_Iso]
Iso_trm.To_inj [in deBruijn_Fsub_Iso]
Iso_trm.To_inj [in LNameless_Fsub_Iso]
Iso_typ.From_inj [in deBruijn_Fsub_Iso]
Iso_typ.From_inj [in LNameless_Fsub_Iso]
Iso_typ.From_inj [in LNameless_STLC_Iso]
Iso_typ.From_inj [in Tutorial_STLC_Iso]
Iso_typ.From_To [in deBruijn_Fsub_Iso]
Iso_typ.From_To [in LNameless_Fsub_Iso]
Iso_typ.From_To_Rep [in LNameless_Fsub_Iso]
Iso_typ.From_To_Rep [in deBruijn_Fsub_Iso]
Iso_typ.To_From [in LNameless_Fsub_Iso]
Iso_typ.To_From [in LNameless_STLC_Iso]
Iso_typ.To_From [in deBruijn_Fsub_Iso]
Iso_typ.To_From [in Tutorial_STLC_Iso]
Iso_typ.To_inj [in LNameless_Fsub_Iso]
Iso_typ.To_inj [in deBruijn_Fsub_Iso]
Iso_typ_REC [in LNameless_Fsub_Iso]
Iso_typ_REC [in LNameless_STLC_Iso]
Iso_typ_REC [in deBruijn_Fsub_Iso]
L
lelistA_dec [in CoqListFacts]lelistA_unique [in CoqListFacts]
le_max_S_l [in Arith_Max_extra]
le_max_S_r [in Arith_Max_extra]
LNTemplate.env_fv_no_occur [in LN_Template]
LNTemplate.From_Tbsubst [in LN_Template]
LNTemplate.From_Tbsubst_var [in LN_Template]
LNTemplate.From_Tfsubst [in LN_Template]
LNTemplate.From_Tfsubst_var [in LN_Template]
LNTemplate.gTwf_from_Twf_basic [in LN_Template]
LNTemplate.gTwf_Twf [in LN_Template]
LNTemplate.gTwf_Twf_basic [in LN_Template]
LNTemplate.iso_env_map [in LN_Template]
LNTemplate.noRepr_Tbsubst [in LN_Template]
LNTemplate.noRepr_Tfsubst [in LN_Template]
LNTemplate.noRepr_Tfv [in LN_Template]
LNTemplate.noRepr_Twf [in LN_Template]
LNTemplate.noRepr_TwfT [in LN_Template]
LNTemplate.Tbfsubst_var_intro [in LN_Template]
LNTemplate.Tbsubst_homo [in LN_Template]
LNTemplate.Tbsubst_homo_core [in LN_Template]
LNTemplate.Tbsubst_var_twice [in LN_Template]
LNTemplate.Tfsubst_no_occur [in LN_Template]
LNTemplate.Tfsubst_self [in LN_Template]
LNTemplate.Tfv_pass_binder [in LN_Template]
LNTemplate.Tfv_pass_binder_1 [in LN_Template]
LNTemplate.TSize_Tbsubst [in LN_Template]
LNTemplate.TwfT_Twf [in LN_Template]
LNTemplate.Twf_basic_from_gTwf [in LN_Template]
LNTemplate.Twf_basic_from_Twf [in LN_Template]
LNTemplate.Twf_from_Twf_basic [in LN_Template]
LNTemplate.Twf_gTwf [in LN_Template]
LNTemplate.Twf_gTwf_basic [in LN_Template]
local_preservation_app [in dB_Fsub_basic_Main]
local_preservation_tapp [in dB_Fsub_basic_Main]
local_progress [in dB_Fsub_basic_Main]
lth_preserving [in deBruijn_Meta_Env]
lt_max_SS_l [in Arith_Max_extra]
lt_max_SS_r [in Arith_Max_extra]
lt_max_S_l [in Arith_Max_extra]
lt_max_S_r [in Arith_Max_extra]
lt_SS_max_l [in Arith_Max_extra]
lt_SS_max_r [in Arith_Max_extra]
lt_S_max_l [in Arith_Max_extra]
lt_S_max_r [in Arith_Max_extra]
M
Make.alist_ind [in AssocList]Make.app_assoc [in AssocList]
Make.app_assoc_map_push [in AssocList]
Make.app_eq_one [in AssocList]
Make.app_nil_1 [in AssocList]
Make.app_nil_2 [in AssocList]
Make.binds_app_iff [in AssocList]
Make.binds_app_uniq_iff [in AssocList]
Make.binds_app_uniq_1 [in AssocList]
Make.binds_app_1 [in AssocList]
Make.binds_app_2 [in AssocList]
Make.binds_app_3 [in AssocList]
Make.binds_cons_iff [in AssocList]
Make.binds_cons_uniq_iff [in AssocList]
Make.binds_cons_uniq_1 [in AssocList]
Make.binds_cons_1 [in AssocList]
Make.binds_cons_2 [in AssocList]
Make.binds_cons_3 [in AssocList]
Make.binds_cons_4 [in AssocList]
Make.binds_dec [in AssocList]
Make.binds_dom_contradiction [in AssocList]
Make.binds_head [in AssocList]
Make.binds_In [in AssocList]
Make.binds_In_inv [in AssocList]
Make.binds_lookup [in AssocList]
Make.binds_lookup_dec [in AssocList]
Make.binds_map_1 [in AssocList]
Make.binds_map_2 [in AssocList]
Make.binds_mid_eq [in AssocList]
Make.binds_nil_iff [in AssocList]
Make.binds_one_iff [in AssocList]
Make.binds_one_1 [in AssocList]
Make.binds_one_2 [in AssocList]
Make.binds_one_3 [in AssocList]
Make.binds_remove_mid [in AssocList]
Make.binds_unique [in AssocList]
Make.binds_weaken [in AssocList]
Make.cons_app_assoc [in AssocList]
Make.cons_app_one [in AssocList]
Make.disjoint_app_l [in AssocList]
Make.disjoint_app_r [in AssocList]
Make.disjoint_app_1 [in AssocList]
Make.disjoint_app_2 [in AssocList]
Make.disjoint_app_3 [in AssocList]
Make.disjoint_cons_l [in AssocList]
Make.disjoint_cons_r [in AssocList]
Make.disjoint_cons_1 [in AssocList]
Make.disjoint_cons_2 [in AssocList]
Make.disjoint_cons_3 [in AssocList]
Make.disjoint_map_l [in AssocList]
Make.disjoint_map_r [in AssocList]
Make.disjoint_map_1 [in AssocList]
Make.disjoint_map_2 [in AssocList]
Make.disjoint_nil_1 [in AssocList]
Make.disjoint_one_l [in AssocList]
Make.disjoint_one_r [in AssocList]
Make.disjoint_one_1 [in AssocList]
Make.disjoint_one_2 [in AssocList]
Make.disjoint_sym [in AssocList]
Make.disjoint_sym_1 [in AssocList]
Make.dom_app [in AssocList]
Make.dom_cons [in AssocList]
Make.dom_map [in AssocList]
Make.dom_nil [in AssocList]
Make.dom_one [in AssocList]
Make.dom_push [in AssocList]
Make.eq_push_inv [in AssocList]
Make.fresh_app_l [in AssocList]
Make.fresh_app_r [in AssocList]
Make.fresh_mid_head [in AssocList]
Make.fresh_mid_tail [in AssocList]
Make.in_app_iff [in AssocList]
Make.in_nil_iff [in AssocList]
Make.in_one_iff [in AssocList]
Make.map_app [in AssocList]
Make.map_cons [in AssocList]
Make.map_nil [in AssocList]
Make.map_one [in AssocList]
Make.nil_neq_one_mid [in AssocList]
Make.one_eq_app [in AssocList]
Make.one_mid_neq_nil [in AssocList]
Make.uniq_app_iff [in AssocList]
Make.uniq_app_1 [in AssocList]
Make.uniq_app_2 [in AssocList]
Make.uniq_app_3 [in AssocList]
Make.uniq_app_4 [in AssocList]
Make.uniq_cons_iff [in AssocList]
Make.uniq_cons_1 [in AssocList]
Make.uniq_cons_2 [in AssocList]
Make.uniq_cons_3 [in AssocList]
Make.uniq_dom_only [in AssocList]
Make.uniq_dom_only_1 [in AssocList]
Make.uniq_insert_mid [in AssocList]
Make.uniq_map_app_1 [in AssocList]
Make.uniq_map_app_2 [in AssocList]
Make.uniq_map_iff [in AssocList]
Make.uniq_map_1 [in AssocList]
Make.uniq_map_2 [in AssocList]
Make.uniq_one_1 [in AssocList]
Make.uniq_remove_mid [in AssocList]
Make.uniq_reorder_1 [in AssocList]
Make.uniq_reorder_2 [in AssocList]
map_extends_1 [in Metatheory_Env]
map_extends_2 [in Metatheory_Env]
map_subst_tb_id [in LN_Fsub_basic_Infrastructure]
map_uniq_1 [in Metatheory_Env]
map_uniq_2 [in Metatheory_Env]
map_uniq_3 [in Metatheory_Env]
map_uniq_4 [in Metatheory_Env]
map_uniq_5 [in Metatheory_Env]
max_lt_1 [in Arith_Max_extra]
max_lt_2 [in Arith_Max_extra]
modus_ponens [in LibTactics]
N
narrowing_case [in dB_Fsub_basic_Main]narrow_wf_env [in dB_Fsub_basic_Main]
narrow_wf_typ [in dB_Fsub_basic_Main]
nil_eq_app [in CoqListFacts]
noRepr_bsubstRep_hetero [in LNameless_Meta_Env]
noRepr_bsubst_hetero [in LNameless_Meta_Env]
noRepr_envTRep_hetero [in LNameless_Meta_Env]
noRepr_envT_fsubst [in LNameless_Meta_Env]
noRepr_envT_fsubstRep [in LNameless_Meta_Env]
noRepr_envT_fsubstRep_ [in LNameless_Meta_Env]
noRepr_envT_fsubst_ [in LNameless_Meta_Env]
noRepr_envT_hetero [in LNameless_Meta_Env]
noRepr_freevarsRep_hetero [in LNameless_Meta_Env]
noRepr_freevars_hetero [in LNameless_Meta_Env]
noRepr_fsubstRep_hetero [in LNameless_Meta_Env]
noRepr_fsubst_hetero [in LNameless_Meta_Env]
noRepr_shiftRep_hetero [in deBruijn_Meta]
noRepr_shift_hetero [in deBruijn_Meta]
noRepr_shift_preserves_size [in deBruijn_Meta]
noRepr_shift_preserves_sizeRep [in deBruijn_Meta]
noRepr_shift_shift [in deBruijn_Meta]
noRepr_shift_shiftRep [in deBruijn_Meta]
noRepr_shift_substRep_1 [in deBruijn_Meta]
noRepr_shift_substRep_2 [in deBruijn_Meta]
noRepr_shift_subst_1 [in deBruijn_Meta]
noRepr_shift_subst_2 [in deBruijn_Meta]
noRepr_substRep_hetero [in deBruijn_Meta]
noRepr_subst_hetero [in deBruijn_Meta]
noRepr_subst_shift [in deBruijn_Meta]
noRepr_subst_shiftRep [in deBruijn_Meta]
noRepr_subst_subst [in deBruijn_Meta]
noRepr_subst_substRep [in deBruijn_Meta]
noRepr_THbfsubst_permutation_var [in LN_Template_Two_Sort]
noRepr_THbfsubst_permutation_var_1 [in LN_Template_Two_Sort]
noRepr_THbfsubst_permutation_var_1_wf [in LN_Template_Two_Sort]
noRepr_TTwfT_THfsubst [in LN_Template_Two_Sort]
noRepr_TTwf_THfsubst [in LN_Template_Two_Sort]
noRepr_wfRep_hetero [in LNameless_Meta_Env]
noRepr_wfTRep_hetero [in LNameless_Meta_Env]
noRepr_wfT_hetero [in LNameless_Meta_Env]
noRepr_wf_env_fsubst [in LNameless_Meta_Env]
noRepr_wf_hetero [in LNameless_Meta_Env]
noRepr_YenvT_Yfsubst [in LN_Template_Two_Sort]
noRepr_Yshift_preserves_Ysize [in dB_Template_Two_Sort]
noRepr_Yshift_Yshift [in dB_Template_Two_Sort]
noRepr_Yshift_Ysubst_1 [in dB_Template_Two_Sort]
noRepr_Yshift_Ysubst_2 [in dB_Template_Two_Sort]
noRepr_Ysubst_Yshift [in dB_Template_Two_Sort]
noRepr_Ysubst_Ysubst [in dB_Template_Two_Sort]
noRepr_YTenvT_Yfsubst [in LN_Template_Two_Sort]
noRepr_YTenvT_Yfsubst_left [in LN_Template_Two_Sort]
noRepr_YTwf_env_Yfsubst [in LN_Template_Two_Sort]
noRepr_YTwf_env_Yfsubst_left [in LN_Template_Two_Sort]
noRepr_Ywf_env_Yfsubst [in LN_Template_Two_Sort]
notin_app_1 [in Metatheory_Env]
notin_app_2 [in Metatheory_Env]
notin_cons_mid [in Metatheory_Env]
Notin_fun.notin_add_1 [in FSetWeakNotin]
Notin_fun.notin_add_1' [in FSetWeakNotin]
Notin_fun.notin_add_2 [in FSetWeakNotin]
Notin_fun.notin_add_3 [in FSetWeakNotin]
Notin_fun.notin_diff_1 [in FSetWeakNotin]
Notin_fun.notin_diff_2 [in FSetWeakNotin]
Notin_fun.notin_diff_3 [in FSetWeakNotin]
Notin_fun.notin_empty_1 [in FSetWeakNotin]
Notin_fun.notin_inter_1 [in FSetWeakNotin]
Notin_fun.notin_inter_2 [in FSetWeakNotin]
Notin_fun.notin_inter_3 [in FSetWeakNotin]
Notin_fun.notin_remove_1 [in FSetWeakNotin]
Notin_fun.notin_remove_2 [in FSetWeakNotin]
Notin_fun.notin_remove_3 [in FSetWeakNotin]
Notin_fun.notin_remove_3' [in FSetWeakNotin]
Notin_fun.notin_singleton_1 [in FSetWeakNotin]
Notin_fun.notin_singleton_1' [in FSetWeakNotin]
Notin_fun.notin_singleton_2 [in FSetWeakNotin]
Notin_fun.notin_union_1 [in FSetWeakNotin]
Notin_fun.notin_union_2 [in FSetWeakNotin]
Notin_fun.notin_union_3 [in FSetWeakNotin]
Notin_fun.test_solve_notin_1 [in FSetWeakNotin]
Notin_fun.test_solve_notin_2 [in FSetWeakNotin]
Notin_fun.test_solve_notin_3 [in FSetWeakNotin]
Notin_fun.test_solve_notin_4 [in FSetWeakNotin]
Notin_fun.test_solve_notin_5 [in FSetWeakNotin]
Notin_fun.test_solve_notin_6 [in FSetWeakNotin]
Notin_fun.test_solve_notin_7 [in FSetWeakNotin]
notin_fv_wf [in LN_Fsub_basic_Infrastructure]
notin_neq [in LNameless_Meta_Env]
notin_neq [in Metatheory_Env]
not_In_app [in CoqListFacts]
not_In_cons [in CoqListFacts]
O
okt_narrow [in LN_Fsub_basic_Infrastructure]okt_strengthen [in LN_Fsub_basic_Infrastructure]
okt_subst_tb [in LN_Fsub_basic_Infrastructure]
ok_from_okt [in LN_Fsub_basic_Infrastructure]
opt_map_none [in deBruijn_Meta_Env]
opt_map_none_1 [in deBruijn_Meta_Env]
P
preservation [in dB_Fsub_basic_Main]preservation' [in dB_Fsub_basic_Main]
preservation_result [in LN_Fsub_basic_Soundness]
preservation_result [in LN_STLC_basic_Soundness]
preservation_result [in LN_Fsub_adv_Soundness]
progress [in dB_Fsub_basic_Main]
progress' [in dB_Fsub_basic_Main]
progress_result [in LN_Fsub_basic_Soundness]
progress_result [in LN_Fsub_adv_Soundness]
progress_result [in LN_STLC_basic_Soundness]
PWellformed.envT_Tfv [in LN_Template]
PWellformed.extends_TenvT [in LN_Template]
PWellformed.Tbfsubst_permutation [in LN_Template]
PWellformed.Tbfsubst_permutation_var [in LN_Template]
PWellformed.TenvT_dom_subset [in LN_Template]
PWellformed.TenvT_narrow [in LN_Template]
PWellformed.TenvT_narrow_left [in LN_Template]
PWellformed.TenvT_narrow_right [in LN_Template]
PWellformed.TenvT_Twf [in LN_Template]
PWellformed.TenvT_TwfT [in LN_Template]
PWellformed.TenvT_weaken [in LN_Template]
PWellformed.TenvT_weaken_left [in LN_Template]
PWellformed.TenvT_weaken_right [in LN_Template]
PWellformed.Tfsubst_fresh [in LN_Template]
R
red_regular [in LN_Fsub_basic_Infrastructure]red_regular [in LN_Fsub_adv_Infrastructure]
red_regular [in LN_STLC_basic_Infrastructure]
Rep_dec [in DGP_Core]
Rep_dec_or [in DGP_Core]
Rep_dec_unicity [in DGP_Core]
S
sort_dec [in CoqListFacts]Sort_InA_eq [in CoqListFacts]
Sort_In_eq [in CoqListFacts]
sort_unique [in CoqListFacts]
subst_preserves_typing [in dB_Fsub_basic_Main]
subst_typ_preserves_typing [in dB_Fsub_basic_Main]
subst_typ_preserves_typing_ind [in dB_Fsub_basic_Main]
sub_extensionality [in dB_Fsub_basic_Main]
sub_narrowing [in LN_Fsub_basic_Soundness]
sub_narrowing [in LN_Fsub_adv_Soundness]
sub_narrowing [in dB_Fsub_basic_Main]
sub_narrowing_aux [in LN_Fsub_adv_Soundness]
sub_narrowing_aux [in LN_Fsub_basic_Soundness]
sub_reflexivity [in LN_Fsub_adv_Soundness]
sub_reflexivity [in LN_Fsub_basic_Soundness]
sub_reflexivity [in dB_Fsub_basic_Main]
sub_regular [in LN_Fsub_basic_Infrastructure]
sub_regular [in LN_Fsub_adv_Infrastructure]
sub_strengthening [in LN_Fsub_basic_Soundness]
sub_strengthening [in LN_Fsub_adv_Soundness]
sub_strengthening_right [in dB_Fsub_basic_Main]
sub_through_subst_tt [in LN_Fsub_basic_Soundness]
sub_through_subst_tt [in LN_Fsub_adv_Soundness]
sub_transitivity [in LN_Fsub_adv_Soundness]
sub_transitivity [in dB_Fsub_basic_Main]
sub_transitivity [in LN_Fsub_basic_Soundness]
sub_typ_indep [in LN_Fsub_adv_Infrastructure]
sub_weakening [in LN_Fsub_basic_Soundness]
sub_weakening [in LN_Fsub_adv_Soundness]
sub_weakening_left [in dB_Fsub_basic_Main]
sub_weakening_left_ind [in dB_Fsub_basic_Main]
sub_weakening_right [in dB_Fsub_basic_Main]
sub_weakening_right_ind [in dB_Fsub_basic_Main]
sub_wf [in dB_Fsub_basic_Main]
S_plus_1 [in Arith_Max_extra]
T
Tbfsubst_permutation [in LN_Template_One_Sort]Tbfsubst_permutation [in LN_Template_Two_Sort]
Tbfsubst_permutation_core [in LN_Template_One_Sort]
Tbfsubst_permutation_core [in LN_Template_Two_Sort]
Tbfsubst_permutation_core_TTwf [in LN_Template_Two_Sort]
Tbfsubst_permutation_core_TTwfT [in LN_Template_Two_Sort]
Tbfsubst_permutation_core_wf [in LN_Template_One_Sort]
Tbfsubst_permutation_core_wf [in LN_Template_Two_Sort]
Tbfsubst_permutation_ind [in LN_Template_One_Sort]
Tbfsubst_permutation_ind [in LN_Template_Two_Sort]
Tbfsubst_permutation_ind_wf [in LN_Template_One_Sort]
Tbfsubst_permutation_ind_wf [in LN_Template_Two_Sort]
Tbfsubst_permutation_var [in LN_Template_One_Sort]
Tbfsubst_permutation_var [in LN_Template_Two_Sort]
Tbfsubst_permutation_var_TTwf [in LN_Template_Two_Sort]
Tbfsubst_permutation_var_TTwfT [in LN_Template_Two_Sort]
Tbfsubst_permutation_var_wf [in LN_Template_Two_Sort]
Tbfsubst_permutation_var_wf [in LN_Template_One_Sort]
Tbfsubst_permutation_var_wfT [in LN_Template_Two_Sort]
Tbfsubst_permutation_var_wfT [in LN_Template_One_Sort]
Tbfsubst_permutation_wf [in LN_Template_One_Sort]
Tbfsubst_permutation_wf [in LN_Template_Two_Sort]
Tbfsubst_permutation_wfT [in LN_Template_One_Sort]
Tbfsubst_permutation_wfT [in LN_Template_Two_Sort]
Tbsubst_homo_wf [in LN_Template_One_Sort]
Tbsubst_homo_wf [in LN_Template_Two_Sort]
Tbsubst_var_twice_wf [in LN_Template_One_Sort]
Tbsubst_var_twice_wf [in LN_Template_Two_Sort]
TenvT_dom_subset [in LN_Template_Two_Sort]
TenvT_dom_subset [in LN_Template_One_Sort]
TenvT_Twf [in LN_Template_One_Sort]
TenvT_Twf [in LN_Template_Two_Sort]
TenvT_TwfT [in LN_Template_Two_Sort]
TenvT_TwfT [in LN_Template_One_Sort]
term_TTwf [in LN_Fsub_basic_Infrastructure]
term_TTwfT [in LN_Fsub_adv_Infrastructure]
Tfsubst_fresh [in LN_Template_One_Sort]
Tfsubst_fresh [in LN_Template_Two_Sort]
Tfsubst_Lemma [in LN_Template_Two_Sort]
Tfsubst_Lemma [in LN_Template_One_Sort]
Tget_left_gTget_left [in dB_Template_Two_Sort]
Tget_left_insert_left_ge [in dB_Template_Two_Sort]
Tget_left_insert_left_lt [in dB_Template_Two_Sort]
Tget_left_remove_right [in dB_Template_Two_Sort]
Tget_left_some_gt [in dB_Template_Two_Sort]
Tget_right_gTget_right [in dB_Template_Two_Sort]
Tget_right_insert_left [in dB_Template_Two_Sort]
Tget_right_remove_right_ge [in dB_Template_Two_Sort]
Tget_right_remove_right_lt [in dB_Template_Two_Sort]
Tget_right_wf [in dB_Template_Two_Sort]
THbfsubst_permutation [in LN_Template_Two_Sort]
THbfsubst_permutation_core [in LN_Template_Two_Sort]
THbfsubst_permutation_core_Ywf [in LN_Template_Two_Sort]
THbfsubst_permutation_ind [in LN_Template_Two_Sort]
THbfsubst_permutation_ind_Ywf [in LN_Template_Two_Sort]
THbfsubst_permutation_var [in LN_Template_Two_Sort]
THbfsubst_permutation_var_wf [in LN_Template_Two_Sort]
THbfsubst_permutation_var_wfT [in LN_Template_Two_Sort]
THbfsubst_permutation_wf [in LN_Template_Two_Sort]
THbfsubst_permutation_wfT [in LN_Template_Two_Sort]
THbsubst_hetero [in LN_Template_Two_Sort]
THbsubst_hetero_core_1 [in LN_Template_Two_Sort]
THbsubst_hetero_core_2 [in LN_Template_Two_Sort]
THbsubst_hetero_wf [in LN_Template_Two_Sort]
THbsubst_homo_wf [in LN_Template_Two_Sort]
THbsubst_var_twice_wf [in LN_Template_Two_Sort]
THenvT_dom_subset [in LN_Template_Two_Sort]
THfsubst_fresh [in LN_Template_Two_Sort]
THfsubst_Lemma [in LN_Template_Two_Sort]
THwfT_Tbsubst [in LN_Template_Two_Sort]
THwfT_Tbsubst_1 [in LN_Template_Two_Sort]
THwfT_Tfsubst [in LN_Template_Two_Sort]
THwfT_THfsubst [in LN_Template_Two_Sort]
THwf_Tfsubst [in LN_Template_Two_Sort]
THwf_THfsubst [in LN_Template_Two_Sort]
Tinsert_left_gTinsert_left [in dB_Template_Two_Sort]
Tinsert_left_length [in dB_Template_Two_Sort]
Tinsert_left_length_1 [in dB_Template_Two_Sort]
Tinsert_left_wf_env [in dB_Template_Two_Sort]
Tinsert_left_wf_typ [in dB_Template_Two_Sort]
Tinsert_T [in dB_Template_Two_Sort]
Tinsert_T_ind [in dB_Template_Two_Sort]
Tlth_preserving [in dB_Template_Two_Sort]
transitivity_and_narrowing [in dB_Fsub_basic_Main]
transitivity_case [in dB_Fsub_basic_Main]
trm_typ [in LNameless_Fsub_Iso]
trm_typ [in deBruijn_Fsub_Iso]
trm_typ [in LNameless_STLC_Iso]
TTenvT_fv [in LN_Template_Two_Sort]
TTenvT_narrow [in LN_Template_Two_Sort]
TTenvT_narrow_left [in LN_Template_Two_Sort]
TTenvT_narrow_right [in LN_Template_Two_Sort]
TTenvT_Tfv [in LN_Template_Two_Sort]
TTenvT_THfv [in LN_Template_Two_Sort]
TTenvT_weaken [in LN_Template_Two_Sort]
TTenvT_weaken_left [in LN_Template_Two_Sort]
TTenvT_weaken_right [in LN_Template_Two_Sort]
TTwfT_term [in LN_Fsub_adv_Infrastructure]
TTwfT_Tfsubst [in LN_Template_Two_Sort]
TTwfT_THfsubst [in LN_Template_Two_Sort]
TTwfT_THwf [in LN_Template_Two_Sort]
TTwfT_Twf [in LN_Template_Two_Sort]
TTwf_basic_from_TTwf [in LN_Template_Two_Sort]
TTwf_from_TTwf_basic [in LN_Template_Two_Sort]
TTwf_gTTwf [in LN_Template_Two_Sort]
TTwf_gTTwf_basic [in LN_Template_Two_Sort]
TTwf_term [in LN_Fsub_basic_Infrastructure]
TTwf_Tfsubst [in LN_Template_Two_Sort]
TTwf_THfsubst [in LN_Template_Two_Sort]
TwfT_abs_inv [in LN_STLC_basic_Infrastructure]
TwfT_Tfsubst [in LN_Template_Two_Sort]
TwfT_Tfsubst [in LN_Template_One_Sort]
TwfT_THbsubst [in LN_Template_Two_Sort]
TwfT_THbsubst_1 [in LN_Template_Two_Sort]
TwfT_THfsubst [in LN_Template_Two_Sort]
twf_nil_top [in dB_Fsub_basic_Main]
Twf_Tfsubst [in LN_Template_Two_Sort]
Twf_Tfsubst [in LN_Template_One_Sort]
Twf_THfsubst [in LN_Template_Two_Sort]
Twf_typ_env_weaken [in dB_Template_Two_Sort]
Twf_typ_extensionality [in dB_Template_Two_Sort]
Twf_typ_weakening_left [in dB_Template_Two_Sort]
typefun_value [in dB_Fsub_basic_Main]
type_from_wft [in LN_Fsub_basic_Infrastructure]
type_Ywf [in LN_Fsub_basic_Infrastructure]
type_YwfT [in LN_Fsub_adv_Infrastructure]
typing_inv_abs [in LN_Fsub_basic_Soundness]
typing_inv_abs [in LN_Fsub_adv_Soundness]
typing_inv_tabs [in LN_Fsub_basic_Soundness]
typing_inv_tabs [in LN_Fsub_adv_Soundness]
typing_narrowing [in LN_Fsub_adv_Soundness]
typing_narrowing [in dB_Fsub_basic_Main]
typing_narrowing [in LN_Fsub_basic_Soundness]
typing_narrowing_ind [in dB_Fsub_basic_Main]
typing_regular [in LN_Fsub_adv_Infrastructure]
typing_regular [in LN_Fsub_basic_Infrastructure]
typing_regular [in LN_STLC_basic_Infrastructure]
typing_subst [in LN_STLC_basic_Soundness]
typing_through_subst_ee [in LN_Fsub_basic_Soundness]
typing_through_subst_ee [in LN_Fsub_adv_Soundness]
typing_through_subst_te [in LN_Fsub_basic_Soundness]
typing_through_subst_te [in LN_Fsub_adv_Soundness]
typing_weaken [in LN_STLC_basic_Soundness]
typing_weakening [in LN_Fsub_basic_Soundness]
typing_weakening_left [in dB_Fsub_basic_Main]
typing_weakening_left_ind [in dB_Fsub_basic_Main]
typing_weakening_right [in dB_Fsub_basic_Main]
typing_weakening_right_ind [in dB_Fsub_basic_Main]
typing_weakening_sub [in LN_Fsub_adv_Soundness]
typing_weakening_typ [in LN_Fsub_adv_Soundness]
typing_wf [in dB_Fsub_basic_Main]
typ_noRepr [in deBruijn_Fsub_Iso]
typ_noRepr [in LNameless_Fsub_Iso]
typ_noRepr [in LNameless_STLC_Iso]
t_abs_inversion [in dB_Fsub_basic_Main]
t_tabs_inversion [in dB_Fsub_basic_Main]
U
uniq_dom_only [in LNameless_Meta_Env]uniq_from_wf_env [in LNameless_Meta_Env]
uniq_from_YTwf_env_1 [in LN_Template_Two_Sort]
uniq_from_YTwf_env_2 [in LN_Template_Two_Sort]
V
value_regular [in LN_STLC_basic_Infrastructure]value_regular [in LN_Fsub_adv_Infrastructure]
value_regular [in LN_Fsub_basic_Infrastructure]
W
WDecide_fun.FSetDecideAuxiliary.dec_eq [in CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.dec_In [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_4 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [in CoqFSetDecide]
wfTRep_wfRep [in LNameless_Meta]
wfT_bsubstRep_hetero [in LNameless_Meta]
wfT_bsubstRep_hetero_ [in LNameless_Meta]
wfT_bsubstRep_hetero_1 [in LNameless_Meta]
wfT_bsubst_hetero [in LNameless_Meta]
wfT_bsubst_hetero_ [in LNameless_Meta]
wfT_bsubst_hetero_1 [in LNameless_Meta]
wft_from_env_has_sub [in LN_Fsub_basic_Infrastructure]
wft_from_env_has_typ [in LN_Fsub_basic_Infrastructure]
wft_from_okt_sub [in LN_Fsub_basic_Infrastructure]
wft_from_okt_typ [in LN_Fsub_basic_Infrastructure]
wfT_fsubst [in LNameless_Meta]
wfT_fsubstRep [in LNameless_Meta]
wft_narrow [in LN_Fsub_basic_Infrastructure]
wft_open [in LN_Fsub_adv_Infrastructure]
wft_open [in LN_Fsub_basic_Infrastructure]
wft_strengthen [in LN_Fsub_basic_Infrastructure]
wft_subst_tb [in LN_Fsub_basic_Infrastructure]
wft_weaken [in LN_Fsub_basic_Infrastructure]
wft_weaken_right [in LN_Fsub_basic_Infrastructure]
wfT_wf [in LNameless_Meta]
wft_YTenvT [in LN_Fsub_adv_Infrastructure]
wf_env_binds [in LNameless_Meta_Env]
wf_env_narrow [in LNameless_Meta_Env]
wf_env_narrow_left [in LNameless_Meta_Env]
wf_env_remove_right [in deBruijn_Meta_Env]
wf_from_wf_basic [in LNameless_Meta]
wf_fsubst [in LNameless_Meta]
wf_fsubstRep [in LNameless_Meta]
wf_fsubstRep_ [in LNameless_Meta]
wf_fsubst_ [in LNameless_Meta]
wf_parameter [in LNameless_Meta]
Y
Ybfsubst_permutation [in LN_Template_Two_Sort]Ybfsubst_permutation_core [in LN_Template_Two_Sort]
Ybfsubst_permutation_core_Ywf [in LN_Template_Two_Sort]
Ybfsubst_permutation_ind [in LN_Template_Two_Sort]
Ybfsubst_permutation_ind_Ywf [in LN_Template_Two_Sort]
Ybfsubst_permutation_var [in LN_Template_Two_Sort]
Ybfsubst_permutation_var_wf [in LN_Template_Two_Sort]
Ybfsubst_permutation_var_wfT [in LN_Template_Two_Sort]
Ybfsubst_permutation_wf [in LN_Template_Two_Sort]
Ybfsubst_permutation_wfT [in LN_Template_Two_Sort]
Ybsubst_homo_wf [in LN_Template_Two_Sort]
Ybsubst_var_twice_wf [in LN_Template_Two_Sort]
YenvT_dom_subset [in LN_Template_Two_Sort]
YenvT_from_Ywf_env [in LN_Template_Two_Sort]
YenvT_from_Ywf_env_left [in LN_Template_Two_Sort]
Yfsubst_fresh [in LN_Template_Two_Sort]
Yfsubst_Lemma [in LN_Template_Two_Sort]
YHfsubst_Lemma [in LN_Template_Two_Sort]
Ysubst_preserves_subtyping [in dB_Fsub_basic_Main]
YTenvT_all_inv [in LN_Fsub_adv_Infrastructure]
YTenvT_from_YTwf_env_1 [in LN_Template_Two_Sort]
YTenvT_from_YTwf_env_1_left [in LN_Template_Two_Sort]
YTenvT_from_YTwf_env_2 [in LN_Template_Two_Sort]
YTenvT_from_YTwf_env_2_left [in LN_Template_Two_Sort]
YTenvT_wft [in LN_Fsub_adv_Infrastructure]
YTenvT_Yfv [in LN_Template_Two_Sort]
YTenvT_YwfT [in LN_Template_Two_Sort]
YTwf_env_binds_1 [in LN_Template_Two_Sort]
YTwf_env_binds_2 [in LN_Template_Two_Sort]
YTwf_env_fv_1 [in LN_Template_Two_Sort]
YTwf_env_fv_2 [in LN_Template_Two_Sort]
YTwf_env_map_subst_id_1 [in LN_Template_Two_Sort]
YTwf_env_map_subst_id_2 [in LN_Template_Two_Sort]
YTwf_env_map_subst_id_3 [in LN_Template_Two_Sort]
YTwf_env_narrow [in LN_Template_Two_Sort]
YTwf_env_strengthening [in LN_Template_Two_Sort]
YTwf_env_strengthening_left [in LN_Template_Two_Sort]
YTwf_env_strengthening_1 [in LN_Template_Two_Sort]
YwfT_all_inv [in LN_Fsub_adv_Infrastructure]
YwfT_arrow_inv [in LN_Fsub_adv_Infrastructure]
YwfT_type [in LN_Fsub_adv_Infrastructure]
YwfT_Yfsubst [in LN_Template_Two_Sort]
Ywf_basic_type [in LN_Fsub_basic_Infrastructure]
Ywf_env_binds [in LN_Template_Two_Sort]
Ywf_env_cons [in LN_Template_Two_Sort]
Ywf_env_from_YTwf_env [in LN_Template_Two_Sort]
Ywf_env_narrow [in LN_Template_Two_Sort]
Ywf_env_narrow_left [in LN_Template_Two_Sort]
Ywf_type [in LN_Fsub_basic_Infrastructure]
Ywf_Yfsubst [in LN_Template_Two_Sort]
Section Index
D
DecidableSorting [in CoqListFacts]E
Env_Definitions [in Metatheory_Env]M
Make.AssortedListProperties [in AssocList]Make.BindsDerived [in AssocList]
Make.BindsProperties [in AssocList]
Make.BindsProperties2 [in AssocList]
Make.Disjoint [in AssocList]
Make.ListProperties [in AssocList]
Make.Properties [in AssocList]
Make.UniqDerived [in AssocList]
Make.UniqProperties [in AssocList]
Mapping_Env [in Metatheory_Env]
N
NarrowTrans [in LN_Fsub_basic_Soundness]NarrowTrans [in LN_Fsub_adv_Soundness]
notin_extra [in Metatheory_Env]
Notin_fun.Lemmas [in FSetWeakNotin]
S
Sfun.Spec [in CoqFSetInterface]SortedListEquality [in CoqListFacts]
U
Uniqueness_Of_SetoidList_Proofs [in CoqListFacts]W
WSfun.Spec [in CoqFSetInterface]WSfun.Spec.Filter [in CoqFSetInterface]
Constructor Index
A
abs [in deBruijn_Fsub_Iso]all [in deBruijn_Fsub_Iso]
app [in deBruijn_Fsub_Iso]
appabs [in dB_Fsub_basic_Main]
apparg [in dB_Fsub_basic_Main]
appfun [in dB_Fsub_basic_Main]
arrow [in deBruijn_Fsub_Iso]
B
BIND [in DGP_Core]bind_sub [in LN_Fsub_basic_Definitions]
bind_typ [in LN_Fsub_basic_Definitions]
C
CONST [in DGP_Core]c_apparg [in dB_Fsub_basic_Main]
c_appfun [in dB_Fsub_basic_Main]
c_hole [in dB_Fsub_basic_Main]
c_typefun [in dB_Fsub_basic_Main]
D
Dgp.Bind [in DGP_Core]Dgp.Const [in DGP_Core]
Dgp.InL [in DGP_Core]
Dgp.InR [in DGP_Core]
Dgp.Pair [in DGP_Core]
Dgp.Rec [in DGP_Core]
Dgp.Repr [in DGP_Core]
Dgp.Term [in DGP_Core]
Dgp.Unit [in DGP_Core]
Dgp.Var [in DGP_Core]
E
env_Bind_hetero [in LNameless_Meta_Env]env_Bind_homo [in LNameless_Meta_Env]
env_Bind_REC_hetero [in LNameless_Meta_Env]
env_Bind_REC_homo [in LNameless_Meta_Env]
env_Const [in LNameless_Meta_Env]
env_fvar [in LNameless_Meta_Env]
env_InL [in LNameless_Meta_Env]
env_InR [in LNameless_Meta_Env]
env_Pair [in LNameless_Meta_Env]
env_Rec [in LNameless_Meta_Env]
env_Repr [in LNameless_Meta_Env]
env_Term [in LNameless_Meta_Env]
env_Unit [in LNameless_Meta_Env]
env_Var [in LNameless_Meta_Env]
eq_dec [in CoqEqDec]
es_here [in dB_Fsub_basic_Main]
es_left [in dB_Fsub_basic_Main]
es_right [in dB_Fsub_basic_Main]
E_AppAbs [in dB_Fsub_basic_Main]
E_Ctx [in dB_Fsub_basic_Main]
E_TappTabs [in dB_Fsub_basic_Main]
I
il_here [in deBruijn_Meta_Env]il_left [in deBruijn_Meta_Env]
il_right [in deBruijn_Meta_Env]
M
Make.uniq_nil [in AssocList]Make.uniq_push [in AssocList]
N
narrow_extend_left [in dB_Fsub_basic_Main]narrow_extend_right [in dB_Fsub_basic_Main]
narrow_0 [in dB_Fsub_basic_Main]
O
okt_empty [in LN_Fsub_basic_Definitions]okt_sub [in LN_Fsub_basic_Definitions]
okt_typ [in LN_Fsub_basic_Definitions]
P
PLUS [in DGP_Core]PROD [in DGP_Core]
R
REC [in DGP_Core]red_abs [in LN_Fsub_adv_Definitions]
red_abs [in LN_Fsub_basic_Definitions]
red_app_1 [in LN_Fsub_adv_Definitions]
red_app_1 [in Tutorial_STLC_Formalization]
red_app_1 [in LN_STLC_basic_Definitions]
red_app_1 [in LN_Fsub_basic_Definitions]
red_app_2 [in LN_Fsub_adv_Definitions]
red_app_2 [in LN_Fsub_basic_Definitions]
red_app_2 [in Tutorial_STLC_Formalization]
red_app_2 [in LN_STLC_basic_Definitions]
red_beta [in LN_STLC_basic_Definitions]
red_beta [in Tutorial_STLC_Formalization]
red_tabs [in LN_Fsub_adv_Definitions]
red_tabs [in LN_Fsub_basic_Definitions]
red_tapp [in LN_Fsub_basic_Definitions]
red_tapp [in LN_Fsub_adv_Definitions]
REPR [in DGP_Core]
S
SA_All [in dB_Fsub_basic_Main]SA_Arrow [in dB_Fsub_basic_Main]
SA_Refl_TVar [in dB_Fsub_basic_Main]
SA_Top [in dB_Fsub_basic_Main]
SA_Trans_TVar [in dB_Fsub_basic_Main]
sub_all [in LN_Fsub_basic_Definitions]
sub_all [in LN_Fsub_adv_Definitions]
sub_arrow [in LN_Fsub_adv_Definitions]
sub_arrow [in LN_Fsub_basic_Definitions]
sub_refl_tvar [in LN_Fsub_basic_Definitions]
sub_refl_tvar [in LN_Fsub_adv_Definitions]
sub_top [in LN_Fsub_basic_Definitions]
sub_top [in LN_Fsub_adv_Definitions]
sub_trans_tvar [in LN_Fsub_adv_Definitions]
sub_trans_tvar [in LN_Fsub_basic_Definitions]
T
tabs [in deBruijn_Fsub_Iso]tapp [in deBruijn_Fsub_Iso]
tapptabs [in dB_Fsub_basic_Main]
term_abs [in LN_Fsub_adv_Definitions]
term_abs [in LN_Fsub_basic_Definitions]
term_app [in LN_Fsub_adv_Definitions]
term_app [in LN_Fsub_basic_Definitions]
term_tabs [in LN_Fsub_basic_Definitions]
term_tabs [in LN_Fsub_adv_Definitions]
term_tapp [in LN_Fsub_basic_Definitions]
term_tapp [in LN_Fsub_adv_Definitions]
term_var [in LN_Fsub_basic_Definitions]
term_var [in LN_Fsub_adv_Definitions]
Til_here [in dB_Template_Two_Sort]
Til_left [in dB_Template_Two_Sort]
Til_right [in dB_Template_Two_Sort]
top [in deBruijn_Fsub_Iso]
trm_abs [in LNameless_Fsub_Iso]
trm_abs [in LNameless_STLC_Iso]
trm_abs [in Tutorial_STLC_Iso]
trm_abs [in Tutorial_STLC_Syntax]
trm_app [in Tutorial_STLC_Syntax]
trm_app [in LNameless_STLC_Iso]
trm_app [in LNameless_Fsub_Iso]
trm_app [in Tutorial_STLC_Iso]
trm_bvar [in LNameless_Fsub_Iso]
trm_bvar [in LNameless_STLC_Iso]
trm_bvar [in Tutorial_STLC_Syntax]
trm_bvar [in Tutorial_STLC_Iso]
trm_fvar [in Tutorial_STLC_Syntax]
trm_fvar [in Tutorial_STLC_Iso]
trm_fvar [in LNameless_Fsub_Iso]
trm_fvar [in LNameless_STLC_Iso]
trm_tabs [in LNameless_Fsub_Iso]
trm_tapp [in LNameless_Fsub_Iso]
tvar [in deBruijn_Fsub_Iso]
typefun [in dB_Fsub_basic_Main]
type_all [in LN_Fsub_adv_Definitions]
type_all [in LN_Fsub_basic_Definitions]
type_arrow [in LN_Fsub_basic_Definitions]
type_arrow [in LN_Fsub_adv_Definitions]
type_top [in LN_Fsub_basic_Definitions]
type_top [in LN_Fsub_adv_Definitions]
type_var [in LN_Fsub_adv_Definitions]
type_var [in LN_Fsub_basic_Definitions]
typing_abs [in LN_Fsub_adv_Definitions]
typing_abs [in LN_STLC_basic_Definitions]
typing_abs [in LN_Fsub_basic_Definitions]
typing_abs [in Tutorial_STLC_Formalization]
typing_app [in LN_Fsub_basic_Definitions]
typing_app [in LN_STLC_basic_Definitions]
typing_app [in LN_Fsub_adv_Definitions]
typing_app [in Tutorial_STLC_Formalization]
typing_sub [in LN_Fsub_adv_Definitions]
typing_sub [in LN_Fsub_basic_Definitions]
typing_tabs [in LN_Fsub_adv_Definitions]
typing_tabs [in LN_Fsub_basic_Definitions]
typing_tapp [in LN_Fsub_adv_Definitions]
typing_tapp [in LN_Fsub_basic_Definitions]
typing_var [in LN_Fsub_basic_Definitions]
typing_var [in LN_Fsub_adv_Definitions]
typing_var [in LN_STLC_basic_Definitions]
typing_var [in Tutorial_STLC_Formalization]
typ_all [in LNameless_Fsub_Iso]
typ_arrow [in Tutorial_STLC_Syntax]
typ_arrow [in LNameless_STLC_Iso]
typ_arrow [in LNameless_Fsub_Iso]
typ_arrow [in Tutorial_STLC_Iso]
typ_bvar [in LNameless_Fsub_Iso]
typ_fvar [in LNameless_Fsub_Iso]
typ_top [in LNameless_Fsub_Iso]
typ_var [in Tutorial_STLC_Syntax]
typ_var [in Tutorial_STLC_Iso]
typ_var [in LNameless_STLC_Iso]
T_Abs [in dB_Fsub_basic_Main]
T_App [in dB_Fsub_basic_Main]
T_Sub [in dB_Fsub_basic_Main]
T_Tabs [in dB_Fsub_basic_Main]
T_Tapp [in dB_Fsub_basic_Main]
T_Var [in dB_Fsub_basic_Main]
U
UNIT [in DGP_Core]V
value_abs [in Tutorial_STLC_Formalization]value_abs [in LN_STLC_basic_Definitions]
value_abs [in LN_Fsub_adv_Definitions]
value_abs [in LN_Fsub_basic_Definitions]
value_tabs [in LN_Fsub_basic_Definitions]
value_tabs [in LN_Fsub_adv_Definitions]
var [in deBruijn_Fsub_Iso]
W
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [in CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [in CoqFSetDecide]
wft_all [in LN_Fsub_basic_Definitions]
wft_all [in LN_Fsub_adv_Definitions]
wft_arrow [in LN_Fsub_basic_Definitions]
wft_arrow [in LN_Fsub_adv_Definitions]
wft_top [in LN_Fsub_basic_Definitions]
wft_top [in LN_Fsub_adv_Definitions]
wft_var [in LN_Fsub_adv_Definitions]
wft_var [in LN_Fsub_basic_Definitions]
wf_Bind_hetero [in LNameless_Meta]
wf_Bind_homo [in LNameless_Meta]
wf_Bind_REC_hetero [in LNameless_Meta]
wf_Bind_REC_homo [in LNameless_Meta]
wf_Const [in LNameless_Meta]
wf_env_cons [in LNameless_Meta_Env]
wf_env_empty [in LNameless_Meta_Env]
wf_fvar [in LNameless_Meta]
wf_InL [in LNameless_Meta]
wf_InR [in LNameless_Meta]
wf_Pair [in LNameless_Meta]
wf_Rec [in LNameless_Meta]
wf_Repr [in LNameless_Meta]
wf_Term [in LNameless_Meta]
wf_Unit [in LNameless_Meta]
wf_Var [in LNameless_Meta]
Y
YTwf_empty [in LN_Template_Two_Sort]YTwf_sub [in LN_Template_Two_Sort]
YTwf_typ [in LN_Template_Two_Sort]
Inductive Index
B
bind [in LN_Fsub_basic_Definitions]C
ctx [in dB_Fsub_basic_Main]D
Dgp.Interpret [in DGP_Core]Dgp.InterpretRep [in DGP_Core]
E
envT [in LNameless_Meta_Env]envTRep [in LNameless_Meta_Env]
env_subst [in dB_Fsub_basic_Main]
EqDec_eq [in CoqEqDec]
I
insert_left [in deBruijn_Meta_Env]M
Make.uniq [in AssocList]N
narrow [in dB_Fsub_basic_Main]O
okt [in LN_Fsub_basic_Definitions]R
red [in LN_STLC_basic_Definitions]red [in LN_Fsub_basic_Definitions]
red [in dB_Fsub_basic_Main]
red [in Tutorial_STLC_Formalization]
red [in LN_Fsub_adv_Definitions]
red' [in dB_Fsub_basic_Main]
Rep [in DGP_Core]
S
sub [in LN_Fsub_basic_Definitions]sub [in LN_Fsub_adv_Definitions]
sub [in dB_Fsub_basic_Main]
T
term [in LN_Fsub_adv_Definitions]term [in deBruijn_Fsub_Iso]
term [in LN_Fsub_basic_Definitions]
Tinsert_left [in dB_Template_Two_Sort]
trm [in Tutorial_STLC_Iso]
trm [in LNameless_Fsub_Iso]
trm [in LNameless_STLC_Iso]
trm [in Tutorial_STLC_Syntax]
typ [in deBruijn_Fsub_Iso]
typ [in LNameless_Fsub_Iso]
typ [in Tutorial_STLC_Iso]
typ [in LNameless_STLC_Iso]
typ [in Tutorial_STLC_Syntax]
type [in LN_Fsub_basic_Definitions]
type [in LN_Fsub_adv_Definitions]
typing [in Tutorial_STLC_Formalization]
typing [in LN_Fsub_adv_Definitions]
typing [in LN_Fsub_basic_Definitions]
typing [in LN_STLC_basic_Definitions]
typing [in dB_Fsub_basic_Main]
V
value [in Tutorial_STLC_Formalization]value [in LN_STLC_basic_Definitions]
value [in LN_Fsub_adv_Definitions]
value [in LN_Fsub_basic_Definitions]
W
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [in CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.FSet_Prop [in CoqFSetDecide]
wft [in LN_Fsub_adv_Definitions]
wfT [in LNameless_Meta]
wft [in LN_Fsub_basic_Definitions]
wfTRep [in LNameless_Meta]
wf_env [in LNameless_Meta_Env]
Y
YTwf_env [in LN_Template_Two_Sort]Abbreviation Index
A
add [in Metatheory_Env]atm [in Tutorial_STLC_Iso]
atm [in LNameless_STLC_Iso]
atoms [in MetatheoryAtom]
D
dBTemplate.TEnv [in dB_Template]E
empty [in Metatheory_Env]ENV [in deBruijn_Meta_Env]
I
Inf [in CoqListFacts]R
remove [in Metatheory_Env]S
singleton [in Metatheory_Env]Sort [in CoqListFacts]
U
union [in Metatheory_Env]V
var [in LNameless_STLC_Iso]var [in Tutorial_STLC_Iso]
var [in LNameless_Fsub_Iso]
Definition Index
A
apply_tuple [in CoqUniquenessTac]arrow [in CoqUniquenessTac]
AtomDT.eq [in MetatheoryAtom]
AtomDT.eq_dec [in MetatheoryAtom]
AtomDT.eq_refl [in MetatheoryAtom]
AtomDT.eq_sym [in MetatheoryAtom]
AtomDT.eq_trans [in MetatheoryAtom]
AtomDT.t [in MetatheoryAtom]
AtomImpl.atom [in MetatheoryAtom]
AtomImpl.eq_atom_dec [in MetatheoryAtom]
B
bsubst [in LNameless_Meta]bsubstRep [in LNameless_Meta]
C
ctx_app [in dB_Fsub_basic_Main]D
dBTemplate.From_TEnv [in dB_Template]dBTemplate.gTget_left [in dB_Template]
dBTemplate.gTget_right [in dB_Template]
dBTemplate.gTinsert_left [in dB_Template]
dBTemplate.gTremove_right [in dB_Template]
dBTemplate.gTwf_env [in dB_Template]
dBTemplate.opt_From [in dB_Template]
dBTemplate.opt_To [in dB_Template]
dBTemplate.Tinsert [in dB_Template]
dBTemplate.Tlth [in dB_Template]
dBTemplate.To_TEnv [in dB_Template]
dBTemplate.Tremove_right [in dB_Template]
dBTemplate.Tshift [in dB_Template]
dBTemplate.Tsubst [in dB_Template]
dBTemplate.Twf_env [in dB_Template]
dBTemplate.Twf_typ [in dB_Template]
dBTemplate.Ysize [in dB_Template]
Dgp.conv [in DGP_Core]
Dgp.QQ [in DGP_Core]
Dgp.size [in DGP_Core]
Dgp.sizeRep [in DGP_Core]
Dgp.VV [in DGP_Core]
DisjUnionUsualDecidableType.eq [in Metatheory_Var]
DisjUnionUsualDecidableType.eq_dec [in Metatheory_Var]
DisjUnionUsualDecidableType.eq_refl [in Metatheory_Var]
DisjUnionUsualDecidableType.eq_sym [in Metatheory_Var]
DisjUnionUsualDecidableType.eq_trans [in Metatheory_Var]
DisjUnionUsualDecidableType.t [in Metatheory_Var]
E
empty_env [in Metatheory_Env]env [in Metatheory_Env]
Env [in deBruijn_Meta_Env]
extends [in Metatheory_Env]
F
freevars [in LNameless_Meta]freevarsRep [in LNameless_Meta]
fsubst [in LNameless_Meta]
fsubstRep [in LNameless_Meta]
fun_inj [in deBruijn_Isomorphism]
fun_inj [in LNameless_Isomorphism]
FWellformed.TenvT [in LN_Template]
FWellformed.THenvT [in LN_Template]
FWellformed.YenvT [in LN_Template]
FWellformed.YHenvT [in LN_Template]
FWellformed.YTenvT [in LN_Template]
FWellformed.Ywf_env [in LN_Template]
G
get_left [in deBruijn_Meta_Env]get_right [in deBruijn_Meta_Env]
gTTwf [in LN_Template_Two_Sort]
gTTwf_basic [in LN_Template_Two_Sort]
H
HO_wf [in deBruijn_Meta_Env]HO_wfRep [in deBruijn_Meta_Env]
I
insert [in deBruijn_Meta_Env]Iso [in LNameless_Isomorphism]
Iso [in deBruijn_Isomorphism]
Iso_nat.From [in Tutorial_STLC_Iso]
Iso_nat.From [in deBruijn_Isomorphism]
Iso_nat.From [in LNameless_Isomorphism]
Iso_nat.RR [in LNameless_Isomorphism]
Iso_nat.RR [in deBruijn_Isomorphism]
Iso_nat.RR [in Tutorial_STLC_Iso]
Iso_nat.To [in LNameless_Isomorphism]
Iso_nat.To [in deBruijn_Isomorphism]
Iso_nat.To [in Tutorial_STLC_Iso]
Iso_nat.To_ [in deBruijn_Isomorphism]
Iso_nat.To_ [in LNameless_Isomorphism]
Iso_nat.To_ [in Tutorial_STLC_Iso]
Iso_nat.TT [in deBruijn_Isomorphism]
Iso_nat.TT [in Tutorial_STLC_Iso]
Iso_nat.TT [in LNameless_Isomorphism]
Iso_partial.ISO [in deBruijn_Isomorphism]
Iso_partial.ISO [in LNameless_Isomorphism]
Iso_trm.From [in LNameless_Fsub_Iso]
Iso_trm.From [in deBruijn_Fsub_Iso]
Iso_trm.From [in LNameless_STLC_Iso]
Iso_trm.From [in Tutorial_STLC_Iso]
Iso_trm.ISO [in Tutorial_STLC_Iso]
Iso_trm.ISO [in LNameless_Fsub_Iso]
Iso_trm.ISO [in LNameless_STLC_Iso]
Iso_trm.ISO [in deBruijn_Fsub_Iso]
Iso_trm.RR [in Tutorial_STLC_Iso]
Iso_trm.RR [in LNameless_STLC_Iso]
Iso_trm.RR [in LNameless_Fsub_Iso]
Iso_trm.RR [in deBruijn_Fsub_Iso]
Iso_trm.To [in Tutorial_STLC_Iso]
Iso_trm.To [in deBruijn_Fsub_Iso]
Iso_trm.To [in LNameless_STLC_Iso]
Iso_trm.To [in LNameless_Fsub_Iso]
Iso_trm.To_ [in LNameless_Fsub_Iso]
Iso_trm.To_ [in deBruijn_Fsub_Iso]
Iso_trm.To_ [in LNameless_STLC_Iso]
Iso_trm.To_ [in Tutorial_STLC_Iso]
Iso_trm.TT [in LNameless_STLC_Iso]
Iso_trm.TT [in Tutorial_STLC_Iso]
Iso_trm.TT [in deBruijn_Fsub_Iso]
Iso_trm.TT [in LNameless_Fsub_Iso]
Iso_typ.From [in Tutorial_STLC_Iso]
Iso_typ.From [in LNameless_STLC_Iso]
Iso_typ.From [in LNameless_Fsub_Iso]
Iso_typ.From [in deBruijn_Fsub_Iso]
Iso_typ.ISO [in deBruijn_Fsub_Iso]
Iso_typ.ISO [in LNameless_Fsub_Iso]
Iso_typ.ISO [in LNameless_STLC_Iso]
Iso_typ.ISO [in Tutorial_STLC_Iso]
Iso_typ.RR [in Tutorial_STLC_Iso]
Iso_typ.RR [in LNameless_STLC_Iso]
Iso_typ.RR [in deBruijn_Fsub_Iso]
Iso_typ.RR [in LNameless_Fsub_Iso]
Iso_typ.To [in LNameless_STLC_Iso]
Iso_typ.To [in LNameless_Fsub_Iso]
Iso_typ.To [in deBruijn_Fsub_Iso]
Iso_typ.To [in Tutorial_STLC_Iso]
Iso_typ.To_ [in LNameless_STLC_Iso]
Iso_typ.To_ [in deBruijn_Fsub_Iso]
Iso_typ.To_ [in Tutorial_STLC_Iso]
Iso_typ.To_ [in LNameless_Fsub_Iso]
Iso_typ.TT [in LNameless_STLC_Iso]
Iso_typ.TT [in Tutorial_STLC_Iso]
Iso_typ.TT [in LNameless_Fsub_Iso]
Iso_typ.TT [in deBruijn_Fsub_Iso]
L
list_rev [in CoqUniquenessTac]LNTemplate.env_fv [in LN_Template]
LNTemplate.gTwf [in LN_Template]
LNTemplate.gTwf_basic [in LN_Template]
LNTemplate.Tbsubst [in LN_Template]
LNTemplate.Tfsubst [in LN_Template]
LNTemplate.Tfv [in LN_Template]
LNTemplate.TSize [in LN_Template]
LNTemplate.Twf [in LN_Template]
LNTemplate.TwfT [in LN_Template]
LNTemplate.Twf_basic [in LN_Template]
lth [in deBruijn_Meta_Env]
M
Make.binds [in AssocList]Make.disjoint [in AssocList]
Make.disjoint [in FSetExtra]
Make.dom [in AssocList]
Make.fresh_list [in FSetExtra]
Make.get [in AssocList]
Make.map [in AssocList]
Make.maps [in AssocList]
Make.notin [in FSetExtra]
Make.one [in AssocList]
N
narrowing_prop [in dB_Fsub_basic_Main]noRepr [in DGP_Core]
O
opt_map [in deBruijn_Meta_Env]P
preservation [in LN_Fsub_basic_Definitions]preservation [in LN_Fsub_adv_Definitions]
preservation [in LN_STLC_basic_Definitions]
preservation [in Tutorial_STLC_Formalization]
progress [in LN_STLC_basic_Definitions]
progress [in Tutorial_STLC_Formalization]
progress [in LN_Fsub_adv_Definitions]
progress [in LN_Fsub_basic_Definitions]
PWellformed.TenvT [in LN_Template]
R
remove_right [in deBruijn_Meta_Env]S
Sdep.Add [in CoqFSetInterface]Sdep.elt [in CoqFSetInterface]
Sdep.Empty [in CoqFSetInterface]
Sdep.eq [in CoqFSetInterface]
Sdep.Equal [in CoqFSetInterface]
Sdep.Exists [in CoqFSetInterface]
Sdep.For_all [in CoqFSetInterface]
Sdep.Subset [in CoqFSetInterface]
shift [in deBruijn_Meta]
shiftRep [in deBruijn_Meta]
Single.eq_dec [in Variable_Sets]
Single.t [in Variable_Sets]
subst [in deBruijn_Meta]
substRep [in deBruijn_Meta]
subst_tb [in LN_Fsub_basic_Infrastructure]
T
Tbsubst_var_twice [in LN_Template_Two_Sort]Tget_left [in dB_Template_Two_Sort]
Tget_right [in dB_Template_Two_Sort]
THbsubst_var_twice [in LN_Template_Two_Sort]
transitivity_on [in LN_Fsub_basic_Soundness]
transitivity_on [in LN_Fsub_adv_Soundness]
transitivity_prop [in dB_Fsub_basic_Main]
tr_list_rev [in CoqUniquenessTac]
tr_tuple_rev [in CoqUniquenessTac]
TSize_Tbsubst [in LN_Template_Two_Sort]
TSize_THbsubst [in LN_Template_Two_Sort]
TTenvT [in LN_Template_Two_Sort]
TTwf [in LN_Template_Two_Sort]
TTwfT [in LN_Template_Two_Sort]
TTwf_basic [in LN_Template_Two_Sort]
tuple [in CoqUniquenessTac]
tuple_rev [in CoqUniquenessTac]
V
value [in dB_Fsub_basic_Main]W
wf [in LNameless_Meta]wfRep [in LNameless_Meta]
wfRep_basic [in LNameless_Meta]
wf_basic [in LNameless_Meta]
wf_env [in deBruijn_Meta_Env]
wf_term [in dB_Fsub_basic_Main]
WSfun.disjoint [in FSetExtra]
WSfun.elt [in CoqFSetInterface]
WSfun.Empty [in CoqFSetInterface]
WSfun.eq [in CoqFSetInterface]
WSfun.Equal [in CoqFSetInterface]
WSfun.Exists [in CoqFSetInterface]
WSfun.For_all [in CoqFSetInterface]
WSfun.fresh_list [in FSetExtra]
WSfun.notin [in FSetExtra]
WSfun.Subset [in CoqFSetInterface]
Y
Ybsubst_var_twice [in LN_Template_Two_Sort]YSize_Ybsubst [in LN_Template_Two_Sort]
Module Index
A
ATOM [in MetatheoryAtom]AtomDT [in MetatheoryAtom]
AtomImpl [in MetatheoryAtom]
AtomSetDecide [in MetatheoryAtom]
AtomSetFacts [in MetatheoryAtom]
AtomSetImpl [in MetatheoryAtom]
AtomSetNotin [in MetatheoryAtom]
AtomSetProperties [in MetatheoryAtom]
D
D [in AssocList]D [in FSetWeakNotin]
dBTemplate [in dB_Template]
deBruijn [in deBruijn_Meta]
Decide [in CoqFSetDecide]
Dgp [in DGP_Core]
DisjUnionUsualDecidableType [in Metatheory_Var]
E
E [in CoqFSetInterface]E [in CoqFSetInterface]
E [in CoqFSetInterface]
EnvImpl [in Metatheory_Env]
F
F [in CoqFSetDecide]FSetDecideAuxiliary [in CoqFSetDecide]
FSetDecideTestCases [in CoqFSetDecide]
FSetLogicalFacts [in CoqFSetDecide]
FWellformed [in LN_Template]
G
GenericVarSig [in Metatheory_Var]GVar_to_Quant [in Metatheory_Var]
I
Iso_full [in LNameless_Isomorphism]Iso_full [in deBruijn_Isomorphism]
Iso_nat [in LNameless_Isomorphism]
Iso_nat [in deBruijn_Isomorphism]
Iso_nat [in Tutorial_STLC_Iso]
Iso_partial [in deBruijn_Isomorphism]
Iso_partial [in LNameless_Isomorphism]
Iso_trm [in LNameless_STLC_Iso]
Iso_trm [in Tutorial_STLC_Iso]
Iso_trm [in deBruijn_Fsub_Iso]
Iso_trm [in LNameless_Fsub_Iso]
Iso_typ [in Tutorial_STLC_Iso]
Iso_typ [in LNameless_Fsub_Iso]
Iso_typ [in LNameless_STLC_Iso]
Iso_typ [in deBruijn_Fsub_Iso]
K
KeySetFacts [in AssocList]KeySetProperties [in AssocList]
L
LNameless [in LNameless_Meta]LNTemplate [in LN_Template]
M
M [in LN_Template]M [in LN_Template]
Make [in FSetExtra]
Make [in AssocList]
MT [in dB_Template_Two_Sort]
MT [in LN_Template_One_Sort]
MT [in LN_Template_Two_Sort]
MY [in LN_Template_One_Sort]
MY [in LN_Template_Two_Sort]
MY [in dB_Template_Two_Sort]
M_tt [in LN_Template_One_Sort]
M_tt [in dB_Template_Two_Sort]
M_tt [in LN_Template_Two_Sort]
M_ty [in dB_Template_Two_Sort]
M_ty [in LN_Template_Two_Sort]
M_yt [in LN_Template_Two_Sort]
M_yt [in dB_Template_Two_Sort]
M_yt [in LN_Template_One_Sort]
M_yy [in dB_Template_Two_Sort]
M_yy [in LN_Template_Two_Sort]
N
Nat [in Variable_Sets]Notin_fun [in FSetWeakNotin]
P
PWellformed [in LN_Template]Q
QuantificationVarSig [in Metatheory_Var]S
S [in CoqFSetInterface]Sdep [in CoqFSetInterface]
Sfun [in CoqFSetInterface]
Single [in Variable_Sets]
T
TwoNat [in Variable_Sets]W
WDecide [in CoqFSetDecide]WDecide_fun [in CoqFSetDecide]
WS [in CoqFSetInterface]
WSfun [in FSetExtra]
WSfun [in CoqFSetInterface]
Axiom Index
A
ATOM.atom [in MetatheoryAtom]ATOM.atom_fresh_for_list [in MetatheoryAtom]
ATOM.eq_atom_dec [in MetatheoryAtom]
I
Iso_full.From_To [in LNameless_Isomorphism]Iso_full.From_To [in deBruijn_Isomorphism]
Iso_full.To_inj [in deBruijn_Isomorphism]
Iso_full.To_inj [in LNameless_Isomorphism]
Iso_partial.From [in LNameless_Isomorphism]
Iso_partial.From [in deBruijn_Isomorphism]
Iso_partial.From_inj [in deBruijn_Isomorphism]
Iso_partial.From_inj [in LNameless_Isomorphism]
Iso_partial.RR [in LNameless_Isomorphism]
Iso_partial.RR [in deBruijn_Isomorphism]
Iso_partial.To [in LNameless_Isomorphism]
Iso_partial.To [in deBruijn_Isomorphism]
Iso_partial.To_From [in deBruijn_Isomorphism]
Iso_partial.To_From [in LNameless_Isomorphism]
Iso_partial.TT [in deBruijn_Isomorphism]
Iso_partial.TT [in LNameless_Isomorphism]
S
Sdep.add [in CoqFSetInterface]Sdep.cardinal [in CoqFSetInterface]
Sdep.choose [in CoqFSetInterface]
Sdep.choose_equal [in CoqFSetInterface]
Sdep.compare [in CoqFSetInterface]
Sdep.diff [in CoqFSetInterface]
Sdep.elements [in CoqFSetInterface]
Sdep.empty [in CoqFSetInterface]
Sdep.equal [in CoqFSetInterface]
Sdep.eq_In [in CoqFSetInterface]
Sdep.eq_refl [in CoqFSetInterface]
Sdep.eq_sym [in CoqFSetInterface]
Sdep.eq_trans [in CoqFSetInterface]
Sdep.exists_ [in CoqFSetInterface]
Sdep.filter [in CoqFSetInterface]
Sdep.fold [in CoqFSetInterface]
Sdep.for_all [in CoqFSetInterface]
Sdep.In [in CoqFSetInterface]
Sdep.inter [in CoqFSetInterface]
Sdep.is_empty [in CoqFSetInterface]
Sdep.lt [in CoqFSetInterface]
Sdep.lt_not_eq [in CoqFSetInterface]
Sdep.lt_trans [in CoqFSetInterface]
Sdep.max_elt [in CoqFSetInterface]
Sdep.mem [in CoqFSetInterface]
Sdep.min_elt [in CoqFSetInterface]
Sdep.partition [in CoqFSetInterface]
Sdep.remove [in CoqFSetInterface]
Sdep.singleton [in CoqFSetInterface]
Sdep.subset [in CoqFSetInterface]
Sdep.t [in CoqFSetInterface]
Sdep.union [in CoqFSetInterface]
Sfun.choose_3 [in CoqFSetInterface]
Sfun.compare [in CoqFSetInterface]
Sfun.elements_3 [in CoqFSetInterface]
Sfun.lt [in CoqFSetInterface]
Sfun.lt_not_eq [in CoqFSetInterface]
Sfun.lt_trans [in CoqFSetInterface]
Sfun.max_elt [in CoqFSetInterface]
Sfun.max_elt_1 [in CoqFSetInterface]
Sfun.max_elt_2 [in CoqFSetInterface]
Sfun.max_elt_3 [in CoqFSetInterface]
Sfun.min_elt [in CoqFSetInterface]
Sfun.min_elt_1 [in CoqFSetInterface]
Sfun.min_elt_2 [in CoqFSetInterface]
Sfun.min_elt_3 [in CoqFSetInterface]
skip [in LibTactics]
W
WSfun.add [in CoqFSetInterface]WSfun.add_1 [in CoqFSetInterface]
WSfun.add_2 [in CoqFSetInterface]
WSfun.add_3 [in CoqFSetInterface]
WSfun.cardinal [in CoqFSetInterface]
WSfun.cardinal_1 [in CoqFSetInterface]
WSfun.choose [in CoqFSetInterface]
WSfun.choose_1 [in CoqFSetInterface]
WSfun.choose_2 [in CoqFSetInterface]
WSfun.diff [in CoqFSetInterface]
WSfun.diff_1 [in CoqFSetInterface]
WSfun.diff_2 [in CoqFSetInterface]
WSfun.diff_3 [in CoqFSetInterface]
WSfun.elements [in CoqFSetInterface]
WSfun.elements_1 [in CoqFSetInterface]
WSfun.elements_2 [in CoqFSetInterface]
WSfun.elements_3w [in CoqFSetInterface]
WSfun.empty [in CoqFSetInterface]
WSfun.empty_1 [in CoqFSetInterface]
WSfun.equal [in CoqFSetInterface]
WSfun.equal_1 [in CoqFSetInterface]
WSfun.equal_2 [in CoqFSetInterface]
WSfun.eq_dec [in CoqFSetInterface]
WSfun.eq_refl [in CoqFSetInterface]
WSfun.eq_sym [in CoqFSetInterface]
WSfun.eq_trans [in CoqFSetInterface]
WSfun.exists_ [in CoqFSetInterface]
WSfun.exists_1 [in CoqFSetInterface]
WSfun.exists_2 [in CoqFSetInterface]
WSfun.filter [in CoqFSetInterface]
WSfun.filter_1 [in CoqFSetInterface]
WSfun.filter_2 [in CoqFSetInterface]
WSfun.filter_3 [in CoqFSetInterface]
WSfun.fold [in CoqFSetInterface]
WSfun.fold_1 [in CoqFSetInterface]
WSfun.for_all [in CoqFSetInterface]
WSfun.for_all_1 [in CoqFSetInterface]
WSfun.for_all_2 [in CoqFSetInterface]
WSfun.In [in CoqFSetInterface]
WSfun.inter [in CoqFSetInterface]
WSfun.inter_1 [in CoqFSetInterface]
WSfun.inter_2 [in CoqFSetInterface]
WSfun.inter_3 [in CoqFSetInterface]
WSfun.In_1 [in CoqFSetInterface]
WSfun.is_empty [in CoqFSetInterface]
WSfun.is_empty_1 [in CoqFSetInterface]
WSfun.is_empty_2 [in CoqFSetInterface]
WSfun.mem [in CoqFSetInterface]
WSfun.mem_1 [in CoqFSetInterface]
WSfun.mem_2 [in CoqFSetInterface]
WSfun.partition [in CoqFSetInterface]
WSfun.partition_1 [in CoqFSetInterface]
WSfun.partition_2 [in CoqFSetInterface]
WSfun.remove [in CoqFSetInterface]
WSfun.remove_1 [in CoqFSetInterface]
WSfun.remove_2 [in CoqFSetInterface]
WSfun.remove_3 [in CoqFSetInterface]
WSfun.singleton [in CoqFSetInterface]
WSfun.singleton_1 [in CoqFSetInterface]
WSfun.singleton_2 [in CoqFSetInterface]
WSfun.subset [in CoqFSetInterface]
WSfun.subset_1 [in CoqFSetInterface]
WSfun.subset_2 [in CoqFSetInterface]
WSfun.t [in CoqFSetInterface]
WSfun.union [in CoqFSetInterface]
WSfun.union_1 [in CoqFSetInterface]
WSfun.union_2 [in CoqFSetInterface]
WSfun.union_3 [in CoqFSetInterface]
Variable Index
D
DecidableSorting.A [in CoqListFacts]DecidableSorting.leA [in CoqListFacts]
DecidableSorting.leA_dec [in CoqListFacts]
E
Env_Definitions.A [in Metatheory_Env]M
Make.AssortedListProperties.x [in AssocList]Make.AssortedListProperties.X [in AssocList]
Make.AssortedListProperties.xs [in AssocList]
Make.AssortedListProperties.ys [in AssocList]
Make.AssortedListProperties.zs [in AssocList]
Make.BindsDerived.a [in AssocList]
Make.BindsDerived.A [in AssocList]
Make.BindsDerived.b [in AssocList]
Make.BindsDerived.B [in AssocList]
Make.BindsDerived.E [in AssocList]
Make.BindsDerived.F [in AssocList]
Make.BindsDerived.f [in AssocList]
Make.BindsDerived.G [in AssocList]
Make.BindsDerived.x [in AssocList]
Make.BindsDerived.y [in AssocList]
Make.BindsProperties.A [in AssocList]
Make.BindsProperties.a [in AssocList]
Make.BindsProperties.B [in AssocList]
Make.BindsProperties.b [in AssocList]
Make.BindsProperties.E [in AssocList]
Make.BindsProperties.f [in AssocList]
Make.BindsProperties.F [in AssocList]
Make.BindsProperties.G [in AssocList]
Make.BindsProperties.x [in AssocList]
Make.BindsProperties.y [in AssocList]
Make.BindsProperties2.a [in AssocList]
Make.BindsProperties2.A [in AssocList]
Make.BindsProperties2.B [in AssocList]
Make.BindsProperties2.b [in AssocList]
Make.BindsProperties2.E [in AssocList]
Make.BindsProperties2.f [in AssocList]
Make.BindsProperties2.F [in AssocList]
Make.BindsProperties2.G [in AssocList]
Make.BindsProperties2.x [in AssocList]
Make.BindsProperties2.y [in AssocList]
Make.ListProperties.l [in AssocList]
Make.ListProperties.l1 [in AssocList]
Make.ListProperties.l2 [in AssocList]
Make.ListProperties.l3 [in AssocList]
Make.ListProperties.x [in AssocList]
Make.ListProperties.X [in AssocList]
Make.ListProperties.y [in AssocList]
Make.Properties.a [in AssocList]
Make.Properties.A [in AssocList]
Make.Properties.b [in AssocList]
Make.Properties.B [in AssocList]
Make.Properties.c [in AssocList]
Make.Properties.E [in AssocList]
Make.Properties.F [in AssocList]
Make.Properties.f [in AssocList]
Make.Properties.g [in AssocList]
Make.Properties.G [in AssocList]
Make.Properties.key [in AssocList]
Make.Properties.x [in AssocList]
Make.Properties.y [in AssocList]
Make.UniqDerived.A [in AssocList]
Make.UniqDerived.a [in AssocList]
Make.UniqDerived.b [in AssocList]
Make.UniqDerived.E [in AssocList]
Make.UniqDerived.F [in AssocList]
Make.UniqDerived.G [in AssocList]
Make.UniqDerived.x [in AssocList]
Make.UniqDerived.y [in AssocList]
Make.UniqProperties.a [in AssocList]
Make.UniqProperties.A [in AssocList]
Make.UniqProperties.b [in AssocList]
Make.UniqProperties.B [in AssocList]
Make.UniqProperties.E [in AssocList]
Make.UniqProperties.F [in AssocList]
Make.UniqProperties.f [in AssocList]
Make.UniqProperties.G [in AssocList]
Make.UniqProperties.x [in AssocList]
Mapping_Env.A [in Metatheory_Env]
Mapping_Env.B [in Metatheory_Env]
Mapping_Env.f [in Metatheory_Env]
Mapping_Env.g [in Metatheory_Env]
N
Notin_fun.Lemmas.s [in FSetWeakNotin]Notin_fun.Lemmas.s' [in FSetWeakNotin]
Notin_fun.Lemmas.x [in FSetWeakNotin]
Notin_fun.Lemmas.y [in FSetWeakNotin]
S
Sfun.Spec.s [in CoqFSetInterface]Sfun.Spec.s' [in CoqFSetInterface]
Sfun.Spec.s'' [in CoqFSetInterface]
Sfun.Spec.x [in CoqFSetInterface]
Sfun.Spec.y [in CoqFSetInterface]
SortedListEquality.A [in CoqListFacts]
SortedListEquality.eqA_ltA [in CoqListFacts]
SortedListEquality.ltA [in CoqListFacts]
SortedListEquality.ltA_eqA [in CoqListFacts]
SortedListEquality.ltA_not_eqA [in CoqListFacts]
SortedListEquality.ltA_trans [in CoqListFacts]
U
Uniqueness_Of_SetoidList_Proofs.A [in CoqListFacts]Uniqueness_Of_SetoidList_Proofs.list_eq_dec [in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R [in CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R_unique [in CoqListFacts]
W
WSfun.Spec.Filter.f [in CoqFSetInterface]WSfun.Spec.s [in CoqFSetInterface]
WSfun.Spec.s' [in CoqFSetInterface]
WSfun.Spec.s'' [in CoqFSetInterface]
WSfun.Spec.x [in CoqFSetInterface]
WSfun.Spec.y [in CoqFSetInterface]
Library Index
A
Arith_Max_extraAssocList
C
CoqEqDecCoqFSetDecide
CoqFSetInterface
CoqListFacts
CoqUniquenessTac
D
dB_Fsub_basic_MaindB_Template
dB_Template_Two_Sort
deBruijn_Fsub_Iso
deBruijn_Isomorphism
deBruijn_Meta
deBruijn_Meta_Env
DGP_Core
F
FSetExtraFSetWeakNotin
L
LibTacticsLNameless_Fsub_Iso
LNameless_Isomorphism
LNameless_Meta
LNameless_Meta_Env
LNameless_STLC_Iso
LN_Fsub_adv_Definitions
LN_Fsub_adv_Infrastructure
LN_Fsub_adv_Soundness
LN_Fsub_basic_Definitions
LN_Fsub_basic_Infrastructure
LN_Fsub_basic_Soundness
LN_STLC_basic_Definitions
LN_STLC_basic_Infrastructure
LN_STLC_basic_Soundness
LN_Template
LN_Template_One_Sort
LN_Template_Two_Sort
M
MetatheoryAtomMetatheory_Env
Metatheory_Var
T
Tutorial_STLC_FormalizationTutorial_STLC_Iso
Tutorial_STLC_Syntax
V
Variable_Sets| 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 | _ | (1749 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (2 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
| 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 | _ | (858 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (21 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 | _ | (220 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 | _ | (54 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (15 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 | _ | (217 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 | _ | (79 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 | _ | (134 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (105 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 | _ | (42 entries) |
This page has been generated by coqdoc