| 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 | _ | (282 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 | _ | (123 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 | _ | (106 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 | _ | (18 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 | _ | (32 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 | _ | (3 entries) |
Global Index
B
bind [inductive, in Fsup_Definitions]bind_bound [constructor, in Fsup_Definitions]
bind_typ [constructor, in Fsup_Definitions]
C
canonical_form_abs [lemma, in Fsup_Soundness]canonical_form_tabs [lemma, in Fsup_Soundness]
close_open_subs_rewr_abs_change_vars [lemma, in Fsup_Infrastructure]
close_open_trm_rewr_abs_change_vars [lemma, in Fsup_Infrastructure]
close_open_ts_rec_change_vars [lemma, in Fsup_Infrastructure]
close_open_tt_rec_change_vars [lemma, in Fsup_Infrastructure]
close_var_ee [definition, in Fsup_Definitions]
close_var_ee_rec [definition, in Fsup_Definitions]
close_var_te [definition, in Fsup_Definitions]
close_var_te_rec [definition, in Fsup_Definitions]
close_var_ts [definition, in Fsup_Definitions]
close_var_ts_rec [definition, in Fsup_Definitions]
close_var_tt [definition, in Fsup_Definitions]
close_var_tt_rec [definition, in Fsup_Definitions]
E
env [definition, in Fsup_Definitions]ered [inductive, in Fsup_Definitions]
ered_abs [constructor, in Fsup_Definitions]
ered_app_1 [constructor, in Fsup_Definitions]
ered_app_2 [constructor, in Fsup_Definitions]
ered_beta [constructor, in Fsup_Definitions]
ered_tabs [constructor, in Fsup_Definitions]
ered_tapp [constructor, in Fsup_Definitions]
ered_tapp_comp [constructor, in Fsup_Definitions]
ered_tapp_elim [constructor, in Fsup_Definitions]
ered_tapp_id [constructor, in Fsup_Definitions]
ered_tapp_inner [constructor, in Fsup_Definitions]
ered_tapp_intro [constructor, in Fsup_Definitions]
ered_tapp_outer [constructor, in Fsup_Definitions]
F
Fsup_Definitions [library]Fsup_Infrastructure [library]
Fsup_Soundness [library]
fv_ee [definition, in Fsup_Definitions]
fv_te [definition, in Fsup_Definitions]
fv_ts [definition, in Fsup_Definitions]
fv_tt [definition, in Fsup_Definitions]
I
inst [inductive, in Fsup_Definitions]inst_abs [constructor, in Fsup_Definitions]
inst_bot [constructor, in Fsup_Definitions]
inst_comp [constructor, in Fsup_Definitions]
inst_deterministic [lemma, in Fsup_Soundness]
inst_elim [constructor, in Fsup_Definitions]
inst_id [constructor, in Fsup_Definitions]
inst_inner [constructor, in Fsup_Definitions]
inst_intro [constructor, in Fsup_Definitions]
inst_outer [constructor, in Fsup_Definitions]
inst_regular [lemma, in Fsup_Infrastructure]
inst_strengthening [lemma, in Fsup_Soundness]
inst_through_narrowing [lemma, in Fsup_Soundness]
inst_through_subst_tt [lemma, in Fsup_Soundness]
inst_weakening [lemma, in Fsup_Soundness]
L
level_ee [inductive, in Fsup_Infrastructure]level_ee_abs [constructor, in Fsup_Infrastructure]
level_ee_app [constructor, in Fsup_Infrastructure]
level_ee_bvar [constructor, in Fsup_Infrastructure]
level_ee_fvar [constructor, in Fsup_Infrastructure]
level_ee_of_trm [lemma, in Fsup_Infrastructure]
level_ee_open_ee [lemma, in Fsup_Infrastructure]
level_ee_open_te [lemma, in Fsup_Infrastructure]
level_ee_promote [lemma, in Fsup_Infrastructure]
level_ee_tabs [constructor, in Fsup_Infrastructure]
level_ee_tapp [constructor, in Fsup_Infrastructure]
level_te [inductive, in Fsup_Infrastructure]
level_te_abs [constructor, in Fsup_Infrastructure]
level_te_app [constructor, in Fsup_Infrastructure]
level_te_bvar [constructor, in Fsup_Infrastructure]
level_te_fvar [constructor, in Fsup_Infrastructure]
level_te_of_trm [lemma, in Fsup_Infrastructure]
level_te_open_ee [lemma, in Fsup_Infrastructure]
level_te_open_te [lemma, in Fsup_Infrastructure]
level_te_promote [lemma, in Fsup_Infrastructure]
level_te_tabs [constructor, in Fsup_Infrastructure]
level_te_tapp [constructor, in Fsup_Infrastructure]
level_ts [inductive, in Fsup_Infrastructure]
level_ts_abs [constructor, in Fsup_Infrastructure]
level_ts_bot [constructor, in Fsup_Infrastructure]
level_ts_comp [constructor, in Fsup_Infrastructure]
level_ts_elim [constructor, in Fsup_Infrastructure]
level_ts_id [constructor, in Fsup_Infrastructure]
level_ts_inner [constructor, in Fsup_Infrastructure]
level_ts_intro [constructor, in Fsup_Infrastructure]
level_ts_of_subst [lemma, in Fsup_Infrastructure]
level_ts_open_ts [lemma, in Fsup_Infrastructure]
level_ts_outer [constructor, in Fsup_Infrastructure]
level_ts_promote [lemma, in Fsup_Infrastructure]
level_tt [inductive, in Fsup_Infrastructure]
level_tt_all [constructor, in Fsup_Infrastructure]
level_tt_arrow [constructor, in Fsup_Infrastructure]
level_tt_bot [constructor, in Fsup_Infrastructure]
level_tt_bvar [constructor, in Fsup_Infrastructure]
level_tt_fvar [constructor, in Fsup_Infrastructure]
level_tt_of_type [lemma, in Fsup_Infrastructure]
level_tt_open_tt [lemma, in Fsup_Infrastructure]
level_tt_promote [lemma, in Fsup_Infrastructure]
M
map_subst_tb_id [lemma, in Fsup_Infrastructure]N
notin_fv_ts_open [lemma, in Fsup_Infrastructure]notin_fv_tt_open [lemma, in Fsup_Infrastructure]
notin_fv_wft [lemma, in Fsup_Infrastructure]
O
okt [inductive, in Fsup_Definitions]okt_bound [constructor, in Fsup_Definitions]
okt_empty [constructor, in Fsup_Definitions]
okt_inv [lemma, in Fsup_Infrastructure]
okt_narrow [lemma, in Fsup_Infrastructure]
okt_right_concat [lemma, in Fsup_Infrastructure]
okt_strengthen [lemma, in Fsup_Infrastructure]
okt_subst_tb [lemma, in Fsup_Infrastructure]
okt_typ [constructor, in Fsup_Definitions]
okt_var [constructor, in Fsup_Definitions]
ok_from_okt [lemma, in Fsup_Infrastructure]
open_ee [definition, in Fsup_Definitions]
open_ee_close_ee_inv [lemma, in Fsup_Infrastructure]
open_ee_close_ee_inv_rec [lemma, in Fsup_Infrastructure]
open_ee_rec [definition, in Fsup_Definitions]
open_ee_rec_comm_trm_rewr_abs_f [lemma, in Fsup_Infrastructure]
open_ee_rec_eq [lemma, in Fsup_Infrastructure]
open_ee_rec_term [lemma, in Fsup_Infrastructure]
open_ee_rec_term_core [lemma, in Fsup_Infrastructure]
open_ee_rec_type_core [lemma, in Fsup_Infrastructure]
open_ee_var_comm_trm_rewr_abs_f [lemma, in Fsup_Infrastructure]
open_te [definition, in Fsup_Definitions]
open_te_close_te_inv [lemma, in Fsup_Infrastructure]
open_te_close_te_inv_rec [lemma, in Fsup_Infrastructure]
open_te_rec [definition, in Fsup_Definitions]
open_te_rec_comm_trm_rewr_abs_f [lemma, in Fsup_Infrastructure]
open_te_rec_eq [lemma, in Fsup_Infrastructure]
open_te_rec_term [lemma, in Fsup_Infrastructure]
open_te_rec_term_core [lemma, in Fsup_Infrastructure]
open_te_rec_type_core [lemma, in Fsup_Infrastructure]
open_te_var_comm_trm_rewr_abs_f [lemma, in Fsup_Infrastructure]
open_ts [definition, in Fsup_Definitions]
open_ts_close_ts_inv [lemma, in Fsup_Infrastructure]
open_ts_close_ts_inv_rec [lemma, in Fsup_Infrastructure]
open_ts_rec [definition, in Fsup_Definitions]
open_ts_rec_comm_subs_rewr_abs_f [lemma, in Fsup_Infrastructure]
open_ts_rec_eq [lemma, in Fsup_Infrastructure]
open_ts_rec_type [lemma, in Fsup_Infrastructure]
open_ts_rec_type_core [lemma, in Fsup_Infrastructure]
open_ts_var_comm_subs_rewr_abs_f [lemma, in Fsup_Infrastructure]
open_tt [definition, in Fsup_Definitions]
open_tt_close_tt_inv [lemma, in Fsup_Infrastructure]
open_tt_close_tt_inv_rec [lemma, in Fsup_Infrastructure]
open_tt_rec [definition, in Fsup_Definitions]
open_tt_rec_eq [lemma, in Fsup_Infrastructure]
open_tt_rec_type [lemma, in Fsup_Infrastructure]
open_tt_rec_type_core [lemma, in Fsup_Infrastructure]
P
preservation [definition, in Fsup_Definitions]preservation_result [lemma, in Fsup_Soundness]
progress [lemma, in Fsup_Soundness]
progress [definition, in Fsup_Definitions]
R
red_regular [lemma, in Fsup_Infrastructure]S
subs [inductive, in Fsup_Definitions]subst [inductive, in Fsup_Definitions]
subst_abs [constructor, in Fsup_Definitions]
subst_bot [constructor, in Fsup_Definitions]
subst_comp [constructor, in Fsup_Definitions]
subst_ee [definition, in Fsup_Infrastructure]
subst_ee_fresh [lemma, in Fsup_Infrastructure]
subst_ee_intro [lemma, in Fsup_Infrastructure]
subst_ee_open_ee [lemma, in Fsup_Infrastructure]
subst_ee_open_ee_var [lemma, in Fsup_Infrastructure]
subst_ee_open_te_var [lemma, in Fsup_Infrastructure]
subst_ee_term [lemma, in Fsup_Infrastructure]
subst_elim [constructor, in Fsup_Definitions]
subst_from_wfs [lemma, in Fsup_Infrastructure]
subst_id [constructor, in Fsup_Definitions]
subst_inner [constructor, in Fsup_Definitions]
subst_intro [constructor, in Fsup_Definitions]
subst_open_close_te [lemma, in Fsup_Infrastructure]
subst_open_close_te_rec [lemma, in Fsup_Infrastructure]
subst_open_close_ts_rec [lemma, in Fsup_Infrastructure]
subst_open_close_tt_rec [lemma, in Fsup_Infrastructure]
subst_outer [constructor, in Fsup_Definitions]
subst_tb [definition, in Fsup_Infrastructure]
subst_tb_bound [definition, in Fsup_Infrastructure]
subst_te [definition, in Fsup_Infrastructure]
subst_te_fresh [lemma, in Fsup_Infrastructure]
subst_te_intro [lemma, in Fsup_Infrastructure]
subst_te_open_ee_var [lemma, in Fsup_Infrastructure]
subst_te_open_te [lemma, in Fsup_Infrastructure]
subst_te_open_te_var [lemma, in Fsup_Infrastructure]
subst_te_term [lemma, in Fsup_Infrastructure]
subst_ts [definition, in Fsup_Infrastructure]
subst_ts_fresh [lemma, in Fsup_Infrastructure]
subst_ts_open_tt [lemma, in Fsup_Infrastructure]
subst_ts_open_tt_rec [lemma, in Fsup_Infrastructure]
subst_ts_open_tt_var [lemma, in Fsup_Infrastructure]
subst_ts_type [lemma, in Fsup_Infrastructure]
subst_tt [definition, in Fsup_Infrastructure]
subst_tt_fresh [lemma, in Fsup_Infrastructure]
subst_tt_intro [lemma, in Fsup_Infrastructure]
subst_tt_open_tt [lemma, in Fsup_Infrastructure]
subst_tt_open_tt_rec [lemma, in Fsup_Infrastructure]
subst_tt_open_tt_var [lemma, in Fsup_Infrastructure]
subst_tt_type [lemma, in Fsup_Infrastructure]
subs_abs [constructor, in Fsup_Definitions]
subs_bot [constructor, in Fsup_Definitions]
subs_comp [constructor, in Fsup_Definitions]
subs_elim [constructor, in Fsup_Definitions]
subs_id [constructor, in Fsup_Definitions]
subs_inner [constructor, in Fsup_Definitions]
subs_intro [constructor, in Fsup_Definitions]
subs_outer [constructor, in Fsup_Definitions]
subs_rewr_abs_f [definition, in Fsup_Definitions]
subs_rewr_abs_f_regular [lemma, in Fsup_Infrastructure]
T
term [inductive, in Fsup_Definitions]term_abs [constructor, in Fsup_Definitions]
term_app [constructor, in Fsup_Definitions]
term_tabs [constructor, in Fsup_Definitions]
term_tapp [constructor, in Fsup_Definitions]
term_var [constructor, in Fsup_Definitions]
trm [inductive, in Fsup_Definitions]
trm_abs [constructor, in Fsup_Definitions]
trm_app [constructor, in Fsup_Definitions]
trm_bvar [constructor, in Fsup_Definitions]
trm_fvar [constructor, in Fsup_Definitions]
trm_rewr_abs [definition, in Fsup_Definitions]
trm_rewr_abs_change_vars [lemma, in Fsup_Infrastructure]
trm_rewr_abs_f [definition, in Fsup_Definitions]
trm_rewr_abs_f_regular [lemma, in Fsup_Infrastructure]
trm_rewr_abs_regular [lemma, in Fsup_Infrastructure]
trm_tabs [constructor, in Fsup_Definitions]
trm_tapp [constructor, in Fsup_Definitions]
typ [inductive, in Fsup_Definitions]
type [inductive, in Fsup_Definitions]
type_all [constructor, in Fsup_Definitions]
type_arrow [constructor, in Fsup_Definitions]
type_bot [constructor, in Fsup_Definitions]
type_from_wft [lemma, in Fsup_Infrastructure]
type_var [constructor, in Fsup_Definitions]
typing [inductive, in Fsup_Definitions]
typing_abs [constructor, in Fsup_Definitions]
typing_app [constructor, in Fsup_Definitions]
typing_deterministic [lemma, in Fsup_Soundness]
typing_regular [lemma, in Fsup_Infrastructure]
typing_tabs [constructor, in Fsup_Definitions]
typing_tapp [constructor, in Fsup_Definitions]
typing_through_narrowing [lemma, in Fsup_Soundness]
typing_through_subst_ee [lemma, in Fsup_Soundness]
typing_through_subst_te [lemma, in Fsup_Soundness]
typing_var [constructor, in Fsup_Definitions]
typing_weakening [lemma, in Fsup_Soundness]
typ_all [constructor, in Fsup_Definitions]
typ_arrow [constructor, in Fsup_Definitions]
typ_bot [constructor, in Fsup_Definitions]
typ_bvar [constructor, in Fsup_Definitions]
typ_fvar [constructor, in Fsup_Definitions]
V
value [inductive, in Fsup_Definitions]value_abs [constructor, in Fsup_Definitions]
value_regular [lemma, in Fsup_Infrastructure]
value_tabs [constructor, in Fsup_Definitions]
W
wfs [inductive, in Fsup_Definitions]wfs_abs [constructor, in Fsup_Definitions]
wfs_bot [constructor, in Fsup_Definitions]
wfs_comp [constructor, in Fsup_Definitions]
wfs_forget_bind_bound [lemma, in Fsup_Infrastructure]
wfs_inner [constructor, in Fsup_Definitions]
wfs_learn_bind_bound [lemma, in Fsup_Infrastructure]
wfs_narrow [lemma, in Fsup_Infrastructure]
wfs_outer [constructor, in Fsup_Definitions]
wfs_weaken [lemma, in Fsup_Infrastructure]
wft [inductive, in Fsup_Definitions]
wft_all [constructor, in Fsup_Definitions]
wft_arrow [constructor, in Fsup_Definitions]
wft_bot [constructor, in Fsup_Definitions]
wft_forget_bind_bound [lemma, in Fsup_Infrastructure]
wft_from_env_has_sub [lemma, in Fsup_Infrastructure]
wft_from_env_has_typ [lemma, in Fsup_Infrastructure]
wft_from_okt_sub [lemma, in Fsup_Infrastructure]
wft_from_okt_typ [lemma, in Fsup_Infrastructure]
wft_learn_bind_bound [lemma, in Fsup_Infrastructure]
wft_narrow [lemma, in Fsup_Infrastructure]
wft_open [lemma, in Fsup_Infrastructure]
wft_strengthen [lemma, in Fsup_Infrastructure]
wft_subst_tb [lemma, in Fsup_Infrastructure]
wft_var [constructor, in Fsup_Definitions]
wft_weaken [lemma, in Fsup_Infrastructure]
wft_weaken_right [lemma, in Fsup_Infrastructure]
wsg_elim [constructor, in Fsup_Definitions]
wsg_id [constructor, in Fsup_Definitions]
wsg_intro [constructor, in Fsup_Definitions]
Lemma Index
C
canonical_form_abs [in Fsup_Soundness]canonical_form_tabs [in Fsup_Soundness]
close_open_subs_rewr_abs_change_vars [in Fsup_Infrastructure]
close_open_trm_rewr_abs_change_vars [in Fsup_Infrastructure]
close_open_ts_rec_change_vars [in Fsup_Infrastructure]
close_open_tt_rec_change_vars [in Fsup_Infrastructure]
I
inst_deterministic [in Fsup_Soundness]inst_regular [in Fsup_Infrastructure]
inst_strengthening [in Fsup_Soundness]
inst_through_narrowing [in Fsup_Soundness]
inst_through_subst_tt [in Fsup_Soundness]
inst_weakening [in Fsup_Soundness]
L
level_ee_of_trm [in Fsup_Infrastructure]level_ee_open_ee [in Fsup_Infrastructure]
level_ee_open_te [in Fsup_Infrastructure]
level_ee_promote [in Fsup_Infrastructure]
level_te_of_trm [in Fsup_Infrastructure]
level_te_open_ee [in Fsup_Infrastructure]
level_te_open_te [in Fsup_Infrastructure]
level_te_promote [in Fsup_Infrastructure]
level_ts_of_subst [in Fsup_Infrastructure]
level_ts_open_ts [in Fsup_Infrastructure]
level_ts_promote [in Fsup_Infrastructure]
level_tt_of_type [in Fsup_Infrastructure]
level_tt_open_tt [in Fsup_Infrastructure]
level_tt_promote [in Fsup_Infrastructure]
M
map_subst_tb_id [in Fsup_Infrastructure]N
notin_fv_ts_open [in Fsup_Infrastructure]notin_fv_tt_open [in Fsup_Infrastructure]
notin_fv_wft [in Fsup_Infrastructure]
O
okt_inv [in Fsup_Infrastructure]okt_narrow [in Fsup_Infrastructure]
okt_right_concat [in Fsup_Infrastructure]
okt_strengthen [in Fsup_Infrastructure]
okt_subst_tb [in Fsup_Infrastructure]
ok_from_okt [in Fsup_Infrastructure]
open_ee_close_ee_inv [in Fsup_Infrastructure]
open_ee_close_ee_inv_rec [in Fsup_Infrastructure]
open_ee_rec_comm_trm_rewr_abs_f [in Fsup_Infrastructure]
open_ee_rec_eq [in Fsup_Infrastructure]
open_ee_rec_term [in Fsup_Infrastructure]
open_ee_rec_term_core [in Fsup_Infrastructure]
open_ee_rec_type_core [in Fsup_Infrastructure]
open_ee_var_comm_trm_rewr_abs_f [in Fsup_Infrastructure]
open_te_close_te_inv [in Fsup_Infrastructure]
open_te_close_te_inv_rec [in Fsup_Infrastructure]
open_te_rec_comm_trm_rewr_abs_f [in Fsup_Infrastructure]
open_te_rec_eq [in Fsup_Infrastructure]
open_te_rec_term [in Fsup_Infrastructure]
open_te_rec_term_core [in Fsup_Infrastructure]
open_te_rec_type_core [in Fsup_Infrastructure]
open_te_var_comm_trm_rewr_abs_f [in Fsup_Infrastructure]
open_ts_close_ts_inv [in Fsup_Infrastructure]
open_ts_close_ts_inv_rec [in Fsup_Infrastructure]
open_ts_rec_comm_subs_rewr_abs_f [in Fsup_Infrastructure]
open_ts_rec_eq [in Fsup_Infrastructure]
open_ts_rec_type [in Fsup_Infrastructure]
open_ts_rec_type_core [in Fsup_Infrastructure]
open_ts_var_comm_subs_rewr_abs_f [in Fsup_Infrastructure]
open_tt_close_tt_inv [in Fsup_Infrastructure]
open_tt_close_tt_inv_rec [in Fsup_Infrastructure]
open_tt_rec_eq [in Fsup_Infrastructure]
open_tt_rec_type [in Fsup_Infrastructure]
open_tt_rec_type_core [in Fsup_Infrastructure]
P
preservation_result [in Fsup_Soundness]progress [in Fsup_Soundness]
R
red_regular [in Fsup_Infrastructure]S
subst_ee_fresh [in Fsup_Infrastructure]subst_ee_intro [in Fsup_Infrastructure]
subst_ee_open_ee [in Fsup_Infrastructure]
subst_ee_open_ee_var [in Fsup_Infrastructure]
subst_ee_open_te_var [in Fsup_Infrastructure]
subst_ee_term [in Fsup_Infrastructure]
subst_from_wfs [in Fsup_Infrastructure]
subst_open_close_te [in Fsup_Infrastructure]
subst_open_close_te_rec [in Fsup_Infrastructure]
subst_open_close_ts_rec [in Fsup_Infrastructure]
subst_open_close_tt_rec [in Fsup_Infrastructure]
subst_te_fresh [in Fsup_Infrastructure]
subst_te_intro [in Fsup_Infrastructure]
subst_te_open_ee_var [in Fsup_Infrastructure]
subst_te_open_te [in Fsup_Infrastructure]
subst_te_open_te_var [in Fsup_Infrastructure]
subst_te_term [in Fsup_Infrastructure]
subst_ts_fresh [in Fsup_Infrastructure]
subst_ts_open_tt [in Fsup_Infrastructure]
subst_ts_open_tt_rec [in Fsup_Infrastructure]
subst_ts_open_tt_var [in Fsup_Infrastructure]
subst_ts_type [in Fsup_Infrastructure]
subst_tt_fresh [in Fsup_Infrastructure]
subst_tt_intro [in Fsup_Infrastructure]
subst_tt_open_tt [in Fsup_Infrastructure]
subst_tt_open_tt_rec [in Fsup_Infrastructure]
subst_tt_open_tt_var [in Fsup_Infrastructure]
subst_tt_type [in Fsup_Infrastructure]
subs_rewr_abs_f_regular [in Fsup_Infrastructure]
T
trm_rewr_abs_change_vars [in Fsup_Infrastructure]trm_rewr_abs_f_regular [in Fsup_Infrastructure]
trm_rewr_abs_regular [in Fsup_Infrastructure]
type_from_wft [in Fsup_Infrastructure]
typing_deterministic [in Fsup_Soundness]
typing_regular [in Fsup_Infrastructure]
typing_through_narrowing [in Fsup_Soundness]
typing_through_subst_ee [in Fsup_Soundness]
typing_through_subst_te [in Fsup_Soundness]
typing_weakening [in Fsup_Soundness]
V
value_regular [in Fsup_Infrastructure]W
wfs_forget_bind_bound [in Fsup_Infrastructure]wfs_learn_bind_bound [in Fsup_Infrastructure]
wfs_narrow [in Fsup_Infrastructure]
wfs_weaken [in Fsup_Infrastructure]
wft_forget_bind_bound [in Fsup_Infrastructure]
wft_from_env_has_sub [in Fsup_Infrastructure]
wft_from_env_has_typ [in Fsup_Infrastructure]
wft_from_okt_sub [in Fsup_Infrastructure]
wft_from_okt_typ [in Fsup_Infrastructure]
wft_learn_bind_bound [in Fsup_Infrastructure]
wft_narrow [in Fsup_Infrastructure]
wft_open [in Fsup_Infrastructure]
wft_strengthen [in Fsup_Infrastructure]
wft_subst_tb [in Fsup_Infrastructure]
wft_weaken [in Fsup_Infrastructure]
wft_weaken_right [in Fsup_Infrastructure]
Constructor Index
B
bind_bound [in Fsup_Definitions]bind_typ [in Fsup_Definitions]
E
ered_abs [in Fsup_Definitions]ered_app_1 [in Fsup_Definitions]
ered_app_2 [in Fsup_Definitions]
ered_beta [in Fsup_Definitions]
ered_tabs [in Fsup_Definitions]
ered_tapp [in Fsup_Definitions]
ered_tapp_comp [in Fsup_Definitions]
ered_tapp_elim [in Fsup_Definitions]
ered_tapp_id [in Fsup_Definitions]
ered_tapp_inner [in Fsup_Definitions]
ered_tapp_intro [in Fsup_Definitions]
ered_tapp_outer [in Fsup_Definitions]
I
inst_abs [in Fsup_Definitions]inst_bot [in Fsup_Definitions]
inst_comp [in Fsup_Definitions]
inst_elim [in Fsup_Definitions]
inst_id [in Fsup_Definitions]
inst_inner [in Fsup_Definitions]
inst_intro [in Fsup_Definitions]
inst_outer [in Fsup_Definitions]
L
level_ee_abs [in Fsup_Infrastructure]level_ee_app [in Fsup_Infrastructure]
level_ee_bvar [in Fsup_Infrastructure]
level_ee_fvar [in Fsup_Infrastructure]
level_ee_tabs [in Fsup_Infrastructure]
level_ee_tapp [in Fsup_Infrastructure]
level_te_abs [in Fsup_Infrastructure]
level_te_app [in Fsup_Infrastructure]
level_te_bvar [in Fsup_Infrastructure]
level_te_fvar [in Fsup_Infrastructure]
level_te_tabs [in Fsup_Infrastructure]
level_te_tapp [in Fsup_Infrastructure]
level_ts_abs [in Fsup_Infrastructure]
level_ts_bot [in Fsup_Infrastructure]
level_ts_comp [in Fsup_Infrastructure]
level_ts_elim [in Fsup_Infrastructure]
level_ts_id [in Fsup_Infrastructure]
level_ts_inner [in Fsup_Infrastructure]
level_ts_intro [in Fsup_Infrastructure]
level_ts_outer [in Fsup_Infrastructure]
level_tt_all [in Fsup_Infrastructure]
level_tt_arrow [in Fsup_Infrastructure]
level_tt_bot [in Fsup_Infrastructure]
level_tt_bvar [in Fsup_Infrastructure]
level_tt_fvar [in Fsup_Infrastructure]
O
okt_bound [in Fsup_Definitions]okt_empty [in Fsup_Definitions]
okt_typ [in Fsup_Definitions]
okt_var [in Fsup_Definitions]
S
subst_abs [in Fsup_Definitions]subst_bot [in Fsup_Definitions]
subst_comp [in Fsup_Definitions]
subst_elim [in Fsup_Definitions]
subst_id [in Fsup_Definitions]
subst_inner [in Fsup_Definitions]
subst_intro [in Fsup_Definitions]
subst_outer [in Fsup_Definitions]
subs_abs [in Fsup_Definitions]
subs_bot [in Fsup_Definitions]
subs_comp [in Fsup_Definitions]
subs_elim [in Fsup_Definitions]
subs_id [in Fsup_Definitions]
subs_inner [in Fsup_Definitions]
subs_intro [in Fsup_Definitions]
subs_outer [in Fsup_Definitions]
T
term_abs [in Fsup_Definitions]term_app [in Fsup_Definitions]
term_tabs [in Fsup_Definitions]
term_tapp [in Fsup_Definitions]
term_var [in Fsup_Definitions]
trm_abs [in Fsup_Definitions]
trm_app [in Fsup_Definitions]
trm_bvar [in Fsup_Definitions]
trm_fvar [in Fsup_Definitions]
trm_tabs [in Fsup_Definitions]
trm_tapp [in Fsup_Definitions]
type_all [in Fsup_Definitions]
type_arrow [in Fsup_Definitions]
type_bot [in Fsup_Definitions]
type_var [in Fsup_Definitions]
typing_abs [in Fsup_Definitions]
typing_app [in Fsup_Definitions]
typing_tabs [in Fsup_Definitions]
typing_tapp [in Fsup_Definitions]
typing_var [in Fsup_Definitions]
typ_all [in Fsup_Definitions]
typ_arrow [in Fsup_Definitions]
typ_bot [in Fsup_Definitions]
typ_bvar [in Fsup_Definitions]
typ_fvar [in Fsup_Definitions]
V
value_abs [in Fsup_Definitions]value_tabs [in Fsup_Definitions]
W
wfs_abs [in Fsup_Definitions]wfs_bot [in Fsup_Definitions]
wfs_comp [in Fsup_Definitions]
wfs_inner [in Fsup_Definitions]
wfs_outer [in Fsup_Definitions]
wft_all [in Fsup_Definitions]
wft_arrow [in Fsup_Definitions]
wft_bot [in Fsup_Definitions]
wft_var [in Fsup_Definitions]
wsg_elim [in Fsup_Definitions]
wsg_id [in Fsup_Definitions]
wsg_intro [in Fsup_Definitions]
Inductive Index
B
bind [in Fsup_Definitions]E
ered [in Fsup_Definitions]I
inst [in Fsup_Definitions]L
level_ee [in Fsup_Infrastructure]level_te [in Fsup_Infrastructure]
level_ts [in Fsup_Infrastructure]
level_tt [in Fsup_Infrastructure]
O
okt [in Fsup_Definitions]S
subs [in Fsup_Definitions]subst [in Fsup_Definitions]
T
term [in Fsup_Definitions]trm [in Fsup_Definitions]
typ [in Fsup_Definitions]
type [in Fsup_Definitions]
typing [in Fsup_Definitions]
V
value [in Fsup_Definitions]W
wfs [in Fsup_Definitions]wft [in Fsup_Definitions]
Definition Index
C
close_var_ee [in Fsup_Definitions]close_var_ee_rec [in Fsup_Definitions]
close_var_te [in Fsup_Definitions]
close_var_te_rec [in Fsup_Definitions]
close_var_ts [in Fsup_Definitions]
close_var_ts_rec [in Fsup_Definitions]
close_var_tt [in Fsup_Definitions]
close_var_tt_rec [in Fsup_Definitions]
E
env [in Fsup_Definitions]F
fv_ee [in Fsup_Definitions]fv_te [in Fsup_Definitions]
fv_ts [in Fsup_Definitions]
fv_tt [in Fsup_Definitions]
O
open_ee [in Fsup_Definitions]open_ee_rec [in Fsup_Definitions]
open_te [in Fsup_Definitions]
open_te_rec [in Fsup_Definitions]
open_ts [in Fsup_Definitions]
open_ts_rec [in Fsup_Definitions]
open_tt [in Fsup_Definitions]
open_tt_rec [in Fsup_Definitions]
P
preservation [in Fsup_Definitions]progress [in Fsup_Definitions]
S
subst_ee [in Fsup_Infrastructure]subst_tb [in Fsup_Infrastructure]
subst_tb_bound [in Fsup_Infrastructure]
subst_te [in Fsup_Infrastructure]
subst_ts [in Fsup_Infrastructure]
subst_tt [in Fsup_Infrastructure]
subs_rewr_abs_f [in Fsup_Definitions]
T
trm_rewr_abs [in Fsup_Definitions]trm_rewr_abs_f [in Fsup_Definitions]
Library Index
F
Fsup_DefinitionsFsup_Infrastructure
Fsup_Soundness
| 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 | _ | (282 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 | _ | (123 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 | _ | (106 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 | _ | (18 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 | _ | (32 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 | _ | (3 entries) |
This page has been generated by coqdoc