| 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 | (1222 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 | (49 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 | (8 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 | (17 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 | (803 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 | (14 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 | (97 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 | (27 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 | (66 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 | (3 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 | (7 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 | (131 entries) |
Global Index
A
act [definition, in atoms]act_comp_app [lemma, in atoms]
act_nil [lemma, in atoms]
all_atoms [definition, in restr_atoms]
and_stronger_l [lemma, in tools]
and_or_distr [lemma, in tools]
and_rel_stronger_stronger_stronger [instance, in tools]
and_rel_eq_rel_eq_rel_eq_rel [instance, in tools]
and_pred_eq_pred_eq_pred_eq_pred [instance, in tools]
and_pred [definition, in tools]
and_rel [definition, in tools]
antisym_incl_lst [instance, in equiv_lst]
anti_incl_lst [instance, in equiv_lst]
apply_fun_morph [lemma, in restr_atoms]
apply_ψ_φ_id [lemma, in restr_atoms]
apply_fun_ext [lemma, in restr_atoms]
apply_fun_id [lemma, in restr_atoms]
apply_fun_comp [lemma, in restr_atoms]
apply_perm_eq [lemma, in restr_atoms]
apply_φ_apply_perm_p [lemma, in restr_atoms]
apply_φ_eq_ax [lemma, in restr_atoms]
apply_perm_app [lemma, in restr_atoms]
apply_φ_apply_perm [lemma, in restr_atoms]
apply_φ_fresh [lemma, in restr_atoms]
apply_φ_stage [lemma, in restr_atoms]
apply_φ_support [lemma, in restr_atoms]
apply_φ_eq_expr [lemma, in restr_atoms]
apply_φ_positive [lemma, in restr_atoms]
apply_φ_str_positive [lemma, in restr_atoms]
apply_φ_has_type [lemma, in restr_atoms]
apply_φ_untyped [lemma, in restr_atoms]
apply_φ_single [lemma, in restr_atoms]
apply_φ_multi [lemma, in restr_atoms]
apply_φ_no_perm [lemma, in restr_atoms]
apply_φ_restr [lemma, in restr_atoms]
apply_fun [definition, in restr_atoms]
apply_perm_id [lemma, in morphisms]
apply_perm_nil [lemma, in morphisms]
apply_perm_has_type [lemma, in morphisms]
apply_perm_size [lemma, in morphisms]
apply_perm_equiv_perm [instance, in morphisms]
apply_perm [definition, in morphisms]
apply_perm_var_equiv_perm_eq_letter [lemma, in morphisms]
apply_perm_var_eq_letter [lemma, in morphisms]
apply_perm_var_equiv_perm [lemma, in morphisms]
apply_perm_var_app [lemma, in morphisms]
apply_perm_var_τ [lemma, in morphisms]
apply_perm_var [definition, in morphisms]
apply_perm_var_bis [lemma, in morphisms]
apply_perm_θ_u [lemma, in perm]
apply_perm_θ_t [lemma, in perm]
apply_perm_equiv_perm [lemma, in perm]
app_length_eq [lemma, in restr_atoms]
app_com [lemma, in equiv_lst]
app_l_l [lemma, in equiv_lst]
app_incl [instance, in equiv_lst]
app_equiv [instance, in equiv_lst]
app_cong [lemma, in equiv_lst]
assoc_or_rel1 [lemma, in tools]
Atom [axiom, in atoms]
atoms [library]
atoms_ops [library]
Atom_eq_dec [lemma, in atoms]
at_diff_un_NKA_p [lemma, in theories]
at_diff_un_NKA_θp [lemma, in theories]
augm_transfer2 [lemma, in order]
augm_transfer' [lemma, in order]
augm_transfer [lemma, in order]
aux [lemma, in restr_atoms]
aux2 [lemma, in restr_atoms]
ax_eq_restr_ax_eq [lemma, in restr_atoms]
B
bequiv_perm_spec [lemma, in equiv_lst]bequiv_perm [definition, in equiv_lst]
beq_letter_spec [lemma, in letter]
beq_letter [definition, in letter]
beq_name_spec [axiom, in letter]
beq_name [axiom, in letter]
beq_expr_spec [lemma, in predicates]
beq_expr [definition, in predicates]
beq_perm_spec [lemma, in atoms]
beq_perm [definition, in atoms]
beq_list_spec [lemma, in atoms]
beq_list [definition, in atoms]
beq_neq_atom [lemma, in atoms]
beq_neq_atom1 [lemma, in atoms]
beq_eq_atom [lemma, in atoms]
beq_atom_spec [lemma, in atoms]
beq_atom_refl [axiom, in atoms]
beq_atom [axiom, in atoms]
bot [constructor, in expr]
bot_equiv_lst_eq [instance, in proofs]
Bs [definition, in expr]
C
can_var_length [lemma, in normalise]can_var_NoDup [lemma, in normalise]
can_var [definition, in normalise]
cons_rm_eq' [lemma, in equiv_lst]
cons_rm_eq [lemma, in equiv_lst]
cons_incl [instance, in equiv_lst]
cons_equiv [instance, in equiv_lst]
cons_cong [lemma, in equiv_lst]
cons_comm [lemma, in equiv_lst]
convert [definition, in normalise]
convert_morph [lemma, in normalise]
convert_eq2 [lemma, in normalise]
convert_eq [lemma, in normalise]
convert_fresh [lemma, in normalise]
convert_multi [lemma, in normalise]
convert_single [lemma, in normalise]
convert_str_positive [lemma, in normalise]
convert_untyped [lemma, in normalise]
convert_eq_perm [lemma, in normalise]
convert_involutive [lemma, in normalise]
conv_lst_inv [lemma, in normalise]
conv_can_var [lemma, in normalise]
conv_lst [lemma, in normalise]
conv_lst_perm [definition, in normalise]
D
decidable_no_perm [lemma, in predicates]decidable_single [lemma, in predicates]
decidable_multi [lemma, in predicates]
decidable_positive [lemma, in predicates]
decidable_str_positive [lemma, in predicates]
decidable_untyped [lemma, in predicates]
decidable_typed [lemma, in predicates]
derivable_axioms [lemma, in proofs]
disjoint_purge [lemma, in atoms_ops]
disjoint_com [lemma, in atoms_ops]
disjoint_In [lemma, in atoms_ops]
E
elements [definition, in equiv_lst]elements_In [lemma, in restr_atoms]
elements_map_pair [lemma, in restr_atoms]
elements_in_mact [lemma, in equiv_lst]
elements_act_in_equiv [lemma, in equiv_lst]
elements_inv_eq [lemma, in equiv_lst]
elements_app [lemma, in equiv_lst]
elements_inv_mact [lemma, in equiv_lst]
elements_inv_act [lemma, in equiv_lst]
eq [inductive, in proofs]
eqt_ν1 [lemma, in proofs]
eqt_ν4 [constructor, in proofs]
eqt_ν3 [constructor, in proofs]
eqt_νω2 [constructor, in proofs]
eqt_νω1 [constructor, in proofs]
eqt_θν [constructor, in proofs]
eqt_θν' [constructor, in proofs]
eqt_ν0 [constructor, in proofs]
equiv_perm_mact [instance, in atoms_ops]
equiv_perm_map_ψ [lemma, in restr_atoms]
equiv_perm_map_φ [lemma, in restr_atoms]
equiv_th_Equivalence [instance, in order]
equiv_th [definition, in order]
equiv_lst_b_spec [lemma, in equiv_lst]
equiv_lst_b [definition, in equiv_lst]
equiv_lst_Equiv [instance, in equiv_lst]
equiv_lst_trans [instance, in equiv_lst]
equiv_lst_sym [instance, in equiv_lst]
equiv_lst_refl [instance, in equiv_lst]
equiv_lst [definition, in equiv_lst]
equiv_perm_spec [instance, in atoms]
equiv_perm_app [instance, in atoms]
equiv_perm_inverse [instance, in atoms]
equiv_perm_Equivalence [instance, in atoms]
equiv_perm_trans [lemma, in atoms]
equiv_perm_sym [lemma, in atoms]
equiv_perm_refl [lemma, in atoms]
equiv_perm [definition, in atoms]
equiv_lst_length_undup [lemma, in normalise]
equiv_lst [library]
equ_ν4 [constructor, in proofs]
equ_ν3 [constructor, in proofs]
equ_νω1 [constructor, in proofs]
equ_θν [constructor, in proofs]
equ_θν' [constructor, in proofs]
equ_ν0 [constructor, in proofs]
eq_pred_Equivalence [instance, in tools]
eq_rel_Equivalence [instance, in tools]
eq_pred [definition, in tools]
eq_rel [definition, in tools]
eq_nom_typed_apply_φ [lemma, in restr_atoms]
eq_nom_typed_np_apply_φ [lemma, in restr_atoms]
eq_nom_typed_p_apply_φ [lemma, in restr_atoms]
eq_nom_untyped_apply_φ [lemma, in restr_atoms]
eq_nom_untyped_np_apply_φ [lemma, in restr_atoms]
eq_nom_untyped_p_apply_φ [lemma, in restr_atoms]
eq_ω_smpl_apply_φ [lemma, in restr_atoms]
eq_ν_smpl_apply_φ [lemma, in restr_atoms]
eq_perm_elim_apply_φ [lemma, in restr_atoms]
eq_perm_ω_apply_φ [lemma, in restr_atoms]
eq_perm_apply_φ [lemma, in restr_atoms]
eq_str_positive [lemma, in proofs]
eq_perm_str_positive [lemma, in proofs]
eq_perm_ω_str_positive [lemma, in proofs]
eq_ν_smpl_str_positive [lemma, in proofs]
eq_ω_smpl_str_positive [lemma, in proofs]
eq_nom_untyped_np_str_positive [lemma, in proofs]
eq_nom_typed_np_str_positive [lemma, in proofs]
eq_nom_untyped_str_positive [lemma, in proofs]
eq_nom_typed_str_positive [lemma, in proofs]
eq_no_perm [lemma, in proofs]
eq_perm_no_perm [lemma, in proofs]
eq_perm_ω_no_perm [lemma, in proofs]
eq_ν_smpl_no_perm [lemma, in proofs]
eq_ω_smpl_no_perm [lemma, in proofs]
eq_nom_untyped_np_no_perm [lemma, in proofs]
eq_nom_typed_np_no_perm [lemma, in proofs]
eq_nom_untyped_no_perm [lemma, in proofs]
eq_nom_typed_no_perm [lemma, in proofs]
eq_multi [lemma, in proofs]
eq_perm_multi [lemma, in proofs]
eq_perm_ω_multi [lemma, in proofs]
eq_perm_elim_multi [lemma, in proofs]
eq_ν_smpl_multi [lemma, in proofs]
eq_ω_smpl_multi [lemma, in proofs]
eq_nom_untyped_p_multi [lemma, in proofs]
eq_nom_untyped_np_multi [lemma, in proofs]
eq_nom_untyped_multi [lemma, in proofs]
eq_nom_typed_p_multi [lemma, in proofs]
eq_nom_typed_np_multi [lemma, in proofs]
eq_nom_typed_multi [lemma, in proofs]
eq_single [lemma, in proofs]
eq_perm_single [lemma, in proofs]
eq_perm_ω_single [lemma, in proofs]
eq_perm_elim_single [lemma, in proofs]
eq_ν_smpl_single [lemma, in proofs]
eq_ω_smpl_single [lemma, in proofs]
eq_nom_untyped_p_single [lemma, in proofs]
eq_nom_untyped_np_single [lemma, in proofs]
eq_nom_untyped_single [lemma, in proofs]
eq_nom_typed_p_single [lemma, in proofs]
eq_nom_typed_np_single [lemma, in proofs]
eq_nom_typed_single [lemma, in proofs]
eq_untyped [lemma, in proofs]
eq_ω_smpl_untyped [lemma, in proofs]
eq_ν_smpl_untyped [lemma, in proofs]
eq_perm_ω_untyped [lemma, in proofs]
eq_perm_untyped [lemma, in proofs]
eq_perm_elim_untyped [lemma, in proofs]
eq_nom_untyped_p_untyped [lemma, in proofs]
eq_nom_untyped_np_untyped [lemma, in proofs]
eq_nom_untyped_untyped [lemma, in proofs]
eq_type [lemma, in proofs]
eq_ω_smpl_type [lemma, in proofs]
eq_ν_smpl_type [lemma, in proofs]
eq_perm_ω_type [lemma, in proofs]
eq_perm_type [lemma, in proofs]
eq_perm_elim_type [lemma, in proofs]
eq_nom_typed_type [lemma, in proofs]
eq_nom_typed_p_type [lemma, in proofs]
eq_nom_typed_np_type [lemma, in proofs]
eq_nom_typed [inductive, in proofs]
eq_nom_typed_np [inductive, in proofs]
eq_nom_typed_p [inductive, in proofs]
eq_nom_untyped [inductive, in proofs]
eq_nom_untyped_np [inductive, in proofs]
eq_nom_untyped_p [inductive, in proofs]
eq_ωω [constructor, in proofs]
eq_ω_s [constructor, in proofs]
eq_ω_t [constructor, in proofs]
eq_ω_p [constructor, in proofs]
eq_ω_id [constructor, in proofs]
eq_ω_smpl [inductive, in proofs]
eq_νab [constructor, in proofs]
eq_νp [constructor, in proofs]
eq_ν_smpl [inductive, in proofs]
eq_nil_e [constructor, in proofs]
eq_θ_id [constructor, in proofs]
eq_θ_var [constructor, in proofs]
eq_θ_at [constructor, in proofs]
eq_θ_1 [constructor, in proofs]
eq_perm_elim [inductive, in proofs]
eq_θ_ω [constructor, in proofs]
eq_perm_ω [inductive, in proofs]
eq_θ_θ [constructor, in proofs]
eq_θ_ν [constructor, in proofs]
eq_θ_s [constructor, in proofs]
eq_θ_t [constructor, in proofs]
eq_θ_p [constructor, in proofs]
eq_perm [inductive, in proofs]
eq_ω_bot [constructor, in proofs]
eq_θ_bot [constructor, in proofs]
eq_θ_0 [constructor, in proofs]
eq_expr_eq [lemma, in proofs]
eq_Equiv [instance, in proofs]
eq_refl [lemma, in proofs]
eq_ax [constructor, in proofs]
eq_ka_impl [constructor, in proofs]
eq_ka [constructor, in proofs]
eq_ω [constructor, in proofs]
eq_θ [constructor, in proofs]
eq_ν [constructor, in proofs]
eq_star [constructor, in proofs]
eq_times [constructor, in proofs]
eq_plus [constructor, in proofs]
eq_vat [constructor, in proofs]
eq_var [constructor, in proofs]
eq_id [constructor, in proofs]
eq_bot [constructor, in proofs]
eq_un [constructor, in proofs]
eq_zero [constructor, in proofs]
eq_trans [constructor, in proofs]
eq_sym [constructor, in proofs]
eq_NKA_θp_untyped [lemma, in sg_to_mlt]
eq_NKA_θtp_single [lemma, in sg_to_mlt]
eq_NKA_θp_single [lemma, in sg_to_mlt]
eq_NKA_θtp_image [lemma, in sg_to_mlt]
eq_NKA_θp_image [lemma, in sg_to_mlt]
eq_nom_typed_p_image [lemma, in sg_to_mlt]
eq_nom_untyped_p_image [lemma, in sg_to_mlt]
eq_perm_elim_image [lemma, in sg_to_mlt]
eq_perm_image [lemma, in sg_to_mlt]
eq_nom_typed_image [lemma, in sg_to_mlt]
eq_nom_untyped_image [lemma, in sg_to_mlt]
eq_ν_smpl_image [lemma, in sg_to_mlt]
eq_letter_τ [lemma, in letter]
eq_letter_Equivalence [instance, in letter]
eq_letter [definition, in letter]
eq_perm_ω_eq0 [lemma, in rm0]
eq_perm_eq0 [lemma, in rm0]
eq_ω_smpl_eq0 [lemma, in rm0]
eq_ν_smpl_eq0 [lemma, in rm0]
eq_perm_elim_eq0 [lemma, in rm0]
eq_nom_untyped_eq0 [lemma, in rm0]
eq_nom_untyped_np_eq0 [lemma, in rm0]
eq_nom_untyped_p_eq0 [lemma, in rm0]
eq_nom_typed_eq0 [lemma, in rm0]
eq_nom_typed_np_eq0 [lemma, in rm0]
eq_nom_typed_p_eq0 [lemma, in rm0]
eq_eq0 [lemma, in rm0]
eq_expr_rm_perm [lemma, in morphisms]
eq_expr_rm0 [lemma, in morphisms]
eq_expr_erase [lemma, in morphisms]
eq_typed_vers [lemma, in removetype]
eq_ν_smpl_typed_vers [lemma, in removetype]
eq_perm_typed_vers [lemma, in removetype]
eq_perm_elim_typed_vers [lemma, in removetype]
eq_nom_typed_np_vers [lemma, in removetype]
eq_nom_typed_p_vers [lemma, in removetype]
eq_nom_typed_vers [lemma, in removetype]
eq_νW2 [lemma, in removetype]
eq_smpl_ω_W [lemma, in removetype]
eq_perm_ω_W [lemma, in removetype]
eq_WW [constructor, in removetype]
eq_W_s [constructor, in removetype]
eq_W_t [constructor, in removetype]
eq_W_p [constructor, in removetype]
eq_W_id [constructor, in removetype]
eq_W_smpl [inductive, in removetype]
eq_θ_W [constructor, in removetype]
eq_perm_W [inductive, in removetype]
eq_support [lemma, in removetype]
eq_ν_smpl_support [lemma, in removetype]
eq_perm_support [lemma, in removetype]
eq_perm_elim_support [lemma, in removetype]
eq_nom_untyped_np_support [lemma, in removetype]
eq_nom_untyped_p_support [lemma, in removetype]
eq_nom_untyped_support [lemma, in removetype]
eq_erase [lemma, in removetype]
eq_ω_smpl_erase [lemma, in removetype]
eq_ν_smpl_erase [lemma, in removetype]
eq_perm_ω_erase [lemma, in removetype]
eq_perm_erase [lemma, in removetype]
eq_perm_elim_erase [lemma, in removetype]
eq_nom_np_erase [lemma, in removetype]
eq_nom_untyped_np_no_perm [lemma, in removetype]
eq_nom_p_erase [lemma, in removetype]
eq_nom_erase [lemma, in removetype]
eq_nom_untyped_np_rm_perm_pos [lemma, in perm]
eq_apply_perm_pos [lemma, in perm]
eq_apply_perm_ut_pos [lemma, in perm]
eq_rm_perm_pos [lemma, in perm]
eq_rm_perm_ut_pos [lemma, in perm]
eq_apply_perm [lemma, in perm]
eq_nom_typed_np_apply_perm [lemma, in perm]
eq_nom_untyped_np_apply_perm [lemma, in perm]
eq_nom_typed_p_apply_perm [lemma, in perm]
eq_nom_untyped_p_apply_perm [lemma, in perm]
eq_perm_elim_apply_perm [lemma, in perm]
eq_perm_ω_apply_perm [lemma, in perm]
eq_perm_apply_perm [lemma, in perm]
eq_rm_perm_bis [lemma, in perm]
eq_rm_perm [lemma, in perm]
eq_expr_get_bot [lemma, in predicates]
eq_expr_eq0' [lemma, in predicates]
eq_expr_eq0 [lemma, in predicates]
eq_expr_stage [lemma, in predicates]
eq_expr_support [lemma, in predicates]
eq_expr_size [lemma, in predicates]
eq_expr_W [lemma, in predicates]
eq_expr_Equivalence [instance, in predicates]
eq_expr [definition, in predicates]
eq_perm_elim_convert [lemma, in normalise]
eq_θ_fr_id [constructor, in normalise]
eq_θ_fr_nil [constructor, in normalise]
eq_θ_fresh [constructor, in normalise]
eq_perm_fresh [inductive, in normalise]
eq0 [definition, in expr]
eq0_proof_typed [lemma, in rm0]
eq0_untyped_refl [lemma, in rm0]
eq0_proof_untyped [lemma, in rm0]
eq0_apply_perm [lemma, in morphisms]
eq0_rm0_u [lemma, in morphisms]
eq0_erase [lemma, in removetype]
eq0' [definition, in expr]
eq0'_get_bot_positive [lemma, in expr]
eq0'_spec [lemma, in expr]
eq0'_rm0_apply_perm [lemma, in morphisms]
eq0'_get_bot_positivet [lemma, in predicates]
eq0'_t_spec [lemma, in predicates]
eq0'_get_bot_positiveu [lemma, in predicates]
eq0'_u_spec [lemma, in predicates]
erase [definition, in morphisms]
erase_apply_perm [lemma, in morphisms]
erase_typed_vers_np [lemma, in removetype]
erase_typed_vers [lemma, in removetype]
expr [inductive, in expr]
expr [library]
ex_ax_eq [definition, in restr_atoms]
F
FFalse [abbreviation, in tools]FFalse [abbreviation, in tools]
FFalse_spec [lemma, in tools]
filter_app [lemma, in atoms_ops]
filter_id [lemma, in atoms_ops]
filter_length [lemma, in atoms_ops]
fresh [definition, in predicates]
freshb [definition, in predicates]
freshb_spec [lemma, in predicates]
fresh_rm_perm [lemma, in morphisms]
fresh_apply_perm [lemma, in morphisms]
fresh_rm0 [lemma, in morphisms]
fresh_type [lemma, in morphisms]
fresh_support [lemma, in predicates]
G
get_bot_spec [lemma, in expr]get_bot [definition, in expr]
get_atom [definition, in sg_to_mlt]
get_new [axiom, in letter]
get_bot_t_spec [lemma, in predicates]
get_bot_u_spec [lemma, in predicates]
good [definition, in theories]
goodNKAmpt [lemma, in theories]
goodNKAmpu [lemma, in theories]
goodNKAnmpt [lemma, in theories]
goodNKAnmpu [lemma, in theories]
goodNKAnspt [lemma, in theories]
goodNKAnspu [lemma, in theories]
goodNKAspt [lemma, in theories]
goodNKAspu [lemma, in theories]
H
has_type_multi_to_single [lemma, in sg_to_mlt]has_type_single_to_multi [lemma, in sg_to_mlt]
has_type_rm_perm_apply_perm [lemma, in morphisms]
has_type_apply_perm [lemma, in morphisms]
has_type [definition, in predicates]
ht_id_eq [instance, in predicates]
ht_bot_eq [instance, in predicates]
ht_equiv_iff [instance, in predicates]
ht_equiv [instance, in predicates]
ht_convert [lemma, in predicates]
I
id [constructor, in expr]id_equiv_lst_eq [instance, in proofs]
id_a_diff_un_NKA_tp [lemma, in theories]
id_a_diff_un_NKA_θtp [lemma, in theories]
id_morph [lemma, in normalise]
if_Atom_eq_dec_neq [lemma, in atoms]
if_Atom_eq_dec_eq [lemma, in atoms]
image [definition, in sg_to_mlt]
image_mlt [lemma, in sg_to_mlt]
Img [definition, in sg_to_mlt]
img_ut_fresh_multi_to_single [lemma, in sg_to_mlt]
img_sg_multi_to_single [lemma, in sg_to_mlt]
inb [definition, in atoms]
inb_spec [lemma, in atoms]
included_th_decidable [lemma, in order]
included_th_PreOrder [instance, in order]
included_th [definition, in order]
incl_p_fun_l [lemma, in order]
incl_p_fun_r [lemma, in order]
incl_p_fun [lemma, in order]
incl_ty_ut_np [lemma, in removetype]
incl_ty_ut [lemma, in removetype]
incl_ut_ty [lemma, in removetype]
incl_lst_b_spec [lemma, in equiv_lst]
incl_lst_b [definition, in equiv_lst]
incl_lst [definition, in equiv_lst]
inf [abbreviation, in proofs]
inf_antisym [instance, in proofs]
inter [definition, in atoms_ops]
inter_length [lemma, in atoms_ops]
inter_incl [instance, in equiv_lst]
inter_equiv [instance, in equiv_lst]
inter_cong [lemma, in equiv_lst]
inverse [definition, in atoms]
inverse_app [lemma, in atoms]
inverse_comp_r [lemma, in atoms]
inverse_comp_l [lemma, in atoms]
inverse_inv [lemma, in atoms]
In_mact [lemma, in atoms_ops]
In_rm [lemma, in atoms_ops]
In_inter [lemma, in atoms_ops]
In_undup [lemma, in atoms_ops]
In_purge [lemma, in atoms_ops]
In_app_iff [lemma, in atoms_ops]
In_cons [lemma, in atoms_ops]
in_X_X [lemma, in restr_atoms]
in_X_spec [lemma, in restr_atoms]
in_X [definition, in restr_atoms]
In_incl [instance, in equiv_lst]
In_equiv [instance, in equiv_lst]
in_double_neg [lemma, in atoms]
is_restr_stable [lemma, in restr_atoms]
is_restr [definition, in restr_atoms]
is_perm_bool_is_perm [lemma, in letter]
is_perm_bool_spec [lemma, in letter]
is_perm_bool [definition, in letter]
is_perm_no_dup_length [lemma, in letter]
is_perm [definition, in letter]
is_model [definition, in order]
K
K [axiom, in expr]kat_s2 [constructor, in proofs]
kat_s1 [constructor, in proofs]
kat_1t [constructor, in proofs]
kat_t1 [constructor, in proofs]
kau_s2 [constructor, in proofs]
kau_s1 [constructor, in proofs]
kau_1t [constructor, in proofs]
kau_t1 [constructor, in proofs]
ka_eq_str_positive [lemma, in proofs]
ka_eq_u_str_positive [lemma, in proofs]
ka_eq_t_str_positive [lemma, in proofs]
ka_eq_no_perm [lemma, in proofs]
ka_eq_u_no_perm [lemma, in proofs]
ka_eq_t_no_perm [lemma, in proofs]
ka_eq_multi [lemma, in proofs]
ka_eq_u_multi [lemma, in proofs]
ka_eq_t_multi [lemma, in proofs]
ka_eq_single [lemma, in proofs]
ka_eq_u_single [lemma, in proofs]
ka_eq_t_single [lemma, in proofs]
ka_eq_untyped [lemma, in proofs]
ka_eq_u_untyped [lemma, in proofs]
ka_eq_type [lemma, in proofs]
ka_eq_t_type [lemma, in proofs]
ka_eq_t [inductive, in proofs]
ka_eq_u [inductive, in proofs]
ka_s4 [constructor, in proofs]
ka_s3 [constructor, in proofs]
ka_impl [inductive, in proofs]
ka_tp [constructor, in proofs]
ka_pt [constructor, in proofs]
ka_pi [constructor, in proofs]
ka_pc [constructor, in proofs]
ka_pp [constructor, in proofs]
ka_tt [constructor, in proofs]
ka_eq [inductive, in proofs]
ka_eq_t_image [lemma, in sg_to_mlt]
ka_eq_u_image [lemma, in sg_to_mlt]
ka_eq_u_eq0 [lemma, in rm0]
ka_eq_t_eq0 [lemma, in rm0]
ka_eq_eq0 [lemma, in rm0]
ka_eq_tu_typed_vers [lemma, in removetype]
ka_eq_typed_vers [lemma, in removetype]
ka_eq_u_support [lemma, in removetype]
ka_eq_support [lemma, in removetype]
ka_eq_tu_erase [lemma, in removetype]
ka_eq_erase [lemma, in removetype]
L
length_support_size [lemma, in expr]Letter [definition, in letter]
letter [library]
le_diff_un_NKA_p [lemma, in theories]
le_diff_un_NKA_θp [lemma, in theories]
M
mact [definition, in atoms_ops]mact_undup [lemma, in atoms_ops]
mact_app_distr [lemma, in atoms_ops]
mact_id1 [lemma, in atoms_ops]
mact_nil [lemma, in atoms_ops]
mact_id2 [lemma, in atoms_ops]
mact_purge [lemma, in atoms_ops]
mact_rm [lemma, in atoms_ops]
mact_inv_l [lemma, in atoms_ops]
mact_inv_r [lemma, in atoms_ops]
mact_comp_app [lemma, in atoms_ops]
mact_length [lemma, in atoms_ops]
mact_elements_equiv_perm [lemma, in equiv_lst]
mact_incl [instance, in equiv_lst]
mact_equiv [instance, in equiv_lst]
mact_cong [lemma, in equiv_lst]
mact_eq_act_eq [lemma, in normalise]
map_φ_inj [lemma, in restr_atoms]
map_φ_rm [lemma, in restr_atoms]
map_φ_mact [lemma, in restr_atoms]
map_ψ_act_φ [lemma, in restr_atoms]
map_ψ_map_φ_act_φ [lemma, in restr_atoms]
map_φ_act [lemma, in restr_atoms]
map_pair_inv [lemma, in restr_atoms]
map_pair [definition, in restr_atoms]
map_act_inv_eq [lemma, in equiv_lst]
map1 [lemma, in equiv_lst]
map2 [lemma, in equiv_lst]
mlt [definition, in predicates]
mlt_single_to_multi [lemma, in sg_to_mlt]
morphisms [library]
multi [definition, in predicates]
multib [definition, in predicates]
multib_spec [lemma, in predicates]
multi_to_single [definition, in sg_to_mlt]
multi_rm_perm [lemma, in morphisms]
multi_apply_perm [lemma, in morphisms]
multi_rm0 [lemma, in morphisms]
multi_typed_vers [lemma, in morphisms]
multi_erase [lemma, in morphisms]
multi_W [lemma, in predicates]
N
Name [axiom, in letter]new_atom [axiom, in letter]
Nice [definition, in normalise]
nice [definition, in normalise]
Nice_NKAspu [lemma, in normalise]
nice_convert_eq [lemma, in normalise]
nice_eq [lemma, in normalise]
nice_NKA_nice [lemma, in normalise]
nice_convert [lemma, in normalise]
NKA [definition, in theories]
NKAmpt [definition, in theories]
NKAmpt_is_model_NKAmt [lemma, in order]
NKAmpt_is_model_NKAnmpt [lemma, in order]
NKAmpu [definition, in theories]
NKAmpu_NKAmpt_eq [lemma, in order]
NKAmpu_is_model_NKAmpt [lemma, in order]
NKAmpu_is_model_NKAmu [lemma, in order]
NKAmpu_is_model_NKAnmpu [lemma, in order]
NKAmt [definition, in theories]
NKAmt_NKAmpt_eq [lemma, in order]
NKAmu [definition, in theories]
NKAmu_NKAmpu_eq [lemma, in order]
NKAnmpt [definition, in theories]
NKAnmpt_NKAmpt_eq [lemma, in order]
NKAnmpt_is_model_NKAmpt [lemma, in order]
NKAnmpt_is_model_NKAnmt [lemma, in order]
NKAnmpu [definition, in theories]
NKAnmpu_NKAmpu_eq [lemma, in order]
NKAnmpu_is_model_NKAmpu [lemma, in order]
NKAnmpu_NKAnmpt_eq [lemma, in order]
NKAnmpu_is_model_NKAnmpt [lemma, in order]
NKAnmpu_is_model_NKAnmu [lemma, in order]
NKAnmt [definition, in theories]
NKAnmt_NKAnmpt_eq [lemma, in order]
NKAnmu [definition, in theories]
NKAnmu_NKAnmpu_eq [lemma, in order]
NKAnspt [definition, in theories]
NKAnspt_NKAspt_eq [lemma, in order]
NKAnspt_is_model_NKAspt [lemma, in order]
NKAnspt_is_model_NKAnst [lemma, in order]
NKAnspu [definition, in theories]
NKAnspu_NKAspu_eq [lemma, in order]
NKAnspu_is_model_NKAspu [lemma, in order]
NKAnspu_NKAnspt_eq [lemma, in order]
NKAnspu_is_model_NKAnspt [lemma, in order]
NKAnspu_is_model_NKAnsu [lemma, in order]
NKAnst [definition, in theories]
NKAnst_NKAnspt_eq [lemma, in order]
NKAnsu [definition, in theories]
NKAnsu_NKAnspu_eq [lemma, in order]
NKAspt [definition, in theories]
NKAspt_is_model_NKAst [lemma, in order]
NKAspt_is_model_NKAnspt [lemma, in order]
NKAspu [definition, in theories]
NKAspu_NKAspt_eq [lemma, in order]
NKAspu_is_model_NKAspt [lemma, in order]
NKAspu_is_model_NKAsu [lemma, in order]
NKAspu_is_model_NKAnspu [lemma, in order]
NKAspu_Nice [lemma, in normalise]
NKAst [definition, in theories]
NKAst_NKAspt_eq [lemma, in order]
NKAsu [definition, in theories]
NKAsu_NKAspu_eq [lemma, in order]
NKA_θp_untyped [lemma, in sg_to_mlt]
NKA_θtp_single [lemma, in sg_to_mlt]
NKA_θp_single [lemma, in sg_to_mlt]
NKA_θtp_image [lemma, in sg_to_mlt]
NKA_θp_image [lemma, in sg_to_mlt]
NKA_θtp_NKA_tp_rm_perm_apply_perm [lemma, in theories]
NKA_θp_NKA_p_rm_perm_apply_perm [lemma, in theories]
NKA_tp_NKA_θtp [lemma, in theories]
NKA_p'_NKA_p_eq [lemma, in theories]
NKA_tp'_NKA_tp_eq [lemma, in theories]
NKA_tp_Np [lemma, in theories]
NKA_p_Np [lemma, in theories]
NKA_pos [lemma, in theories]
NKA_typed_vers' [lemma, in theories]
NKA_erase' [lemma, in theories]
NKA_p'_support [lemma, in theories]
NKA_p_support [lemma, in theories]
NKA_θp_support [lemma, in theories]
NKA_p_rm0 [lemma, in theories]
NKA_θp_rm0 [lemma, in theories]
NKA_tp_rm0 [lemma, in theories]
NKA_θtp_rm0 [lemma, in theories]
NKA_eq0 [lemma, in theories]
NKA_p_eq0 [lemma, in theories]
NKA_θ_eq0 [lemma, in theories]
NKA_θp_eq0 [lemma, in theories]
NKA_t_eq0 [lemma, in theories]
NKA_tp_eq0 [lemma, in theories]
NKA_θt_eq0 [lemma, in theories]
NKA_θtp_eq0 [lemma, in theories]
NKA_p'_untyped [lemma, in theories]
NKA_tp'_has_type [lemma, in theories]
NKA_untyped [lemma, in theories]
NKA_p_untyped [lemma, in theories]
NKA_θ_untyped [lemma, in theories]
NKA_θp_untyped [lemma, in theories]
NKA_t_has_type [lemma, in theories]
NKA_tp_has_type [lemma, in theories]
NKA_θt_has_type [lemma, in theories]
NKA_θtp_has_type [lemma, in theories]
NKA_θtp_str_positive [lemma, in theories]
NKA_θp_str_positive [lemma, in theories]
NKA_tp_str_positive [lemma, in theories]
NKA_p_str_positive [lemma, in theories]
NKA_θtp_multi [lemma, in theories]
NKA_θp_multi [lemma, in theories]
NKA_tp_multi [lemma, in theories]
NKA_p_multi [lemma, in theories]
NKA_θtp_single [lemma, in theories]
NKA_θp_single [lemma, in theories]
NKA_tp_single [lemma, in theories]
NKA_p_single [lemma, in theories]
NKA_p' [definition, in theories]
NKA_tp' [definition, in theories]
NKA_p [definition, in theories]
NKA_t [definition, in theories]
NKA_tp [definition, in theories]
NKA_θ [definition, in theories]
NKA_θp [definition, in theories]
NKA_θt [definition, in theories]
NKA_θtp [definition, in theories]
NKA_NKA_θ_m [lemma, in order]
NKA_NKA_θ_s [lemma, in order]
NKA_t_NKA_θt_fun [lemma, in order]
NKA_NKA_θ_fun [lemma, in order]
NKA_θ_NKA_m [lemma, in order]
NKA_θ_NKA_s [lemma, in order]
NKA_θt_NKA_t_fun [lemma, in order]
NKA_θ_NKA_fun [lemma, in order]
NKA_θtp_NKA_θp_m [lemma, in order]
NKA_tp_NKA_p_m [lemma, in order]
NKA_θtp_NKA_θp_s [lemma, in order]
NKA_tp_NKA_p_s [lemma, in order]
NKA_θp_NKA_θtp_m [lemma, in order]
NKA_p_NKA_tp_m [lemma, in order]
NKA_θp_NKA_θtp_s [lemma, in order]
NKA_p_NKA_tp_s [lemma, in order]
NKA_tp_NKA_p [lemma, in order]
NKA_p_NKA_tp_precise [lemma, in order]
NKA_p_NKA_tp [lemma, in order]
NKA_θtp_NKA_θp_fun [lemma, in order]
NKA_θp_NKA_θtp_precise [lemma, in order]
NKA_θp_NKA_θtp_fun [lemma, in order]
NKA_θtp_incl_NKA_θt_m [lemma, in order]
NKA_θtp_incl_NKA_θt_s [lemma, in order]
NKA_θtp_incl_NKA_θt [lemma, in order]
NKA_θt_incl_NKA_θtp_m [lemma, in order]
NKA_θt_incl_NKA_θtp_s [lemma, in order]
NKA_θt_incl_NKA_θtp [lemma, in order]
NKA_θt_NKA_θtp [lemma, in order]
NKA_θp_incl_NKA_θ_m [lemma, in order]
NKA_θp_incl_NKA_θ_s [lemma, in order]
NKA_θp_incl_NKA_θ [lemma, in order]
NKA_θ_incl_NKA_θp_m [lemma, in order]
NKA_θ_incl_NKA_θp_s [lemma, in order]
NKA_θ_incl_NKA_θp [lemma, in order]
NKA_θ_NKA_θp [lemma, in order]
NKA_tp_incl_NKA_tns [lemma, in order]
NKA_tp_incl_NKA_tnm [lemma, in order]
NKA_tp_incl_NKA_t [lemma, in order]
NKA_t_incl_NKA_tp_ns [lemma, in order]
NKA_t_incl_NKA_tp_nm [lemma, in order]
NKA_t_incl_NKA_tp [lemma, in order]
NKA_t_NKA_tp [lemma, in order]
NKA_p_incl_NKA_ns [lemma, in order]
NKA_p_incl_NKA_nm [lemma, in order]
NKA_p_incl_NKA [lemma, in order]
NKA_incl_NKA_p_ns [lemma, in order]
NKA_incl_NKA_p_nm [lemma, in order]
NKA_incl_NKA_p [lemma, in order]
NKA_NKA_p [lemma, in order]
NKA_nice_stronger_NKA_θp [lemma, in normalise]
NKA_nice [definition, in normalise]
NKA' [definition, in theories]
NKA'_NKA_θp [lemma, in theories]
NKA'_pos [lemma, in theories]
NKA'_support [lemma, in theories]
NKA'_untyped [lemma, in theories]
NKAθ_typed_vers [lemma, in theories]
NKAθ_erase [lemma, in theories]
NoDup_undup_eq [lemma, in atoms_ops]
NoDup_mact [lemma, in atoms_ops]
NoDup_app_inv [lemma, in atoms_ops]
NoDup_app [lemma, in atoms_ops]
NoDup_rm [lemma, in atoms_ops]
NoDup_inter [lemma, in atoms_ops]
NoDup_purge [lemma, in atoms_ops]
NoDup_filter [lemma, in atoms_ops]
NoDup_cons_iff [lemma, in atoms_ops]
NoDup_undup [lemma, in atoms_ops]
NoDup_map_φ [lemma, in restr_atoms]
nodup_bool_spec [lemma, in letter]
nodup_bool [definition, in letter]
normalise [library]
no_perm_rm_perm [lemma, in morphisms]
no_perm_rm_perm_id [lemma, in morphisms]
no_perm_apply_perm [lemma, in morphisms]
no_perm_rm0 [lemma, in morphisms]
no_perm_typed_vers [lemma, in morphisms]
no_perm_erase [lemma, in morphisms]
no_perm_W [lemma, in predicates]
no_permb_spec [lemma, in predicates]
no_permb [definition, in predicates]
no_perm [definition, in predicates]
np [definition, in predicates]
O
one_star_is_one_t [lemma, in proofs]one_star_is_one_u [lemma, in proofs]
order [library]
or_and_distr [lemma, in tools]
or_rel_stronger_r [lemma, in tools]
or_rel_stronger_l [lemma, in tools]
or_rel_stronger_stronger_stronger [instance, in tools]
or_rel_eq_rel_eq_rel_eq_rel [instance, in tools]
or_rel [definition, in tools]
P
perm [definition, in atoms]perm [library]
perm_fun_lst_mact [lemma, in restr_atoms]
perm_fun_lst [definition, in restr_atoms]
perm_p_pinv_eq_nil [lemma, in atoms]
perm_pinv_p_eq_nil [lemma, in atoms]
perm_a_a_eq_nil [lemma, in atoms]
perm_bij [lemma, in atoms]
perm_inj [lemma, in atoms]
plus [constructor, in expr]
plus_eq [instance, in proofs]
po [definition, in predicates]
poa_poa_single_to_multi [lemma, in sg_to_mlt]
poly [section, in expr]
poly [section, in morphisms]
poly.bounded_τ [variable, in expr]
poly.bounded_τ [variable, in morphisms]
poly.K_not_zero [variable, in expr]
poly.K_not_zero [variable, in morphisms]
positive [definition, in predicates]
positiveb [definition, in predicates]
positiveb_spec [lemma, in predicates]
positive_rm_perm [lemma, in morphisms]
positive_apply_perm [lemma, in morphisms]
positive_rm0_id [lemma, in morphisms]
positive_rm0 [lemma, in morphisms]
positive_or_nul_rm0 [lemma, in morphisms]
positive_typed_vers [lemma, in morphisms]
positive_erase [lemma, in morphisms]
pos_rev_rm0 [lemma, in order]
pos_disj [lemma, in predicates]
po_po_single_to_multi [lemma, in sg_to_mlt]
po_to_str_rm0 [lemma, in order]
predicate [definition, in tools]
predicates [library]
pre_incl_lst [instance, in equiv_lst]
proofs [library]
proper_and_split [lemma, in tools]
proper_or_split [lemma, in tools]
proper_stronger_r [lemma, in tools]
proper_stronger_l [lemma, in tools]
proper_S_le [instance, in tools]
proper_plus_le [instance, in tools]
proper_ex_ax_eq [lemma, in restr_atoms]
proper_eq [lemma, in proofs]
Proper_ty_img_eq [lemma, in sg_to_mlt]
Proper_ty_img_ax [lemma, in sg_to_mlt]
Proper_ut_img_eq [lemma, in sg_to_mlt]
Proper_ut_img_ax [lemma, in sg_to_mlt]
Proper_ty_sg_eq [lemma, in sg_to_mlt]
Proper_ty_sg_ax [lemma, in sg_to_mlt]
Proper_ut_sg_eq [lemma, in sg_to_mlt]
Proper_ut_sg_ax [lemma, in sg_to_mlt]
purge [definition, in atoms_ops]
purge_rm [lemma, in atoms_ops]
purge_app [lemma, in atoms_ops]
purge_l_l [lemma, in atoms_ops]
purge_cons [lemma, in atoms_ops]
purge_nil [lemma, in atoms_ops]
purge_length [lemma, in atoms_ops]
purge_l_m_nil [lemma, in equiv_lst]
purge_incl [instance, in equiv_lst]
purge_eq [instance, in equiv_lst]
purge_equiv [instance, in equiv_lst]
purge_cong [lemma, in equiv_lst]
R
reflect3 [inductive, in tools]rel [definition, in tools]
rel_and_pred [lemma, in tools]
rel_eq_pred_eq_rel [instance, in tools]
remain_Sp [lemma, in proofs]
remain_Np [lemma, in proofs]
remain_Mlt [lemma, in proofs]
remain_Sg [lemma, in proofs]
remain_Ut [lemma, in proofs]
remain_Ty [lemma, in proofs]
removetype [library]
restr_perm_is_restr [lemma, in restr_atoms]
restr_ax_eq_ax_eq [lemma, in restr_atoms]
restr_ax [definition, in restr_atoms]
restr_perm_map_φ [lemma, in restr_atoms]
restr_expr [definition, in restr_atoms]
restr_perm_mact [lemma, in restr_atoms]
restr_list [definition, in restr_atoms]
restr_perm_act [lemma, in restr_atoms]
restr_perm [definition, in restr_atoms]
restr_atoms [library]
rm [definition, in atoms_ops]
rm_cons [lemma, in atoms_ops]
rm_id [lemma, in atoms_ops]
rm_purge [lemma, in atoms_ops]
rm_app [lemma, in atoms_ops]
rm_comm [lemma, in atoms_ops]
rm_length [lemma, in atoms_ops]
rm_perm_apply_perm_swap [lemma, in morphisms]
rm_perm_size [lemma, in morphisms]
rm_perm [definition, in morphisms]
rm_cons_eq' [lemma, in equiv_lst]
rm_cons_eq [lemma, in equiv_lst]
rm_incl [instance, in equiv_lst]
rm_equiv [instance, in equiv_lst]
rm_cong [lemma, in equiv_lst]
rm0 [definition, in morphisms]
rm0 [library]
rm0_eq_nom_typed_np [lemma, in rm0]
rm0_eq_nom_typed_p [lemma, in rm0]
rm0_eq_nom_typed [lemma, in rm0]
rm0_eq_nom_untyped [lemma, in rm0]
rm0_eq_nom_untyped_np [lemma, in rm0]
rm0_eq_nom_untyped_p [lemma, in rm0]
rm0_u_ka_eq [lemma, in rm0]
rm0_t_ka_eq [lemma, in rm0]
rm0_eq_perm_ω [lemma, in rm0]
rm0_eq_perm_elim [lemma, in rm0]
rm0_eq_ω_smpl_typed [lemma, in rm0]
rm0_eq_ν_smpl_untyped [lemma, in rm0]
rm0_eq_ν_smpl_typed [lemma, in rm0]
rm0_zero_eq_t [lemma, in rm0]
rm0_zero_eq_u [lemma, in rm0]
rm0_eq_typed [lemma, in rm0]
rm0_eq_untyped [lemma, in rm0]
rm0_apply_perm [lemma, in morphisms]
rm0_eq0_get_bot [lemma, in morphisms]
rm0_inv_apply_perm [lemma, in morphisms]
rm0_involutive [lemma, in morphisms]
r3_true [constructor, in tools]
r3_Some [constructor, in tools]
r3_false [constructor, in tools]
S
s [section, in tools]sg [definition, in predicates]
sg_image_single_to_multi [lemma, in sg_to_mlt]
sg_to_mlt [library]
single [definition, in predicates]
singleb [definition, in predicates]
singleb_spec [lemma, in predicates]
single_to_multi [definition, in sg_to_mlt]
single_rm_perm [lemma, in morphisms]
single_apply_perm [lemma, in morphisms]
single_rm0 [lemma, in morphisms]
single_typed_vers [lemma, in morphisms]
single_erase [lemma, in morphisms]
single_multi_ty [lemma, in order]
single_multi_ut [lemma, in order]
single_W [lemma, in predicates]
single_support_le_size [lemma, in predicates]
size [definition, in expr]
size_W [lemma, in expr]
size_non_zero [lemma, in expr]
size_single_to_multi [lemma, in sg_to_mlt]
size_rm0 [lemma, in morphisms]
size_typed_vers [lemma, in morphisms]
size_erase [lemma, in morphisms]
sp [definition, in predicates]
stage [definition, in expr]
stage_has_type [lemma, in predicates]
star [constructor, in expr]
star_eq [instance, in proofs]
stronger [definition, in tools]
stronger_Preorder [instance, in tools]
stronger_Ty_ka_eq_t [lemma, in proofs]
stronger_Ty_zero_ka_t [lemma, in proofs]
stronger_eq_or_rel_r [lemma, in proofs]
stronger_eq_or_rel_l [lemma, in proofs]
stronger_ax_eq [lemma, in proofs]
stronger_ax_proof [instance, in proofs]
stronger_Ty_eq_nom_typed_np [lemma, in rm0]
str_positive_rm_perm [lemma, in morphisms]
str_positive_apply_perm [lemma, in morphisms]
str_positive_rm0_id [lemma, in morphisms]
str_positive_rm0 [lemma, in morphisms]
str_positive_typed_vers [lemma, in morphisms]
str_positive_erase [lemma, in morphisms]
str_pos_rev_rm0 [lemma, in order]
str_positive_eq0 [lemma, in removetype]
str_positive_W [lemma, in predicates]
str_positive_positive [lemma, in predicates]
str_positiveb_spec [lemma, in predicates]
str_positiveb [definition, in predicates]
str_positive [definition, in predicates]
str_positive_NKA_nice [lemma, in normalise]
support [definition, in expr]
support_or_diff_NKA_θp [lemma, in theories]
support_or_diff_NKA_p [lemma, in theories]
support_apply_perm [lemma, in morphisms]
support_min_type [lemma, in morphisms]
switch_NKA_p_NKA' [lemma, in theories]
switch_NKA'_NKA_p [lemma, in theories]
s.T [variable, in tools]
_ ↔ _ [notation, in tools]
_ ^2 [notation, in tools]
_ ⊗ _ [notation, in tools]
_ ⇔ _ [notation, in tools]
_ ∧ _ [notation, in tools]
_ ∨ _ [notation, in tools]
_ ⇒ _ [notation, in tools]
T
technical [lemma, in order]theories [library]
times [constructor, in expr]
times_eq [instance, in proofs]
tools [library]
transfer_perm [definition, in letter]
transfer_fun_proper_iff_2 [instance, in order]
transfer_fun_proper_iff_1 [instance, in order]
transfer_fun_proper_iff [instance, in order]
transfer_fun_proper_eq_impl_rev [instance, in order]
transfer_fun_proper_eq_impl [instance, in order]
transfer_fun_proper_str_impl [instance, in order]
transfer_fun_included_th [lemma, in order]
transfer_fun_preorder [lemma, in order]
transfer_fun [definition, in order]
TTrue [abbreviation, in tools]
TTrue [abbreviation, in tools]
TTrue_spec [lemma, in tools]
TTrue_unit_r [lemma, in order]
TTrue_unit_l [lemma, in order]
ty [definition, in predicates]
TyEq [definition, in theories]
typed [definition, in predicates]
typedb [definition, in predicates]
typedb_spec [lemma, in predicates]
typed_equiv_rm0 [lemma, in rm0]
typed_impl_rm0 [lemma, in rm0]
typed_vers_apply_perm [lemma, in morphisms]
typed_rm0 [lemma, in morphisms]
typed_version_support_type [lemma, in morphisms]
typed_version_erase [lemma, in morphisms]
typed_vers_size [lemma, in morphisms]
typed_vers [definition, in morphisms]
typed_stage_has_type [lemma, in predicates]
type_W' [lemma, in predicates]
type_eq_cons [lemma, in predicates]
type_unicity [lemma, in predicates]
ty_multi_to_single_single_to_multi [lemma, in sg_to_mlt]
ty_multi_to_single [lemma, in sg_to_mlt]
ty_ty_single_to_multi [lemma, in sg_to_mlt]
ty_Single_to_Multi [lemma, in order]
Ty_eq_perm_ω_W [lemma, in removetype]
ty' [definition, in predicates]
ty'_or_diff_NKA_θtp [lemma, in theories]
ty'_or_diff_NKA_tp [lemma, in theories]
U
un [constructor, in expr]undup [definition, in atoms_ops]
undup_rm [lemma, in atoms_ops]
undup_app [lemma, in atoms_ops]
undup_purge [lemma, in atoms_ops]
undup_length [lemma, in atoms_ops]
undup_equiv [instance, in equiv_lst]
undup_equiv_lst [lemma, in equiv_lst]
untyped [definition, in predicates]
untypedb [definition, in predicates]
untypedb_spec [lemma, in predicates]
untyped_equiv_rm0 [lemma, in rm0]
untyped_impl_rm0 [lemma, in rm0]
untyped_rm_perm [lemma, in morphisms]
untyped_apply_perm [lemma, in morphisms]
untyped_rm0 [lemma, in morphisms]
untyped_erase [lemma, in morphisms]
untyped_NKA_nice [lemma, in normalise]
ut [definition, in predicates]
ut_multi_to_single_single_to_multi [lemma, in sg_to_mlt]
ut_multi_to_single [lemma, in sg_to_mlt]
ut_single_fresh_single_to_multi [lemma, in sg_to_mlt]
ut_ut_single_to_multi [lemma, in sg_to_mlt]
ut_Single_to_Multi [lemma, in order]
V
var [constructor, in expr]vat [constructor, in expr]
W
W [definition, in expr]W_app [lemma, in expr]
W_apply_perm [lemma, in morphisms]
W_erase [lemma, in morphisms]
W_ω_extract [lemma, in removetype]
W_equiv_lst [lemma, in removetype]
W_ω_exchange [lemma, in removetype]
W_eq [instance, in removetype]
W_type [lemma, in predicates]
X
X [definition, in restr_atoms]Z
zero [constructor, in expr]zero_nom_t_apply_φ [lemma, in restr_atoms]
zero_nom_u_apply_φ [lemma, in restr_atoms]
zero_perm_t_apply_φ [lemma, in restr_atoms]
zero_perm_u_apply_φ [lemma, in restr_atoms]
zero_ka_t_apply_φ [lemma, in restr_atoms]
zero_ka_u_apply_φ [lemma, in restr_atoms]
zero_star_is_one_t [lemma, in proofs]
zero_star_is_one_u [lemma, in proofs]
zero_nom_u_str_positive [lemma, in proofs]
zero_nom_t_str_positive [lemma, in proofs]
zero_nom_u_no_perm [lemma, in proofs]
zero_nom_t_no_perm [lemma, in proofs]
zero_perm_u_multi [lemma, in proofs]
zero_perm_t_multi [lemma, in proofs]
zero_nom_u_multi [lemma, in proofs]
zero_nom_t_multi [lemma, in proofs]
zero_perm_u_single [lemma, in proofs]
zero_perm_t_single [lemma, in proofs]
zero_nom_u_single [lemma, in proofs]
zero_nom_t_single [lemma, in proofs]
zero_nom_u_untyped [lemma, in proofs]
zero_perm_u_untyped [lemma, in proofs]
zero_ka_u_untyped [lemma, in proofs]
zero_nom_t_type [lemma, in proofs]
zero_perm_t_type [lemma, in proofs]
zero_ka_t_type [lemma, in proofs]
zero_nom_u_derivable [lemma, in proofs]
zero_eq_u [abbreviation, in proofs]
zero_eq_t [abbreviation, in proofs]
zero_nom_t [inductive, in proofs]
zero_nom_u [inductive, in proofs]
zero_perm_t [inductive, in proofs]
zero_perm_u [inductive, in proofs]
zero_t_0t [constructor, in proofs]
zero_t_t0 [constructor, in proofs]
zero_t_p0 [constructor, in proofs]
zero_ka_t [inductive, in proofs]
zero_u_0t [constructor, in proofs]
zero_u_t0 [constructor, in proofs]
zero_u_p0 [constructor, in proofs]
zero_ka_u [inductive, in proofs]
zero_eq_t_eq0 [lemma, in rm0]
zero_eq_u_eq0 [lemma, in rm0]
zero_nom_u_eq0 [lemma, in rm0]
zero_nom_t_eq0 [lemma, in rm0]
zero_perm_u_eq0 [lemma, in rm0]
zero_perm_t_eq0 [lemma, in rm0]
zero_ka_u_eq0 [lemma, in rm0]
zero_ka_t_eq0 [lemma, in rm0]
zero_diff_un_NKA_tp [lemma, in theories]
zero_diff_un_NKA_p [lemma, in theories]
zero_diff_un_NKA_θtp [lemma, in theories]
zero_diff_un_NKA_θp [lemma, in theories]
zero_perm_t_apply_perm [lemma, in perm]
zero_perm_u_apply_perm [lemma, in perm]
other
[ _ , _ ] (list_scope) [notation, in tools]_ ⧓ _ [notation, in atoms_ops]
_ ∩ _ [notation, in atoms_ops]
_ -- _ [notation, in atoms_ops]
_ ^* [notation, in expr]
_ · _ [notation, in expr]
_ + _ [notation, in expr]
_ ↔ _ [notation, in tools]
_ ^2 [notation, in tools]
_ ⊗ _ [notation, in tools]
_ ⇔ _ [notation, in tools]
_ ∧ _ [notation, in tools]
_ ∨ _ [notation, in tools]
_ ⇒ _ [notation, in tools]
_ ∘ _ [notation, in tools]
_ ⊢ _ ≤ _ [notation, in proofs]
_ ⊢ _ ≡ _ [notation, in proofs]
_ =* _ [notation, in proofs]
_ ≃ _ [notation, in letter]
_ • _ [notation, in morphisms]
_ ⊲ _ [notation, in order]
_ ⊩ _ → _ [notation, in order]
_ ≡≡ _ [notation, in order]
_ << _ [notation, in order]
_ ⊆ _ [notation, in equiv_lst]
_ ≈ _ [notation, in equiv_lst]
_ #' _ [notation, in predicates]
_ # _ [notation, in predicates]
_ ⊨ _ [notation, in predicates]
_ == _ [notation, in predicates]
_ ≌ _ [notation, in atoms]
_ ⋆ [notation, in atoms]
_ ⋈ _ [notation, in atoms]
$ _ [notation, in sg_to_mlt]
0 [notation, in expr]
1 [notation, in expr]
‹ _ › _ [notation, in expr]
⊥ _ [notation, in expr]
〈 _ 〉 [notation, in atoms_ops]
⎡ _ ⎤ [notation, in morphisms]
⎣ _ ⎦ [notation, in morphisms]
£ _ [notation, in sg_to_mlt]
α [axiom, in sg_to_mlt]
θ [constructor, in expr]
θ_eq [instance, in proofs]
λ [axiom, in sg_to_mlt]
ν [constructor, in expr]
ν_eq [instance, in proofs]
τ [definition, in letter]
τ_λ [axiom, in sg_to_mlt]
τ_spec [lemma, in letter]
τ_nm_spec [axiom, in letter]
τ_nm [axiom, in letter]
φ [variable, in restr_atoms]
φ_lst_incl_mact [lemma, in restr_atoms]
φ_lst_act [lemma, in restr_atoms]
φ_inv [lemma, in restr_atoms]
φ_in_X [lemma, in restr_atoms]
φ_X [lemma, in restr_atoms]
φ_inj [lemma, in restr_atoms]
ψ [variable, in restr_atoms]
ψ_inj_implies_φ_surj [lemma, in restr_atoms]
ψ_surj [lemma, in restr_atoms]
ψ_φ_id [variable, in restr_atoms]
ω [constructor, in expr]
ω_eq [instance, in proofs]
Notation Index
S
_ ↔ _ [in tools]_ ^2 [in tools]
_ ⊗ _ [in tools]
_ ⇔ _ [in tools]
_ ∧ _ [in tools]
_ ∨ _ [in tools]
_ ⇒ _ [in tools]
other
[ _ , _ ] (list_scope) [in tools]_ ⧓ _ [in atoms_ops]
_ ∩ _ [in atoms_ops]
_ -- _ [in atoms_ops]
_ ^* [in expr]
_ · _ [in expr]
_ + _ [in expr]
_ ↔ _ [in tools]
_ ^2 [in tools]
_ ⊗ _ [in tools]
_ ⇔ _ [in tools]
_ ∧ _ [in tools]
_ ∨ _ [in tools]
_ ⇒ _ [in tools]
_ ∘ _ [in tools]
_ ⊢ _ ≤ _ [in proofs]
_ ⊢ _ ≡ _ [in proofs]
_ =* _ [in proofs]
_ ≃ _ [in letter]
_ • _ [in morphisms]
_ ⊲ _ [in order]
_ ⊩ _ → _ [in order]
_ ≡≡ _ [in order]
_ << _ [in order]
_ ⊆ _ [in equiv_lst]
_ ≈ _ [in equiv_lst]
_ #' _ [in predicates]
_ # _ [in predicates]
_ ⊨ _ [in predicates]
_ == _ [in predicates]
_ ≌ _ [in atoms]
_ ⋆ [in atoms]
_ ⋈ _ [in atoms]
$ _ [in sg_to_mlt]
0 [in expr]
1 [in expr]
‹ _ › _ [in expr]
⊥ _ [in expr]
〈 _ 〉 [in atoms_ops]
⎡ _ ⎤ [in morphisms]
⎣ _ ⎦ [in morphisms]
£ _ [in sg_to_mlt]
Variable Index
P
poly.bounded_τ [in expr]poly.bounded_τ [in morphisms]
poly.K_not_zero [in expr]
poly.K_not_zero [in morphisms]
S
s.T [in tools]other
φ [in restr_atoms]ψ [in restr_atoms]
ψ_φ_id [in restr_atoms]
Library Index
A
atomsatoms_ops
E
equiv_lstexpr
L
letterM
morphismsN
normaliseO
orderP
permpredicates
proofs
R
removetyperestr_atoms
rm0
S
sg_to_mltT
theoriestools
Lemma Index
A
act_comp_app [in atoms]act_nil [in atoms]
and_stronger_l [in tools]
and_or_distr [in tools]
apply_fun_morph [in restr_atoms]
apply_ψ_φ_id [in restr_atoms]
apply_fun_ext [in restr_atoms]
apply_fun_id [in restr_atoms]
apply_fun_comp [in restr_atoms]
apply_perm_eq [in restr_atoms]
apply_φ_apply_perm_p [in restr_atoms]
apply_φ_eq_ax [in restr_atoms]
apply_perm_app [in restr_atoms]
apply_φ_apply_perm [in restr_atoms]
apply_φ_fresh [in restr_atoms]
apply_φ_stage [in restr_atoms]
apply_φ_support [in restr_atoms]
apply_φ_eq_expr [in restr_atoms]
apply_φ_positive [in restr_atoms]
apply_φ_str_positive [in restr_atoms]
apply_φ_has_type [in restr_atoms]
apply_φ_untyped [in restr_atoms]
apply_φ_single [in restr_atoms]
apply_φ_multi [in restr_atoms]
apply_φ_no_perm [in restr_atoms]
apply_φ_restr [in restr_atoms]
apply_perm_id [in morphisms]
apply_perm_nil [in morphisms]
apply_perm_has_type [in morphisms]
apply_perm_size [in morphisms]
apply_perm_var_equiv_perm_eq_letter [in morphisms]
apply_perm_var_eq_letter [in morphisms]
apply_perm_var_equiv_perm [in morphisms]
apply_perm_var_app [in morphisms]
apply_perm_var_τ [in morphisms]
apply_perm_var_bis [in morphisms]
apply_perm_θ_u [in perm]
apply_perm_θ_t [in perm]
apply_perm_equiv_perm [in perm]
app_length_eq [in restr_atoms]
app_com [in equiv_lst]
app_l_l [in equiv_lst]
app_cong [in equiv_lst]
assoc_or_rel1 [in tools]
Atom_eq_dec [in atoms]
at_diff_un_NKA_p [in theories]
at_diff_un_NKA_θp [in theories]
augm_transfer2 [in order]
augm_transfer' [in order]
augm_transfer [in order]
aux [in restr_atoms]
aux2 [in restr_atoms]
ax_eq_restr_ax_eq [in restr_atoms]
B
bequiv_perm_spec [in equiv_lst]beq_letter_spec [in letter]
beq_expr_spec [in predicates]
beq_perm_spec [in atoms]
beq_list_spec [in atoms]
beq_neq_atom [in atoms]
beq_neq_atom1 [in atoms]
beq_eq_atom [in atoms]
beq_atom_spec [in atoms]
C
can_var_length [in normalise]can_var_NoDup [in normalise]
cons_rm_eq' [in equiv_lst]
cons_rm_eq [in equiv_lst]
cons_cong [in equiv_lst]
cons_comm [in equiv_lst]
convert_morph [in normalise]
convert_eq2 [in normalise]
convert_eq [in normalise]
convert_fresh [in normalise]
convert_multi [in normalise]
convert_single [in normalise]
convert_str_positive [in normalise]
convert_untyped [in normalise]
convert_eq_perm [in normalise]
convert_involutive [in normalise]
conv_lst_inv [in normalise]
conv_can_var [in normalise]
conv_lst [in normalise]
D
decidable_no_perm [in predicates]decidable_single [in predicates]
decidable_multi [in predicates]
decidable_positive [in predicates]
decidable_str_positive [in predicates]
decidable_untyped [in predicates]
decidable_typed [in predicates]
derivable_axioms [in proofs]
disjoint_purge [in atoms_ops]
disjoint_com [in atoms_ops]
disjoint_In [in atoms_ops]
E
elements_In [in restr_atoms]elements_map_pair [in restr_atoms]
elements_in_mact [in equiv_lst]
elements_act_in_equiv [in equiv_lst]
elements_inv_eq [in equiv_lst]
elements_app [in equiv_lst]
elements_inv_mact [in equiv_lst]
elements_inv_act [in equiv_lst]
eqt_ν1 [in proofs]
equiv_perm_map_ψ [in restr_atoms]
equiv_perm_map_φ [in restr_atoms]
equiv_lst_b_spec [in equiv_lst]
equiv_perm_trans [in atoms]
equiv_perm_sym [in atoms]
equiv_perm_refl [in atoms]
equiv_lst_length_undup [in normalise]
eq_nom_typed_apply_φ [in restr_atoms]
eq_nom_typed_np_apply_φ [in restr_atoms]
eq_nom_typed_p_apply_φ [in restr_atoms]
eq_nom_untyped_apply_φ [in restr_atoms]
eq_nom_untyped_np_apply_φ [in restr_atoms]
eq_nom_untyped_p_apply_φ [in restr_atoms]
eq_ω_smpl_apply_φ [in restr_atoms]
eq_ν_smpl_apply_φ [in restr_atoms]
eq_perm_elim_apply_φ [in restr_atoms]
eq_perm_ω_apply_φ [in restr_atoms]
eq_perm_apply_φ [in restr_atoms]
eq_str_positive [in proofs]
eq_perm_str_positive [in proofs]
eq_perm_ω_str_positive [in proofs]
eq_ν_smpl_str_positive [in proofs]
eq_ω_smpl_str_positive [in proofs]
eq_nom_untyped_np_str_positive [in proofs]
eq_nom_typed_np_str_positive [in proofs]
eq_nom_untyped_str_positive [in proofs]
eq_nom_typed_str_positive [in proofs]
eq_no_perm [in proofs]
eq_perm_no_perm [in proofs]
eq_perm_ω_no_perm [in proofs]
eq_ν_smpl_no_perm [in proofs]
eq_ω_smpl_no_perm [in proofs]
eq_nom_untyped_np_no_perm [in proofs]
eq_nom_typed_np_no_perm [in proofs]
eq_nom_untyped_no_perm [in proofs]
eq_nom_typed_no_perm [in proofs]
eq_multi [in proofs]
eq_perm_multi [in proofs]
eq_perm_ω_multi [in proofs]
eq_perm_elim_multi [in proofs]
eq_ν_smpl_multi [in proofs]
eq_ω_smpl_multi [in proofs]
eq_nom_untyped_p_multi [in proofs]
eq_nom_untyped_np_multi [in proofs]
eq_nom_untyped_multi [in proofs]
eq_nom_typed_p_multi [in proofs]
eq_nom_typed_np_multi [in proofs]
eq_nom_typed_multi [in proofs]
eq_single [in proofs]
eq_perm_single [in proofs]
eq_perm_ω_single [in proofs]
eq_perm_elim_single [in proofs]
eq_ν_smpl_single [in proofs]
eq_ω_smpl_single [in proofs]
eq_nom_untyped_p_single [in proofs]
eq_nom_untyped_np_single [in proofs]
eq_nom_untyped_single [in proofs]
eq_nom_typed_p_single [in proofs]
eq_nom_typed_np_single [in proofs]
eq_nom_typed_single [in proofs]
eq_untyped [in proofs]
eq_ω_smpl_untyped [in proofs]
eq_ν_smpl_untyped [in proofs]
eq_perm_ω_untyped [in proofs]
eq_perm_untyped [in proofs]
eq_perm_elim_untyped [in proofs]
eq_nom_untyped_p_untyped [in proofs]
eq_nom_untyped_np_untyped [in proofs]
eq_nom_untyped_untyped [in proofs]
eq_type [in proofs]
eq_ω_smpl_type [in proofs]
eq_ν_smpl_type [in proofs]
eq_perm_ω_type [in proofs]
eq_perm_type [in proofs]
eq_perm_elim_type [in proofs]
eq_nom_typed_type [in proofs]
eq_nom_typed_p_type [in proofs]
eq_nom_typed_np_type [in proofs]
eq_expr_eq [in proofs]
eq_refl [in proofs]
eq_NKA_θp_untyped [in sg_to_mlt]
eq_NKA_θtp_single [in sg_to_mlt]
eq_NKA_θp_single [in sg_to_mlt]
eq_NKA_θtp_image [in sg_to_mlt]
eq_NKA_θp_image [in sg_to_mlt]
eq_nom_typed_p_image [in sg_to_mlt]
eq_nom_untyped_p_image [in sg_to_mlt]
eq_perm_elim_image [in sg_to_mlt]
eq_perm_image [in sg_to_mlt]
eq_nom_typed_image [in sg_to_mlt]
eq_nom_untyped_image [in sg_to_mlt]
eq_ν_smpl_image [in sg_to_mlt]
eq_letter_τ [in letter]
eq_perm_ω_eq0 [in rm0]
eq_perm_eq0 [in rm0]
eq_ω_smpl_eq0 [in rm0]
eq_ν_smpl_eq0 [in rm0]
eq_perm_elim_eq0 [in rm0]
eq_nom_untyped_eq0 [in rm0]
eq_nom_untyped_np_eq0 [in rm0]
eq_nom_untyped_p_eq0 [in rm0]
eq_nom_typed_eq0 [in rm0]
eq_nom_typed_np_eq0 [in rm0]
eq_nom_typed_p_eq0 [in rm0]
eq_eq0 [in rm0]
eq_expr_rm_perm [in morphisms]
eq_expr_rm0 [in morphisms]
eq_expr_erase [in morphisms]
eq_typed_vers [in removetype]
eq_ν_smpl_typed_vers [in removetype]
eq_perm_typed_vers [in removetype]
eq_perm_elim_typed_vers [in removetype]
eq_nom_typed_np_vers [in removetype]
eq_nom_typed_p_vers [in removetype]
eq_nom_typed_vers [in removetype]
eq_νW2 [in removetype]
eq_smpl_ω_W [in removetype]
eq_perm_ω_W [in removetype]
eq_support [in removetype]
eq_ν_smpl_support [in removetype]
eq_perm_support [in removetype]
eq_perm_elim_support [in removetype]
eq_nom_untyped_np_support [in removetype]
eq_nom_untyped_p_support [in removetype]
eq_nom_untyped_support [in removetype]
eq_erase [in removetype]
eq_ω_smpl_erase [in removetype]
eq_ν_smpl_erase [in removetype]
eq_perm_ω_erase [in removetype]
eq_perm_erase [in removetype]
eq_perm_elim_erase [in removetype]
eq_nom_np_erase [in removetype]
eq_nom_untyped_np_no_perm [in removetype]
eq_nom_p_erase [in removetype]
eq_nom_erase [in removetype]
eq_nom_untyped_np_rm_perm_pos [in perm]
eq_apply_perm_pos [in perm]
eq_apply_perm_ut_pos [in perm]
eq_rm_perm_pos [in perm]
eq_rm_perm_ut_pos [in perm]
eq_apply_perm [in perm]
eq_nom_typed_np_apply_perm [in perm]
eq_nom_untyped_np_apply_perm [in perm]
eq_nom_typed_p_apply_perm [in perm]
eq_nom_untyped_p_apply_perm [in perm]
eq_perm_elim_apply_perm [in perm]
eq_perm_ω_apply_perm [in perm]
eq_perm_apply_perm [in perm]
eq_rm_perm_bis [in perm]
eq_rm_perm [in perm]
eq_expr_get_bot [in predicates]
eq_expr_eq0' [in predicates]
eq_expr_eq0 [in predicates]
eq_expr_stage [in predicates]
eq_expr_support [in predicates]
eq_expr_size [in predicates]
eq_expr_W [in predicates]
eq_perm_elim_convert [in normalise]
eq0_proof_typed [in rm0]
eq0_untyped_refl [in rm0]
eq0_proof_untyped [in rm0]
eq0_apply_perm [in morphisms]
eq0_rm0_u [in morphisms]
eq0_erase [in removetype]
eq0'_get_bot_positive [in expr]
eq0'_spec [in expr]
eq0'_rm0_apply_perm [in morphisms]
eq0'_get_bot_positivet [in predicates]
eq0'_t_spec [in predicates]
eq0'_get_bot_positiveu [in predicates]
eq0'_u_spec [in predicates]
erase_apply_perm [in morphisms]
erase_typed_vers_np [in removetype]
erase_typed_vers [in removetype]
F
FFalse_spec [in tools]filter_app [in atoms_ops]
filter_id [in atoms_ops]
filter_length [in atoms_ops]
freshb_spec [in predicates]
fresh_rm_perm [in morphisms]
fresh_apply_perm [in morphisms]
fresh_rm0 [in morphisms]
fresh_type [in morphisms]
fresh_support [in predicates]
G
get_bot_spec [in expr]get_bot_t_spec [in predicates]
get_bot_u_spec [in predicates]
goodNKAmpt [in theories]
goodNKAmpu [in theories]
goodNKAnmpt [in theories]
goodNKAnmpu [in theories]
goodNKAnspt [in theories]
goodNKAnspu [in theories]
goodNKAspt [in theories]
goodNKAspu [in theories]
H
has_type_multi_to_single [in sg_to_mlt]has_type_single_to_multi [in sg_to_mlt]
has_type_rm_perm_apply_perm [in morphisms]
has_type_apply_perm [in morphisms]
ht_convert [in predicates]
I
id_a_diff_un_NKA_tp [in theories]id_a_diff_un_NKA_θtp [in theories]
id_morph [in normalise]
if_Atom_eq_dec_neq [in atoms]
if_Atom_eq_dec_eq [in atoms]
image_mlt [in sg_to_mlt]
img_ut_fresh_multi_to_single [in sg_to_mlt]
img_sg_multi_to_single [in sg_to_mlt]
inb_spec [in atoms]
included_th_decidable [in order]
incl_p_fun_l [in order]
incl_p_fun_r [in order]
incl_p_fun [in order]
incl_ty_ut_np [in removetype]
incl_ty_ut [in removetype]
incl_ut_ty [in removetype]
incl_lst_b_spec [in equiv_lst]
inter_length [in atoms_ops]
inter_cong [in equiv_lst]
inverse_app [in atoms]
inverse_comp_r [in atoms]
inverse_comp_l [in atoms]
inverse_inv [in atoms]
In_mact [in atoms_ops]
In_rm [in atoms_ops]
In_inter [in atoms_ops]
In_undup [in atoms_ops]
In_purge [in atoms_ops]
In_app_iff [in atoms_ops]
In_cons [in atoms_ops]
in_X_X [in restr_atoms]
in_X_spec [in restr_atoms]
in_double_neg [in atoms]
is_restr_stable [in restr_atoms]
is_perm_bool_is_perm [in letter]
is_perm_bool_spec [in letter]
is_perm_no_dup_length [in letter]
K
ka_eq_str_positive [in proofs]ka_eq_u_str_positive [in proofs]
ka_eq_t_str_positive [in proofs]
ka_eq_no_perm [in proofs]
ka_eq_u_no_perm [in proofs]
ka_eq_t_no_perm [in proofs]
ka_eq_multi [in proofs]
ka_eq_u_multi [in proofs]
ka_eq_t_multi [in proofs]
ka_eq_single [in proofs]
ka_eq_u_single [in proofs]
ka_eq_t_single [in proofs]
ka_eq_untyped [in proofs]
ka_eq_u_untyped [in proofs]
ka_eq_type [in proofs]
ka_eq_t_type [in proofs]
ka_eq_t_image [in sg_to_mlt]
ka_eq_u_image [in sg_to_mlt]
ka_eq_u_eq0 [in rm0]
ka_eq_t_eq0 [in rm0]
ka_eq_eq0 [in rm0]
ka_eq_tu_typed_vers [in removetype]
ka_eq_typed_vers [in removetype]
ka_eq_u_support [in removetype]
ka_eq_support [in removetype]
ka_eq_tu_erase [in removetype]
ka_eq_erase [in removetype]
L
length_support_size [in expr]le_diff_un_NKA_p [in theories]
le_diff_un_NKA_θp [in theories]
M
mact_undup [in atoms_ops]mact_app_distr [in atoms_ops]
mact_id1 [in atoms_ops]
mact_nil [in atoms_ops]
mact_id2 [in atoms_ops]
mact_purge [in atoms_ops]
mact_rm [in atoms_ops]
mact_inv_l [in atoms_ops]
mact_inv_r [in atoms_ops]
mact_comp_app [in atoms_ops]
mact_length [in atoms_ops]
mact_elements_equiv_perm [in equiv_lst]
mact_cong [in equiv_lst]
mact_eq_act_eq [in normalise]
map_φ_inj [in restr_atoms]
map_φ_rm [in restr_atoms]
map_φ_mact [in restr_atoms]
map_ψ_act_φ [in restr_atoms]
map_ψ_map_φ_act_φ [in restr_atoms]
map_φ_act [in restr_atoms]
map_pair_inv [in restr_atoms]
map_act_inv_eq [in equiv_lst]
map1 [in equiv_lst]
map2 [in equiv_lst]
mlt_single_to_multi [in sg_to_mlt]
multib_spec [in predicates]
multi_rm_perm [in morphisms]
multi_apply_perm [in morphisms]
multi_rm0 [in morphisms]
multi_typed_vers [in morphisms]
multi_erase [in morphisms]
multi_W [in predicates]
N
Nice_NKAspu [in normalise]nice_convert_eq [in normalise]
nice_eq [in normalise]
nice_NKA_nice [in normalise]
nice_convert [in normalise]
NKAmpt_is_model_NKAmt [in order]
NKAmpt_is_model_NKAnmpt [in order]
NKAmpu_NKAmpt_eq [in order]
NKAmpu_is_model_NKAmpt [in order]
NKAmpu_is_model_NKAmu [in order]
NKAmpu_is_model_NKAnmpu [in order]
NKAmt_NKAmpt_eq [in order]
NKAmu_NKAmpu_eq [in order]
NKAnmpt_NKAmpt_eq [in order]
NKAnmpt_is_model_NKAmpt [in order]
NKAnmpt_is_model_NKAnmt [in order]
NKAnmpu_NKAmpu_eq [in order]
NKAnmpu_is_model_NKAmpu [in order]
NKAnmpu_NKAnmpt_eq [in order]
NKAnmpu_is_model_NKAnmpt [in order]
NKAnmpu_is_model_NKAnmu [in order]
NKAnmt_NKAnmpt_eq [in order]
NKAnmu_NKAnmpu_eq [in order]
NKAnspt_NKAspt_eq [in order]
NKAnspt_is_model_NKAspt [in order]
NKAnspt_is_model_NKAnst [in order]
NKAnspu_NKAspu_eq [in order]
NKAnspu_is_model_NKAspu [in order]
NKAnspu_NKAnspt_eq [in order]
NKAnspu_is_model_NKAnspt [in order]
NKAnspu_is_model_NKAnsu [in order]
NKAnst_NKAnspt_eq [in order]
NKAnsu_NKAnspu_eq [in order]
NKAspt_is_model_NKAst [in order]
NKAspt_is_model_NKAnspt [in order]
NKAspu_NKAspt_eq [in order]
NKAspu_is_model_NKAspt [in order]
NKAspu_is_model_NKAsu [in order]
NKAspu_is_model_NKAnspu [in order]
NKAspu_Nice [in normalise]
NKAst_NKAspt_eq [in order]
NKAsu_NKAspu_eq [in order]
NKA_θp_untyped [in sg_to_mlt]
NKA_θtp_single [in sg_to_mlt]
NKA_θp_single [in sg_to_mlt]
NKA_θtp_image [in sg_to_mlt]
NKA_θp_image [in sg_to_mlt]
NKA_θtp_NKA_tp_rm_perm_apply_perm [in theories]
NKA_θp_NKA_p_rm_perm_apply_perm [in theories]
NKA_tp_NKA_θtp [in theories]
NKA_p'_NKA_p_eq [in theories]
NKA_tp'_NKA_tp_eq [in theories]
NKA_tp_Np [in theories]
NKA_p_Np [in theories]
NKA_pos [in theories]
NKA_typed_vers' [in theories]
NKA_erase' [in theories]
NKA_p'_support [in theories]
NKA_p_support [in theories]
NKA_θp_support [in theories]
NKA_p_rm0 [in theories]
NKA_θp_rm0 [in theories]
NKA_tp_rm0 [in theories]
NKA_θtp_rm0 [in theories]
NKA_eq0 [in theories]
NKA_p_eq0 [in theories]
NKA_θ_eq0 [in theories]
NKA_θp_eq0 [in theories]
NKA_t_eq0 [in theories]
NKA_tp_eq0 [in theories]
NKA_θt_eq0 [in theories]
NKA_θtp_eq0 [in theories]
NKA_p'_untyped [in theories]
NKA_tp'_has_type [in theories]
NKA_untyped [in theories]
NKA_p_untyped [in theories]
NKA_θ_untyped [in theories]
NKA_θp_untyped [in theories]
NKA_t_has_type [in theories]
NKA_tp_has_type [in theories]
NKA_θt_has_type [in theories]
NKA_θtp_has_type [in theories]
NKA_θtp_str_positive [in theories]
NKA_θp_str_positive [in theories]
NKA_tp_str_positive [in theories]
NKA_p_str_positive [in theories]
NKA_θtp_multi [in theories]
NKA_θp_multi [in theories]
NKA_tp_multi [in theories]
NKA_p_multi [in theories]
NKA_θtp_single [in theories]
NKA_θp_single [in theories]
NKA_tp_single [in theories]
NKA_p_single [in theories]
NKA_NKA_θ_m [in order]
NKA_NKA_θ_s [in order]
NKA_t_NKA_θt_fun [in order]
NKA_NKA_θ_fun [in order]
NKA_θ_NKA_m [in order]
NKA_θ_NKA_s [in order]
NKA_θt_NKA_t_fun [in order]
NKA_θ_NKA_fun [in order]
NKA_θtp_NKA_θp_m [in order]
NKA_tp_NKA_p_m [in order]
NKA_θtp_NKA_θp_s [in order]
NKA_tp_NKA_p_s [in order]
NKA_θp_NKA_θtp_m [in order]
NKA_p_NKA_tp_m [in order]
NKA_θp_NKA_θtp_s [in order]
NKA_p_NKA_tp_s [in order]
NKA_tp_NKA_p [in order]
NKA_p_NKA_tp_precise [in order]
NKA_p_NKA_tp [in order]
NKA_θtp_NKA_θp_fun [in order]
NKA_θp_NKA_θtp_precise [in order]
NKA_θp_NKA_θtp_fun [in order]
NKA_θtp_incl_NKA_θt_m [in order]
NKA_θtp_incl_NKA_θt_s [in order]
NKA_θtp_incl_NKA_θt [in order]
NKA_θt_incl_NKA_θtp_m [in order]
NKA_θt_incl_NKA_θtp_s [in order]
NKA_θt_incl_NKA_θtp [in order]
NKA_θt_NKA_θtp [in order]
NKA_θp_incl_NKA_θ_m [in order]
NKA_θp_incl_NKA_θ_s [in order]
NKA_θp_incl_NKA_θ [in order]
NKA_θ_incl_NKA_θp_m [in order]
NKA_θ_incl_NKA_θp_s [in order]
NKA_θ_incl_NKA_θp [in order]
NKA_θ_NKA_θp [in order]
NKA_tp_incl_NKA_tns [in order]
NKA_tp_incl_NKA_tnm [in order]
NKA_tp_incl_NKA_t [in order]
NKA_t_incl_NKA_tp_ns [in order]
NKA_t_incl_NKA_tp_nm [in order]
NKA_t_incl_NKA_tp [in order]
NKA_t_NKA_tp [in order]
NKA_p_incl_NKA_ns [in order]
NKA_p_incl_NKA_nm [in order]
NKA_p_incl_NKA [in order]
NKA_incl_NKA_p_ns [in order]
NKA_incl_NKA_p_nm [in order]
NKA_incl_NKA_p [in order]
NKA_NKA_p [in order]
NKA_nice_stronger_NKA_θp [in normalise]
NKA'_NKA_θp [in theories]
NKA'_pos [in theories]
NKA'_support [in theories]
NKA'_untyped [in theories]
NKAθ_typed_vers [in theories]
NKAθ_erase [in theories]
NoDup_undup_eq [in atoms_ops]
NoDup_mact [in atoms_ops]
NoDup_app_inv [in atoms_ops]
NoDup_app [in atoms_ops]
NoDup_rm [in atoms_ops]
NoDup_inter [in atoms_ops]
NoDup_purge [in atoms_ops]
NoDup_filter [in atoms_ops]
NoDup_cons_iff [in atoms_ops]
NoDup_undup [in atoms_ops]
NoDup_map_φ [in restr_atoms]
nodup_bool_spec [in letter]
no_perm_rm_perm [in morphisms]
no_perm_rm_perm_id [in morphisms]
no_perm_apply_perm [in morphisms]
no_perm_rm0 [in morphisms]
no_perm_typed_vers [in morphisms]
no_perm_erase [in morphisms]
no_perm_W [in predicates]
no_permb_spec [in predicates]
O
one_star_is_one_t [in proofs]one_star_is_one_u [in proofs]
or_and_distr [in tools]
or_rel_stronger_r [in tools]
or_rel_stronger_l [in tools]
P
perm_fun_lst_mact [in restr_atoms]perm_p_pinv_eq_nil [in atoms]
perm_pinv_p_eq_nil [in atoms]
perm_a_a_eq_nil [in atoms]
perm_bij [in atoms]
perm_inj [in atoms]
poa_poa_single_to_multi [in sg_to_mlt]
positiveb_spec [in predicates]
positive_rm_perm [in morphisms]
positive_apply_perm [in morphisms]
positive_rm0_id [in morphisms]
positive_rm0 [in morphisms]
positive_or_nul_rm0 [in morphisms]
positive_typed_vers [in morphisms]
positive_erase [in morphisms]
pos_rev_rm0 [in order]
pos_disj [in predicates]
po_po_single_to_multi [in sg_to_mlt]
po_to_str_rm0 [in order]
proper_and_split [in tools]
proper_or_split [in tools]
proper_stronger_r [in tools]
proper_stronger_l [in tools]
proper_ex_ax_eq [in restr_atoms]
proper_eq [in proofs]
Proper_ty_img_eq [in sg_to_mlt]
Proper_ty_img_ax [in sg_to_mlt]
Proper_ut_img_eq [in sg_to_mlt]
Proper_ut_img_ax [in sg_to_mlt]
Proper_ty_sg_eq [in sg_to_mlt]
Proper_ty_sg_ax [in sg_to_mlt]
Proper_ut_sg_eq [in sg_to_mlt]
Proper_ut_sg_ax [in sg_to_mlt]
purge_rm [in atoms_ops]
purge_app [in atoms_ops]
purge_l_l [in atoms_ops]
purge_cons [in atoms_ops]
purge_nil [in atoms_ops]
purge_length [in atoms_ops]
purge_l_m_nil [in equiv_lst]
purge_cong [in equiv_lst]
R
rel_and_pred [in tools]remain_Sp [in proofs]
remain_Np [in proofs]
remain_Mlt [in proofs]
remain_Sg [in proofs]
remain_Ut [in proofs]
remain_Ty [in proofs]
restr_perm_is_restr [in restr_atoms]
restr_ax_eq_ax_eq [in restr_atoms]
restr_perm_map_φ [in restr_atoms]
restr_perm_mact [in restr_atoms]
restr_perm_act [in restr_atoms]
rm_cons [in atoms_ops]
rm_id [in atoms_ops]
rm_purge [in atoms_ops]
rm_app [in atoms_ops]
rm_comm [in atoms_ops]
rm_length [in atoms_ops]
rm_perm_apply_perm_swap [in morphisms]
rm_perm_size [in morphisms]
rm_cons_eq' [in equiv_lst]
rm_cons_eq [in equiv_lst]
rm_cong [in equiv_lst]
rm0_eq_nom_typed_np [in rm0]
rm0_eq_nom_typed_p [in rm0]
rm0_eq_nom_typed [in rm0]
rm0_eq_nom_untyped [in rm0]
rm0_eq_nom_untyped_np [in rm0]
rm0_eq_nom_untyped_p [in rm0]
rm0_u_ka_eq [in rm0]
rm0_t_ka_eq [in rm0]
rm0_eq_perm_ω [in rm0]
rm0_eq_perm_elim [in rm0]
rm0_eq_ω_smpl_typed [in rm0]
rm0_eq_ν_smpl_untyped [in rm0]
rm0_eq_ν_smpl_typed [in rm0]
rm0_zero_eq_t [in rm0]
rm0_zero_eq_u [in rm0]
rm0_eq_typed [in rm0]
rm0_eq_untyped [in rm0]
rm0_apply_perm [in morphisms]
rm0_eq0_get_bot [in morphisms]
rm0_inv_apply_perm [in morphisms]
rm0_involutive [in morphisms]
S
sg_image_single_to_multi [in sg_to_mlt]singleb_spec [in predicates]
single_rm_perm [in morphisms]
single_apply_perm [in morphisms]
single_rm0 [in morphisms]
single_typed_vers [in morphisms]
single_erase [in morphisms]
single_multi_ty [in order]
single_multi_ut [in order]
single_W [in predicates]
single_support_le_size [in predicates]
size_W [in expr]
size_non_zero [in expr]
size_single_to_multi [in sg_to_mlt]
size_rm0 [in morphisms]
size_typed_vers [in morphisms]
size_erase [in morphisms]
stage_has_type [in predicates]
stronger_Ty_ka_eq_t [in proofs]
stronger_Ty_zero_ka_t [in proofs]
stronger_eq_or_rel_r [in proofs]
stronger_eq_or_rel_l [in proofs]
stronger_ax_eq [in proofs]
stronger_Ty_eq_nom_typed_np [in rm0]
str_positive_rm_perm [in morphisms]
str_positive_apply_perm [in morphisms]
str_positive_rm0_id [in morphisms]
str_positive_rm0 [in morphisms]
str_positive_typed_vers [in morphisms]
str_positive_erase [in morphisms]
str_pos_rev_rm0 [in order]
str_positive_eq0 [in removetype]
str_positive_W [in predicates]
str_positive_positive [in predicates]
str_positiveb_spec [in predicates]
str_positive_NKA_nice [in normalise]
support_or_diff_NKA_θp [in theories]
support_or_diff_NKA_p [in theories]
support_apply_perm [in morphisms]
support_min_type [in morphisms]
switch_NKA_p_NKA' [in theories]
switch_NKA'_NKA_p [in theories]
T
technical [in order]transfer_fun_included_th [in order]
transfer_fun_preorder [in order]
TTrue_spec [in tools]
TTrue_unit_r [in order]
TTrue_unit_l [in order]
typedb_spec [in predicates]
typed_equiv_rm0 [in rm0]
typed_impl_rm0 [in rm0]
typed_vers_apply_perm [in morphisms]
typed_rm0 [in morphisms]
typed_version_support_type [in morphisms]
typed_version_erase [in morphisms]
typed_vers_size [in morphisms]
typed_stage_has_type [in predicates]
type_W' [in predicates]
type_eq_cons [in predicates]
type_unicity [in predicates]
ty_multi_to_single_single_to_multi [in sg_to_mlt]
ty_multi_to_single [in sg_to_mlt]
ty_ty_single_to_multi [in sg_to_mlt]
ty_Single_to_Multi [in order]
Ty_eq_perm_ω_W [in removetype]
ty'_or_diff_NKA_θtp [in theories]
ty'_or_diff_NKA_tp [in theories]
U
undup_rm [in atoms_ops]undup_app [in atoms_ops]
undup_purge [in atoms_ops]
undup_length [in atoms_ops]
undup_equiv_lst [in equiv_lst]
untypedb_spec [in predicates]
untyped_equiv_rm0 [in rm0]
untyped_impl_rm0 [in rm0]
untyped_rm_perm [in morphisms]
untyped_apply_perm [in morphisms]
untyped_rm0 [in morphisms]
untyped_erase [in morphisms]
untyped_NKA_nice [in normalise]
ut_multi_to_single_single_to_multi [in sg_to_mlt]
ut_multi_to_single [in sg_to_mlt]
ut_single_fresh_single_to_multi [in sg_to_mlt]
ut_ut_single_to_multi [in sg_to_mlt]
ut_Single_to_Multi [in order]
W
W_app [in expr]W_apply_perm [in morphisms]
W_erase [in morphisms]
W_ω_extract [in removetype]
W_equiv_lst [in removetype]
W_ω_exchange [in removetype]
W_type [in predicates]
Z
zero_nom_t_apply_φ [in restr_atoms]zero_nom_u_apply_φ [in restr_atoms]
zero_perm_t_apply_φ [in restr_atoms]
zero_perm_u_apply_φ [in restr_atoms]
zero_ka_t_apply_φ [in restr_atoms]
zero_ka_u_apply_φ [in restr_atoms]
zero_star_is_one_t [in proofs]
zero_star_is_one_u [in proofs]
zero_nom_u_str_positive [in proofs]
zero_nom_t_str_positive [in proofs]
zero_nom_u_no_perm [in proofs]
zero_nom_t_no_perm [in proofs]
zero_perm_u_multi [in proofs]
zero_perm_t_multi [in proofs]
zero_nom_u_multi [in proofs]
zero_nom_t_multi [in proofs]
zero_perm_u_single [in proofs]
zero_perm_t_single [in proofs]
zero_nom_u_single [in proofs]
zero_nom_t_single [in proofs]
zero_nom_u_untyped [in proofs]
zero_perm_u_untyped [in proofs]
zero_ka_u_untyped [in proofs]
zero_nom_t_type [in proofs]
zero_perm_t_type [in proofs]
zero_ka_t_type [in proofs]
zero_nom_u_derivable [in proofs]
zero_eq_t_eq0 [in rm0]
zero_eq_u_eq0 [in rm0]
zero_nom_u_eq0 [in rm0]
zero_nom_t_eq0 [in rm0]
zero_perm_u_eq0 [in rm0]
zero_perm_t_eq0 [in rm0]
zero_ka_u_eq0 [in rm0]
zero_ka_t_eq0 [in rm0]
zero_diff_un_NKA_tp [in theories]
zero_diff_un_NKA_p [in theories]
zero_diff_un_NKA_θtp [in theories]
zero_diff_un_NKA_θp [in theories]
zero_perm_t_apply_perm [in perm]
zero_perm_u_apply_perm [in perm]
other
τ_spec [in letter]φ_lst_incl_mact [in restr_atoms]
φ_lst_act [in restr_atoms]
φ_inv [in restr_atoms]
φ_in_X [in restr_atoms]
φ_X [in restr_atoms]
φ_inj [in restr_atoms]
ψ_inj_implies_φ_surj [in restr_atoms]
ψ_surj [in restr_atoms]
Axiom Index
A
Atom [in atoms]B
beq_name_spec [in letter]beq_name [in letter]
beq_atom_refl [in atoms]
beq_atom [in atoms]
G
get_new [in letter]K
K [in expr]N
Name [in letter]new_atom [in letter]
other
α [in sg_to_mlt]λ [in sg_to_mlt]
τ_λ [in sg_to_mlt]
τ_nm_spec [in letter]
τ_nm [in letter]
Constructor Index
B
bot [in expr]E
eqt_ν4 [in proofs]eqt_ν3 [in proofs]
eqt_νω2 [in proofs]
eqt_νω1 [in proofs]
eqt_θν [in proofs]
eqt_θν' [in proofs]
eqt_ν0 [in proofs]
equ_ν4 [in proofs]
equ_ν3 [in proofs]
equ_νω1 [in proofs]
equ_θν [in proofs]
equ_θν' [in proofs]
equ_ν0 [in proofs]
eq_ωω [in proofs]
eq_ω_s [in proofs]
eq_ω_t [in proofs]
eq_ω_p [in proofs]
eq_ω_id [in proofs]
eq_νab [in proofs]
eq_νp [in proofs]
eq_nil_e [in proofs]
eq_θ_id [in proofs]
eq_θ_var [in proofs]
eq_θ_at [in proofs]
eq_θ_1 [in proofs]
eq_θ_ω [in proofs]
eq_θ_θ [in proofs]
eq_θ_ν [in proofs]
eq_θ_s [in proofs]
eq_θ_t [in proofs]
eq_θ_p [in proofs]
eq_ω_bot [in proofs]
eq_θ_bot [in proofs]
eq_θ_0 [in proofs]
eq_ax [in proofs]
eq_ka_impl [in proofs]
eq_ka [in proofs]
eq_ω [in proofs]
eq_θ [in proofs]
eq_ν [in proofs]
eq_star [in proofs]
eq_times [in proofs]
eq_plus [in proofs]
eq_vat [in proofs]
eq_var [in proofs]
eq_id [in proofs]
eq_bot [in proofs]
eq_un [in proofs]
eq_zero [in proofs]
eq_trans [in proofs]
eq_sym [in proofs]
eq_WW [in removetype]
eq_W_s [in removetype]
eq_W_t [in removetype]
eq_W_p [in removetype]
eq_W_id [in removetype]
eq_θ_W [in removetype]
eq_θ_fr_id [in normalise]
eq_θ_fr_nil [in normalise]
eq_θ_fresh [in normalise]
I
id [in expr]K
kat_s2 [in proofs]kat_s1 [in proofs]
kat_1t [in proofs]
kat_t1 [in proofs]
kau_s2 [in proofs]
kau_s1 [in proofs]
kau_1t [in proofs]
kau_t1 [in proofs]
ka_s4 [in proofs]
ka_s3 [in proofs]
ka_tp [in proofs]
ka_pt [in proofs]
ka_pi [in proofs]
ka_pc [in proofs]
ka_pp [in proofs]
ka_tt [in proofs]
P
plus [in expr]R
r3_true [in tools]r3_Some [in tools]
r3_false [in tools]
S
star [in expr]T
times [in expr]U
un [in expr]V
var [in expr]vat [in expr]
Z
zero [in expr]zero_t_0t [in proofs]
zero_t_t0 [in proofs]
zero_t_p0 [in proofs]
zero_u_0t [in proofs]
zero_u_t0 [in proofs]
zero_u_p0 [in proofs]
other
θ [in expr]ν [in expr]
ω [in expr]
Inductive Index
E
eq [in proofs]eq_nom_typed [in proofs]
eq_nom_typed_np [in proofs]
eq_nom_typed_p [in proofs]
eq_nom_untyped [in proofs]
eq_nom_untyped_np [in proofs]
eq_nom_untyped_p [in proofs]
eq_ω_smpl [in proofs]
eq_ν_smpl [in proofs]
eq_perm_elim [in proofs]
eq_perm_ω [in proofs]
eq_perm [in proofs]
eq_W_smpl [in removetype]
eq_perm_W [in removetype]
eq_perm_fresh [in normalise]
expr [in expr]
K
ka_eq_t [in proofs]ka_eq_u [in proofs]
ka_impl [in proofs]
ka_eq [in proofs]
R
reflect3 [in tools]Z
zero_nom_t [in proofs]zero_nom_u [in proofs]
zero_perm_t [in proofs]
zero_perm_u [in proofs]
zero_ka_t [in proofs]
zero_ka_u [in proofs]
Instance Index
A
and_rel_stronger_stronger_stronger [in tools]and_rel_eq_rel_eq_rel_eq_rel [in tools]
and_pred_eq_pred_eq_pred_eq_pred [in tools]
antisym_incl_lst [in equiv_lst]
anti_incl_lst [in equiv_lst]
apply_perm_equiv_perm [in morphisms]
app_incl [in equiv_lst]
app_equiv [in equiv_lst]
B
bot_equiv_lst_eq [in proofs]C
cons_incl [in equiv_lst]cons_equiv [in equiv_lst]
E
equiv_perm_mact [in atoms_ops]equiv_th_Equivalence [in order]
equiv_lst_Equiv [in equiv_lst]
equiv_lst_trans [in equiv_lst]
equiv_lst_sym [in equiv_lst]
equiv_lst_refl [in equiv_lst]
equiv_perm_spec [in atoms]
equiv_perm_app [in atoms]
equiv_perm_inverse [in atoms]
equiv_perm_Equivalence [in atoms]
eq_pred_Equivalence [in tools]
eq_rel_Equivalence [in tools]
eq_Equiv [in proofs]
eq_letter_Equivalence [in letter]
eq_expr_Equivalence [in predicates]
H
ht_id_eq [in predicates]ht_bot_eq [in predicates]
ht_equiv_iff [in predicates]
ht_equiv [in predicates]
I
id_equiv_lst_eq [in proofs]included_th_PreOrder [in order]
inf_antisym [in proofs]
inter_incl [in equiv_lst]
inter_equiv [in equiv_lst]
In_incl [in equiv_lst]
In_equiv [in equiv_lst]
M
mact_incl [in equiv_lst]mact_equiv [in equiv_lst]
O
or_rel_stronger_stronger_stronger [in tools]or_rel_eq_rel_eq_rel_eq_rel [in tools]
P
plus_eq [in proofs]pre_incl_lst [in equiv_lst]
proper_S_le [in tools]
proper_plus_le [in tools]
purge_incl [in equiv_lst]
purge_eq [in equiv_lst]
purge_equiv [in equiv_lst]
R
rel_eq_pred_eq_rel [in tools]rm_incl [in equiv_lst]
rm_equiv [in equiv_lst]
S
star_eq [in proofs]stronger_Preorder [in tools]
stronger_ax_proof [in proofs]
T
times_eq [in proofs]transfer_fun_proper_iff_2 [in order]
transfer_fun_proper_iff_1 [in order]
transfer_fun_proper_iff [in order]
transfer_fun_proper_eq_impl_rev [in order]
transfer_fun_proper_eq_impl [in order]
transfer_fun_proper_str_impl [in order]
U
undup_equiv [in equiv_lst]W
W_eq [in removetype]other
θ_eq [in proofs]ν_eq [in proofs]
ω_eq [in proofs]
Section Index
P
poly [in expr]poly [in morphisms]
S
s [in tools]Abbreviation Index
F
FFalse [in tools]FFalse [in tools]
I
inf [in proofs]T
TTrue [in tools]TTrue [in tools]
Z
zero_eq_u [in proofs]zero_eq_t [in proofs]
Definition Index
A
act [in atoms]all_atoms [in restr_atoms]
and_pred [in tools]
and_rel [in tools]
apply_fun [in restr_atoms]
apply_perm [in morphisms]
apply_perm_var [in morphisms]
B
bequiv_perm [in equiv_lst]beq_letter [in letter]
beq_expr [in predicates]
beq_perm [in atoms]
beq_list [in atoms]
Bs [in expr]
C
can_var [in normalise]convert [in normalise]
conv_lst_perm [in normalise]
E
elements [in equiv_lst]equiv_th [in order]
equiv_lst_b [in equiv_lst]
equiv_lst [in equiv_lst]
equiv_perm [in atoms]
eq_pred [in tools]
eq_rel [in tools]
eq_letter [in letter]
eq_expr [in predicates]
eq0 [in expr]
eq0' [in expr]
erase [in morphisms]
ex_ax_eq [in restr_atoms]
F
fresh [in predicates]freshb [in predicates]
G
get_bot [in expr]get_atom [in sg_to_mlt]
good [in theories]
H
has_type [in predicates]I
image [in sg_to_mlt]Img [in sg_to_mlt]
inb [in atoms]
included_th [in order]
incl_lst_b [in equiv_lst]
incl_lst [in equiv_lst]
inter [in atoms_ops]
inverse [in atoms]
in_X [in restr_atoms]
is_restr [in restr_atoms]
is_perm_bool [in letter]
is_perm [in letter]
is_model [in order]
L
Letter [in letter]M
mact [in atoms_ops]map_pair [in restr_atoms]
mlt [in predicates]
multi [in predicates]
multib [in predicates]
multi_to_single [in sg_to_mlt]
N
Nice [in normalise]nice [in normalise]
NKA [in theories]
NKAmpt [in theories]
NKAmpu [in theories]
NKAmt [in theories]
NKAmu [in theories]
NKAnmpt [in theories]
NKAnmpu [in theories]
NKAnmt [in theories]
NKAnmu [in theories]
NKAnspt [in theories]
NKAnspu [in theories]
NKAnst [in theories]
NKAnsu [in theories]
NKAspt [in theories]
NKAspu [in theories]
NKAst [in theories]
NKAsu [in theories]
NKA_p' [in theories]
NKA_tp' [in theories]
NKA_p [in theories]
NKA_t [in theories]
NKA_tp [in theories]
NKA_θ [in theories]
NKA_θp [in theories]
NKA_θt [in theories]
NKA_θtp [in theories]
NKA_nice [in normalise]
NKA' [in theories]
nodup_bool [in letter]
no_permb [in predicates]
no_perm [in predicates]
np [in predicates]
O
or_rel [in tools]P
perm [in atoms]perm_fun_lst [in restr_atoms]
po [in predicates]
positive [in predicates]
positiveb [in predicates]
predicate [in tools]
purge [in atoms_ops]
R
rel [in tools]restr_ax [in restr_atoms]
restr_expr [in restr_atoms]
restr_list [in restr_atoms]
restr_perm [in restr_atoms]
rm [in atoms_ops]
rm_perm [in morphisms]
rm0 [in morphisms]
S
sg [in predicates]single [in predicates]
singleb [in predicates]
single_to_multi [in sg_to_mlt]
size [in expr]
sp [in predicates]
stage [in expr]
stronger [in tools]
str_positiveb [in predicates]
str_positive [in predicates]
support [in expr]
T
transfer_perm [in letter]transfer_fun [in order]
ty [in predicates]
TyEq [in theories]
typed [in predicates]
typedb [in predicates]
typed_vers [in morphisms]
ty' [in predicates]
U
undup [in atoms_ops]untyped [in predicates]
untypedb [in predicates]
ut [in predicates]
W
W [in expr]X
X [in restr_atoms]other
τ [in letter]| 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 | (1222 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 | (49 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 | (8 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 | (17 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 | (803 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 | (14 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 | (97 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 | (27 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 | (66 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 | (3 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 | (7 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 | (131 entries) |
This page has been generated by coqdoc