| 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) |
S (lemma)
sigma_functionality [in Lambda.TPOSR.TypesFunctionality]simpl_lift [in Lambda.LiftSubst]
simpl_lift_rec [in Lambda.LiftSubst]
simpl_llift [in Lambda.TPOSR.LiftSubst]
simpl_llift_rec [in Lambda.TPOSR.LiftSubst]
simpl_lsubst [in Lambda.TPOSR.LiftSubst]
simpl_lsubst_rec [in Lambda.TPOSR.LiftSubst]
simpl_subst [in Lambda.LiftSubst]
simpl_subst_rec [in Lambda.LiftSubst]
sn_lred_sn [in Lambda.TPOSR.Reduction]
sn_lsubst [in Lambda.TPOSR.Reduction]
sn_pair [in Lambda.Reduction]
sn_pair [in Lambda.TPOSR.Reduction]
sn_prod [in Lambda.Reduction]
sn_prod [in Lambda.TPOSR.Reduction]
sn_red_sn [in Lambda.Reduction]
sn_subset [in Lambda.Reduction]
sn_subset [in Lambda.TPOSR.Reduction]
sn_subst [in Lambda.Reduction]
sn_sum [in Lambda.Reduction]
sn_sum [in Lambda.TPOSR.Reduction]
sorting_lambda [in Lambda.Russell.Generation]
sorting_lambda_aux [in Lambda.Russell.Generation]
sorts_of_sorted [in Lambda.Russell.GenerationCoerce]
sorts_of_sorted [in Lambda.JRussell.GenerationCoerce]
sort_conv_eq [in Lambda.Russell.GenerationCoerce]
sort_conv_eq [in Lambda.JRussell.GenerationCoerce]
sort_eq_eq [in Lambda.JRussell.GenerationCoerce]
sort_judgement_empty_env [in Lambda.JRussell.Validity]
sort_level_ind [in Lambda.Terms]
sort_of_abs_range [in Lambda.Russell.GenerationRange]
sort_of_abs_range [in Lambda.JRussell.GenerationRange]
sort_of_abs_range_aux [in Lambda.JRussell.GenerationRange]
sort_of_abs_range_aux [in Lambda.Russell.GenerationRange]
sort_of_app [in Lambda.Russell.Generation]
sort_of_app2 [in Lambda.Russell.Generation]
sort_of_app_aux [in Lambda.Russell.Generation]
sort_of_app_aux2 [in Lambda.Russell.Generation]
sort_of_app_range [in Lambda.JRussell.GenerationRange]
sort_of_app_range [in Lambda.Russell.GenerationRange]
sort_of_app_range_aux [in Lambda.JRussell.GenerationRange]
sort_of_app_range_aux [in Lambda.Russell.GenerationRange]
sort_of_kinded [in Lambda.Russell.GenerationCoerce]
sort_of_kinded [in Lambda.JRussell.GenerationCoerce]
sort_of_kinded_aux [in Lambda.Russell.GenerationCoerce]
sort_of_kinded_aux [in Lambda.JRussell.GenerationCoerce]
sort_of_pair_range [in Lambda.JRussell.GenerationRange]
sort_of_pair_range [in Lambda.Russell.GenerationRange]
sort_of_pair_range_aux [in Lambda.Russell.GenerationRange]
sort_of_pair_range_aux [in Lambda.JRussell.GenerationRange]
sort_of_pi1_range [in Lambda.Russell.GenerationRange]
sort_of_pi1_range [in Lambda.JRussell.GenerationRange]
sort_of_pi1_range_aux [in Lambda.Russell.GenerationRange]
sort_of_pi1_range_aux [in Lambda.JRussell.GenerationRange]
sort_of_pi2_range [in Lambda.Russell.GenerationRange]
sort_of_pi2_range [in Lambda.JRussell.GenerationRange]
sort_of_pi2_range_aux [in Lambda.Russell.GenerationRange]
sort_of_pi2_range_aux [in Lambda.JRussell.GenerationRange]
sort_of_propset [in Lambda.JRussell.GenerationCoerce]
sort_of_propset [in Lambda.Russell.GenerationCoerce]
sort_of_sum [in Lambda.Russell.GenerationRange]
sort_of_sum [in Lambda.JRussell.GenerationRange]
sort_of_sum_aux [in Lambda.JRussell.GenerationRange]
sort_of_sum_aux [in Lambda.Russell.GenerationRange]
strength_sort_judgement [in Lambda.JRussell.Validity]
strength_sort_judgement [in Lambda.Russell.Generation]
strip_lemma [in Lambda.TPOSR.Conv]
strip_lemma [in Lambda.Conv]
str_confluence_par_lred1 [in Lambda.TPOSR.Conv]
str_confluence_par_red1 [in Lambda.Conv]
subject_reduction [in Lambda.CCSum.SubjectReduction]
subject_reduction [in Lambda.Russell.SubjectReduction]
subject_reduction [in Lambda.TPOSR.SubjectReduction]
subject_reduction_depth [in Lambda.TPOSR.SubjectReduction]
subject_reduction_p [in Lambda.TPOSR.SubjectReduction]
subj_red [in Lambda.Russell.SubjectReduction]
subj_red [in Lambda.CCSum.SubjectReduction]
sublterm_abs [in Lambda.TPOSR.Reduction]
sublterm_ord_norm [in Lambda.TPOSR.Conv_Dec]
sublterm_prod [in Lambda.TPOSR.Reduction]
sublterm_sn [in Lambda.TPOSR.Reduction]
sublterm_subset [in Lambda.TPOSR.Reduction]
sublterm_sum [in Lambda.TPOSR.Reduction]
subset_conv_left [in Lambda.TPOSR.TypesFunctionality]
subset_conv_right [in Lambda.TPOSR.TypesFunctionality]
subset_conv_right_aux [in Lambda.TPOSR.TypesFunctionality]
subset_functionality [in Lambda.TPOSR.TypesFunctionality]
subset_functionality_aux [in Lambda.TPOSR.TypesFunctionality]
substitution [in Lambda.TPOSR.Substitution]
substitution [in Lambda.Russell.Substitution]
substitution [in Lambda.CCSum.Substitution]
substitution [in Lambda.JRussell.Substitution]
substitution_coerce [in Lambda.JRussell.Substitution]
substitution_coerce [in Lambda.TPOSR.Substitution]
substitution_coerce [in Lambda.Russell.Substitution]
substitution_coerce_conv_l [in Lambda.Russell.Substitution]
substitution_coerce_conv_l_n [in Lambda.Russell.Substitution]
substitution_coerce_eq [in Lambda.TPOSR.UnlabConv]
substitution_coerce_n [in Lambda.TPOSR.Substitution]
substitution_coerce_tposrp [in Lambda.TPOSR.CtxCoercion]
substitution_eq [in Lambda.TPOSR.Substitution]
substitution_eq_n [in Lambda.TPOSR.Substitution]
substitution_jeq [in Lambda.JRussell.Substitution]
substitution_sorted [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_sorted [in Lambda.TPOSR.Substitution]
substitution_sorted [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_sorted_n [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_sorted_n [in Lambda.TPOSR.Substitution]
substitution_sorted_n [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposrp [in Lambda.TPOSR.Substitution]
substitution_tposrp_aux [in Lambda.TPOSR.Substitution]
substitution_tposrp_coerce [in Lambda.TPOSR.TPOSR_trans]
substitution_tposrp_tposr [in Lambda.TPOSR.TPOSR_trans]
substitution_tposr_coerce [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_coerce [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_coerce_n [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_coerce_n [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_eq [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_eq [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_eq_n [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_eq_n [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_n [in Lambda.TPOSR.Substitution]
substitution_tposr_tposr [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposr [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposrp [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposrp [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposrp_aux [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposrp_aux [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposr_n [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_tposr_n [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposr_wf_n [in Lambda.TPOSR.SubstitutionTPOSR]
substitution_tposr_tposr_wf_n [in Lambda.TPOSR.PreSubstitutionTPOSR]
substitution_tposr_wf_n [in Lambda.TPOSR.Substitution]
subst_ref_eq [in Lambda.LiftSubst]
subst_ref_gt [in Lambda.LiftSubst]
subst_ref_lt [in Lambda.LiftSubst]
subst_to_sort [in Lambda.JRussell.GenerationCoerce]
subst_to_sort [in Lambda.Russell.GenerationCoerce]
subterm_abs [in Lambda.Reduction]
subterm_ord_norm [in Lambda.Conv_Dec]
subterm_prod [in Lambda.Reduction]
subterm_sn [in Lambda.Reduction]
subterm_subset [in Lambda.Reduction]
subterm_sum [in Lambda.Reduction]
sub_red_env [in Lambda.TPOSR.PreSubstitutionTPOSR]
sum_conv_left [in Lambda.TPOSR.TypesFunctionality]
sum_conv_right [in Lambda.TPOSR.TypesFunctionality]
sum_conv_right_aux [in Lambda.TPOSR.TypesFunctionality]
sum_sort_functional [in Lambda.TPOSR.UniquenessOfTypes]
sum_sort_functional [in Lambda.JRussell.UnicityOfSortingRange]
sum_sort_prop [in Lambda.JRussell.GenerationRange]
sum_sort_prop [in Lambda.Russell.GenerationRange]
sym_conv [in Lambda.Reduction]
sym_conv [in Lambda.TPOSR.Reduction]
| 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) |