| 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 |
_ |
(471 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 |
_ |
(56 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 |
_ |
(298 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(29 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 |
_ |
(13 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 |
_ |
(53 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 |
_ |
(9 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 |
_ |
(13 entries) |
Global Index
A
abs [definition, in STLCImpl]
abs_eq [lemma, in STLCImpl]
abs_inst_inv [lemma, in STLCImpl]
abs_neq [lemma, in STLCImpl]
abs_value [constructor, in UseSTLC]
add_add [lemma, in ExtFset]
add_add_incl [lemma, in ExtFset]
add_elim_1 [lemma, in ExtFset]
add_elim_2 [lemma, in ExtFset]
add_neg_elim_1 [lemma, in ExtFset]
add_neg_elim_2 [lemma, in ExtFset]
add_neg_intro [lemma, in ExtFset]
add_union [lemma, in ExtFset]
app [definition, in STLCImpl]
app [axiom, in STLC]
application_fresh [lemma, in Support]
application_supports [lemma, in Support]
arrow [constructor, in STLC]
arrow [constructor, in STLCImpl]
AtomImplementation [module, in Atoms]
AtomImplementationSig [module, in Atoms]
Atoms [library]
AtomT [inductive, in Atoms]
atom_eqdec_contract [lemma, in Atoms]
atom_eqdec_eq [lemma, in Atoms]
atom_eqdec_neq [lemma, in Atoms]
atom_swap_left [lemma, in Swaps]
atom_swap_left' [lemma, in Swaps]
atom_swap_neither [lemma, in Swaps]
atom_swap_right [lemma, in Swaps]
atom_swap_right' [lemma, in Swaps]
AuxLib [library]
Axioms [library]
C
cbv [inductive, in UseSTLC]
cbv_beta [constructor, in UseSTLC]
cbv_deterministic [lemma, in UseSTLC]
cbv_equivariant [lemma, in UseSTLC]
cbv_left [constructor, in UseSTLC]
cbv_right [constructor, in UseSTLC]
D
diff_empty_1 [lemma, in ExtFset]
diff_empty_2 [lemma, in ExtFset]
diff_neg_elim [lemma, in ExtFset]
diff_neg_elim_1 [lemma, in ExtFset]
diff_neg_elim_2 [lemma, in ExtFset]
diff_neg_intro_1 [lemma, in ExtFset]
diff_neg_intro_2 [lemma, in ExtFset]
distinctness_app_dot [axiom, in STLC]
distinctness_app_dot [lemma, in STLCImpl]
distinctness_app_lam [axiom, in STLC]
distinctness_app_lam [lemma, in STLCImpl]
distinctness_app_var [lemma, in STLCImpl]
distinctness_app_var [axiom, in STLC]
distinctness_dot_app [lemma, in STLCImpl]
distinctness_dot_app [axiom, in STLC]
distinctness_dot_lam [axiom, in STLC]
distinctness_dot_lam [lemma, in STLCImpl]
distinctness_dot_var [lemma, in STLCImpl]
distinctness_dot_var [axiom, in STLC]
distinctness_lam_app [axiom, in STLC]
distinctness_lam_app [lemma, in STLCImpl]
distinctness_lam_dot [axiom, in STLC]
distinctness_lam_dot [lemma, in STLCImpl]
distinctness_lam_var [axiom, in STLC]
distinctness_lam_var [lemma, in STLCImpl]
distinctness_var_app [axiom, in STLC]
distinctness_var_app [lemma, in STLCImpl]
distinctness_var_dot [axiom, in STLC]
distinctness_var_dot [lemma, in STLCImpl]
distinctness_var_lam [lemma, in STLCImpl]
distinctness_var_lam [axiom, in STLC]
dot [axiom, in STLC]
dot [definition, in STLCImpl]
E
elements_empty [lemma, in ExtFset]
empty_elim [lemma, in ExtFset]
eq_lam [lemma, in STLCImpl]
eq_lam [axiom, in STLC]
eq_lam_diff [lemma, in STLCImpl]
ExtFset [inductive, in ExtFset]
ExtFset [library]
ExtFsetImpl [library]
ExtFsetImplementation [module, in ExtFsetImpl]
ExtFsetSig [module, in ExtFsetImpl]
F
finite_nat_list_max [lemma, in AuxLib]
finite_nat_list_max' [lemma, in AuxLib]
fresh [definition, in Support]
freshP [definition, in Psets]
freshP_application [lemma, in Psets]
freshP_atom [lemma, in Psets]
freshP_from_supports [lemma, in Psets]
fresh_atom_from_neq [lemma, in Support]
function_constancy_v1 [lemma, in Psets]
function_constancy_v1 [lemma, in Support]
function_constancy_v2 [lemma, in Support]
function_constancy_v2 [lemma, in Psets]
function_supports [lemma, in Support]
func_swap [definition, in Swaps]
func_swap_distrib [lemma, in Swaps]
func_swap_invol [lemma, in Swaps]
func_swap_same [lemma, in Swaps]
fun_extensionality [axiom, in Axioms]
fvar [axiom, in STLC]
fvar [definition, in STLCImpl]
fvar_app [axiom, in STLC]
fvar_app [lemma, in STLCImpl]
fvar_dot [axiom, in STLC]
fvar_dot [lemma, in STLCImpl]
fvar_lam [axiom, in STLC]
fvar_lam [lemma, in STLCImpl]
fvar_subst [lemma, in UseSTLC]
fvar_swap [lemma, in UseSTLC]
fvar_var [axiom, in STLC]
fvar_var [lemma, in STLCImpl]
I
id_swap [definition, in Swaps]
id_swap_distrib [lemma, in Swaps]
id_swap_invol [lemma, in Swaps]
id_swap_reduce [lemma, in Swaps]
id_swap_same [lemma, in Swaps]
injection_app_arg [lemma, in STLCImpl]
injection_app_arg [axiom, in STLC]
injection_app_fun [axiom, in STLC]
injection_app_fun [lemma, in STLCImpl]
injection_lam_body [lemma, in STLCImpl]
injection_lam_body [axiom, in STLC]
injection_lam_ty [axiom, in STLC]
injection_lam_ty [lemma, in STLCImpl]
injection_papp_arg [lemma, in STLCImpl]
injection_papp_fun [lemma, in STLCImpl]
injection_plam [lemma, in STLCImpl]
injection_var [lemma, in STLCImpl]
injection_var [axiom, in STLC]
inst [definition, in STLCImpl]
inst_abs_inv [lemma, in STLCImpl]
inst_aux [definition, in STLCImpl]
inst_papp [lemma, in STLCImpl]
inst_plam [lemma, in STLCImpl]
intersection_empty_1 [lemma, in ExtFset]
intersection_empty_2 [lemma, in ExtFset]
intersection_neg_elim [lemma, in ExtFset]
intersection_neg_elim_1 [lemma, in ExtFset]
intersection_neg_elim_2 [lemma, in ExtFset]
intersection_neg_intro_1 [lemma, in ExtFset]
intersection_neg_intro_2 [lemma, in ExtFset]
intersection_supports [lemma, in Psets]
K
K [constructor, in UseSTLC]
K_equivariant [lemma, in UseSTLC]
L
lam [axiom, in STLC]
lam [definition, in STLCImpl]
le_lt_S [lemma, in AuxLib]
list_not_in_cons_l [lemma, in AuxLib]
list_swap [definition, in Swaps]
list_swap_distrib [lemma, in Swaps]
list_swap_In [lemma, in Swaps]
list_swap_invol [lemma, in Swaps]
list_swap_same [lemma, in Swaps]
lt_Sn_n [lemma, in AuxLib]
M
MakeSTLC [module, in STLCImpl]
map_compose [lemma, in ExtFset]
max_lt_l [lemma, in AuxLib]
max_lt_r [lemma, in AuxLib]
mkAtomPset [definition, in Psets]
mkAtomRec [axiom, in Atoms]
mkAtomSwap [definition, in Swaps]
mkExtFsetPset [definition, in Psets]
mkFuncSwap [definition, in Swaps]
mkFunPset [definition, in Psets]
mkIdPset [definition, in Psets]
mkIdSwap [definition, in Swaps]
mkListPset [definition, in Psets]
mkListSwap [definition, in Swaps]
mkOrderedListExtFset [axiom, in ExtFsetImpl]
mkPairPset [definition, in Psets]
mkPairSwap [definition, in Swaps]
N
Nominal [library]
P
pair_swap [definition, in Swaps]
pair_swap_distrib [lemma, in Swaps]
pair_swap_invol [lemma, in Swaps]
pair_swap_same [lemma, in Swaps]
papp [constructor, in STLCImpl]
pbound [constructor, in STLCImpl]
pbound_eq [lemma, in STLCImpl]
pcompose [axiom, in Permutations]
pdot [constructor, in STLCImpl]
perma [axiom, in Permutations]
perma_compose [axiom, in Permutations]
perma_compose_inv_eq [lemma, in Permutations]
perma_compose_inv_eq' [lemma, in Permutations]
perma_double_inv_eq [lemma, in Permutations]
perma_eq [axiom, in Permutations]
perma_extend [axiom, in Permutations]
perma_id [axiom, in Permutations]
perma_injective [lemma, in Permutations]
perma_inverse [axiom, in Permutations]
perma_inverse' [lemma, in Permutations]
perma_inv_compose [lemma, in Permutations]
perma_inv_compose_eq [lemma, in Permutations]
perma_inv_id [lemma, in Permutations]
perma_inv_id_eq [lemma, in Permutations]
perma_inv_swap [lemma, in Permutations]
perma_inv_swap_eq [lemma, in Permutations]
perma_swap_commute [lemma, in Permutations]
perma_swap_distrib [lemma, in Permutations]
perma_swap_invol [lemma, in Permutations]
perma_swap_invol_eq [lemma, in Permutations]
perma_swap_same [lemma, in Permutations]
perma_swap_same_eq [lemma, in Permutations]
perma_swap_switch [lemma, in Permutations]
perma_swap_switch_eq [lemma, in Permutations]
permt [axiom, in Permutations]
Permutations [library]
PermutationsAbstraction [module, in Permutations]
PermutationsImplementation [module, in Permutations]
perm_app [lemma, in Psets]
perm_app [axiom, in STLC]
perm_app [lemma, in STLCImpl]
perm_atom [lemma, in Psets]
perm_dot [axiom, in STLC]
perm_dot [lemma, in STLCImpl]
perm_eq [lemma, in Psets]
perm_extFset_add [lemma, in Psets]
perm_extFset_diff [lemma, in Psets]
perm_extFset_empty [lemma, in Psets]
perm_extFset_In [lemma, in Psets]
perm_extFset_In' [lemma, in Psets]
perm_extFset_neg_In [lemma, in Psets]
perm_extFset_neg_In' [lemma, in Psets]
perm_extFset_remove [lemma, in Psets]
perm_extFset_singleton [lemma, in Psets]
perm_extFset_Subset [lemma, in Psets]
perm_extFset_union [lemma, in Psets]
perm_freshP [lemma, in Psets]
perm_freshP' [lemma, in Psets]
perm_fun [lemma, in Psets]
perm_injective [lemma, in Psets]
perm_inv [lemma, in Psets]
perm_inv' [lemma, in Psets]
perm_lam [lemma, in STLCImpl]
perm_lam [axiom, in STLC]
perm_list_cons [lemma, in Psets]
perm_list_In [lemma, in Psets]
perm_list_In' [lemma, in Psets]
perm_list_nil [lemma, in Psets]
perm_list_not_In [lemma, in Psets]
perm_list_not_In' [lemma, in Psets]
perm_on_extFset [definition, in Psets]
perm_on_extFset_In_raw [lemma, in Psets]
perm_on_fun [definition, in Psets]
perm_on_list [definition, in Psets]
perm_on_pair [definition, in Psets]
perm_pair [lemma, in Psets]
perm_supports [lemma, in Psets]
perm_supports' [lemma, in Psets]
perm_swap_invol [lemma, in Psets]
perm_swap_move [lemma, in Psets]
perm_swap_move' [lemma, in Psets]
perm_swap_same [lemma, in Psets]
perm_swap_switch [lemma, in Psets]
perm_var [lemma, in STLCImpl]
perm_var [axiom, in STLC]
pextend [axiom, in Permutations]
pfree [constructor, in STLCImpl]
Phi [inductive, in STLCImpl]
PhiPermR [definition, in STLCImpl]
Phi_case [lemma, in STLCImpl]
Phi_fv [definition, in STLCImpl]
Phi_fv_abs [lemma, in STLCImpl]
Phi_ind_size_multi [lemma, in STLCImpl]
Phi_ind_size_single [lemma, in STLCImpl]
Phi_perm [definition, in STLCImpl]
Phi_perm_abs [lemma, in STLCImpl]
Phi_size [definition, in STLCImpl]
Phi_size_abs [lemma, in STLCImpl]
Phi_size_eq_O [lemma, in STLCImpl]
Phi_size_inst [lemma, in STLCImpl]
Phi_size_lt_O [lemma, in STLCImpl]
Phi_size_lt_papp_arg [lemma, in STLCImpl]
Phi_size_lt_papp_fun [lemma, in STLCImpl]
Phi_size_lt_plam [lemma, in STLCImpl]
Phi_size_perm [lemma, in STLCImpl]
Phi_swap_inst [lemma, in STLCImpl]
Phi_swap_inst_commute [lemma, in STLCImpl]
Phi_weaken [definition, in STLCImpl]
pid [axiom, in Permutations]
pinv [axiom, in Permutations]
plam [constructor, in STLCImpl]
Proof_irrelevance [axiom, in Axioms]
Psets [library]
PsetT [inductive, in Psets]
R
recF [definition, in STLCImpl]
recF_stable [lemma, in STLCImpl]
recF_stable_gen [lemma, in STLCImpl]
remove [definition, in ExtFset]
remove_elim_1 [lemma, in ExtFset]
remove_elim_2 [lemma, in ExtFset]
remove_empty [lemma, in ExtFset]
remove_intro [lemma, in ExtFset]
remove_neg_elim [lemma, in ExtFset]
remove_neg_elim_strong_1 [lemma, in ExtFset]
remove_neg_elim_strong_2 [lemma, in ExtFset]
remove_neg_intro_1 [lemma, in ExtFset]
remove_neg_intro_2 [lemma, in ExtFset]
remove_singleton_1 [lemma, in ExtFset]
remove_singleton_2 [lemma, in ExtFset]
remove_union [lemma, in ExtFset]
rewrite_and_swap [lemma, in STLCImpl]
rewrite_to_swap [lemma, in STLCImpl]
S
S [constructor, in UseSTLC]
singleton [definition, in ExtFset]
singleton_elim [lemma, in ExtFset]
singleton_intro [lemma, in ExtFset]
singleton_neg_elim [lemma, in ExtFset]
singleton_neg_intro [lemma, in ExtFset]
size [inductive, in UseSTLC]
size2 [lemma, in UseSTLC]
size_app [constructor, in UseSTLC]
size_lam [constructor, in UseSTLC]
size_total [lemma, in UseSTLC]
size_unit [constructor, in UseSTLC]
size_var [constructor, in UseSTLC]
SKabs [inductive, in UseSTLC]
SKabs_equivariant [lemma, in UseSTLC]
SKabs_I [constructor, in UseSTLC]
SKabs_K [constructor, in UseSTLC]
SKabs_S [constructor, in UseSTLC]
SKapp [constructor, in UseSTLC]
SKapp_equivariant [lemma, in UseSTLC]
SKcomp [inductive, in UseSTLC]
SKcomp_app [constructor, in UseSTLC]
SKcomp_equivariant [lemma, in UseSTLC]
SKcomp_lam [constructor, in UseSTLC]
SKcomp_var [constructor, in UseSTLC]
SKfvar [definition, in UseSTLC]
SKfvar_equivariant [lemma, in UseSTLC]
SKP [definition, in UseSTLC]
SKperm [definition, in UseSTLC]
SKtm [inductive, in UseSTLC]
SKvar [constructor, in UseSTLC]
SKvar_equivariant [lemma, in UseSTLC]
STLC [module, in STLC]
STLC [library]
STLCImpl [library]
Subset [definition, in ExtFset]
Subset_add [lemma, in ExtFset]
Subset_add_l_to_remove [lemma, in ExtFset]
Subset_add_r [lemma, in ExtFset]
Subset_empty [lemma, in ExtFset]
Subset_refl [lemma, in ExtFset]
Subset_remove_l_to_add [lemma, in ExtFset]
Subset_singleton_l [lemma, in ExtFset]
Subset_supports [lemma, in Psets]
Subset_trans [lemma, in ExtFset]
Subset_union_l [lemma, in ExtFset]
Subset_union_r1 [lemma, in ExtFset]
Subset_union_r2 [lemma, in ExtFset]
Subset_union_union [lemma, in ExtFset]
subst [definition, in UseSTLC]
subst_app [lemma, in UseSTLC]
subst_commute [lemma, in UseSTLC]
subst_dot [lemma, in UseSTLC]
subst_equal [lemma, in UseSTLC]
subst_equivariant [lemma, in UseSTLC]
subst_fresh_var [lemma, in UseSTLC]
subst_lam [lemma, in UseSTLC]
subst_not_fv [lemma, in UseSTLC]
subst_supp_app [lemma, in UseSTLC]
subst_supp_dot [lemma, in UseSTLC]
subst_supp_lam [lemma, in UseSTLC]
subst_supp_var [lemma, in UseSTLC]
subst_var_eq [lemma, in UseSTLC]
subst_var_neq [lemma, in UseSTLC]
subst_var_same' [lemma, in UseSTLC]
Support [library]
supports [definition, in Support]
supports [definition, in Psets]
supports_application [lemma, in Psets]
supports_atom [lemma, in Psets]
supports_atom [lemma, in Support]
supports_fun [lemma, in Psets]
supports_intersection [lemma, in Support]
supports_list_cons [lemma, in Psets]
supports_list_nil [lemma, in Psets]
supports_pair [lemma, in Psets]
supports_subset [lemma, in Support]
supports_subst [lemma, in UseSTLC]
supports_tm [lemma, in UseSTLC]
supports_to_fresh [lemma, in Support]
swapa [definition, in Atoms]
swapa_distrib [lemma, in Atoms]
swapa_injective [lemma, in Atoms]
swapa_invol [lemma, in Atoms]
swapa_left [lemma, in Atoms]
swapa_left' [lemma, in Atoms]
swapa_neither [lemma, in Atoms]
swapa_right [lemma, in Atoms]
swapa_right' [lemma, in Atoms]
swapa_same [lemma, in Atoms]
swapa_switch [lemma, in Atoms]
Swaps [library]
SwapT [inductive, in Swaps]
swap_app [lemma, in Swaps]
swap_fresh [lemma, in Support]
swap_freshP_atoms [lemma, in Psets]
swap_fresh_atoms [lemma, in Support]
swap_func [lemma, in Swaps]
swap_injective [lemma, in Swaps]
swap_invol' [lemma, in Swaps]
swap_in_abs [lemma, in STLCImpl]
swap_move_left [lemma, in Swaps]
swap_move_right [lemma, in Swaps]
swap_non_supports [lemma, in Support]
swap_non_supports [lemma, in Psets]
swap_not_in_set [lemma, in Support]
swap_not_in_set [lemma, in Psets]
swap_not_in_set' [lemma, in Psets]
swap_same' [lemma, in Swaps]
swap_switch [lemma, in Swaps]
swap_switch_invol [lemma, in Swaps]
swap_switch_invol' [lemma, in Swaps]
swap_to_rewrite [lemma, in STLCImpl]
swap_undistrib [lemma, in Swaps]
S_equivariant [lemma, in UseSTLC]
T
tm [definition, in STLCImpl]
tm [axiom, in STLC]
tmP [axiom, in STLC]
tmP [definition, in STLCImpl]
tmvar [axiom, in STLC]
tmvar [definition, in STLCImpl]
tmvarP [definition, in STLC]
tmvarP [definition, in STLCImpl]
tm_induction [lemma, in STLCImpl]
tm_induction [lemma, in UseSTLC]
tm_induction' [lemma, in UseSTLC]
tm_induction_weak [axiom, in STLC]
tm_induction_weak [lemma, in STLCImpl]
tm_induction_weak_derived [lemma, in UseSTLC]
tm_rec [definition, in STLCImpl]
tm_rec [axiom, in STLC]
tm_rec_app [lemma, in STLCImpl]
tm_rec_app [axiom, in STLC]
tm_rec_dot [axiom, in STLC]
tm_rec_dot [lemma, in STLCImpl]
tm_rec_lam [lemma, in STLCImpl]
tm_rec_lam [axiom, in STLC]
tm_rec_supp [lemma, in STLCImpl]
tm_rec_supp [axiom, in STLC]
tm_rec_var [axiom, in STLC]
tm_rec_var [lemma, in STLCImpl]
ty [inductive, in STLCImpl]
ty [inductive, in STLC]
tyP [definition, in STLCImpl]
tyP [definition, in STLC]
U
u [constructor, in UseSTLC]
union_commute [lemma, in ExtFset]
union_elim_1 [lemma, in ExtFset]
union_elim_2 [lemma, in ExtFset]
union_empty_1 [lemma, in ExtFset]
union_empty_2 [lemma, in ExtFset]
union_neg_elim_1 [lemma, in ExtFset]
union_neg_elim_2 [lemma, in ExtFset]
union_neg_intro [lemma, in ExtFset]
union_union_distrib [lemma, in ExtFset]
unit [constructor, in STLCImpl]
unit [constructor, in STLC]
unit_value [constructor, in UseSTLC]
unswap_fresh [lemma, in Support]
UseSTLC [module, in UseSTLC]
UseSTLC [library]
V
value [inductive, in UseSTLC]
values_are_normal_forms [lemma, in UseSTLC]
value_equivariant [lemma, in UseSTLC]
var [axiom, in STLC]
var [definition, in STLCImpl]
Axiom Index
A
app [in STLC]
D
distinctness_app_dot [in STLC]
distinctness_app_lam [in STLC]
distinctness_app_var [in STLC]
distinctness_dot_app [in STLC]
distinctness_dot_lam [in STLC]
distinctness_dot_var [in STLC]
distinctness_lam_app [in STLC]
distinctness_lam_dot [in STLC]
distinctness_lam_var [in STLC]
distinctness_var_app [in STLC]
distinctness_var_dot [in STLC]
distinctness_var_lam [in STLC]
dot [in STLC]
E
eq_lam [in STLC]
F
fun_extensionality [in Axioms]
fvar [in STLC]
fvar_app [in STLC]
fvar_dot [in STLC]
fvar_lam [in STLC]
fvar_var [in STLC]
I
injection_app_arg [in STLC]
injection_app_fun [in STLC]
injection_lam_body [in STLC]
injection_lam_ty [in STLC]
injection_var [in STLC]
L
lam [in STLC]
M
mkAtomRec [in Atoms]
mkOrderedListExtFset [in ExtFsetImpl]
P
pcompose [in Permutations]
perma [in Permutations]
perma_compose [in Permutations]
perma_eq [in Permutations]
perma_extend [in Permutations]
perma_id [in Permutations]
perma_inverse [in Permutations]
permt [in Permutations]
perm_app [in STLC]
perm_dot [in STLC]
perm_lam [in STLC]
perm_var [in STLC]
pextend [in Permutations]
pid [in Permutations]
pinv [in Permutations]
Proof_irrelevance [in Axioms]
T
tm [in STLC]
tmP [in STLC]
tmvar [in STLC]
tm_induction_weak [in STLC]
tm_rec [in STLC]
tm_rec_app [in STLC]
tm_rec_dot [in STLC]
tm_rec_lam [in STLC]
tm_rec_supp [in STLC]
tm_rec_var [in STLC]
V
var [in STLC]
Lemma Index
A
abs_eq [in STLCImpl]
abs_inst_inv [in STLCImpl]
abs_neq [in STLCImpl]
add_add [in ExtFset]
add_add_incl [in ExtFset]
add_elim_1 [in ExtFset]
add_elim_2 [in ExtFset]
add_neg_elim_1 [in ExtFset]
add_neg_elim_2 [in ExtFset]
add_neg_intro [in ExtFset]
add_union [in ExtFset]
application_fresh [in Support]
application_supports [in Support]
atom_eqdec_contract [in Atoms]
atom_eqdec_eq [in Atoms]
atom_eqdec_neq [in Atoms]
atom_swap_left [in Swaps]
atom_swap_left' [in Swaps]
atom_swap_neither [in Swaps]
atom_swap_right [in Swaps]
atom_swap_right' [in Swaps]
C
cbv_deterministic [in UseSTLC]
cbv_equivariant [in UseSTLC]
D
diff_empty_1 [in ExtFset]
diff_empty_2 [in ExtFset]
diff_neg_elim [in ExtFset]
diff_neg_elim_1 [in ExtFset]
diff_neg_elim_2 [in ExtFset]
diff_neg_intro_1 [in ExtFset]
diff_neg_intro_2 [in ExtFset]
distinctness_app_dot [in STLCImpl]
distinctness_app_lam [in STLCImpl]
distinctness_app_var [in STLCImpl]
distinctness_dot_app [in STLCImpl]
distinctness_dot_lam [in STLCImpl]
distinctness_dot_var [in STLCImpl]
distinctness_lam_app [in STLCImpl]
distinctness_lam_dot [in STLCImpl]
distinctness_lam_var [in STLCImpl]
distinctness_var_app [in STLCImpl]
distinctness_var_dot [in STLCImpl]
distinctness_var_lam [in STLCImpl]
E
elements_empty [in ExtFset]
empty_elim [in ExtFset]
eq_lam [in STLCImpl]
eq_lam_diff [in STLCImpl]
F
finite_nat_list_max [in AuxLib]
finite_nat_list_max' [in AuxLib]
freshP_application [in Psets]
freshP_atom [in Psets]
freshP_from_supports [in Psets]
fresh_atom_from_neq [in Support]
function_constancy_v1 [in Psets]
function_constancy_v1 [in Support]
function_constancy_v2 [in Support]
function_constancy_v2 [in Psets]
function_supports [in Support]
func_swap_distrib [in Swaps]
func_swap_invol [in Swaps]
func_swap_same [in Swaps]
fvar_app [in STLCImpl]
fvar_dot [in STLCImpl]
fvar_lam [in STLCImpl]
fvar_subst [in UseSTLC]
fvar_swap [in UseSTLC]
fvar_var [in STLCImpl]
I
id_swap_distrib [in Swaps]
id_swap_invol [in Swaps]
id_swap_reduce [in Swaps]
id_swap_same [in Swaps]
injection_app_arg [in STLCImpl]
injection_app_fun [in STLCImpl]
injection_lam_body [in STLCImpl]
injection_lam_ty [in STLCImpl]
injection_papp_arg [in STLCImpl]
injection_papp_fun [in STLCImpl]
injection_plam [in STLCImpl]
injection_var [in STLCImpl]
inst_abs_inv [in STLCImpl]
inst_papp [in STLCImpl]
inst_plam [in STLCImpl]
intersection_empty_1 [in ExtFset]
intersection_empty_2 [in ExtFset]
intersection_neg_elim [in ExtFset]
intersection_neg_elim_1 [in ExtFset]
intersection_neg_elim_2 [in ExtFset]
intersection_neg_intro_1 [in ExtFset]
intersection_neg_intro_2 [in ExtFset]
intersection_supports [in Psets]
K
K_equivariant [in UseSTLC]
L
le_lt_S [in AuxLib]
list_not_in_cons_l [in AuxLib]
list_swap_distrib [in Swaps]
list_swap_In [in Swaps]
list_swap_invol [in Swaps]
list_swap_same [in Swaps]
lt_Sn_n [in AuxLib]
M
map_compose [in ExtFset]
max_lt_l [in AuxLib]
max_lt_r [in AuxLib]
P
pair_swap_distrib [in Swaps]
pair_swap_invol [in Swaps]
pair_swap_same [in Swaps]
pbound_eq [in STLCImpl]
perma_compose_inv_eq [in Permutations]
perma_compose_inv_eq' [in Permutations]
perma_double_inv_eq [in Permutations]
perma_injective [in Permutations]
perma_inverse' [in Permutations]
perma_inv_compose [in Permutations]
perma_inv_compose_eq [in Permutations]
perma_inv_id [in Permutations]
perma_inv_id_eq [in Permutations]
perma_inv_swap [in Permutations]
perma_inv_swap_eq [in Permutations]
perma_swap_commute [in Permutations]
perma_swap_distrib [in Permutations]
perma_swap_invol [in Permutations]
perma_swap_invol_eq [in Permutations]
perma_swap_same [in Permutations]
perma_swap_same_eq [in Permutations]
perma_swap_switch [in Permutations]
perma_swap_switch_eq [in Permutations]
perm_app [in Psets]
perm_app [in STLCImpl]
perm_atom [in Psets]
perm_dot [in STLCImpl]
perm_eq [in Psets]
perm_extFset_add [in Psets]
perm_extFset_diff [in Psets]
perm_extFset_empty [in Psets]
perm_extFset_In [in Psets]
perm_extFset_In' [in Psets]
perm_extFset_neg_In [in Psets]
perm_extFset_neg_In' [in Psets]
perm_extFset_remove [in Psets]
perm_extFset_singleton [in Psets]
perm_extFset_Subset [in Psets]
perm_extFset_union [in Psets]
perm_freshP [in Psets]
perm_freshP' [in Psets]
perm_fun [in Psets]
perm_injective [in Psets]
perm_inv [in Psets]
perm_inv' [in Psets]
perm_lam [in STLCImpl]
perm_list_cons [in Psets]
perm_list_In [in Psets]
perm_list_In' [in Psets]
perm_list_nil [in Psets]
perm_list_not_In [in Psets]
perm_list_not_In' [in Psets]
perm_on_extFset_In_raw [in Psets]
perm_pair [in Psets]
perm_supports [in Psets]
perm_supports' [in Psets]
perm_swap_invol [in Psets]
perm_swap_move [in Psets]
perm_swap_move' [in Psets]
perm_swap_same [in Psets]
perm_swap_switch [in Psets]
perm_var [in STLCImpl]
Phi_case [in STLCImpl]
Phi_fv_abs [in STLCImpl]
Phi_ind_size_multi [in STLCImpl]
Phi_ind_size_single [in STLCImpl]
Phi_perm_abs [in STLCImpl]
Phi_size_abs [in STLCImpl]
Phi_size_eq_O [in STLCImpl]
Phi_size_inst [in STLCImpl]
Phi_size_lt_O [in STLCImpl]
Phi_size_lt_papp_arg [in STLCImpl]
Phi_size_lt_papp_fun [in STLCImpl]
Phi_size_lt_plam [in STLCImpl]
Phi_size_perm [in STLCImpl]
Phi_swap_inst [in STLCImpl]
Phi_swap_inst_commute [in STLCImpl]
R
recF_stable [in STLCImpl]
recF_stable_gen [in STLCImpl]
remove_elim_1 [in ExtFset]
remove_elim_2 [in ExtFset]
remove_empty [in ExtFset]
remove_intro [in ExtFset]
remove_neg_elim [in ExtFset]
remove_neg_elim_strong_1 [in ExtFset]
remove_neg_elim_strong_2 [in ExtFset]
remove_neg_intro_1 [in ExtFset]
remove_neg_intro_2 [in ExtFset]
remove_singleton_1 [in ExtFset]
remove_singleton_2 [in ExtFset]
remove_union [in ExtFset]
rewrite_and_swap [in STLCImpl]
rewrite_to_swap [in STLCImpl]
S
singleton_elim [in ExtFset]
singleton_intro [in ExtFset]
singleton_neg_elim [in ExtFset]
singleton_neg_intro [in ExtFset]
size2 [in UseSTLC]
size_total [in UseSTLC]
SKabs_equivariant [in UseSTLC]
SKapp_equivariant [in UseSTLC]
SKcomp_equivariant [in UseSTLC]
SKfvar_equivariant [in UseSTLC]
SKvar_equivariant [in UseSTLC]
Subset_add [in ExtFset]
Subset_add_l_to_remove [in ExtFset]
Subset_add_r [in ExtFset]
Subset_empty [in ExtFset]
Subset_refl [in ExtFset]
Subset_remove_l_to_add [in ExtFset]
Subset_singleton_l [in ExtFset]
Subset_supports [in Psets]
Subset_trans [in ExtFset]
Subset_union_l [in ExtFset]
Subset_union_r1 [in ExtFset]
Subset_union_r2 [in ExtFset]
Subset_union_union [in ExtFset]
subst_app [in UseSTLC]
subst_commute [in UseSTLC]
subst_dot [in UseSTLC]
subst_equal [in UseSTLC]
subst_equivariant [in UseSTLC]
subst_fresh_var [in UseSTLC]
subst_lam [in UseSTLC]
subst_not_fv [in UseSTLC]
subst_supp_app [in UseSTLC]
subst_supp_dot [in UseSTLC]
subst_supp_lam [in UseSTLC]
subst_supp_var [in UseSTLC]
subst_var_eq [in UseSTLC]
subst_var_neq [in UseSTLC]
subst_var_same' [in UseSTLC]
supports_application [in Psets]
supports_atom [in Psets]
supports_atom [in Support]
supports_fun [in Psets]
supports_intersection [in Support]
supports_list_cons [in Psets]
supports_list_nil [in Psets]
supports_pair [in Psets]
supports_subset [in Support]
supports_subst [in UseSTLC]
supports_tm [in UseSTLC]
supports_to_fresh [in Support]
swapa_distrib [in Atoms]
swapa_injective [in Atoms]
swapa_invol [in Atoms]
swapa_left [in Atoms]
swapa_left' [in Atoms]
swapa_neither [in Atoms]
swapa_right [in Atoms]
swapa_right' [in Atoms]
swapa_same [in Atoms]
swapa_switch [in Atoms]
swap_app [in Swaps]
swap_fresh [in Support]
swap_freshP_atoms [in Psets]
swap_fresh_atoms [in Support]
swap_func [in Swaps]
swap_injective [in Swaps]
swap_invol' [in Swaps]
swap_in_abs [in STLCImpl]
swap_move_left [in Swaps]
swap_move_right [in Swaps]
swap_non_supports [in Support]
swap_non_supports [in Psets]
swap_not_in_set [in Support]
swap_not_in_set [in Psets]
swap_not_in_set' [in Psets]
swap_same' [in Swaps]
swap_switch [in Swaps]
swap_switch_invol [in Swaps]
swap_switch_invol' [in Swaps]
swap_to_rewrite [in STLCImpl]
swap_undistrib [in Swaps]
S_equivariant [in UseSTLC]
T
tm_induction [in STLCImpl]
tm_induction [in UseSTLC]
tm_induction' [in UseSTLC]
tm_induction_weak [in STLCImpl]
tm_induction_weak_derived [in UseSTLC]
tm_rec_app [in STLCImpl]
tm_rec_dot [in STLCImpl]
tm_rec_lam [in STLCImpl]
tm_rec_supp [in STLCImpl]
tm_rec_var [in STLCImpl]
U
union_commute [in ExtFset]
union_elim_1 [in ExtFset]
union_elim_2 [in ExtFset]
union_empty_1 [in ExtFset]
union_empty_2 [in ExtFset]
union_neg_elim_1 [in ExtFset]
union_neg_elim_2 [in ExtFset]
union_neg_intro [in ExtFset]
union_union_distrib [in ExtFset]
unswap_fresh [in Support]
V
values_are_normal_forms [in UseSTLC]
value_equivariant [in UseSTLC]
Constructor Index
A
abs_value [in UseSTLC]
arrow [in STLC]
arrow [in STLCImpl]
C
cbv_beta [in UseSTLC]
cbv_left [in UseSTLC]
cbv_right [in UseSTLC]
K
K [in UseSTLC]
P
papp [in STLCImpl]
pbound [in STLCImpl]
pdot [in STLCImpl]
pfree [in STLCImpl]
plam [in STLCImpl]
S
S [in UseSTLC]
size_app [in UseSTLC]
size_lam [in UseSTLC]
size_unit [in UseSTLC]
size_var [in UseSTLC]
SKabs_I [in UseSTLC]
SKabs_K [in UseSTLC]
SKabs_S [in UseSTLC]
SKapp [in UseSTLC]
SKcomp_app [in UseSTLC]
SKcomp_lam [in UseSTLC]
SKcomp_var [in UseSTLC]
SKvar [in UseSTLC]
U
u [in UseSTLC]
unit [in STLCImpl]
unit [in STLC]
unit_value [in UseSTLC]
Inductive Index
A
AtomT [in Atoms]
C
cbv [in UseSTLC]
E
ExtFset [in ExtFset]
P
Phi [in STLCImpl]
PsetT [in Psets]
S
size [in UseSTLC]
SKabs [in UseSTLC]
SKcomp [in UseSTLC]
SKtm [in UseSTLC]
SwapT [in Swaps]
T
ty [in STLCImpl]
ty [in STLC]
V
value [in UseSTLC]
Definition Index
A
abs [in STLCImpl]
app [in STLCImpl]
D
dot [in STLCImpl]
F
fresh [in Support]
freshP [in Psets]
func_swap [in Swaps]
fvar [in STLCImpl]
I
id_swap [in Swaps]
inst [in STLCImpl]
inst_aux [in STLCImpl]
L
lam [in STLCImpl]
list_swap [in Swaps]
M
mkAtomPset [in Psets]
mkAtomSwap [in Swaps]
mkExtFsetPset [in Psets]
mkFuncSwap [in Swaps]
mkFunPset [in Psets]
mkIdPset [in Psets]
mkIdSwap [in Swaps]
mkListPset [in Psets]
mkListSwap [in Swaps]
mkPairPset [in Psets]
mkPairSwap [in Swaps]
P
pair_swap [in Swaps]
perm_on_extFset [in Psets]
perm_on_fun [in Psets]
perm_on_list [in Psets]
perm_on_pair [in Psets]
PhiPermR [in STLCImpl]
Phi_fv [in STLCImpl]
Phi_perm [in STLCImpl]
Phi_size [in STLCImpl]
Phi_weaken [in STLCImpl]
R
recF [in STLCImpl]
remove [in ExtFset]
S
singleton [in ExtFset]
SKfvar [in UseSTLC]
SKP [in UseSTLC]
SKperm [in UseSTLC]
Subset [in ExtFset]
subst [in UseSTLC]
supports [in Support]
supports [in Psets]
swapa [in Atoms]
T
tm [in STLCImpl]
tmP [in STLCImpl]
tmvar [in STLCImpl]
tmvarP [in STLC]
tmvarP [in STLCImpl]
tm_rec [in STLCImpl]
tyP [in STLCImpl]
tyP [in STLC]
V
var [in STLCImpl]
Module Index
A
AtomImplementation [in Atoms]
AtomImplementationSig [in Atoms]
E
ExtFsetImplementation [in ExtFsetImpl]
ExtFsetSig [in ExtFsetImpl]
M
MakeSTLC [in STLCImpl]
P
PermutationsAbstraction [in Permutations]
PermutationsImplementation [in Permutations]
S
STLC [in STLC]
U
UseSTLC [in UseSTLC]
Library Index
A
Atoms
AuxLib
Axioms
E
ExtFset
ExtFsetImpl
N
Nominal
P
Permutations
Psets
S
STLC
STLCImpl
Support
Swaps
U
UseSTLC
| 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 |
_ |
(471 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 |
_ |
(56 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 |
_ |
(298 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(29 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 |
_ |
(13 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 |
_ |
(53 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 |
_ |
(9 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 |
_ |
(13 entries) |
This page has been generated by coqdoc