| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1929 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (141 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (902 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (213 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (202 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Global Index
A
add [abbreviation, in Metalib.Metatheory]apply_tuple [definition, in Metalib.CoqUniquenessTac]
app_cons_not_nil [lemma, in Metalib.CoqListFacts]
app_eq_cons [lemma, in Metalib.CoqListFacts]
arrow [definition, in Metalib.CoqUniquenessTac]
AssocList [library]
atom [abbreviation, in Metalib.MetatheoryAtom]
Atom [module, in Metalib.MetatheoryAtom]
ATOM [module, in Metalib.MetatheoryAtom]
atoms [abbreviation, in Metalib.MetatheoryAtom]
AtomSetDecide [module, in Metalib.MetatheoryAtom]
AtomSetFacts [module, in Metalib.MetatheoryAtom]
AtomSetImpl [module, in Metalib.MetatheoryAtom]
AtomSetNotin [module, in Metalib.MetatheoryAtom]
AtomSetProperties [module, in Metalib.MetatheoryAtom]
atom_fresh [lemma, in Metalib.MetatheoryAtom]
atom_fresh_for_list [abbreviation, in Metalib.MetatheoryAtom]
Atom.atom [definition, in Metalib.MetatheoryAtom]
ATOM.atom [axiom, in Metalib.MetatheoryAtom]
Atom.atom_fresh_for_list [lemma, in Metalib.MetatheoryAtom]
ATOM.atom_fresh_for_list [axiom, in Metalib.MetatheoryAtom]
Atom.eq_dec [definition, in Metalib.MetatheoryAtom]
ATOM.eq_dec [axiom, in Metalib.MetatheoryAtom]
Atom.fresh [definition, in Metalib.MetatheoryAtom]
ATOM.fresh [axiom, in Metalib.MetatheoryAtom]
Atom.fresh_not_in [lemma, in Metalib.MetatheoryAtom]
ATOM.fresh_not_in [axiom, in Metalib.MetatheoryAtom]
Atom.max_lt_r [lemma, in Metalib.MetatheoryAtom]
Atom.nat_of [definition, in Metalib.MetatheoryAtom]
Atom.nat_list_max [lemma, in Metalib.MetatheoryAtom]
ATOM.nat_of [axiom, in Metalib.MetatheoryAtom]
Atom.t [definition, in Metalib.MetatheoryAtom]
ATOM.t [definition, in Metalib.MetatheoryAtom]
B
binding [inductive, in LNgen.Fsub_ott]binding [inductive, in LN.Fsub_Definitions]
binding_mutrec [definition, in LNgen.Fsub_inf]
binding_rec' [definition, in LNgen.Fsub_inf]
binding_mutind [definition, in LNgen.Fsub_inf]
binding_ind' [definition, in LNgen.Fsub_inf]
binds_map [abbreviation, in Metalib.Metatheory]
binds_app_r [abbreviation, in Metalib.Metatheory]
binds_app_l [abbreviation, in Metalib.Metatheory]
binds_cons [abbreviation, in Metalib.Metatheory]
binds_one [abbreviation, in Metalib.Metatheory]
bind_typ [constructor, in LNgen.Fsub_ott]
bind_sub [constructor, in LNgen.Fsub_ott]
bind_typ [constructor, in LN.Fsub_Definitions]
bind_sub [constructor, in LN.Fsub_Definitions]
body_exp_wrt_exp [definition, in LNgen.Fsub_inf]
body_exp_wrt_typ [definition, in LNgen.Fsub_inf]
body_binding_wrt_typ [definition, in LNgen.Fsub_inf]
body_typ_wrt_typ [definition, in LNgen.Fsub_inf]
body_inr_from_expr_case [lemma, in LN.Fsub_Infrastructure]
body_inl_from_expr_case [lemma, in LN.Fsub_Infrastructure]
body_from_expr_let [lemma, in LN.Fsub_Infrastructure]
body_e [definition, in LN.Fsub_Definitions]
C
canonical_form_sum [lemma, in LN.Fsub_Soundness]canonical_form_tabs [lemma, in LN.Fsub_Soundness]
canonical_form_abs [lemma, in LN.Fsub_Soundness]
canonical_form_sum [lemma, in LNgen.Fsub_proofs]
canonical_form_tabs [lemma, in LNgen.Fsub_proofs]
canonical_form_abs [lemma, in LNgen.Fsub_proofs]
close_exp_wrt_exp_lc_exp [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_lc_exp [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_lc_binding [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_lc_typ [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_degree_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_degree_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_degree_exp_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_degree_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_degree_binding_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_degree_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_degree_typ_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_open_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_open_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_open_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_open_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_open_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_open_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_inj [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_inj [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_inj [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_inj [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_inj [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_inj [lemma, in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_inj [lemma, in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_inj [lemma, in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
close_exp_wrt_exp [definition, in LNgen.Fsub_inf]
close_exp_wrt_typ [definition, in LNgen.Fsub_inf]
close_exp_wrt_exp_rec [definition, in LNgen.Fsub_inf]
close_exp_wrt_typ_rec [definition, in LNgen.Fsub_inf]
close_binding_wrt_typ [definition, in LNgen.Fsub_inf]
close_binding_wrt_typ_rec [definition, in LNgen.Fsub_inf]
close_typ_wrt_typ [definition, in LNgen.Fsub_inf]
close_typ_wrt_typ_rec [definition, in LNgen.Fsub_inf]
cons_eq_app [lemma, in Metalib.CoqListFacts]
CoqEqDec [library]
CoqFSetDecide [library]
CoqFSetInterface [library]
CoqListFacts [library]
CoqMSetDecide [library]
CoqMSetInterface [library]
CoqUniquenessTac [library]
CoqUniquenessTacEx [library]
D
DecidableSorting [section, in Metalib.CoqListFacts]DecidableSorting.A [variable, in Metalib.CoqListFacts]
DecidableSorting.leA [variable, in Metalib.CoqListFacts]
DecidableSorting.leA_dec [variable, in Metalib.CoqListFacts]
Decide [module, in Metalib.CoqFSetDecide]
Decide [module, in Metalib.CoqMSetDecide]
degree_exp_wrt_exp_of_lc_exp [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_of_lc_exp_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_of_lc_exp [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_of_lc_exp_mutual [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_of_lc_binding [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_of_lc_binding_mutual [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_of_lc_typ [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_of_lc_typ_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec_inv [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec_inv_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_O [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_O [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_O [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_O [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_S [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_S_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_S [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_typ_S_mutual [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_S [lemma, in LNgen.Fsub_inf]
degree_binding_wrt_typ_S_mutual [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_S [lemma, in LNgen.Fsub_inf]
degree_typ_wrt_typ_S_mutual [lemma, in LNgen.Fsub_inf]
degree_exp_wrt_exp_mutind [definition, in LNgen.Fsub_inf]
degree_exp_wrt_exp_ind' [definition, in LNgen.Fsub_inf]
degree_exp_wrt_typ_mutind [definition, in LNgen.Fsub_inf]
degree_exp_wrt_typ_ind' [definition, in LNgen.Fsub_inf]
degree_wrt_exp_exp_case [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_inr [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_inl [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_let [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_tapp [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_tabs [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_app [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_abs [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_var_b [constructor, in LNgen.Fsub_inf]
degree_wrt_exp_exp_var_f [constructor, in LNgen.Fsub_inf]
degree_exp_wrt_exp [inductive, in LNgen.Fsub_inf]
degree_wrt_typ_exp_case [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_inr [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_inl [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_let [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_tapp [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_tabs [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_app [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_abs [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_var_b [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_exp_var_f [constructor, in LNgen.Fsub_inf]
degree_exp_wrt_typ [inductive, in LNgen.Fsub_inf]
degree_binding_wrt_typ_mutind [definition, in LNgen.Fsub_inf]
degree_binding_wrt_typ_ind' [definition, in LNgen.Fsub_inf]
degree_wrt_typ_bind_typ [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_bind_sub [constructor, in LNgen.Fsub_inf]
degree_binding_wrt_typ [inductive, in LNgen.Fsub_inf]
degree_typ_wrt_typ_mutind [definition, in LNgen.Fsub_inf]
degree_typ_wrt_typ_ind' [definition, in LNgen.Fsub_inf]
degree_wrt_typ_typ_sum [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_typ_all [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_typ_arrow [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_typ_var_b [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_typ_var_f [constructor, in LNgen.Fsub_inf]
degree_wrt_typ_typ_top [constructor, in LNgen.Fsub_inf]
degree_typ_wrt_typ [inductive, in LNgen.Fsub_inf]
E
elim_incl_app [lemma, in Metalib.CoqListFacts]elim_incl_cons [lemma, in Metalib.CoqListFacts]
elim_not_In_app [lemma, in Metalib.CoqListFacts]
elim_not_In_cons [lemma, in Metalib.CoqListFacts]
empty [abbreviation, in Metalib.Metatheory]
empty [abbreviation, in LNgen.Fsub_proofs]
empty [abbreviation, in LN.Fsub_Definitions]
env [definition, in LNgen.Fsub_ott]
env [abbreviation, in LN.Fsub_Definitions]
EnvImpl [module, in Metalib.Metatheory]
EqDec_atom [instance, in Metalib.MetatheoryAtom]
EqDec_eq_of_EqDec [instance, in Metalib.CoqEqDec]
EqDec_eq [record, in Metalib.CoqEqDec]
EqDec_eq [inductive, in Metalib.CoqEqDec]
eqlistA_unique [lemma, in Metalib.CoqListFacts]
eqlistA_ind' [definition, in Metalib.CoqListFacts]
eqlistA_unique [lemma, in Metalib.CoqUniquenessTacEx]
eqlistA_ind' [definition, in Metalib.CoqUniquenessTacEx]
eqlist_eq [lemma, in Metalib.CoqListFacts]
Equal_union_compat [lemma, in Metalib.LibLNgen]
equiv_decidable [lemma, in Metalib.CoqEqDec]
equiv_transitive' [lemma, in Metalib.CoqEqDec]
equiv_symmetric' [lemma, in Metalib.CoqEqDec]
equiv_reflexive' [lemma, in Metalib.CoqEqDec]
eq_var [abbreviation, in Metalib.Metatheory]
eq_pair_dec [lemma, in Metalib.CoqUniquenessTac]
eq_unit_dec [lemma, in Metalib.CoqUniquenessTac]
eq_dec_refl [lemma, in Metalib.CoqEqDec]
eq_dec [projection, in Metalib.CoqEqDec]
eq_dec [constructor, in Metalib.CoqEqDec]
example_pick_fresh_use [lemma, in Metalib.MetatheoryAtom]
exp [inductive, in LNgen.Fsub_ott]
exp [inductive, in LN.Fsub_Definitions]
expr [inductive, in LN.Fsub_Definitions]
expr_case_from_body [lemma, in LN.Fsub_Infrastructure]
expr_let_from_body [lemma, in LN.Fsub_Infrastructure]
expr_case [constructor, in LN.Fsub_Definitions]
expr_inr [constructor, in LN.Fsub_Definitions]
expr_inl [constructor, in LN.Fsub_Definitions]
expr_let [constructor, in LN.Fsub_Definitions]
expr_tapp [constructor, in LN.Fsub_Definitions]
expr_tabs [constructor, in LN.Fsub_Definitions]
expr_app [constructor, in LN.Fsub_Definitions]
expr_abs [constructor, in LN.Fsub_Definitions]
expr_var [constructor, in LN.Fsub_Definitions]
expvar [definition, in LNgen.Fsub_ott]
exp_mutrec [definition, in LNgen.Fsub_inf]
exp_rec' [definition, in LNgen.Fsub_inf]
exp_mutind [definition, in LNgen.Fsub_inf]
exp_ind' [definition, in LNgen.Fsub_inf]
exp_case [constructor, in LNgen.Fsub_ott]
exp_inr [constructor, in LNgen.Fsub_ott]
exp_inl [constructor, in LNgen.Fsub_ott]
exp_let [constructor, in LNgen.Fsub_ott]
exp_tapp [constructor, in LNgen.Fsub_ott]
exp_tabs [constructor, in LNgen.Fsub_ott]
exp_app [constructor, in LNgen.Fsub_ott]
exp_abs [constructor, in LNgen.Fsub_ott]
exp_var_f [constructor, in LNgen.Fsub_ott]
exp_var_b [constructor, in LNgen.Fsub_ott]
exp_case [constructor, in LN.Fsub_Definitions]
exp_inr [constructor, in LN.Fsub_Definitions]
exp_inl [constructor, in LN.Fsub_Definitions]
exp_let [constructor, in LN.Fsub_Definitions]
exp_tapp [constructor, in LN.Fsub_Definitions]
exp_tabs [constructor, in LN.Fsub_Definitions]
exp_app [constructor, in LN.Fsub_Definitions]
exp_abs [constructor, in LN.Fsub_Definitions]
exp_fvar [constructor, in LN.Fsub_Definitions]
exp_bvar [constructor, in LN.Fsub_Definitions]
F
fresh [abbreviation, in Metalib.MetatheoryAtom]fresh_not_in [abbreviation, in Metalib.MetatheoryAtom]
FSetExtra [library]
FSetWeakNotin [library]
Fsub_Lemmas [library]
Fsub_Soundness [library]
Fsub_proofs [library]
Fsub_Infrastructure [library]
Fsub_Definitions [library]
Fsub_inf [library]
Fsub_ott [library]
fv_exp_in_exp_subst_exp_in_exp_upper [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_upper [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_notin [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_notin_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_notin [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_notin_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_notin [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_notin_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_notin [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_notin_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_notin [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_notin_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_notin [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_notin_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_lower [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_lower [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_fresh [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_fresh_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_fresh [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_fresh_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_fresh [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_fresh_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_fresh [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_fresh_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_fresh [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_fresh_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_upper [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_upper [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_upper [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_upper [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_upper [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_upper_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_lower [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_lower [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_lower [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_lower [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_lower [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_lower_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_close_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_close_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_close_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
fv_typ_in_binding_close_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_close_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
fv_typ_in_typ_close_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
fv_ee [definition, in LN.Fsub_Infrastructure]
fv_te [definition, in LN.Fsub_Infrastructure]
fv_tt [definition, in LN.Fsub_Infrastructure]
fv_typ_in_exp [definition, in LNgen.Fsub_ott]
fv_exp_in_exp [definition, in LNgen.Fsub_ott]
fv_typ_in_binding [definition, in LNgen.Fsub_ott]
fv_typ_in_typ [definition, in LNgen.Fsub_ott]
H
HasOrdOps [module, in Metalib.CoqMSetInterface]HasOrdOps.compare [axiom, in Metalib.CoqMSetInterface]
HasOrdOps.max_elt [axiom, in Metalib.CoqMSetInterface]
HasOrdOps.min_elt [axiom, in Metalib.CoqMSetInterface]
HasWOps [module, in Metalib.CoqMSetInterface]
HasWOps.add [axiom, in Metalib.CoqMSetInterface]
HasWOps.cardinal [axiom, in Metalib.CoqMSetInterface]
HasWOps.choose [axiom, in Metalib.CoqMSetInterface]
HasWOps.diff [axiom, in Metalib.CoqMSetInterface]
HasWOps.elements [axiom, in Metalib.CoqMSetInterface]
HasWOps.empty [axiom, in Metalib.CoqMSetInterface]
HasWOps.equal [axiom, in Metalib.CoqMSetInterface]
HasWOps.exists_ [axiom, in Metalib.CoqMSetInterface]
HasWOps.filter [axiom, in Metalib.CoqMSetInterface]
HasWOps.fold [axiom, in Metalib.CoqMSetInterface]
HasWOps.for_all [axiom, in Metalib.CoqMSetInterface]
HasWOps.inter [axiom, in Metalib.CoqMSetInterface]
HasWOps.is_empty [axiom, in Metalib.CoqMSetInterface]
HasWOps.mem [axiom, in Metalib.CoqMSetInterface]
HasWOps.partition [axiom, in Metalib.CoqMSetInterface]
HasWOps.remove [axiom, in Metalib.CoqMSetInterface]
HasWOps.singleton [axiom, in Metalib.CoqMSetInterface]
HasWOps.subset [axiom, in Metalib.CoqMSetInterface]
HasWOps.union [axiom, in Metalib.CoqMSetInterface]
I
IN [module, in Metalib.CoqMSetInterface]InA_iff_In [lemma, in Metalib.CoqListFacts]
InA_In [lemma, in Metalib.CoqListFacts]
incl_nil [lemma, in Metalib.CoqListFacts]
Inf [abbreviation, in Metalib.CoqListFacts]
In_incl [lemma, in Metalib.CoqListFacts]
In_map [lemma, in Metalib.CoqListFacts]
IN.Empty [definition, in Metalib.CoqMSetInterface]
IN.Equal [definition, in Metalib.CoqMSetInterface]
IN.In [axiom, in Metalib.CoqMSetInterface]
IN.In_compat [instance, in Metalib.CoqMSetInterface]
IN.t [axiom, in Metalib.CoqMSetInterface]
is_value_of_exp [definition, in LNgen.Fsub_ott]
L
lc_set_exp_of_lc_exp [lemma, in LNgen.Fsub_inf]lc_set_exp_of_lc_exp_size_mutual [lemma, in LNgen.Fsub_inf]
lc_set_binding_of_lc_binding [lemma, in LNgen.Fsub_inf]
lc_set_binding_of_lc_binding_size_mutual [lemma, in LNgen.Fsub_inf]
lc_set_typ_of_lc_typ [lemma, in LNgen.Fsub_inf]
lc_set_typ_of_lc_typ_size_mutual [lemma, in LNgen.Fsub_inf]
lc_exp_of_lc_set_exp [lemma, in LNgen.Fsub_inf]
lc_exp_of_lc_set_exp_mutual [lemma, in LNgen.Fsub_inf]
lc_binding_of_lc_set_binding [lemma, in LNgen.Fsub_inf]
lc_binding_of_lc_set_binding_mutual [lemma, in LNgen.Fsub_inf]
lc_typ_of_lc_set_typ [lemma, in LNgen.Fsub_inf]
lc_typ_of_lc_set_typ_mutual [lemma, in LNgen.Fsub_inf]
lc_exp_unique [lemma, in LNgen.Fsub_inf]
lc_exp_unique_mutual [lemma, in LNgen.Fsub_inf]
lc_binding_unique [lemma, in LNgen.Fsub_inf]
lc_binding_unique_mutual [lemma, in LNgen.Fsub_inf]
lc_typ_unique [lemma, in LNgen.Fsub_inf]
lc_typ_unique_mutual [lemma, in LNgen.Fsub_inf]
lc_body_exp_case_3 [lemma, in LNgen.Fsub_inf]
lc_body_exp_case_2 [lemma, in LNgen.Fsub_inf]
lc_body_exp_let_2 [lemma, in LNgen.Fsub_inf]
lc_body_exp_tabs_2 [lemma, in LNgen.Fsub_inf]
lc_body_exp_abs_2 [lemma, in LNgen.Fsub_inf]
lc_body_typ_all_2 [lemma, in LNgen.Fsub_inf]
lc_body_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
lc_body_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
lc_body_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
lc_body_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
lc_exp_case_exists [lemma, in LNgen.Fsub_inf]
lc_exp_let_exists [lemma, in LNgen.Fsub_inf]
lc_exp_tabs_exists [lemma, in LNgen.Fsub_inf]
lc_exp_abs_exists [lemma, in LNgen.Fsub_inf]
lc_typ_all_exists [lemma, in LNgen.Fsub_inf]
lc_exp_of_degree [lemma, in LNgen.Fsub_inf]
lc_exp_of_degree_size_mutual [lemma, in LNgen.Fsub_inf]
lc_binding_of_degree [lemma, in LNgen.Fsub_inf]
lc_binding_of_degree_size_mutual [lemma, in LNgen.Fsub_inf]
lc_typ_of_degree [lemma, in LNgen.Fsub_inf]
lc_typ_of_degree_size_mutual [lemma, in LNgen.Fsub_inf]
lc_set_exp_mutrec [definition, in LNgen.Fsub_inf]
lc_set_exp_rec' [definition, in LNgen.Fsub_inf]
lc_set_exp_mutind [definition, in LNgen.Fsub_inf]
lc_set_exp_ind' [definition, in LNgen.Fsub_inf]
lc_exp_mutind [definition, in LNgen.Fsub_inf]
lc_exp_ind' [definition, in LNgen.Fsub_inf]
lc_set_exp_case [constructor, in LNgen.Fsub_inf]
lc_set_exp_inr [constructor, in LNgen.Fsub_inf]
lc_set_exp_inl [constructor, in LNgen.Fsub_inf]
lc_set_exp_let [constructor, in LNgen.Fsub_inf]
lc_set_exp_tapp [constructor, in LNgen.Fsub_inf]
lc_set_exp_tabs [constructor, in LNgen.Fsub_inf]
lc_set_exp_app [constructor, in LNgen.Fsub_inf]
lc_set_exp_abs [constructor, in LNgen.Fsub_inf]
lc_set_exp_var_f [constructor, in LNgen.Fsub_inf]
lc_set_exp [inductive, in LNgen.Fsub_inf]
lc_set_binding_mutrec [definition, in LNgen.Fsub_inf]
lc_set_binding_rec' [definition, in LNgen.Fsub_inf]
lc_set_binding_mutind [definition, in LNgen.Fsub_inf]
lc_set_binding_ind' [definition, in LNgen.Fsub_inf]
lc_binding_mutind [definition, in LNgen.Fsub_inf]
lc_binding_ind' [definition, in LNgen.Fsub_inf]
lc_set_bind_typ [constructor, in LNgen.Fsub_inf]
lc_set_bind_sub [constructor, in LNgen.Fsub_inf]
lc_set_binding [inductive, in LNgen.Fsub_inf]
lc_set_typ_mutrec [definition, in LNgen.Fsub_inf]
lc_set_typ_rec' [definition, in LNgen.Fsub_inf]
lc_set_typ_mutind [definition, in LNgen.Fsub_inf]
lc_set_typ_ind' [definition, in LNgen.Fsub_inf]
lc_typ_mutind [definition, in LNgen.Fsub_inf]
lc_typ_ind' [definition, in LNgen.Fsub_inf]
lc_set_typ_sum [constructor, in LNgen.Fsub_inf]
lc_set_typ_all [constructor, in LNgen.Fsub_inf]
lc_set_typ_arrow [constructor, in LNgen.Fsub_inf]
lc_set_typ_var_f [constructor, in LNgen.Fsub_inf]
lc_set_typ_top [constructor, in LNgen.Fsub_inf]
lc_set_typ [inductive, in LNgen.Fsub_inf]
lc_exp_case [constructor, in LNgen.Fsub_ott]
lc_exp_inr [constructor, in LNgen.Fsub_ott]
lc_exp_inl [constructor, in LNgen.Fsub_ott]
lc_exp_let [constructor, in LNgen.Fsub_ott]
lc_exp_tapp [constructor, in LNgen.Fsub_ott]
lc_exp_tabs [constructor, in LNgen.Fsub_ott]
lc_exp_app [constructor, in LNgen.Fsub_ott]
lc_exp_abs [constructor, in LNgen.Fsub_ott]
lc_exp_var_f [constructor, in LNgen.Fsub_ott]
lc_exp [inductive, in LNgen.Fsub_ott]
lc_bind_typ [constructor, in LNgen.Fsub_ott]
lc_bind_sub [constructor, in LNgen.Fsub_ott]
lc_binding [inductive, in LNgen.Fsub_ott]
lc_typ_sum [constructor, in LNgen.Fsub_ott]
lc_typ_all [constructor, in LNgen.Fsub_ott]
lc_typ_arrow [constructor, in LNgen.Fsub_ott]
lc_typ_var_f [constructor, in LNgen.Fsub_ott]
lc_typ_top [constructor, in LNgen.Fsub_ott]
lc_typ [inductive, in LNgen.Fsub_ott]
lelistA_unique [lemma, in Metalib.CoqListFacts]
lelistA_ind' [definition, in Metalib.CoqListFacts]
lelistA_dec [lemma, in Metalib.CoqListFacts]
lelistA_unique [lemma, in Metalib.CoqUniquenessTacEx]
lelistA_ind' [definition, in Metalib.CoqUniquenessTacEx]
le_unique [lemma, in Metalib.CoqUniquenessTacEx]
le_ind' [definition, in Metalib.CoqUniquenessTacEx]
LibDefaultSimp [library]
LibLNgen [library]
LibTactics [library]
list_rev [definition, in Metalib.CoqUniquenessTac]
lt_ge_dec [definition, in Metalib.LibLNgen]
M
Make [module, in Metalib.FSetExtra]Make [module, in Metalib.AssocList]
Make [module, in Metalib.MSetExtra]
MakeListOrdering [module, in Metalib.CoqMSetInterface]
MakeListOrdering.cons_CompSpec [lemma, in Metalib.CoqMSetInterface]
MakeListOrdering.eq [definition, in Metalib.CoqMSetInterface]
MakeListOrdering.eq_cons [lemma, in Metalib.CoqMSetInterface]
MakeListOrdering.eq_equiv [instance, in Metalib.CoqMSetInterface]
MakeListOrdering.In [abbreviation, in Metalib.CoqMSetInterface]
MakeListOrdering.lt [definition, in Metalib.CoqMSetInterface]
MakeListOrdering.lt_compat' [instance, in Metalib.CoqMSetInterface]
MakeListOrdering.lt_strorder [instance, in Metalib.CoqMSetInterface]
MakeListOrdering.lt_cons_eq [constructor, in Metalib.CoqMSetInterface]
MakeListOrdering.lt_cons_lt [constructor, in Metalib.CoqMSetInterface]
MakeListOrdering.lt_nil [constructor, in Metalib.CoqMSetInterface]
MakeListOrdering.lt_list [inductive, in Metalib.CoqMSetInterface]
MakeListOrdering.MO [module, in Metalib.CoqMSetInterface]
MakeListOrdering.t [abbreviation, in Metalib.CoqMSetInterface]
MakeSetOrdering [module, in Metalib.CoqMSetInterface]
MakeSetOrdering.Above [definition, in Metalib.CoqMSetInterface]
MakeSetOrdering.Add [definition, in Metalib.CoqMSetInterface]
MakeSetOrdering.Below [definition, in Metalib.CoqMSetInterface]
MakeSetOrdering.EmptyBetween [definition, in Metalib.CoqMSetInterface]
MakeSetOrdering.eq [definition, in Metalib.CoqMSetInterface]
MakeSetOrdering.EquivBefore [definition, in Metalib.CoqMSetInterface]
MakeSetOrdering.eq_equiv [instance, in Metalib.CoqMSetInterface]
MakeSetOrdering.lt [definition, in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_add_eq [lemma, in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_add_lt [lemma, in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_empty_l [lemma, in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_empty_r [lemma, in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_strorder [instance, in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_compat [instance, in Metalib.CoqMSetInterface]
MakeSetOrdering.MO [module, in Metalib.CoqMSetInterface]
Make.alist_ind [lemma, in Metalib.AssocList]
Make.app_eq_one [lemma, in Metalib.AssocList]
Make.app_nil_2 [lemma, in Metalib.AssocList]
Make.app_nil_1 [lemma, in Metalib.AssocList]
Make.app_assoc [lemma, in Metalib.AssocList]
Make.AssortedListProperties [section, in Metalib.AssocList]
Make.AssortedListProperties.x [variable, in Metalib.AssocList]
Make.AssortedListProperties.X [variable, in Metalib.AssocList]
Make.AssortedListProperties.xs [variable, in Metalib.AssocList]
Make.AssortedListProperties.ys [variable, in Metalib.AssocList]
Make.AssortedListProperties.zs [variable, in Metalib.AssocList]
Make.binds [definition, in Metalib.AssocList]
Make.BindsDerived [section, in Metalib.AssocList]
Make.BindsDerived.a [variable, in Metalib.AssocList]
Make.BindsDerived.A [variable, in Metalib.AssocList]
Make.BindsDerived.b [variable, in Metalib.AssocList]
Make.BindsDerived.B [variable, in Metalib.AssocList]
Make.BindsDerived.E [variable, in Metalib.AssocList]
Make.BindsDerived.F [variable, in Metalib.AssocList]
Make.BindsDerived.f [variable, in Metalib.AssocList]
Make.BindsDerived.G [variable, in Metalib.AssocList]
Make.BindsDerived.x [variable, in Metalib.AssocList]
Make.BindsDerived.y [variable, in Metalib.AssocList]
Make.BindsProperties [section, in Metalib.AssocList]
Make.BindsProperties.a [variable, in Metalib.AssocList]
Make.BindsProperties.A [variable, in Metalib.AssocList]
Make.BindsProperties.b [variable, in Metalib.AssocList]
Make.BindsProperties.B [variable, in Metalib.AssocList]
Make.BindsProperties.b0 [variable, in Metalib.AssocList]
Make.BindsProperties.E [variable, in Metalib.AssocList]
Make.BindsProperties.F [variable, in Metalib.AssocList]
Make.BindsProperties.f [variable, in Metalib.AssocList]
Make.BindsProperties.G [variable, in Metalib.AssocList]
Make.BindsProperties.x [variable, in Metalib.AssocList]
Make.BindsProperties.y [variable, in Metalib.AssocList]
Make.BindsProperties2 [section, in Metalib.AssocList]
Make.BindsProperties2.a [variable, in Metalib.AssocList]
Make.BindsProperties2.A [variable, in Metalib.AssocList]
Make.BindsProperties2.b [variable, in Metalib.AssocList]
Make.BindsProperties2.B [variable, in Metalib.AssocList]
Make.BindsProperties2.E [variable, in Metalib.AssocList]
Make.BindsProperties2.F [variable, in Metalib.AssocList]
Make.BindsProperties2.f [variable, in Metalib.AssocList]
Make.BindsProperties2.G [variable, in Metalib.AssocList]
Make.BindsProperties2.x [variable, in Metalib.AssocList]
Make.BindsProperties2.y [variable, in Metalib.AssocList]
Make.binds_split [lemma, in Metalib.AssocList]
Make.binds_unique [lemma, in Metalib.AssocList]
Make.binds_In_inv [lemma, in Metalib.AssocList]
Make.binds_In [lemma, in Metalib.AssocList]
Make.binds_remove_mid [lemma, in Metalib.AssocList]
Make.binds_mid_eq [lemma, in Metalib.AssocList]
Make.binds_weaken [lemma, in Metalib.AssocList]
Make.binds_lookup_dec [lemma, in Metalib.AssocList]
Make.binds_lookup [lemma, in Metalib.AssocList]
Make.binds_dec [lemma, in Metalib.AssocList]
Make.binds_cons_uniq_iff [lemma, in Metalib.AssocList]
Make.binds_cons_uniq_1 [lemma, in Metalib.AssocList]
Make.binds_app_uniq_iff [lemma, in Metalib.AssocList]
Make.binds_app_uniq_1 [lemma, in Metalib.AssocList]
Make.binds_dom_contradiction [lemma, in Metalib.AssocList]
Make.binds_map_3 [lemma, in Metalib.AssocList]
Make.binds_map_2 [lemma, in Metalib.AssocList]
Make.binds_map_1 [lemma, in Metalib.AssocList]
Make.binds_app_iff [lemma, in Metalib.AssocList]
Make.binds_app_3 [lemma, in Metalib.AssocList]
Make.binds_app_2 [lemma, in Metalib.AssocList]
Make.binds_app_1 [lemma, in Metalib.AssocList]
Make.binds_cons_iff [lemma, in Metalib.AssocList]
Make.binds_cons_3 [lemma, in Metalib.AssocList]
Make.binds_cons_2 [lemma, in Metalib.AssocList]
Make.binds_cons_1 [lemma, in Metalib.AssocList]
Make.binds_one_iff [lemma, in Metalib.AssocList]
Make.binds_one_3 [lemma, in Metalib.AssocList]
Make.binds_one_2 [lemma, in Metalib.AssocList]
Make.binds_one_1 [lemma, in Metalib.AssocList]
Make.binds_nil_iff [lemma, in Metalib.AssocList]
Make.cons_app_assoc [lemma, in Metalib.AssocList]
Make.cons_app_one [lemma, in Metalib.AssocList]
Make.D [module, in Metalib.AssocList]
Make.disjoint [definition, in Metalib.FSetExtra]
Make.Disjoint [section, in Metalib.AssocList]
Make.disjoint [definition, in Metalib.AssocList]
Make.disjoint [definition, in Metalib.MSetExtra]
Make.disjoint_map_r [lemma, in Metalib.AssocList]
Make.disjoint_map_l [lemma, in Metalib.AssocList]
Make.disjoint_map_2 [lemma, in Metalib.AssocList]
Make.disjoint_map_1 [lemma, in Metalib.AssocList]
Make.disjoint_app_r [lemma, in Metalib.AssocList]
Make.disjoint_app_l [lemma, in Metalib.AssocList]
Make.disjoint_app_3 [lemma, in Metalib.AssocList]
Make.disjoint_app_2 [lemma, in Metalib.AssocList]
Make.disjoint_app_1 [lemma, in Metalib.AssocList]
Make.disjoint_cons_r [lemma, in Metalib.AssocList]
Make.disjoint_cons_l [lemma, in Metalib.AssocList]
Make.disjoint_cons_3 [lemma, in Metalib.AssocList]
Make.disjoint_cons_2 [lemma, in Metalib.AssocList]
Make.disjoint_cons_1 [lemma, in Metalib.AssocList]
Make.disjoint_one_r [lemma, in Metalib.AssocList]
Make.disjoint_one_l [lemma, in Metalib.AssocList]
Make.disjoint_one_2 [lemma, in Metalib.AssocList]
Make.disjoint_one_1 [lemma, in Metalib.AssocList]
Make.disjoint_nil_1 [lemma, in Metalib.AssocList]
Make.disjoint_sym [lemma, in Metalib.AssocList]
Make.disjoint_sym_1 [lemma, in Metalib.AssocList]
Make.dom [definition, in Metalib.AssocList]
Make.dom_map [lemma, in Metalib.AssocList]
Make.dom_app [lemma, in Metalib.AssocList]
Make.dom_cons [lemma, in Metalib.AssocList]
Make.dom_one [lemma, in Metalib.AssocList]
Make.dom_nil [lemma, in Metalib.AssocList]
Make.EqDec_eq_of_X [instance, in Metalib.AssocList]
Make.EqDec_of_X [instance, in Metalib.AssocList]
Make.fresh_list [definition, in Metalib.FSetExtra]
Make.fresh_app_r [lemma, in Metalib.AssocList]
Make.fresh_app_l [lemma, in Metalib.AssocList]
Make.fresh_mid_head [lemma, in Metalib.AssocList]
Make.fresh_mid_tail [lemma, in Metalib.AssocList]
Make.fresh_list [definition, in Metalib.MSetExtra]
Make.get [definition, in Metalib.AssocList]
Make.in_app_iff [lemma, in Metalib.AssocList]
Make.in_one_iff [lemma, in Metalib.AssocList]
Make.in_nil_iff [lemma, in Metalib.AssocList]
Make.KeySetFacts [module, in Metalib.AssocList]
Make.KeySetProperties [module, in Metalib.AssocList]
Make.ListProperties [section, in Metalib.AssocList]
Make.ListProperties.l [variable, in Metalib.AssocList]
Make.ListProperties.l1 [variable, in Metalib.AssocList]
Make.ListProperties.l2 [variable, in Metalib.AssocList]
Make.ListProperties.l3 [variable, in Metalib.AssocList]
Make.ListProperties.x [variable, in Metalib.AssocList]
Make.ListProperties.X [variable, in Metalib.AssocList]
Make.ListProperties.y [variable, in Metalib.AssocList]
Make.map [definition, in Metalib.AssocList]
Make.maps [definition, in Metalib.AssocList]
Make.map_app [lemma, in Metalib.AssocList]
Make.map_cons [lemma, in Metalib.AssocList]
Make.map_one [lemma, in Metalib.AssocList]
Make.map_nil [lemma, in Metalib.AssocList]
Make.nil_neq_one_mid [lemma, in Metalib.AssocList]
Make.notin [definition, in Metalib.FSetExtra]
Make.notin [definition, in Metalib.MSetExtra]
Make.one [definition, in Metalib.AssocList]
Make.one_mid_neq_nil [lemma, in Metalib.AssocList]
Make.one_eq_app [lemma, in Metalib.AssocList]
Make.Properties [section, in Metalib.AssocList]
Make.Properties.A [variable, in Metalib.AssocList]
Make.Properties.b [variable, in Metalib.AssocList]
Make.Properties.B [variable, in Metalib.AssocList]
Make.Properties.E [variable, in Metalib.AssocList]
Make.Properties.F [variable, in Metalib.AssocList]
Make.Properties.f [variable, in Metalib.AssocList]
Make.Properties.G [variable, in Metalib.AssocList]
Make.Properties.key [variable, in Metalib.AssocList]
Make.Properties.x [variable, in Metalib.AssocList]
Make.uniq [inductive, in Metalib.AssocList]
Make.UniqDerived [section, in Metalib.AssocList]
Make.UniqDerived.a [variable, in Metalib.AssocList]
Make.UniqDerived.A [variable, in Metalib.AssocList]
Make.UniqDerived.b [variable, in Metalib.AssocList]
Make.UniqDerived.E [variable, in Metalib.AssocList]
Make.UniqDerived.F [variable, in Metalib.AssocList]
Make.UniqDerived.G [variable, in Metalib.AssocList]
Make.UniqDerived.x [variable, in Metalib.AssocList]
Make.UniqDerived.y [variable, in Metalib.AssocList]
Make.UniqMid [section, in Metalib.AssocList]
Make.UniqMid.a [variable, in Metalib.AssocList]
Make.UniqMid.A [variable, in Metalib.AssocList]
Make.UniqMid.B [variable, in Metalib.AssocList]
Make.UniqMid.E [variable, in Metalib.AssocList]
Make.UniqMid.F [variable, in Metalib.AssocList]
Make.UniqMid.f [variable, in Metalib.AssocList]
Make.UniqMid.x [variable, in Metalib.AssocList]
Make.UniqMid.y [variable, in Metalib.AssocList]
Make.UniqProperties [section, in Metalib.AssocList]
Make.UniqProperties.a [variable, in Metalib.AssocList]
Make.UniqProperties.A [variable, in Metalib.AssocList]
Make.UniqProperties.b [variable, in Metalib.AssocList]
Make.UniqProperties.B [variable, in Metalib.AssocList]
Make.UniqProperties.E [variable, in Metalib.AssocList]
Make.UniqProperties.F [variable, in Metalib.AssocList]
Make.UniqProperties.f [variable, in Metalib.AssocList]
Make.UniqProperties.G [variable, in Metalib.AssocList]
Make.UniqProperties.x [variable, in Metalib.AssocList]
Make.uniq_align_eq [lemma, in Metalib.AssocList]
Make.uniq_mid [lemma, in Metalib.AssocList]
Make.uniq_map_app_l [lemma, in Metalib.AssocList]
Make.uniq_reorder_2 [lemma, in Metalib.AssocList]
Make.uniq_reorder_1 [lemma, in Metalib.AssocList]
Make.uniq_remove_mid [lemma, in Metalib.AssocList]
Make.uniq_insert_mid [lemma, in Metalib.AssocList]
Make.uniq_map_iff [lemma, in Metalib.AssocList]
Make.uniq_map_2 [lemma, in Metalib.AssocList]
Make.uniq_map_1 [lemma, in Metalib.AssocList]
Make.uniq_app_iff [lemma, in Metalib.AssocList]
Make.uniq_app_4 [lemma, in Metalib.AssocList]
Make.uniq_app_3 [lemma, in Metalib.AssocList]
Make.uniq_app_2 [lemma, in Metalib.AssocList]
Make.uniq_app_1 [lemma, in Metalib.AssocList]
Make.uniq_cons_iff [lemma, in Metalib.AssocList]
Make.uniq_cons_3 [lemma, in Metalib.AssocList]
Make.uniq_cons_2 [lemma, in Metalib.AssocList]
Make.uniq_cons_1 [lemma, in Metalib.AssocList]
Make.uniq_one_1 [lemma, in Metalib.AssocList]
Make.uniq_push [constructor, in Metalib.AssocList]
Make.uniq_nil [constructor, in Metalib.AssocList]
_ ~ _ (list_scope) [notation, in Metalib.AssocList]
map_subst_typ_in_binding_id [lemma, in LNgen.Fsub_proofs]
map_subst_tb_id [lemma, in LN.Fsub_Lemmas]
Metatheory [library]
MetatheoryAtom [library]
MSetExtra [library]
MSetWeakNotin [library]
N
nil_eq_app [lemma, in Metalib.CoqListFacts]Notin_fun.test_solve_notin_7 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_6 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_5 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_4 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_3 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_2 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_diff_3 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_diff_2 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_diff_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_inter_3 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_inter_2 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_inter_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_union_3 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_union_2 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_union_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_3' [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_3 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_2 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_singleton_2 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_singleton_1' [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_singleton_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_add_3 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_add_2 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_add_1' [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_add_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.notin_empty_1 [lemma, in Metalib.FSetWeakNotin]
Notin_fun.Lemmas.s' [variable, in Metalib.FSetWeakNotin]
Notin_fun.Lemmas.s [variable, in Metalib.FSetWeakNotin]
Notin_fun.Lemmas.y [variable, in Metalib.FSetWeakNotin]
Notin_fun.Lemmas.x [variable, in Metalib.FSetWeakNotin]
Notin_fun.Lemmas [section, in Metalib.FSetWeakNotin]
Notin_fun.D [module, in Metalib.FSetWeakNotin]
Notin_fun [module, in Metalib.FSetWeakNotin]
notin_union [abbreviation, in Metalib.Metatheory]
notin_singleton [abbreviation, in Metalib.Metatheory]
notin_add [abbreviation, in Metalib.Metatheory]
notin_empty [abbreviation, in Metalib.Metatheory]
Notin_fun.test_solve_notin_7 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_6 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_5 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_4 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_3 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_2 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_diff_3 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_diff_2 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_diff_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_inter_3 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_inter_2 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_inter_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_union_3 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_union_2 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_union_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_3' [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_3 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_2 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_singleton_2 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_singleton_1' [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_singleton_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_add_3 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_add_2 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_add_1' [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_add_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.notin_empty_1 [lemma, in Metalib.MSetWeakNotin]
Notin_fun.Lemmas.s' [variable, in Metalib.MSetWeakNotin]
Notin_fun.Lemmas.s [variable, in Metalib.MSetWeakNotin]
Notin_fun.Lemmas.y [variable, in Metalib.MSetWeakNotin]
Notin_fun.Lemmas.x [variable, in Metalib.MSetWeakNotin]
Notin_fun.Lemmas [section, in Metalib.MSetWeakNotin]
Notin_fun.D [module, in Metalib.MSetWeakNotin]
Notin_fun [module, in Metalib.MSetWeakNotin]
notin_fv_wf [lemma, in LNgen.Fsub_proofs]
notin_fv_typ_in_typ_open [lemma, in LNgen.Fsub_proofs]
notin_fv_wf [lemma, in LN.Fsub_Lemmas]
notin_fv_tt_open [lemma, in LN.Fsub_Lemmas]
not_In_app [lemma, in Metalib.CoqListFacts]
not_In_cons [lemma, in Metalib.CoqListFacts]
O
open_exp_wrt_exp_lc_exp [lemma, in LNgen.Fsub_inf]open_exp_wrt_typ_lc_exp [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_lc_binding [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_lc_typ [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_degree_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_degree_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_degree_exp_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_degree_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_degree_binding_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_degree_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_degree_typ_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_inj [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_inj [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_inj [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_inj [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_inj [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_inj [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_inj [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_inj [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_inj_mutual [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_close_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_close_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_close_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_close_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_close_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_close_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
open_ee_body_e [lemma, in LN.Fsub_Infrastructure]
open_ee_rec_expr [lemma, in LN.Fsub_Infrastructure]
open_ee_rec_type_aux [lemma, in LN.Fsub_Infrastructure]
open_ee_rec_expr_aux [lemma, in LN.Fsub_Infrastructure]
open_te_rec_expr [lemma, in LN.Fsub_Infrastructure]
open_te_rec_type_aux [lemma, in LN.Fsub_Infrastructure]
open_te_rec_expr_aux [lemma, in LN.Fsub_Infrastructure]
open_tt_rec_type [lemma, in LN.Fsub_Infrastructure]
open_tt_rec_type_aux [lemma, in LN.Fsub_Infrastructure]
open_typ_wrt_typ [definition, in LNgen.Fsub_ott]
open_exp_wrt_typ [definition, in LNgen.Fsub_ott]
open_exp_wrt_exp [definition, in LNgen.Fsub_ott]
open_binding_wrt_typ [definition, in LNgen.Fsub_ott]
open_exp_wrt_typ_rec [definition, in LNgen.Fsub_ott]
open_exp_wrt_exp_rec [definition, in LNgen.Fsub_ott]
open_binding_wrt_typ_rec [definition, in LNgen.Fsub_ott]
open_typ_wrt_typ_rec [definition, in LNgen.Fsub_ott]
open_ee [definition, in LN.Fsub_Definitions]
open_te [definition, in LN.Fsub_Definitions]
open_tt [definition, in LN.Fsub_Definitions]
open_ee_rec [definition, in LN.Fsub_Definitions]
open_te_rec [definition, in LN.Fsub_Definitions]
open_tt_rec [definition, in LN.Fsub_Definitions]
Ops [module, in Metalib.CoqMSetInterface]
P
preservation [lemma, in LN.Fsub_Soundness]preservation [lemma, in LNgen.Fsub_proofs]
progress [lemma, in LN.Fsub_Soundness]
progress [lemma, in LNgen.Fsub_proofs]
R
RawSets [module, in Metalib.CoqMSetInterface]RawSets.choose_spec3 [axiom, in Metalib.CoqMSetInterface]
RawSets.compare_spec [axiom, in Metalib.CoqMSetInterface]
RawSets.elements_spec2 [axiom, in Metalib.CoqMSetInterface]
RawSets.max_elt_spec3 [axiom, in Metalib.CoqMSetInterface]
RawSets.max_elt_spec2 [axiom, in Metalib.CoqMSetInterface]
RawSets.max_elt_spec1 [axiom, in Metalib.CoqMSetInterface]
RawSets.min_elt_spec3 [axiom, in Metalib.CoqMSetInterface]
RawSets.min_elt_spec2 [axiom, in Metalib.CoqMSetInterface]
RawSets.min_elt_spec1 [axiom, in Metalib.CoqMSetInterface]
RawSets.Spec [section, in Metalib.CoqMSetInterface]
RawSets.Spec.s [variable, in Metalib.CoqMSetInterface]
RawSets.Spec.s' [variable, in Metalib.CoqMSetInterface]
RawSets.Spec.x [variable, in Metalib.CoqMSetInterface]
RawSets.Spec.y [variable, in Metalib.CoqMSetInterface]
Raw2Sets [module, in Metalib.CoqMSetInterface]
Raw2SetsOn [module, in Metalib.CoqMSetInterface]
Raw2SetsOn.choose_spec3 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.compare [definition, in Metalib.CoqMSetInterface]
Raw2SetsOn.compare_spec [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.elements_spec2 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.lt [definition, in Metalib.CoqMSetInterface]
Raw2SetsOn.lt_compat [instance, in Metalib.CoqMSetInterface]
Raw2SetsOn.lt_strorder [instance, in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt_spec3 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt_spec2 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt_spec1 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt [definition, in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt_spec3 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt_spec2 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt_spec1 [lemma, in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt [definition, in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec [section, in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.s [variable, in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.s' [variable, in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.s'' [variable, in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.x [variable, in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.y [variable, in Metalib.CoqMSetInterface]
Raw2Sets.E [module, in Metalib.CoqMSetInterface]
red [inductive, in LNgen.Fsub_ott]
red [inductive, in LN.Fsub_Definitions]
red_case_inr [constructor, in LNgen.Fsub_ott]
red_case_inl [constructor, in LNgen.Fsub_ott]
red_case_1 [constructor, in LNgen.Fsub_ott]
red_inr_1 [constructor, in LNgen.Fsub_ott]
red_inl_1 [constructor, in LNgen.Fsub_ott]
red_let [constructor, in LNgen.Fsub_ott]
red_let_1 [constructor, in LNgen.Fsub_ott]
red_tabs [constructor, in LNgen.Fsub_ott]
red_abs [constructor, in LNgen.Fsub_ott]
red_tapp_1 [constructor, in LNgen.Fsub_ott]
red_app_2 [constructor, in LNgen.Fsub_ott]
red_app_1 [constructor, in LNgen.Fsub_ott]
red_regular [lemma, in LNgen.Fsub_proofs]
red_case_inr [constructor, in LN.Fsub_Definitions]
red_case_inl [constructor, in LN.Fsub_Definitions]
red_case_1 [constructor, in LN.Fsub_Definitions]
red_inr_1 [constructor, in LN.Fsub_Definitions]
red_inl_1 [constructor, in LN.Fsub_Definitions]
red_let [constructor, in LN.Fsub_Definitions]
red_let_1 [constructor, in LN.Fsub_Definitions]
red_tabs [constructor, in LN.Fsub_Definitions]
red_abs [constructor, in LN.Fsub_Definitions]
red_tapp [constructor, in LN.Fsub_Definitions]
red_app_2 [constructor, in LN.Fsub_Definitions]
red_app_1 [constructor, in LN.Fsub_Definitions]
red_regular [lemma, in LN.Fsub_Lemmas]
remove [abbreviation, in Metalib.Metatheory]
remove_union_distrib [lemma, in Metalib.LibLNgen]
S
S [module, in Metalib.CoqMSetInterface]S [module, in Metalib.CoqFSetInterface]
Sdep [module, in Metalib.CoqFSetInterface]
Sdep.add [axiom, in Metalib.CoqFSetInterface]
Sdep.Add [definition, in Metalib.CoqFSetInterface]
Sdep.cardinal [axiom, in Metalib.CoqFSetInterface]
Sdep.choose [axiom, in Metalib.CoqFSetInterface]
Sdep.choose_equal [axiom, in Metalib.CoqFSetInterface]
Sdep.compare [axiom, in Metalib.CoqFSetInterface]
Sdep.diff [axiom, in Metalib.CoqFSetInterface]
Sdep.E [module, in Metalib.CoqFSetInterface]
Sdep.elements [axiom, in Metalib.CoqFSetInterface]
Sdep.elt [definition, in Metalib.CoqFSetInterface]
Sdep.empty [axiom, in Metalib.CoqFSetInterface]
Sdep.Empty [definition, in Metalib.CoqFSetInterface]
Sdep.eq [definition, in Metalib.CoqFSetInterface]
Sdep.equal [axiom, in Metalib.CoqFSetInterface]
Sdep.Equal [definition, in Metalib.CoqFSetInterface]
Sdep.eq_In [axiom, in Metalib.CoqFSetInterface]
Sdep.eq_trans [axiom, in Metalib.CoqFSetInterface]
Sdep.eq_sym [axiom, in Metalib.CoqFSetInterface]
Sdep.eq_refl [axiom, in Metalib.CoqFSetInterface]
Sdep.Exists [definition, in Metalib.CoqFSetInterface]
Sdep.exists_ [axiom, in Metalib.CoqFSetInterface]
Sdep.filter [axiom, in Metalib.CoqFSetInterface]
Sdep.fold [axiom, in Metalib.CoqFSetInterface]
Sdep.for_all [axiom, in Metalib.CoqFSetInterface]
Sdep.For_all [definition, in Metalib.CoqFSetInterface]
Sdep.In [axiom, in Metalib.CoqFSetInterface]
Sdep.inter [axiom, in Metalib.CoqFSetInterface]
Sdep.is_empty [axiom, in Metalib.CoqFSetInterface]
Sdep.lt [axiom, in Metalib.CoqFSetInterface]
Sdep.lt_not_eq [axiom, in Metalib.CoqFSetInterface]
Sdep.lt_trans [axiom, in Metalib.CoqFSetInterface]
Sdep.max_elt [axiom, in Metalib.CoqFSetInterface]
Sdep.mem [axiom, in Metalib.CoqFSetInterface]
Sdep.min_elt [axiom, in Metalib.CoqFSetInterface]
Sdep.partition [axiom, in Metalib.CoqFSetInterface]
Sdep.remove [axiom, in Metalib.CoqFSetInterface]
Sdep.singleton [axiom, in Metalib.CoqFSetInterface]
Sdep.subset [axiom, in Metalib.CoqFSetInterface]
Sdep.Subset [definition, in Metalib.CoqFSetInterface]
Sdep.t [axiom, in Metalib.CoqFSetInterface]
Sdep.union [axiom, in Metalib.CoqFSetInterface]
_ [=] _ [notation, in Metalib.CoqFSetInterface]
Sets [module, in Metalib.CoqMSetInterface]
SetsOn [module, in Metalib.CoqMSetInterface]
SetsOn.choose_spec3 [axiom, in Metalib.CoqMSetInterface]
SetsOn.compare_spec [axiom, in Metalib.CoqMSetInterface]
SetsOn.elements_spec2 [axiom, in Metalib.CoqMSetInterface]
SetsOn.max_elt_spec3 [axiom, in Metalib.CoqMSetInterface]
SetsOn.max_elt_spec2 [axiom, in Metalib.CoqMSetInterface]
SetsOn.max_elt_spec1 [axiom, in Metalib.CoqMSetInterface]
SetsOn.min_elt_spec3 [axiom, in Metalib.CoqMSetInterface]
SetsOn.min_elt_spec2 [axiom, in Metalib.CoqMSetInterface]
SetsOn.min_elt_spec1 [axiom, in Metalib.CoqMSetInterface]
SetsOn.Spec [section, in Metalib.CoqMSetInterface]
SetsOn.Spec.s [variable, in Metalib.CoqMSetInterface]
SetsOn.Spec.s' [variable, in Metalib.CoqMSetInterface]
SetsOn.Spec.x [variable, in Metalib.CoqMSetInterface]
SetsOn.Spec.y [variable, in Metalib.CoqMSetInterface]
Sets.E [module, in Metalib.CoqMSetInterface]
Sfun [module, in Metalib.CoqFSetInterface]
Sfun.choose_3 [axiom, in Metalib.CoqFSetInterface]
Sfun.compare [axiom, in Metalib.CoqFSetInterface]
Sfun.elements_3 [axiom, in Metalib.CoqFSetInterface]
Sfun.lt [axiom, in Metalib.CoqFSetInterface]
Sfun.lt_not_eq [axiom, in Metalib.CoqFSetInterface]
Sfun.lt_trans [axiom, in Metalib.CoqFSetInterface]
Sfun.max_elt_3 [axiom, in Metalib.CoqFSetInterface]
Sfun.max_elt_2 [axiom, in Metalib.CoqFSetInterface]
Sfun.max_elt_1 [axiom, in Metalib.CoqFSetInterface]
Sfun.max_elt [axiom, in Metalib.CoqFSetInterface]
Sfun.min_elt_3 [axiom, in Metalib.CoqFSetInterface]
Sfun.min_elt_2 [axiom, in Metalib.CoqFSetInterface]
Sfun.min_elt_1 [axiom, in Metalib.CoqFSetInterface]
Sfun.min_elt [axiom, in Metalib.CoqFSetInterface]
Sfun.Spec [section, in Metalib.CoqFSetInterface]
Sfun.Spec.s [variable, in Metalib.CoqFSetInterface]
Sfun.Spec.s' [variable, in Metalib.CoqFSetInterface]
Sfun.Spec.s'' [variable, in Metalib.CoqFSetInterface]
Sfun.Spec.x [variable, in Metalib.CoqFSetInterface]
Sfun.Spec.y [variable, in Metalib.CoqFSetInterface]
singleton [abbreviation, in Metalib.Metatheory]
size_exp_open_exp_wrt_exp_var [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_var [lemma, in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_var [lemma, in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_var [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec_var [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec_var_mutual [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec_var [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec_var_mutual [lemma, in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec_var [lemma, in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec_var_mutual [lemma, in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec_var [lemma, in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec_var_mutual [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
size_exp_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
size_exp_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
size_binding_close_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
size_typ_close_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
size_exp_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
size_exp_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
size_exp_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
size_exp_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
size_binding_close_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
size_binding_close_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
size_typ_close_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
size_typ_close_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
size_exp_min [lemma, in LNgen.Fsub_inf]
size_exp_min_mutual [lemma, in LNgen.Fsub_inf]
size_binding_min [lemma, in LNgen.Fsub_inf]
size_binding_min_mutual [lemma, in LNgen.Fsub_inf]
size_typ_min [lemma, in LNgen.Fsub_inf]
size_typ_min_mutual [lemma, in LNgen.Fsub_inf]
size_exp [definition, in LNgen.Fsub_inf]
size_binding [definition, in LNgen.Fsub_inf]
size_typ [definition, in LNgen.Fsub_inf]
Sort [abbreviation, in Metalib.CoqListFacts]
SortedListEquality [section, in Metalib.CoqListFacts]
SortedListEquality.A [variable, in Metalib.CoqListFacts]
SortedListEquality.eqA_ltA [variable, in Metalib.CoqListFacts]
SortedListEquality.ltA [variable, in Metalib.CoqListFacts]
SortedListEquality.ltA_eqA [variable, in Metalib.CoqListFacts]
SortedListEquality.ltA_not_eqA [variable, in Metalib.CoqListFacts]
SortedListEquality.ltA_trans [variable, in Metalib.CoqListFacts]
sort_unique [lemma, in Metalib.CoqListFacts]
sort_ind' [definition, in Metalib.CoqListFacts]
Sort_In_eq [lemma, in Metalib.CoqListFacts]
Sort_InA_eq [lemma, in Metalib.CoqListFacts]
sort_dec [lemma, in Metalib.CoqListFacts]
sort_unique [lemma, in Metalib.CoqUniquenessTacEx]
sort_ind' [definition, in Metalib.CoqUniquenessTacEx]
sub [inductive, in LNgen.Fsub_ott]
sub [inductive, in LN.Fsub_Definitions]
Subset_union_lngen_open_upper [lemma, in Metalib.LibLNgen]
Subset_union_right [lemma, in Metalib.LibLNgen]
Subset_union_left [lemma, in Metalib.LibLNgen]
Subset_union_compat [lemma, in Metalib.LibLNgen]
Subset_empty_any [lemma, in Metalib.LibLNgen]
Subset_refl [lemma, in Metalib.LibLNgen]
subst_exp_in_exp_intro [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_intro [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_intro [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_intro [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_intro_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_intro_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_intro_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_intro_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_intro_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_intro_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_intro_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_intro_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_exp_case [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_exp_let [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_exp_tabs [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_exp_abs [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_exp_case [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_exp_let [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_exp_tabs [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_exp_abs [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_typ_all [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_open_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_open_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec_open_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec_open_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec_open_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec_open_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_subst_exp_in_exp [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_subst_exp_in_exp_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_subst_typ_in_exp [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_subst_typ_in_exp_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_subst_exp_in_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_subst_exp_in_exp_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_subst_typ_in_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_subst_typ_in_exp_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_subst_typ_in_binding [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_subst_typ_in_binding_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_subst_typ_in_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_subst_typ_in_typ_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_spec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_spec [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_spec [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_spec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_spec_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_spec_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_spec_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_spec_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_spec_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_spec_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_spec_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_spec_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp_var [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ_var [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp_var [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ_var [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ_var [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ_var [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_lc_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_lc_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_lc_binding [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_lc_typ [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_fresh [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_fresh [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_fresh [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_fresh [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_same [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_same_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_same [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_same_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_same [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_same_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_same [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_same_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_eq [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_eq_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_eq [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_eq_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_eq [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_eq_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_eq [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_eq_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_exp_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_exp_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_degree_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_degree_binding_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_degree_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_degree_typ_wrt_typ_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec [lemma, in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec_mutual [lemma, in LNgen.Fsub_inf]
subst_ee_expr [lemma, in LN.Fsub_Infrastructure]
subst_te_expr [lemma, in LN.Fsub_Infrastructure]
subst_tt_type [lemma, in LN.Fsub_Infrastructure]
subst_ee_intro [lemma, in LN.Fsub_Infrastructure]
subst_ee_intro_rec [lemma, in LN.Fsub_Infrastructure]
subst_ee_open_te_var [lemma, in LN.Fsub_Infrastructure]
subst_ee_open_te [lemma, in LN.Fsub_Infrastructure]
subst_ee_open_te_rec [lemma, in LN.Fsub_Infrastructure]
subst_te_open_ee_var [lemma, in LN.Fsub_Infrastructure]
subst_te_open_ee [lemma, in LN.Fsub_Infrastructure]
subst_te_open_ee_rec [lemma, in LN.Fsub_Infrastructure]
subst_ee_open_ee_var [lemma, in LN.Fsub_Infrastructure]
subst_ee_open_ee [lemma, in LN.Fsub_Infrastructure]
subst_ee_open_ee_rec [lemma, in LN.Fsub_Infrastructure]
subst_ee_fresh [lemma, in LN.Fsub_Infrastructure]
subst_te_intro [lemma, in LN.Fsub_Infrastructure]
subst_te_intro_rec [lemma, in LN.Fsub_Infrastructure]
subst_te_open_te_var [lemma, in LN.Fsub_Infrastructure]
subst_te_open_te [lemma, in LN.Fsub_Infrastructure]
subst_te_open_te_rec [lemma, in LN.Fsub_Infrastructure]
subst_te_fresh [lemma, in LN.Fsub_Infrastructure]
subst_tt_intro [lemma, in LN.Fsub_Infrastructure]
subst_tt_intro_rec [lemma, in LN.Fsub_Infrastructure]
subst_tt_open_tt_var [lemma, in LN.Fsub_Infrastructure]
subst_tt_open_tt [lemma, in LN.Fsub_Infrastructure]
subst_tt_open_tt_rec [lemma, in LN.Fsub_Infrastructure]
subst_tt_fresh [lemma, in LN.Fsub_Infrastructure]
subst_tb [definition, in LN.Fsub_Infrastructure]
subst_ee [definition, in LN.Fsub_Infrastructure]
subst_te [definition, in LN.Fsub_Infrastructure]
subst_tt [definition, in LN.Fsub_Infrastructure]
subst_typ_in_exp [definition, in LNgen.Fsub_ott]
subst_exp_in_exp [definition, in LNgen.Fsub_ott]
subst_typ_in_binding [definition, in LNgen.Fsub_ott]
subst_typ_in_typ [definition, in LNgen.Fsub_ott]
sub_strengthening [lemma, in LN.Fsub_Soundness]
sub_through_subst_tt [lemma, in LN.Fsub_Soundness]
sub_narrowing [lemma, in LN.Fsub_Soundness]
sub_transitivity [lemma, in LN.Fsub_Soundness]
sub_narrowing_aux [lemma, in LN.Fsub_Soundness]
sub_weakening [lemma, in LN.Fsub_Soundness]
sub_reflexivity [lemma, in LN.Fsub_Soundness]
sub_sum [constructor, in LNgen.Fsub_ott]
sub_all [constructor, in LNgen.Fsub_ott]
sub_arrow [constructor, in LNgen.Fsub_ott]
sub_trans_tvar [constructor, in LNgen.Fsub_ott]
sub_refl_tvar [constructor, in LNgen.Fsub_ott]
sub_top [constructor, in LNgen.Fsub_ott]
sub_strengthening [lemma, in LNgen.Fsub_proofs]
sub_through_subst_typ_in_typ [lemma, in LNgen.Fsub_proofs]
sub_narrowing [lemma, in LNgen.Fsub_proofs]
sub_transitivity [lemma, in LNgen.Fsub_proofs]
sub_narrowing_aux [lemma, in LNgen.Fsub_proofs]
sub_weakening [lemma, in LNgen.Fsub_proofs]
sub_reflexivity [lemma, in LNgen.Fsub_proofs]
sub_regular [lemma, in LNgen.Fsub_proofs]
sub_sum [constructor, in LN.Fsub_Definitions]
sub_all [constructor, in LN.Fsub_Definitions]
sub_arrow [constructor, in LN.Fsub_Definitions]
sub_trans_tvar [constructor, in LN.Fsub_Definitions]
sub_refl_tvar [constructor, in LN.Fsub_Definitions]
sub_top [constructor, in LN.Fsub_Definitions]
sub_regular [lemma, in LN.Fsub_Lemmas]
S.E [module, in Metalib.CoqFSetInterface]
T
transitivity_on [definition, in LN.Fsub_Soundness]transitivity_on [definition, in LNgen.Fsub_proofs]
tr_tuple_rev [definition, in Metalib.CoqUniquenessTac]
tr_list_rev [definition, in Metalib.CoqUniquenessTac]
tuple [definition, in Metalib.CoqUniquenessTac]
tuple_rev [definition, in Metalib.CoqUniquenessTac]
typ [inductive, in LNgen.Fsub_ott]
typ [inductive, in LN.Fsub_Definitions]
type [inductive, in LN.Fsub_Definitions]
TypElt [module, in Metalib.CoqMSetInterface]
TypElt.elt [axiom, in Metalib.CoqMSetInterface]
TypElt.t [axiom, in Metalib.CoqMSetInterface]
type_from_wf_typ [lemma, in LNgen.Fsub_proofs]
type_sum [constructor, in LN.Fsub_Definitions]
type_all [constructor, in LN.Fsub_Definitions]
type_arrow [constructor, in LN.Fsub_Definitions]
type_var [constructor, in LN.Fsub_Definitions]
type_top [constructor, in LN.Fsub_Definitions]
type_from_wf_typ [lemma, in LN.Fsub_Lemmas]
typing [inductive, in LNgen.Fsub_ott]
typing [inductive, in LN.Fsub_Definitions]
typing_inv_inr [lemma, in LN.Fsub_Soundness]
typing_inv_inl [lemma, in LN.Fsub_Soundness]
typing_inv_tabs [lemma, in LN.Fsub_Soundness]
typing_inv_abs [lemma, in LN.Fsub_Soundness]
typing_through_subst_te [lemma, in LN.Fsub_Soundness]
typing_through_subst_ee [lemma, in LN.Fsub_Soundness]
typing_narrowing [lemma, in LN.Fsub_Soundness]
typing_weakening [lemma, in LN.Fsub_Soundness]
typing_case [constructor, in LNgen.Fsub_ott]
typing_inr [constructor, in LNgen.Fsub_ott]
typing_inl [constructor, in LNgen.Fsub_ott]
typing_let [constructor, in LNgen.Fsub_ott]
typing_sub [constructor, in LNgen.Fsub_ott]
typing_tapp [constructor, in LNgen.Fsub_ott]
typing_tabs [constructor, in LNgen.Fsub_ott]
typing_app [constructor, in LNgen.Fsub_ott]
typing_abs [constructor, in LNgen.Fsub_ott]
typing_var [constructor, in LNgen.Fsub_ott]
typing_inv_inr [lemma, in LNgen.Fsub_proofs]
typing_inv_inl [lemma, in LNgen.Fsub_proofs]
typing_inv_tabs [lemma, in LNgen.Fsub_proofs]
typing_inv_abs [lemma, in LNgen.Fsub_proofs]
typing_through_subst_typ_in_exp [lemma, in LNgen.Fsub_proofs]
typing_through_subst_exp_in_exp [lemma, in LNgen.Fsub_proofs]
typing_narrowing [lemma, in LNgen.Fsub_proofs]
typing_weakening [lemma, in LNgen.Fsub_proofs]
typing_regular [lemma, in LNgen.Fsub_proofs]
typing_case [constructor, in LN.Fsub_Definitions]
typing_inr [constructor, in LN.Fsub_Definitions]
typing_inl [constructor, in LN.Fsub_Definitions]
typing_let [constructor, in LN.Fsub_Definitions]
typing_sub [constructor, in LN.Fsub_Definitions]
typing_tapp [constructor, in LN.Fsub_Definitions]
typing_tabs [constructor, in LN.Fsub_Definitions]
typing_app [constructor, in LN.Fsub_Definitions]
typing_abs [constructor, in LN.Fsub_Definitions]
typing_var [constructor, in LN.Fsub_Definitions]
typing_regular [lemma, in LN.Fsub_Lemmas]
typvar [definition, in LNgen.Fsub_ott]
typ_mutrec [definition, in LNgen.Fsub_inf]
typ_rec' [definition, in LNgen.Fsub_inf]
typ_mutind [definition, in LNgen.Fsub_inf]
typ_ind' [definition, in LNgen.Fsub_inf]
typ_sum [constructor, in LNgen.Fsub_ott]
typ_all [constructor, in LNgen.Fsub_ott]
typ_arrow [constructor, in LNgen.Fsub_ott]
typ_var_f [constructor, in LNgen.Fsub_ott]
typ_var_b [constructor, in LNgen.Fsub_ott]
typ_top [constructor, in LNgen.Fsub_ott]
typ_sum [constructor, in LN.Fsub_Definitions]
typ_all [constructor, in LN.Fsub_Definitions]
typ_arrow [constructor, in LN.Fsub_Definitions]
typ_fvar [constructor, in LN.Fsub_Definitions]
typ_bvar [constructor, in LN.Fsub_Definitions]
typ_top [constructor, in LN.Fsub_Definitions]
U
union [abbreviation, in Metalib.Metatheory]union_map [definition, in Metalib.Metatheory]
Uniqueness_Of_SetoidList_Proofs.list_eq_dec [variable, in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R_unique [variable, in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R [variable, in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.A [variable, in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs [section, in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.list_eq_dec [variable, in Metalib.CoqUniquenessTacEx]
Uniqueness_Of_SetoidList_Proofs.R_unique [variable, in Metalib.CoqUniquenessTacEx]
Uniqueness_Of_SetoidList_Proofs.R [variable, in Metalib.CoqUniquenessTacEx]
Uniqueness_Of_SetoidList_Proofs.A [variable, in Metalib.CoqUniquenessTacEx]
Uniqueness_Of_SetoidList_Proofs [section, in Metalib.CoqUniquenessTacEx]
uniq_map [abbreviation, in Metalib.Metatheory]
uniq_app [abbreviation, in Metalib.Metatheory]
uniq_cons [abbreviation, in Metalib.Metatheory]
uniq_one [abbreviation, in Metalib.Metatheory]
uniq_from_wf_env [lemma, in LNgen.Fsub_proofs]
uniq_from_wf_env [lemma, in LN.Fsub_Lemmas]
V
value [inductive, in LN.Fsub_Definitions]value_inr [constructor, in LN.Fsub_Definitions]
value_inl [constructor, in LN.Fsub_Definitions]
value_tabs [constructor, in LN.Fsub_Definitions]
value_abs [constructor, in LN.Fsub_Definitions]
value_regular [lemma, in LN.Fsub_Lemmas]
var [abbreviation, in Metalib.Metatheory]
vars [abbreviation, in Metalib.Metatheory]
vcons [constructor, in Metalib.CoqUniquenessTacEx]
vector [inductive, in Metalib.CoqUniquenessTacEx]
vector_O_eq [lemma, in Metalib.CoqUniquenessTacEx]
vnil [constructor, in Metalib.CoqUniquenessTacEx]
W
WDecide [module, in Metalib.CoqFSetDecide]WDecide [module, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_sweirich [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_4 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases [module, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [inductive, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [constructor, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [inductive, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary [module, in Metalib.CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [lemma, in Metalib.CoqFSetDecide]
WDecide_fun.FSetLogicalFacts [module, in Metalib.CoqFSetDecide]
WDecide_fun.F [module, in Metalib.CoqFSetDecide]
WDecide_fun [module, in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_sweirich [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_4 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases [module, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [inductive, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [constructor, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [inductive, in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary [module, in Metalib.CoqMSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [lemma, in Metalib.CoqMSetDecide]
WDecide_fun.FSetLogicalFacts [module, in Metalib.CoqMSetDecide]
WDecide_fun.F [module, in Metalib.CoqMSetDecide]
WDecide_fun [module, in Metalib.CoqMSetDecide]
wf_env_typ [constructor, in LNgen.Fsub_ott]
wf_env_sub [constructor, in LNgen.Fsub_ott]
wf_env_empty [constructor, in LNgen.Fsub_ott]
wf_env [inductive, in LNgen.Fsub_ott]
wf_typ_sum [constructor, in LNgen.Fsub_ott]
wf_typ_all [constructor, in LNgen.Fsub_ott]
wf_typ_arrow [constructor, in LNgen.Fsub_ott]
wf_typ_var [constructor, in LNgen.Fsub_ott]
wf_typ_top [constructor, in LNgen.Fsub_ott]
wf_typ [inductive, in LNgen.Fsub_ott]
wf_env_subst_typ_in_binding [lemma, in LNgen.Fsub_proofs]
wf_env_strengthening [lemma, in LNgen.Fsub_proofs]
wf_env_narrowing [lemma, in LNgen.Fsub_proofs]
wf_typ_from_wf_env_sub [lemma, in LNgen.Fsub_proofs]
wf_typ_from_wf_env_typ [lemma, in LNgen.Fsub_proofs]
wf_typ_from_binds_typ [lemma, in LNgen.Fsub_proofs]
wf_typ_open [lemma, in LNgen.Fsub_proofs]
wf_typ_subst_typ_in_binding [lemma, in LNgen.Fsub_proofs]
wf_typ_strengthening [lemma, in LNgen.Fsub_proofs]
wf_typ_narrowing [lemma, in LNgen.Fsub_proofs]
wf_typ_weaken_head [lemma, in LNgen.Fsub_proofs]
wf_typ_weakening [lemma, in LNgen.Fsub_proofs]
wf_env_typ [constructor, in LN.Fsub_Definitions]
wf_env_sub [constructor, in LN.Fsub_Definitions]
wf_env_empty [constructor, in LN.Fsub_Definitions]
wf_env [inductive, in LN.Fsub_Definitions]
wf_typ_sum [constructor, in LN.Fsub_Definitions]
wf_typ_all [constructor, in LN.Fsub_Definitions]
wf_typ_arrow [constructor, in LN.Fsub_Definitions]
wf_typ_var [constructor, in LN.Fsub_Definitions]
wf_typ_top [constructor, in LN.Fsub_Definitions]
wf_typ [inductive, in LN.Fsub_Definitions]
wf_env_subst_tb [lemma, in LN.Fsub_Lemmas]
wf_env_strengthening [lemma, in LN.Fsub_Lemmas]
wf_env_narrowing [lemma, in LN.Fsub_Lemmas]
wf_typ_from_wf_env_sub [lemma, in LN.Fsub_Lemmas]
wf_typ_from_wf_env_typ [lemma, in LN.Fsub_Lemmas]
wf_typ_from_binds_typ [lemma, in LN.Fsub_Lemmas]
wf_typ_open [lemma, in LN.Fsub_Lemmas]
wf_typ_subst_tb [lemma, in LN.Fsub_Lemmas]
wf_typ_strengthening [lemma, in LN.Fsub_Lemmas]
wf_typ_narrowing [lemma, in LN.Fsub_Lemmas]
wf_typ_weaken_head [lemma, in LN.Fsub_Lemmas]
wf_typ_weakening [lemma, in LN.Fsub_Lemmas]
WOps [module, in Metalib.CoqMSetInterface]
WOps.elt [definition, in Metalib.CoqMSetInterface]
WOps.t [axiom, in Metalib.CoqMSetInterface]
WRawSets [module, in Metalib.CoqMSetInterface]
WRawSets.add_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.add_ok [instance, in Metalib.CoqMSetInterface]
WRawSets.cardinal_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.choose_spec2 [axiom, in Metalib.CoqMSetInterface]
WRawSets.choose_spec1 [axiom, in Metalib.CoqMSetInterface]
WRawSets.compatb [abbreviation, in Metalib.CoqMSetInterface]
WRawSets.diff_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.diff_ok [instance, in Metalib.CoqMSetInterface]
WRawSets.elements_spec2w [axiom, in Metalib.CoqMSetInterface]
WRawSets.elements_spec1 [axiom, in Metalib.CoqMSetInterface]
WRawSets.Empty [definition, in Metalib.CoqMSetInterface]
WRawSets.empty_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.empty_ok [instance, in Metalib.CoqMSetInterface]
WRawSets.eq [definition, in Metalib.CoqMSetInterface]
WRawSets.Equal [definition, in Metalib.CoqMSetInterface]
WRawSets.equal_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.eq_equiv [instance, in Metalib.CoqMSetInterface]
WRawSets.Exists [definition, in Metalib.CoqMSetInterface]
WRawSets.exists_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.filter_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.filter_ok [instance, in Metalib.CoqMSetInterface]
WRawSets.fold_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.for_all_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.For_all [definition, in Metalib.CoqMSetInterface]
WRawSets.In [axiom, in Metalib.CoqMSetInterface]
WRawSets.inter_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.inter_ok [instance, in Metalib.CoqMSetInterface]
WRawSets.In_compat [instance, in Metalib.CoqMSetInterface]
WRawSets.isok [axiom, in Metalib.CoqMSetInterface]
WRawSets.IsOk [axiom, in Metalib.CoqMSetInterface]
WRawSets.isok_Ok [instance, in Metalib.CoqMSetInterface]
WRawSets.is_empty_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.mem_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.ok [projection, in Metalib.CoqMSetInterface]
WRawSets.Ok [record, in Metalib.CoqMSetInterface]
WRawSets.ok [constructor, in Metalib.CoqMSetInterface]
WRawSets.Ok [inductive, in Metalib.CoqMSetInterface]
WRawSets.partition_spec2 [axiom, in Metalib.CoqMSetInterface]
WRawSets.partition_spec1 [axiom, in Metalib.CoqMSetInterface]
WRawSets.partition_ok2 [instance, in Metalib.CoqMSetInterface]
WRawSets.partition_ok1 [instance, in Metalib.CoqMSetInterface]
WRawSets.remove_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.remove_ok [instance, in Metalib.CoqMSetInterface]
WRawSets.singleton_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.singleton_ok [instance, in Metalib.CoqMSetInterface]
WRawSets.Spec [section, in Metalib.CoqMSetInterface]
WRawSets.Spec.f [variable, in Metalib.CoqMSetInterface]
WRawSets.Spec.s [variable, in Metalib.CoqMSetInterface]
WRawSets.Spec.s' [variable, in Metalib.CoqMSetInterface]
WRawSets.Spec.x [variable, in Metalib.CoqMSetInterface]
WRawSets.Spec.y [variable, in Metalib.CoqMSetInterface]
WRawSets.Subset [definition, in Metalib.CoqMSetInterface]
WRawSets.subset_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.union_spec [axiom, in Metalib.CoqMSetInterface]
WRawSets.union_ok [instance, in Metalib.CoqMSetInterface]
_ [<=] _ [notation, in Metalib.CoqMSetInterface]
_ [=] _ [notation, in Metalib.CoqMSetInterface]
WRaw2Sets [module, in Metalib.CoqMSetInterface]
WRaw2SetsOn [module, in Metalib.CoqMSetInterface]
WRaw2SetsOn.add [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.add_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.cardinal [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.cardinal_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.choose [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.choose_spec2 [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.choose_spec1 [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.compatb [abbreviation, in Metalib.CoqMSetInterface]
WRaw2SetsOn.diff [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.diff_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.elements [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.elements_spec2w [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.elements_spec1 [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.elt [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.empty [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Empty [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.empty_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.eq [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.equal [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Equal [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.equal_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.eq_dec [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.eq_equiv [instance, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Exists [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.exists_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.exists_ [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.filter [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.filter_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.fold [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.fold_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.for_all_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.for_all [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.For_all [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.In [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.inter [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.inter_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.In_compat [instance, in Metalib.CoqMSetInterface]
WRaw2SetsOn.is_empty_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.is_empty [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.is_ok [projection, in Metalib.CoqMSetInterface]
WRaw2SetsOn.mem [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.mem_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Mkt [constructor, in Metalib.CoqMSetInterface]
WRaw2SetsOn.partition [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.partition_spec2 [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.partition_spec1 [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.remove [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.remove_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.singleton [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.singleton_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec [section, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.f [variable, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.s [variable, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.s' [variable, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.x [variable, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.y [variable, in Metalib.CoqMSetInterface]
WRaw2SetsOn.subset [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.Subset [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.subset_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2SetsOn.t [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.this [projection, in Metalib.CoqMSetInterface]
WRaw2SetsOn.t_ [record, in Metalib.CoqMSetInterface]
WRaw2SetsOn.union [definition, in Metalib.CoqMSetInterface]
WRaw2SetsOn.union_spec [lemma, in Metalib.CoqMSetInterface]
WRaw2Sets.E [module, in Metalib.CoqMSetInterface]
WS [module, in Metalib.CoqFSetInterface]
WSets [module, in Metalib.CoqMSetInterface]
WSetsOn [module, in Metalib.CoqMSetInterface]
WSetsOn.add_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.cardinal_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.choose_spec2 [axiom, in Metalib.CoqMSetInterface]
WSetsOn.choose_spec1 [axiom, in Metalib.CoqMSetInterface]
WSetsOn.compatb [abbreviation, in Metalib.CoqMSetInterface]
WSetsOn.diff_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.elements_spec2w [axiom, in Metalib.CoqMSetInterface]
WSetsOn.elements_spec1 [axiom, in Metalib.CoqMSetInterface]
WSetsOn.Empty [definition, in Metalib.CoqMSetInterface]
WSetsOn.empty_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.eq [definition, in Metalib.CoqMSetInterface]
WSetsOn.Equal [definition, in Metalib.CoqMSetInterface]
WSetsOn.equal_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.Exists [definition, in Metalib.CoqMSetInterface]
WSetsOn.exists_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.filter_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.fold_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.for_all_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.For_all [definition, in Metalib.CoqMSetInterface]
WSetsOn.In [axiom, in Metalib.CoqMSetInterface]
WSetsOn.inter_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.In_compat [instance, in Metalib.CoqMSetInterface]
WSetsOn.is_empty_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.mem_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.partition_spec2 [axiom, in Metalib.CoqMSetInterface]
WSetsOn.partition_spec1 [axiom, in Metalib.CoqMSetInterface]
WSetsOn.remove_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.singleton_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.Spec [section, in Metalib.CoqMSetInterface]
WSetsOn.Spec.f [variable, in Metalib.CoqMSetInterface]
WSetsOn.Spec.s [variable, in Metalib.CoqMSetInterface]
WSetsOn.Spec.s' [variable, in Metalib.CoqMSetInterface]
WSetsOn.Spec.x [variable, in Metalib.CoqMSetInterface]
WSetsOn.Spec.y [variable, in Metalib.CoqMSetInterface]
WSetsOn.Subset [definition, in Metalib.CoqMSetInterface]
WSetsOn.subset_spec [axiom, in Metalib.CoqMSetInterface]
WSetsOn.union_spec [axiom, in Metalib.CoqMSetInterface]
_ [<=] _ [notation, in Metalib.CoqMSetInterface]
_ [=] _ [notation, in Metalib.CoqMSetInterface]
WSets.E [module, in Metalib.CoqMSetInterface]
WSfun [module, in Metalib.FSetExtra]
WSfun [module, in Metalib.CoqFSetInterface]
WSfun [module, in Metalib.MSetExtra]
WSfun.add [axiom, in Metalib.CoqFSetInterface]
WSfun.add_3 [axiom, in Metalib.CoqFSetInterface]
WSfun.add_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.add_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.cardinal [axiom, in Metalib.CoqFSetInterface]
WSfun.cardinal_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.choose [axiom, in Metalib.CoqFSetInterface]
WSfun.choose_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.choose_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.diff [axiom, in Metalib.CoqFSetInterface]
WSfun.diff_3 [axiom, in Metalib.CoqFSetInterface]
WSfun.diff_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.diff_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.disjoint [definition, in Metalib.FSetExtra]
WSfun.disjoint [definition, in Metalib.MSetExtra]
WSfun.elements [axiom, in Metalib.CoqFSetInterface]
WSfun.elements_3w [axiom, in Metalib.CoqFSetInterface]
WSfun.elements_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.elements_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.elt [definition, in Metalib.CoqFSetInterface]
WSfun.empty [axiom, in Metalib.CoqFSetInterface]
WSfun.Empty [definition, in Metalib.CoqFSetInterface]
WSfun.empty_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.eq [definition, in Metalib.CoqFSetInterface]
WSfun.equal [axiom, in Metalib.CoqFSetInterface]
WSfun.Equal [definition, in Metalib.CoqFSetInterface]
WSfun.equal_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.equal_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.eq_trans [axiom, in Metalib.CoqFSetInterface]
WSfun.eq_sym [axiom, in Metalib.CoqFSetInterface]
WSfun.eq_refl [axiom, in Metalib.CoqFSetInterface]
WSfun.eq_dec [axiom, in Metalib.CoqFSetInterface]
WSfun.Exists [definition, in Metalib.CoqFSetInterface]
WSfun.exists_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.exists_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.exists_ [axiom, in Metalib.CoqFSetInterface]
WSfun.filter [axiom, in Metalib.CoqFSetInterface]
WSfun.filter_3 [axiom, in Metalib.CoqFSetInterface]
WSfun.filter_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.filter_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.fold [axiom, in Metalib.CoqFSetInterface]
WSfun.fold_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.for_all_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.for_all_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.for_all [axiom, in Metalib.CoqFSetInterface]
WSfun.For_all [definition, in Metalib.CoqFSetInterface]
WSfun.fresh_list [definition, in Metalib.FSetExtra]
WSfun.fresh_list [definition, in Metalib.MSetExtra]
WSfun.In [axiom, in Metalib.CoqFSetInterface]
WSfun.inter [axiom, in Metalib.CoqFSetInterface]
WSfun.inter_3 [axiom, in Metalib.CoqFSetInterface]
WSfun.inter_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.inter_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.In_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.is_empty_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.is_empty_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.is_empty [axiom, in Metalib.CoqFSetInterface]
WSfun.mem [axiom, in Metalib.CoqFSetInterface]
WSfun.mem_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.mem_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.notin [definition, in Metalib.FSetExtra]
WSfun.notin [definition, in Metalib.MSetExtra]
WSfun.partition [axiom, in Metalib.CoqFSetInterface]
WSfun.partition_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.partition_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.remove [axiom, in Metalib.CoqFSetInterface]
WSfun.remove_3 [axiom, in Metalib.CoqFSetInterface]
WSfun.remove_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.remove_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.singleton [axiom, in Metalib.CoqFSetInterface]
WSfun.singleton_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.singleton_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.Spec [section, in Metalib.CoqFSetInterface]
WSfun.Spec.Filter [section, in Metalib.CoqFSetInterface]
WSfun.Spec.Filter.f [variable, in Metalib.CoqFSetInterface]
WSfun.Spec.s [variable, in Metalib.CoqFSetInterface]
WSfun.Spec.s' [variable, in Metalib.CoqFSetInterface]
WSfun.Spec.s'' [variable, in Metalib.CoqFSetInterface]
WSfun.Spec.x [variable, in Metalib.CoqFSetInterface]
WSfun.Spec.y [variable, in Metalib.CoqFSetInterface]
WSfun.subset [axiom, in Metalib.CoqFSetInterface]
WSfun.Subset [definition, in Metalib.CoqFSetInterface]
WSfun.subset_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.subset_1 [axiom, in Metalib.CoqFSetInterface]
WSfun.t [axiom, in Metalib.CoqFSetInterface]
WSfun.union [axiom, in Metalib.CoqFSetInterface]
WSfun.union_3 [axiom, in Metalib.CoqFSetInterface]
WSfun.union_2 [axiom, in Metalib.CoqFSetInterface]
WSfun.union_1 [axiom, in Metalib.CoqFSetInterface]
_ [<=] _ [notation, in Metalib.CoqFSetInterface]
_ [=] _ [notation, in Metalib.CoqFSetInterface]
WS.E [module, in Metalib.CoqFSetInterface]
other
_ === _ (coqeqdec_scope) [notation, in Metalib.Metatheory]_ == _ (coqeqdec_scope) [notation, in Metalib.Metatheory]
_ == _ (coqeqdec_scope) [notation, in Metalib.CoqEqDec]
[ _ ] (env_scope) [notation, in Metalib.Metatheory]
_ \u _ (set_sl_scope) [notation, in Metalib.Metatheory]
_ \notin _ (set_sl_scope) [notation, in Metalib.Metatheory]
_ \in _ (set_sl_scope) [notation, in Metalib.Metatheory]
_ `union` _ (set_hs_scope) [notation, in Metalib.Metatheory]
_ `notin` _ (set_hs_scope) [notation, in Metalib.Metatheory]
_ `in` _ (set_hs_scope) [notation, in Metalib.Metatheory]
{{ _ }} (set_scope) [notation, in Metalib.Metatheory]
{} (set_scope) [notation, in Metalib.Metatheory]
_ [<=] _ (set_scope) [notation, in Metalib.Metatheory]
_ [=] _ (set_scope) [notation, in Metalib.Metatheory]
Notation Index
M
_ ~ _ (list_scope) [in Metalib.AssocList]S
_ [=] _ [in Metalib.CoqFSetInterface]W
_ [<=] _ [in Metalib.CoqMSetInterface]_ [=] _ [in Metalib.CoqMSetInterface]
_ [<=] _ [in Metalib.CoqMSetInterface]
_ [=] _ [in Metalib.CoqMSetInterface]
_ [<=] _ [in Metalib.CoqFSetInterface]
_ [=] _ [in Metalib.CoqFSetInterface]
other
_ === _ (coqeqdec_scope) [in Metalib.Metatheory]_ == _ (coqeqdec_scope) [in Metalib.Metatheory]
_ == _ (coqeqdec_scope) [in Metalib.CoqEqDec]
[ _ ] (env_scope) [in Metalib.Metatheory]
_ \u _ (set_sl_scope) [in Metalib.Metatheory]
_ \notin _ (set_sl_scope) [in Metalib.Metatheory]
_ \in _ (set_sl_scope) [in Metalib.Metatheory]
_ `union` _ (set_hs_scope) [in Metalib.Metatheory]
_ `notin` _ (set_hs_scope) [in Metalib.Metatheory]
_ `in` _ (set_hs_scope) [in Metalib.Metatheory]
{{ _ }} (set_scope) [in Metalib.Metatheory]
{} (set_scope) [in Metalib.Metatheory]
_ [<=] _ (set_scope) [in Metalib.Metatheory]
_ [=] _ (set_scope) [in Metalib.Metatheory]
Module Index
A
Atom [in Metalib.MetatheoryAtom]ATOM [in Metalib.MetatheoryAtom]
AtomSetDecide [in Metalib.MetatheoryAtom]
AtomSetFacts [in Metalib.MetatheoryAtom]
AtomSetImpl [in Metalib.MetatheoryAtom]
AtomSetNotin [in Metalib.MetatheoryAtom]
AtomSetProperties [in Metalib.MetatheoryAtom]
D
Decide [in Metalib.CoqFSetDecide]Decide [in Metalib.CoqMSetDecide]
E
EnvImpl [in Metalib.Metatheory]H
HasOrdOps [in Metalib.CoqMSetInterface]HasWOps [in Metalib.CoqMSetInterface]
I
IN [in Metalib.CoqMSetInterface]M
Make [in Metalib.FSetExtra]Make [in Metalib.AssocList]
Make [in Metalib.MSetExtra]
MakeListOrdering [in Metalib.CoqMSetInterface]
MakeListOrdering.MO [in Metalib.CoqMSetInterface]
MakeSetOrdering [in Metalib.CoqMSetInterface]
MakeSetOrdering.MO [in Metalib.CoqMSetInterface]
Make.D [in Metalib.AssocList]
Make.KeySetFacts [in Metalib.AssocList]
Make.KeySetProperties [in Metalib.AssocList]
N
Notin_fun.D [in Metalib.FSetWeakNotin]Notin_fun [in Metalib.FSetWeakNotin]
Notin_fun.D [in Metalib.MSetWeakNotin]
Notin_fun [in Metalib.MSetWeakNotin]
O
Ops [in Metalib.CoqMSetInterface]R
RawSets [in Metalib.CoqMSetInterface]Raw2Sets [in Metalib.CoqMSetInterface]
Raw2SetsOn [in Metalib.CoqMSetInterface]
Raw2Sets.E [in Metalib.CoqMSetInterface]
S
S [in Metalib.CoqMSetInterface]S [in Metalib.CoqFSetInterface]
Sdep [in Metalib.CoqFSetInterface]
Sdep.E [in Metalib.CoqFSetInterface]
Sets [in Metalib.CoqMSetInterface]
SetsOn [in Metalib.CoqMSetInterface]
Sets.E [in Metalib.CoqMSetInterface]
Sfun [in Metalib.CoqFSetInterface]
S.E [in Metalib.CoqFSetInterface]
T
TypElt [in Metalib.CoqMSetInterface]W
WDecide [in Metalib.CoqFSetDecide]WDecide [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary [in Metalib.CoqFSetDecide]
WDecide_fun.FSetLogicalFacts [in Metalib.CoqFSetDecide]
WDecide_fun.F [in Metalib.CoqFSetDecide]
WDecide_fun [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary [in Metalib.CoqMSetDecide]
WDecide_fun.FSetLogicalFacts [in Metalib.CoqMSetDecide]
WDecide_fun.F [in Metalib.CoqMSetDecide]
WDecide_fun [in Metalib.CoqMSetDecide]
WOps [in Metalib.CoqMSetInterface]
WRawSets [in Metalib.CoqMSetInterface]
WRaw2Sets [in Metalib.CoqMSetInterface]
WRaw2SetsOn [in Metalib.CoqMSetInterface]
WRaw2Sets.E [in Metalib.CoqMSetInterface]
WS [in Metalib.CoqFSetInterface]
WSets [in Metalib.CoqMSetInterface]
WSetsOn [in Metalib.CoqMSetInterface]
WSets.E [in Metalib.CoqMSetInterface]
WSfun [in Metalib.FSetExtra]
WSfun [in Metalib.CoqFSetInterface]
WSfun [in Metalib.MSetExtra]
WS.E [in Metalib.CoqFSetInterface]
Variable Index
D
DecidableSorting.A [in Metalib.CoqListFacts]DecidableSorting.leA [in Metalib.CoqListFacts]
DecidableSorting.leA_dec [in Metalib.CoqListFacts]
M
Make.AssortedListProperties.x [in Metalib.AssocList]Make.AssortedListProperties.X [in Metalib.AssocList]
Make.AssortedListProperties.xs [in Metalib.AssocList]
Make.AssortedListProperties.ys [in Metalib.AssocList]
Make.AssortedListProperties.zs [in Metalib.AssocList]
Make.BindsDerived.a [in Metalib.AssocList]
Make.BindsDerived.A [in Metalib.AssocList]
Make.BindsDerived.b [in Metalib.AssocList]
Make.BindsDerived.B [in Metalib.AssocList]
Make.BindsDerived.E [in Metalib.AssocList]
Make.BindsDerived.F [in Metalib.AssocList]
Make.BindsDerived.f [in Metalib.AssocList]
Make.BindsDerived.G [in Metalib.AssocList]
Make.BindsDerived.x [in Metalib.AssocList]
Make.BindsDerived.y [in Metalib.AssocList]
Make.BindsProperties.a [in Metalib.AssocList]
Make.BindsProperties.A [in Metalib.AssocList]
Make.BindsProperties.b [in Metalib.AssocList]
Make.BindsProperties.B [in Metalib.AssocList]
Make.BindsProperties.b0 [in Metalib.AssocList]
Make.BindsProperties.E [in Metalib.AssocList]
Make.BindsProperties.F [in Metalib.AssocList]
Make.BindsProperties.f [in Metalib.AssocList]
Make.BindsProperties.G [in Metalib.AssocList]
Make.BindsProperties.x [in Metalib.AssocList]
Make.BindsProperties.y [in Metalib.AssocList]
Make.BindsProperties2.a [in Metalib.AssocList]
Make.BindsProperties2.A [in Metalib.AssocList]
Make.BindsProperties2.b [in Metalib.AssocList]
Make.BindsProperties2.B [in Metalib.AssocList]
Make.BindsProperties2.E [in Metalib.AssocList]
Make.BindsProperties2.F [in Metalib.AssocList]
Make.BindsProperties2.f [in Metalib.AssocList]
Make.BindsProperties2.G [in Metalib.AssocList]
Make.BindsProperties2.x [in Metalib.AssocList]
Make.BindsProperties2.y [in Metalib.AssocList]
Make.ListProperties.l [in Metalib.AssocList]
Make.ListProperties.l1 [in Metalib.AssocList]
Make.ListProperties.l2 [in Metalib.AssocList]
Make.ListProperties.l3 [in Metalib.AssocList]
Make.ListProperties.x [in Metalib.AssocList]
Make.ListProperties.X [in Metalib.AssocList]
Make.ListProperties.y [in Metalib.AssocList]
Make.Properties.A [in Metalib.AssocList]
Make.Properties.b [in Metalib.AssocList]
Make.Properties.B [in Metalib.AssocList]
Make.Properties.E [in Metalib.AssocList]
Make.Properties.F [in Metalib.AssocList]
Make.Properties.f [in Metalib.AssocList]
Make.Properties.G [in Metalib.AssocList]
Make.Properties.key [in Metalib.AssocList]
Make.Properties.x [in Metalib.AssocList]
Make.UniqDerived.a [in Metalib.AssocList]
Make.UniqDerived.A [in Metalib.AssocList]
Make.UniqDerived.b [in Metalib.AssocList]
Make.UniqDerived.E [in Metalib.AssocList]
Make.UniqDerived.F [in Metalib.AssocList]
Make.UniqDerived.G [in Metalib.AssocList]
Make.UniqDerived.x [in Metalib.AssocList]
Make.UniqDerived.y [in Metalib.AssocList]
Make.UniqMid.a [in Metalib.AssocList]
Make.UniqMid.A [in Metalib.AssocList]
Make.UniqMid.B [in Metalib.AssocList]
Make.UniqMid.E [in Metalib.AssocList]
Make.UniqMid.F [in Metalib.AssocList]
Make.UniqMid.f [in Metalib.AssocList]
Make.UniqMid.x [in Metalib.AssocList]
Make.UniqMid.y [in Metalib.AssocList]
Make.UniqProperties.a [in Metalib.AssocList]
Make.UniqProperties.A [in Metalib.AssocList]
Make.UniqProperties.b [in Metalib.AssocList]
Make.UniqProperties.B [in Metalib.AssocList]
Make.UniqProperties.E [in Metalib.AssocList]
Make.UniqProperties.F [in Metalib.AssocList]
Make.UniqProperties.f [in Metalib.AssocList]
Make.UniqProperties.G [in Metalib.AssocList]
Make.UniqProperties.x [in Metalib.AssocList]
N
Notin_fun.Lemmas.s' [in Metalib.FSetWeakNotin]Notin_fun.Lemmas.s [in Metalib.FSetWeakNotin]
Notin_fun.Lemmas.y [in Metalib.FSetWeakNotin]
Notin_fun.Lemmas.x [in Metalib.FSetWeakNotin]
Notin_fun.Lemmas.s' [in Metalib.MSetWeakNotin]
Notin_fun.Lemmas.s [in Metalib.MSetWeakNotin]
Notin_fun.Lemmas.y [in Metalib.MSetWeakNotin]
Notin_fun.Lemmas.x [in Metalib.MSetWeakNotin]
R
RawSets.Spec.s [in Metalib.CoqMSetInterface]RawSets.Spec.s' [in Metalib.CoqMSetInterface]
RawSets.Spec.x [in Metalib.CoqMSetInterface]
RawSets.Spec.y [in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.s [in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.s' [in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.s'' [in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.x [in Metalib.CoqMSetInterface]
Raw2SetsOn.Spec.y [in Metalib.CoqMSetInterface]
S
SetsOn.Spec.s [in Metalib.CoqMSetInterface]SetsOn.Spec.s' [in Metalib.CoqMSetInterface]
SetsOn.Spec.x [in Metalib.CoqMSetInterface]
SetsOn.Spec.y [in Metalib.CoqMSetInterface]
Sfun.Spec.s [in Metalib.CoqFSetInterface]
Sfun.Spec.s' [in Metalib.CoqFSetInterface]
Sfun.Spec.s'' [in Metalib.CoqFSetInterface]
Sfun.Spec.x [in Metalib.CoqFSetInterface]
Sfun.Spec.y [in Metalib.CoqFSetInterface]
SortedListEquality.A [in Metalib.CoqListFacts]
SortedListEquality.eqA_ltA [in Metalib.CoqListFacts]
SortedListEquality.ltA [in Metalib.CoqListFacts]
SortedListEquality.ltA_eqA [in Metalib.CoqListFacts]
SortedListEquality.ltA_not_eqA [in Metalib.CoqListFacts]
SortedListEquality.ltA_trans [in Metalib.CoqListFacts]
U
Uniqueness_Of_SetoidList_Proofs.list_eq_dec [in Metalib.CoqListFacts]Uniqueness_Of_SetoidList_Proofs.R_unique [in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.R [in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.A [in Metalib.CoqListFacts]
Uniqueness_Of_SetoidList_Proofs.list_eq_dec [in Metalib.CoqUniquenessTacEx]
Uniqueness_Of_SetoidList_Proofs.R_unique [in Metalib.CoqUniquenessTacEx]
Uniqueness_Of_SetoidList_Proofs.R [in Metalib.CoqUniquenessTacEx]
Uniqueness_Of_SetoidList_Proofs.A [in Metalib.CoqUniquenessTacEx]
W
WRawSets.Spec.f [in Metalib.CoqMSetInterface]WRawSets.Spec.s [in Metalib.CoqMSetInterface]
WRawSets.Spec.s' [in Metalib.CoqMSetInterface]
WRawSets.Spec.x [in Metalib.CoqMSetInterface]
WRawSets.Spec.y [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.f [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.s [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.s' [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.x [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Spec.y [in Metalib.CoqMSetInterface]
WSetsOn.Spec.f [in Metalib.CoqMSetInterface]
WSetsOn.Spec.s [in Metalib.CoqMSetInterface]
WSetsOn.Spec.s' [in Metalib.CoqMSetInterface]
WSetsOn.Spec.x [in Metalib.CoqMSetInterface]
WSetsOn.Spec.y [in Metalib.CoqMSetInterface]
WSfun.Spec.Filter.f [in Metalib.CoqFSetInterface]
WSfun.Spec.s [in Metalib.CoqFSetInterface]
WSfun.Spec.s' [in Metalib.CoqFSetInterface]
WSfun.Spec.s'' [in Metalib.CoqFSetInterface]
WSfun.Spec.x [in Metalib.CoqFSetInterface]
WSfun.Spec.y [in Metalib.CoqFSetInterface]
Library Index
A
AssocListC
CoqEqDecCoqFSetDecide
CoqFSetInterface
CoqListFacts
CoqMSetDecide
CoqMSetInterface
CoqUniquenessTac
CoqUniquenessTacEx
F
FSetExtraFSetWeakNotin
Fsub_Lemmas
Fsub_Soundness
Fsub_proofs
Fsub_Infrastructure
Fsub_Definitions
Fsub_inf
Fsub_ott
L
LibDefaultSimpLibLNgen
LibTactics
M
MetatheoryMetatheoryAtom
MSetExtra
MSetWeakNotin
Lemma Index
A
app_cons_not_nil [in Metalib.CoqListFacts]app_eq_cons [in Metalib.CoqListFacts]
atom_fresh [in Metalib.MetatheoryAtom]
Atom.atom_fresh_for_list [in Metalib.MetatheoryAtom]
Atom.fresh_not_in [in Metalib.MetatheoryAtom]
Atom.max_lt_r [in Metalib.MetatheoryAtom]
Atom.nat_list_max [in Metalib.MetatheoryAtom]
B
body_inr_from_expr_case [in LN.Fsub_Infrastructure]body_inl_from_expr_case [in LN.Fsub_Infrastructure]
body_from_expr_let [in LN.Fsub_Infrastructure]
C
canonical_form_sum [in LN.Fsub_Soundness]canonical_form_tabs [in LN.Fsub_Soundness]
canonical_form_abs [in LN.Fsub_Soundness]
canonical_form_sum [in LNgen.Fsub_proofs]
canonical_form_tabs [in LNgen.Fsub_proofs]
canonical_form_abs [in LNgen.Fsub_proofs]
close_exp_wrt_exp_lc_exp [in LNgen.Fsub_inf]
close_exp_wrt_typ_lc_exp [in LNgen.Fsub_inf]
close_binding_wrt_typ_lc_binding [in LNgen.Fsub_inf]
close_typ_wrt_typ_lc_typ [in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_degree_exp_wrt_exp [in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_degree_exp_wrt_typ [in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_degree_exp_wrt_typ_mutual [in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_degree_binding_wrt_typ [in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_degree_binding_wrt_typ_mutual [in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_degree_typ_wrt_typ [in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_degree_typ_wrt_typ_mutual [in LNgen.Fsub_inf]
close_exp_wrt_exp_open_exp_wrt_exp [in LNgen.Fsub_inf]
close_exp_wrt_typ_open_exp_wrt_typ [in LNgen.Fsub_inf]
close_binding_wrt_typ_open_binding_wrt_typ [in LNgen.Fsub_inf]
close_typ_wrt_typ_open_typ_wrt_typ [in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_open_binding_wrt_typ_rec [in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_open_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_open_typ_wrt_typ_rec [in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_open_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
close_exp_wrt_exp_inj [in LNgen.Fsub_inf]
close_exp_wrt_typ_inj [in LNgen.Fsub_inf]
close_binding_wrt_typ_inj [in LNgen.Fsub_inf]
close_typ_wrt_typ_inj [in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_inj [in LNgen.Fsub_inf]
close_exp_wrt_exp_rec_inj_mutual [in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_inj [in LNgen.Fsub_inf]
close_exp_wrt_typ_rec_inj_mutual [in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_inj [in LNgen.Fsub_inf]
close_binding_wrt_typ_rec_inj_mutual [in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_inj [in LNgen.Fsub_inf]
close_typ_wrt_typ_rec_inj_mutual [in LNgen.Fsub_inf]
cons_eq_app [in Metalib.CoqListFacts]
D
degree_exp_wrt_exp_of_lc_exp [in LNgen.Fsub_inf]degree_exp_wrt_exp_of_lc_exp_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_of_lc_exp [in LNgen.Fsub_inf]
degree_exp_wrt_typ_of_lc_exp_mutual [in LNgen.Fsub_inf]
degree_binding_wrt_typ_of_lc_binding [in LNgen.Fsub_inf]
degree_binding_wrt_typ_of_lc_binding_mutual [in LNgen.Fsub_inf]
degree_typ_wrt_typ_of_lc_typ [in LNgen.Fsub_inf]
degree_typ_wrt_typ_of_lc_typ_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_inv [in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_inv [in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ [in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ [in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
degree_exp_wrt_exp_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
degree_exp_wrt_typ_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec [in LNgen.Fsub_inf]
degree_binding_wrt_typ_open_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec [in LNgen.Fsub_inf]
degree_typ_wrt_typ_open_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_inv [in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_inv [in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec_inv [in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec_inv_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ [in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ [in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
degree_exp_wrt_exp_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
degree_exp_wrt_typ_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec [in LNgen.Fsub_inf]
degree_binding_wrt_typ_close_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec [in LNgen.Fsub_inf]
degree_typ_wrt_typ_close_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_exp_O [in LNgen.Fsub_inf]
degree_exp_wrt_typ_O [in LNgen.Fsub_inf]
degree_binding_wrt_typ_O [in LNgen.Fsub_inf]
degree_typ_wrt_typ_O [in LNgen.Fsub_inf]
degree_exp_wrt_exp_S [in LNgen.Fsub_inf]
degree_exp_wrt_exp_S_mutual [in LNgen.Fsub_inf]
degree_exp_wrt_typ_S [in LNgen.Fsub_inf]
degree_exp_wrt_typ_S_mutual [in LNgen.Fsub_inf]
degree_binding_wrt_typ_S [in LNgen.Fsub_inf]
degree_binding_wrt_typ_S_mutual [in LNgen.Fsub_inf]
degree_typ_wrt_typ_S [in LNgen.Fsub_inf]
degree_typ_wrt_typ_S_mutual [in LNgen.Fsub_inf]
E
elim_incl_app [in Metalib.CoqListFacts]elim_incl_cons [in Metalib.CoqListFacts]
elim_not_In_app [in Metalib.CoqListFacts]
elim_not_In_cons [in Metalib.CoqListFacts]
eqlistA_unique [in Metalib.CoqListFacts]
eqlistA_unique [in Metalib.CoqUniquenessTacEx]
eqlist_eq [in Metalib.CoqListFacts]
Equal_union_compat [in Metalib.LibLNgen]
equiv_decidable [in Metalib.CoqEqDec]
equiv_transitive' [in Metalib.CoqEqDec]
equiv_symmetric' [in Metalib.CoqEqDec]
equiv_reflexive' [in Metalib.CoqEqDec]
eq_pair_dec [in Metalib.CoqUniquenessTac]
eq_unit_dec [in Metalib.CoqUniquenessTac]
eq_dec_refl [in Metalib.CoqEqDec]
example_pick_fresh_use [in Metalib.MetatheoryAtom]
expr_case_from_body [in LN.Fsub_Infrastructure]
expr_let_from_body [in LN.Fsub_Infrastructure]
F
fv_exp_in_exp_subst_exp_in_exp_upper [in LNgen.Fsub_inf]fv_exp_in_exp_subst_exp_in_exp_upper_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_upper [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_upper [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_upper [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_upper [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_upper [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_upper_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_notin [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_notin_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_notin [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_notin_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_notin [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_notin_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_notin [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_notin_mutual [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_notin [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_notin_mutual [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_notin [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_notin_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_lower [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_lower_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_lower [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_typ_in_exp_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_lower [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_lower [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_lower [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_lower [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_lower_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_fresh [in LNgen.Fsub_inf]
fv_exp_in_exp_subst_exp_in_exp_fresh_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_fresh [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_exp_in_exp_fresh_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_fresh [in LNgen.Fsub_inf]
fv_typ_in_exp_subst_typ_in_exp_fresh_mutual [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_fresh [in LNgen.Fsub_inf]
fv_typ_in_binding_subst_typ_in_binding_fresh_mutual [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_fresh [in LNgen.Fsub_inf]
fv_typ_in_typ_subst_typ_in_typ_fresh_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_upper [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_upper [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_upper [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_upper [in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_upper [in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_upper [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_upper [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_upper_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_upper [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_upper [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_upper [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_upper [in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_upper_mutual [in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_upper [in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_upper_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_lower [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_lower [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_lower [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_lower [in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_lower [in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_lower [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_lower [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_exp_rec_lower_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_lower [in LNgen.Fsub_inf]
fv_exp_in_exp_open_exp_wrt_typ_rec_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_lower [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_exp_rec_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_lower [in LNgen.Fsub_inf]
fv_typ_in_exp_open_exp_wrt_typ_rec_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_lower [in LNgen.Fsub_inf]
fv_typ_in_binding_open_binding_wrt_typ_rec_lower_mutual [in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_lower [in LNgen.Fsub_inf]
fv_typ_in_typ_open_typ_wrt_typ_rec_lower_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_exp [in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_typ [in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_exp [in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_typ [in LNgen.Fsub_inf]
fv_typ_in_binding_close_binding_wrt_typ [in LNgen.Fsub_inf]
fv_typ_in_typ_close_typ_wrt_typ [in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
fv_exp_in_exp_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
fv_typ_in_exp_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
fv_typ_in_binding_close_binding_wrt_typ_rec [in LNgen.Fsub_inf]
fv_typ_in_binding_close_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
fv_typ_in_typ_close_typ_wrt_typ_rec [in LNgen.Fsub_inf]
fv_typ_in_typ_close_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
I
InA_iff_In [in Metalib.CoqListFacts]InA_In [in Metalib.CoqListFacts]
incl_nil [in Metalib.CoqListFacts]
In_incl [in Metalib.CoqListFacts]
In_map [in Metalib.CoqListFacts]
L
lc_set_exp_of_lc_exp [in LNgen.Fsub_inf]lc_set_exp_of_lc_exp_size_mutual [in LNgen.Fsub_inf]
lc_set_binding_of_lc_binding [in LNgen.Fsub_inf]
lc_set_binding_of_lc_binding_size_mutual [in LNgen.Fsub_inf]
lc_set_typ_of_lc_typ [in LNgen.Fsub_inf]
lc_set_typ_of_lc_typ_size_mutual [in LNgen.Fsub_inf]
lc_exp_of_lc_set_exp [in LNgen.Fsub_inf]
lc_exp_of_lc_set_exp_mutual [in LNgen.Fsub_inf]
lc_binding_of_lc_set_binding [in LNgen.Fsub_inf]
lc_binding_of_lc_set_binding_mutual [in LNgen.Fsub_inf]
lc_typ_of_lc_set_typ [in LNgen.Fsub_inf]
lc_typ_of_lc_set_typ_mutual [in LNgen.Fsub_inf]
lc_exp_unique [in LNgen.Fsub_inf]
lc_exp_unique_mutual [in LNgen.Fsub_inf]
lc_binding_unique [in LNgen.Fsub_inf]
lc_binding_unique_mutual [in LNgen.Fsub_inf]
lc_typ_unique [in LNgen.Fsub_inf]
lc_typ_unique_mutual [in LNgen.Fsub_inf]
lc_body_exp_case_3 [in LNgen.Fsub_inf]
lc_body_exp_case_2 [in LNgen.Fsub_inf]
lc_body_exp_let_2 [in LNgen.Fsub_inf]
lc_body_exp_tabs_2 [in LNgen.Fsub_inf]
lc_body_exp_abs_2 [in LNgen.Fsub_inf]
lc_body_typ_all_2 [in LNgen.Fsub_inf]
lc_body_exp_wrt_exp [in LNgen.Fsub_inf]
lc_body_exp_wrt_typ [in LNgen.Fsub_inf]
lc_body_binding_wrt_typ [in LNgen.Fsub_inf]
lc_body_typ_wrt_typ [in LNgen.Fsub_inf]
lc_exp_case_exists [in LNgen.Fsub_inf]
lc_exp_let_exists [in LNgen.Fsub_inf]
lc_exp_tabs_exists [in LNgen.Fsub_inf]
lc_exp_abs_exists [in LNgen.Fsub_inf]
lc_typ_all_exists [in LNgen.Fsub_inf]
lc_exp_of_degree [in LNgen.Fsub_inf]
lc_exp_of_degree_size_mutual [in LNgen.Fsub_inf]
lc_binding_of_degree [in LNgen.Fsub_inf]
lc_binding_of_degree_size_mutual [in LNgen.Fsub_inf]
lc_typ_of_degree [in LNgen.Fsub_inf]
lc_typ_of_degree_size_mutual [in LNgen.Fsub_inf]
lelistA_unique [in Metalib.CoqListFacts]
lelistA_dec [in Metalib.CoqListFacts]
lelistA_unique [in Metalib.CoqUniquenessTacEx]
le_unique [in Metalib.CoqUniquenessTacEx]
M
MakeListOrdering.cons_CompSpec [in Metalib.CoqMSetInterface]MakeListOrdering.eq_cons [in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_add_eq [in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_add_lt [in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_empty_l [in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_empty_r [in Metalib.CoqMSetInterface]
Make.alist_ind [in Metalib.AssocList]
Make.app_eq_one [in Metalib.AssocList]
Make.app_nil_2 [in Metalib.AssocList]
Make.app_nil_1 [in Metalib.AssocList]
Make.app_assoc [in Metalib.AssocList]
Make.binds_split [in Metalib.AssocList]
Make.binds_unique [in Metalib.AssocList]
Make.binds_In_inv [in Metalib.AssocList]
Make.binds_In [in Metalib.AssocList]
Make.binds_remove_mid [in Metalib.AssocList]
Make.binds_mid_eq [in Metalib.AssocList]
Make.binds_weaken [in Metalib.AssocList]
Make.binds_lookup_dec [in Metalib.AssocList]
Make.binds_lookup [in Metalib.AssocList]
Make.binds_dec [in Metalib.AssocList]
Make.binds_cons_uniq_iff [in Metalib.AssocList]
Make.binds_cons_uniq_1 [in Metalib.AssocList]
Make.binds_app_uniq_iff [in Metalib.AssocList]
Make.binds_app_uniq_1 [in Metalib.AssocList]
Make.binds_dom_contradiction [in Metalib.AssocList]
Make.binds_map_3 [in Metalib.AssocList]
Make.binds_map_2 [in Metalib.AssocList]
Make.binds_map_1 [in Metalib.AssocList]
Make.binds_app_iff [in Metalib.AssocList]
Make.binds_app_3 [in Metalib.AssocList]
Make.binds_app_2 [in Metalib.AssocList]
Make.binds_app_1 [in Metalib.AssocList]
Make.binds_cons_iff [in Metalib.AssocList]
Make.binds_cons_3 [in Metalib.AssocList]
Make.binds_cons_2 [in Metalib.AssocList]
Make.binds_cons_1 [in Metalib.AssocList]
Make.binds_one_iff [in Metalib.AssocList]
Make.binds_one_3 [in Metalib.AssocList]
Make.binds_one_2 [in Metalib.AssocList]
Make.binds_one_1 [in Metalib.AssocList]
Make.binds_nil_iff [in Metalib.AssocList]
Make.cons_app_assoc [in Metalib.AssocList]
Make.cons_app_one [in Metalib.AssocList]
Make.disjoint_map_r [in Metalib.AssocList]
Make.disjoint_map_l [in Metalib.AssocList]
Make.disjoint_map_2 [in Metalib.AssocList]
Make.disjoint_map_1 [in Metalib.AssocList]
Make.disjoint_app_r [in Metalib.AssocList]
Make.disjoint_app_l [in Metalib.AssocList]
Make.disjoint_app_3 [in Metalib.AssocList]
Make.disjoint_app_2 [in Metalib.AssocList]
Make.disjoint_app_1 [in Metalib.AssocList]
Make.disjoint_cons_r [in Metalib.AssocList]
Make.disjoint_cons_l [in Metalib.AssocList]
Make.disjoint_cons_3 [in Metalib.AssocList]
Make.disjoint_cons_2 [in Metalib.AssocList]
Make.disjoint_cons_1 [in Metalib.AssocList]
Make.disjoint_one_r [in Metalib.AssocList]
Make.disjoint_one_l [in Metalib.AssocList]
Make.disjoint_one_2 [in Metalib.AssocList]
Make.disjoint_one_1 [in Metalib.AssocList]
Make.disjoint_nil_1 [in Metalib.AssocList]
Make.disjoint_sym [in Metalib.AssocList]
Make.disjoint_sym_1 [in Metalib.AssocList]
Make.dom_map [in Metalib.AssocList]
Make.dom_app [in Metalib.AssocList]
Make.dom_cons [in Metalib.AssocList]
Make.dom_one [in Metalib.AssocList]
Make.dom_nil [in Metalib.AssocList]
Make.fresh_app_r [in Metalib.AssocList]
Make.fresh_app_l [in Metalib.AssocList]
Make.fresh_mid_head [in Metalib.AssocList]
Make.fresh_mid_tail [in Metalib.AssocList]
Make.in_app_iff [in Metalib.AssocList]
Make.in_one_iff [in Metalib.AssocList]
Make.in_nil_iff [in Metalib.AssocList]
Make.map_app [in Metalib.AssocList]
Make.map_cons [in Metalib.AssocList]
Make.map_one [in Metalib.AssocList]
Make.map_nil [in Metalib.AssocList]
Make.nil_neq_one_mid [in Metalib.AssocList]
Make.one_mid_neq_nil [in Metalib.AssocList]
Make.one_eq_app [in Metalib.AssocList]
Make.uniq_align_eq [in Metalib.AssocList]
Make.uniq_mid [in Metalib.AssocList]
Make.uniq_map_app_l [in Metalib.AssocList]
Make.uniq_reorder_2 [in Metalib.AssocList]
Make.uniq_reorder_1 [in Metalib.AssocList]
Make.uniq_remove_mid [in Metalib.AssocList]
Make.uniq_insert_mid [in Metalib.AssocList]
Make.uniq_map_iff [in Metalib.AssocList]
Make.uniq_map_2 [in Metalib.AssocList]
Make.uniq_map_1 [in Metalib.AssocList]
Make.uniq_app_iff [in Metalib.AssocList]
Make.uniq_app_4 [in Metalib.AssocList]
Make.uniq_app_3 [in Metalib.AssocList]
Make.uniq_app_2 [in Metalib.AssocList]
Make.uniq_app_1 [in Metalib.AssocList]
Make.uniq_cons_iff [in Metalib.AssocList]
Make.uniq_cons_3 [in Metalib.AssocList]
Make.uniq_cons_2 [in Metalib.AssocList]
Make.uniq_cons_1 [in Metalib.AssocList]
Make.uniq_one_1 [in Metalib.AssocList]
map_subst_typ_in_binding_id [in LNgen.Fsub_proofs]
map_subst_tb_id [in LN.Fsub_Lemmas]
N
nil_eq_app [in Metalib.CoqListFacts]Notin_fun.test_solve_notin_7 [in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_6 [in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_5 [in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_4 [in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_3 [in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_2 [in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_1 [in Metalib.FSetWeakNotin]
Notin_fun.notin_diff_3 [in Metalib.FSetWeakNotin]
Notin_fun.notin_diff_2 [in Metalib.FSetWeakNotin]
Notin_fun.notin_diff_1 [in Metalib.FSetWeakNotin]
Notin_fun.notin_inter_3 [in Metalib.FSetWeakNotin]
Notin_fun.notin_inter_2 [in Metalib.FSetWeakNotin]
Notin_fun.notin_inter_1 [in Metalib.FSetWeakNotin]
Notin_fun.notin_union_3 [in Metalib.FSetWeakNotin]
Notin_fun.notin_union_2 [in Metalib.FSetWeakNotin]
Notin_fun.notin_union_1 [in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_3' [in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_3 [in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_2 [in Metalib.FSetWeakNotin]
Notin_fun.notin_remove_1 [in Metalib.FSetWeakNotin]
Notin_fun.notin_singleton_2 [in Metalib.FSetWeakNotin]
Notin_fun.notin_singleton_1' [in Metalib.FSetWeakNotin]
Notin_fun.notin_singleton_1 [in Metalib.FSetWeakNotin]
Notin_fun.notin_add_3 [in Metalib.FSetWeakNotin]
Notin_fun.notin_add_2 [in Metalib.FSetWeakNotin]
Notin_fun.notin_add_1' [in Metalib.FSetWeakNotin]
Notin_fun.notin_add_1 [in Metalib.FSetWeakNotin]
Notin_fun.notin_empty_1 [in Metalib.FSetWeakNotin]
Notin_fun.test_solve_notin_7 [in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_6 [in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_5 [in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_4 [in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_3 [in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_2 [in Metalib.MSetWeakNotin]
Notin_fun.test_solve_notin_1 [in Metalib.MSetWeakNotin]
Notin_fun.notin_diff_3 [in Metalib.MSetWeakNotin]
Notin_fun.notin_diff_2 [in Metalib.MSetWeakNotin]
Notin_fun.notin_diff_1 [in Metalib.MSetWeakNotin]
Notin_fun.notin_inter_3 [in Metalib.MSetWeakNotin]
Notin_fun.notin_inter_2 [in Metalib.MSetWeakNotin]
Notin_fun.notin_inter_1 [in Metalib.MSetWeakNotin]
Notin_fun.notin_union_3 [in Metalib.MSetWeakNotin]
Notin_fun.notin_union_2 [in Metalib.MSetWeakNotin]
Notin_fun.notin_union_1 [in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_3' [in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_3 [in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_2 [in Metalib.MSetWeakNotin]
Notin_fun.notin_remove_1 [in Metalib.MSetWeakNotin]
Notin_fun.notin_singleton_2 [in Metalib.MSetWeakNotin]
Notin_fun.notin_singleton_1' [in Metalib.MSetWeakNotin]
Notin_fun.notin_singleton_1 [in Metalib.MSetWeakNotin]
Notin_fun.notin_add_3 [in Metalib.MSetWeakNotin]
Notin_fun.notin_add_2 [in Metalib.MSetWeakNotin]
Notin_fun.notin_add_1' [in Metalib.MSetWeakNotin]
Notin_fun.notin_add_1 [in Metalib.MSetWeakNotin]
Notin_fun.notin_empty_1 [in Metalib.MSetWeakNotin]
notin_fv_wf [in LNgen.Fsub_proofs]
notin_fv_typ_in_typ_open [in LNgen.Fsub_proofs]
notin_fv_wf [in LN.Fsub_Lemmas]
notin_fv_tt_open [in LN.Fsub_Lemmas]
not_In_app [in Metalib.CoqListFacts]
not_In_cons [in Metalib.CoqListFacts]
O
open_exp_wrt_exp_lc_exp [in LNgen.Fsub_inf]open_exp_wrt_typ_lc_exp [in LNgen.Fsub_inf]
open_binding_wrt_typ_lc_binding [in LNgen.Fsub_inf]
open_typ_wrt_typ_lc_typ [in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_degree_exp_wrt_exp [in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_degree_exp_wrt_typ [in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_degree_exp_wrt_typ_mutual [in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_degree_binding_wrt_typ [in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_degree_binding_wrt_typ_mutual [in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_degree_typ_wrt_typ [in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_degree_typ_wrt_typ_mutual [in LNgen.Fsub_inf]
open_exp_wrt_exp_inj [in LNgen.Fsub_inf]
open_exp_wrt_typ_inj [in LNgen.Fsub_inf]
open_binding_wrt_typ_inj [in LNgen.Fsub_inf]
open_typ_wrt_typ_inj [in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_inj [in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_inj_mutual [in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_inj [in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_inj_mutual [in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_inj [in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_inj_mutual [in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_inj [in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_inj_mutual [in LNgen.Fsub_inf]
open_exp_wrt_exp_close_exp_wrt_exp [in LNgen.Fsub_inf]
open_exp_wrt_typ_close_exp_wrt_typ [in LNgen.Fsub_inf]
open_binding_wrt_typ_close_binding_wrt_typ [in LNgen.Fsub_inf]
open_typ_wrt_typ_close_typ_wrt_typ [in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
open_exp_wrt_typ_rec_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_close_binding_wrt_typ_rec [in LNgen.Fsub_inf]
open_binding_wrt_typ_rec_close_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_close_typ_wrt_typ_rec [in LNgen.Fsub_inf]
open_typ_wrt_typ_rec_close_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
open_ee_body_e [in LN.Fsub_Infrastructure]
open_ee_rec_expr [in LN.Fsub_Infrastructure]
open_ee_rec_type_aux [in LN.Fsub_Infrastructure]
open_ee_rec_expr_aux [in LN.Fsub_Infrastructure]
open_te_rec_expr [in LN.Fsub_Infrastructure]
open_te_rec_type_aux [in LN.Fsub_Infrastructure]
open_te_rec_expr_aux [in LN.Fsub_Infrastructure]
open_tt_rec_type [in LN.Fsub_Infrastructure]
open_tt_rec_type_aux [in LN.Fsub_Infrastructure]
P
preservation [in LN.Fsub_Soundness]preservation [in LNgen.Fsub_proofs]
progress [in LN.Fsub_Soundness]
progress [in LNgen.Fsub_proofs]
R
Raw2SetsOn.choose_spec3 [in Metalib.CoqMSetInterface]Raw2SetsOn.compare_spec [in Metalib.CoqMSetInterface]
Raw2SetsOn.elements_spec2 [in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt_spec3 [in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt_spec2 [in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt_spec1 [in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt_spec3 [in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt_spec2 [in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt_spec1 [in Metalib.CoqMSetInterface]
red_regular [in LNgen.Fsub_proofs]
red_regular [in LN.Fsub_Lemmas]
remove_union_distrib [in Metalib.LibLNgen]
S
size_exp_open_exp_wrt_exp_var [in LNgen.Fsub_inf]size_exp_open_exp_wrt_typ_var [in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_var [in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_var [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec_var [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec_var_mutual [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec_var [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec_var_mutual [in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec_var [in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec_var_mutual [in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec_var [in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec_var_mutual [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ [in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ [in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
size_exp_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec [in LNgen.Fsub_inf]
size_binding_open_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec [in LNgen.Fsub_inf]
size_typ_open_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
size_exp_close_exp_wrt_exp [in LNgen.Fsub_inf]
size_exp_close_exp_wrt_typ [in LNgen.Fsub_inf]
size_binding_close_binding_wrt_typ [in LNgen.Fsub_inf]
size_typ_close_typ_wrt_typ [in LNgen.Fsub_inf]
size_exp_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
size_exp_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
size_exp_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
size_exp_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
size_binding_close_binding_wrt_typ_rec [in LNgen.Fsub_inf]
size_binding_close_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
size_typ_close_typ_wrt_typ_rec [in LNgen.Fsub_inf]
size_typ_close_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
size_exp_min [in LNgen.Fsub_inf]
size_exp_min_mutual [in LNgen.Fsub_inf]
size_binding_min [in LNgen.Fsub_inf]
size_binding_min_mutual [in LNgen.Fsub_inf]
size_typ_min [in LNgen.Fsub_inf]
size_typ_min_mutual [in LNgen.Fsub_inf]
sort_unique [in Metalib.CoqListFacts]
Sort_In_eq [in Metalib.CoqListFacts]
Sort_InA_eq [in Metalib.CoqListFacts]
sort_dec [in Metalib.CoqListFacts]
sort_unique [in Metalib.CoqUniquenessTacEx]
Subset_union_lngen_open_upper [in Metalib.LibLNgen]
Subset_union_right [in Metalib.LibLNgen]
Subset_union_left [in Metalib.LibLNgen]
Subset_union_compat [in Metalib.LibLNgen]
Subset_empty_any [in Metalib.LibLNgen]
Subset_refl [in Metalib.LibLNgen]
subst_exp_in_exp_intro [in LNgen.Fsub_inf]
subst_typ_in_exp_intro [in LNgen.Fsub_inf]
subst_typ_in_binding_intro [in LNgen.Fsub_inf]
subst_typ_in_typ_intro [in LNgen.Fsub_inf]
subst_exp_in_exp_intro_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_intro_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_intro_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_intro_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_intro_rec [in LNgen.Fsub_inf]
subst_typ_in_binding_intro_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_intro_rec [in LNgen.Fsub_inf]
subst_typ_in_typ_intro_rec_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_exp_case [in LNgen.Fsub_inf]
subst_exp_in_exp_exp_let [in LNgen.Fsub_inf]
subst_exp_in_exp_exp_tabs [in LNgen.Fsub_inf]
subst_exp_in_exp_exp_abs [in LNgen.Fsub_inf]
subst_typ_in_exp_exp_case [in LNgen.Fsub_inf]
subst_typ_in_exp_exp_let [in LNgen.Fsub_inf]
subst_typ_in_exp_exp_tabs [in LNgen.Fsub_inf]
subst_typ_in_exp_exp_abs [in LNgen.Fsub_inf]
subst_typ_in_typ_typ_all [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_open_exp_wrt_exp [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_open_exp_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_open_exp_wrt_exp [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_open_exp_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_open_binding_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_open_typ_wrt_typ [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec_open_binding_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec_open_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec_open_typ_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec_open_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_subst_exp_in_exp [in LNgen.Fsub_inf]
subst_exp_in_exp_subst_exp_in_exp_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_subst_typ_in_exp [in LNgen.Fsub_inf]
subst_exp_in_exp_subst_typ_in_exp_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_subst_exp_in_exp [in LNgen.Fsub_inf]
subst_typ_in_exp_subst_exp_in_exp_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_subst_typ_in_exp [in LNgen.Fsub_inf]
subst_typ_in_exp_subst_typ_in_exp_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_subst_typ_in_binding [in LNgen.Fsub_inf]
subst_typ_in_binding_subst_typ_in_binding_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_subst_typ_in_typ [in LNgen.Fsub_inf]
subst_typ_in_typ_subst_typ_in_typ_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_spec [in LNgen.Fsub_inf]
subst_typ_in_exp_spec [in LNgen.Fsub_inf]
subst_typ_in_binding_spec [in LNgen.Fsub_inf]
subst_typ_in_typ_spec [in LNgen.Fsub_inf]
subst_exp_in_exp_spec_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_spec_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_spec_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_spec_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_spec_rec [in LNgen.Fsub_inf]
subst_typ_in_binding_spec_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_spec_rec [in LNgen.Fsub_inf]
subst_typ_in_typ_spec_rec_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp_var [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ_var [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp_var [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ_var [in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ_var [in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ_var [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_open_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_binding_open_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_typ_open_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_lc_exp [in LNgen.Fsub_inf]
subst_typ_in_exp_lc_exp [in LNgen.Fsub_inf]
subst_typ_in_binding_lc_binding [in LNgen.Fsub_inf]
subst_typ_in_typ_lc_typ [in LNgen.Fsub_inf]
subst_exp_in_exp_fresh [in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_fresh [in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_fresh [in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_fresh [in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_same [in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_same_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_same [in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_same_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_same [in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_same_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_same [in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_same_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_eq [in LNgen.Fsub_inf]
subst_exp_in_exp_fresh_eq_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_eq [in LNgen.Fsub_inf]
subst_typ_in_exp_fresh_eq_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_eq [in LNgen.Fsub_inf]
subst_typ_in_binding_fresh_eq_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_eq [in LNgen.Fsub_inf]
subst_typ_in_typ_fresh_eq_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_exp [in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_exp_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_typ [in LNgen.Fsub_inf]
subst_exp_in_exp_degree_exp_wrt_typ_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_exp [in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_exp_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_exp_degree_exp_wrt_typ_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_degree_binding_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_binding_degree_binding_wrt_typ_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_degree_typ_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_typ_degree_typ_wrt_typ_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ [in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
subst_exp_in_exp_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_exp_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_exp_close_exp_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_binding_close_binding_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec [in LNgen.Fsub_inf]
subst_typ_in_typ_close_typ_wrt_typ_rec_mutual [in LNgen.Fsub_inf]
subst_ee_expr [in LN.Fsub_Infrastructure]
subst_te_expr [in LN.Fsub_Infrastructure]
subst_tt_type [in LN.Fsub_Infrastructure]
subst_ee_intro [in LN.Fsub_Infrastructure]
subst_ee_intro_rec [in LN.Fsub_Infrastructure]
subst_ee_open_te_var [in LN.Fsub_Infrastructure]
subst_ee_open_te [in LN.Fsub_Infrastructure]
subst_ee_open_te_rec [in LN.Fsub_Infrastructure]
subst_te_open_ee_var [in LN.Fsub_Infrastructure]
subst_te_open_ee [in LN.Fsub_Infrastructure]
subst_te_open_ee_rec [in LN.Fsub_Infrastructure]
subst_ee_open_ee_var [in LN.Fsub_Infrastructure]
subst_ee_open_ee [in LN.Fsub_Infrastructure]
subst_ee_open_ee_rec [in LN.Fsub_Infrastructure]
subst_ee_fresh [in LN.Fsub_Infrastructure]
subst_te_intro [in LN.Fsub_Infrastructure]
subst_te_intro_rec [in LN.Fsub_Infrastructure]
subst_te_open_te_var [in LN.Fsub_Infrastructure]
subst_te_open_te [in LN.Fsub_Infrastructure]
subst_te_open_te_rec [in LN.Fsub_Infrastructure]
subst_te_fresh [in LN.Fsub_Infrastructure]
subst_tt_intro [in LN.Fsub_Infrastructure]
subst_tt_intro_rec [in LN.Fsub_Infrastructure]
subst_tt_open_tt_var [in LN.Fsub_Infrastructure]
subst_tt_open_tt [in LN.Fsub_Infrastructure]
subst_tt_open_tt_rec [in LN.Fsub_Infrastructure]
subst_tt_fresh [in LN.Fsub_Infrastructure]
sub_strengthening [in LN.Fsub_Soundness]
sub_through_subst_tt [in LN.Fsub_Soundness]
sub_narrowing [in LN.Fsub_Soundness]
sub_transitivity [in LN.Fsub_Soundness]
sub_narrowing_aux [in LN.Fsub_Soundness]
sub_weakening [in LN.Fsub_Soundness]
sub_reflexivity [in LN.Fsub_Soundness]
sub_strengthening [in LNgen.Fsub_proofs]
sub_through_subst_typ_in_typ [in LNgen.Fsub_proofs]
sub_narrowing [in LNgen.Fsub_proofs]
sub_transitivity [in LNgen.Fsub_proofs]
sub_narrowing_aux [in LNgen.Fsub_proofs]
sub_weakening [in LNgen.Fsub_proofs]
sub_reflexivity [in LNgen.Fsub_proofs]
sub_regular [in LNgen.Fsub_proofs]
sub_regular [in LN.Fsub_Lemmas]
T
type_from_wf_typ [in LNgen.Fsub_proofs]type_from_wf_typ [in LN.Fsub_Lemmas]
typing_inv_inr [in LN.Fsub_Soundness]
typing_inv_inl [in LN.Fsub_Soundness]
typing_inv_tabs [in LN.Fsub_Soundness]
typing_inv_abs [in LN.Fsub_Soundness]
typing_through_subst_te [in LN.Fsub_Soundness]
typing_through_subst_ee [in LN.Fsub_Soundness]
typing_narrowing [in LN.Fsub_Soundness]
typing_weakening [in LN.Fsub_Soundness]
typing_inv_inr [in LNgen.Fsub_proofs]
typing_inv_inl [in LNgen.Fsub_proofs]
typing_inv_tabs [in LNgen.Fsub_proofs]
typing_inv_abs [in LNgen.Fsub_proofs]
typing_through_subst_typ_in_exp [in LNgen.Fsub_proofs]
typing_through_subst_exp_in_exp [in LNgen.Fsub_proofs]
typing_narrowing [in LNgen.Fsub_proofs]
typing_weakening [in LNgen.Fsub_proofs]
typing_regular [in LNgen.Fsub_proofs]
typing_regular [in LN.Fsub_Lemmas]
U
uniq_from_wf_env [in LNgen.Fsub_proofs]uniq_from_wf_env [in LN.Fsub_Lemmas]
V
value_regular [in LN.Fsub_Lemmas]vector_O_eq [in Metalib.CoqUniquenessTacEx]
W
WDecide_fun.FSetDecideTestCases.test_sweirich [in Metalib.CoqFSetDecide]WDecide_fun.FSetDecideTestCases.test_baydemir_4 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [in Metalib.CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [in Metalib.CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_sweirich [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_4 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [in Metalib.CoqMSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [in Metalib.CoqMSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [in Metalib.CoqMSetDecide]
wf_env_subst_typ_in_binding [in LNgen.Fsub_proofs]
wf_env_strengthening [in LNgen.Fsub_proofs]
wf_env_narrowing [in LNgen.Fsub_proofs]
wf_typ_from_wf_env_sub [in LNgen.Fsub_proofs]
wf_typ_from_wf_env_typ [in LNgen.Fsub_proofs]
wf_typ_from_binds_typ [in LNgen.Fsub_proofs]
wf_typ_open [in LNgen.Fsub_proofs]
wf_typ_subst_typ_in_binding [in LNgen.Fsub_proofs]
wf_typ_strengthening [in LNgen.Fsub_proofs]
wf_typ_narrowing [in LNgen.Fsub_proofs]
wf_typ_weaken_head [in LNgen.Fsub_proofs]
wf_typ_weakening [in LNgen.Fsub_proofs]
wf_env_subst_tb [in LN.Fsub_Lemmas]
wf_env_strengthening [in LN.Fsub_Lemmas]
wf_env_narrowing [in LN.Fsub_Lemmas]
wf_typ_from_wf_env_sub [in LN.Fsub_Lemmas]
wf_typ_from_wf_env_typ [in LN.Fsub_Lemmas]
wf_typ_from_binds_typ [in LN.Fsub_Lemmas]
wf_typ_open [in LN.Fsub_Lemmas]
wf_typ_subst_tb [in LN.Fsub_Lemmas]
wf_typ_strengthening [in LN.Fsub_Lemmas]
wf_typ_narrowing [in LN.Fsub_Lemmas]
wf_typ_weaken_head [in LN.Fsub_Lemmas]
wf_typ_weakening [in LN.Fsub_Lemmas]
WRaw2SetsOn.add_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.cardinal_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.choose_spec2 [in Metalib.CoqMSetInterface]
WRaw2SetsOn.choose_spec1 [in Metalib.CoqMSetInterface]
WRaw2SetsOn.diff_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.elements_spec2w [in Metalib.CoqMSetInterface]
WRaw2SetsOn.elements_spec1 [in Metalib.CoqMSetInterface]
WRaw2SetsOn.empty_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.equal_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.exists_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.filter_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.fold_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.for_all_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.inter_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.is_empty_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.mem_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.partition_spec2 [in Metalib.CoqMSetInterface]
WRaw2SetsOn.partition_spec1 [in Metalib.CoqMSetInterface]
WRaw2SetsOn.remove_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.singleton_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.subset_spec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.union_spec [in Metalib.CoqMSetInterface]
Axiom Index
A
ATOM.atom [in Metalib.MetatheoryAtom]ATOM.atom_fresh_for_list [in Metalib.MetatheoryAtom]
ATOM.eq_dec [in Metalib.MetatheoryAtom]
ATOM.fresh [in Metalib.MetatheoryAtom]
ATOM.fresh_not_in [in Metalib.MetatheoryAtom]
ATOM.nat_of [in Metalib.MetatheoryAtom]
H
HasOrdOps.compare [in Metalib.CoqMSetInterface]HasOrdOps.max_elt [in Metalib.CoqMSetInterface]
HasOrdOps.min_elt [in Metalib.CoqMSetInterface]
HasWOps.add [in Metalib.CoqMSetInterface]
HasWOps.cardinal [in Metalib.CoqMSetInterface]
HasWOps.choose [in Metalib.CoqMSetInterface]
HasWOps.diff [in Metalib.CoqMSetInterface]
HasWOps.elements [in Metalib.CoqMSetInterface]
HasWOps.empty [in Metalib.CoqMSetInterface]
HasWOps.equal [in Metalib.CoqMSetInterface]
HasWOps.exists_ [in Metalib.CoqMSetInterface]
HasWOps.filter [in Metalib.CoqMSetInterface]
HasWOps.fold [in Metalib.CoqMSetInterface]
HasWOps.for_all [in Metalib.CoqMSetInterface]
HasWOps.inter [in Metalib.CoqMSetInterface]
HasWOps.is_empty [in Metalib.CoqMSetInterface]
HasWOps.mem [in Metalib.CoqMSetInterface]
HasWOps.partition [in Metalib.CoqMSetInterface]
HasWOps.remove [in Metalib.CoqMSetInterface]
HasWOps.singleton [in Metalib.CoqMSetInterface]
HasWOps.subset [in Metalib.CoqMSetInterface]
HasWOps.union [in Metalib.CoqMSetInterface]
I
IN.In [in Metalib.CoqMSetInterface]IN.t [in Metalib.CoqMSetInterface]
R
RawSets.choose_spec3 [in Metalib.CoqMSetInterface]RawSets.compare_spec [in Metalib.CoqMSetInterface]
RawSets.elements_spec2 [in Metalib.CoqMSetInterface]
RawSets.max_elt_spec3 [in Metalib.CoqMSetInterface]
RawSets.max_elt_spec2 [in Metalib.CoqMSetInterface]
RawSets.max_elt_spec1 [in Metalib.CoqMSetInterface]
RawSets.min_elt_spec3 [in Metalib.CoqMSetInterface]
RawSets.min_elt_spec2 [in Metalib.CoqMSetInterface]
RawSets.min_elt_spec1 [in Metalib.CoqMSetInterface]
S
Sdep.add [in Metalib.CoqFSetInterface]Sdep.cardinal [in Metalib.CoqFSetInterface]
Sdep.choose [in Metalib.CoqFSetInterface]
Sdep.choose_equal [in Metalib.CoqFSetInterface]
Sdep.compare [in Metalib.CoqFSetInterface]
Sdep.diff [in Metalib.CoqFSetInterface]
Sdep.elements [in Metalib.CoqFSetInterface]
Sdep.empty [in Metalib.CoqFSetInterface]
Sdep.equal [in Metalib.CoqFSetInterface]
Sdep.eq_In [in Metalib.CoqFSetInterface]
Sdep.eq_trans [in Metalib.CoqFSetInterface]
Sdep.eq_sym [in Metalib.CoqFSetInterface]
Sdep.eq_refl [in Metalib.CoqFSetInterface]
Sdep.exists_ [in Metalib.CoqFSetInterface]
Sdep.filter [in Metalib.CoqFSetInterface]
Sdep.fold [in Metalib.CoqFSetInterface]
Sdep.for_all [in Metalib.CoqFSetInterface]
Sdep.In [in Metalib.CoqFSetInterface]
Sdep.inter [in Metalib.CoqFSetInterface]
Sdep.is_empty [in Metalib.CoqFSetInterface]
Sdep.lt [in Metalib.CoqFSetInterface]
Sdep.lt_not_eq [in Metalib.CoqFSetInterface]
Sdep.lt_trans [in Metalib.CoqFSetInterface]
Sdep.max_elt [in Metalib.CoqFSetInterface]
Sdep.mem [in Metalib.CoqFSetInterface]
Sdep.min_elt [in Metalib.CoqFSetInterface]
Sdep.partition [in Metalib.CoqFSetInterface]
Sdep.remove [in Metalib.CoqFSetInterface]
Sdep.singleton [in Metalib.CoqFSetInterface]
Sdep.subset [in Metalib.CoqFSetInterface]
Sdep.t [in Metalib.CoqFSetInterface]
Sdep.union [in Metalib.CoqFSetInterface]
SetsOn.choose_spec3 [in Metalib.CoqMSetInterface]
SetsOn.compare_spec [in Metalib.CoqMSetInterface]
SetsOn.elements_spec2 [in Metalib.CoqMSetInterface]
SetsOn.max_elt_spec3 [in Metalib.CoqMSetInterface]
SetsOn.max_elt_spec2 [in Metalib.CoqMSetInterface]
SetsOn.max_elt_spec1 [in Metalib.CoqMSetInterface]
SetsOn.min_elt_spec3 [in Metalib.CoqMSetInterface]
SetsOn.min_elt_spec2 [in Metalib.CoqMSetInterface]
SetsOn.min_elt_spec1 [in Metalib.CoqMSetInterface]
Sfun.choose_3 [in Metalib.CoqFSetInterface]
Sfun.compare [in Metalib.CoqFSetInterface]
Sfun.elements_3 [in Metalib.CoqFSetInterface]
Sfun.lt [in Metalib.CoqFSetInterface]
Sfun.lt_not_eq [in Metalib.CoqFSetInterface]
Sfun.lt_trans [in Metalib.CoqFSetInterface]
Sfun.max_elt_3 [in Metalib.CoqFSetInterface]
Sfun.max_elt_2 [in Metalib.CoqFSetInterface]
Sfun.max_elt_1 [in Metalib.CoqFSetInterface]
Sfun.max_elt [in Metalib.CoqFSetInterface]
Sfun.min_elt_3 [in Metalib.CoqFSetInterface]
Sfun.min_elt_2 [in Metalib.CoqFSetInterface]
Sfun.min_elt_1 [in Metalib.CoqFSetInterface]
Sfun.min_elt [in Metalib.CoqFSetInterface]
T
TypElt.elt [in Metalib.CoqMSetInterface]TypElt.t [in Metalib.CoqMSetInterface]
W
WOps.t [in Metalib.CoqMSetInterface]WRawSets.add_spec [in Metalib.CoqMSetInterface]
WRawSets.cardinal_spec [in Metalib.CoqMSetInterface]
WRawSets.choose_spec2 [in Metalib.CoqMSetInterface]
WRawSets.choose_spec1 [in Metalib.CoqMSetInterface]
WRawSets.diff_spec [in Metalib.CoqMSetInterface]
WRawSets.elements_spec2w [in Metalib.CoqMSetInterface]
WRawSets.elements_spec1 [in Metalib.CoqMSetInterface]
WRawSets.empty_spec [in Metalib.CoqMSetInterface]
WRawSets.equal_spec [in Metalib.CoqMSetInterface]
WRawSets.exists_spec [in Metalib.CoqMSetInterface]
WRawSets.filter_spec [in Metalib.CoqMSetInterface]
WRawSets.fold_spec [in Metalib.CoqMSetInterface]
WRawSets.for_all_spec [in Metalib.CoqMSetInterface]
WRawSets.In [in Metalib.CoqMSetInterface]
WRawSets.inter_spec [in Metalib.CoqMSetInterface]
WRawSets.isok [in Metalib.CoqMSetInterface]
WRawSets.IsOk [in Metalib.CoqMSetInterface]
WRawSets.is_empty_spec [in Metalib.CoqMSetInterface]
WRawSets.mem_spec [in Metalib.CoqMSetInterface]
WRawSets.partition_spec2 [in Metalib.CoqMSetInterface]
WRawSets.partition_spec1 [in Metalib.CoqMSetInterface]
WRawSets.remove_spec [in Metalib.CoqMSetInterface]
WRawSets.singleton_spec [in Metalib.CoqMSetInterface]
WRawSets.subset_spec [in Metalib.CoqMSetInterface]
WRawSets.union_spec [in Metalib.CoqMSetInterface]
WSetsOn.add_spec [in Metalib.CoqMSetInterface]
WSetsOn.cardinal_spec [in Metalib.CoqMSetInterface]
WSetsOn.choose_spec2 [in Metalib.CoqMSetInterface]
WSetsOn.choose_spec1 [in Metalib.CoqMSetInterface]
WSetsOn.diff_spec [in Metalib.CoqMSetInterface]
WSetsOn.elements_spec2w [in Metalib.CoqMSetInterface]
WSetsOn.elements_spec1 [in Metalib.CoqMSetInterface]
WSetsOn.empty_spec [in Metalib.CoqMSetInterface]
WSetsOn.equal_spec [in Metalib.CoqMSetInterface]
WSetsOn.exists_spec [in Metalib.CoqMSetInterface]
WSetsOn.filter_spec [in Metalib.CoqMSetInterface]
WSetsOn.fold_spec [in Metalib.CoqMSetInterface]
WSetsOn.for_all_spec [in Metalib.CoqMSetInterface]
WSetsOn.In [in Metalib.CoqMSetInterface]
WSetsOn.inter_spec [in Metalib.CoqMSetInterface]
WSetsOn.is_empty_spec [in Metalib.CoqMSetInterface]
WSetsOn.mem_spec [in Metalib.CoqMSetInterface]
WSetsOn.partition_spec2 [in Metalib.CoqMSetInterface]
WSetsOn.partition_spec1 [in Metalib.CoqMSetInterface]
WSetsOn.remove_spec [in Metalib.CoqMSetInterface]
WSetsOn.singleton_spec [in Metalib.CoqMSetInterface]
WSetsOn.subset_spec [in Metalib.CoqMSetInterface]
WSetsOn.union_spec [in Metalib.CoqMSetInterface]
WSfun.add [in Metalib.CoqFSetInterface]
WSfun.add_3 [in Metalib.CoqFSetInterface]
WSfun.add_2 [in Metalib.CoqFSetInterface]
WSfun.add_1 [in Metalib.CoqFSetInterface]
WSfun.cardinal [in Metalib.CoqFSetInterface]
WSfun.cardinal_1 [in Metalib.CoqFSetInterface]
WSfun.choose [in Metalib.CoqFSetInterface]
WSfun.choose_2 [in Metalib.CoqFSetInterface]
WSfun.choose_1 [in Metalib.CoqFSetInterface]
WSfun.diff [in Metalib.CoqFSetInterface]
WSfun.diff_3 [in Metalib.CoqFSetInterface]
WSfun.diff_2 [in Metalib.CoqFSetInterface]
WSfun.diff_1 [in Metalib.CoqFSetInterface]
WSfun.elements [in Metalib.CoqFSetInterface]
WSfun.elements_3w [in Metalib.CoqFSetInterface]
WSfun.elements_2 [in Metalib.CoqFSetInterface]
WSfun.elements_1 [in Metalib.CoqFSetInterface]
WSfun.empty [in Metalib.CoqFSetInterface]
WSfun.empty_1 [in Metalib.CoqFSetInterface]
WSfun.equal [in Metalib.CoqFSetInterface]
WSfun.equal_2 [in Metalib.CoqFSetInterface]
WSfun.equal_1 [in Metalib.CoqFSetInterface]
WSfun.eq_trans [in Metalib.CoqFSetInterface]
WSfun.eq_sym [in Metalib.CoqFSetInterface]
WSfun.eq_refl [in Metalib.CoqFSetInterface]
WSfun.eq_dec [in Metalib.CoqFSetInterface]
WSfun.exists_2 [in Metalib.CoqFSetInterface]
WSfun.exists_1 [in Metalib.CoqFSetInterface]
WSfun.exists_ [in Metalib.CoqFSetInterface]
WSfun.filter [in Metalib.CoqFSetInterface]
WSfun.filter_3 [in Metalib.CoqFSetInterface]
WSfun.filter_2 [in Metalib.CoqFSetInterface]
WSfun.filter_1 [in Metalib.CoqFSetInterface]
WSfun.fold [in Metalib.CoqFSetInterface]
WSfun.fold_1 [in Metalib.CoqFSetInterface]
WSfun.for_all_2 [in Metalib.CoqFSetInterface]
WSfun.for_all_1 [in Metalib.CoqFSetInterface]
WSfun.for_all [in Metalib.CoqFSetInterface]
WSfun.In [in Metalib.CoqFSetInterface]
WSfun.inter [in Metalib.CoqFSetInterface]
WSfun.inter_3 [in Metalib.CoqFSetInterface]
WSfun.inter_2 [in Metalib.CoqFSetInterface]
WSfun.inter_1 [in Metalib.CoqFSetInterface]
WSfun.In_1 [in Metalib.CoqFSetInterface]
WSfun.is_empty_2 [in Metalib.CoqFSetInterface]
WSfun.is_empty_1 [in Metalib.CoqFSetInterface]
WSfun.is_empty [in Metalib.CoqFSetInterface]
WSfun.mem [in Metalib.CoqFSetInterface]
WSfun.mem_2 [in Metalib.CoqFSetInterface]
WSfun.mem_1 [in Metalib.CoqFSetInterface]
WSfun.partition [in Metalib.CoqFSetInterface]
WSfun.partition_2 [in Metalib.CoqFSetInterface]
WSfun.partition_1 [in Metalib.CoqFSetInterface]
WSfun.remove [in Metalib.CoqFSetInterface]
WSfun.remove_3 [in Metalib.CoqFSetInterface]
WSfun.remove_2 [in Metalib.CoqFSetInterface]
WSfun.remove_1 [in Metalib.CoqFSetInterface]
WSfun.singleton [in Metalib.CoqFSetInterface]
WSfun.singleton_2 [in Metalib.CoqFSetInterface]
WSfun.singleton_1 [in Metalib.CoqFSetInterface]
WSfun.subset [in Metalib.CoqFSetInterface]
WSfun.subset_2 [in Metalib.CoqFSetInterface]
WSfun.subset_1 [in Metalib.CoqFSetInterface]
WSfun.t [in Metalib.CoqFSetInterface]
WSfun.union [in Metalib.CoqFSetInterface]
WSfun.union_3 [in Metalib.CoqFSetInterface]
WSfun.union_2 [in Metalib.CoqFSetInterface]
WSfun.union_1 [in Metalib.CoqFSetInterface]
Constructor Index
B
bind_typ [in LNgen.Fsub_ott]bind_sub [in LNgen.Fsub_ott]
bind_typ [in LN.Fsub_Definitions]
bind_sub [in LN.Fsub_Definitions]
D
degree_wrt_exp_exp_case [in LNgen.Fsub_inf]degree_wrt_exp_exp_inr [in LNgen.Fsub_inf]
degree_wrt_exp_exp_inl [in LNgen.Fsub_inf]
degree_wrt_exp_exp_let [in LNgen.Fsub_inf]
degree_wrt_exp_exp_tapp [in LNgen.Fsub_inf]
degree_wrt_exp_exp_tabs [in LNgen.Fsub_inf]
degree_wrt_exp_exp_app [in LNgen.Fsub_inf]
degree_wrt_exp_exp_abs [in LNgen.Fsub_inf]
degree_wrt_exp_exp_var_b [in LNgen.Fsub_inf]
degree_wrt_exp_exp_var_f [in LNgen.Fsub_inf]
degree_wrt_typ_exp_case [in LNgen.Fsub_inf]
degree_wrt_typ_exp_inr [in LNgen.Fsub_inf]
degree_wrt_typ_exp_inl [in LNgen.Fsub_inf]
degree_wrt_typ_exp_let [in LNgen.Fsub_inf]
degree_wrt_typ_exp_tapp [in LNgen.Fsub_inf]
degree_wrt_typ_exp_tabs [in LNgen.Fsub_inf]
degree_wrt_typ_exp_app [in LNgen.Fsub_inf]
degree_wrt_typ_exp_abs [in LNgen.Fsub_inf]
degree_wrt_typ_exp_var_b [in LNgen.Fsub_inf]
degree_wrt_typ_exp_var_f [in LNgen.Fsub_inf]
degree_wrt_typ_bind_typ [in LNgen.Fsub_inf]
degree_wrt_typ_bind_sub [in LNgen.Fsub_inf]
degree_wrt_typ_typ_sum [in LNgen.Fsub_inf]
degree_wrt_typ_typ_all [in LNgen.Fsub_inf]
degree_wrt_typ_typ_arrow [in LNgen.Fsub_inf]
degree_wrt_typ_typ_var_b [in LNgen.Fsub_inf]
degree_wrt_typ_typ_var_f [in LNgen.Fsub_inf]
degree_wrt_typ_typ_top [in LNgen.Fsub_inf]
E
eq_dec [in Metalib.CoqEqDec]expr_case [in LN.Fsub_Definitions]
expr_inr [in LN.Fsub_Definitions]
expr_inl [in LN.Fsub_Definitions]
expr_let [in LN.Fsub_Definitions]
expr_tapp [in LN.Fsub_Definitions]
expr_tabs [in LN.Fsub_Definitions]
expr_app [in LN.Fsub_Definitions]
expr_abs [in LN.Fsub_Definitions]
expr_var [in LN.Fsub_Definitions]
exp_case [in LNgen.Fsub_ott]
exp_inr [in LNgen.Fsub_ott]
exp_inl [in LNgen.Fsub_ott]
exp_let [in LNgen.Fsub_ott]
exp_tapp [in LNgen.Fsub_ott]
exp_tabs [in LNgen.Fsub_ott]
exp_app [in LNgen.Fsub_ott]
exp_abs [in LNgen.Fsub_ott]
exp_var_f [in LNgen.Fsub_ott]
exp_var_b [in LNgen.Fsub_ott]
exp_case [in LN.Fsub_Definitions]
exp_inr [in LN.Fsub_Definitions]
exp_inl [in LN.Fsub_Definitions]
exp_let [in LN.Fsub_Definitions]
exp_tapp [in LN.Fsub_Definitions]
exp_tabs [in LN.Fsub_Definitions]
exp_app [in LN.Fsub_Definitions]
exp_abs [in LN.Fsub_Definitions]
exp_fvar [in LN.Fsub_Definitions]
exp_bvar [in LN.Fsub_Definitions]
L
lc_set_exp_case [in LNgen.Fsub_inf]lc_set_exp_inr [in LNgen.Fsub_inf]
lc_set_exp_inl [in LNgen.Fsub_inf]
lc_set_exp_let [in LNgen.Fsub_inf]
lc_set_exp_tapp [in LNgen.Fsub_inf]
lc_set_exp_tabs [in LNgen.Fsub_inf]
lc_set_exp_app [in LNgen.Fsub_inf]
lc_set_exp_abs [in LNgen.Fsub_inf]
lc_set_exp_var_f [in LNgen.Fsub_inf]
lc_set_bind_typ [in LNgen.Fsub_inf]
lc_set_bind_sub [in LNgen.Fsub_inf]
lc_set_typ_sum [in LNgen.Fsub_inf]
lc_set_typ_all [in LNgen.Fsub_inf]
lc_set_typ_arrow [in LNgen.Fsub_inf]
lc_set_typ_var_f [in LNgen.Fsub_inf]
lc_set_typ_top [in LNgen.Fsub_inf]
lc_exp_case [in LNgen.Fsub_ott]
lc_exp_inr [in LNgen.Fsub_ott]
lc_exp_inl [in LNgen.Fsub_ott]
lc_exp_let [in LNgen.Fsub_ott]
lc_exp_tapp [in LNgen.Fsub_ott]
lc_exp_tabs [in LNgen.Fsub_ott]
lc_exp_app [in LNgen.Fsub_ott]
lc_exp_abs [in LNgen.Fsub_ott]
lc_exp_var_f [in LNgen.Fsub_ott]
lc_bind_typ [in LNgen.Fsub_ott]
lc_bind_sub [in LNgen.Fsub_ott]
lc_typ_sum [in LNgen.Fsub_ott]
lc_typ_all [in LNgen.Fsub_ott]
lc_typ_arrow [in LNgen.Fsub_ott]
lc_typ_var_f [in LNgen.Fsub_ott]
lc_typ_top [in LNgen.Fsub_ott]
M
MakeListOrdering.lt_cons_eq [in Metalib.CoqMSetInterface]MakeListOrdering.lt_cons_lt [in Metalib.CoqMSetInterface]
MakeListOrdering.lt_nil [in Metalib.CoqMSetInterface]
Make.uniq_push [in Metalib.AssocList]
Make.uniq_nil [in Metalib.AssocList]
R
red_case_inr [in LNgen.Fsub_ott]red_case_inl [in LNgen.Fsub_ott]
red_case_1 [in LNgen.Fsub_ott]
red_inr_1 [in LNgen.Fsub_ott]
red_inl_1 [in LNgen.Fsub_ott]
red_let [in LNgen.Fsub_ott]
red_let_1 [in LNgen.Fsub_ott]
red_tabs [in LNgen.Fsub_ott]
red_abs [in LNgen.Fsub_ott]
red_tapp_1 [in LNgen.Fsub_ott]
red_app_2 [in LNgen.Fsub_ott]
red_app_1 [in LNgen.Fsub_ott]
red_case_inr [in LN.Fsub_Definitions]
red_case_inl [in LN.Fsub_Definitions]
red_case_1 [in LN.Fsub_Definitions]
red_inr_1 [in LN.Fsub_Definitions]
red_inl_1 [in LN.Fsub_Definitions]
red_let [in LN.Fsub_Definitions]
red_let_1 [in LN.Fsub_Definitions]
red_tabs [in LN.Fsub_Definitions]
red_abs [in LN.Fsub_Definitions]
red_tapp [in LN.Fsub_Definitions]
red_app_2 [in LN.Fsub_Definitions]
red_app_1 [in LN.Fsub_Definitions]
S
sub_sum [in LNgen.Fsub_ott]sub_all [in LNgen.Fsub_ott]
sub_arrow [in LNgen.Fsub_ott]
sub_trans_tvar [in LNgen.Fsub_ott]
sub_refl_tvar [in LNgen.Fsub_ott]
sub_top [in LNgen.Fsub_ott]
sub_sum [in LN.Fsub_Definitions]
sub_all [in LN.Fsub_Definitions]
sub_arrow [in LN.Fsub_Definitions]
sub_trans_tvar [in LN.Fsub_Definitions]
sub_refl_tvar [in LN.Fsub_Definitions]
sub_top [in LN.Fsub_Definitions]
T
type_sum [in LN.Fsub_Definitions]type_all [in LN.Fsub_Definitions]
type_arrow [in LN.Fsub_Definitions]
type_var [in LN.Fsub_Definitions]
type_top [in LN.Fsub_Definitions]
typing_case [in LNgen.Fsub_ott]
typing_inr [in LNgen.Fsub_ott]
typing_inl [in LNgen.Fsub_ott]
typing_let [in LNgen.Fsub_ott]
typing_sub [in LNgen.Fsub_ott]
typing_tapp [in LNgen.Fsub_ott]
typing_tabs [in LNgen.Fsub_ott]
typing_app [in LNgen.Fsub_ott]
typing_abs [in LNgen.Fsub_ott]
typing_var [in LNgen.Fsub_ott]
typing_case [in LN.Fsub_Definitions]
typing_inr [in LN.Fsub_Definitions]
typing_inl [in LN.Fsub_Definitions]
typing_let [in LN.Fsub_Definitions]
typing_sub [in LN.Fsub_Definitions]
typing_tapp [in LN.Fsub_Definitions]
typing_tabs [in LN.Fsub_Definitions]
typing_app [in LN.Fsub_Definitions]
typing_abs [in LN.Fsub_Definitions]
typing_var [in LN.Fsub_Definitions]
typ_sum [in LNgen.Fsub_ott]
typ_all [in LNgen.Fsub_ott]
typ_arrow [in LNgen.Fsub_ott]
typ_var_f [in LNgen.Fsub_ott]
typ_var_b [in LNgen.Fsub_ott]
typ_top [in LNgen.Fsub_ott]
typ_sum [in LN.Fsub_Definitions]
typ_all [in LN.Fsub_Definitions]
typ_arrow [in LN.Fsub_Definitions]
typ_fvar [in LN.Fsub_Definitions]
typ_bvar [in LN.Fsub_Definitions]
typ_top [in LN.Fsub_Definitions]
V
value_inr [in LN.Fsub_Definitions]value_inl [in LN.Fsub_Definitions]
value_tabs [in LN.Fsub_Definitions]
value_abs [in LN.Fsub_Definitions]
vcons [in Metalib.CoqUniquenessTacEx]
vnil [in Metalib.CoqUniquenessTacEx]
W
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [in Metalib.CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [in Metalib.CoqMSetDecide]
wf_env_typ [in LNgen.Fsub_ott]
wf_env_sub [in LNgen.Fsub_ott]
wf_env_empty [in LNgen.Fsub_ott]
wf_typ_sum [in LNgen.Fsub_ott]
wf_typ_all [in LNgen.Fsub_ott]
wf_typ_arrow [in LNgen.Fsub_ott]
wf_typ_var [in LNgen.Fsub_ott]
wf_typ_top [in LNgen.Fsub_ott]
wf_env_typ [in LN.Fsub_Definitions]
wf_env_sub [in LN.Fsub_Definitions]
wf_env_empty [in LN.Fsub_Definitions]
wf_typ_sum [in LN.Fsub_Definitions]
wf_typ_all [in LN.Fsub_Definitions]
wf_typ_arrow [in LN.Fsub_Definitions]
wf_typ_var [in LN.Fsub_Definitions]
wf_typ_top [in LN.Fsub_Definitions]
WRawSets.ok [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Mkt [in Metalib.CoqMSetInterface]
Inductive Index
B
binding [in LNgen.Fsub_ott]binding [in LN.Fsub_Definitions]
D
degree_exp_wrt_exp [in LNgen.Fsub_inf]degree_exp_wrt_typ [in LNgen.Fsub_inf]
degree_binding_wrt_typ [in LNgen.Fsub_inf]
degree_typ_wrt_typ [in LNgen.Fsub_inf]
E
EqDec_eq [in Metalib.CoqEqDec]exp [in LNgen.Fsub_ott]
exp [in LN.Fsub_Definitions]
expr [in LN.Fsub_Definitions]
L
lc_set_exp [in LNgen.Fsub_inf]lc_set_binding [in LNgen.Fsub_inf]
lc_set_typ [in LNgen.Fsub_inf]
lc_exp [in LNgen.Fsub_ott]
lc_binding [in LNgen.Fsub_ott]
lc_typ [in LNgen.Fsub_ott]
M
MakeListOrdering.lt_list [in Metalib.CoqMSetInterface]Make.uniq [in Metalib.AssocList]
R
red [in LNgen.Fsub_ott]red [in LN.Fsub_Definitions]
S
sub [in LNgen.Fsub_ott]sub [in LN.Fsub_Definitions]
T
typ [in LNgen.Fsub_ott]typ [in LN.Fsub_Definitions]
type [in LN.Fsub_Definitions]
typing [in LNgen.Fsub_ott]
typing [in LN.Fsub_Definitions]
V
value [in LN.Fsub_Definitions]vector [in Metalib.CoqUniquenessTacEx]
W
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [in Metalib.CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [in Metalib.CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [in Metalib.CoqMSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [in Metalib.CoqMSetDecide]
wf_env [in LNgen.Fsub_ott]
wf_typ [in LNgen.Fsub_ott]
wf_env [in LN.Fsub_Definitions]
wf_typ [in LN.Fsub_Definitions]
WRawSets.Ok [in Metalib.CoqMSetInterface]
Projection Index
E
eq_dec [in Metalib.CoqEqDec]W
WRawSets.ok [in Metalib.CoqMSetInterface]WRaw2SetsOn.is_ok [in Metalib.CoqMSetInterface]
WRaw2SetsOn.this [in Metalib.CoqMSetInterface]
Instance Index
E
EqDec_atom [in Metalib.MetatheoryAtom]EqDec_eq_of_EqDec [in Metalib.CoqEqDec]
I
IN.In_compat [in Metalib.CoqMSetInterface]M
MakeListOrdering.eq_equiv [in Metalib.CoqMSetInterface]MakeListOrdering.lt_compat' [in Metalib.CoqMSetInterface]
MakeListOrdering.lt_strorder [in Metalib.CoqMSetInterface]
MakeSetOrdering.eq_equiv [in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_strorder [in Metalib.CoqMSetInterface]
MakeSetOrdering.lt_compat [in Metalib.CoqMSetInterface]
Make.EqDec_eq_of_X [in Metalib.AssocList]
Make.EqDec_of_X [in Metalib.AssocList]
R
Raw2SetsOn.lt_compat [in Metalib.CoqMSetInterface]Raw2SetsOn.lt_strorder [in Metalib.CoqMSetInterface]
W
WRawSets.add_ok [in Metalib.CoqMSetInterface]WRawSets.diff_ok [in Metalib.CoqMSetInterface]
WRawSets.empty_ok [in Metalib.CoqMSetInterface]
WRawSets.eq_equiv [in Metalib.CoqMSetInterface]
WRawSets.filter_ok [in Metalib.CoqMSetInterface]
WRawSets.inter_ok [in Metalib.CoqMSetInterface]
WRawSets.In_compat [in Metalib.CoqMSetInterface]
WRawSets.isok_Ok [in Metalib.CoqMSetInterface]
WRawSets.partition_ok2 [in Metalib.CoqMSetInterface]
WRawSets.partition_ok1 [in Metalib.CoqMSetInterface]
WRawSets.remove_ok [in Metalib.CoqMSetInterface]
WRawSets.singleton_ok [in Metalib.CoqMSetInterface]
WRawSets.union_ok [in Metalib.CoqMSetInterface]
WRaw2SetsOn.eq_equiv [in Metalib.CoqMSetInterface]
WRaw2SetsOn.In_compat [in Metalib.CoqMSetInterface]
WSetsOn.In_compat [in Metalib.CoqMSetInterface]
Section Index
D
DecidableSorting [in Metalib.CoqListFacts]M
Make.AssortedListProperties [in Metalib.AssocList]Make.BindsDerived [in Metalib.AssocList]
Make.BindsProperties [in Metalib.AssocList]
Make.BindsProperties2 [in Metalib.AssocList]
Make.Disjoint [in Metalib.AssocList]
Make.ListProperties [in Metalib.AssocList]
Make.Properties [in Metalib.AssocList]
Make.UniqDerived [in Metalib.AssocList]
Make.UniqMid [in Metalib.AssocList]
Make.UniqProperties [in Metalib.AssocList]
N
Notin_fun.Lemmas [in Metalib.FSetWeakNotin]Notin_fun.Lemmas [in Metalib.MSetWeakNotin]
R
RawSets.Spec [in Metalib.CoqMSetInterface]Raw2SetsOn.Spec [in Metalib.CoqMSetInterface]
S
SetsOn.Spec [in Metalib.CoqMSetInterface]Sfun.Spec [in Metalib.CoqFSetInterface]
SortedListEquality [in Metalib.CoqListFacts]
U
Uniqueness_Of_SetoidList_Proofs [in Metalib.CoqListFacts]Uniqueness_Of_SetoidList_Proofs [in Metalib.CoqUniquenessTacEx]
W
WRawSets.Spec [in Metalib.CoqMSetInterface]WRaw2SetsOn.Spec [in Metalib.CoqMSetInterface]
WSetsOn.Spec [in Metalib.CoqMSetInterface]
WSfun.Spec [in Metalib.CoqFSetInterface]
WSfun.Spec.Filter [in Metalib.CoqFSetInterface]
Abbreviation Index
A
add [in Metalib.Metatheory]atom [in Metalib.MetatheoryAtom]
atoms [in Metalib.MetatheoryAtom]
atom_fresh_for_list [in Metalib.MetatheoryAtom]
B
binds_map [in Metalib.Metatheory]binds_app_r [in Metalib.Metatheory]
binds_app_l [in Metalib.Metatheory]
binds_cons [in Metalib.Metatheory]
binds_one [in Metalib.Metatheory]
E
empty [in Metalib.Metatheory]empty [in LNgen.Fsub_proofs]
empty [in LN.Fsub_Definitions]
env [in LN.Fsub_Definitions]
eq_var [in Metalib.Metatheory]
F
fresh [in Metalib.MetatheoryAtom]fresh_not_in [in Metalib.MetatheoryAtom]
I
Inf [in Metalib.CoqListFacts]M
MakeListOrdering.In [in Metalib.CoqMSetInterface]MakeListOrdering.t [in Metalib.CoqMSetInterface]
N
notin_union [in Metalib.Metatheory]notin_singleton [in Metalib.Metatheory]
notin_add [in Metalib.Metatheory]
notin_empty [in Metalib.Metatheory]
R
remove [in Metalib.Metatheory]S
singleton [in Metalib.Metatheory]Sort [in Metalib.CoqListFacts]
U
union [in Metalib.Metatheory]uniq_map [in Metalib.Metatheory]
uniq_app [in Metalib.Metatheory]
uniq_cons [in Metalib.Metatheory]
uniq_one [in Metalib.Metatheory]
V
var [in Metalib.Metatheory]vars [in Metalib.Metatheory]
W
WRawSets.compatb [in Metalib.CoqMSetInterface]WRaw2SetsOn.compatb [in Metalib.CoqMSetInterface]
WSetsOn.compatb [in Metalib.CoqMSetInterface]
Definition Index
A
apply_tuple [in Metalib.CoqUniquenessTac]arrow [in Metalib.CoqUniquenessTac]
Atom.atom [in Metalib.MetatheoryAtom]
Atom.eq_dec [in Metalib.MetatheoryAtom]
Atom.fresh [in Metalib.MetatheoryAtom]
Atom.nat_of [in Metalib.MetatheoryAtom]
Atom.t [in Metalib.MetatheoryAtom]
ATOM.t [in Metalib.MetatheoryAtom]
B
binding_mutrec [in LNgen.Fsub_inf]binding_rec' [in LNgen.Fsub_inf]
binding_mutind [in LNgen.Fsub_inf]
binding_ind' [in LNgen.Fsub_inf]
body_exp_wrt_exp [in LNgen.Fsub_inf]
body_exp_wrt_typ [in LNgen.Fsub_inf]
body_binding_wrt_typ [in LNgen.Fsub_inf]
body_typ_wrt_typ [in LNgen.Fsub_inf]
body_e [in LN.Fsub_Definitions]
C
close_exp_wrt_exp [in LNgen.Fsub_inf]close_exp_wrt_typ [in LNgen.Fsub_inf]
close_exp_wrt_exp_rec [in LNgen.Fsub_inf]
close_exp_wrt_typ_rec [in LNgen.Fsub_inf]
close_binding_wrt_typ [in LNgen.Fsub_inf]
close_binding_wrt_typ_rec [in LNgen.Fsub_inf]
close_typ_wrt_typ [in LNgen.Fsub_inf]
close_typ_wrt_typ_rec [in LNgen.Fsub_inf]
D
degree_exp_wrt_exp_mutind [in LNgen.Fsub_inf]degree_exp_wrt_exp_ind' [in LNgen.Fsub_inf]
degree_exp_wrt_typ_mutind [in LNgen.Fsub_inf]
degree_exp_wrt_typ_ind' [in LNgen.Fsub_inf]
degree_binding_wrt_typ_mutind [in LNgen.Fsub_inf]
degree_binding_wrt_typ_ind' [in LNgen.Fsub_inf]
degree_typ_wrt_typ_mutind [in LNgen.Fsub_inf]
degree_typ_wrt_typ_ind' [in LNgen.Fsub_inf]
E
env [in LNgen.Fsub_ott]eqlistA_ind' [in Metalib.CoqListFacts]
eqlistA_ind' [in Metalib.CoqUniquenessTacEx]
expvar [in LNgen.Fsub_ott]
exp_mutrec [in LNgen.Fsub_inf]
exp_rec' [in LNgen.Fsub_inf]
exp_mutind [in LNgen.Fsub_inf]
exp_ind' [in LNgen.Fsub_inf]
F
fv_ee [in LN.Fsub_Infrastructure]fv_te [in LN.Fsub_Infrastructure]
fv_tt [in LN.Fsub_Infrastructure]
fv_typ_in_exp [in LNgen.Fsub_ott]
fv_exp_in_exp [in LNgen.Fsub_ott]
fv_typ_in_binding [in LNgen.Fsub_ott]
fv_typ_in_typ [in LNgen.Fsub_ott]
I
IN.Empty [in Metalib.CoqMSetInterface]IN.Equal [in Metalib.CoqMSetInterface]
is_value_of_exp [in LNgen.Fsub_ott]
L
lc_set_exp_mutrec [in LNgen.Fsub_inf]lc_set_exp_rec' [in LNgen.Fsub_inf]
lc_set_exp_mutind [in LNgen.Fsub_inf]
lc_set_exp_ind' [in LNgen.Fsub_inf]
lc_exp_mutind [in LNgen.Fsub_inf]
lc_exp_ind' [in LNgen.Fsub_inf]
lc_set_binding_mutrec [in LNgen.Fsub_inf]
lc_set_binding_rec' [in LNgen.Fsub_inf]
lc_set_binding_mutind [in LNgen.Fsub_inf]
lc_set_binding_ind' [in LNgen.Fsub_inf]
lc_binding_mutind [in LNgen.Fsub_inf]
lc_binding_ind' [in LNgen.Fsub_inf]
lc_set_typ_mutrec [in LNgen.Fsub_inf]
lc_set_typ_rec' [in LNgen.Fsub_inf]
lc_set_typ_mutind [in LNgen.Fsub_inf]
lc_set_typ_ind' [in LNgen.Fsub_inf]
lc_typ_mutind [in LNgen.Fsub_inf]
lc_typ_ind' [in LNgen.Fsub_inf]
lelistA_ind' [in Metalib.CoqListFacts]
lelistA_ind' [in Metalib.CoqUniquenessTacEx]
le_ind' [in Metalib.CoqUniquenessTacEx]
list_rev [in Metalib.CoqUniquenessTac]
lt_ge_dec [in Metalib.LibLNgen]
M
MakeListOrdering.eq [in Metalib.CoqMSetInterface]MakeListOrdering.lt [in Metalib.CoqMSetInterface]
MakeSetOrdering.Above [in Metalib.CoqMSetInterface]
MakeSetOrdering.Add [in Metalib.CoqMSetInterface]
MakeSetOrdering.Below [in Metalib.CoqMSetInterface]
MakeSetOrdering.EmptyBetween [in Metalib.CoqMSetInterface]
MakeSetOrdering.eq [in Metalib.CoqMSetInterface]
MakeSetOrdering.EquivBefore [in Metalib.CoqMSetInterface]
MakeSetOrdering.lt [in Metalib.CoqMSetInterface]
Make.binds [in Metalib.AssocList]
Make.disjoint [in Metalib.FSetExtra]
Make.disjoint [in Metalib.AssocList]
Make.disjoint [in Metalib.MSetExtra]
Make.dom [in Metalib.AssocList]
Make.fresh_list [in Metalib.FSetExtra]
Make.fresh_list [in Metalib.MSetExtra]
Make.get [in Metalib.AssocList]
Make.map [in Metalib.AssocList]
Make.maps [in Metalib.AssocList]
Make.notin [in Metalib.FSetExtra]
Make.notin [in Metalib.MSetExtra]
Make.one [in Metalib.AssocList]
O
open_typ_wrt_typ [in LNgen.Fsub_ott]open_exp_wrt_typ [in LNgen.Fsub_ott]
open_exp_wrt_exp [in LNgen.Fsub_ott]
open_binding_wrt_typ [in LNgen.Fsub_ott]
open_exp_wrt_typ_rec [in LNgen.Fsub_ott]
open_exp_wrt_exp_rec [in LNgen.Fsub_ott]
open_binding_wrt_typ_rec [in LNgen.Fsub_ott]
open_typ_wrt_typ_rec [in LNgen.Fsub_ott]
open_ee [in LN.Fsub_Definitions]
open_te [in LN.Fsub_Definitions]
open_tt [in LN.Fsub_Definitions]
open_ee_rec [in LN.Fsub_Definitions]
open_te_rec [in LN.Fsub_Definitions]
open_tt_rec [in LN.Fsub_Definitions]
R
Raw2SetsOn.compare [in Metalib.CoqMSetInterface]Raw2SetsOn.lt [in Metalib.CoqMSetInterface]
Raw2SetsOn.max_elt [in Metalib.CoqMSetInterface]
Raw2SetsOn.min_elt [in Metalib.CoqMSetInterface]
S
Sdep.Add [in Metalib.CoqFSetInterface]Sdep.elt [in Metalib.CoqFSetInterface]
Sdep.Empty [in Metalib.CoqFSetInterface]
Sdep.eq [in Metalib.CoqFSetInterface]
Sdep.Equal [in Metalib.CoqFSetInterface]
Sdep.Exists [in Metalib.CoqFSetInterface]
Sdep.For_all [in Metalib.CoqFSetInterface]
Sdep.Subset [in Metalib.CoqFSetInterface]
size_exp [in LNgen.Fsub_inf]
size_binding [in LNgen.Fsub_inf]
size_typ [in LNgen.Fsub_inf]
sort_ind' [in Metalib.CoqListFacts]
sort_ind' [in Metalib.CoqUniquenessTacEx]
subst_tb [in LN.Fsub_Infrastructure]
subst_ee [in LN.Fsub_Infrastructure]
subst_te [in LN.Fsub_Infrastructure]
subst_tt [in LN.Fsub_Infrastructure]
subst_typ_in_exp [in LNgen.Fsub_ott]
subst_exp_in_exp [in LNgen.Fsub_ott]
subst_typ_in_binding [in LNgen.Fsub_ott]
subst_typ_in_typ [in LNgen.Fsub_ott]
T
transitivity_on [in LN.Fsub_Soundness]transitivity_on [in LNgen.Fsub_proofs]
tr_tuple_rev [in Metalib.CoqUniquenessTac]
tr_list_rev [in Metalib.CoqUniquenessTac]
tuple [in Metalib.CoqUniquenessTac]
tuple_rev [in Metalib.CoqUniquenessTac]
typvar [in LNgen.Fsub_ott]
typ_mutrec [in LNgen.Fsub_inf]
typ_rec' [in LNgen.Fsub_inf]
typ_mutind [in LNgen.Fsub_inf]
typ_ind' [in LNgen.Fsub_inf]
U
union_map [in Metalib.Metatheory]W
WOps.elt [in Metalib.CoqMSetInterface]WRawSets.Empty [in Metalib.CoqMSetInterface]
WRawSets.eq [in Metalib.CoqMSetInterface]
WRawSets.Equal [in Metalib.CoqMSetInterface]
WRawSets.Exists [in Metalib.CoqMSetInterface]
WRawSets.For_all [in Metalib.CoqMSetInterface]
WRawSets.Subset [in Metalib.CoqMSetInterface]
WRaw2SetsOn.add [in Metalib.CoqMSetInterface]
WRaw2SetsOn.cardinal [in Metalib.CoqMSetInterface]
WRaw2SetsOn.choose [in Metalib.CoqMSetInterface]
WRaw2SetsOn.diff [in Metalib.CoqMSetInterface]
WRaw2SetsOn.elements [in Metalib.CoqMSetInterface]
WRaw2SetsOn.elt [in Metalib.CoqMSetInterface]
WRaw2SetsOn.empty [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Empty [in Metalib.CoqMSetInterface]
WRaw2SetsOn.eq [in Metalib.CoqMSetInterface]
WRaw2SetsOn.equal [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Equal [in Metalib.CoqMSetInterface]
WRaw2SetsOn.eq_dec [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Exists [in Metalib.CoqMSetInterface]
WRaw2SetsOn.exists_ [in Metalib.CoqMSetInterface]
WRaw2SetsOn.filter [in Metalib.CoqMSetInterface]
WRaw2SetsOn.fold [in Metalib.CoqMSetInterface]
WRaw2SetsOn.for_all [in Metalib.CoqMSetInterface]
WRaw2SetsOn.For_all [in Metalib.CoqMSetInterface]
WRaw2SetsOn.In [in Metalib.CoqMSetInterface]
WRaw2SetsOn.inter [in Metalib.CoqMSetInterface]
WRaw2SetsOn.is_empty [in Metalib.CoqMSetInterface]
WRaw2SetsOn.mem [in Metalib.CoqMSetInterface]
WRaw2SetsOn.partition [in Metalib.CoqMSetInterface]
WRaw2SetsOn.remove [in Metalib.CoqMSetInterface]
WRaw2SetsOn.singleton [in Metalib.CoqMSetInterface]
WRaw2SetsOn.subset [in Metalib.CoqMSetInterface]
WRaw2SetsOn.Subset [in Metalib.CoqMSetInterface]
WRaw2SetsOn.t [in Metalib.CoqMSetInterface]
WRaw2SetsOn.union [in Metalib.CoqMSetInterface]
WSetsOn.Empty [in Metalib.CoqMSetInterface]
WSetsOn.eq [in Metalib.CoqMSetInterface]
WSetsOn.Equal [in Metalib.CoqMSetInterface]
WSetsOn.Exists [in Metalib.CoqMSetInterface]
WSetsOn.For_all [in Metalib.CoqMSetInterface]
WSetsOn.Subset [in Metalib.CoqMSetInterface]
WSfun.disjoint [in Metalib.FSetExtra]
WSfun.disjoint [in Metalib.MSetExtra]
WSfun.elt [in Metalib.CoqFSetInterface]
WSfun.Empty [in Metalib.CoqFSetInterface]
WSfun.eq [in Metalib.CoqFSetInterface]
WSfun.Equal [in Metalib.CoqFSetInterface]
WSfun.Exists [in Metalib.CoqFSetInterface]
WSfun.For_all [in Metalib.CoqFSetInterface]
WSfun.fresh_list [in Metalib.FSetExtra]
WSfun.fresh_list [in Metalib.MSetExtra]
WSfun.notin [in Metalib.FSetExtra]
WSfun.notin [in Metalib.MSetExtra]
WSfun.Subset [in Metalib.CoqFSetInterface]
Record Index
E
EqDec_eq [in Metalib.CoqEqDec]W
WRawSets.Ok [in Metalib.CoqMSetInterface]WRaw2SetsOn.t_ [in Metalib.CoqMSetInterface]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1929 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (67 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (141 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (902 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (213 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (222 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (202 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |