| 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) |
C (lemma)
church_rosser [in Lambda.Conv]church_rosser [in Lambda.TPOSR.ChurchRosser]
church_rosser [in Lambda.TPOSR.Conv]
church_rosser_depth [in Lambda.TPOSR.ChurchRosserDepth]
coerces_coerce [in Lambda.TPOSR.CoerceNoTrans]
coerces_coerce [in Lambda.Russell.Narrowing]
coerces_coerces_db [in Lambda.Russell.Narrowing]
coerces_coerces_env [in Lambda.TPOSR.CoerceNoTrans]
coerces_coerce_rc_depth [in Lambda.TPOSR.CoerceNoTrans]
coerces_db_coerce [in Lambda.Russell.Depth]
coerces_db_coerces [in Lambda.Russell.Narrowing]
coerces_db_depth [in Lambda.Russell.Narrowing]
coerces_in_env_coerce_in_env [in Lambda.TPOSR.CoerceNoTrans]
coerces_sort_l [in Lambda.Russell.Transitivity]
coerces_sort_l [in Lambda.TPOSR.TransitivitySet]
coerces_sort_r [in Lambda.Russell.Transitivity]
coerces_sort_r [in Lambda.TPOSR.TransitivitySet]
coerces_sym [in Lambda.TPOSR.CoerceNoTrans]
coerces_trans [in Lambda.TPOSR.Transitivity]
coerce_coerces_db [in Lambda.Russell.Depth]
coerce_coerce_env [in Lambda.JRussell.Coercion]
coerce_coerce_env [in Lambda.TPOSR.CtxCoercion]
coerce_coerce_free [in Lambda.JRussell.Derivable]
coerce_coerce_l [in Lambda.TPOSR.LeftReflexivity]
coerce_coerce_r [in Lambda.TPOSR.LeftReflexivity]
coerce_coerce_rc_depth [in Lambda.TPOSR.Transitivity]
coerce_consistent [in Lambda.JRussell.Basic]
coerce_conv_env [in Lambda.Russell.Coercion]
coerce_conv_env [in Lambda.Russell.Narrowing]
coerce_conv_env [in Lambda.TPOSR.CtxConversion]
coerce_conv_env [in Lambda.JRussell.Conversion]
coerce_conv_env [in Lambda.JRussell.Validity]
coerce_conv_env_full [in Lambda.TPOSR.UnlabConv]
coerce_exp_env [in Lambda.TPOSR.CtxExpansion]
coerce_free_coerce [in Lambda.JRussell.Derivable]
coerce_free_db [in Lambda.JRussell.Freevars]
coerce_in_env_from_coercion [in Lambda.Russell.Narrowing]
coerce_in_env_pre [in Lambda.TPOSR.CtxCoercion]
coerce_in_env_sym [in Lambda.TPOSR.CtxCoercion]
coerce_in_env_to_coercion [in Lambda.Russell.Narrowing]
coerce_is_prop [in Lambda.Russell.Types]
coerce_is_prop [in Lambda.JRussell.Basic]
coerce_item [in Lambda.TPOSR.PreCtxCoercion]
coerce_jrussell_to_russell [in Lambda.Meta.JRussell_Russell]
coerce_not_kind [in Lambda.JRussell.Generation]
coerce_not_kind_l [in Lambda.Russell.GenerationCoerce]
coerce_not_kind_l [in Lambda.JRussell.GenerationCoerce]
coerce_not_kind_r [in Lambda.Russell.GenerationCoerce]
coerce_not_kind_r [in Lambda.JRussell.GenerationCoerce]
coerce_pre_coerce_env [in Lambda.TPOSR.PreCtxCoercion]
coerce_pre_coerce_env_full [in Lambda.TPOSR.PreCtxCoercion]
coerce_propset_aux [in Lambda.JRussell.GenerationCoerce]
coerce_propset_l [in Lambda.Russell.GenerationCoerce]
coerce_propset_l [in Lambda.JRussell.GenerationCoerce]
coerce_propset_l_aux [in Lambda.Russell.GenerationCoerce]
coerce_propset_r [in Lambda.JRussell.GenerationCoerce]
coerce_propset_r [in Lambda.Russell.GenerationCoerce]
coerce_propset_r_aux [in Lambda.Russell.GenerationCoerce]
coerce_prop_prop [in Lambda.JRussell.Basic]
coerce_prop_prop [in Lambda.Russell.Types]
coerce_rc_depth_coerce [in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_coerces [in Lambda.TPOSR.CoerceNoTrans]
coerce_rc_depth_sym [in Lambda.TPOSR.Transitivity]
coerce_rc_depth_trans [in Lambda.TPOSR.Transitivity]
coerce_red_env [in Lambda.TPOSR.CtxReduction]
coerce_refls [in Lambda.TPOSR.RightReflexivity]
coerce_refl_l [in Lambda.TPOSR.RightReflexivity]
coerce_refl_r [in Lambda.TPOSR.RightReflexivity]
coerce_russell_tposr [in Lambda.Meta.Russell_TPOSR]
coerce_set_set [in Lambda.JRussell.Basic]
coerce_set_set [in Lambda.Russell.Types]
coerce_sort [in Lambda.Russell.Types]
coerce_sort_l [in Lambda.JRussell.Validity]
coerce_sort_l [in Lambda.Russell.Types]
coerce_sort_l_in_kind [in Lambda.JRussell.GenerationCoerce]
coerce_sort_l_in_kind [in Lambda.Russell.GenerationCoerce]
coerce_sort_r [in Lambda.Russell.Types]
coerce_sort_r [in Lambda.JRussell.Validity]
coerce_sort_r_in_kind [in Lambda.Russell.GenerationCoerce]
coerce_sort_r_in_kind [in Lambda.JRussell.GenerationCoerce]
coerce_sub_weak [in Lambda.JRussell.Substitution]
coerce_sym [in Lambda.Russell.Coercion]
coerce_trans [in Lambda.Russell.Transitivity]
coerce_trans_aux [in Lambda.TPOSR.TransitivitySet]
coerce_trans_aux [in Lambda.Russell.Transitivity]
coerce_trans_d [in Lambda.Russell.Transitivity]
coerce_trans_db_set [in Lambda.Russell.Transitivity]
coerce_unlab_conv_ctx [in Lambda.TPOSR.UnlabConv]
coerce_weak_lift_rec [in Lambda.JRussell.Thinning]
coerce_weak_weak [in Lambda.JRussell.Thinning]
commut_lift_subst [in Lambda.LiftSubst]
commut_lift_subst_rec [in Lambda.LiftSubst]
commut_llift_lsubst [in Lambda.TPOSR.LiftSubst]
commut_llift_lsubst_rec [in Lambda.TPOSR.LiftSubst]
commut_lred1_sublterm [in Lambda.TPOSR.Reduction]
commut_red1_subterm [in Lambda.Reduction]
compute_nf [in Lambda.TPOSR.Conv_Dec]
compute_nf [in Lambda.Conv_Dec]
confluence_lred [in Lambda.TPOSR.Conv]
confluence_par_lred [in Lambda.TPOSR.Conv]
confluence_par_red [in Lambda.Conv]
confluence_red [in Lambda.Conv]
consistency_ind [in Lambda.JRussell.Basic]
context_validity [in Lambda.TPOSR.Basic]
conv_coerce [in Lambda.Russell.Types]
conv_conv_abs [in Lambda.Reduction]
conv_conv_app [in Lambda.Reduction]
conv_conv_lift [in Lambda.Reduction]
conv_conv_llift [in Lambda.TPOSR.Reduction]
conv_conv_lsubst [in Lambda.TPOSR.Reduction]
conv_conv_pair [in Lambda.TPOSR.Reduction]
conv_conv_pair [in Lambda.Reduction]
conv_conv_pi1 [in Lambda.Reduction]
conv_conv_pi2 [in Lambda.Reduction]
conv_conv_prod [in Lambda.Reduction]
conv_conv_prod [in Lambda.TPOSR.Reduction]
conv_conv_subset [in Lambda.Reduction]
conv_conv_subset [in Lambda.TPOSR.Reduction]
conv_conv_subst [in Lambda.Reduction]
conv_conv_sum [in Lambda.TPOSR.Reduction]
conv_conv_sum [in Lambda.Reduction]
conv_dom [in Lambda.Russell.GenerationRange]
conv_dom [in Lambda.JRussell.GenerationRange]
conv_env [in Lambda.TPOSR.CtxConversion]
conv_env_conv_in_env [in Lambda.JRussell.Validity]
conv_env_full [in Lambda.TPOSR.UnlabConv]
conv_env_full_cons [in Lambda.TPOSR.UnlabConv]
conv_env_full_sym [in Lambda.TPOSR.UnlabConv]
conv_eq [in Lambda.TPOSR.UnlabConv]
conv_eq2 [in Lambda.Meta.Russell_TPOSR]
conv_in_env_coerce_in_env [in Lambda.TPOSR.CtxConversion]
conv_in_env_sym [in Lambda.TPOSR.CtxConversion]
conv_item [in Lambda.CCSum.SubjectReduction]
conv_item [in Lambda.Russell.Coercion]
conv_kind_prop [in Lambda.Conv]
conv_kind_prop [in Lambda.TPOSR.Conv]
conv_kind_set [in Lambda.TPOSR.Conv]
conv_kind_set [in Lambda.Conv]
conv_prod_abs [in Lambda.Conv]
conv_prod_pair [in Lambda.Conv]
conv_prod_subset [in Lambda.TPOSR.Conv]
conv_prod_subset [in Lambda.Conv]
conv_prod_sum [in Lambda.Conv]
conv_prod_sum [in Lambda.TPOSR.Conv]
conv_ref_prod [in Lambda.Conv]
conv_ref_subset [in Lambda.Conv]
conv_ref_sum [in Lambda.Conv]
conv_russell_jrussell [in Lambda.Meta.Russell_JRussell]
conv_sort [in Lambda.TPOSR.Conv]
conv_sort [in Lambda.Conv]
conv_sort_prod [in Lambda.TPOSR.Conv]
conv_sort_prod [in Lambda.Conv]
conv_sort_ref [in Lambda.Conv]
conv_sort_ref [in Lambda.TPOSR.Conv]
conv_sort_subset [in Lambda.Conv]
conv_sort_subset [in Lambda.TPOSR.Conv]
conv_sort_sum [in Lambda.TPOSR.Conv]
conv_sort_sum [in Lambda.Conv]
conv_subset_abs [in Lambda.Conv]
conv_subset_pair [in Lambda.Conv]
conv_subset_sum [in Lambda.Conv]
conv_subset_sum [in Lambda.TPOSR.Conv]
conv_sum_abs [in Lambda.Conv]
conv_sum_pair [in Lambda.Conv]
conv_unlab_conv [in Lambda.TPOSR.Unlab]
| 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) |