| 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 | _ | (1755 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 | _ | (1070 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 | _ | (6 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 | _ | (426 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 | _ | (81 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 | _ | (73 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 | _ | (3 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 | _ | (96 entries) |
T
Tactics [library]TCs [constructor, in Lambda.ListType]
term [inductive, in Lambda.Terms]
Terms [library]
Terms [library]
term_free_db [lemma, in Lambda.JRussell.Freevars]
term_type_range_kinded [lemma, in Lambda.JRussell.GenerationRange]
term_type_range_kinded [lemma, in Lambda.Russell.GenerationRange]
term_type_range_not_kind [lemma, in Lambda.JRussell.GenerationRange]
term_type_range_not_kind [lemma, in Lambda.Russell.GenerationRange]
Tfaf_cs [constructor, in Lambda.ListType]
Tfaf_nil [constructor, in Lambda.ListType]
Tfa2_cs [constructor, in Lambda.ListType]
Tfa2_nil [constructor, in Lambda.ListType]
Tfa_cs [constructor, in Lambda.ListType]
Tfa_nil [constructor, in Lambda.ListType]
Tfor_all [inductive, in Lambda.ListType]
Tfor_all2 [inductive, in Lambda.ListType]
Tfor_all_fold [inductive, in Lambda.ListType]
thinning [lemma, in Lambda.CCSum.Thinning]
thinning [lemma, in Lambda.TPOSR.Thinning]
thinning [lemma, in Lambda.Russell.Thinning]
Thinning [library]
Thinning [library]
Thinning [library]
Thinning [library]
thinning_coerce [lemma, in Lambda.TPOSR.Thinning]
thinning_coerce [lemma, in Lambda.Russell.Thinning]
thinning_eq [lemma, in Lambda.TPOSR.Thinning]
thinning_n [lemma, in Lambda.JRussell.Thinning]
thinning_n [lemma, in Lambda.Russell.Thinning]
thinning_n [lemma, in Lambda.CCSum.Thinning]
thinning_n [lemma, in Lambda.TPOSR.Thinning]
thinning_n_coerce [lemma, in Lambda.JRussell.Thinning]
thinning_n_coerce [lemma, in Lambda.Russell.Thinning]
thinning_n_coerce [lemma, in Lambda.TPOSR.Thinning]
thinning_n_eq [lemma, in Lambda.TPOSR.Thinning]
TIns [inductive, in Lambda.ListType]
Tins_eq [lemma, in Lambda.ListType]
Tins_gt [lemma, in Lambda.ListType]
TIns_hd [constructor, in Lambda.ListType]
Tins_le [lemma, in Lambda.ListType]
TIns_tl [constructor, in Lambda.ListType]
TList [inductive, in Lambda.ListType]
TListes [section, in Lambda.ListType]
TListes.A [variable, in Lambda.ListType]
TList_iter [definition, in Lambda.ListType]
Tmap [definition, in Lambda.ListType]
TNl [constructor, in Lambda.ListType]
Tnth_def [definition, in Lambda.ListType]
tod [definition, in Lambda.TPOSR.TypesDepth]
toq [lemma, in Lambda.TPOSR.UniquenessOfTypes]
tposr [inductive, in Lambda.TPOSR.Types]
tposrd [inductive, in Lambda.TPOSR.TypesDepth]
tposrd_abs [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_app [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_beta [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_conv [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_pair [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_pi1 [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_pi1_red [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_pi2 [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_pi2_red [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_prod [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_prop [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_set [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_subset [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_sum [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_tposr [lemma, in Lambda.TPOSR.TypesDepth]
tposrd_tposr_coerce [lemma, in Lambda.TPOSR.ChurchRosserDepth]
tposrd_tposr_term_depth [lemma, in Lambda.TPOSR.TypesDepth]
tposrd_tposr_type [lemma, in Lambda.TPOSR.TypesDepth]
tposrd_tposr_wf [lemma, in Lambda.TPOSR.TypesDepth]
tposrd_unique_sort [lemma, in Lambda.TPOSR.Equiv]
tposrd_var [constructor, in Lambda.TPOSR.TypesDepth]
tposrd_wf [inductive, in Lambda.TPOSR.TypesDepth]
tposrp [inductive, in Lambda.TPOSR.Types]
tposrp_abs [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_abs_aux [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_abs_aux2 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_app [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_app_aux [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_app_aux2 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_app_aux3 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_coerce_env [lemma, in Lambda.TPOSR.CtxCoercion]
tposrp_conv [lemma, in Lambda.TPOSR.Basic]
tposrp_conv_env [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_conv_env_full [lemma, in Lambda.TPOSR.UnlabConv]
tposrp_conv_l [lemma, in Lambda.TPOSR.Basic]
tposrp_conv_r [lemma, in Lambda.TPOSR.Basic]
tposrp_cr [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_equiv_l [lemma, in Lambda.TPOSR.Equiv]
tposrp_n [inductive, in Lambda.TPOSR.ChurchRosser]
tposrp_n_cr [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_n_tposr [constructor, in Lambda.TPOSR.ChurchRosser]
tposrp_n_tposrp [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_n_trans [constructor, in Lambda.TPOSR.ChurchRosser]
tposrp_n_transitive [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_pair [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux1 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux2 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux3 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux4 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pi [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_pi1 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pi1_aux [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pi2 [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pi2_aux [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_pi_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_pre_coerce_env_full [lemma, in Lambda.TPOSR.PreCtxCoercion]
tposrp_prod [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_prod_aux [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_prod_prod [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_prod_prod_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_refl_l [lemma, in Lambda.TPOSR.LeftReflexivity]
tposrp_refl_r [lemma, in Lambda.TPOSR.RightReflexivity]
tposrp_sigma [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_sigma_aux [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_sort [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_sort_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_sort_eq [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_sort_eq_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_subset [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_subset [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_subset_aux [lemma, in Lambda.TPOSR.TPOSR_trans]
tposrp_subset_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_subset_subset [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_subset_subset_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_sum [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_sum_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_sum_sum [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_sum_sum_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_tposr [constructor, in Lambda.TPOSR.Types]
tposrp_tposrp_n [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_tposr_eq [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_tposr_eq [lemma, in Lambda.TPOSR.Basic]
tposrp_tposr_eq_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposrp_tposr_eq_aux [lemma, in Lambda.TPOSR.Basic]
tposrp_trans [constructor, in Lambda.TPOSR.Types]
tposrp_uniqueness_of_types [lemma, in Lambda.TPOSR.UniquenessOfTypes]
tposrp_unique_sort [lemma, in Lambda.TPOSR.UnicityOfSorting]
tposr_abs [constructor, in Lambda.TPOSR.Types]
tposr_app [constructor, in Lambda.TPOSR.Types]
tposr_beta [constructor, in Lambda.TPOSR.Types]
tposr_coerce [inductive, in Lambda.TPOSR.Types]
tposr_coerces_env [lemma, in Lambda.TPOSR.CoerceNoTrans]
tposr_coerce_conv [constructor, in Lambda.TPOSR.Types]
tposr_coerce_env [lemma, in Lambda.TPOSR.CtxCoercion]
tposr_coerce_equiv [definition, in Lambda.TPOSR.Equiv]
tposr_coerce_eq_sort [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_coerce_eq_sort_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_coerce_prod [constructor, in Lambda.TPOSR.Types]
tposr_coerce_russell [lemma, in Lambda.Meta.TPOSR_Russell]
tposr_coerce_sorts [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_coerce_sort_l [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_coerce_sort_r [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_coerce_sub_l [constructor, in Lambda.TPOSR.Types]
tposr_coerce_sub_r [constructor, in Lambda.TPOSR.Types]
tposr_coerce_sum [constructor, in Lambda.TPOSR.Types]
tposr_coerce_sym [constructor, in Lambda.TPOSR.Types]
tposr_coerce_trans [constructor, in Lambda.TPOSR.Types]
tposr_coerce_unique_sort [lemma, in Lambda.Meta.TPOSR_JRussell]
tposr_coerce_unique_sort_right [lemma, in Lambda.TPOSR.Equiv]
tposr_conv [constructor, in Lambda.TPOSR.Types]
tposr_conv_eq [lemma, in Lambda.TPOSR.Basic]
tposr_conv_l [lemma, in Lambda.TPOSR.Basic]
tposr_conv_r [lemma, in Lambda.TPOSR.Basic]
tposr_eq [inductive, in Lambda.TPOSR.Types]
tposr_equiv_l [lemma, in Lambda.TPOSR.Equiv]
tposr_equiv_r [lemma, in Lambda.TPOSR.Equiv]
tposr_eq_cr [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_equiv [definition, in Lambda.TPOSR.Equiv]
tposr_eq_prod_subset [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_prod_sum [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_russell [lemma, in Lambda.Meta.TPOSR_Russell]
tposr_eq_sort [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_prod [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_subset [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_sum [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_tposrp [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_tposrp_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_sum_subset [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_eq_sym [constructor, in Lambda.TPOSR.Types]
tposr_eq_tposr [constructor, in Lambda.TPOSR.Types]
tposr_eq_trans [constructor, in Lambda.TPOSR.Types]
tposr_eq_unique_sort [lemma, in Lambda.Meta.TPOSR_JRussell]
tposr_eq_unique_sort_right [lemma, in Lambda.TPOSR.Equiv]
tposr_exp_env [lemma, in Lambda.TPOSR.CtxExpansion]
TPOSR_JRussell [library]
tposr_not_kind [lemma, in Lambda.TPOSR.Basic]
tposr_not_kind_aux [lemma, in Lambda.TPOSR.Basic]
tposr_pair [constructor, in Lambda.TPOSR.Types]
tposr_pair_coerce_left [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_coerce_left_aux [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_coerce_right [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_coerce_right_aux [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_comp [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_comp_aux [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_left [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_left_aux [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_right [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_right_aux [lemma, in Lambda.TPOSR.RightReflexivity]
tposr_pi1 [constructor, in Lambda.TPOSR.Types]
tposr_pi1_red [constructor, in Lambda.TPOSR.Types]
tposr_pi2 [constructor, in Lambda.TPOSR.Types]
tposr_pi2_red [constructor, in Lambda.TPOSR.Types]
tposr_pre_coerce_env [lemma, in Lambda.TPOSR.PreCtxCoercion]
tposr_prod [constructor, in Lambda.TPOSR.Types]
tposr_prod_prod [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_prop [constructor, in Lambda.TPOSR.Types]
tposr_red_env [lemma, in Lambda.TPOSR.CtxReduction]
tposr_russell [lemma, in Lambda.Meta.TPOSR_Russell]
TPOSR_Russell [library]
tposr_set [constructor, in Lambda.TPOSR.Types]
tposr_sort [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_sort_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_sort_eq [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_sort_eq_aux [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_sort_kinded [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_sort_kinded_depth [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_sort_strenghten [lemma, in Lambda.TPOSR.UnlabConv]
tposr_subset [constructor, in Lambda.TPOSR.Types]
tposr_subset_subset [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_sum [constructor, in Lambda.TPOSR.Types]
tposr_sum_sum [lemma, in Lambda.TPOSR.ChurchRosser]
tposr_term [definition, in Lambda.TPOSR.Types]
tposr_term_conv_env [lemma, in Lambda.TPOSR.UnlabConv]
tposr_term_depth [definition, in Lambda.TPOSR.TypesDepth]
tposr_term_fromd [lemma, in Lambda.TPOSR.TypesDepth]
tposr_term_tod [lemma, in Lambda.TPOSR.TypesDepth]
tposr_to_tposrd [lemma, in Lambda.TPOSR.TypesDepth]
tposr_to_tposrd_wf [definition, in Lambda.TPOSR.TypesDepth]
tposr_tposrd [lemma, in Lambda.TPOSR.TypesDepth]
tposr_tposrd_type [lemma, in Lambda.TPOSR.TypesDepth]
tposr_tposrd_wf [lemma, in Lambda.TPOSR.TypesDepth]
tposr_tposr_coerce [lemma, in Lambda.TPOSR.ChurchRosserDepth]
tposr_tposr_term [lemma, in Lambda.TPOSR.Types]
TPOSR_trans [library]
tposr_uniqueness_of_types [lemma, in Lambda.TPOSR.UniquenessOfTypes]
tposr_unique_sort [lemma, in Lambda.Meta.TPOSR_JRussell]
tposr_unique_sort_right [lemma, in Lambda.TPOSR.Equiv]
tposr_unlab_conv [lemma, in Lambda.TPOSR.UnlabConv]
tposr_var [constructor, in Lambda.TPOSR.Types]
tposr_wf [inductive, in Lambda.TPOSR.Types]
Transitivity [library]
Transitivity [library]
TransitivitySet [library]
trans_conv_conv [lemma, in Lambda.Reduction]
trans_conv_conv [lemma, in Lambda.TPOSR.Reduction]
trans_conv_exp [constructor, in Lambda.Reduction]
trans_conv_exp [constructor, in Lambda.TPOSR.Reduction]
trans_conv_lred [constructor, in Lambda.TPOSR.Reduction]
trans_conv_red [constructor, in Lambda.Reduction]
trans_lred [constructor, in Lambda.TPOSR.Reduction]
trans_lred_lred [lemma, in Lambda.TPOSR.Reduction]
trans_red [constructor, in Lambda.Reduction]
trans_red_red [lemma, in Lambda.Reduction]
trunc [inductive, in Lambda.MyList]
trunc_list [lemma, in Lambda.JRussell.Validity]
trunc_O [constructor, in Lambda.MyList]
trunc_S [constructor, in Lambda.MyList]
TSmap [definition, in Lambda.ListType]
TTrunc [inductive, in Lambda.ListType]
Ttr_O [constructor, in Lambda.ListType]
Ttr_S [constructor, in Lambda.ListType]
typ [inductive, in Lambda.CCSum.Types]
typ [inductive, in Lambda.Russell.Types]
typ [inductive, in Lambda.JRussell.Types]
TypeCase [library]
Types [library]
Types [library]
Types [library]
Types [library]
TypesDepth [library]
TypesFunctionality [library]
type_abs [constructor, in Lambda.Russell.Types]
type_abs [constructor, in Lambda.CCSum.Types]
type_abs [constructor, in Lambda.JRussell.Types]
type_app [constructor, in Lambda.CCSum.Types]
type_app [constructor, in Lambda.Russell.Types]
type_app [constructor, in Lambda.JRussell.Types]
type_case [lemma, in Lambda.CCSum.TypeCase]
type_conv [constructor, in Lambda.Russell.Types]
type_conv [constructor, in Lambda.JRussell.Types]
type_conv [constructor, in Lambda.CCSum.Types]
type_conv_env [lemma, in Lambda.JRussell.Validity]
type_conv_env [lemma, in Lambda.JRussell.Conversion]
type_free_db [lemma, in Lambda.CCSum.TypeCase]
type_free_db [lemma, in Lambda.JRussell.Freevars]
type_has_no_kind [lemma, in Lambda.JRussell.GenerationNotKind]
type_has_no_kind [lemma, in Lambda.Russell.GenerationNotKind]
type_jrussell_to_russell [lemma, in Lambda.Meta.JRussell_Russell]
type_kind_not_conv [lemma, in Lambda.Russell.Unicity]
type_kind_not_conv [lemma, in Lambda.CCSum.Unicity]
type_kind_range [lemma, in Lambda.Russell.GenerationCoerce]
type_kind_range [lemma, in Lambda.JRussell.GenerationCoerce]
type_no_kind [definition, in Lambda.Russell.GenerationNotKind]
type_no_kind [definition, in Lambda.JRussell.GenerationNotKind]
type_no_kind_lift [lemma, in Lambda.Russell.GenerationNotKind]
type_no_kind_lift [lemma, in Lambda.JRussell.GenerationNotKind]
type_no_kind_not_kind [lemma, in Lambda.JRussell.GenerationNotKind]
type_no_kind_not_kind [lemma, in Lambda.Russell.GenerationNotKind]
type_no_kind_prod_type [lemma, in Lambda.JRussell.GenerationNotKind]
type_no_kind_prod_type [lemma, in Lambda.Russell.GenerationNotKind]
type_no_kind_sum_type [lemma, in Lambda.JRussell.GenerationNotKind]
type_no_kind_sum_type [lemma, in Lambda.Russell.GenerationNotKind]
type_no_kind_type [lemma, in Lambda.JRussell.GenerationNotKind]
type_no_kind_type [lemma, in Lambda.Russell.GenerationNotKind]
type_pair [constructor, in Lambda.CCSum.Types]
type_pair [constructor, in Lambda.JRussell.Types]
type_pair [constructor, in Lambda.Russell.Types]
type_pair_unique [lemma, in Lambda.CCSum.Inversion]
type_pair_unique [lemma, in Lambda.Russell.Unicity]
type_pair_unique2 [lemma, in Lambda.Russell.Unicity]
type_pair_unique2 [lemma, in Lambda.CCSum.Inversion]
type_pi1 [constructor, in Lambda.JRussell.Types]
type_pi1 [constructor, in Lambda.Russell.Types]
type_pi1 [constructor, in Lambda.CCSum.Types]
type_pi2 [constructor, in Lambda.CCSum.Types]
type_pi2 [constructor, in Lambda.JRussell.Types]
type_pi2 [constructor, in Lambda.Russell.Types]
type_prod [constructor, in Lambda.Russell.Types]
type_prod [constructor, in Lambda.JRussell.Types]
type_prod [constructor, in Lambda.CCSum.Types]
type_prop [constructor, in Lambda.Russell.Types]
type_prop [constructor, in Lambda.JRussell.Types]
type_prop [constructor, in Lambda.CCSum.Types]
type_prop_set [lemma, in Lambda.CCSum.Types]
type_prop_set [lemma, in Lambda.Russell.Types]
type_range [definition, in Lambda.Russell.GenerationCoerce]
type_range [definition, in Lambda.JRussell.GenerationCoerce]
type_range_lift [lemma, in Lambda.JRussell.GenerationRange]
type_range_lift [lemma, in Lambda.Russell.GenerationRange]
type_range_lift_inv [lemma, in Lambda.JRussell.GenerationRange]
type_range_sub [lemma, in Lambda.JRussell.GenerationRange]
type_range_sub [lemma, in Lambda.Russell.GenerationRange]
type_range_subst [lemma, in Lambda.JRussell.GenerationRange]
type_range_subst [lemma, in Lambda.Russell.GenerationRange]
type_range_subst2 [lemma, in Lambda.Russell.GenerationRange]
type_range_subst_inv [lemma, in Lambda.JRussell.GenerationRange]
type_range_subst_not_kind [lemma, in Lambda.JRussell.GenerationNotKind]
type_range_subst_not_kind [lemma, in Lambda.Russell.GenerationNotKind]
type_reduction [lemma, in Lambda.CCSum.Unicity]
type_reduction [lemma, in Lambda.Russell.Unicity]
type_russell_jrussell [lemma, in Lambda.Meta.Russell_JRussell]
type_russell_tposr [lemma, in Lambda.Meta.Russell_TPOSR]
type_set [constructor, in Lambda.CCSum.Types]
type_set [constructor, in Lambda.JRussell.Types]
type_set [constructor, in Lambda.Russell.Types]
type_sorted [lemma, in Lambda.Russell.Generation]
type_subset [constructor, in Lambda.JRussell.Types]
type_subset [constructor, in Lambda.CCSum.Types]
type_subset [constructor, in Lambda.Russell.Types]
type_sum [constructor, in Lambda.Russell.Types]
type_sum [constructor, in Lambda.JRussell.Types]
type_sum [constructor, in Lambda.CCSum.Types]
type_var [constructor, in Lambda.JRussell.Types]
type_var [constructor, in Lambda.CCSum.Types]
type_var [constructor, in Lambda.Russell.Types]
type_weak [constructor, in Lambda.JRussell.Types]
type_weak_lift_rec [lemma, in Lambda.JRussell.Thinning]
type_weak_weak [lemma, in Lambda.JRussell.Thinning]
typ_coerce_env [lemma, in Lambda.JRussell.Coercion]
typ_consistent [lemma, in Lambda.JRussell.Basic]
typ_conv_conv [lemma, in Lambda.CCSum.Unicity]
typ_conv_conv_coerce [lemma, in Lambda.Russell.Unicity]
typ_conv_env [lemma, in Lambda.Russell.Coercion]
typ_conv_env [lemma, in Lambda.CCSum.SubjectReduction]
typ_conv_env [lemma, in Lambda.Russell.Narrowing]
typ_exp_env [lemma, in Lambda.CCSum.SubjectReduction]
typ_free_db [lemma, in Lambda.CCSum.Types]
typ_free_db [lemma, in Lambda.Russell.Types]
typ_free_db [lemma, in Lambda.JRussell.Freevars]
typ_inversion [lemma, in Lambda.Russell.Inversion]
typ_inversion [lemma, in Lambda.Russell.Inversion]
typ_inversion [lemma, in Lambda.CCSum.Inversion]
typ_mem_kind [lemma, in Lambda.Russell.Inversion]
typ_mem_kind [lemma, in Lambda.Russell.Inversion]
typ_mem_kind [lemma, in Lambda.CCSum.Inversion]
typ_not_kind [lemma, in Lambda.Russell.GenerationNotKind]
typ_not_kind [lemma, in Lambda.Russell.Types]
typ_not_kind [lemma, in Lambda.JRussell.GenerationNotKind]
typ_not_kind2 [lemma, in Lambda.Russell.GenerationNotKind]
typ_not_kind2 [lemma, in Lambda.JRussell.GenerationNotKind]
typ_red_env [lemma, in Lambda.CCSum.SubjectReduction]
typ_red_env [lemma, in Lambda.Russell.SubjectReduction]
typ_sort [lemma, in Lambda.JRussell.GenerationCoerce]
typ_sort [lemma, in Lambda.Russell.Types]
typ_sort_aux [lemma, in Lambda.Russell.Types]
typ_sort_kind [lemma, in Lambda.Russell.Inversion]
typ_sort_kind [lemma, in Lambda.Russell.Inversion]
typ_sub_weak [lemma, in Lambda.CCSum.Substitution]
typ_sub_weak [lemma, in Lambda.JRussell.Substitution]
typ_unique [lemma, in Lambda.CCSum.Unicity]
typ_unique [lemma, in Lambda.Russell.Unicity]
typ_weak_weak [lemma, in Lambda.CCSum.Thinning]
typ_wf [lemma, in Lambda.CCSum.Types]
typ_wf [lemma, in Lambda.Russell.Types]
| 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 | _ | (1755 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 | _ | (1070 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 | _ | (6 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 | _ | (426 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 | _ | (81 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 | _ | (73 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 | _ | (3 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 | _ | (96 entries) |