| 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
ChurchRosser [library]ChurchRosserDepth [library]
Church_Rosser [section, in Lambda.Conv]
church_rosser [lemma, in Lambda.Conv]
church_rosser [lemma, in Lambda.TPOSR.ChurchRosser]
Church_Rosser [section, in Lambda.TPOSR.Conv]
church_rosser [lemma, in Lambda.TPOSR.Conv]
church_rosser_depth [lemma, in Lambda.TPOSR.ChurchRosserDepth]
coerce [inductive, in Lambda.JRussell.Types]
coerce [inductive, in Lambda.Russell.Types]
CoerceDepth [library]
CoerceNoTrans [library]
coerces [inductive, in Lambda.Russell.Narrowing]
coerces [inductive, in Lambda.TPOSR.CoerceNoTrans]
coerces_coerce [lemma, in Lambda.TPOSR.CoerceNoTrans]
coerces_coerce [lemma, in Lambda.Russell.Narrowing]
coerces_coerces_db [lemma, in Lambda.Russell.Narrowing]
coerces_coerces_env [lemma, in Lambda.TPOSR.CoerceNoTrans]
coerces_coerce_rc_depth [lemma, in Lambda.TPOSR.CoerceNoTrans]
coerces_conv_l [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_conv_l [constructor, in Lambda.Russell.Depth]
coerces_conv_l [constructor, in Lambda.Russell.Narrowing]
coerces_conv_r [constructor, in Lambda.Russell.Narrowing]
coerces_conv_r [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_conv_r [constructor, in Lambda.Russell.Depth]
coerces_db [inductive, in Lambda.Russell.Depth]
coerces_db [inductive, in Lambda.Russell.Narrowing]
coerces_db_coerce [lemma, in Lambda.Russell.Depth]
coerces_db_coerces [lemma, in Lambda.Russell.Narrowing]
coerces_db_depth [lemma, in Lambda.Russell.Narrowing]
coerces_env_hd [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_env_tl [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_in_env [inductive, in Lambda.TPOSR.CoerceNoTrans]
coerces_in_env_coerce_in_env [lemma, in Lambda.TPOSR.CoerceNoTrans]
coerces_prod [constructor, in Lambda.Russell.Depth]
coerces_prod [constructor, in Lambda.Russell.Narrowing]
coerces_prod [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_refl [constructor, in Lambda.Russell.Depth]
coerces_refl [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_refl [constructor, in Lambda.Russell.Narrowing]
coerces_sort_l [lemma, in Lambda.Russell.Transitivity]
coerces_sort_l [lemma, in Lambda.TPOSR.TransitivitySet]
coerces_sort_r [lemma, in Lambda.Russell.Transitivity]
coerces_sort_r [lemma, in Lambda.TPOSR.TransitivitySet]
coerces_sub_l [constructor, in Lambda.Russell.Narrowing]
coerces_sub_l [constructor, in Lambda.Russell.Depth]
coerces_sub_l [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_sub_r [constructor, in Lambda.Russell.Narrowing]
coerces_sub_r [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_sub_r [constructor, in Lambda.Russell.Depth]
coerces_sum [constructor, in Lambda.Russell.Depth]
coerces_sum [constructor, in Lambda.TPOSR.CoerceNoTrans]
coerces_sum [constructor, in Lambda.Russell.Narrowing]
coerces_sym [lemma, in Lambda.TPOSR.CoerceNoTrans]
coerces_trans [lemma, in Lambda.TPOSR.Transitivity]
coerce_coerces_db [lemma, in Lambda.Russell.Depth]
coerce_coerce_env [lemma, in Lambda.JRussell.Coercion]
coerce_coerce_env [lemma, in Lambda.TPOSR.CtxCoercion]
coerce_coerce_free [lemma, in Lambda.JRussell.Derivable]
coerce_coerce_l [lemma, in Lambda.TPOSR.LeftReflexivity]
coerce_coerce_r [lemma, in Lambda.TPOSR.LeftReflexivity]
coerce_coerce_rc_depth [lemma, in Lambda.TPOSR.Transitivity]
coerce_consistent [lemma, in Lambda.JRussell.Basic]
coerce_conv [constructor, in Lambda.JRussell.Types]
coerce_conv [constructor, in Lambda.Russell.Types]
coerce_conv [constructor, in Lambda.Russell.Narrowing]
coerce_conv_env [lemma, in Lambda.Russell.Coercion]
coerce_conv_env [lemma, in Lambda.Russell.Narrowing]
coerce_conv_env [lemma, in Lambda.TPOSR.CtxConversion]
coerce_conv_env [lemma, in Lambda.JRussell.Conversion]
coerce_conv_env [lemma, in Lambda.JRussell.Validity]
coerce_conv_env_full [lemma, in Lambda.TPOSR.UnlabConv]
coerce_env_hd [constructor, in Lambda.Russell.Narrowing]
coerce_env_hd [constructor, in Lambda.Russell.Coercion]
coerce_env_hd [constructor, in Lambda.TPOSR.CtxCoercion]
coerce_env_hd [constructor, in Lambda.JRussell.Coercion]
coerce_env_tl [constructor, in Lambda.JRussell.Coercion]
coerce_env_tl [constructor, in Lambda.Russell.Narrowing]
coerce_env_tl [constructor, in Lambda.Russell.Coercion]
coerce_env_tl [constructor, in Lambda.TPOSR.CtxCoercion]
coerce_exp_env [lemma, in Lambda.TPOSR.CtxExpansion]
coerce_free [inductive, in Lambda.JRussell.Derivable]
coerce_free_coerce [lemma, in Lambda.JRussell.Derivable]
coerce_free_conv [constructor, in Lambda.JRussell.Derivable]
coerce_free_db [lemma, in Lambda.JRussell.Freevars]
coerce_free_prod [constructor, in Lambda.JRussell.Derivable]
coerce_free_sub_l [constructor, in Lambda.JRussell.Derivable]
coerce_free_sub_r [constructor, in Lambda.JRussell.Derivable]
coerce_free_sum [constructor, in Lambda.JRussell.Derivable]
coerce_free_sym [constructor, in Lambda.JRussell.Derivable]
coerce_free_trans [constructor, in Lambda.JRussell.Derivable]
coerce_free_weak [constructor, in Lambda.JRussell.Derivable]
coerce_in_env [inductive, in Lambda.Russell.Coercion]
coerce_in_env [inductive, in Lambda.TPOSR.CtxCoercion]
coerce_in_env [inductive, in Lambda.JRussell.Coercion]
coerce_in_env [inductive, in Lambda.Russell.Narrowing]
coerce_in_env_from_coercion [lemma, in Lambda.Russell.Narrowing]
coerce_in_env_pre [lemma, in Lambda.TPOSR.CtxCoercion]
coerce_in_env_sym [lemma, in Lambda.TPOSR.CtxCoercion]
coerce_in_env_to_coercion [lemma, in Lambda.Russell.Narrowing]
coerce_is_prop [lemma, in Lambda.Russell.Types]
coerce_is_prop [lemma, in Lambda.JRussell.Basic]
coerce_item [lemma, in Lambda.TPOSR.PreCtxCoercion]
coerce_jrussell_to_russell [lemma, in Lambda.Meta.JRussell_Russell]
coerce_not_kind [lemma, in Lambda.JRussell.Generation]
coerce_not_kind_l [lemma, in Lambda.Russell.GenerationCoerce]
coerce_not_kind_l [lemma, in Lambda.JRussell.GenerationCoerce]
coerce_not_kind_r [lemma, in Lambda.Russell.GenerationCoerce]
coerce_not_kind_r [lemma, in Lambda.JRussell.GenerationCoerce]
coerce_pre_coerce_env [lemma, in Lambda.TPOSR.PreCtxCoercion]
coerce_pre_coerce_env_full [lemma, in Lambda.TPOSR.PreCtxCoercion]
coerce_prod [constructor, in Lambda.JRussell.Types]
coerce_prod [constructor, in Lambda.Russell.Types]
coerce_prod [constructor, in Lambda.Russell.Narrowing]
coerce_propset_aux [lemma, in Lambda.JRussell.GenerationCoerce]
coerce_propset_l [lemma, in Lambda.Russell.GenerationCoerce]
coerce_propset_l [lemma, in Lambda.JRussell.GenerationCoerce]
coerce_propset_l_aux [lemma, in Lambda.Russell.GenerationCoerce]
coerce_propset_r [lemma, in Lambda.JRussell.GenerationCoerce]
coerce_propset_r [lemma, in Lambda.Russell.GenerationCoerce]
coerce_propset_r_aux [lemma, in Lambda.Russell.GenerationCoerce]
coerce_prop_prop [lemma, in Lambda.JRussell.Basic]
coerce_prop_prop [lemma, in Lambda.Russell.Types]
coerce_rc_depth [inductive, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_coerce [lemma, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_coerces [lemma, in Lambda.TPOSR.CoerceNoTrans]
coerce_rc_depth_conv_l [constructor, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_conv_r [constructor, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_prod [constructor, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_refl [constructor, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_sub_l [constructor, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_sub_r [constructor, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_sum [constructor, in Lambda.TPOSR.CoerceDepth]
coerce_rc_depth_sym [lemma, in Lambda.TPOSR.Transitivity]
coerce_rc_depth_trans [lemma, in Lambda.TPOSR.Transitivity]
coerce_red_env [lemma, in Lambda.TPOSR.CtxReduction]
coerce_refl [constructor, in Lambda.Russell.Types]
coerce_refl [constructor, in Lambda.Russell.Narrowing]
coerce_refls [lemma, in Lambda.TPOSR.RightReflexivity]
coerce_refl_l [lemma, in Lambda.TPOSR.RightReflexivity]
coerce_refl_r [lemma, in Lambda.TPOSR.RightReflexivity]
coerce_russell_tposr [lemma, in Lambda.Meta.Russell_TPOSR]
coerce_set_set [lemma, in Lambda.JRussell.Basic]
coerce_set_set [lemma, in Lambda.Russell.Types]
coerce_sort [lemma, in Lambda.Russell.Types]
coerce_sort_l [lemma, in Lambda.JRussell.Validity]
coerce_sort_l [lemma, in Lambda.Russell.Types]
coerce_sort_l_in_kind [lemma, in Lambda.JRussell.GenerationCoerce]
coerce_sort_l_in_kind [lemma, in Lambda.Russell.GenerationCoerce]
coerce_sort_r [lemma, in Lambda.Russell.Types]
coerce_sort_r [lemma, in Lambda.JRussell.Validity]
coerce_sort_r_in_kind [lemma, in Lambda.Russell.GenerationCoerce]
coerce_sort_r_in_kind [lemma, in Lambda.JRussell.GenerationCoerce]
coerce_sub_l [constructor, in Lambda.JRussell.Types]
coerce_sub_l [constructor, in Lambda.Russell.Narrowing]
coerce_sub_l [constructor, in Lambda.Russell.Types]
coerce_sub_r [constructor, in Lambda.JRussell.Types]
coerce_sub_r [constructor, in Lambda.Russell.Types]
coerce_sub_r [constructor, in Lambda.Russell.Narrowing]
coerce_sub_weak [lemma, in Lambda.JRussell.Substitution]
coerce_sum [constructor, in Lambda.JRussell.Types]
coerce_sum [constructor, in Lambda.Russell.Types]
coerce_sum [constructor, in Lambda.Russell.Narrowing]
coerce_sym [lemma, in Lambda.Russell.Coercion]
coerce_sym [constructor, in Lambda.JRussell.Types]
coerce_trans [lemma, in Lambda.Russell.Transitivity]
coerce_trans [constructor, in Lambda.JRussell.Types]
coerce_trans_aux [lemma, in Lambda.TPOSR.TransitivitySet]
coerce_trans_aux [lemma, in Lambda.Russell.Transitivity]
coerce_trans_d [lemma, in Lambda.Russell.Transitivity]
coerce_trans_db_set [lemma, in Lambda.Russell.Transitivity]
coerce_unique_sort [definition, in Lambda.TPOSR.UnicityOfSorting]
coerce_unlab_conv_ctx [lemma, in Lambda.TPOSR.UnlabConv]
coerce_weak [constructor, in Lambda.JRussell.Types]
coerce_weak_lift_rec [lemma, in Lambda.JRussell.Thinning]
coerce_weak_weak [lemma, in Lambda.JRussell.Thinning]
Coercion [library]
Coercion [library]
commut_lift_subst [lemma, in Lambda.LiftSubst]
commut_lift_subst_rec [lemma, in Lambda.LiftSubst]
commut_llift_lsubst [lemma, in Lambda.TPOSR.LiftSubst]
commut_llift_lsubst_rec [lemma, in Lambda.TPOSR.LiftSubst]
commut_lred1_sublterm [lemma, in Lambda.TPOSR.Reduction]
commut_red1_subterm [lemma, in Lambda.Reduction]
compute_nf [lemma, in Lambda.TPOSR.Conv_Dec]
compute_nf [lemma, in Lambda.Conv_Dec]
confluence_lred [lemma, in Lambda.TPOSR.Conv]
confluence_par_lred [lemma, in Lambda.TPOSR.Conv]
confluence_par_red [lemma, in Lambda.Conv]
confluence_red [lemma, in Lambda.Conv]
consistency_ind [lemma, in Lambda.JRussell.Basic]
consistent [inductive, in Lambda.JRussell.Types]
consistent_cons [constructor, in Lambda.JRussell.Types]
consistent_nil [constructor, in Lambda.JRussell.Types]
context_validity [lemma, in Lambda.TPOSR.Basic]
conv [inductive, in Lambda.TPOSR.Reduction]
conv [inductive, in Lambda.Reduction]
Conv [library]
Conv [library]
Conversion [library]
conv_coerce [lemma, in Lambda.Russell.Types]
conv_conv_abs [lemma, in Lambda.Reduction]
conv_conv_app [lemma, in Lambda.Reduction]
conv_conv_lift [lemma, in Lambda.Reduction]
conv_conv_llift [lemma, in Lambda.TPOSR.Reduction]
conv_conv_lsubst [lemma, in Lambda.TPOSR.Reduction]
conv_conv_pair [lemma, in Lambda.TPOSR.Reduction]
conv_conv_pair [lemma, in Lambda.Reduction]
conv_conv_pi1 [lemma, in Lambda.Reduction]
conv_conv_pi2 [lemma, in Lambda.Reduction]
conv_conv_prod [lemma, in Lambda.Reduction]
conv_conv_prod [lemma, in Lambda.TPOSR.Reduction]
conv_conv_subset [lemma, in Lambda.Reduction]
conv_conv_subset [lemma, in Lambda.TPOSR.Reduction]
conv_conv_subst [lemma, in Lambda.Reduction]
conv_conv_sum [lemma, in Lambda.TPOSR.Reduction]
conv_conv_sum [lemma, in Lambda.Reduction]
Conv_Dec [library]
Conv_Dec [library]
conv_dom [lemma, in Lambda.Russell.GenerationRange]
conv_dom [lemma, in Lambda.JRussell.GenerationRange]
conv_env [inductive, in Lambda.JRussell.Validity]
conv_env [lemma, in Lambda.TPOSR.CtxConversion]
conv_env_conv_in_env [lemma, in Lambda.JRussell.Validity]
conv_env_full [lemma, in Lambda.TPOSR.UnlabConv]
conv_env_full_cons [lemma, in Lambda.TPOSR.UnlabConv]
conv_env_full_sym [lemma, in Lambda.TPOSR.UnlabConv]
conv_env_hd [constructor, in Lambda.CCSum.SubjectReduction]
conv_env_hd [constructor, in Lambda.JRussell.Validity]
conv_env_hd [constructor, in Lambda.TPOSR.CtxConversion]
conv_env_hd [constructor, in Lambda.JRussell.Conversion]
conv_env_in_env [constructor, in Lambda.TPOSR.UnlabConv]
conv_env_nil [constructor, in Lambda.TPOSR.UnlabConv]
conv_env_tl [constructor, in Lambda.CCSum.SubjectReduction]
conv_env_tl [constructor, in Lambda.JRussell.Conversion]
conv_env_tl [constructor, in Lambda.JRussell.Validity]
conv_env_tl [constructor, in Lambda.TPOSR.CtxConversion]
conv_env_trans [constructor, in Lambda.TPOSR.UnlabConv]
conv_eq [lemma, in Lambda.TPOSR.UnlabConv]
conv_eq2 [lemma, in Lambda.Meta.Russell_TPOSR]
conv_in_env [inductive, in Lambda.CCSum.SubjectReduction]
conv_in_env [inductive, in Lambda.TPOSR.CtxConversion]
conv_in_env [inductive, in Lambda.JRussell.Conversion]
conv_in_env_coerce_in_env [lemma, in Lambda.TPOSR.CtxConversion]
conv_in_env_full [inductive, in Lambda.TPOSR.UnlabConv]
conv_in_env_sym [lemma, in Lambda.TPOSR.CtxConversion]
conv_item [lemma, in Lambda.CCSum.SubjectReduction]
conv_item [lemma, in Lambda.Russell.Coercion]
conv_kind_prop [lemma, in Lambda.Conv]
conv_kind_prop [lemma, in Lambda.TPOSR.Conv]
conv_kind_set [lemma, in Lambda.TPOSR.Conv]
conv_kind_set [lemma, in Lambda.Conv]
conv_prod_abs [lemma, in Lambda.Conv]
conv_prod_pair [lemma, in Lambda.Conv]
conv_prod_subset [lemma, in Lambda.TPOSR.Conv]
conv_prod_subset [lemma, in Lambda.Conv]
conv_prod_sum [lemma, in Lambda.Conv]
conv_prod_sum [lemma, in Lambda.TPOSR.Conv]
conv_ref_prod [lemma, in Lambda.Conv]
conv_ref_subset [lemma, in Lambda.Conv]
conv_ref_sum [lemma, in Lambda.Conv]
conv_russell_jrussell [lemma, in Lambda.Meta.Russell_JRussell]
conv_sort [lemma, in Lambda.TPOSR.Conv]
conv_sort [lemma, in Lambda.Conv]
conv_sort_prod [lemma, in Lambda.TPOSR.Conv]
conv_sort_prod [lemma, in Lambda.Conv]
conv_sort_ref [lemma, in Lambda.Conv]
conv_sort_ref [lemma, in Lambda.TPOSR.Conv]
conv_sort_subset [lemma, in Lambda.Conv]
conv_sort_subset [lemma, in Lambda.TPOSR.Conv]
conv_sort_sum [lemma, in Lambda.TPOSR.Conv]
conv_sort_sum [lemma, in Lambda.Conv]
conv_subset_abs [lemma, in Lambda.Conv]
conv_subset_pair [lemma, in Lambda.Conv]
conv_subset_sum [lemma, in Lambda.Conv]
conv_subset_sum [lemma, in Lambda.TPOSR.Conv]
conv_sum_abs [lemma, in Lambda.Conv]
conv_sum_pair [lemma, in Lambda.Conv]
conv_unlab_conv [lemma, in Lambda.TPOSR.Unlab]
CtxCoercion [library]
CtxConversion [library]
CtxExpansion [library]
CtxReduction [library]
| 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) |