| 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 (lemma)
term_free_db [in Lambda.JRussell.Freevars]term_type_range_kinded [in Lambda.JRussell.GenerationRange]
term_type_range_kinded [in Lambda.Russell.GenerationRange]
term_type_range_not_kind [in Lambda.JRussell.GenerationRange]
term_type_range_not_kind [in Lambda.Russell.GenerationRange]
thinning [in Lambda.CCSum.Thinning]
thinning [in Lambda.TPOSR.Thinning]
thinning [in Lambda.Russell.Thinning]
thinning_coerce [in Lambda.TPOSR.Thinning]
thinning_coerce [in Lambda.Russell.Thinning]
thinning_eq [in Lambda.TPOSR.Thinning]
thinning_n [in Lambda.JRussell.Thinning]
thinning_n [in Lambda.Russell.Thinning]
thinning_n [in Lambda.CCSum.Thinning]
thinning_n [in Lambda.TPOSR.Thinning]
thinning_n_coerce [in Lambda.JRussell.Thinning]
thinning_n_coerce [in Lambda.Russell.Thinning]
thinning_n_coerce [in Lambda.TPOSR.Thinning]
thinning_n_eq [in Lambda.TPOSR.Thinning]
Tins_eq [in Lambda.ListType]
Tins_gt [in Lambda.ListType]
Tins_le [in Lambda.ListType]
toq [in Lambda.TPOSR.UniquenessOfTypes]
tposrd_tposr [in Lambda.TPOSR.TypesDepth]
tposrd_tposr_coerce [in Lambda.TPOSR.ChurchRosserDepth]
tposrd_tposr_term_depth [in Lambda.TPOSR.TypesDepth]
tposrd_tposr_type [in Lambda.TPOSR.TypesDepth]
tposrd_tposr_wf [in Lambda.TPOSR.TypesDepth]
tposrd_unique_sort [in Lambda.TPOSR.Equiv]
tposrp_abs [in Lambda.TPOSR.TPOSR_trans]
tposrp_abs_aux [in Lambda.TPOSR.TPOSR_trans]
tposrp_abs_aux2 [in Lambda.TPOSR.TPOSR_trans]
tposrp_app [in Lambda.TPOSR.TPOSR_trans]
tposrp_app_aux [in Lambda.TPOSR.TPOSR_trans]
tposrp_app_aux2 [in Lambda.TPOSR.TPOSR_trans]
tposrp_app_aux3 [in Lambda.TPOSR.TPOSR_trans]
tposrp_coerce_env [in Lambda.TPOSR.CtxCoercion]
tposrp_conv [in Lambda.TPOSR.Basic]
tposrp_conv_env [in Lambda.TPOSR.ChurchRosser]
tposrp_conv_env_full [in Lambda.TPOSR.UnlabConv]
tposrp_conv_l [in Lambda.TPOSR.Basic]
tposrp_conv_r [in Lambda.TPOSR.Basic]
tposrp_cr [in Lambda.TPOSR.ChurchRosser]
tposrp_equiv_l [in Lambda.TPOSR.Equiv]
tposrp_n_cr [in Lambda.TPOSR.ChurchRosser]
tposrp_n_tposrp [in Lambda.TPOSR.ChurchRosser]
tposrp_n_transitive [in Lambda.TPOSR.ChurchRosser]
tposrp_pair [in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux1 [in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux2 [in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux3 [in Lambda.TPOSR.TPOSR_trans]
tposrp_pair_aux4 [in Lambda.TPOSR.TPOSR_trans]
tposrp_pi [in Lambda.TPOSR.ChurchRosser]
tposrp_pi1 [in Lambda.TPOSR.TPOSR_trans]
tposrp_pi1_aux [in Lambda.TPOSR.TPOSR_trans]
tposrp_pi2 [in Lambda.TPOSR.TPOSR_trans]
tposrp_pi2_aux [in Lambda.TPOSR.TPOSR_trans]
tposrp_pi_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_pre_coerce_env_full [in Lambda.TPOSR.PreCtxCoercion]
tposrp_prod [in Lambda.TPOSR.TPOSR_trans]
tposrp_prod_aux [in Lambda.TPOSR.TPOSR_trans]
tposrp_prod_prod [in Lambda.TPOSR.ChurchRosser]
tposrp_prod_prod_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_refl_l [in Lambda.TPOSR.LeftReflexivity]
tposrp_refl_r [in Lambda.TPOSR.RightReflexivity]
tposrp_sigma [in Lambda.TPOSR.TPOSR_trans]
tposrp_sigma_aux [in Lambda.TPOSR.TPOSR_trans]
tposrp_sort [in Lambda.TPOSR.ChurchRosser]
tposrp_sort_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_sort_eq [in Lambda.TPOSR.ChurchRosser]
tposrp_sort_eq_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_subset [in Lambda.TPOSR.TPOSR_trans]
tposrp_subset [in Lambda.TPOSR.ChurchRosser]
tposrp_subset_aux [in Lambda.TPOSR.TPOSR_trans]
tposrp_subset_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_subset_subset [in Lambda.TPOSR.ChurchRosser]
tposrp_subset_subset_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_sum [in Lambda.TPOSR.ChurchRosser]
tposrp_sum_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_sum_sum [in Lambda.TPOSR.ChurchRosser]
tposrp_sum_sum_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_tposrp_n [in Lambda.TPOSR.ChurchRosser]
tposrp_tposr_eq [in Lambda.TPOSR.ChurchRosser]
tposrp_tposr_eq [in Lambda.TPOSR.Basic]
tposrp_tposr_eq_aux [in Lambda.TPOSR.ChurchRosser]
tposrp_tposr_eq_aux [in Lambda.TPOSR.Basic]
tposrp_uniqueness_of_types [in Lambda.TPOSR.UniquenessOfTypes]
tposrp_unique_sort [in Lambda.TPOSR.UnicityOfSorting]
tposr_coerces_env [in Lambda.TPOSR.CoerceNoTrans]
tposr_coerce_env [in Lambda.TPOSR.CtxCoercion]
tposr_coerce_eq_sort [in Lambda.TPOSR.ChurchRosser]
tposr_coerce_eq_sort_aux [in Lambda.TPOSR.ChurchRosser]
tposr_coerce_russell [in Lambda.Meta.TPOSR_Russell]
tposr_coerce_sorts [in Lambda.TPOSR.ChurchRosser]
tposr_coerce_sort_l [in Lambda.TPOSR.ChurchRosser]
tposr_coerce_sort_r [in Lambda.TPOSR.ChurchRosser]
tposr_coerce_unique_sort [in Lambda.Meta.TPOSR_JRussell]
tposr_coerce_unique_sort_right [in Lambda.TPOSR.Equiv]
tposr_conv_eq [in Lambda.TPOSR.Basic]
tposr_conv_l [in Lambda.TPOSR.Basic]
tposr_conv_r [in Lambda.TPOSR.Basic]
tposr_equiv_l [in Lambda.TPOSR.Equiv]
tposr_equiv_r [in Lambda.TPOSR.Equiv]
tposr_eq_cr [in Lambda.TPOSR.ChurchRosser]
tposr_eq_prod_subset [in Lambda.TPOSR.ChurchRosser]
tposr_eq_prod_sum [in Lambda.TPOSR.ChurchRosser]
tposr_eq_russell [in Lambda.Meta.TPOSR_Russell]
tposr_eq_sort [in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_prod [in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_subset [in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_sum [in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_tposrp [in Lambda.TPOSR.ChurchRosser]
tposr_eq_sort_tposrp_aux [in Lambda.TPOSR.ChurchRosser]
tposr_eq_sum_subset [in Lambda.TPOSR.ChurchRosser]
tposr_eq_unique_sort [in Lambda.Meta.TPOSR_JRussell]
tposr_eq_unique_sort_right [in Lambda.TPOSR.Equiv]
tposr_exp_env [in Lambda.TPOSR.CtxExpansion]
tposr_not_kind [in Lambda.TPOSR.Basic]
tposr_not_kind_aux [in Lambda.TPOSR.Basic]
tposr_pair_coerce_left [in Lambda.TPOSR.RightReflexivity]
tposr_pair_coerce_left_aux [in Lambda.TPOSR.RightReflexivity]
tposr_pair_coerce_right [in Lambda.TPOSR.RightReflexivity]
tposr_pair_coerce_right_aux [in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_comp [in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_comp_aux [in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_left [in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_left_aux [in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_right [in Lambda.TPOSR.RightReflexivity]
tposr_pair_red_right_aux [in Lambda.TPOSR.RightReflexivity]
tposr_pre_coerce_env [in Lambda.TPOSR.PreCtxCoercion]
tposr_prod_prod [in Lambda.TPOSR.ChurchRosser]
tposr_red_env [in Lambda.TPOSR.CtxReduction]
tposr_russell [in Lambda.Meta.TPOSR_Russell]
tposr_sort [in Lambda.TPOSR.ChurchRosser]
tposr_sort_aux [in Lambda.TPOSR.ChurchRosser]
tposr_sort_eq [in Lambda.TPOSR.ChurchRosser]
tposr_sort_eq_aux [in Lambda.TPOSR.ChurchRosser]
tposr_sort_kinded [in Lambda.TPOSR.ChurchRosser]
tposr_sort_kinded_depth [in Lambda.TPOSR.ChurchRosser]
tposr_sort_strenghten [in Lambda.TPOSR.UnlabConv]
tposr_subset_subset [in Lambda.TPOSR.ChurchRosser]
tposr_sum_sum [in Lambda.TPOSR.ChurchRosser]
tposr_term_conv_env [in Lambda.TPOSR.UnlabConv]
tposr_term_fromd [in Lambda.TPOSR.TypesDepth]
tposr_term_tod [in Lambda.TPOSR.TypesDepth]
tposr_to_tposrd [in Lambda.TPOSR.TypesDepth]
tposr_tposrd [in Lambda.TPOSR.TypesDepth]
tposr_tposrd_type [in Lambda.TPOSR.TypesDepth]
tposr_tposrd_wf [in Lambda.TPOSR.TypesDepth]
tposr_tposr_coerce [in Lambda.TPOSR.ChurchRosserDepth]
tposr_tposr_term [in Lambda.TPOSR.Types]
tposr_uniqueness_of_types [in Lambda.TPOSR.UniquenessOfTypes]
tposr_unique_sort [in Lambda.Meta.TPOSR_JRussell]
tposr_unique_sort_right [in Lambda.TPOSR.Equiv]
tposr_unlab_conv [in Lambda.TPOSR.UnlabConv]
trans_conv_conv [in Lambda.Reduction]
trans_conv_conv [in Lambda.TPOSR.Reduction]
trans_lred_lred [in Lambda.TPOSR.Reduction]
trans_red_red [in Lambda.Reduction]
trunc_list [in Lambda.JRussell.Validity]
type_case [in Lambda.CCSum.TypeCase]
type_conv_env [in Lambda.JRussell.Validity]
type_conv_env [in Lambda.JRussell.Conversion]
type_free_db [in Lambda.CCSum.TypeCase]
type_free_db [in Lambda.JRussell.Freevars]
type_has_no_kind [in Lambda.JRussell.GenerationNotKind]
type_has_no_kind [in Lambda.Russell.GenerationNotKind]
type_jrussell_to_russell [in Lambda.Meta.JRussell_Russell]
type_kind_not_conv [in Lambda.Russell.Unicity]
type_kind_not_conv [in Lambda.CCSum.Unicity]
type_kind_range [in Lambda.Russell.GenerationCoerce]
type_kind_range [in Lambda.JRussell.GenerationCoerce]
type_no_kind_lift [in Lambda.Russell.GenerationNotKind]
type_no_kind_lift [in Lambda.JRussell.GenerationNotKind]
type_no_kind_not_kind [in Lambda.JRussell.GenerationNotKind]
type_no_kind_not_kind [in Lambda.Russell.GenerationNotKind]
type_no_kind_prod_type [in Lambda.JRussell.GenerationNotKind]
type_no_kind_prod_type [in Lambda.Russell.GenerationNotKind]
type_no_kind_sum_type [in Lambda.JRussell.GenerationNotKind]
type_no_kind_sum_type [in Lambda.Russell.GenerationNotKind]
type_no_kind_type [in Lambda.JRussell.GenerationNotKind]
type_no_kind_type [in Lambda.Russell.GenerationNotKind]
type_pair_unique [in Lambda.CCSum.Inversion]
type_pair_unique [in Lambda.Russell.Unicity]
type_pair_unique2 [in Lambda.Russell.Unicity]
type_pair_unique2 [in Lambda.CCSum.Inversion]
type_prop_set [in Lambda.CCSum.Types]
type_prop_set [in Lambda.Russell.Types]
type_range_lift [in Lambda.JRussell.GenerationRange]
type_range_lift [in Lambda.Russell.GenerationRange]
type_range_lift_inv [in Lambda.JRussell.GenerationRange]
type_range_sub [in Lambda.JRussell.GenerationRange]
type_range_sub [in Lambda.Russell.GenerationRange]
type_range_subst [in Lambda.JRussell.GenerationRange]
type_range_subst [in Lambda.Russell.GenerationRange]
type_range_subst2 [in Lambda.Russell.GenerationRange]
type_range_subst_inv [in Lambda.JRussell.GenerationRange]
type_range_subst_not_kind [in Lambda.JRussell.GenerationNotKind]
type_range_subst_not_kind [in Lambda.Russell.GenerationNotKind]
type_reduction [in Lambda.CCSum.Unicity]
type_reduction [in Lambda.Russell.Unicity]
type_russell_jrussell [in Lambda.Meta.Russell_JRussell]
type_russell_tposr [in Lambda.Meta.Russell_TPOSR]
type_sorted [in Lambda.Russell.Generation]
type_weak_lift_rec [in Lambda.JRussell.Thinning]
type_weak_weak [in Lambda.JRussell.Thinning]
typ_coerce_env [in Lambda.JRussell.Coercion]
typ_consistent [in Lambda.JRussell.Basic]
typ_conv_conv [in Lambda.CCSum.Unicity]
typ_conv_conv_coerce [in Lambda.Russell.Unicity]
typ_conv_env [in Lambda.Russell.Coercion]
typ_conv_env [in Lambda.CCSum.SubjectReduction]
typ_conv_env [in Lambda.Russell.Narrowing]
typ_exp_env [in Lambda.CCSum.SubjectReduction]
typ_free_db [in Lambda.CCSum.Types]
typ_free_db [in Lambda.Russell.Types]
typ_free_db [in Lambda.JRussell.Freevars]
typ_inversion [in Lambda.Russell.Inversion]
typ_inversion [in Lambda.Russell.Inversion]
typ_inversion [in Lambda.CCSum.Inversion]
typ_mem_kind [in Lambda.Russell.Inversion]
typ_mem_kind [in Lambda.Russell.Inversion]
typ_mem_kind [in Lambda.CCSum.Inversion]
typ_not_kind [in Lambda.Russell.GenerationNotKind]
typ_not_kind [in Lambda.Russell.Types]
typ_not_kind [in Lambda.JRussell.GenerationNotKind]
typ_not_kind2 [in Lambda.Russell.GenerationNotKind]
typ_not_kind2 [in Lambda.JRussell.GenerationNotKind]
typ_red_env [in Lambda.CCSum.SubjectReduction]
typ_red_env [in Lambda.Russell.SubjectReduction]
typ_sort [in Lambda.JRussell.GenerationCoerce]
typ_sort [in Lambda.Russell.Types]
typ_sort_aux [in Lambda.Russell.Types]
typ_sort_kind [in Lambda.Russell.Inversion]
typ_sort_kind [in Lambda.Russell.Inversion]
typ_sub_weak [in Lambda.CCSum.Substitution]
typ_sub_weak [in Lambda.JRussell.Substitution]
typ_unique [in Lambda.CCSum.Unicity]
typ_unique [in Lambda.Russell.Unicity]
typ_weak_weak [in Lambda.CCSum.Thinning]
typ_wf [in Lambda.CCSum.Types]
typ_wf [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) |