FGJ-omega
| 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 | _ | (1109 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 | _ | (533 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 | _ | (7 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 | _ | (276 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 | _ | (74 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 | _ | (82 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 | _ | (60 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 | _ | (31 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 | _ | (19 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 | _ | (27 entries) |
Global Index
A
Accessibility_is_preserved_by_inclusion [lemma, in Util]app_inject [lemma, in Util]
app_length_right [lemma, in Util]
Auxiliary [library]
Auxiliary_proofs [library]
B
Binders [library]Binders_proofs [library]
BoundCompliantSubstitutions_proofs [library]
by_omega1 [lemma, in Util]
C
Confluence [library]cons_destruct [lemma, in Util]
correct_witness [lemma, in Util]
D
Declaration_of_variable_1 [lemma, in Util]Declaration_of_variable_2 [lemma, in Util]
E
empty_is_empty_1 [lemma, in Util]empty_is_empty_2 [lemma, in Util]
empty_union_left [lemma, in Util]
empty_union_right [lemma, in Util]
Exists_Section [section, in Util]
Exists_Section.A [variable, in Util]
Exists_Section.B [variable, in Util]
Exists_Section.existence [variable, in Util]
Exists_Section.P [variable, in Util]
F
Forall2 [inductive, in Util]Forall2_and_ListAt [lemma, in Util]
Forall2_and_ListFrom [lemma, in Util]
Forall2_conj [lemma, in Util]
Forall2_cons [constructor, in Util]
Forall2_implies [lemma, in Util]
Forall2_implies_same_length [lemma, in Util]
Forall2_nil [constructor, in Util]
Forall2_of_map [lemma, in Util]
Forall2_of_map_cor1 [lemma, in Util]
Forall2_of_map_cor2 [lemma, in Util]
Forall2_refl [lemma, in Util]
Forall2_section [section, in Util]
Forall2_section.A [variable, in Util]
Forall2_section.B [variable, in Util]
Forall2_snoc [lemma, in Util]
Forall2_trans [lemma, in Util]
forall_implies_forall [lemma, in WellFoundation]
fun_extension [definition, in WellFoundation]
G
get_witness [definition, in Util]L
LambdaCalculus [module, in SimplyTypedLambdaCalculus]LambdaCalculusNormalization [module, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Constants_are_reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.First_projections_are_reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Lambda_redices_are_reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.lift_in_term_by_zero [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.lift_in_var_by_zero [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Permuting_lifting_and_polySubstitution [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PolySubstitution_preserves_typing [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PolySubstitution_preserves_typing_cor1 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_by_snoc [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_app [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_const [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_fst [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_fun [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_pair [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_snd [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_term [definition, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_var1 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_var_variant [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_of_var_invariant [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed [axiom, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_implies_SN [axiom, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_implies_WellTyped [axiom, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_left_weakening [axiom, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_not_a_function [axiom, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_not_a_pair [axiom, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_subject_reduction [axiom, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed [definition, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_implies_WellTyped [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_left_weakening [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_not_a_function [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_not_a_pair [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_subject_reduction [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed [definition, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_implies_WellTyped [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_left_weakening [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_not_a_function [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_not_a_pair [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_subject_reduction [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed [definition, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_implies_WellTyped [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_left_weakening [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_not_a_function [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_not_a_pair [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_subject_reduction [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed [definition, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_implies_WellTyped [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_left_weakening [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_not_a_function [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_not_a_pair [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_subject_reduction [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed [definition, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_implies_WellTyped [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_left_weakening [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_not_a_function [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_not_a_pair [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_subject_reduction [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_appFun [inductive, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_appFun_intro [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_const [inductive, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_const_intro [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_fstProj [inductive, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_fstProj_intro [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_sndProj [inductive, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_sndProj_intro [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_var [inductive, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_var_intro [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed [inductive, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_app [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_base [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_fst [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_Reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN_aux1 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN_aux2 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN_aux3 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_WellTyped [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_left_weakening [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_not_a_function [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_not_a_pair [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_snd [constructor, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_subject_reduction [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.PreRed_implies_Reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible [definition, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible2 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible3 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible3_cor [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible4 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible5 [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_base [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_fun [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_implies_WellTyped [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_left_weakening [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_prod [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_subject_reduction [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_subject_reduction_star [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Second_projections_are_reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_fun_intro [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_pair_intro [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_subst_inversion [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_var_intro [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Variables_are_reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.WellTyped_implies_Reductible [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.WellTyped_implies_Reductible_aux [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.WellTyped_implies_SN [lemma, in SimplyTypedLambdaCalculus_normalization]
LambdaCalculus.LEnv [definition, in SimplyTypedLambdaCalculus]
LambdaCalculus.lift_at_depth_in_term [definition, in SimplyTypedLambdaCalculus]
LambdaCalculus.lift_at_depth_in_var [definition, in SimplyTypedLambdaCalculus]
LambdaCalculus.lift_in_term [definition, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm [inductive, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_app [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_const [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_fst [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_fun [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_pair [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_snd [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_var [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_liftings_aux [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_lifting_and_substitution [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_lifting_and_substitution_aux [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_lifting_and_substitution_2_aux [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_substitutions [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm [inductive, in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTermStar [inductive, in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm_refl [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm_step [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm_trans [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_and_substitution_star [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_in_lifting [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_in_substitution [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_in_substitution_star [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_app_left [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_app_right [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_fst_cong [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_fun [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_pair_left [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_pair_right [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_snd_cong [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_app_left [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_app_redex [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_app_right [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_fst_cong [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_fst_redex [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_fun [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_pair_left [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_pair_right [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_snd_cong [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.R_snd_redex [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.Subject_reduction [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Subject_reduction_star [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_in_reduction [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_in_reduction_star [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_preserves_typing [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_preserves_typing_snoc [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.subst_in_term [definition, in SimplyTypedLambdaCalculus]
LambdaCalculus.subst_in_var [definition, in SimplyTypedLambdaCalculus]
LambdaCalculus.Successive_type_liftings_aux [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Successive_variable_liftings [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Type_lifting_stronger_than_substitution [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Type_lifting_stronger_than_substitution_aux [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_declaration_by_the_right [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_well_typing_by_the_left [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_well_typing_by_the_right [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_well_typing_by_the_right_aux [lemma, in SimplyTypedLambdaCalculus]
LambdaCalculus.WellTyped [inductive, in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_app [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_const [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_fst [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_fun [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_pair [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_snd [constructor, in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_var [constructor, in SimplyTypedLambdaCalculus]
LambdaConstants [module, in SimplyTypedLambdaCalculus]
LambdaConstants.LConst [axiom, in SimplyTypedLambdaCalculus]
LambdaConstants.LType [inductive, in SimplyTypedLambdaCalculus]
LambdaConstants.LType_base [constructor, in SimplyTypedLambdaCalculus]
LambdaConstants.LType_fun [constructor, in SimplyTypedLambdaCalculus]
LambdaConstants.LType_prod [constructor, in SimplyTypedLambdaCalculus]
LambdaConstants.type_of_const [axiom, in SimplyTypedLambdaCalculus]
length_of_append [lemma, in Util]
length_of_map [lemma, in Util]
length_of_snoc [lemma, in Util]
LexicographicExtension [section, in WellFoundation]
LexicographicExtension.A1 [variable, in WellFoundation]
LexicographicExtension.A2 [variable, in WellFoundation]
LexicographicExtension.R1 [variable, in WellFoundation]
LexicographicExtension.R2 [variable, in WellFoundation]
lexicographic_extension_preserves_well_foundedness [lemma, in WellFoundation]
ListAt_implies_ListFrom [lemma, in Util]
ListFrom_implies_ListAt [lemma, in Util]
List_at [inductive, in Util]
List_at_head [constructor, in Util]
List_at_of_map [lemma, in Util]
List_at_right_weakening [lemma, in Util]
List_at_snoc_tail [lemma, in Util]
List_at_tail [constructor, in Util]
List_forall [inductive, in Util]
List_forall [inductive, in WellFoundation]
List_forall3 [lemma, in WellFoundation]
List_forall_and_List_at [lemma, in Util]
List_forall_and_List_from [lemma, in Util]
List_forall_cons [constructor, in WellFoundation]
List_forall_cons [constructor, in Util]
List_forall_equal_maps [lemma, in Util]
List_forall_equal_maps_cor1 [lemma, in Util]
List_forall_implies_forall [lemma, in Util]
List_forall_implies_Forall2 [lemma, in Util]
List_forall_implies_Forall2_right [lemma, in Util]
List_forall_implies_map_id [lemma, in Util]
List_forall_nil [constructor, in WellFoundation]
List_forall_nil [constructor, in Util]
List_forall_of_append_cor1 [lemma, in Util]
List_forall_of_append_elim [lemma, in Util]
List_forall_of_append_intro [lemma, in Util]
List_forall_of_map [lemma, in Util]
List_forall_section [section, in WellFoundation]
List_forall_section.A [variable, in WellFoundation]
List_from [inductive, in Util]
List_from_domain [lemma, in Util]
List_from_head [constructor, in Util]
List_from_inversion_on_length [lemma, in Util]
List_from_is_a_partial_function [lemma, in Util]
List_from_lem1 [lemma, in Util]
List_from_lem1_cor1 [lemma, in Util]
List_from_lem2 [lemma, in Util]
List_from_lem3 [lemma, in Util]
List_from_lem4 [lemma, in Util]
List_from_lem6 [lemma, in Util]
List_from_of_map [lemma, in Util]
List_from_tail [constructor, in Util]
M
map_elim [lemma, in Util]map_id_is_id [lemma, in Util]
map_intro [lemma, in Util]
map_of_append [lemma, in Util]
MatchCompNat [library]
Match2 [lemma, in MatchCompNat]
Match2_diff [lemma, in MatchCompNat]
Match3 [lemma, in MatchCompNat]
Match3_diff [lemma, in MatchCompNat]
match_comp_nat2 [definition, in MatchCompNat]
match_comp_nat2_aux_0 [lemma, in MatchCompNat]
match_comp_nat2_aux_1 [lemma, in MatchCompNat]
match_comp_nat2_aux_2 [lemma, in MatchCompNat]
match_comp_nat2_ge [lemma, in MatchCompNat]
match_comp_nat2_lt [lemma, in MatchCompNat]
match_comp_nat3 [definition, in MatchCompNat]
match_comp_nat3_aux_1 [lemma, in MatchCompNat]
match_comp_nat3_aux_2 [lemma, in MatchCompNat]
match_comp_nat3_aux_3 [lemma, in MatchCompNat]
match_comp_nat3_eq [lemma, in MatchCompNat]
match_comp_nat3_gt [lemma, in MatchCompNat]
match_comp_nat3_lt [lemma, in MatchCompNat]
myarith_1 [lemma, in Util]
myarith_2 [lemma, in Util]
My_Auxiliary [module, in Typing]
My_Auxiliary_proofs [module, in Confluence]
My_Binders [module, in Substitutions]
My_Binders_proofs [module, in Substitutions_proofs]
My_BoundCompliantSubstitutions_proofs [module, in TypeSubstitutionInTyping]
My_Confluence [module, in Typing_proofs]
My_Constants [module, in Normalization_proofs]
My_LambdaCalculus [module, in SimplyTypedLambdaCalculus_normalization]
My_LambdaCalculusNormalization [module, in Normalization_proofs]
My_Normalization_proofs [module, in TransitivityElimination_proofs]
My_Progress_proofs [module, in BoundCompliantSubstitutions_proofs]
My_Semantics [module, in Binders_proofs]
My_SubjectReduction_preliminaries [module, in SubjectReduction_proofs]
My_SubjectReduction_proofs [module, in TypeSafety]
My_Substitutions [module, in Auxiliary]
My_Substitutions_proofs [module, in Auxiliary_proofs]
My_Subtyping_proofs [module, in Normalization_proofs]
My_TermSubstitutionInTyping [module, in SubjectReduction_preliminaries]
My_TransitivityElimination_proofs [module, in Progress_proofs]
My_TypeSubstitutionInTyping [module, in TermSubstitutionInTyping]
My_Typing [module, in WellFormedness]
My_Typing_proofs [module, in Subtyping_proofs]
My_WellFormedness [module, in Semantics]
N
natSet [definition, in Util]natSet_add [definition, in Util]
natSet_empty [definition, in Util]
natSet_in [definition, in Util]
natSet_union [definition, in Util]
Normalization_proofs [library]
P
plus_minus_assoc [lemma, in Util]PreReductible [module, in SimplyTypedLambdaCalculus_normalization]
PreReductible_appFun [module, in SimplyTypedLambdaCalculus_normalization]
PreReductible_const [module, in SimplyTypedLambdaCalculus_normalization]
PreReductible_fstProj [module, in SimplyTypedLambdaCalculus_normalization]
PreReductible_sndProj [module, in SimplyTypedLambdaCalculus_normalization]
PreReductible_var [module, in SimplyTypedLambdaCalculus_normalization]
Program [module, in Syntax]
Program.classSuper [axiom, in Syntax]
Program.ClassSym [axiom, in Syntax]
Program.ClassSym_eqdec [axiom, in Syntax]
Program.classTypeParams [axiom, in Syntax]
Program.Class_type [definition, in Syntax]
Program.ConstrKind [constructor, in Syntax]
Program.ConstrKindList [constructor, in Syntax]
Program.fieldOwner [axiom, in Syntax]
Program.FieldSym [axiom, in Syntax]
Program.FieldSym_eqdec [axiom, in Syntax]
Program.FieldTerm_cons [constructor, in Syntax]
Program.FieldTerm_nil [constructor, in Syntax]
Program.fieldType [axiom, in Syntax]
Program.Fun_type [definition, in Syntax]
Program.is_classType [definition, in Syntax]
Program.KindC [inductive, in Syntax]
Program.KindS [inductive, in Syntax]
Program.Kind_cons [constructor, in Syntax]
Program.Kind_constr [constructor, in Syntax]
Program.Kind_nil [constructor, in Syntax]
Program.Kind_tuple [constructor, in Syntax]
Program.Kind_WD [inductive, in Syntax]
Program.mainTerm [axiom, in Syntax]
Program.methodImpl [axiom, in Syntax]
Program.methodOwner [axiom, in Syntax]
Program.methodParams [axiom, in Syntax]
Program.MethodSym [axiom, in Syntax]
Program.MethodSym_eqdec [axiom, in Syntax]
Program.methodType [axiom, in Syntax]
Program.methodTypeParams [axiom, in Syntax]
Program.Term [inductive, in Syntax]
Program.TermEnv [definition, in Syntax]
Program.Term_call [constructor, in Syntax]
Program.Term_cons [constructor, in Syntax]
Program.Term_new [constructor, in Syntax]
Program.Term_nil [constructor, in Syntax]
Program.Term_select [constructor, in Syntax]
Program.Term_var [constructor, in Syntax]
Program.TupleKind [constructor, in Syntax]
Program.TypeC [inductive, in Syntax]
Program.TypeConstr [constructor, in Syntax]
Program.TypeConstrList [constructor, in Syntax]
Program.TypeEnv [definition, in Syntax]
Program.TypeOption [constructor, in Syntax]
Program.TypeParam [constructor, in Syntax]
Program.TypeParamList [constructor, in Syntax]
Program.TypeS [inductive, in Syntax]
Program.TypeSection [constructor, in Syntax]
Program.TypeTuple [constructor, in Syntax]
Program.TypeVar [definition, in Syntax]
Program.Type_ [constructor, in Syntax]
Program.Type_apply [constructor, in Syntax]
Program.Type_class [constructor, in Syntax]
Program.Type_cons [constructor, in Syntax]
Program.Type_fun [constructor, in Syntax]
Program.Type_nil [constructor, in Syntax]
Program.Type_none [constructor, in Syntax]
Program.Type_param [constructor, in Syntax]
Program.Type_proj [constructor, in Syntax]
Program.Type_section [constructor, in Syntax]
Program.Type_some [constructor, in Syntax]
Program.Type_tuple [constructor, in Syntax]
Program.Type_var [constructor, in Syntax]
Program.Var [definition, in Syntax]
Program.Var_type [definition, in Syntax]
Program.WD_cons [constructor, in Syntax]
Program.WD_constr [constructor, in Syntax]
Program.WD_nil [constructor, in Syntax]
Program.WD_tuple [constructor, in Syntax]
Progress_proofs [library]
ProveReductible [module, in SimplyTypedLambdaCalculus_normalization]
ProveReductible_appFun [module, in SimplyTypedLambdaCalculus_normalization]
ProveReductible_const [module, in SimplyTypedLambdaCalculus_normalization]
ProveReductible_fstProj [module, in SimplyTypedLambdaCalculus_normalization]
ProveReductible_sndProj [module, in SimplyTypedLambdaCalculus_normalization]
ProveReductible_var [module, in SimplyTypedLambdaCalculus_normalization]
R
RList [inductive, in WellFoundation]RList_head [constructor, in WellFoundation]
RList_tail [constructor, in WellFoundation]
RPair [inductive, in WellFoundation]
RPair_fst [constructor, in WellFoundation]
RPair_snd [constructor, in WellFoundation]
Rplus [inductive, in Util]
Rplus1 [inductive, in Util]
Rplus1_implies_Rplus [lemma, in Util]
Rplus1_is_transitive [lemma, in Util]
Rplus1_of_symRel [lemma, in Util]
Rplus_implies_Rplus1 [lemma, in Util]
Rplus_is_transitive [lemma, in Util]
Rplus_of_symRel [lemma, in Util]
Rplus_Section [section, in Util]
Rplus_Section.A [variable, in Util]
Rplus_Section.R [variable, in Util]
RTriple1 [lemma, in WellFoundation]
RTriple2 [lemma, in WellFoundation]
RTriple3 [lemma, in WellFoundation]
S
Semantics [library]SequenceExtension [section, in WellFoundation]
SequenceExtension.A [variable, in WellFoundation]
SequenceExtension.R [variable, in WellFoundation]
sequence_extension_preserves_accessibility [lemma, in WellFoundation]
sequence_extension_preserves_accessibility_aux [lemma, in WellFoundation]
sequence_extension_preserves_well_foundedness [lemma, in WellFoundation]
SetProgram [module, in Auxiliary_proofs]
SetProgram [module, in Progress_proofs]
SetProgram [module, in WellFormedness]
SetProgram [module, in TermSubstitutionInTyping]
SetProgram [module, in Semantics]
SetProgram [module, in Binders]
SetProgram [module, in Typing]
SetProgram [module, in TypeSafety]
SetProgram [module, in Confluence]
SetProgram [module, in SubjectReduction_proofs]
SetProgram [module, in BoundCompliantSubstitutions_proofs]
SetProgram [module, in Subtyping_proofs]
SetProgram [module, in Substitutions]
SetProgram [module, in Normalization_proofs]
SetProgram [module, in Binders_proofs]
SetProgram [module, in TransitivityElimination_proofs]
SetProgram [module, in Auxiliary]
SetProgram [module, in Typing_proofs]
SetProgram [module, in Substitutions_proofs]
SetProgram [module, in SubjectReduction_preliminaries]
SetProgram [module, in TypeSubstitutionInTyping]
SetProgram.Accessibility_is_anti_reflexive [lemma, in SubjectReduction_preliminaries]
SetProgram.BetaType [inductive, in SubjectReduction_preliminaries]
SetProgram.BetaType_implies_subtyping_lem1 [lemma, in SubjectReduction_preliminaries]
SetProgram.BetaType_refl [constructor, in SubjectReduction_preliminaries]
SetProgram.BetaType_step [constructor, in SubjectReduction_preliminaries]
SetProgram.BetaType_sym [constructor, in SubjectReduction_preliminaries]
SetProgram.BetaType_trans [constructor, in SubjectReduction_preliminaries]
SetProgram.Bound [inductive, in Auxiliary]
SetProgram.by_omega1 [lemma, in Typing_proofs]
SetProgram.B_Class [constructor, in Auxiliary]
SetProgram.B_Red [constructor, in Auxiliary]
SetProgram.B_Var [constructor, in Auxiliary]
SetProgram.ChurchRosser [lemma, in SubjectReduction_preliminaries]
SetProgram.classes_are_well_kinded [axiom, in WellFormedness]
SetProgram.classInheritance [inductive, in WellFormedness]
SetProgram.classInheritance_intro [constructor, in WellFormedness]
SetProgram.ClassSat [definition, in WellFormedness]
SetProgram.classTypeParams_closed [lemma, in SubjectReduction_preliminaries]
SetProgram.classtype_expansion_preserves_well_kindedness_1 [lemma, in TransitivityElimination_proofs]
SetProgram.Class_inheritance_is_anti_reflexive [lemma, in SubjectReduction_preliminaries]
SetProgram.Class_inheritance_is_well_founded [axiom, in WellFormedness]
SetProgram.Class_kind_existence [lemma, in Normalization_proofs]
SetProgram.Class_subtyping [inductive, in Auxiliary]
SetProgram.Class_subtyping_aux1 [lemma, in SubjectReduction_preliminaries]
SetProgram.Class_subtyping_implies_subtyping [lemma, in SubjectReduction_proofs]
SetProgram.Class_subtyping_subject_reduction [lemma, in SubjectReduction_preliminaries]
SetProgram.Class_type_expansion_preserves_well_kindedness [lemma, in TransitivityElimination_proofs]
SetProgram.Class_type_subtyping_injection [lemma, in SubjectReduction_preliminaries]
SetProgram.Class_type_subtyping_injection_aux1 [lemma, in SubjectReduction_preliminaries]
SetProgram.Class_type_subtyping_is_linear [lemma, in SubjectReduction_preliminaries]
SetProgram.Class_WK [inductive, in WellFormedness]
SetProgram.Class_WK_intro [constructor, in WellFormedness]
SetProgram.clos_refl [inductive, in Subtyping_proofs]
SetProgram.Conform [inductive, in SubjectReduction_preliminaries]
SetProgram.Conform_intro [constructor, in SubjectReduction_preliminaries]
SetProgram.CS_Extends [constructor, in Auxiliary]
SetProgram.CS_Refl [constructor, in Auxiliary]
SetProgram.Declaration_of_type_variable_is_preserved_by_reduction [lemma, in Subtyping_proofs]
SetProgram.Declaration_of_type_variable_1 [lemma, in Typing_proofs]
SetProgram.Declaration_of_type_variable_1_bis [lemma, in Typing_proofs]
SetProgram.Declaration_of_type_variable_2 [lemma, in Typing_proofs]
SetProgram.Declaration_of_type_variable_3 [lemma, in Typing_proofs]
SetProgram.decl_of_typeVar [inductive, in Auxiliary]
SetProgram.decl_of_typeVar_and_kind_of [lemma, in Typing_proofs]
SetProgram.decl_of_typeVar_and_kind_of_cor1 [lemma, in Typing_proofs]
SetProgram.decl_of_typeVar_intro [constructor, in Auxiliary]
SetProgram.decl_of_typeVar_is_a_partial_function [lemma, in Typing_proofs]
SetProgram.DiamondProperty [definition, in Confluence]
SetProgram.DiamondProperty_aux [definition, in Confluence]
SetProgram.Dropping_preserves_kind_of [lemma, in Typing_proofs]
SetProgram.drop_at_depth_in_type [definition, in Binders]
SetProgram.drop_at_depth_in_typeEnv [definition, in Binders]
SetProgram.drop_at_depth_in_typeVar [definition, in Binders]
SetProgram.drop_in_type [definition, in Binders]
SetProgram.drop_in_typeEnv [definition, in Binders]
SetProgram.drop_in_typeVar [definition, in Binders]
SetProgram.Equality_preserves_diamond_property [lemma, in Confluence]
SetProgram.Evaluate [inductive, in Semantics]
SetProgram.evaluated_fieldTerm_cons [constructor, in Semantics]
SetProgram.evaluated_fieldTerm_nil [constructor, in Semantics]
SetProgram.evaluated_new [constructor, in Semantics]
SetProgram.evaluated_term [inductive, in Semantics]
SetProgram.evaluated_term_cons [constructor, in Semantics]
SetProgram.evaluated_term_dec [lemma, in Progress_proofs]
SetProgram.evaluated_term_new_inversion [lemma, in Progress_proofs]
SetProgram.evaluated_term_nil [constructor, in Semantics]
SetProgram.EvaluateMain [definition, in Semantics]
SetProgram.Evaluate_end [constructor, in Semantics]
SetProgram.Evaluate_step [constructor, in Semantics]
SetProgram.FieldDecl_WF [inductive, in WellFormedness]
SetProgram.FieldDecl_WF_intro [constructor, in WellFormedness]
SetProgram.fields_of_fieldTermList [definition, in Typing]
SetProgram.FieldTermListI [constructor, in Typing]
SetProgram.fieldTerm_lookup [inductive, in Semantics]
SetProgram.fieldTerm_lookup_head [constructor, in Semantics]
SetProgram.fieldTerm_lookup_tail [constructor, in Semantics]
SetProgram.FieldVal_WF [inductive, in SubjectReduction_proofs]
SetProgram.FieldVal_WF_intro [constructor, in SubjectReduction_proofs]
SetProgram.field_declarations_are_well_formed [axiom, in WellFormedness]
SetProgram.Forall2_app [lemma, in Typing_proofs]
SetProgram.Forall_ParamSat [definition, in Typing]
SetProgram.Forall_ParamSat_build [inductive, in Typing]
SetProgram.Forall_ParamSat_build_cons [constructor, in Typing]
SetProgram.Forall_ParamSat_build_nil [constructor, in Typing]
SetProgram.fv_at_depth_in_type [definition, in Binders]
SetProgram.fv_at_depth_in_typeVar [definition, in Binders]
SetProgram.fv_in_type [definition, in Binders]
SetProgram.Info_WK [definition, in Progress_proofs]
SetProgram.IsComplete [inductive, in Typing]
SetProgram.IsComplete_fields [definition, in Typing]
SetProgram.IsComplete_intro [constructor, in Typing]
SetProgram.IsComplete_methods [definition, in Typing]
SetProgram.is_arbitraryType [definition, in Typing]
SetProgram.KindS_at [inductive, in Auxiliary]
SetProgram.KindS_at_and_size [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.KindS_at_is_a_partial_function [lemma, in Progress_proofs]
SetProgram.Kind_at_head [constructor, in Auxiliary]
SetProgram.Kind_at_tail [constructor, in Auxiliary]
SetProgram.kind_equality_implies_param_satisfaction [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.kind_equality_implies_poly_satisfaction [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.kind_of [inductive, in Auxiliary]
SetProgram.kind_of_is_a_partial_function [lemma, in Typing_proofs]
SetProgram.Kind_of_param [constructor, in Auxiliary]
SetProgram.Kind_of_paramList_cons [constructor, in Auxiliary]
SetProgram.Kind_of_paramList_nil [constructor, in Auxiliary]
SetProgram.kind_of_params_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.kind_of_params_inversion_variant1 [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Kind_of_section [constructor, in Auxiliary]
SetProgram.length_of_typeLift [lemma, in Typing_proofs]
SetProgram.length_of_typeSubst [lemma, in Typing_proofs]
SetProgram.Lifting_in_closed_type_aux [lemma, in Subtyping_proofs]
SetProgram.Lifting_in_closed_type_cor1 [lemma, in Subtyping_proofs]
SetProgram.Lifting_in_closed_type_cor2 [lemma, in Subtyping_proofs]
SetProgram.Lifting_preserves_class_types [lemma, in Typing_proofs]
SetProgram.Lifting_preserves_kind_of [lemma, in Typing_proofs]
SetProgram.Lifting_preserves_kind_of_reverse [lemma, in Typing_proofs]
SetProgram.Lifting_preserves_removeBounds [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Lifting_then_dropping [lemma, in Binders_proofs]
SetProgram.Lifting_then_dropping_in_typeVar [lemma, in Binders_proofs]
SetProgram.lift_at_depth_in_term [definition, in Binders]
SetProgram.lift_at_depth_in_type [definition, in Binders]
SetProgram.lift_at_depth_in_typeEnv [definition, in Binders]
SetProgram.lift_at_depth_in_typeVar [definition, in Binders]
SetProgram.lift_at_depth_in_var [definition, in Binders]
SetProgram.lift_in_term [definition, in Binders]
SetProgram.lift_in_type [definition, in Binders]
SetProgram.lift_in_typeEnv [definition, in Binders]
SetProgram.lift_in_typeVar_by_zero [lemma, in Binders_proofs]
SetProgram.lift_in_type_by_zero [lemma, in Binders_proofs]
SetProgram.lift_of_cons_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.lift_of_LTerm_proj [lemma, in Normalization_proofs]
SetProgram.lift_of_snoc [lemma, in Typing_proofs]
SetProgram.lift_of_snoc_aux [lemma, in Typing_proofs]
SetProgram.lift_of_some_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.List_from_implies_TypeSection_at [lemma, in Typing_proofs]
SetProgram.list_of_termList [definition, in Semantics]
SetProgram.LTerm_proj [definition, in Normalization_proofs]
SetProgram.main_term_is_well_typed [axiom, in WellFormedness]
SetProgram.MethodDecl_WF [inductive, in WellFormedness]
SetProgram.MethodDecl_WF_intro [constructor, in WellFormedness]
SetProgram.MethodImpl_WF [inductive, in WellFormedness]
SetProgram.MethodImpl_WF_intro [constructor, in WellFormedness]
SetProgram.methodParams_closed [lemma, in SubjectReduction_preliminaries]
SetProgram.methodTypeParams_closed [lemma, in SubjectReduction_preliminaries]
SetProgram.methodType_closed [lemma, in SubjectReduction_preliminaries]
SetProgram.method_declarations_are_well_formed [axiom, in WellFormedness]
SetProgram.method_implementations_are_well_formed [axiom, in WellFormedness]
SetProgram.My_Constants.LConst [definition, in Normalization_proofs]
SetProgram.My_Constants.LConst_class [constructor, in Normalization_proofs]
SetProgram.My_Constants.LConst_definition [inductive, in Normalization_proofs]
SetProgram.My_Constants.LConst_nil [constructor, in Normalization_proofs]
SetProgram.My_Constants.LConst_none [constructor, in Normalization_proofs]
SetProgram.My_Constants.LType [inductive, in Normalization_proofs]
SetProgram.My_Constants.LType_base [constructor, in Normalization_proofs]
SetProgram.My_Constants.LType_fun [constructor, in Normalization_proofs]
SetProgram.My_Constants.LType_prod [constructor, in Normalization_proofs]
SetProgram.My_Constants.type_of [inductive, in Normalization_proofs]
SetProgram.My_Constants.type_of_const [definition, in Normalization_proofs]
SetProgram.My_Constants.type_of_const_class [constructor, in Normalization_proofs]
SetProgram.My_Constants.type_of_const_def [inductive, in Normalization_proofs]
SetProgram.My_Constants.type_of_const_nil [constructor, in Normalization_proofs]
SetProgram.My_Constants.type_of_const_none [constructor, in Normalization_proofs]
SetProgram.My_Constants.Type_of_intro [constructor, in Normalization_proofs]
SetProgram.My_Constants.Type_of_is_a_partial_function [lemma, in Normalization_proofs]
SetProgram.My_Constants.type_of_kind [definition, in Normalization_proofs]
SetProgram.Parallel_reduction_and_list_lookup [lemma, in Confluence]
SetProgram.Parallel_reduction_in_lifting [lemma, in Confluence]
SetProgram.Parallel_reduction_is_confluent [lemma, in Confluence]
SetProgram.ParamSat [inductive, in Typing]
SetProgram.ParamSat_intro [constructor, in Typing]
SetProgram.Param_satisfaction_left_weakening [lemma, in Subtyping_proofs]
SetProgram.Permuting_type_liftings_aux [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_liftings_cor1 [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_aux [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_cor1 [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_2_aux [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_2_cor1 [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_substitutions [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_substitutions_cor1 [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_substitutions_cor2 [lemma, in Substitutions_proofs]
SetProgram.Permuting_type_substitutions_in_lists [lemma, in TypeSubstitutionInTyping]
SetProgram.Permuting_type_substitutions_in_lists_cor1 [lemma, in TypeSubstitutionInTyping]
SetProgram.Permuting_type_substitutions_in_lists_cor2 [lemma, in TypeSubstitutionInTyping]
SetProgram.Pointwise_subtyping [definition, in Typing]
SetProgram.polySubst_by_snoc [lemma, in TermSubstitutionInTyping]
SetProgram.polyTermSubst_in_term [definition, in Semantics]
SetProgram.Poly_term_substitution_preserves_typing [lemma, in TermSubstitutionInTyping]
SetProgram.Poly_term_substitution_preserves_typing_cor1 [lemma, in TermSubstitutionInTyping]
SetProgram.Poly_term_substitution_preserves_typing_cor2 [lemma, in TermSubstitutionInTyping]
SetProgram.Preservation_of_semantics [lemma, in Normalization_proofs]
SetProgram.Preservation_of_semantics_cor1 [lemma, in Normalization_proofs]
SetProgram.Preservation_of_typing [lemma, in Normalization_proofs]
SetProgram.Progress [lemma, in Progress_proofs]
SetProgram.Progress_aux_1 [lemma, in Progress_proofs]
SetProgram.RedTerm [inductive, in Semantics]
SetProgram.RedTermStar [definition, in TypeSafety]
SetProgram.RedType [inductive, in Auxiliary]
SetProgram.RedTypeEnv [inductive, in Auxiliary]
SetProgram.RedTypeEnvStar [inductive, in Auxiliary_proofs]
SetProgram.RedTypeEnv_included_in_RedTypeEnv_snoc [lemma, in Subtyping_proofs]
SetProgram.RedTypeEnv_included_in_RedTypeEnv_snoc_aux1 [lemma, in Subtyping_proofs]
SetProgram.RedTypeEnv_included_in_RedTypeEnv_snoc_aux2 [lemma, in Subtyping_proofs]
SetProgram.RedTypeEnv_refl [constructor, in Auxiliary_proofs]
SetProgram.RedTypeEnv_snoc [inductive, in Subtyping_proofs]
SetProgram.RedTypeEnv_snoc_included_in_RedTypeEnv [lemma, in Subtyping_proofs]
SetProgram.RedTypeEnv_snoc_included_in_RedTypeEnv_aux1 [lemma, in Subtyping_proofs]
SetProgram.RedTypeEnv_snoc_included_in_RedTypeEnv_aux2 [lemma, in Subtyping_proofs]
SetProgram.RedTypeEnv_step [constructor, in Auxiliary_proofs]
SetProgram.RedTypeEnv_trans [constructor, in Auxiliary_proofs]
SetProgram.RedTypePar [inductive, in Confluence]
SetProgram.RedTypeParTrans [definition, in Confluence]
SetProgram.RedTypeParTrans_has_diamond_property [lemma, in Confluence]
SetProgram.RedTypeParTrans_included_in_RedTypeStar [lemma, in Confluence]
SetProgram.RedTypeParTrans_in_lifting [lemma, in Subtyping_proofs]
SetProgram.RedTypePar_included_in_RedTypeStar [lemma, in Confluence]
SetProgram.RedTypeStar [inductive, in Auxiliary_proofs]
SetProgram.RedTypeStar_implies_BetaType [lemma, in SubjectReduction_preliminaries]
SetProgram.RedTypeStar_included_in_RedTypeParTrans [lemma, in Confluence]
SetProgram.RedTypeStar_in_lifting [lemma, in Subtyping_proofs]
SetProgram.RedType_included_in_RedTypePar [lemma, in Confluence]
SetProgram.RedType_refl [constructor, in Auxiliary_proofs]
SetProgram.RedType_step [constructor, in Auxiliary_proofs]
SetProgram.RedType_trans [constructor, in Auxiliary_proofs]
SetProgram.Reduction_and_substitution_par [lemma, in Confluence]
SetProgram.Reduction_and_substitution_star [lemma, in Auxiliary_proofs]
SetProgram.Reduction_in_lifting [lemma, in Auxiliary_proofs]
SetProgram.Reduction_in_substitution [lemma, in Auxiliary_proofs]
SetProgram.Reduction_in_substitution_star [lemma, in Auxiliary_proofs]
SetProgram.Reduction_of_class_types [lemma, in Subtyping_proofs]
SetProgram.Reduction_of_class_types_star [lemma, in Subtyping_proofs]
SetProgram.Reduction_of_variable_types [lemma, in Subtyping_proofs]
SetProgram.Reduction_of_variable_types_star [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_class_types [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_forall_satisfaction [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_forall_satisfaction_build [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_kind_of [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_removeBounds [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_satisfaction [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_simultaneous_satisfaction [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_subtyping [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_subtypingWTR [lemma, in TransitivityElimination_proofs]
SetProgram.Reduction_preserves_TypeSection_at [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_TypeS_at [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_type_declaration_lookup [lemma, in Subtyping_proofs]
SetProgram.Reduction_preserves_type_of [lemma, in Normalization_proofs]
SetProgram.removeBounds [inductive, in Typing]
SetProgram.removeBounds_and_kind_of_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_invariant_by_lifting [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_invariant_by_substitution [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_is_idempotent [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_of_params_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_param [constructor, in Typing]
SetProgram.removeBounds_param_cons [constructor, in Typing]
SetProgram.removeBounds_param_nil [constructor, in Typing]
SetProgram.removeBounds_preserves_kind_of [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_preserves_well_kindedness [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_section [constructor, in Typing]
SetProgram.removeBounds_then_substitution [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Rplus_app_left [lemma, in Normalization_proofs]
SetProgram.Rplus_app_right [lemma, in Normalization_proofs]
SetProgram.Rplus_fst_cong [lemma, in Normalization_proofs]
SetProgram.Rplus_fun [lemma, in Normalization_proofs]
SetProgram.Rplus_pair_left [lemma, in Normalization_proofs]
SetProgram.Rplus_pair_right [lemma, in Normalization_proofs]
SetProgram.Rplus_proj_cong [lemma, in Normalization_proofs]
SetProgram.Rplus_snd_cong [lemma, in Normalization_proofs]
SetProgram.RTE_head [constructor, in Auxiliary]
SetProgram.RTE_head_star [lemma, in SubjectReduction_proofs]
SetProgram.RTE_snoc_head [constructor, in Subtyping_proofs]
SetProgram.RTE_snoc_tail [constructor, in Subtyping_proofs]
SetProgram.RTE_tail [constructor, in Auxiliary]
SetProgram.RTE_tail_star [lemma, in SubjectReduction_proofs]
SetProgram.RTP_apply_left_right [constructor, in Confluence]
SetProgram.RTP_apply_redex [constructor, in Confluence]
SetProgram.RTP_class [constructor, in Confluence]
SetProgram.RTP_cons_head_tail [constructor, in Confluence]
SetProgram.RTP_fun_left_right [constructor, in Confluence]
SetProgram.RTP_nil [constructor, in Confluence]
SetProgram.RTP_none [constructor, in Confluence]
SetProgram.RTP_param_left_right [constructor, in Confluence]
SetProgram.RTP_proj_redex [constructor, in Confluence]
SetProgram.RTP_proj_sub [constructor, in Confluence]
SetProgram.RTP_refl [lemma, in Confluence]
SetProgram.RTP_section [constructor, in Confluence]
SetProgram.RTP_some [constructor, in Confluence]
SetProgram.RTP_tuple [constructor, in Confluence]
SetProgram.RTP_var [constructor, in Confluence]
SetProgram.RTS_apply_left [lemma, in Auxiliary_proofs]
SetProgram.RTS_apply_right [lemma, in Auxiliary_proofs]
SetProgram.RTS_class_type [lemma, in SubjectReduction_proofs]
SetProgram.RTS_cons_head [lemma, in Auxiliary_proofs]
SetProgram.RTS_cons_inversion [lemma, in Subtyping_proofs]
SetProgram.RTS_cons_inversion_right [lemma, in Subtyping_proofs]
SetProgram.RTS_cons_tail [lemma, in Auxiliary_proofs]
SetProgram.RTS_fun_left [lemma, in Auxiliary_proofs]
SetProgram.RTS_fun_right [lemma, in Auxiliary_proofs]
SetProgram.RTS_nil_inversion [lemma, in Subtyping_proofs]
SetProgram.RTS_param_inversion [lemma, in Subtyping_proofs]
SetProgram.RTS_param_left [lemma, in Auxiliary_proofs]
SetProgram.RTS_param_right [lemma, in Auxiliary_proofs]
SetProgram.RTS_proj_sub [lemma, in Auxiliary_proofs]
SetProgram.RTS_section [lemma, in Auxiliary_proofs]
SetProgram.RTS_section_inversion [lemma, in Subtyping_proofs]
SetProgram.RTS_snoc_left [lemma, in Subtyping_proofs]
SetProgram.RTS_snoc_right [lemma, in Subtyping_proofs]
SetProgram.RTS_some [lemma, in Auxiliary_proofs]
SetProgram.RTS_some_inversion [lemma, in Subtyping_proofs]
SetProgram.RTS_some_inversion_right [lemma, in Subtyping_proofs]
SetProgram.RTS_tuple [lemma, in Auxiliary_proofs]
SetProgram.RT_apply_left [constructor, in Auxiliary]
SetProgram.RT_apply_redex [constructor, in Auxiliary]
SetProgram.RT_apply_right [constructor, in Auxiliary]
SetProgram.RT_cons_head [constructor, in Auxiliary]
SetProgram.RT_cons_tail [constructor, in Auxiliary]
SetProgram.RT_fun_left [constructor, in Auxiliary]
SetProgram.RT_fun_right [constructor, in Auxiliary]
SetProgram.RT_param_left [constructor, in Auxiliary]
SetProgram.RT_param_right [constructor, in Auxiliary]
SetProgram.RT_proj_redex [constructor, in Auxiliary]
SetProgram.RT_proj_sub [constructor, in Auxiliary]
SetProgram.RT_section [constructor, in Auxiliary]
SetProgram.RT_snoc_left [lemma, in Subtyping_proofs]
SetProgram.RT_snoc_right [lemma, in Subtyping_proofs]
SetProgram.RT_some [constructor, in Auxiliary]
SetProgram.RT_tuple [constructor, in Auxiliary]
SetProgram.R_call_left [constructor, in Semantics]
SetProgram.R_call_redex [constructor, in Semantics]
SetProgram.R_call_right [constructor, in Semantics]
SetProgram.R_cons_left [constructor, in Semantics]
SetProgram.R_cons_right [constructor, in Semantics]
SetProgram.R_fieldTerm_cons_left [constructor, in Semantics]
SetProgram.R_fieldTerm_cons_right [constructor, in Semantics]
SetProgram.R_new [constructor, in Semantics]
SetProgram.R_proj_cong [lemma, in Normalization_proofs]
SetProgram.R_proj_redex [lemma, in Normalization_proofs]
SetProgram.r_refl [constructor, in Subtyping_proofs]
SetProgram.R_select [constructor, in Semantics]
SetProgram.R_select_redex [constructor, in Semantics]
SetProgram.r_step [constructor, in Subtyping_proofs]
SetProgram.SameCategory [inductive, in Progress_proofs]
SetProgram.SameCategory_TypeConstr [constructor, in Progress_proofs]
SetProgram.SameCategory_TypeConstrList [constructor, in Progress_proofs]
SetProgram.SameCategory_TypeOption [constructor, in Progress_proofs]
SetProgram.SameCategory_TypeParam [constructor, in Progress_proofs]
SetProgram.SameCategory_TypeParamList [constructor, in Progress_proofs]
SetProgram.SameCategory_TypeSection [constructor, in Progress_proofs]
SetProgram.SameCategory_TypeTuple [constructor, in Progress_proofs]
SetProgram.SameCategory_Type_ [constructor, in Progress_proofs]
SetProgram.Satisfaction_implies_same_kind [lemma, in Progress_proofs]
SetProgram.Satisfaction_left_weakening [lemma, in Subtyping_proofs]
SetProgram.SC_Extends [constructor, in Auxiliary]
SetProgram.SC_Refl [constructor, in Auxiliary]
SetProgram.SectionSat [inductive, in Typing]
SetProgram.SectionSat_intro [constructor, in Typing]
SetProgram.Self_type_is_well_kinded [lemma, in SubjectReduction_proofs]
SetProgram.size [definition, in Confluence]
SetProgram.size_of_kind [definition, in BoundCompliantSubstitutions_proofs]
SetProgram.StarReduction_preserves_kind_of [lemma, in Subtyping_proofs]
SetProgram.StarReduction_preserves_removeBounds [lemma, in Subtyping_proofs]
SetProgram.StarReduction_preserves_TypeS_at [lemma, in Subtyping_proofs]
SetProgram.StarReduction_preserves_type_declaration_lookup [lemma, in Subtyping_proofs]
SetProgram.Subclass [inductive, in Auxiliary]
SetProgram.Subclass_implies_class_expansion [lemma, in Auxiliary_proofs]
SetProgram.SubInfo [inductive, in TermSubstitutionInTyping]
SetProgram.SubInfo_fieldTermList [constructor, in TermSubstitutionInTyping]
SetProgram.SubInfo_refl [lemma, in TermSubstitutionInTyping]
SetProgram.SubInfo_term [constructor, in TermSubstitutionInTyping]
SetProgram.SubInfo_termList [constructor, in TermSubstitutionInTyping]
SetProgram.SubInfo_trans [lemma, in TermSubstitutionInTyping]
SetProgram.SubInfo_trans_cor1 [lemma, in TermSubstitutionInTyping]
SetProgram.Subject_reduction [lemma, in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux1 [lemma, in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux2 [lemma, in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux3 [lemma, in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux4 [lemma, in SubjectReduction_proofs]
SetProgram.Subject_reduction_star [lemma, in TypeSafety]
SetProgram.Subject_reduction_star_cor1 [lemma, in TypeSafety]
SetProgram.SubRelation [definition, in Confluence]
SetProgram.Substitution_in_closed_type_aux [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Substitution_in_field_type [lemma, in Progress_proofs]
SetProgram.Substitution_in_method_param_types [lemma, in Progress_proofs]
SetProgram.Substitution_in_method_param_types_2 [lemma, in Progress_proofs]
SetProgram.Substitution_in_method_type [lemma, in Progress_proofs]
SetProgram.Substitution_in_method_type_params [lemma, in Progress_proofs]
SetProgram.Substitution_in_method_type_2 [lemma, in Progress_proofs]
SetProgram.Substitution_in_reduction [lemma, in Auxiliary_proofs]
SetProgram.Substitution_in_reduction_star [lemma, in Auxiliary_proofs]
SetProgram.Substitution_in_well_kinded_type_env [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Substitution_preserves_class_types [lemma, in Typing_proofs]
SetProgram.Substitution_preserves_kind_of [lemma, in Typing_proofs]
SetProgram.Substitution_preserves_removeBounds [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Substitution_preserves_well_kindedness_snoc [lemma, in Typing_proofs]
SetProgram.Subtyping [inductive, in Typing]
SetProgram.SubtypingWTR [inductive, in TransitivityElimination_proofs]
SetProgram.SubtypingWTR_implies_class_type_subtyping [lemma, in SubjectReduction_preliminaries]
SetProgram.SubtypingWTR_is_consistent_with_subclassing [lemma, in TransitivityElimination_proofs]
SetProgram.Subtyping_is_consistent_with_subclassing [lemma, in TransitivityElimination_proofs]
SetProgram.Subtyping_left_weakening [lemma, in Subtyping_proofs]
SetProgram.Successive_type_liftings [lemma, in Binders_proofs]
SetProgram.Successive_type_liftings_aux [lemma, in Binders_proofs]
SetProgram.Successive_type_liftings_cor1 [lemma, in Binders_proofs]
SetProgram.Successive_variable_liftings [lemma, in Binders_proofs]
SetProgram.SWTR_Beta_Left [constructor, in TransitivityElimination_proofs]
SetProgram.SWTR_beta_left_star [lemma, in TransitivityElimination_proofs]
SetProgram.SWTR_Beta_Right [constructor, in TransitivityElimination_proofs]
SetProgram.SWTR_beta_right_star [lemma, in TransitivityElimination_proofs]
SetProgram.SWTR_Class [constructor, in TransitivityElimination_proofs]
SetProgram.SWTR_Refl [constructor, in TransitivityElimination_proofs]
SetProgram.SWTR_Trans [lemma, in TransitivityElimination_proofs]
SetProgram.SWTR_Trans_aux [lemma, in TransitivityElimination_proofs]
SetProgram.SWTR_Var [constructor, in TransitivityElimination_proofs]
SetProgram.S_Beta_Left [constructor, in Typing]
SetProgram.S_beta_left_star [lemma, in Subtyping_proofs]
SetProgram.S_Beta_Right [constructor, in Typing]
SetProgram.S_beta_right_star [lemma, in Subtyping_proofs]
SetProgram.S_Class [constructor, in Typing]
SetProgram.S_Refl [constructor, in Typing]
SetProgram.S_Trans [constructor, in Typing]
SetProgram.S_Var [constructor, in Typing]
SetProgram.TermEnv_WK [definition, in TypeSubstitutionInTyping]
SetProgram.TermI [constructor, in Typing]
SetProgram.TermInfo [inductive, in Typing]
SetProgram.TermListI [constructor, in Typing]
SetProgram.termSubst_in_term [definition, in Substitutions]
SetProgram.termSubst_in_var [definition, in Substitutions]
SetProgram.Term_lifting_preserves_fields_of_fieldTermList [lemma, in TermSubstitutionInTyping]
SetProgram.Term_reduction_preserves_fields_of_fieldTermList [lemma, in SubjectReduction_proofs]
SetProgram.Term_substitution_preserves_fields_of_fieldTermList [lemma, in TermSubstitutionInTyping]
SetProgram.Term_substitution_preserves_typing [lemma, in TermSubstitutionInTyping]
SetProgram.Term_WT [inductive, in Typing]
SetProgram.TE_Beta [constructor, in TransitivityElimination_proofs]
SetProgram.TE_Class [constructor, in TransitivityElimination_proofs]
SetProgram.trans [inductive, in Normalization_proofs]
SetProgram.transcat_TypeConstr [constructor, in Normalization_proofs]
SetProgram.transcat_TypeConstrList [constructor, in Normalization_proofs]
SetProgram.transcat_TypeOption [constructor, in Normalization_proofs]
SetProgram.transcat_TypeParam [constructor, in Normalization_proofs]
SetProgram.transcat_TypeParamList [constructor, in Normalization_proofs]
SetProgram.transcat_TypeSection [constructor, in Normalization_proofs]
SetProgram.transcat_TypeTuple [constructor, in Normalization_proofs]
SetProgram.transcat_Type_ [constructor, in Normalization_proofs]
SetProgram.Transitive_closure_preserves_diamond_property [lemma, in Confluence]
SetProgram.Transitive_closure_preserves_diamond_property_aux [lemma, in Confluence]
SetProgram.Transitive_closure_preserves_inclusion [lemma, in Confluence]
SetProgram.TransitivityElimination [lemma, in TransitivityElimination_proofs]
SetProgram.TransitivityElimination_aux [lemma, in TransitivityElimination_proofs]
SetProgram.trans_apply [constructor, in Normalization_proofs]
SetProgram.trans_category [inductive, in Normalization_proofs]
SetProgram.trans_class [constructor, in Normalization_proofs]
SetProgram.trans_cons [constructor, in Normalization_proofs]
SetProgram.trans_fun [constructor, in Normalization_proofs]
SetProgram.trans_is_a_partial_function [lemma, in Normalization_proofs]
SetProgram.trans_nil [constructor, in Normalization_proofs]
SetProgram.trans_none [constructor, in Normalization_proofs]
SetProgram.trans_of_lift [lemma, in Normalization_proofs]
SetProgram.trans_of_typeSubst [lemma, in Normalization_proofs]
SetProgram.trans_param [constructor, in Normalization_proofs]
SetProgram.trans_proj [constructor, in Normalization_proofs]
SetProgram.trans_section [constructor, in Normalization_proofs]
SetProgram.trans_some [constructor, in Normalization_proofs]
SetProgram.trans_tuple [constructor, in Normalization_proofs]
SetProgram.trans_typeEnv [inductive, in Normalization_proofs]
SetProgram.trans_typeEnv_and_TypeSection_at [lemma, in Normalization_proofs]
SetProgram.trans_typeEnv_nil [constructor, in Normalization_proofs]
SetProgram.trans_typeEnv_snoc [constructor, in Normalization_proofs]
SetProgram.trans_var [constructor, in Normalization_proofs]
SetProgram.Typed_term_list [lemma, in SubjectReduction_proofs]
SetProgram.TypeEnv_WK [inductive, in Normalization_proofs]
SetProgram.TypeEnv_WK_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.TypeEnv_WK_inversion_cor1 [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.TypeEnv_WK_inversion_cor2 [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.TypeExp [inductive, in TransitivityElimination_proofs]
SetProgram.TypeParamList_ind [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.TypeParamList_WK_inversion [lemma, in Subtyping_proofs]
SetProgram.TypeSection_at [inductive, in Auxiliary]
SetProgram.TypeSection_at_and_kind_of [lemma, in Typing_proofs]
SetProgram.TypeSection_at_head [constructor, in Auxiliary]
SetProgram.TypeSection_at_implies_List_from [lemma, in Typing_proofs]
SetProgram.TypeSection_at_is_a_partial_function [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem1 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem1_cor1 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem2 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem3 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem4 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem5 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem6 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem7 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem8 [lemma, in Typing_proofs]
SetProgram.TypeSection_at_lem9 [lemma, in Subtyping_proofs]
SetProgram.TypeSection_at_tail [constructor, in Auxiliary]
SetProgram.typeSubst_in_term [definition, in Substitutions]
SetProgram.typeSubst_in_termEnv [definition, in TypeSubstitutionInTyping]
SetProgram.typeSubst_in_termInfo [definition, in TypeSubstitutionInTyping]
SetProgram.typeSubst_in_type [definition, in Substitutions]
SetProgram.typeSubst_in_typeEnv [definition, in Substitutions]
SetProgram.typeSubst_in_typeList [definition, in Typing]
SetProgram.typeSubst_in_typeVar [definition, in Substitutions]
SetProgram.typeSubst_of_class_type [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.typeSubst_of_cons_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.typeSubst_of_LTerm_proj [lemma, in Normalization_proofs]
SetProgram.typeSubst_of_snoc [lemma, in Typing_proofs]
SetProgram.typeSubst_of_some_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.TypeS_at [inductive, in Auxiliary]
SetProgram.TypeS_at_head [constructor, in Auxiliary]
SetProgram.TypeS_at_is_a_partial_function [lemma, in Auxiliary_proofs]
SetProgram.TypeS_at_is_preserved_by_reduction [lemma, in Subtyping_proofs]
SetProgram.TypeS_at_of_lift [lemma, in Auxiliary_proofs]
SetProgram.TypeS_at_of_lift_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.TypeS_at_of_typeSubst [lemma, in Auxiliary_proofs]
SetProgram.TypeS_at_of_typeSubst_inversion [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.TypeS_at_tail [constructor, in Auxiliary]
SetProgram.Type_env_reduction_preserves_typing [lemma, in SubjectReduction_proofs]
SetProgram.Type_eqdec [lemma, in Auxiliary_proofs]
SetProgram.Type_expansion_is_well_founded [lemma, in TransitivityElimination_proofs]
SetProgram.Type_expansion_is_well_founded_aux1 [lemma, in TransitivityElimination_proofs]
SetProgram.Type_lifting_stronger_than_substitution [lemma, in Substitutions_proofs]
SetProgram.Type_lifting_stronger_than_substitution_aux [lemma, in Substitutions_proofs]
SetProgram.type_of_of_lift [lemma, in Normalization_proofs]
SetProgram.type_of_of_typeSubst [lemma, in Normalization_proofs]
SetProgram.Type_reduction_is_confluent [lemma, in Confluence]
SetProgram.Type_reduction_is_well_founded [lemma, in Normalization_proofs]
SetProgram.Type_safety [lemma, in TypeSafety]
SetProgram.Type_substitution_preserves_fields_of_fieldTermList [lemma, in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_param_satisfaction [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_satisfaction [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_satisfaction_snoc [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_aux1 [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_cor1 [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_cor2 [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_snoc [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_typing [lemma, in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor1 [lemma, in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor2 [lemma, in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor3 [lemma, in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor4 [lemma, in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor5 [lemma, in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_well_kindedness [lemma, in Typing_proofs]
SetProgram.Type_substitution_preserves_well_kindedness_cor1 [lemma, in Typing_proofs]
SetProgram.Type_substitution_preserves_well_kindedness_cor2 [lemma, in Typing_proofs]
SetProgram.Type_WK [inductive, in Typing]
SetProgram.Typing_returns_well_kinded_types [lemma, in Progress_proofs]
SetProgram.Typing_returns_well_kinded_types_cor1 [lemma, in Progress_proofs]
SetProgram.Typing_right_weakening [lemma, in TermSubstitutionInTyping]
SetProgram.T_Call [constructor, in Typing]
SetProgram.T_fieldTerm_Cons [constructor, in Typing]
SetProgram.T_fieldTerm_Nil [constructor, in Typing]
SetProgram.T_New [constructor, in Typing]
SetProgram.T_Select [constructor, in Typing]
SetProgram.T_term_Cons [constructor, in Typing]
SetProgram.T_term_Nil [constructor, in Typing]
SetProgram.T_Var [constructor, in Typing]
SetProgram.Uniqueness_of_class_type_subtyping [lemma, in SubjectReduction_preliminaries]
SetProgram.Uniqueness_of_subtyping [lemma, in SubjectReduction_preliminaries]
SetProgram.Uniqueness_of_well_kindedness [lemma, in Progress_proofs]
SetProgram.Var_eqdec [lemma, in Substitutions]
SetProgram.Var_expansion_preserves_well_kindedness [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Var_expansion_preserves_well_kindedness_aux [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_param_satisfaction [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_satisfaction [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_satisfaction_by_the_right [lemma, in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_subtyping [lemma, in Subtyping_proofs]
SetProgram.Weakening_of_type_declaration [lemma, in Typing_proofs]
SetProgram.Weakening_of_type_declaration_by_the_left [lemma, in Typing_proofs]
SetProgram.Weakening_of_type_declaration_by_the_right [lemma, in Typing_proofs]
SetProgram.Weakening_of_well_kindedness [lemma, in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_left [lemma, in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_right [lemma, in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_right_aux [lemma, in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_right_snoc [lemma, in Typing_proofs]
SetProgram.wellKinded_implies_kind_of_exists [lemma, in Normalization_proofs]
SetProgram.wellKinded_implies_trans_typeEnv_exists [lemma, in Normalization_proofs]
SetProgram.Well_formed_field_value [lemma, in SubjectReduction_proofs]
SetProgram.Well_kindedness_does_not_depend_on_bounds [lemma, in Typing_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_env_reduction [lemma, in Subtyping_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_env_reduction_star [lemma, in Subtyping_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_reduction [lemma, in Subtyping_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_reduction_star [lemma, in Subtyping_proofs]
SetProgram.Well_kindedness_of_tuple [lemma, in Subtyping_proofs]
SetProgram.WK_apply [constructor, in Typing]
SetProgram.WK_class [constructor, in Typing]
SetProgram.WK_constr_cons [constructor, in Typing]
SetProgram.WK_constr_nil [constructor, in Typing]
SetProgram.WK_fun [constructor, in Typing]
SetProgram.WK_none [constructor, in Typing]
SetProgram.WK_param [constructor, in Typing]
SetProgram.WK_param_cons [constructor, in Typing]
SetProgram.WK_param_nil [constructor, in Typing]
SetProgram.WK_proj [constructor, in Typing]
SetProgram.WK_section [constructor, in Typing]
SetProgram.WK_some [constructor, in Typing]
SetProgram.WK_tuple [constructor, in Typing]
SetProgram.WK_typeEnv_nil [constructor, in Normalization_proofs]
SetProgram.WK_typeEnv_snoc [constructor, in Normalization_proofs]
SetProgram.WK_var [constructor, in Typing]
SetProgram.WT_proj [lemma, in Normalization_proofs]
SimplyTypedLambdaCalculus [library]
SimplyTypedLambdaCalculus_normalization [library]
snoc [definition, in Util]
SnocInd [section, in Util]
SnocInd.A [variable, in Util]
SnocInd.H_nil [variable, in Util]
SnocInd.H_snoc [variable, in Util]
SnocInd.P [variable, in Util]
snoc_ind [lemma, in Util]
snoc_ind_aux_1 [lemma, in Util]
snoc_ind_aux_2 [lemma, in Util]
snoc_ind_aux_3 [lemma, in Util]
snoc_ind_aux_4 [lemma, in Util]
snoc_ind_aux_5 [lemma, in Util]
snoc_ind_aux_6 [lemma, in Util]
snoc_inject [lemma, in Util]
snoc_nil [lemma, in Util]
snoc_of_append [lemma, in Util]
snoc_of_cons [lemma, in Util]
snoc_then_append [lemma, in Util]
SubjectReduction_preliminaries [library]
SubjectReduction_proofs [library]
subrel [definition, in Util]
Substitutions [library]
Substitutions_proofs [library]
Subtyping_proofs [library]
symRel [definition, in Util]
symRel_of_Rplus [lemma, in Util]
Syntax [library]
T
tc_step [constructor, in Util]tc_step1 [constructor, in Util]
tc_trans [constructor, in Util]
tc_trans1 [constructor, in Util]
TermSubstitutionInTyping [library]
transitive_closure_well_founded [lemma, in Util]
TransitivityElimination_proofs [library]
TypeSafety [library]
TypeSubstitutionInTyping [library]
Typing [library]
Typing_proofs [library]
U
Util [library]W
WellFormedness [library]WellFoundation [library]
well_foundation1 [lemma, in WellFoundation]
well_foundation2 [lemma, in WellFoundation]
well_foundation3 [lemma, in WellFoundation]
well_foundation4 [lemma, in WellFoundation]
Lemma Index
A
Accessibility_is_preserved_by_inclusion [in Util]app_inject [in Util]
app_length_right [in Util]
B
by_omega1 [in Util]C
cons_destruct [in Util]correct_witness [in Util]
D
Declaration_of_variable_1 [in Util]Declaration_of_variable_2 [in Util]
E
empty_is_empty_1 [in Util]empty_is_empty_2 [in Util]
empty_union_left [in Util]
empty_union_right [in Util]
F
Forall2_and_ListAt [in Util]Forall2_and_ListFrom [in Util]
Forall2_conj [in Util]
Forall2_implies [in Util]
Forall2_implies_same_length [in Util]
Forall2_of_map [in Util]
Forall2_of_map_cor1 [in Util]
Forall2_of_map_cor2 [in Util]
Forall2_refl [in Util]
Forall2_snoc [in Util]
Forall2_trans [in Util]
forall_implies_forall [in WellFoundation]
L
LambdaCalculusNormalization.Constants_are_reductible [in SimplyTypedLambdaCalculus_normalization]LambdaCalculusNormalization.First_projections_are_reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Lambda_redices_are_reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.lift_in_term_by_zero [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.lift_in_var_by_zero [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Permuting_lifting_and_polySubstitution [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PolySubstitution_preserves_typing [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PolySubstitution_preserves_typing_cor1 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_by_snoc [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_app [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_const [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_fst [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_fun [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_snd [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_var1 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_in_var_variant [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.polySubst_of_var_invariant [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_not_a_function [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_not_a_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_appFun.PreRed_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_not_a_function [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_not_a_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_not_a_function [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_not_a_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_not_a_function [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_not_a_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_not_a_function [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_not_a_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_Reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN_aux1 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN_aux2 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_SN_aux3 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_not_a_function [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_not_a_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.PreRed_implies_Reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible2 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible3 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible3_cor [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible4 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible5 [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_base [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_fun [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_prod [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible_subject_reduction_star [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Second_projections_are_reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_fun_intro [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_pair_intro [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_subst_inversion [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.SN_var_intro [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Variables_are_reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.WellTyped_implies_Reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.WellTyped_implies_Reductible_aux [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.WellTyped_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculus.Permuting_type_liftings_aux [in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_lifting_and_substitution [in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_lifting_and_substitution_aux [in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_lifting_and_substitution_2_aux [in SimplyTypedLambdaCalculus]
LambdaCalculus.Permuting_type_substitutions [in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_and_substitution_star [in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_in_lifting [in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_in_substitution [in SimplyTypedLambdaCalculus]
LambdaCalculus.Reduction_in_substitution_star [in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_app_left [in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_app_right [in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_fst_cong [in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_fun [in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_pair_left [in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_pair_right [in SimplyTypedLambdaCalculus]
LambdaCalculus.RS_snd_cong [in SimplyTypedLambdaCalculus]
LambdaCalculus.Subject_reduction [in SimplyTypedLambdaCalculus]
LambdaCalculus.Subject_reduction_star [in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_in_reduction [in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_in_reduction_star [in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_preserves_typing [in SimplyTypedLambdaCalculus]
LambdaCalculus.Substitution_preserves_typing_snoc [in SimplyTypedLambdaCalculus]
LambdaCalculus.Successive_type_liftings_aux [in SimplyTypedLambdaCalculus]
LambdaCalculus.Successive_variable_liftings [in SimplyTypedLambdaCalculus]
LambdaCalculus.Type_lifting_stronger_than_substitution [in SimplyTypedLambdaCalculus]
LambdaCalculus.Type_lifting_stronger_than_substitution_aux [in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_declaration_by_the_right [in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_well_typing_by_the_left [in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_well_typing_by_the_right [in SimplyTypedLambdaCalculus]
LambdaCalculus.Weakening_of_well_typing_by_the_right_aux [in SimplyTypedLambdaCalculus]
length_of_append [in Util]
length_of_map [in Util]
length_of_snoc [in Util]
lexicographic_extension_preserves_well_foundedness [in WellFoundation]
ListAt_implies_ListFrom [in Util]
ListFrom_implies_ListAt [in Util]
List_at_of_map [in Util]
List_at_right_weakening [in Util]
List_at_snoc_tail [in Util]
List_forall3 [in WellFoundation]
List_forall_and_List_at [in Util]
List_forall_and_List_from [in Util]
List_forall_equal_maps [in Util]
List_forall_equal_maps_cor1 [in Util]
List_forall_implies_forall [in Util]
List_forall_implies_Forall2 [in Util]
List_forall_implies_Forall2_right [in Util]
List_forall_implies_map_id [in Util]
List_forall_of_append_cor1 [in Util]
List_forall_of_append_elim [in Util]
List_forall_of_append_intro [in Util]
List_forall_of_map [in Util]
List_from_domain [in Util]
List_from_inversion_on_length [in Util]
List_from_is_a_partial_function [in Util]
List_from_lem1 [in Util]
List_from_lem1_cor1 [in Util]
List_from_lem2 [in Util]
List_from_lem3 [in Util]
List_from_lem4 [in Util]
List_from_lem6 [in Util]
List_from_of_map [in Util]
M
map_elim [in Util]map_id_is_id [in Util]
map_intro [in Util]
map_of_append [in Util]
Match2 [in MatchCompNat]
Match2_diff [in MatchCompNat]
Match3 [in MatchCompNat]
Match3_diff [in MatchCompNat]
match_comp_nat2_aux_0 [in MatchCompNat]
match_comp_nat2_aux_1 [in MatchCompNat]
match_comp_nat2_aux_2 [in MatchCompNat]
match_comp_nat2_ge [in MatchCompNat]
match_comp_nat2_lt [in MatchCompNat]
match_comp_nat3_aux_1 [in MatchCompNat]
match_comp_nat3_aux_2 [in MatchCompNat]
match_comp_nat3_aux_3 [in MatchCompNat]
match_comp_nat3_eq [in MatchCompNat]
match_comp_nat3_gt [in MatchCompNat]
match_comp_nat3_lt [in MatchCompNat]
myarith_1 [in Util]
myarith_2 [in Util]
P
plus_minus_assoc [in Util]R
Rplus1_implies_Rplus [in Util]Rplus1_is_transitive [in Util]
Rplus1_of_symRel [in Util]
Rplus_implies_Rplus1 [in Util]
Rplus_is_transitive [in Util]
Rplus_of_symRel [in Util]
RTriple1 [in WellFoundation]
RTriple2 [in WellFoundation]
RTriple3 [in WellFoundation]
S
sequence_extension_preserves_accessibility [in WellFoundation]sequence_extension_preserves_accessibility_aux [in WellFoundation]
sequence_extension_preserves_well_foundedness [in WellFoundation]
SetProgram.Accessibility_is_anti_reflexive [in SubjectReduction_preliminaries]
SetProgram.BetaType_implies_subtyping_lem1 [in SubjectReduction_preliminaries]
SetProgram.by_omega1 [in Typing_proofs]
SetProgram.ChurchRosser [in SubjectReduction_preliminaries]
SetProgram.classTypeParams_closed [in SubjectReduction_preliminaries]
SetProgram.classtype_expansion_preserves_well_kindedness_1 [in TransitivityElimination_proofs]
SetProgram.Class_inheritance_is_anti_reflexive [in SubjectReduction_preliminaries]
SetProgram.Class_kind_existence [in Normalization_proofs]
SetProgram.Class_subtyping_aux1 [in SubjectReduction_preliminaries]
SetProgram.Class_subtyping_implies_subtyping [in SubjectReduction_proofs]
SetProgram.Class_subtyping_subject_reduction [in SubjectReduction_preliminaries]
SetProgram.Class_type_expansion_preserves_well_kindedness [in TransitivityElimination_proofs]
SetProgram.Class_type_subtyping_injection [in SubjectReduction_preliminaries]
SetProgram.Class_type_subtyping_injection_aux1 [in SubjectReduction_preliminaries]
SetProgram.Class_type_subtyping_is_linear [in SubjectReduction_preliminaries]
SetProgram.Declaration_of_type_variable_is_preserved_by_reduction [in Subtyping_proofs]
SetProgram.Declaration_of_type_variable_1 [in Typing_proofs]
SetProgram.Declaration_of_type_variable_1_bis [in Typing_proofs]
SetProgram.Declaration_of_type_variable_2 [in Typing_proofs]
SetProgram.Declaration_of_type_variable_3 [in Typing_proofs]
SetProgram.decl_of_typeVar_and_kind_of [in Typing_proofs]
SetProgram.decl_of_typeVar_and_kind_of_cor1 [in Typing_proofs]
SetProgram.decl_of_typeVar_is_a_partial_function [in Typing_proofs]
SetProgram.Dropping_preserves_kind_of [in Typing_proofs]
SetProgram.Equality_preserves_diamond_property [in Confluence]
SetProgram.evaluated_term_dec [in Progress_proofs]
SetProgram.evaluated_term_new_inversion [in Progress_proofs]
SetProgram.Forall2_app [in Typing_proofs]
SetProgram.KindS_at_and_size [in BoundCompliantSubstitutions_proofs]
SetProgram.KindS_at_is_a_partial_function [in Progress_proofs]
SetProgram.kind_equality_implies_param_satisfaction [in BoundCompliantSubstitutions_proofs]
SetProgram.kind_equality_implies_poly_satisfaction [in BoundCompliantSubstitutions_proofs]
SetProgram.kind_of_is_a_partial_function [in Typing_proofs]
SetProgram.kind_of_params_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.kind_of_params_inversion_variant1 [in BoundCompliantSubstitutions_proofs]
SetProgram.length_of_typeLift [in Typing_proofs]
SetProgram.length_of_typeSubst [in Typing_proofs]
SetProgram.Lifting_in_closed_type_aux [in Subtyping_proofs]
SetProgram.Lifting_in_closed_type_cor1 [in Subtyping_proofs]
SetProgram.Lifting_in_closed_type_cor2 [in Subtyping_proofs]
SetProgram.Lifting_preserves_class_types [in Typing_proofs]
SetProgram.Lifting_preserves_kind_of [in Typing_proofs]
SetProgram.Lifting_preserves_kind_of_reverse [in Typing_proofs]
SetProgram.Lifting_preserves_removeBounds [in BoundCompliantSubstitutions_proofs]
SetProgram.Lifting_then_dropping [in Binders_proofs]
SetProgram.Lifting_then_dropping_in_typeVar [in Binders_proofs]
SetProgram.lift_in_typeVar_by_zero [in Binders_proofs]
SetProgram.lift_in_type_by_zero [in Binders_proofs]
SetProgram.lift_of_cons_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.lift_of_LTerm_proj [in Normalization_proofs]
SetProgram.lift_of_snoc [in Typing_proofs]
SetProgram.lift_of_snoc_aux [in Typing_proofs]
SetProgram.lift_of_some_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.List_from_implies_TypeSection_at [in Typing_proofs]
SetProgram.methodParams_closed [in SubjectReduction_preliminaries]
SetProgram.methodTypeParams_closed [in SubjectReduction_preliminaries]
SetProgram.methodType_closed [in SubjectReduction_preliminaries]
SetProgram.My_Constants.Type_of_is_a_partial_function [in Normalization_proofs]
SetProgram.Parallel_reduction_and_list_lookup [in Confluence]
SetProgram.Parallel_reduction_in_lifting [in Confluence]
SetProgram.Parallel_reduction_is_confluent [in Confluence]
SetProgram.Param_satisfaction_left_weakening [in Subtyping_proofs]
SetProgram.Permuting_type_liftings_aux [in Substitutions_proofs]
SetProgram.Permuting_type_liftings_cor1 [in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution [in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_aux [in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_cor1 [in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_2_aux [in Substitutions_proofs]
SetProgram.Permuting_type_lifting_and_substitution_2_cor1 [in Substitutions_proofs]
SetProgram.Permuting_type_substitutions [in Substitutions_proofs]
SetProgram.Permuting_type_substitutions_cor1 [in Substitutions_proofs]
SetProgram.Permuting_type_substitutions_cor2 [in Substitutions_proofs]
SetProgram.Permuting_type_substitutions_in_lists [in TypeSubstitutionInTyping]
SetProgram.Permuting_type_substitutions_in_lists_cor1 [in TypeSubstitutionInTyping]
SetProgram.Permuting_type_substitutions_in_lists_cor2 [in TypeSubstitutionInTyping]
SetProgram.polySubst_by_snoc [in TermSubstitutionInTyping]
SetProgram.Poly_term_substitution_preserves_typing [in TermSubstitutionInTyping]
SetProgram.Poly_term_substitution_preserves_typing_cor1 [in TermSubstitutionInTyping]
SetProgram.Poly_term_substitution_preserves_typing_cor2 [in TermSubstitutionInTyping]
SetProgram.Preservation_of_semantics [in Normalization_proofs]
SetProgram.Preservation_of_semantics_cor1 [in Normalization_proofs]
SetProgram.Preservation_of_typing [in Normalization_proofs]
SetProgram.Progress [in Progress_proofs]
SetProgram.Progress_aux_1 [in Progress_proofs]
SetProgram.RedTypeEnv_included_in_RedTypeEnv_snoc [in Subtyping_proofs]
SetProgram.RedTypeEnv_included_in_RedTypeEnv_snoc_aux1 [in Subtyping_proofs]
SetProgram.RedTypeEnv_included_in_RedTypeEnv_snoc_aux2 [in Subtyping_proofs]
SetProgram.RedTypeEnv_snoc_included_in_RedTypeEnv [in Subtyping_proofs]
SetProgram.RedTypeEnv_snoc_included_in_RedTypeEnv_aux1 [in Subtyping_proofs]
SetProgram.RedTypeEnv_snoc_included_in_RedTypeEnv_aux2 [in Subtyping_proofs]
SetProgram.RedTypeParTrans_has_diamond_property [in Confluence]
SetProgram.RedTypeParTrans_included_in_RedTypeStar [in Confluence]
SetProgram.RedTypeParTrans_in_lifting [in Subtyping_proofs]
SetProgram.RedTypePar_included_in_RedTypeStar [in Confluence]
SetProgram.RedTypeStar_implies_BetaType [in SubjectReduction_preliminaries]
SetProgram.RedTypeStar_included_in_RedTypeParTrans [in Confluence]
SetProgram.RedTypeStar_in_lifting [in Subtyping_proofs]
SetProgram.RedType_included_in_RedTypePar [in Confluence]
SetProgram.Reduction_and_substitution_par [in Confluence]
SetProgram.Reduction_and_substitution_star [in Auxiliary_proofs]
SetProgram.Reduction_in_lifting [in Auxiliary_proofs]
SetProgram.Reduction_in_substitution [in Auxiliary_proofs]
SetProgram.Reduction_in_substitution_star [in Auxiliary_proofs]
SetProgram.Reduction_of_class_types [in Subtyping_proofs]
SetProgram.Reduction_of_class_types_star [in Subtyping_proofs]
SetProgram.Reduction_of_variable_types [in Subtyping_proofs]
SetProgram.Reduction_of_variable_types_star [in Subtyping_proofs]
SetProgram.Reduction_preserves_class_types [in Subtyping_proofs]
SetProgram.Reduction_preserves_forall_satisfaction [in Subtyping_proofs]
SetProgram.Reduction_preserves_forall_satisfaction_build [in Subtyping_proofs]
SetProgram.Reduction_preserves_kind_of [in Subtyping_proofs]
SetProgram.Reduction_preserves_removeBounds [in Subtyping_proofs]
SetProgram.Reduction_preserves_satisfaction [in Subtyping_proofs]
SetProgram.Reduction_preserves_simultaneous_satisfaction [in Subtyping_proofs]
SetProgram.Reduction_preserves_subtyping [in Subtyping_proofs]
SetProgram.Reduction_preserves_subtypingWTR [in TransitivityElimination_proofs]
SetProgram.Reduction_preserves_TypeSection_at [in Subtyping_proofs]
SetProgram.Reduction_preserves_TypeS_at [in Subtyping_proofs]
SetProgram.Reduction_preserves_type_declaration_lookup [in Subtyping_proofs]
SetProgram.Reduction_preserves_type_of [in Normalization_proofs]
SetProgram.removeBounds_and_kind_of_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_invariant_by_lifting [in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_invariant_by_substitution [in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_is_idempotent [in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_of_params_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_preserves_kind_of [in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_preserves_well_kindedness [in BoundCompliantSubstitutions_proofs]
SetProgram.removeBounds_then_substitution [in BoundCompliantSubstitutions_proofs]
SetProgram.Rplus_app_left [in Normalization_proofs]
SetProgram.Rplus_app_right [in Normalization_proofs]
SetProgram.Rplus_fst_cong [in Normalization_proofs]
SetProgram.Rplus_fun [in Normalization_proofs]
SetProgram.Rplus_pair_left [in Normalization_proofs]
SetProgram.Rplus_pair_right [in Normalization_proofs]
SetProgram.Rplus_proj_cong [in Normalization_proofs]
SetProgram.Rplus_snd_cong [in Normalization_proofs]
SetProgram.RTE_head_star [in SubjectReduction_proofs]
SetProgram.RTE_tail_star [in SubjectReduction_proofs]
SetProgram.RTP_refl [in Confluence]
SetProgram.RTS_apply_left [in Auxiliary_proofs]
SetProgram.RTS_apply_right [in Auxiliary_proofs]
SetProgram.RTS_class_type [in SubjectReduction_proofs]
SetProgram.RTS_cons_head [in Auxiliary_proofs]
SetProgram.RTS_cons_inversion [in Subtyping_proofs]
SetProgram.RTS_cons_inversion_right [in Subtyping_proofs]
SetProgram.RTS_cons_tail [in Auxiliary_proofs]
SetProgram.RTS_fun_left [in Auxiliary_proofs]
SetProgram.RTS_fun_right [in Auxiliary_proofs]
SetProgram.RTS_nil_inversion [in Subtyping_proofs]
SetProgram.RTS_param_inversion [in Subtyping_proofs]
SetProgram.RTS_param_left [in Auxiliary_proofs]
SetProgram.RTS_param_right [in Auxiliary_proofs]
SetProgram.RTS_proj_sub [in Auxiliary_proofs]
SetProgram.RTS_section [in Auxiliary_proofs]
SetProgram.RTS_section_inversion [in Subtyping_proofs]
SetProgram.RTS_snoc_left [in Subtyping_proofs]
SetProgram.RTS_snoc_right [in Subtyping_proofs]
SetProgram.RTS_some [in Auxiliary_proofs]
SetProgram.RTS_some_inversion [in Subtyping_proofs]
SetProgram.RTS_some_inversion_right [in Subtyping_proofs]
SetProgram.RTS_tuple [in Auxiliary_proofs]
SetProgram.RT_snoc_left [in Subtyping_proofs]
SetProgram.RT_snoc_right [in Subtyping_proofs]
SetProgram.R_proj_cong [in Normalization_proofs]
SetProgram.R_proj_redex [in Normalization_proofs]
SetProgram.Satisfaction_implies_same_kind [in Progress_proofs]
SetProgram.Satisfaction_left_weakening [in Subtyping_proofs]
SetProgram.Self_type_is_well_kinded [in SubjectReduction_proofs]
SetProgram.StarReduction_preserves_kind_of [in Subtyping_proofs]
SetProgram.StarReduction_preserves_removeBounds [in Subtyping_proofs]
SetProgram.StarReduction_preserves_TypeS_at [in Subtyping_proofs]
SetProgram.StarReduction_preserves_type_declaration_lookup [in Subtyping_proofs]
SetProgram.Subclass_implies_class_expansion [in Auxiliary_proofs]
SetProgram.SubInfo_refl [in TermSubstitutionInTyping]
SetProgram.SubInfo_trans [in TermSubstitutionInTyping]
SetProgram.SubInfo_trans_cor1 [in TermSubstitutionInTyping]
SetProgram.Subject_reduction [in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux1 [in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux2 [in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux3 [in SubjectReduction_proofs]
SetProgram.Subject_reduction_case_T_call_redex_aux4 [in SubjectReduction_proofs]
SetProgram.Subject_reduction_star [in TypeSafety]
SetProgram.Subject_reduction_star_cor1 [in TypeSafety]
SetProgram.Substitution_in_closed_type_aux [in BoundCompliantSubstitutions_proofs]
SetProgram.Substitution_in_field_type [in Progress_proofs]
SetProgram.Substitution_in_method_param_types [in Progress_proofs]
SetProgram.Substitution_in_method_param_types_2 [in Progress_proofs]
SetProgram.Substitution_in_method_type [in Progress_proofs]
SetProgram.Substitution_in_method_type_params [in Progress_proofs]
SetProgram.Substitution_in_method_type_2 [in Progress_proofs]
SetProgram.Substitution_in_reduction [in Auxiliary_proofs]
SetProgram.Substitution_in_reduction_star [in Auxiliary_proofs]
SetProgram.Substitution_in_well_kinded_type_env [in BoundCompliantSubstitutions_proofs]
SetProgram.Substitution_preserves_class_types [in Typing_proofs]
SetProgram.Substitution_preserves_kind_of [in Typing_proofs]
SetProgram.Substitution_preserves_removeBounds [in BoundCompliantSubstitutions_proofs]
SetProgram.Substitution_preserves_well_kindedness_snoc [in Typing_proofs]
SetProgram.SubtypingWTR_implies_class_type_subtyping [in SubjectReduction_preliminaries]
SetProgram.SubtypingWTR_is_consistent_with_subclassing [in TransitivityElimination_proofs]
SetProgram.Subtyping_is_consistent_with_subclassing [in TransitivityElimination_proofs]
SetProgram.Subtyping_left_weakening [in Subtyping_proofs]
SetProgram.Successive_type_liftings [in Binders_proofs]
SetProgram.Successive_type_liftings_aux [in Binders_proofs]
SetProgram.Successive_type_liftings_cor1 [in Binders_proofs]
SetProgram.Successive_variable_liftings [in Binders_proofs]
SetProgram.SWTR_beta_left_star [in TransitivityElimination_proofs]
SetProgram.SWTR_beta_right_star [in TransitivityElimination_proofs]
SetProgram.SWTR_Trans [in TransitivityElimination_proofs]
SetProgram.SWTR_Trans_aux [in TransitivityElimination_proofs]
SetProgram.S_beta_left_star [in Subtyping_proofs]
SetProgram.S_beta_right_star [in Subtyping_proofs]
SetProgram.Term_lifting_preserves_fields_of_fieldTermList [in TermSubstitutionInTyping]
SetProgram.Term_reduction_preserves_fields_of_fieldTermList [in SubjectReduction_proofs]
SetProgram.Term_substitution_preserves_fields_of_fieldTermList [in TermSubstitutionInTyping]
SetProgram.Term_substitution_preserves_typing [in TermSubstitutionInTyping]
SetProgram.Transitive_closure_preserves_diamond_property [in Confluence]
SetProgram.Transitive_closure_preserves_diamond_property_aux [in Confluence]
SetProgram.Transitive_closure_preserves_inclusion [in Confluence]
SetProgram.TransitivityElimination [in TransitivityElimination_proofs]
SetProgram.TransitivityElimination_aux [in TransitivityElimination_proofs]
SetProgram.trans_is_a_partial_function [in Normalization_proofs]
SetProgram.trans_of_lift [in Normalization_proofs]
SetProgram.trans_of_typeSubst [in Normalization_proofs]
SetProgram.trans_typeEnv_and_TypeSection_at [in Normalization_proofs]
SetProgram.Typed_term_list [in SubjectReduction_proofs]
SetProgram.TypeEnv_WK_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.TypeEnv_WK_inversion_cor1 [in BoundCompliantSubstitutions_proofs]
SetProgram.TypeEnv_WK_inversion_cor2 [in BoundCompliantSubstitutions_proofs]
SetProgram.TypeParamList_ind [in BoundCompliantSubstitutions_proofs]
SetProgram.TypeParamList_WK_inversion [in Subtyping_proofs]
SetProgram.TypeSection_at_and_kind_of [in Typing_proofs]
SetProgram.TypeSection_at_implies_List_from [in Typing_proofs]
SetProgram.TypeSection_at_is_a_partial_function [in Typing_proofs]
SetProgram.TypeSection_at_lem1 [in Typing_proofs]
SetProgram.TypeSection_at_lem1_cor1 [in Typing_proofs]
SetProgram.TypeSection_at_lem2 [in Typing_proofs]
SetProgram.TypeSection_at_lem3 [in Typing_proofs]
SetProgram.TypeSection_at_lem4 [in Typing_proofs]
SetProgram.TypeSection_at_lem5 [in Typing_proofs]
SetProgram.TypeSection_at_lem6 [in Typing_proofs]
SetProgram.TypeSection_at_lem7 [in Typing_proofs]
SetProgram.TypeSection_at_lem8 [in Typing_proofs]
SetProgram.TypeSection_at_lem9 [in Subtyping_proofs]
SetProgram.typeSubst_of_class_type [in BoundCompliantSubstitutions_proofs]
SetProgram.typeSubst_of_cons_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.typeSubst_of_LTerm_proj [in Normalization_proofs]
SetProgram.typeSubst_of_snoc [in Typing_proofs]
SetProgram.typeSubst_of_some_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.TypeS_at_is_a_partial_function [in Auxiliary_proofs]
SetProgram.TypeS_at_is_preserved_by_reduction [in Subtyping_proofs]
SetProgram.TypeS_at_of_lift [in Auxiliary_proofs]
SetProgram.TypeS_at_of_lift_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.TypeS_at_of_typeSubst [in Auxiliary_proofs]
SetProgram.TypeS_at_of_typeSubst_inversion [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_env_reduction_preserves_typing [in SubjectReduction_proofs]
SetProgram.Type_eqdec [in Auxiliary_proofs]
SetProgram.Type_expansion_is_well_founded [in TransitivityElimination_proofs]
SetProgram.Type_expansion_is_well_founded_aux1 [in TransitivityElimination_proofs]
SetProgram.Type_lifting_stronger_than_substitution [in Substitutions_proofs]
SetProgram.Type_lifting_stronger_than_substitution_aux [in Substitutions_proofs]
SetProgram.type_of_of_lift [in Normalization_proofs]
SetProgram.type_of_of_typeSubst [in Normalization_proofs]
SetProgram.Type_reduction_is_confluent [in Confluence]
SetProgram.Type_reduction_is_well_founded [in Normalization_proofs]
SetProgram.Type_safety [in TypeSafety]
SetProgram.Type_substitution_preserves_fields_of_fieldTermList [in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_param_satisfaction [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_satisfaction [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_satisfaction_snoc [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_aux1 [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_cor1 [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_cor2 [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_subtyping_snoc [in BoundCompliantSubstitutions_proofs]
SetProgram.Type_substitution_preserves_typing [in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor1 [in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor2 [in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor3 [in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor4 [in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_typing_cor5 [in TypeSubstitutionInTyping]
SetProgram.Type_substitution_preserves_well_kindedness [in Typing_proofs]
SetProgram.Type_substitution_preserves_well_kindedness_cor1 [in Typing_proofs]
SetProgram.Type_substitution_preserves_well_kindedness_cor2 [in Typing_proofs]
SetProgram.Typing_returns_well_kinded_types [in Progress_proofs]
SetProgram.Typing_returns_well_kinded_types_cor1 [in Progress_proofs]
SetProgram.Typing_right_weakening [in TermSubstitutionInTyping]
SetProgram.Uniqueness_of_class_type_subtyping [in SubjectReduction_preliminaries]
SetProgram.Uniqueness_of_subtyping [in SubjectReduction_preliminaries]
SetProgram.Uniqueness_of_well_kindedness [in Progress_proofs]
SetProgram.Var_eqdec [in Substitutions]
SetProgram.Var_expansion_preserves_well_kindedness [in BoundCompliantSubstitutions_proofs]
SetProgram.Var_expansion_preserves_well_kindedness_aux [in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_param_satisfaction [in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_satisfaction [in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_satisfaction_by_the_right [in BoundCompliantSubstitutions_proofs]
SetProgram.Weakening_of_subtyping [in Subtyping_proofs]
SetProgram.Weakening_of_type_declaration [in Typing_proofs]
SetProgram.Weakening_of_type_declaration_by_the_left [in Typing_proofs]
SetProgram.Weakening_of_type_declaration_by_the_right [in Typing_proofs]
SetProgram.Weakening_of_well_kindedness [in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_left [in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_right [in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_right_aux [in Typing_proofs]
SetProgram.Weakening_of_well_kindedness_by_the_right_snoc [in Typing_proofs]
SetProgram.wellKinded_implies_kind_of_exists [in Normalization_proofs]
SetProgram.wellKinded_implies_trans_typeEnv_exists [in Normalization_proofs]
SetProgram.Well_formed_field_value [in SubjectReduction_proofs]
SetProgram.Well_kindedness_does_not_depend_on_bounds [in Typing_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_env_reduction [in Subtyping_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_env_reduction_star [in Subtyping_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_reduction [in Subtyping_proofs]
SetProgram.Well_kindedness_is_preserved_by_type_reduction_star [in Subtyping_proofs]
SetProgram.Well_kindedness_of_tuple [in Subtyping_proofs]
SetProgram.WT_proj [in Normalization_proofs]
snoc_ind [in Util]
snoc_ind_aux_1 [in Util]
snoc_ind_aux_2 [in Util]
snoc_ind_aux_3 [in Util]
snoc_ind_aux_4 [in Util]
snoc_ind_aux_5 [in Util]
snoc_ind_aux_6 [in Util]
snoc_inject [in Util]
snoc_nil [in Util]
snoc_of_append [in Util]
snoc_of_cons [in Util]
snoc_then_append [in Util]
symRel_of_Rplus [in Util]
T
transitive_closure_well_founded [in Util]W
well_foundation1 [in WellFoundation]well_foundation2 [in WellFoundation]
well_foundation3 [in WellFoundation]
well_foundation4 [in WellFoundation]
Section Index
E
Exists_Section [in Util]F
Forall2_section [in Util]L
LexicographicExtension [in WellFoundation]List_forall_section [in WellFoundation]
R
Rplus_Section [in Util]S
SequenceExtension [in WellFoundation]SnocInd [in Util]
Constructor Index
F
Forall2_cons [in Util]Forall2_nil [in Util]
L
LambdaCalculusNormalization.PreRed_appFun_intro [in SimplyTypedLambdaCalculus_normalization]LambdaCalculusNormalization.PreRed_const_intro [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_fstProj_intro [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_sndProj_intro [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_var_intro [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_app [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_base [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_fst [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed_snd [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculus.LTerm_app [in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_const [in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_fst [in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_fun [in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_pair [in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_snd [in SimplyTypedLambdaCalculus]
LambdaCalculus.LTerm_var [in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm_refl [in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm_step [in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm_trans [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_app_left [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_app_redex [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_app_right [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_fst_cong [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_fst_redex [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_fun [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_pair_left [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_pair_right [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_snd_cong [in SimplyTypedLambdaCalculus]
LambdaCalculus.R_snd_redex [in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_app [in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_const [in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_fst [in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_fun [in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_pair [in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_snd [in SimplyTypedLambdaCalculus]
LambdaCalculus.WT_var [in SimplyTypedLambdaCalculus]
LambdaConstants.LType_base [in SimplyTypedLambdaCalculus]
LambdaConstants.LType_fun [in SimplyTypedLambdaCalculus]
LambdaConstants.LType_prod [in SimplyTypedLambdaCalculus]
List_at_head [in Util]
List_at_tail [in Util]
List_forall_cons [in WellFoundation]
List_forall_cons [in Util]
List_forall_nil [in WellFoundation]
List_forall_nil [in Util]
List_from_head [in Util]
List_from_tail [in Util]
P
Program.ConstrKind [in Syntax]Program.ConstrKindList [in Syntax]
Program.FieldTerm_cons [in Syntax]
Program.FieldTerm_nil [in Syntax]
Program.Kind_cons [in Syntax]
Program.Kind_constr [in Syntax]
Program.Kind_nil [in Syntax]
Program.Kind_tuple [in Syntax]
Program.Term_call [in Syntax]
Program.Term_cons [in Syntax]
Program.Term_new [in Syntax]
Program.Term_nil [in Syntax]
Program.Term_select [in Syntax]
Program.Term_var [in Syntax]
Program.TupleKind [in Syntax]
Program.TypeConstr [in Syntax]
Program.TypeConstrList [in Syntax]
Program.TypeOption [in Syntax]
Program.TypeParam [in Syntax]
Program.TypeParamList [in Syntax]
Program.TypeSection [in Syntax]
Program.TypeTuple [in Syntax]
Program.Type_ [in Syntax]
Program.Type_apply [in Syntax]
Program.Type_class [in Syntax]
Program.Type_cons [in Syntax]
Program.Type_fun [in Syntax]
Program.Type_nil [in Syntax]
Program.Type_none [in Syntax]
Program.Type_param [in Syntax]
Program.Type_proj [in Syntax]
Program.Type_section [in Syntax]
Program.Type_some [in Syntax]
Program.Type_tuple [in Syntax]
Program.Type_var [in Syntax]
Program.WD_cons [in Syntax]
Program.WD_constr [in Syntax]
Program.WD_nil [in Syntax]
Program.WD_tuple [in Syntax]
R
RList_head [in WellFoundation]RList_tail [in WellFoundation]
RPair_fst [in WellFoundation]
RPair_snd [in WellFoundation]
S
SetProgram.BetaType_refl [in SubjectReduction_preliminaries]SetProgram.BetaType_step [in SubjectReduction_preliminaries]
SetProgram.BetaType_sym [in SubjectReduction_preliminaries]
SetProgram.BetaType_trans [in SubjectReduction_preliminaries]
SetProgram.B_Class [in Auxiliary]
SetProgram.B_Red [in Auxiliary]
SetProgram.B_Var [in Auxiliary]
SetProgram.classInheritance_intro [in WellFormedness]
SetProgram.Class_WK_intro [in WellFormedness]
SetProgram.Conform_intro [in SubjectReduction_preliminaries]
SetProgram.CS_Extends [in Auxiliary]
SetProgram.CS_Refl [in Auxiliary]
SetProgram.decl_of_typeVar_intro [in Auxiliary]
SetProgram.evaluated_fieldTerm_cons [in Semantics]
SetProgram.evaluated_fieldTerm_nil [in Semantics]
SetProgram.evaluated_new [in Semantics]
SetProgram.evaluated_term_cons [in Semantics]
SetProgram.evaluated_term_nil [in Semantics]
SetProgram.Evaluate_end [in Semantics]
SetProgram.Evaluate_step [in Semantics]
SetProgram.FieldDecl_WF_intro [in WellFormedness]
SetProgram.FieldTermListI [in Typing]
SetProgram.fieldTerm_lookup_head [in Semantics]
SetProgram.fieldTerm_lookup_tail [in Semantics]
SetProgram.FieldVal_WF_intro [in SubjectReduction_proofs]
SetProgram.Forall_ParamSat_build_cons [in Typing]
SetProgram.Forall_ParamSat_build_nil [in Typing]
SetProgram.IsComplete_intro [in Typing]
SetProgram.Kind_at_head [in Auxiliary]
SetProgram.Kind_at_tail [in Auxiliary]
SetProgram.Kind_of_param [in Auxiliary]
SetProgram.Kind_of_paramList_cons [in Auxiliary]
SetProgram.Kind_of_paramList_nil [in Auxiliary]
SetProgram.Kind_of_section [in Auxiliary]
SetProgram.MethodDecl_WF_intro [in WellFormedness]
SetProgram.MethodImpl_WF_intro [in WellFormedness]
SetProgram.My_Constants.LConst_class [in Normalization_proofs]
SetProgram.My_Constants.LConst_nil [in Normalization_proofs]
SetProgram.My_Constants.LConst_none [in Normalization_proofs]
SetProgram.My_Constants.LType_base [in Normalization_proofs]
SetProgram.My_Constants.LType_fun [in Normalization_proofs]
SetProgram.My_Constants.LType_prod [in Normalization_proofs]
SetProgram.My_Constants.type_of_const_class [in Normalization_proofs]
SetProgram.My_Constants.type_of_const_nil [in Normalization_proofs]
SetProgram.My_Constants.type_of_const_none [in Normalization_proofs]
SetProgram.My_Constants.Type_of_intro [in Normalization_proofs]
SetProgram.ParamSat_intro [in Typing]
SetProgram.RedTypeEnv_refl [in Auxiliary_proofs]
SetProgram.RedTypeEnv_step [in Auxiliary_proofs]
SetProgram.RedTypeEnv_trans [in Auxiliary_proofs]
SetProgram.RedType_refl [in Auxiliary_proofs]
SetProgram.RedType_step [in Auxiliary_proofs]
SetProgram.RedType_trans [in Auxiliary_proofs]
SetProgram.removeBounds_param [in Typing]
SetProgram.removeBounds_param_cons [in Typing]
SetProgram.removeBounds_param_nil [in Typing]
SetProgram.removeBounds_section [in Typing]
SetProgram.RTE_head [in Auxiliary]
SetProgram.RTE_snoc_head [in Subtyping_proofs]
SetProgram.RTE_snoc_tail [in Subtyping_proofs]
SetProgram.RTE_tail [in Auxiliary]
SetProgram.RTP_apply_left_right [in Confluence]
SetProgram.RTP_apply_redex [in Confluence]
SetProgram.RTP_class [in Confluence]
SetProgram.RTP_cons_head_tail [in Confluence]
SetProgram.RTP_fun_left_right [in Confluence]
SetProgram.RTP_nil [in Confluence]
SetProgram.RTP_none [in Confluence]
SetProgram.RTP_param_left_right [in Confluence]
SetProgram.RTP_proj_redex [in Confluence]
SetProgram.RTP_proj_sub [in Confluence]
SetProgram.RTP_section [in Confluence]
SetProgram.RTP_some [in Confluence]
SetProgram.RTP_tuple [in Confluence]
SetProgram.RTP_var [in Confluence]
SetProgram.RT_apply_left [in Auxiliary]
SetProgram.RT_apply_redex [in Auxiliary]
SetProgram.RT_apply_right [in Auxiliary]
SetProgram.RT_cons_head [in Auxiliary]
SetProgram.RT_cons_tail [in Auxiliary]
SetProgram.RT_fun_left [in Auxiliary]
SetProgram.RT_fun_right [in Auxiliary]
SetProgram.RT_param_left [in Auxiliary]
SetProgram.RT_param_right [in Auxiliary]
SetProgram.RT_proj_redex [in Auxiliary]
SetProgram.RT_proj_sub [in Auxiliary]
SetProgram.RT_section [in Auxiliary]
SetProgram.RT_some [in Auxiliary]
SetProgram.RT_tuple [in Auxiliary]
SetProgram.R_call_left [in Semantics]
SetProgram.R_call_redex [in Semantics]
SetProgram.R_call_right [in Semantics]
SetProgram.R_cons_left [in Semantics]
SetProgram.R_cons_right [in Semantics]
SetProgram.R_fieldTerm_cons_left [in Semantics]
SetProgram.R_fieldTerm_cons_right [in Semantics]
SetProgram.R_new [in Semantics]
SetProgram.r_refl [in Subtyping_proofs]
SetProgram.R_select [in Semantics]
SetProgram.R_select_redex [in Semantics]
SetProgram.r_step [in Subtyping_proofs]
SetProgram.SameCategory_TypeConstr [in Progress_proofs]
SetProgram.SameCategory_TypeConstrList [in Progress_proofs]
SetProgram.SameCategory_TypeOption [in Progress_proofs]
SetProgram.SameCategory_TypeParam [in Progress_proofs]
SetProgram.SameCategory_TypeParamList [in Progress_proofs]
SetProgram.SameCategory_TypeSection [in Progress_proofs]
SetProgram.SameCategory_TypeTuple [in Progress_proofs]
SetProgram.SameCategory_Type_ [in Progress_proofs]
SetProgram.SC_Extends [in Auxiliary]
SetProgram.SC_Refl [in Auxiliary]
SetProgram.SectionSat_intro [in Typing]
SetProgram.SubInfo_fieldTermList [in TermSubstitutionInTyping]
SetProgram.SubInfo_term [in TermSubstitutionInTyping]
SetProgram.SubInfo_termList [in TermSubstitutionInTyping]
SetProgram.SWTR_Beta_Left [in TransitivityElimination_proofs]
SetProgram.SWTR_Beta_Right [in TransitivityElimination_proofs]
SetProgram.SWTR_Class [in TransitivityElimination_proofs]
SetProgram.SWTR_Refl [in TransitivityElimination_proofs]
SetProgram.SWTR_Var [in TransitivityElimination_proofs]
SetProgram.S_Beta_Left [in Typing]
SetProgram.S_Beta_Right [in Typing]
SetProgram.S_Class [in Typing]
SetProgram.S_Refl [in Typing]
SetProgram.S_Trans [in Typing]
SetProgram.S_Var [in Typing]
SetProgram.TermI [in Typing]
SetProgram.TermListI [in Typing]
SetProgram.TE_Beta [in TransitivityElimination_proofs]
SetProgram.TE_Class [in TransitivityElimination_proofs]
SetProgram.transcat_TypeConstr [in Normalization_proofs]
SetProgram.transcat_TypeConstrList [in Normalization_proofs]
SetProgram.transcat_TypeOption [in Normalization_proofs]
SetProgram.transcat_TypeParam [in Normalization_proofs]
SetProgram.transcat_TypeParamList [in Normalization_proofs]
SetProgram.transcat_TypeSection [in Normalization_proofs]
SetProgram.transcat_TypeTuple [in Normalization_proofs]
SetProgram.transcat_Type_ [in Normalization_proofs]
SetProgram.trans_apply [in Normalization_proofs]
SetProgram.trans_class [in Normalization_proofs]
SetProgram.trans_cons [in Normalization_proofs]
SetProgram.trans_fun [in Normalization_proofs]
SetProgram.trans_nil [in Normalization_proofs]
SetProgram.trans_none [in Normalization_proofs]
SetProgram.trans_param [in Normalization_proofs]
SetProgram.trans_proj [in Normalization_proofs]
SetProgram.trans_section [in Normalization_proofs]
SetProgram.trans_some [in Normalization_proofs]
SetProgram.trans_tuple [in Normalization_proofs]
SetProgram.trans_typeEnv_nil [in Normalization_proofs]
SetProgram.trans_typeEnv_snoc [in Normalization_proofs]
SetProgram.trans_var [in Normalization_proofs]
SetProgram.TypeSection_at_head [in Auxiliary]
SetProgram.TypeSection_at_tail [in Auxiliary]
SetProgram.TypeS_at_head [in Auxiliary]
SetProgram.TypeS_at_tail [in Auxiliary]
SetProgram.T_Call [in Typing]
SetProgram.T_fieldTerm_Cons [in Typing]
SetProgram.T_fieldTerm_Nil [in Typing]
SetProgram.T_New [in Typing]
SetProgram.T_Select [in Typing]
SetProgram.T_term_Cons [in Typing]
SetProgram.T_term_Nil [in Typing]
SetProgram.T_Var [in Typing]
SetProgram.WK_apply [in Typing]
SetProgram.WK_class [in Typing]
SetProgram.WK_constr_cons [in Typing]
SetProgram.WK_constr_nil [in Typing]
SetProgram.WK_fun [in Typing]
SetProgram.WK_none [in Typing]
SetProgram.WK_param [in Typing]
SetProgram.WK_param_cons [in Typing]
SetProgram.WK_param_nil [in Typing]
SetProgram.WK_proj [in Typing]
SetProgram.WK_section [in Typing]
SetProgram.WK_some [in Typing]
SetProgram.WK_tuple [in Typing]
SetProgram.WK_typeEnv_nil [in Normalization_proofs]
SetProgram.WK_typeEnv_snoc [in Normalization_proofs]
SetProgram.WK_var [in Typing]
T
tc_step [in Util]tc_step1 [in Util]
tc_trans [in Util]
tc_trans1 [in Util]
Inductive Index
F
Forall2 [in Util]L
LambdaCalculusNormalization.PreRed_appFun [in SimplyTypedLambdaCalculus_normalization]LambdaCalculusNormalization.PreRed_const [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_fstProj [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_sndProj [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreRed_var [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.ProveReductible.ClosRed [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculus.LTerm [in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTerm [in SimplyTypedLambdaCalculus]
LambdaCalculus.RedTermStar [in SimplyTypedLambdaCalculus]
LambdaCalculus.WellTyped [in SimplyTypedLambdaCalculus]
LambdaConstants.LType [in SimplyTypedLambdaCalculus]
List_at [in Util]
List_forall [in Util]
List_forall [in WellFoundation]
List_from [in Util]
P
Program.KindC [in Syntax]Program.KindS [in Syntax]
Program.Kind_WD [in Syntax]
Program.Term [in Syntax]
Program.TypeC [in Syntax]
Program.TypeS [in Syntax]
R
RList [in WellFoundation]RPair [in WellFoundation]
Rplus [in Util]
Rplus1 [in Util]
S
SetProgram.BetaType [in SubjectReduction_preliminaries]SetProgram.Bound [in Auxiliary]
SetProgram.classInheritance [in WellFormedness]
SetProgram.Class_subtyping [in Auxiliary]
SetProgram.Class_WK [in WellFormedness]
SetProgram.clos_refl [in Subtyping_proofs]
SetProgram.Conform [in SubjectReduction_preliminaries]
SetProgram.decl_of_typeVar [in Auxiliary]
SetProgram.Evaluate [in Semantics]
SetProgram.evaluated_term [in Semantics]
SetProgram.FieldDecl_WF [in WellFormedness]
SetProgram.fieldTerm_lookup [in Semantics]
SetProgram.FieldVal_WF [in SubjectReduction_proofs]
SetProgram.Forall_ParamSat_build [in Typing]
SetProgram.IsComplete [in Typing]
SetProgram.KindS_at [in Auxiliary]
SetProgram.kind_of [in Auxiliary]
SetProgram.MethodDecl_WF [in WellFormedness]
SetProgram.MethodImpl_WF [in WellFormedness]
SetProgram.My_Constants.LConst_definition [in Normalization_proofs]
SetProgram.My_Constants.LType [in Normalization_proofs]
SetProgram.My_Constants.type_of [in Normalization_proofs]
SetProgram.My_Constants.type_of_const_def [in Normalization_proofs]
SetProgram.ParamSat [in Typing]
SetProgram.RedTerm [in Semantics]
SetProgram.RedType [in Auxiliary]
SetProgram.RedTypeEnv [in Auxiliary]
SetProgram.RedTypeEnvStar [in Auxiliary_proofs]
SetProgram.RedTypeEnv_snoc [in Subtyping_proofs]
SetProgram.RedTypePar [in Confluence]
SetProgram.RedTypeStar [in Auxiliary_proofs]
SetProgram.removeBounds [in Typing]
SetProgram.SameCategory [in Progress_proofs]
SetProgram.SectionSat [in Typing]
SetProgram.Subclass [in Auxiliary]
SetProgram.SubInfo [in TermSubstitutionInTyping]
SetProgram.Subtyping [in Typing]
SetProgram.SubtypingWTR [in TransitivityElimination_proofs]
SetProgram.TermInfo [in Typing]
SetProgram.Term_WT [in Typing]
SetProgram.trans [in Normalization_proofs]
SetProgram.trans_category [in Normalization_proofs]
SetProgram.trans_typeEnv [in Normalization_proofs]
SetProgram.TypeEnv_WK [in Normalization_proofs]
SetProgram.TypeExp [in TransitivityElimination_proofs]
SetProgram.TypeSection_at [in Auxiliary]
SetProgram.TypeS_at [in Auxiliary]
SetProgram.Type_WK [in Typing]
Definition Index
F
fun_extension [in WellFoundation]G
get_witness [in Util]L
LambdaCalculusNormalization.polySubst_in_term [in SimplyTypedLambdaCalculus_normalization]LambdaCalculusNormalization.PreReductible_appFun.PreRed [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_const.PreRed [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_fstProj.PreRed [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_sndProj.PreRed [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible_var.PreRed [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.Reductible [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculus.LEnv [in SimplyTypedLambdaCalculus]
LambdaCalculus.lift_at_depth_in_term [in SimplyTypedLambdaCalculus]
LambdaCalculus.lift_at_depth_in_var [in SimplyTypedLambdaCalculus]
LambdaCalculus.lift_in_term [in SimplyTypedLambdaCalculus]
LambdaCalculus.subst_in_term [in SimplyTypedLambdaCalculus]
LambdaCalculus.subst_in_var [in SimplyTypedLambdaCalculus]
M
match_comp_nat2 [in MatchCompNat]match_comp_nat3 [in MatchCompNat]
N
natSet [in Util]natSet_add [in Util]
natSet_empty [in Util]
natSet_in [in Util]
natSet_union [in Util]
P
Program.Class_type [in Syntax]Program.Fun_type [in Syntax]
Program.is_classType [in Syntax]
Program.TermEnv [in Syntax]
Program.TypeEnv [in Syntax]
Program.TypeVar [in Syntax]
Program.Var [in Syntax]
Program.Var_type [in Syntax]
S
SetProgram.ClassSat [in WellFormedness]SetProgram.DiamondProperty [in Confluence]
SetProgram.DiamondProperty_aux [in Confluence]
SetProgram.drop_at_depth_in_type [in Binders]
SetProgram.drop_at_depth_in_typeEnv [in Binders]
SetProgram.drop_at_depth_in_typeVar [in Binders]
SetProgram.drop_in_type [in Binders]
SetProgram.drop_in_typeEnv [in Binders]
SetProgram.drop_in_typeVar [in Binders]
SetProgram.EvaluateMain [in Semantics]
SetProgram.fields_of_fieldTermList [in Typing]
SetProgram.Forall_ParamSat [in Typing]
SetProgram.fv_at_depth_in_type [in Binders]
SetProgram.fv_at_depth_in_typeVar [in Binders]
SetProgram.fv_in_type [in Binders]
SetProgram.Info_WK [in Progress_proofs]
SetProgram.IsComplete_fields [in Typing]
SetProgram.IsComplete_methods [in Typing]
SetProgram.is_arbitraryType [in Typing]
SetProgram.lift_at_depth_in_term [in Binders]
SetProgram.lift_at_depth_in_type [in Binders]
SetProgram.lift_at_depth_in_typeEnv [in Binders]
SetProgram.lift_at_depth_in_typeVar [in Binders]
SetProgram.lift_at_depth_in_var [in Binders]
SetProgram.lift_in_term [in Binders]
SetProgram.lift_in_type [in Binders]
SetProgram.lift_in_typeEnv [in Binders]
SetProgram.list_of_termList [in Semantics]
SetProgram.LTerm_proj [in Normalization_proofs]
SetProgram.My_Constants.LConst [in Normalization_proofs]
SetProgram.My_Constants.type_of_const [in Normalization_proofs]
SetProgram.My_Constants.type_of_kind [in Normalization_proofs]
SetProgram.Pointwise_subtyping [in Typing]
SetProgram.polyTermSubst_in_term [in Semantics]
SetProgram.RedTermStar [in TypeSafety]
SetProgram.RedTypeParTrans [in Confluence]
SetProgram.size [in Confluence]
SetProgram.size_of_kind [in BoundCompliantSubstitutions_proofs]
SetProgram.SubRelation [in Confluence]
SetProgram.TermEnv_WK [in TypeSubstitutionInTyping]
SetProgram.termSubst_in_term [in Substitutions]
SetProgram.termSubst_in_var [in Substitutions]
SetProgram.typeSubst_in_term [in Substitutions]
SetProgram.typeSubst_in_termEnv [in TypeSubstitutionInTyping]
SetProgram.typeSubst_in_termInfo [in TypeSubstitutionInTyping]
SetProgram.typeSubst_in_type [in Substitutions]
SetProgram.typeSubst_in_typeEnv [in Substitutions]
SetProgram.typeSubst_in_typeList [in Typing]
SetProgram.typeSubst_in_typeVar [in Substitutions]
snoc [in Util]
subrel [in Util]
symRel [in Util]
Module Index
L
LambdaCalculus [in SimplyTypedLambdaCalculus]LambdaCalculusNormalization [in SimplyTypedLambdaCalculus_normalization]
LambdaConstants [in SimplyTypedLambdaCalculus]
M
My_Auxiliary [in Typing]My_Auxiliary_proofs [in Confluence]
My_Binders [in Substitutions]
My_Binders_proofs [in Substitutions_proofs]
My_BoundCompliantSubstitutions_proofs [in TypeSubstitutionInTyping]
My_Confluence [in Typing_proofs]
My_Constants [in Normalization_proofs]
My_LambdaCalculus [in SimplyTypedLambdaCalculus_normalization]
My_LambdaCalculusNormalization [in Normalization_proofs]
My_Normalization_proofs [in TransitivityElimination_proofs]
My_Progress_proofs [in BoundCompliantSubstitutions_proofs]
My_Semantics [in Binders_proofs]
My_SubjectReduction_preliminaries [in SubjectReduction_proofs]
My_SubjectReduction_proofs [in TypeSafety]
My_Substitutions [in Auxiliary]
My_Substitutions_proofs [in Auxiliary_proofs]
My_Subtyping_proofs [in Normalization_proofs]
My_TermSubstitutionInTyping [in SubjectReduction_preliminaries]
My_TransitivityElimination_proofs [in Progress_proofs]
My_TypeSubstitutionInTyping [in TermSubstitutionInTyping]
My_Typing [in WellFormedness]
My_Typing_proofs [in Subtyping_proofs]
My_WellFormedness [in Semantics]
P
PreReductible [in SimplyTypedLambdaCalculus_normalization]PreReductible_appFun [in SimplyTypedLambdaCalculus_normalization]
PreReductible_const [in SimplyTypedLambdaCalculus_normalization]
PreReductible_fstProj [in SimplyTypedLambdaCalculus_normalization]
PreReductible_sndProj [in SimplyTypedLambdaCalculus_normalization]
PreReductible_var [in SimplyTypedLambdaCalculus_normalization]
Program [in Syntax]
ProveReductible [in SimplyTypedLambdaCalculus_normalization]
ProveReductible_appFun [in SimplyTypedLambdaCalculus_normalization]
ProveReductible_const [in SimplyTypedLambdaCalculus_normalization]
ProveReductible_fstProj [in SimplyTypedLambdaCalculus_normalization]
ProveReductible_sndProj [in SimplyTypedLambdaCalculus_normalization]
ProveReductible_var [in SimplyTypedLambdaCalculus_normalization]
S
SetProgram [in Auxiliary_proofs]SetProgram [in Progress_proofs]
SetProgram [in WellFormedness]
SetProgram [in TermSubstitutionInTyping]
SetProgram [in Semantics]
SetProgram [in Binders]
SetProgram [in Typing]
SetProgram [in TypeSafety]
SetProgram [in Confluence]
SetProgram [in SubjectReduction_proofs]
SetProgram [in BoundCompliantSubstitutions_proofs]
SetProgram [in Subtyping_proofs]
SetProgram [in Substitutions]
SetProgram [in Normalization_proofs]
SetProgram [in Binders_proofs]
SetProgram [in TransitivityElimination_proofs]
SetProgram [in Auxiliary]
SetProgram [in Typing_proofs]
SetProgram [in Substitutions_proofs]
SetProgram [in SubjectReduction_preliminaries]
SetProgram [in TypeSubstitutionInTyping]
Axiom Index
L
LambdaCalculusNormalization.PreReductible.PreRed [in SimplyTypedLambdaCalculus_normalization]LambdaCalculusNormalization.PreReductible.PreRed_implies_SN [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_implies_WellTyped [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_left_weakening [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_not_a_function [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_not_a_pair [in SimplyTypedLambdaCalculus_normalization]
LambdaCalculusNormalization.PreReductible.PreRed_subject_reduction [in SimplyTypedLambdaCalculus_normalization]
LambdaConstants.LConst [in SimplyTypedLambdaCalculus]
LambdaConstants.type_of_const [in SimplyTypedLambdaCalculus]
P
Program.classSuper [in Syntax]Program.ClassSym [in Syntax]
Program.ClassSym_eqdec [in Syntax]
Program.classTypeParams [in Syntax]
Program.fieldOwner [in Syntax]
Program.FieldSym [in Syntax]
Program.FieldSym_eqdec [in Syntax]
Program.fieldType [in Syntax]
Program.mainTerm [in Syntax]
Program.methodImpl [in Syntax]
Program.methodOwner [in Syntax]
Program.methodParams [in Syntax]
Program.MethodSym [in Syntax]
Program.MethodSym_eqdec [in Syntax]
Program.methodType [in Syntax]
Program.methodTypeParams [in Syntax]
S
SetProgram.classes_are_well_kinded [in WellFormedness]SetProgram.Class_inheritance_is_well_founded [in WellFormedness]
SetProgram.field_declarations_are_well_formed [in WellFormedness]
SetProgram.main_term_is_well_typed [in WellFormedness]
SetProgram.method_declarations_are_well_formed [in WellFormedness]
SetProgram.method_implementations_are_well_formed [in WellFormedness]
Variable Index
E
Exists_Section.A [in Util]Exists_Section.B [in Util]
Exists_Section.existence [in Util]
Exists_Section.P [in Util]
F
Forall2_section.A [in Util]Forall2_section.B [in Util]
L
LexicographicExtension.A1 [in WellFoundation]LexicographicExtension.A2 [in WellFoundation]
LexicographicExtension.R1 [in WellFoundation]
LexicographicExtension.R2 [in WellFoundation]
List_forall_section.A [in WellFoundation]
R
Rplus_Section.A [in Util]Rplus_Section.R [in Util]
S
SequenceExtension.A [in WellFoundation]SequenceExtension.R [in WellFoundation]
SnocInd.A [in Util]
SnocInd.H_nil [in Util]
SnocInd.H_snoc [in Util]
SnocInd.P [in Util]
Library Index
A
AuxiliaryAuxiliary_proofs
B
BindersBinders_proofs
BoundCompliantSubstitutions_proofs
C
ConfluenceM
MatchCompNatN
Normalization_proofsP
Progress_proofsS
SemanticsSimplyTypedLambdaCalculus
SimplyTypedLambdaCalculus_normalization
SubjectReduction_preliminaries
SubjectReduction_proofs
Substitutions
Substitutions_proofs
Subtyping_proofs
Syntax
T
TermSubstitutionInTypingTransitivityElimination_proofs
TypeSafety
TypeSubstitutionInTyping
Typing
Typing_proofs
U
UtilW
WellFormednessWellFoundation
| 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 | _ | (1109 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 | _ | (533 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 | _ | (7 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 | _ | (276 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 | _ | (74 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 | _ | (82 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 | _ | (60 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 | _ | (31 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 | _ | (19 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 | _ | (27 entries) |
This page has been generated by coqdoc