| 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 | _ | other | (1314 entries) |
| Notation 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 | _ | other | (114 entries) |
| Module 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 | _ | other | (4 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 | _ | other | (22 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 | _ | other | (64 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 | _ | other | (615 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 | _ | other | (238 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 | _ | other | (60 entries) |
| Projection 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 | _ | other | (1 entry) |
| 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 | _ | other | (9 entries) |
| Instance 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 | _ | other | (26 entries) |
| Abbreviation 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 | _ | other | (2 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 | _ | other | (158 entries) |
| Record 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 | _ | other | (1 entry) |
Global Index
A
adjust_exp_eq_level [lemma, in Mctt.Core.Semantic.Consequences]app_ctx_vlookup [lemma, in Mctt.Core.Syntactic.Corollaries]
app_ctx_lookup [lemma, in Mctt.Core.Syntactic.Corollaries]
a_extend [constructor, in Mctt.Core.Syntactic.Syntax]
a_compose [constructor, in Mctt.Core.Syntactic.Syntax]
a_weaken [constructor, in Mctt.Core.Syntactic.Syntax]
a_id [constructor, in Mctt.Core.Syntactic.Syntax]
a_sub [constructor, in Mctt.Core.Syntactic.Syntax]
a_var [constructor, in Mctt.Core.Syntactic.Syntax]
a_eqrec [constructor, in Mctt.Core.Syntactic.Syntax]
a_refl [constructor, in Mctt.Core.Syntactic.Syntax]
a_eq [constructor, in Mctt.Core.Syntactic.Syntax]
a_app [constructor, in Mctt.Core.Syntactic.Syntax]
a_fn [constructor, in Mctt.Core.Syntactic.Syntax]
a_pi [constructor, in Mctt.Core.Syntactic.Syntax]
a_natrec [constructor, in Mctt.Core.Syntactic.Syntax]
a_succ [constructor, in Mctt.Core.Syntactic.Syntax]
a_zero [constructor, in Mctt.Core.Syntactic.Syntax]
a_nat [constructor, in Mctt.Core.Syntactic.Syntax]
a_typ [constructor, in Mctt.Core.Syntactic.Syntax]
B
Base [library]C
canonical_form_of_typ [lemma, in Mctt.Core.Semantic.Consequences]canonical_form_of_nat [lemma, in Mctt.Core.Semantic.Consequences]
canonical_nat_sind [definition, in Mctt.Core.Semantic.Consequences]
canonical_nat_ind [definition, in Mctt.Core.Semantic.Consequences]
canonical_nat_succ [constructor, in Mctt.Core.Semantic.Consequences]
canonical_nat_zero [constructor, in Mctt.Core.Semantic.Consequences]
canonical_nat [inductive, in Mctt.Core.Semantic.Consequences]
canonical_form_of_pi [lemma, in Mctt.Core.Semantic.Consequences]
completeness [lemma, in Mctt.Core.Completeness]
Completeness [library]
completeness_fundamental_ctx_eq [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_subtyp [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub_eq [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp_eq [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx_subtyp [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental [lemma, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental [section, in Mctt.Core.Completeness.FundamentalTheorem]
completeness_ty [lemma, in Mctt.Core.Completeness]
Consequences [library]
consistency [lemma, in Mctt.Core.Semantic.Consequences]
consistency_ne_helper [lemma, in Mctt.Core.Semantic.Consequences]
cons_per_ctx_env [inductive, in Mctt.Core.Semantic.PER.Definitions]
cons_glu_sub_pred_helper [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
cons_glu_sub_pred_resp_wf_sub_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
cons_glu_sub_pred_pi_helper [lemma, in Mctt.Core.Soundness.FunctionCases]
cons_glu_sub_pred [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
cons_glu_sub_pred_q_nat_helper [lemma, in Mctt.Core.Soundness.NatCases]
cons_glu_sub_pred_q_helper [lemma, in Mctt.Core.Soundness.NatCases]
cons_glu_sub_pred_nat_helper [lemma, in Mctt.Core.Soundness.NatCases]
ContextCases [library]
ContextCases [library]
Core [library]
CoreInversions [library]
CoreLemmas [library]
CoreTactics [library]
CoreTactics [library]
Corollaries [library]
Cst [module, in Mctt.Core.Syntactic.Syntax]
Cst.app [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.eqrec [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.fn [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.nat [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.natrec [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.obj [inductive, in Mctt.Core.Syntactic.Syntax]
Cst.obj_sind [definition, in Mctt.Core.Syntactic.Syntax]
Cst.obj_rec [definition, in Mctt.Core.Syntactic.Syntax]
Cst.obj_ind [definition, in Mctt.Core.Syntactic.Syntax]
Cst.obj_rect [definition, in Mctt.Core.Syntactic.Syntax]
Cst.pi [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.prop_eq [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.refl [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.succ [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.typ [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.var [constructor, in Mctt.Core.Syntactic.Syntax]
Cst.zero [constructor, in Mctt.Core.Syntactic.Syntax]
ctx [abbreviation, in Mctt.Core.Syntactic.Syntax]
CtxEq [library]
ctxeq_weakening [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
ctxeq_nbe_ty_eq' [lemma, in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_ty_eq [lemma, in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq' [lemma, in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq [lemma, in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_subtyp [lemma, in Mctt.Core.Syntactic.CtxEq]
ctxeq_sub_eq [lemma, in Mctt.Core.Syntactic.CtxEq]
ctxeq_sub [lemma, in Mctt.Core.Syntactic.CtxEq]
ctxeq_exp_eq [lemma, in Mctt.Core.Syntactic.CtxEq]
ctxeq_exp [lemma, in Mctt.Core.Syntactic.CtxEq]
ctxeq_ctx_lookup [lemma, in Mctt.Core.Syntactic.System.Lemmas]
CtxSub [library]
ctxsub_weakening [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
ctxsub_judg.ctxsub_subtyp [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_subtyp_helper [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq_helper [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_helper [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq_helper [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_helper [lemma, in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg [module, in Mctt.Core.Syntactic.CtxSub]
ctx_lookup_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
ctx_lookup_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
ctx_lookup [inductive, in Mctt.Core.Syntactic.System.Definitions]
ctx_lookup_functional [lemma, in Mctt.Core.Syntactic.Corollaries]
ctx_eq_trans [lemma, in Mctt.Core.Syntactic.CtxEq]
ctx_eq_sym [lemma, in Mctt.Core.Syntactic.CtxEq]
ctx_eq_refl [lemma, in Mctt.Core.Syntactic.CtxEq]
ctx_sub_refl [lemma, in Mctt.Core.Syntactic.CtxSub]
ctx_sub_ctx_lookup [lemma, in Mctt.Core.Syntactic.System.Lemmas]
ctx_eq_refl [lemma, in Mctt.Core.Syntactic.System.Lemmas]
ctx_decomp_right [lemma, in Mctt.Core.Syntactic.System.Lemmas]
ctx_decomp_left [lemma, in Mctt.Core.Syntactic.System.Lemmas]
ctx_decomp [lemma, in Mctt.Core.Syntactic.System.Lemmas]
ctx_lookup_lt [lemma, in Mctt.Core.Syntactic.System.Lemmas]
D
Definitions [library]Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
Definitions [library]
domain [inductive, in Mctt.Core.Semantic.Domain]
Domain [library]
domain:_ ↯ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:_ ↦ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:⇑! _ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:⇓ _ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:⇑ _ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:! _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:eqrec _ under _ as Eq _ _ _ return _ | refl -> _ end (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:refl _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:Eq _ _ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:_ _ .. _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:λ _ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:Π _ _ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:rec _ under _ return _ | zero -> _ | succ -> _ end (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:succ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:zero (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:ℕ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:𝕌 @ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:_ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:^ _ (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
domain:( _ ) (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
d{{{ _ }}} (mctt_scope) [notation, in Mctt.Core.Semantic.Domain]
Domain_Notations [module, in Mctt.Core.Semantic.Domain]
domain_nf_sind [definition, in Mctt.Core.Semantic.Domain]
domain_nf_rec [definition, in Mctt.Core.Semantic.Domain]
domain_nf_ind [definition, in Mctt.Core.Semantic.Domain]
domain_nf_rect [definition, in Mctt.Core.Semantic.Domain]
domain_ne_sind [definition, in Mctt.Core.Semantic.Domain]
domain_ne_rec [definition, in Mctt.Core.Semantic.Domain]
domain_ne_ind [definition, in Mctt.Core.Semantic.Domain]
domain_ne_rect [definition, in Mctt.Core.Semantic.Domain]
domain_sind [definition, in Mctt.Core.Semantic.Domain]
domain_rec [definition, in Mctt.Core.Semantic.Domain]
domain_ind [definition, in Mctt.Core.Semantic.Domain]
domain_rect [definition, in Mctt.Core.Semantic.Domain]
domain_nf [inductive, in Mctt.Core.Semantic.Domain]
domain_ne [inductive, in Mctt.Core.Semantic.Domain]
domain_app_per [lemma, in Mctt.Core.Semantic.PER.Lemmas]
drop_env_extend_env_cancel [lemma, in Mctt.Core.Semantic.Domain]
drop_env [definition, in Mctt.Core.Semantic.Domain]
d_dom [constructor, in Mctt.Core.Semantic.Domain]
d_eqrec [constructor, in Mctt.Core.Semantic.Domain]
d_natrec [constructor, in Mctt.Core.Semantic.Domain]
d_app [constructor, in Mctt.Core.Semantic.Domain]
d_var [constructor, in Mctt.Core.Semantic.Domain]
d_neut [constructor, in Mctt.Core.Semantic.Domain]
d_refl [constructor, in Mctt.Core.Semantic.Domain]
d_eq [constructor, in Mctt.Core.Semantic.Domain]
d_fn [constructor, in Mctt.Core.Semantic.Domain]
d_pi [constructor, in Mctt.Core.Semantic.Domain]
d_succ [constructor, in Mctt.Core.Semantic.Domain]
d_zero [constructor, in Mctt.Core.Semantic.Domain]
d_nat [constructor, in Mctt.Core.Semantic.Domain]
d_univ [constructor, in Mctt.Core.Semantic.Domain]
E
empty_env [definition, in Mctt.Core.Semantic.Domain]EqualityCases [library]
EqualityCases [library]
eq_glu_exp_pred [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
eq_glu_typ_pred [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
eq_is_typ_constr [constructor, in Mctt.Core.Completeness.Consequences.Types]
Evaluation [library]
eval_natrec_sub_rel [lemma, in Mctt.Core.Completeness.NatCases]
eval_natrec_rel [lemma, in Mctt.Core.Completeness.NatCases]
eval_natrec_neut [lemma, in Mctt.Core.Completeness.NatCases]
eval_natrec_sub_neut [lemma, in Mctt.Core.Completeness.NatCases]
eval_sub_mut_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_mut_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_mut_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_mut_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_mut_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_sind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_sind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_sind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_sind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_sind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_ind [definition, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_compose [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_extend [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_weaken [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_id [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub [inductive, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_neut [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_refl [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec [inductive, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_neut [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_fn [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app [inductive, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_neut [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_succ [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_zero [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec [inductive, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_sub [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_eqrec [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_refl [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_eq [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_app [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_fn [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_pi [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_natrec [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_succ [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_zero [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_nat [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_var [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_typ [constructor, in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp [inductive, in Mctt.Core.Semantic.Evaluation.Definitions]
exp [inductive, in Mctt.Core.Syntactic.Syntax]
exp_to_num [definition, in Mctt.Core.Syntactic.Syntax]
exp_to_nat [definition, in Mctt.Core.Syntactic.Syntax]
exp_sind [definition, in Mctt.Core.Syntactic.Syntax]
exp_rec [definition, in Mctt.Core.Syntactic.Syntax]
exp_ind [definition, in Mctt.Core.Syntactic.Syntax]
exp_rect [definition, in Mctt.Core.Syntactic.Syntax]
exp_eq_pi_inversion [lemma, in Mctt.Core.Semantic.Consequences]
exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_sub_decompose_double_q_with_id_double_extend [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_eq_var_sub_rhs_typ_gen [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_pi_eta_rhs_body [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_pi_sub_rhs [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_pi_sub_lhs [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_eq_nat_beta_succ_rhs_typ_gen [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_eq_sub_cong_typ2 [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_rhs_typ [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_lhs_typ_gen [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_eq_natrec_cong_rhs_typ [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_succ_sub_rhs [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_succ_sub_lhs [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_zero_sub_lhs [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_nat_sub_lhs [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_typ_sub_lhs [lemma, in Mctt.Core.Syntactic.Corollaries]
exp_eq_typ_implies_eq_level [lemma, in Mctt.Core.Completeness.Consequences.Types]
exp_eq_var_1_sub_q_sigma [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_q_sigma_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_nat_helper [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_id_double_extend_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_double_extend_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_id_extend_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_extend_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub_to_nat_sub [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat2 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat1 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_typ_helper [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_typ_sub_sub [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_id_double_extend_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_double_extend_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_id_extend_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_extend_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ2' [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ1 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_trans_typ_max [lemma, in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_refl [lemma, in Mctt.Core.Syntactic.System.Lemmas]
extend_env [definition, in Mctt.Core.Semantic.Domain]
F
functional_glu_univ_elem [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]functional_nbe_ty [lemma, in Mctt.Core.Semantic.NbE]
functional_nbe_of_typ [lemma, in Mctt.Core.Semantic.NbE]
functional_nbe [lemma, in Mctt.Core.Semantic.NbE]
functional_initial_env [lemma, in Mctt.Core.Semantic.NbE]
functional_eval_sub [lemma, in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_eqrec [lemma, in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_app [lemma, in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_natrec [lemma, in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_exp [lemma, in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval [lemma, in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval [section, in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_glu_ctx_env [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
functional_read_typ [lemma, in Mctt.Core.Semantic.Readback.Lemmas]
functional_read_ne [lemma, in Mctt.Core.Semantic.Readback.Lemmas]
functional_read_nf [lemma, in Mctt.Core.Semantic.Readback.Lemmas]
functional_read [lemma, in Mctt.Core.Semantic.Readback.Lemmas]
functional_read [section, in Mctt.Core.Semantic.Readback.Lemmas]
functional_ctx_lookup [lemma, in Mctt.Core.Syntactic.System.Lemmas]
FunctionCases [library]
FunctionCases [library]
FundamentalTheorem [library]
FundamentalTheorem [library]
G
Gluing [section, in Mctt.Core.Soundness.LogicalRelation.Definitions]GluingInduction [section, in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_neut [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_eq [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_pi [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_nat [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_univ [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.motive [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
Gluing.glu_univ_typ_rec [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
Gluing.i [variable, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_exp_monotone [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_monotone [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_mut_monotone [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_elem [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_univ [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_univ_elem [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_per_nat [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion2 [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion1 [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_simple_constructor [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_core_univ' [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_exp_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_univ_lvl [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_typ [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_elem [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_univ [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_escape [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk' [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_ctx_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_ctx_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_typ_exp_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_exp_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_lvl [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_readback [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_exp_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_ctx_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_escape [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_per_nat [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_rel_eq_eqrec [lemma, in Mctt.Core.Soundness.EqualityCases]
glu_rel_eq_refl [lemma, in Mctt.Core.Soundness.EqualityCases]
glu_rel_eq [lemma, in Mctt.Core.Soundness.EqualityCases]
glu_rel_exp_sub [lemma, in Mctt.Core.Soundness.TermStructureCases]
glu_rel_exp_vlookup [lemma, in Mctt.Core.Soundness.TermStructureCases]
glu_rel_exp_sub_typ [lemma, in Mctt.Core.Soundness.UniverseCases]
glu_rel_exp_clean_inversion2' [lemma, in Mctt.Core.Soundness.UniverseCases]
glu_rel_exp_typ [lemma, in Mctt.Core.Soundness.UniverseCases]
glu_rel_exp_of_typ [lemma, in Mctt.Core.Soundness.UniverseCases]
glu_rel_ctx_extend [lemma, in Mctt.Core.Soundness.ContextCases]
glu_rel_ctx_empty [lemma, in Mctt.Core.Soundness.ContextCases]
glu_rel_sub_conv [lemma, in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_conv [lemma, in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_conv' [lemma, in Mctt.Core.Soundness.SubtypingCases]
glu_rel_sub_subtyp [lemma, in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_subtyp [lemma, in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_preserves_lvl [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_wf_sub [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion3 [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion2 [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion1 [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_to_wf_exp [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion2 [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion1 [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_monotone [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_subtyp_sub_if [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_cons_clean_inversion [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_resp_per_ctx_helper [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_ctx_env [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_escape [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_wf_ctx [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_env [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_sub_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_ctx_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_typ_with_sub [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_exp_sub_with_typ [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_conv [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_if [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_typ_escape [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_conv' [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_conv [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_right [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_left [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_right [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_left [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_ge [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_right [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_left [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_ge [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumulativity_ge [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumulativity [section, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_right [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_left [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_ge [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_iff [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_unique_upto_exp_eq' [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_unique_upto_exp_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_escape [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_elem_typ_escape [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq' [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq_ge [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_app [lemma, in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_app_helper [lemma, in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_fn [lemma, in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_fn_helper [lemma, in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_of_pi [lemma, in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_pi [lemma, in Mctt.Core.Soundness.FunctionCases]
glu_rel_sub [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_sub_resp_sub_env [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp_resp_sub_env [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_ctx [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_sub_with_sub [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp_with_sub [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_sind [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_ind [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_cons [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_nil [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_typ_with_sub [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top_make [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top_make [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot_make [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_ind [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_typ [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_sind [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_ind [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_neut [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_eq [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_pi [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_nat [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_univ [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_eq_neut [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_eq_refl [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_eq [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_sind [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_ind [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_neut [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_succ [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_zero [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp_natrec [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_helper [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_neut_helper [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_succ_helper [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_zero_helper [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_sub_extend_nat [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_succ [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_zero [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_of_nat [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_clean_inversion2'' [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_sub_nat [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_exp_nat [lemma, in Mctt.Core.Soundness.NatCases]
glu_rel_sub_extend [lemma, in Mctt.Core.Soundness.SubstitutionCases]
glu_rel_sub_compose [lemma, in Mctt.Core.Soundness.SubstitutionCases]
glu_rel_sub_weaken [lemma, in Mctt.Core.Soundness.SubstitutionCases]
glu_rel_sub_id [lemma, in Mctt.Core.Soundness.SubstitutionCases]
H
here [constructor, in Mctt.Core.Syntactic.System.Definitions]I
idempotent_nbe_ty [lemma, in Mctt.Core.Semantic.Consequences]id_sub_lookup_var1 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
id_sub_lookup_var0 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
initial_env_spec [lemma, in Mctt.Core.Semantic.NbE]
initial_env_sind [definition, in Mctt.Core.Semantic.NbE]
initial_env_ind [definition, in Mctt.Core.Semantic.NbE]
initial_env_cons [constructor, in Mctt.Core.Semantic.NbE]
initial_env_nil [constructor, in Mctt.Core.Semantic.NbE]
initial_env [inductive, in Mctt.Core.Semantic.NbE]
initial_env_glu_rel_exp [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
invert_compose_id [lemma, in Mctt.Core.Syntactic.Corollaries]
invert_sub_id_typ [lemma, in Mctt.Core.Syntactic.Corollaries]
invert_sub_id [lemma, in Mctt.Core.Syntactic.Corollaries]
is_typ_constr_and_exp_eq_nat_implies_eq_nat [lemma, in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr_and_exp_eq_typ_implies_eq_typ [lemma, in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr_and_exp_eq_var_implies_eq_var [lemma, in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr_sind [definition, in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr_ind [definition, in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr [inductive, in Mctt.Core.Completeness.Consequences.Types]
L
Lemmas [library]Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
Lemmas [library]
LibTactics [library]
lift_nbe_max_right [lemma, in Mctt.Core.Semantic.NbE]
lift_nbe_max_left [lemma, in Mctt.Core.Semantic.NbE]
lift_nbe_ge [lemma, in Mctt.Core.Semantic.NbE]
lift_exp_eq_max_right [lemma, in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_eq_max_left [lemma, in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_eq_ge [lemma, in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_max_right [lemma, in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_max_left [lemma, in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_ge [lemma, in Mctt.Core.Syntactic.System.Lemmas]
LogicalRelation [library]
LogicalRelation [library]
M
mk_cons_per_ctx_env [constructor, in Mctt.Core.Semantic.PER.Definitions]mk_rel_mod_app [constructor, in Mctt.Core.Semantic.PER.Definitions]
mk_rel_mod_eval [constructor, in Mctt.Core.Semantic.PER.Definitions]
mk_glu_rel_exp_with_sub'' [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_exp_with_sub' [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub'' [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub' [lemma, in Mctt.Core.Soundness.LogicalRelation.Lemmas]
mk_rel_sub [constructor, in Mctt.Core.Completeness.LogicalRelation.Definitions]
mk_rel_exp [constructor, in Mctt.Core.Completeness.LogicalRelation.Definitions]
mk_glu_rel_sub_with_sub [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_glu_rel_exp_with_sub [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_cons_glu_sub_pred [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_glu_rel_typ_with_sub [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_eq_glu_exp_pred [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_eq_glu_typ_pred [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_exp_pred [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_typ_pred [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_neut_glu_exp_pred [constructor, in Mctt.Core.Soundness.LogicalRelation.Definitions]
N
NatCases [library]NatCases [library]
nat_to_exp [definition, in Mctt.Core.Syntactic.Syntax]
nat_glu_exp_pred [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
nat_glu_typ_pred [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
nat_is_typ_constr [constructor, in Mctt.Core.Completeness.Consequences.Types]
nbe [inductive, in Mctt.Core.Semantic.NbE]
NbE [library]
nbe_type_to_nbe_ty [lemma, in Mctt.Core.Semantic.NbE]
nbe_ty_sind [definition, in Mctt.Core.Semantic.NbE]
nbe_ty_ind [definition, in Mctt.Core.Semantic.NbE]
nbe_ty_run [constructor, in Mctt.Core.Semantic.NbE]
nbe_ty [inductive, in Mctt.Core.Semantic.NbE]
nbe_cumu [lemma, in Mctt.Core.Semantic.NbE]
nbe_sind [definition, in Mctt.Core.Semantic.NbE]
nbe_ind [definition, in Mctt.Core.Semantic.NbE]
nbe_run [constructor, in Mctt.Core.Semantic.NbE]
ne [inductive, in Mctt.Core.Syntactic.Syntax]
neut_glu_exp_pred [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
neut_glu_typ_pred [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
ne_eq_dec [lemma, in Mctt.Core.Syntactic.Syntax]
ne_to_exp [definition, in Mctt.Core.Syntactic.Syntax]
ne_sind [definition, in Mctt.Core.Syntactic.Syntax]
ne_rec [definition, in Mctt.Core.Syntactic.Syntax]
ne_ind [definition, in Mctt.Core.Syntactic.Syntax]
ne_rect [definition, in Mctt.Core.Syntactic.Syntax]
ne_eqrec [constructor, in Mctt.Core.Syntactic.Syntax]
ne_var [constructor, in Mctt.Core.Syntactic.Syntax]
ne_app [constructor, in Mctt.Core.Syntactic.Syntax]
ne_natrec [constructor, in Mctt.Core.Syntactic.Syntax]
nf [inductive, in Mctt.Core.Syntactic.Syntax]
nf_eq_dec [lemma, in Mctt.Core.Syntactic.Syntax]
nf_to_exp [definition, in Mctt.Core.Syntactic.Syntax]
nf_sind [definition, in Mctt.Core.Syntactic.Syntax]
nf_rec [definition, in Mctt.Core.Syntactic.Syntax]
nf_ind [definition, in Mctt.Core.Syntactic.Syntax]
nf_rect [definition, in Mctt.Core.Syntactic.Syntax]
nf_neut [constructor, in Mctt.Core.Syntactic.Syntax]
nf_refl [constructor, in Mctt.Core.Syntactic.Syntax]
nf_eq [constructor, in Mctt.Core.Syntactic.Syntax]
nf_fn [constructor, in Mctt.Core.Syntactic.Syntax]
nf_pi [constructor, in Mctt.Core.Syntactic.Syntax]
nf_succ [constructor, in Mctt.Core.Syntactic.Syntax]
nf_zero [constructor, in Mctt.Core.Syntactic.Syntax]
nf_nat [constructor, in Mctt.Core.Syntactic.Syntax]
nf_typ [constructor, in Mctt.Core.Syntactic.Syntax]
nf_of_pi [lemma, in Mctt.Core.Semantic.Consequences]
nil_glu_sub_pred [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
no_closed_neutral [lemma, in Mctt.Core.Syntactic.System.Lemmas]
num_to_exp [definition, in Mctt.Core.Syntactic.Syntax]
P
PER [library]PERElem [record, in Mctt.LibTactics]
PERElem [inductive, in Mctt.LibTactics]
PERProper [instance, in Mctt.LibTactics]
per_ctx_then_per_env_initial_env [lemma, in Mctt.Core.Semantic.Realizability]
per_elem_then_per_top [lemma, in Mctt.Core.Semantic.Realizability]
per_bot_then_per_elem [lemma, in Mctt.Core.Semantic.Realizability]
per_univ_then_per_top_typ [lemma, in Mctt.Core.Semantic.Realizability]
per_nat_then_per_top [lemma, in Mctt.Core.Semantic.Realizability]
per_univ_elem_glu_univ_elem [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
per_univ_glu_univ_elem [lemma, in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
per_ctx_subtyp_sind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_ind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_cons [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_subtyp_nil [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_subtyp [inductive, in Mctt.Core.Semantic.PER.Definitions]
per_ctx [definition, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_sind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_ind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_cons [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_nil [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env [inductive, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_sind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_ind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_neut [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_eq [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_pi [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_nat [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_univ [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_subtyp [inductive, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_ind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_ind' [definition, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_ne [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_Eq [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_Pi [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_N [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_U [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.motive [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def [section, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_univ' [lemma, in Mctt.Core.Semantic.PER.Definitions]
per_univ [definition, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem [definition, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_strong_ind [definition, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_ne [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_Eq [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_Pi [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_nat [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_U [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.motive [variable, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_sind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_ind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_neut [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_eq [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_pi [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_nat [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_univ [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core [inductive, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.per_univ_rec [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.i [variable, in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def [section, in Mctt.Core.Semantic.PER.Definitions]
per_ne_neut [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_ne [inductive, in Mctt.Core.Semantic.PER.Definitions]
per_eq_neut [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_eq_refl [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_eq [inductive, in Mctt.Core.Semantic.PER.Definitions]
per_nat_sind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_nat_ind [definition, in Mctt.Core.Semantic.PER.Definitions]
per_nat_neut [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_nat_succ [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_nat_zero [constructor, in Mctt.Core.Semantic.PER.Definitions]
per_nat [inductive, in Mctt.Core.Semantic.PER.Definitions]
per_top_typ [definition, in Mctt.Core.Semantic.PER.Definitions]
per_top [definition, in Mctt.Core.Semantic.PER.Definitions]
per_bot [definition, in Mctt.Core.Semantic.PER.Definitions]
per_elem [projection, in Mctt.LibTactics]
per_elem [constructor, in Mctt.LibTactics]
PER_refl2 [lemma, in Mctt.LibTactics]
PER_refl1 [lemma, in Mctt.LibTactics]
per_ctx_subtyp_trans_ins [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl2 [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl1 [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_subtyping [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_to_env [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_respects_length [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons_clean_inversion [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons' [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_env_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_env_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_cross_irrel [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_left_irrel [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_env_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_right_irrel [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_right [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_left [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_transp [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_trans_ins [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_refl2 [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_refl1 [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_elem_subtyping_gen [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_elem_subtyping [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_to_univ_elem [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_right [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_left [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_ge [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi_clean_inversion [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_eq' [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi' [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_elem_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_PER' [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_elem_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_trans' [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cross_irrel [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_left_irrel [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_elem_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_sym' [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_right_irrel [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ne_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_ne_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_ne_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_eq_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_eq_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_eq_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_nat_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_nat_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_nat_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_top_typ_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_top_typ_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_top_typ_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_bot_then_per_top [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_top_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_top_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_top_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_bot_PER [instance, in Mctt.Core.Semantic.PER.Lemmas]
per_bot_trans [lemma, in Mctt.Core.Semantic.PER.Lemmas]
per_bot_sym [lemma, in Mctt.Core.Semantic.PER.Lemmas]
pi_glu_exp_pred [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
pi_glu_typ_pred [inductive, in Mctt.Core.Soundness.LogicalRelation.Definitions]
pi_is_typ_constr [constructor, in Mctt.Core.Completeness.Consequences.Types]
predicate_implication_equivalence [instance, in Mctt.LibTactics]
Presup [library]
presup_subtyp [lemma, in Mctt.Core.Syntactic.Presup]
presup_sub_eq [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_sub_compose_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_sub_cong_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_var_S_sub_left [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_var_0_sub_left [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_beta_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_cong_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_refl_cong_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_sub_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_sub_left [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_refl_sub_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_id_sub_helper3 [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_typ_id_sub2_eq [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_id_sub_helper2 [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_sub_helper3 [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_typ_sub2_eq [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_sub_helper2 [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_wf [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_var1 [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_var0 [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_pi_eta_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_app_sub_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_app_sub_left [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_app_cong_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_fn_sub_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_fn_cong_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_beta_succ_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_natrec_sub_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_natrec_sub_left [lemma, in Mctt.Core.Syntactic.Presup]
presup_exp_eq_natrec_cong_right [lemma, in Mctt.Core.Syntactic.Presup]
presup_typ_glu_rel_exp [lemma, in Mctt.Core.Soundness.TermStructureCases]
presup_ctx_glu_rel_exp [lemma, in Mctt.Core.Soundness.TermStructureCases]
presup_glu_rel_exp [lemma, in Mctt.Core.Soundness.TermStructureCases]
presup_subtyp_right [lemma, in Mctt.Core.Syntactic.System.Definitions]
presup_ctx_sub_right [lemma, in Mctt.Core.Syntactic.System.Definitions]
presup_ctx_sub_left [lemma, in Mctt.Core.Syntactic.System.Definitions]
presup_ctx_sub [lemma, in Mctt.Core.Syntactic.System.Definitions]
presup_rel_exp [lemma, in Mctt.Core.Completeness.TermStructureCases]
presup_rel_sub [lemma, in Mctt.Core.Completeness.SubstitutionCases]
presup_right_glu_rel_sub [lemma, in Mctt.Core.Soundness.SubstitutionCases]
presup_left_glu_rel_sub [lemma, in Mctt.Core.Soundness.SubstitutionCases]
presup_glu_rel_sub [lemma, in Mctt.Core.Soundness.SubstitutionCases]
presup_exp [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_exp_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_lookup_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_exp_eq_ctx [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_right [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_left [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_exp_ctx [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_right [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_left [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_sub [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_right [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_left [lemma, in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_eq [lemma, in Mctt.Core.Syntactic.System.Lemmas]
Q
q [definition, in Mctt.Core.Syntactic.Syntax]R
Readback [library]read_typ_mut_ind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_ne_mut_ind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_mut_ind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_typ_sind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_typ_ind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_ne_sind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_ne_ind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_sind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_ind [definition, in Mctt.Core.Semantic.Readback.Definitions]
read_typ_neut [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_typ_eq [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_typ_pi [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_typ_nat [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_typ_univ [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_typ [inductive, in Mctt.Core.Semantic.Readback.Definitions]
read_ne_eqrec [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_ne_app [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_ne_natrec [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_ne_var [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_ne [inductive, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_neut [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_eq_neut [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_refl [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_fn [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_nat_neut [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_succ [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_zero [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf_type [constructor, in Mctt.Core.Semantic.Readback.Definitions]
read_nf [inductive, in Mctt.Core.Semantic.Readback.Definitions]
Realizability [library]
Realizability [library]
realize_per_univ_elem_gen [lemma, in Mctt.Core.Semantic.Realizability]
realize_glu_elem_top [lemma, in Mctt.Core.Soundness.Realizability]
realize_glu_elem_bot [lemma, in Mctt.Core.Soundness.Realizability]
realize_glu_typ_top [lemma, in Mctt.Core.Soundness.Realizability]
realize_glu_univ_elem_gen [lemma, in Mctt.Core.Soundness.Realizability]
rel_exp_cumu [lemma, in Mctt.Core.Completeness.UniverseCases]
rel_exp_typ_sub [lemma, in Mctt.Core.Completeness.UniverseCases]
rel_exp_of_typ [lemma, in Mctt.Core.Completeness.UniverseCases]
rel_exp_under_ctx_implies_rel_typ_under_ctx [lemma, in Mctt.Core.Completeness.UniverseCases]
rel_exp_of_typ_inversion2 [lemma, in Mctt.Core.Completeness.UniverseCases]
rel_exp_of_typ_inversion1 [lemma, in Mctt.Core.Completeness.UniverseCases]
rel_typ [definition, in Mctt.Core.Semantic.PER.Definitions]
rel_mod_app [inductive, in Mctt.Core.Semantic.PER.Definitions]
rel_mod_eval [inductive, in Mctt.Core.Semantic.PER.Definitions]
rel_exp_nat_beta_succ [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_nat_beta_succ_rel_typ [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_nat_beta_zero [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_sub [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_sub_rel_typ [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_cong [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_cong_rel_typ [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_id_N [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_wkwk_succ_var1_inversion [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero_inversion [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_succ_cong [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_succ_sub [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_zero_sub [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_nat_sub [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_of_nat [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_of_nat_inversion [lemma, in Mctt.Core.Completeness.NatCases]
rel_exp_var_weaken [lemma, in Mctt.Core.Completeness.VariableCases]
rel_exp_var_S_sub [lemma, in Mctt.Core.Completeness.VariableCases]
rel_exp_var_0_sub [lemma, in Mctt.Core.Completeness.VariableCases]
rel_ctx_sub_extend [lemma, in Mctt.Core.Completeness.ContextCases]
rel_ctx_sub_empty [lemma, in Mctt.Core.Completeness.ContextCases]
rel_ctx_extend' [lemma, in Mctt.Core.Completeness.ContextCases]
rel_ctx_extend [lemma, in Mctt.Core.Completeness.ContextCases]
rel_sub_under_ctx [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_sind [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_ind [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_sub [inductive, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_under_ctx [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_sind [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_ind [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp [inductive, in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_eq_subtyp [lemma, in Mctt.Core.Completeness.TermStructureCases]
rel_exp_PER [instance, in Mctt.Core.Completeness.TermStructureCases]
rel_exp_trans [lemma, in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sym [lemma, in Mctt.Core.Completeness.TermStructureCases]
rel_exp_conv [lemma, in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sub_compose [lemma, in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sub_id [lemma, in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sub_cong [lemma, in Mctt.Core.Completeness.TermStructureCases]
rel_sub_eq_subtyp [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_conv [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_PER [instance, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_trans [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_sym [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_extend [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_p_extend [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_extend_compose [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_compose_assoc [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_left [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_right [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_extend_cong [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_compose_cong [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_weaken [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_id [lemma, in Mctt.Core.Completeness.SubstitutionCases]
rel_exp_eqrec_beta [lemma, in Mctt.Core.Completeness.EqualityCases]
rel_exp_eqrec_cong [lemma, in Mctt.Core.Completeness.EqualityCases]
rel_exp_eqrec_sub [lemma, in Mctt.Core.Completeness.EqualityCases]
rel_exp_refl_sub [lemma, in Mctt.Core.Completeness.EqualityCases]
rel_exp_eq_sub [lemma, in Mctt.Core.Completeness.EqualityCases]
rel_exp_refl_cong [lemma, in Mctt.Core.Completeness.EqualityCases]
rel_exp_eq_cong [lemma, in Mctt.Core.Completeness.EqualityCases]
rel_exp_pi_eta [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_beta [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_app_sub [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_app_cong [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_fn_sub [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_fn_cong [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_sub [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_cong [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_core [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_of_pi [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_of_pi_inversion [lemma, in Mctt.Core.Completeness.FunctionCases]
rel_exp_clean_inversion [lemma, in Mctt.Core.Completeness.LogicalRelation.Lemmas]
rel_typ_implies_rel_exp [lemma, in Mctt.Core.Completeness.LogicalRelation.Lemmas]
rel_exp_implies_rel_typ [lemma, in Mctt.Core.Completeness.LogicalRelation.Lemmas]
Rules [library]
S
soundness [lemma, in Mctt.Core.Soundness]Soundness [library]
soundness_fundamental_sub [lemma, in Mctt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_exp [lemma, in Mctt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_ctx [lemma, in Mctt.Core.Soundness.FundamentalTheorem]
soundness_fundamental [lemma, in Mctt.Core.Soundness.FundamentalTheorem]
soundness_fundamental [section, in Mctt.Core.Soundness.FundamentalTheorem]
soundness_ty' [lemma, in Mctt.Core.Soundness]
soundness_ty [lemma, in Mctt.Core.Soundness]
soundness' [lemma, in Mctt.Core.Soundness]
sub [inductive, in Mctt.Core.Syntactic.Syntax]
SubstitutionCases [library]
SubstitutionCases [library]
SubtypingCases [library]
SubtypingCases [library]
subtyp_pi [lemma, in Mctt.Core.Completeness.SubtypingCases]
subtyp_univ [lemma, in Mctt.Core.Completeness.SubtypingCases]
subtyp_Transitive [instance, in Mctt.Core.Completeness.SubtypingCases]
subtyp_trans [lemma, in Mctt.Core.Completeness.SubtypingCases]
subtyp_refl [lemma, in Mctt.Core.Completeness.SubtypingCases]
subtyp_under_ctx [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
subtyp_spec [lemma, in Mctt.Core.Semantic.Consequences]
sub_sind [definition, in Mctt.Core.Syntactic.Syntax]
sub_rec [definition, in Mctt.Core.Syntactic.Syntax]
sub_ind [definition, in Mctt.Core.Syntactic.Syntax]
sub_rect [definition, in Mctt.Core.Syntactic.Syntax]
sub_eq_q_compose_nat [lemma, in Mctt.Core.Syntactic.Corollaries]
sub_eq_q_compose [lemma, in Mctt.Core.Syntactic.Corollaries]
sub_eq_p_q_sigma_compose_tau_extend [lemma, in Mctt.Core.Syntactic.Corollaries]
sub_decompose_q_typ [lemma, in Mctt.Core.Syntactic.Corollaries]
sub_decompose_q [lemma, in Mctt.Core.Syntactic.Corollaries]
sub_q_eq [lemma, in Mctt.Core.Syntactic.Corollaries]
sub_id_typ [lemma, in Mctt.Core.Syntactic.Corollaries]
sub_lookup_var1 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_lookup_var0 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_p_q_q_sigma_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_q_sigma_id_extend [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_sigma_compose_weak_id_extend [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_compose_sigma [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_nat_compose_sigma [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_weak_compose_weak_extend_succ_var_1 [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_id_extend_zero [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_q_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_q_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_q [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_id_extend [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_cong [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_on_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_id_extend [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_id_on_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_weaken_var0_id [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_extend_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_extend_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_refl [lemma, in Mctt.Core.Syntactic.System.Lemmas]
Syntax [library]
nf:⇑ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:# _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:eqrec _ as Eq _ _ _ return _ | refl -> _ end (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:refl _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:Eq _ _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:_ _ .. _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:λ _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:Π _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:rec _ return _ | zero -> _ | succ -> _ end (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:succ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:zero (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:ℕ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:Type @ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:_ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:^ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
nf:( _ ) (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
n{{{ _ }}} (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:_ , _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:⋅ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:q _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:_ ,, _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:_ ∘ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:Wk (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:Id (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:# _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:eqrec _ as Eq _ _ _ return _ | refl -> _ end (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:refl _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:Eq _ _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:_ _ .. _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:λ _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:Π _ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:rec _ return _ | zero -> _ | succ -> _ end (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:succ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:zero (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:ℕ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:Type @ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:_ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:^ _ (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:( _ ) (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
{{{ _ }}} (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mctt_scope) [notation, in Mctt.Core.Syntactic.Syntax]
Syntax_Notations [module, in Mctt.Core.Syntactic.Syntax]
System [library]
SystemOpt [library]
T
Tactics [library]Tactics [library]
Tactics [library]
TermStructureCases [library]
TermStructureCases [library]
there [constructor, in Mctt.Core.Syntactic.System.Definitions]
typ [abbreviation, in Mctt.Core.Syntactic.Syntax]
Types [library]
typ_is_typ_constr [constructor, in Mctt.Core.Completeness.Consequences.Types]
U
UniverseCases [library]UniverseCases [library]
univ_glu_exp_pred [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
univ_glu_exp_pred' [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
univ_glu_typ_pred [definition, in Mctt.Core.Soundness.LogicalRelation.Definitions]
V
valid_exp_typ [lemma, in Mctt.Core.Completeness.UniverseCases]valid_ctx [definition, in Mctt.Core.Semantic.PER.Definitions]
valid_exp_zero [lemma, in Mctt.Core.Completeness.NatCases]
valid_exp_nat [lemma, in Mctt.Core.Completeness.NatCases]
valid_exp_var [lemma, in Mctt.Core.Completeness.VariableCases]
valid_lookup [lemma, in Mctt.Core.Completeness.VariableCases]
valid_ctx_empty [lemma, in Mctt.Core.Completeness.ContextCases]
valid_sub_under_ctx [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
valid_exp_under_ctx [definition, in Mctt.Core.Completeness.LogicalRelation.Definitions]
valid_exp_eq [lemma, in Mctt.Core.Completeness.EqualityCases]
VariableCases [library]
var_per_elem [lemma, in Mctt.Core.Semantic.Realizability]
var_per_bot [lemma, in Mctt.Core.Semantic.PER.Lemmas]
var_glu_elem_bot [lemma, in Mctt.Core.Soundness.Realizability]
var_weaken_gen [lemma, in Mctt.Core.Soundness.Realizability]
var_arith [lemma, in Mctt.Core.Soundness.Realizability]
var_is_typ_constr [constructor, in Mctt.Core.Completeness.Consequences.Types]
var_compose_subs [lemma, in Mctt.Core.Syntactic.System.Lemmas]
var0_glu_elem [lemma, in Mctt.Core.Soundness.Realizability]
vlookup_1_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
vlookup_0_nat [lemma, in Mctt.Core.Syntactic.System.Lemmas]
vlookup_1_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
vlookup_0_typ [lemma, in Mctt.Core.Syntactic.System.Lemmas]
W
weakening [inductive, in Mctt.Core.Soundness.Weakening.Definitions]weakening_wk [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_id [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_compose [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_conv [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_resp_equiv [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_escape [lemma, in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_sind [definition, in Mctt.Core.Soundness.Weakening.Definitions]
weakening_ind [definition, in Mctt.Core.Soundness.Weakening.Definitions]
wf_exp_eq_refl_sub' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_subtyp_pi' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_eta' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_beta' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_sub' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_cong' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_sub' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_cong' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong_max [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_sub_max [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_succ' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_zero' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_sub' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_cong' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_sub' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_typ_sub' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_app' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_fn' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_pi_max [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_natrec' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_nat' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_ctx_eq_extend' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_conv' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_conv' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_subtyp_refl' [lemma, in Mctt.Core.Syntactic.SystemOpt]
wf_sub_eq_per_elem [instance, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_per_elem [instance, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_subtyp' [lemma, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp' [lemma, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_subtyp' [lemma, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_subtyp' [lemma, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_Transitive [instance, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq_Symmetric [instance, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_PER [instance, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_PER [instance, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq_extend [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq_empty [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind' [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind' [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind' [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_mut_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_mut_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_mut_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_mut_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_ind [definition, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_pi [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_univ [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_trans [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_refl [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_subtyp [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_trans [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_sym [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_p_extend [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_compose [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_assoc [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_left [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_right [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_weaken [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_id [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_trans [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sym [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_compose [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_id [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_weaken [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_S_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_0_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eqrec_beta [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eqrec_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_refl_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eq_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eqrec_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_refl_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eq_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_eta [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_beta [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_succ [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_zero [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_cong [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_zero_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_typ_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_subtyp [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_extend [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_compose [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_weaken [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub_id [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_sub [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_subtyp [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp_sub [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_eqrec [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_refl [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_eq [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_vlookup [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_app [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_fn [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_pi [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_natrec [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_succ [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_zero [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_nat [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_typ [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_exp [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_extend [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_empty [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_extend [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_empty [constructor, in Mctt.Core.Syntactic.System.Definitions]
wf_ctx [inductive, in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_subst [lemma, in Mctt.Core.Syntactic.Corollaries]
wf_subtyp_subst_eq [lemma, in Mctt.Core.Syntactic.Corollaries]
wf_ctx_sub_length [lemma, in Mctt.Core.Syntactic.Corollaries]
wf_ctx_PER [instance, in Mctt.Core.Syntactic.CtxEq]
wf_sub_extend_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_sub_compose_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_sub_weaken_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_sub_id_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_exp_sub_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_vlookup_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_app_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_fn_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_pi_inversion' [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_pi_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_natrec_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_succ_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_zero_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_nat_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_typ_inversion [lemma, in Mctt.Core.Syntactic.CoreInversions]
wf_ctx_sub_ctx_lookup [lemma, in Mctt.Core.Soundness.Realizability]
wf_ctx_sub_trans_ins [instance, in Mctt.Core.Syntactic.CtxSub]
wf_ctx_sub_trans [lemma, in Mctt.Core.Syntactic.CtxSub]
wf_subtyp_univ_weaken [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_subtyp_sub [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_subtyp_ge [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_subtyp_refl [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_sub_eq_conv [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_exp_eq_conv [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_sub_conv [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_conv [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_ctx_sub_refl [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_exp_eq_cumu [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wf_cumu [lemma, in Mctt.Core.Syntactic.System.Lemmas]
wk_p [constructor, in Mctt.Core.Soundness.Weakening.Definitions]
wk_id [constructor, in Mctt.Core.Soundness.Weakening.Definitions]
_
__mark__ [definition, in Mctt.LibTactics]other
judg:SubE _ <: _ (type_scope) [notation, in Mctt.Core.Semantic.PER.Definitions]judg:Sub _ <: _ at _ (type_scope) [notation, in Mctt.Core.Semantic.PER.Definitions]
judg:Rtyp _ in _ ↘ _ (type_scope) [notation, in Mctt.Core.Semantic.Readback.Definitions]
judg:Rne _ in _ ↘ _ (type_scope) [notation, in Mctt.Core.Semantic.Readback.Definitions]
judg:Rnf _ in _ ↘ _ (type_scope) [notation, in Mctt.Core.Semantic.Readback.Definitions]
judg:⊢ _ ≈ _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ ⊆ _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ ≈ _ : _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ ≈ _ : _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ : _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ : _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:⊢ _ ⊆ _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:⊢ _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:# _ : _ ∈ _ (type_scope) [notation, in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢w _ : _ (type_scope) [notation, in Mctt.Core.Soundness.Weakening.Definitions]
judg:_ ⊨s _ : _ [notation, in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨s _ ≈ _ : _ [notation, in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ : _ [notation, in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ⊆ _ [notation, in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ≈ _ : _ [notation, in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊩s _ : _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊩ _ : _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢s _ ® _ ∈ _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ : _ ® _ ∈ _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ ® _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:DF _ ≈ _ ∈ _ ↘ _ [notation, in Mctt.Core.Semantic.PER.Definitions]
judg:DG _ ∈ _ ↘ _ ↘ _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:Dom _ ≈ _ ∈ _ [notation, in Mctt.Core.Semantic.PER.Definitions]
judg:EF _ ≈ _ ∈ _ ↘ _ [notation, in Mctt.Core.Semantic.PER.Definitions]
judg:EG _ ∈ _ ↘ _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:eqrec _ as Eq _ _ _ ⟦return _ | refl -> _ end⟧ _ ↘ _ [notation, in Mctt.Core.Semantic.Evaluation.Definitions]
judg:Exp _ ≈ _ ∈ _ [notation, in Mctt.Core.Semantic.PER.Definitions]
judg:rec _ ⟦return _ | zero -> _ | succ -> _ end⟧ _ ↘ _ [notation, in Mctt.Core.Semantic.Evaluation.Definitions]
judg:$| _ & _ |↘ _ [notation, in Mctt.Core.Semantic.Evaluation.Definitions]
judg:⊨ _ [notation, in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:⊨ _ ≈ _ [notation, in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:⊩ _ [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:⟦ _ ⟧s _ ↘ _ [notation, in Mctt.Core.Semantic.Evaluation.Definitions]
judg:⟦ _ ⟧ _ ↘ _ [notation, in Mctt.Core.Semantic.Evaluation.Definitions]
_ <~> _ [notation, in Mctt.Core.Semantic.PER.Definitions]
_ ~> _ [notation, in Mctt.Core.Semantic.PER.Definitions]
env [notation, in Mctt.Core.Semantic.Domain]
glu_sub_pred_equivalence [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred_args [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_equivalence [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_args [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_equivalence [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_args [notation, in Mctt.Core.Soundness.LogicalRelation.Definitions]
{{ _ }} [notation, in Mctt.Core.Base]
Notation Index
D
domain:_ ↯ (mctt_scope) [in Mctt.Core.Semantic.Domain]domain:_ ↦ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:⇑! _ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:⇓ _ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:⇑ _ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:! _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:eqrec _ under _ as Eq _ _ _ return _ | refl -> _ end (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:refl _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:Eq _ _ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:_ _ .. _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:λ _ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:Π _ _ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:rec _ under _ return _ | zero -> _ | succ -> _ end (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:succ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:zero (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:ℕ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:𝕌 @ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:_ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:^ _ (mctt_scope) [in Mctt.Core.Semantic.Domain]
domain:( _ ) (mctt_scope) [in Mctt.Core.Semantic.Domain]
d{{{ _ }}} (mctt_scope) [in Mctt.Core.Semantic.Domain]
S
nf:⇑ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]nf:# _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:eqrec _ as Eq _ _ _ return _ | refl -> _ end (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:refl _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:Eq _ _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:_ _ .. _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:λ _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:Π _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:rec _ return _ | zero -> _ | succ -> _ end (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:succ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:zero (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:ℕ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:Type @ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:_ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:^ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
nf:( _ ) (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
n{{{ _ }}} (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:_ , _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:⋅ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:q _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:_ ,, _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:_ ∘ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:Wk (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:Id (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:# _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:eqrec _ as Eq _ _ _ return _ | refl -> _ end (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:refl _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:Eq _ _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:_ _ .. _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:λ _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:Π _ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:rec _ return _ | zero -> _ | succ -> _ end (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:succ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:zero (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:ℕ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:Type @ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:_ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:^ _ (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:( _ ) (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
{{{ _ }}} (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
exp:_ [ _ ] (mctt_scope) [in Mctt.Core.Syntactic.Syntax]
other
judg:SubE _ <: _ (type_scope) [in Mctt.Core.Semantic.PER.Definitions]judg:Sub _ <: _ at _ (type_scope) [in Mctt.Core.Semantic.PER.Definitions]
judg:Rtyp _ in _ ↘ _ (type_scope) [in Mctt.Core.Semantic.Readback.Definitions]
judg:Rne _ in _ ↘ _ (type_scope) [in Mctt.Core.Semantic.Readback.Definitions]
judg:Rnf _ in _ ↘ _ (type_scope) [in Mctt.Core.Semantic.Readback.Definitions]
judg:⊢ _ ≈ _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ ⊆ _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ ≈ _ : _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ ≈ _ : _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢s _ : _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢ _ : _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:⊢ _ ⊆ _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:⊢ _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:# _ : _ ∈ _ (type_scope) [in Mctt.Core.Syntactic.System.Definitions]
judg:_ ⊢w _ : _ (type_scope) [in Mctt.Core.Soundness.Weakening.Definitions]
judg:_ ⊨s _ : _ [in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨s _ ≈ _ : _ [in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ : _ [in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ⊆ _ [in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊨ _ ≈ _ : _ [in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:_ ⊩s _ : _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊩ _ : _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢s _ ® _ ∈ _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ : _ ® _ ∈ _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:_ ⊢ _ ® _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:DF _ ≈ _ ∈ _ ↘ _ [in Mctt.Core.Semantic.PER.Definitions]
judg:DG _ ∈ _ ↘ _ ↘ _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:Dom _ ≈ _ ∈ _ [in Mctt.Core.Semantic.PER.Definitions]
judg:EF _ ≈ _ ∈ _ ↘ _ [in Mctt.Core.Semantic.PER.Definitions]
judg:EG _ ∈ _ ↘ _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:eqrec _ as Eq _ _ _ ⟦return _ | refl -> _ end⟧ _ ↘ _ [in Mctt.Core.Semantic.Evaluation.Definitions]
judg:Exp _ ≈ _ ∈ _ [in Mctt.Core.Semantic.PER.Definitions]
judg:rec _ ⟦return _ | zero -> _ | succ -> _ end⟧ _ ↘ _ [in Mctt.Core.Semantic.Evaluation.Definitions]
judg:$| _ & _ |↘ _ [in Mctt.Core.Semantic.Evaluation.Definitions]
judg:⊨ _ [in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:⊨ _ ≈ _ [in Mctt.Core.Completeness.LogicalRelation.Definitions]
judg:⊩ _ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
judg:⟦ _ ⟧s _ ↘ _ [in Mctt.Core.Semantic.Evaluation.Definitions]
judg:⟦ _ ⟧ _ ↘ _ [in Mctt.Core.Semantic.Evaluation.Definitions]
_ <~> _ [in Mctt.Core.Semantic.PER.Definitions]
_ ~> _ [in Mctt.Core.Semantic.PER.Definitions]
env [in Mctt.Core.Semantic.Domain]
glu_sub_pred_equivalence [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_sub_pred_args [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_equivalence [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_exp_pred_args [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_equivalence [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_pred_args [in Mctt.Core.Soundness.LogicalRelation.Definitions]
{{ _ }} [in Mctt.Core.Base]
Module Index
C
Cst [in Mctt.Core.Syntactic.Syntax]ctxsub_judg [in Mctt.Core.Syntactic.CtxSub]
D
Domain_Notations [in Mctt.Core.Semantic.Domain]S
Syntax_Notations [in Mctt.Core.Syntactic.Syntax]Variable Index
G
GluingInduction.case_neut [in Mctt.Core.Soundness.LogicalRelation.Definitions]GluingInduction.case_eq [in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_pi [in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_nat [in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.case_univ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
GluingInduction.motive [in Mctt.Core.Soundness.LogicalRelation.Definitions]
Gluing.glu_univ_typ_rec [in Mctt.Core.Soundness.LogicalRelation.Definitions]
Gluing.i [in Mctt.Core.Soundness.LogicalRelation.Definitions]
P
Per_univ_elem_ind_def.case_ne [in Mctt.Core.Semantic.PER.Definitions]Per_univ_elem_ind_def.case_Eq [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_Pi [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_N [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.case_U [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_ind_def.motive [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_ne [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_Eq [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_Pi [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_nat [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.case_U [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.motive [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.per_univ_rec [in Mctt.Core.Semantic.PER.Definitions]
Per_univ_elem_core_def.i [in Mctt.Core.Semantic.PER.Definitions]
Library Index
B
BaseC
CompletenessConsequences
ContextCases
ContextCases
Core
CoreInversions
CoreLemmas
CoreTactics
CoreTactics
Corollaries
CtxEq
CtxSub
D
DefinitionsDefinitions
Definitions
Definitions
Definitions
Definitions
Definitions
Domain
E
EqualityCasesEqualityCases
Evaluation
F
FunctionCasesFunctionCases
FundamentalTheorem
FundamentalTheorem
L
LemmasLemmas
Lemmas
Lemmas
Lemmas
Lemmas
Lemmas
LibTactics
LogicalRelation
LogicalRelation
N
NatCasesNatCases
NbE
P
PERPresup
R
ReadbackRealizability
Realizability
Rules
S
SoundnessSubstitutionCases
SubstitutionCases
SubtypingCases
SubtypingCases
Syntax
System
SystemOpt
T
TacticsTactics
Tactics
TermStructureCases
TermStructureCases
Types
U
UniverseCasesUniverseCases
V
VariableCasesLemma Index
A
adjust_exp_eq_level [in Mctt.Core.Semantic.Consequences]app_ctx_vlookup [in Mctt.Core.Syntactic.Corollaries]
app_ctx_lookup [in Mctt.Core.Syntactic.Corollaries]
C
canonical_form_of_typ [in Mctt.Core.Semantic.Consequences]canonical_form_of_nat [in Mctt.Core.Semantic.Consequences]
canonical_form_of_pi [in Mctt.Core.Semantic.Consequences]
completeness [in Mctt.Core.Completeness]
completeness_fundamental_ctx_eq [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_subtyp [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub_eq [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_sub [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp_eq [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_exp [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx_subtyp [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental_ctx [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_fundamental [in Mctt.Core.Completeness.FundamentalTheorem]
completeness_ty [in Mctt.Core.Completeness]
consistency [in Mctt.Core.Semantic.Consequences]
consistency_ne_helper [in Mctt.Core.Semantic.Consequences]
cons_glu_sub_pred_helper [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
cons_glu_sub_pred_resp_wf_sub_eq [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
cons_glu_sub_pred_pi_helper [in Mctt.Core.Soundness.FunctionCases]
cons_glu_sub_pred_q_nat_helper [in Mctt.Core.Soundness.NatCases]
cons_glu_sub_pred_q_helper [in Mctt.Core.Soundness.NatCases]
cons_glu_sub_pred_nat_helper [in Mctt.Core.Soundness.NatCases]
ctxeq_weakening [in Mctt.Core.Soundness.Weakening.Lemmas]
ctxeq_nbe_ty_eq' [in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_ty_eq [in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq' [in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_nbe_eq [in Mctt.Core.Completeness.Consequences.Rules]
ctxeq_subtyp [in Mctt.Core.Syntactic.CtxEq]
ctxeq_sub_eq [in Mctt.Core.Syntactic.CtxEq]
ctxeq_sub [in Mctt.Core.Syntactic.CtxEq]
ctxeq_exp_eq [in Mctt.Core.Syntactic.CtxEq]
ctxeq_exp [in Mctt.Core.Syntactic.CtxEq]
ctxeq_ctx_lookup [in Mctt.Core.Syntactic.System.Lemmas]
ctxsub_weakening [in Mctt.Core.Soundness.Weakening.Lemmas]
ctxsub_judg.ctxsub_subtyp [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_subtyp_helper [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_eq_helper [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_sub_helper [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_eq_helper [in Mctt.Core.Syntactic.CtxSub]
ctxsub_judg.ctxsub_exp_helper [in Mctt.Core.Syntactic.CtxSub]
ctx_lookup_functional [in Mctt.Core.Syntactic.Corollaries]
ctx_eq_trans [in Mctt.Core.Syntactic.CtxEq]
ctx_eq_sym [in Mctt.Core.Syntactic.CtxEq]
ctx_eq_refl [in Mctt.Core.Syntactic.CtxEq]
ctx_sub_refl [in Mctt.Core.Syntactic.CtxSub]
ctx_sub_ctx_lookup [in Mctt.Core.Syntactic.System.Lemmas]
ctx_eq_refl [in Mctt.Core.Syntactic.System.Lemmas]
ctx_decomp_right [in Mctt.Core.Syntactic.System.Lemmas]
ctx_decomp_left [in Mctt.Core.Syntactic.System.Lemmas]
ctx_decomp [in Mctt.Core.Syntactic.System.Lemmas]
ctx_lookup_lt [in Mctt.Core.Syntactic.System.Lemmas]
D
domain_app_per [in Mctt.Core.Semantic.PER.Lemmas]drop_env_extend_env_cancel [in Mctt.Core.Semantic.Domain]
E
eval_natrec_sub_rel [in Mctt.Core.Completeness.NatCases]eval_natrec_rel [in Mctt.Core.Completeness.NatCases]
eval_natrec_neut [in Mctt.Core.Completeness.NatCases]
eval_natrec_sub_neut [in Mctt.Core.Completeness.NatCases]
exp_eq_pi_inversion [in Mctt.Core.Semantic.Consequences]
exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 [in Mctt.Core.Syntactic.Corollaries]
exp_sub_decompose_double_q_with_id_double_extend [in Mctt.Core.Syntactic.Corollaries]
exp_eq_var_sub_rhs_typ_gen [in Mctt.Core.Syntactic.Corollaries]
exp_pi_eta_rhs_body [in Mctt.Core.Syntactic.Corollaries]
exp_pi_sub_rhs [in Mctt.Core.Syntactic.Corollaries]
exp_pi_sub_lhs [in Mctt.Core.Syntactic.Corollaries]
exp_eq_nat_beta_succ_rhs_typ_gen [in Mctt.Core.Syntactic.Corollaries]
exp_eq_sub_cong_typ2 [in Mctt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_rhs_typ [in Mctt.Core.Syntactic.Corollaries]
exp_eq_elim_sub_lhs_typ_gen [in Mctt.Core.Syntactic.Corollaries]
exp_eq_natrec_cong_rhs_typ [in Mctt.Core.Syntactic.Corollaries]
exp_succ_sub_rhs [in Mctt.Core.Syntactic.Corollaries]
exp_succ_sub_lhs [in Mctt.Core.Syntactic.Corollaries]
exp_zero_sub_lhs [in Mctt.Core.Syntactic.Corollaries]
exp_nat_sub_lhs [in Mctt.Core.Syntactic.Corollaries]
exp_typ_sub_lhs [in Mctt.Core.Syntactic.Corollaries]
exp_eq_typ_implies_eq_level [in Mctt.Core.Completeness.Consequences.Types]
exp_eq_var_1_sub_q_sigma [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_q_sigma_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_nat_helper [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_id_double_extend_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_double_extend_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_id_extend_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_extend_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub_to_nat_sub [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_nat_sub_sub [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat2 [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_nat1 [in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_nat [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_sub_compose_cong_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_weaken_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_1_sub_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_var_0_sub_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_typ_helper [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_typ_sub_sub [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_id_double_extend_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_double_weaken_double_extend_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_id_extend_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_weaken_extend_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_compose_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ2' [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_sub_cong_typ1 [in Mctt.Core.Syntactic.System.Lemmas]
exp_sub_typ [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_trans_typ_max [in Mctt.Core.Syntactic.System.Lemmas]
exp_eq_refl [in Mctt.Core.Syntactic.System.Lemmas]
F
functional_glu_univ_elem [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]functional_nbe_ty [in Mctt.Core.Semantic.NbE]
functional_nbe_of_typ [in Mctt.Core.Semantic.NbE]
functional_nbe [in Mctt.Core.Semantic.NbE]
functional_initial_env [in Mctt.Core.Semantic.NbE]
functional_eval_sub [in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_eqrec [in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_app [in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_natrec [in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval_exp [in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_eval [in Mctt.Core.Semantic.Evaluation.Lemmas]
functional_glu_ctx_env [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
functional_read_typ [in Mctt.Core.Semantic.Readback.Lemmas]
functional_read_ne [in Mctt.Core.Semantic.Readback.Lemmas]
functional_read_nf [in Mctt.Core.Semantic.Readback.Lemmas]
functional_read [in Mctt.Core.Semantic.Readback.Lemmas]
functional_ctx_lookup [in Mctt.Core.Syntactic.System.Lemmas]
G
glu_univ_elem_exp_monotone [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]glu_univ_elem_typ_monotone [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_mut_monotone [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_elem [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_univ [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_resp_per_univ_elem [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_per_nat [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion2 [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_pi_clean_inversion1 [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_simple_constructor [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_core_univ' [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_exp_eq [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_univ_lvl [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_typ [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_elem [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_per_univ [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_escape [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_wk' [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_ctx_eq [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_ctx_eq [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_trm_resp_typ_exp_eq [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_typ_resp_exp_eq [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_univ_elem_univ_lvl [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_readback [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_exp_eq [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_resp_ctx_eq [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_escape [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_nat_per_nat [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
glu_rel_eq_eqrec [in Mctt.Core.Soundness.EqualityCases]
glu_rel_eq_refl [in Mctt.Core.Soundness.EqualityCases]
glu_rel_eq [in Mctt.Core.Soundness.EqualityCases]
glu_rel_exp_sub [in Mctt.Core.Soundness.TermStructureCases]
glu_rel_exp_vlookup [in Mctt.Core.Soundness.TermStructureCases]
glu_rel_exp_sub_typ [in Mctt.Core.Soundness.UniverseCases]
glu_rel_exp_clean_inversion2' [in Mctt.Core.Soundness.UniverseCases]
glu_rel_exp_typ [in Mctt.Core.Soundness.UniverseCases]
glu_rel_exp_of_typ [in Mctt.Core.Soundness.UniverseCases]
glu_rel_ctx_extend [in Mctt.Core.Soundness.ContextCases]
glu_rel_ctx_empty [in Mctt.Core.Soundness.ContextCases]
glu_rel_sub_conv [in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_conv [in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_conv' [in Mctt.Core.Soundness.SubtypingCases]
glu_rel_sub_subtyp [in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_subtyp [in Mctt.Core.Soundness.SubtypingCases]
glu_rel_exp_preserves_lvl [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_wf_sub [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion3 [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion2 [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_sub_clean_inversion1 [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_to_wf_exp [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion2 [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_clean_inversion1 [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_monotone [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_subtyp_sub_if [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_cons_clean_inversion [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_resp_per_ctx_helper [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_ctx_env [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_escape [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_wf_ctx [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_per_env [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_sub_eq [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_ctx_env_sub_resp_ctx_eq [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_typ_with_sub [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_with_sub_implies_glu_rel_exp_sub_with_typ [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_conv [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_trm_if [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_subtyp_typ_escape [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_conv' [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_conv [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_right [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower_max_left [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_lower [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_right [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_max_left [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_cumu_ge [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_right [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_max_left [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_cumu_ge [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumulativity_ge [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_right [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_max_left [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_cumu_ge [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_iff [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_unique_upto_exp_eq' [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_exp_unique_upto_exp_eq [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_typ_escape [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_per_univ_elem_typ_escape [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq' [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq_ge [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_univ_elem_typ_unique_upto_exp_eq [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
glu_rel_exp_app [in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_app_helper [in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_fn [in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_fn_helper [in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_of_pi [in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_pi [in Mctt.Core.Soundness.FunctionCases]
glu_rel_exp_natrec [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_helper [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_neut_helper [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_succ_helper [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_natrec_zero_helper [in Mctt.Core.Soundness.NatCases]
glu_rel_sub_extend_nat [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_succ [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_zero [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_of_nat [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_clean_inversion2'' [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_sub_nat [in Mctt.Core.Soundness.NatCases]
glu_rel_exp_nat [in Mctt.Core.Soundness.NatCases]
glu_rel_sub_extend [in Mctt.Core.Soundness.SubstitutionCases]
glu_rel_sub_compose [in Mctt.Core.Soundness.SubstitutionCases]
glu_rel_sub_weaken [in Mctt.Core.Soundness.SubstitutionCases]
glu_rel_sub_id [in Mctt.Core.Soundness.SubstitutionCases]
I
idempotent_nbe_ty [in Mctt.Core.Semantic.Consequences]id_sub_lookup_var1 [in Mctt.Core.Syntactic.System.Lemmas]
id_sub_lookup_var0 [in Mctt.Core.Syntactic.System.Lemmas]
initial_env_spec [in Mctt.Core.Semantic.NbE]
initial_env_glu_rel_exp [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
invert_compose_id [in Mctt.Core.Syntactic.Corollaries]
invert_sub_id_typ [in Mctt.Core.Syntactic.Corollaries]
invert_sub_id [in Mctt.Core.Syntactic.Corollaries]
is_typ_constr_and_exp_eq_nat_implies_eq_nat [in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr_and_exp_eq_typ_implies_eq_typ [in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr_and_exp_eq_var_implies_eq_var [in Mctt.Core.Completeness.Consequences.Types]
L
lift_nbe_max_right [in Mctt.Core.Semantic.NbE]lift_nbe_max_left [in Mctt.Core.Semantic.NbE]
lift_nbe_ge [in Mctt.Core.Semantic.NbE]
lift_exp_eq_max_right [in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_eq_max_left [in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_eq_ge [in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_max_right [in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_max_left [in Mctt.Core.Syntactic.System.Lemmas]
lift_exp_ge [in Mctt.Core.Syntactic.System.Lemmas]
M
mk_glu_rel_exp_with_sub'' [in Mctt.Core.Soundness.LogicalRelation.Lemmas]mk_glu_rel_exp_with_sub' [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub'' [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
mk_glu_rel_typ_with_sub' [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
N
nbe_type_to_nbe_ty [in Mctt.Core.Semantic.NbE]nbe_cumu [in Mctt.Core.Semantic.NbE]
ne_eq_dec [in Mctt.Core.Syntactic.Syntax]
nf_eq_dec [in Mctt.Core.Syntactic.Syntax]
nf_of_pi [in Mctt.Core.Semantic.Consequences]
no_closed_neutral [in Mctt.Core.Syntactic.System.Lemmas]
P
per_ctx_then_per_env_initial_env [in Mctt.Core.Semantic.Realizability]per_elem_then_per_top [in Mctt.Core.Semantic.Realizability]
per_bot_then_per_elem [in Mctt.Core.Semantic.Realizability]
per_univ_then_per_top_typ [in Mctt.Core.Semantic.Realizability]
per_nat_then_per_top [in Mctt.Core.Semantic.Realizability]
per_univ_elem_glu_univ_elem [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
per_univ_glu_univ_elem [in Mctt.Core.Soundness.LogicalRelation.CoreLemmas]
per_univ_elem_core_univ' [in Mctt.Core.Semantic.PER.Definitions]
PER_refl2 [in Mctt.LibTactics]
PER_refl1 [in Mctt.LibTactics]
per_ctx_subtyp_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl2 [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_refl1 [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_subtyping [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_subtyp_to_env [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_respects_length [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons_clean_inversion [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_cons' [in Mctt.Core.Semantic.PER.Lemmas]
per_env_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_cross_irrel [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_left_irrel [in Mctt.Core.Semantic.PER.Lemmas]
per_env_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_env_right_irrel [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_right [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu_left [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_cumu [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_transp [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_refl2 [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_refl1 [in Mctt.Core.Semantic.PER.Lemmas]
per_elem_subtyping_gen [in Mctt.Core.Semantic.PER.Lemmas]
per_elem_subtyping [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_to_univ_elem [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_right [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_max_left [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu_ge [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cumu [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi_clean_inversion [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_eq' [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_pi' [in Mctt.Core.Semantic.PER.Lemmas]
per_elem_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_trans' [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_cross_irrel [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_left_irrel [in Mctt.Core.Semantic.PER.Lemmas]
per_elem_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_sym' [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_elem_right_irrel [in Mctt.Core.Semantic.PER.Lemmas]
per_ne_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_ne_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_eq_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_eq_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_nat_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_nat_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_top_typ_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_top_typ_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_bot_then_per_top [in Mctt.Core.Semantic.PER.Lemmas]
per_top_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_top_sym [in Mctt.Core.Semantic.PER.Lemmas]
per_bot_trans [in Mctt.Core.Semantic.PER.Lemmas]
per_bot_sym [in Mctt.Core.Semantic.PER.Lemmas]
presup_subtyp [in Mctt.Core.Syntactic.Presup]
presup_sub_eq [in Mctt.Core.Syntactic.Presup]
presup_exp_eq [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_sub_compose_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_sub_cong_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_var_S_sub_left [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_var_0_sub_left [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_beta_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_cong_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_refl_cong_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_sub_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_eqrec_sub_left [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_refl_sub_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_id_sub_helper3 [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_typ_id_sub2_eq [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_id_sub_helper2 [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_sub_helper3 [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_typ_sub2_eq [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_sub_helper2 [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_wf [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_var1 [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_prop_eq_var0 [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_pi_eta_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_app_sub_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_app_sub_left [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_app_cong_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_fn_sub_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_fn_cong_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_beta_succ_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_natrec_sub_right [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_natrec_sub_left [in Mctt.Core.Syntactic.Presup]
presup_exp_eq_natrec_cong_right [in Mctt.Core.Syntactic.Presup]
presup_typ_glu_rel_exp [in Mctt.Core.Soundness.TermStructureCases]
presup_ctx_glu_rel_exp [in Mctt.Core.Soundness.TermStructureCases]
presup_glu_rel_exp [in Mctt.Core.Soundness.TermStructureCases]
presup_subtyp_right [in Mctt.Core.Syntactic.System.Definitions]
presup_ctx_sub_right [in Mctt.Core.Syntactic.System.Definitions]
presup_ctx_sub_left [in Mctt.Core.Syntactic.System.Definitions]
presup_ctx_sub [in Mctt.Core.Syntactic.System.Definitions]
presup_rel_exp [in Mctt.Core.Completeness.TermStructureCases]
presup_rel_sub [in Mctt.Core.Completeness.SubstitutionCases]
presup_right_glu_rel_sub [in Mctt.Core.Soundness.SubstitutionCases]
presup_left_glu_rel_sub [in Mctt.Core.Soundness.SubstitutionCases]
presup_glu_rel_sub [in Mctt.Core.Soundness.SubstitutionCases]
presup_exp [in Mctt.Core.Syntactic.System.Lemmas]
presup_exp_typ [in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_lookup_typ [in Mctt.Core.Syntactic.System.Lemmas]
presup_exp_eq_ctx [in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_right [in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx_left [in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_eq_ctx [in Mctt.Core.Syntactic.System.Lemmas]
presup_exp_ctx [in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_right [in Mctt.Core.Syntactic.System.Lemmas]
presup_sub_left [in Mctt.Core.Syntactic.System.Lemmas]
presup_sub [in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_right [in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_eq_left [in Mctt.Core.Syntactic.System.Lemmas]
presup_ctx_eq [in Mctt.Core.Syntactic.System.Lemmas]
R
realize_per_univ_elem_gen [in Mctt.Core.Semantic.Realizability]realize_glu_elem_top [in Mctt.Core.Soundness.Realizability]
realize_glu_elem_bot [in Mctt.Core.Soundness.Realizability]
realize_glu_typ_top [in Mctt.Core.Soundness.Realizability]
realize_glu_univ_elem_gen [in Mctt.Core.Soundness.Realizability]
rel_exp_cumu [in Mctt.Core.Completeness.UniverseCases]
rel_exp_typ_sub [in Mctt.Core.Completeness.UniverseCases]
rel_exp_of_typ [in Mctt.Core.Completeness.UniverseCases]
rel_exp_under_ctx_implies_rel_typ_under_ctx [in Mctt.Core.Completeness.UniverseCases]
rel_exp_of_typ_inversion2 [in Mctt.Core.Completeness.UniverseCases]
rel_exp_of_typ_inversion1 [in Mctt.Core.Completeness.UniverseCases]
rel_exp_nat_beta_succ [in Mctt.Core.Completeness.NatCases]
rel_exp_nat_beta_succ_rel_typ [in Mctt.Core.Completeness.NatCases]
rel_exp_nat_beta_zero [in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_sub [in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_sub_rel_typ [in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_cong [in Mctt.Core.Completeness.NatCases]
rel_exp_natrec_cong_rel_typ [in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_id_N [in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_wkwk_succ_var1_inversion [in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero [in Mctt.Core.Completeness.NatCases]
rel_exp_of_sub_id_zero_inversion [in Mctt.Core.Completeness.NatCases]
rel_exp_succ_cong [in Mctt.Core.Completeness.NatCases]
rel_exp_succ_sub [in Mctt.Core.Completeness.NatCases]
rel_exp_zero_sub [in Mctt.Core.Completeness.NatCases]
rel_exp_nat_sub [in Mctt.Core.Completeness.NatCases]
rel_exp_of_nat [in Mctt.Core.Completeness.NatCases]
rel_exp_of_nat_inversion [in Mctt.Core.Completeness.NatCases]
rel_exp_var_weaken [in Mctt.Core.Completeness.VariableCases]
rel_exp_var_S_sub [in Mctt.Core.Completeness.VariableCases]
rel_exp_var_0_sub [in Mctt.Core.Completeness.VariableCases]
rel_ctx_sub_extend [in Mctt.Core.Completeness.ContextCases]
rel_ctx_sub_empty [in Mctt.Core.Completeness.ContextCases]
rel_ctx_extend' [in Mctt.Core.Completeness.ContextCases]
rel_ctx_extend [in Mctt.Core.Completeness.ContextCases]
rel_exp_eq_subtyp [in Mctt.Core.Completeness.TermStructureCases]
rel_exp_trans [in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sym [in Mctt.Core.Completeness.TermStructureCases]
rel_exp_conv [in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sub_compose [in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sub_id [in Mctt.Core.Completeness.TermStructureCases]
rel_exp_sub_cong [in Mctt.Core.Completeness.TermStructureCases]
rel_sub_eq_subtyp [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_conv [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_trans [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_sym [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_extend [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_p_extend [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_extend_compose [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_compose_assoc [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_left [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_id_compose_right [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_extend_cong [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_compose_cong [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_weaken [in Mctt.Core.Completeness.SubstitutionCases]
rel_sub_id [in Mctt.Core.Completeness.SubstitutionCases]
rel_exp_eqrec_beta [in Mctt.Core.Completeness.EqualityCases]
rel_exp_eqrec_cong [in Mctt.Core.Completeness.EqualityCases]
rel_exp_eqrec_sub [in Mctt.Core.Completeness.EqualityCases]
rel_exp_refl_sub [in Mctt.Core.Completeness.EqualityCases]
rel_exp_eq_sub [in Mctt.Core.Completeness.EqualityCases]
rel_exp_refl_cong [in Mctt.Core.Completeness.EqualityCases]
rel_exp_eq_cong [in Mctt.Core.Completeness.EqualityCases]
rel_exp_pi_eta [in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_beta [in Mctt.Core.Completeness.FunctionCases]
rel_exp_app_sub [in Mctt.Core.Completeness.FunctionCases]
rel_exp_app_cong [in Mctt.Core.Completeness.FunctionCases]
rel_exp_fn_sub [in Mctt.Core.Completeness.FunctionCases]
rel_exp_fn_cong [in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_sub [in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_cong [in Mctt.Core.Completeness.FunctionCases]
rel_exp_pi_core [in Mctt.Core.Completeness.FunctionCases]
rel_exp_of_pi [in Mctt.Core.Completeness.FunctionCases]
rel_exp_of_pi_inversion [in Mctt.Core.Completeness.FunctionCases]
rel_exp_clean_inversion [in Mctt.Core.Completeness.LogicalRelation.Lemmas]
rel_typ_implies_rel_exp [in Mctt.Core.Completeness.LogicalRelation.Lemmas]
rel_exp_implies_rel_typ [in Mctt.Core.Completeness.LogicalRelation.Lemmas]
S
soundness [in Mctt.Core.Soundness]soundness_fundamental_sub [in Mctt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_exp [in Mctt.Core.Soundness.FundamentalTheorem]
soundness_fundamental_ctx [in Mctt.Core.Soundness.FundamentalTheorem]
soundness_fundamental [in Mctt.Core.Soundness.FundamentalTheorem]
soundness_ty' [in Mctt.Core.Soundness]
soundness_ty [in Mctt.Core.Soundness]
soundness' [in Mctt.Core.Soundness]
subtyp_pi [in Mctt.Core.Completeness.SubtypingCases]
subtyp_univ [in Mctt.Core.Completeness.SubtypingCases]
subtyp_trans [in Mctt.Core.Completeness.SubtypingCases]
subtyp_refl [in Mctt.Core.Completeness.SubtypingCases]
subtyp_spec [in Mctt.Core.Semantic.Consequences]
sub_eq_q_compose_nat [in Mctt.Core.Syntactic.Corollaries]
sub_eq_q_compose [in Mctt.Core.Syntactic.Corollaries]
sub_eq_p_q_sigma_compose_tau_extend [in Mctt.Core.Syntactic.Corollaries]
sub_decompose_q_typ [in Mctt.Core.Syntactic.Corollaries]
sub_decompose_q [in Mctt.Core.Syntactic.Corollaries]
sub_q_eq [in Mctt.Core.Syntactic.Corollaries]
sub_id_typ [in Mctt.Core.Syntactic.Corollaries]
sub_lookup_var1 [in Mctt.Core.Syntactic.System.Lemmas]
sub_lookup_var0 [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_p_q_q_sigma_nat [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma_nat [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_q_sigma [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_q_sigma_id_extend [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_sigma_compose_weak_id_extend [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_compose_sigma [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_nat_compose_sigma [in Mctt.Core.Syntactic.System.Lemmas]
sub_weak_compose_weak_extend_succ_var_1 [in Mctt.Core.Syntactic.System.Lemmas]
sub_id_extend_zero [in Mctt.Core.Syntactic.System.Lemmas]
sub_q_nat [in Mctt.Core.Syntactic.System.Lemmas]
sub_q_typ [in Mctt.Core.Syntactic.System.Lemmas]
sub_q [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_id_extend [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_extend_cong [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_id_on_typ [in Mctt.Core.Syntactic.System.Lemmas]
sub_id_extend [in Mctt.Core.Syntactic.System.Lemmas]
sub_id_on_typ [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_weaken_var0_id [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_nat [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_nat [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_nat [in Mctt.Core.Syntactic.System.Lemmas]
sub_extend_nat [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_p_extend_typ [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_compose_typ [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_extend_cong_typ [in Mctt.Core.Syntactic.System.Lemmas]
sub_extend_typ [in Mctt.Core.Syntactic.System.Lemmas]
sub_eq_refl [in Mctt.Core.Syntactic.System.Lemmas]
V
valid_exp_typ [in Mctt.Core.Completeness.UniverseCases]valid_exp_zero [in Mctt.Core.Completeness.NatCases]
valid_exp_nat [in Mctt.Core.Completeness.NatCases]
valid_exp_var [in Mctt.Core.Completeness.VariableCases]
valid_lookup [in Mctt.Core.Completeness.VariableCases]
valid_ctx_empty [in Mctt.Core.Completeness.ContextCases]
valid_exp_eq [in Mctt.Core.Completeness.EqualityCases]
var_per_elem [in Mctt.Core.Semantic.Realizability]
var_per_bot [in Mctt.Core.Semantic.PER.Lemmas]
var_glu_elem_bot [in Mctt.Core.Soundness.Realizability]
var_weaken_gen [in Mctt.Core.Soundness.Realizability]
var_arith [in Mctt.Core.Soundness.Realizability]
var_compose_subs [in Mctt.Core.Syntactic.System.Lemmas]
var0_glu_elem [in Mctt.Core.Soundness.Realizability]
vlookup_1_nat [in Mctt.Core.Syntactic.System.Lemmas]
vlookup_0_nat [in Mctt.Core.Syntactic.System.Lemmas]
vlookup_1_typ [in Mctt.Core.Syntactic.System.Lemmas]
vlookup_0_typ [in Mctt.Core.Syntactic.System.Lemmas]
W
weakening_wk [in Mctt.Core.Soundness.Weakening.Lemmas]weakening_id [in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_compose [in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_conv [in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_resp_equiv [in Mctt.Core.Soundness.Weakening.Lemmas]
weakening_escape [in Mctt.Core.Soundness.Weakening.Lemmas]
wf_exp_eq_refl_sub' [in Mctt.Core.Syntactic.SystemOpt]
wf_subtyp_pi' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_eta' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_beta' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_sub' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_app_cong' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_sub' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_fn_cong' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong_max [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_cong' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_pi_sub_max [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_succ' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_beta_zero' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_sub' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_natrec_cong' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_nat_sub' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_typ_sub' [in Mctt.Core.Syntactic.SystemOpt]
wf_app' [in Mctt.Core.Syntactic.SystemOpt]
wf_fn' [in Mctt.Core.Syntactic.SystemOpt]
wf_pi_max [in Mctt.Core.Syntactic.SystemOpt]
wf_natrec' [in Mctt.Core.Syntactic.SystemOpt]
wf_nat' [in Mctt.Core.Syntactic.SystemOpt]
wf_ctx_eq_extend' [in Mctt.Core.Syntactic.SystemOpt]
wf_exp_eq_conv' [in Mctt.Core.Syntactic.SystemOpt]
wf_conv' [in Mctt.Core.Syntactic.SystemOpt]
wf_subtyp_refl' [in Mctt.Core.Syntactic.SystemOpt]
wf_sub_eq_subtyp' [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp' [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_subtyp' [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_subtyp' [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_subst [in Mctt.Core.Syntactic.Corollaries]
wf_subtyp_subst_eq [in Mctt.Core.Syntactic.Corollaries]
wf_ctx_sub_length [in Mctt.Core.Syntactic.Corollaries]
wf_sub_extend_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_sub_compose_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_sub_weaken_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_sub_id_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_exp_sub_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_vlookup_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_app_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_fn_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_pi_inversion' [in Mctt.Core.Syntactic.CoreInversions]
wf_pi_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_natrec_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_succ_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_zero_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_nat_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_typ_inversion [in Mctt.Core.Syntactic.CoreInversions]
wf_ctx_sub_ctx_lookup [in Mctt.Core.Soundness.Realizability]
wf_ctx_sub_trans [in Mctt.Core.Syntactic.CtxSub]
wf_subtyp_univ_weaken [in Mctt.Core.Syntactic.System.Lemmas]
wf_subtyp_sub [in Mctt.Core.Syntactic.System.Lemmas]
wf_subtyp_ge [in Mctt.Core.Syntactic.System.Lemmas]
wf_subtyp_refl [in Mctt.Core.Syntactic.System.Lemmas]
wf_sub_eq_conv [in Mctt.Core.Syntactic.System.Lemmas]
wf_exp_eq_conv [in Mctt.Core.Syntactic.System.Lemmas]
wf_sub_conv [in Mctt.Core.Syntactic.System.Lemmas]
wf_conv [in Mctt.Core.Syntactic.System.Lemmas]
wf_ctx_sub_refl [in Mctt.Core.Syntactic.System.Lemmas]
wf_exp_eq_cumu [in Mctt.Core.Syntactic.System.Lemmas]
wf_cumu [in Mctt.Core.Syntactic.System.Lemmas]
Constructor Index
A
a_extend [in Mctt.Core.Syntactic.Syntax]a_compose [in Mctt.Core.Syntactic.Syntax]
a_weaken [in Mctt.Core.Syntactic.Syntax]
a_id [in Mctt.Core.Syntactic.Syntax]
a_sub [in Mctt.Core.Syntactic.Syntax]
a_var [in Mctt.Core.Syntactic.Syntax]
a_eqrec [in Mctt.Core.Syntactic.Syntax]
a_refl [in Mctt.Core.Syntactic.Syntax]
a_eq [in Mctt.Core.Syntactic.Syntax]
a_app [in Mctt.Core.Syntactic.Syntax]
a_fn [in Mctt.Core.Syntactic.Syntax]
a_pi [in Mctt.Core.Syntactic.Syntax]
a_natrec [in Mctt.Core.Syntactic.Syntax]
a_succ [in Mctt.Core.Syntactic.Syntax]
a_zero [in Mctt.Core.Syntactic.Syntax]
a_nat [in Mctt.Core.Syntactic.Syntax]
a_typ [in Mctt.Core.Syntactic.Syntax]
C
canonical_nat_succ [in Mctt.Core.Semantic.Consequences]canonical_nat_zero [in Mctt.Core.Semantic.Consequences]
Cst.app [in Mctt.Core.Syntactic.Syntax]
Cst.eqrec [in Mctt.Core.Syntactic.Syntax]
Cst.fn [in Mctt.Core.Syntactic.Syntax]
Cst.nat [in Mctt.Core.Syntactic.Syntax]
Cst.natrec [in Mctt.Core.Syntactic.Syntax]
Cst.pi [in Mctt.Core.Syntactic.Syntax]
Cst.prop_eq [in Mctt.Core.Syntactic.Syntax]
Cst.refl [in Mctt.Core.Syntactic.Syntax]
Cst.succ [in Mctt.Core.Syntactic.Syntax]
Cst.typ [in Mctt.Core.Syntactic.Syntax]
Cst.var [in Mctt.Core.Syntactic.Syntax]
Cst.zero [in Mctt.Core.Syntactic.Syntax]
D
d_dom [in Mctt.Core.Semantic.Domain]d_eqrec [in Mctt.Core.Semantic.Domain]
d_natrec [in Mctt.Core.Semantic.Domain]
d_app [in Mctt.Core.Semantic.Domain]
d_var [in Mctt.Core.Semantic.Domain]
d_neut [in Mctt.Core.Semantic.Domain]
d_refl [in Mctt.Core.Semantic.Domain]
d_eq [in Mctt.Core.Semantic.Domain]
d_fn [in Mctt.Core.Semantic.Domain]
d_pi [in Mctt.Core.Semantic.Domain]
d_succ [in Mctt.Core.Semantic.Domain]
d_zero [in Mctt.Core.Semantic.Domain]
d_nat [in Mctt.Core.Semantic.Domain]
d_univ [in Mctt.Core.Semantic.Domain]
E
eq_is_typ_constr [in Mctt.Core.Completeness.Consequences.Types]eval_sub_compose [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_extend [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_weaken [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_id [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_neut [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_refl [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_neut [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_fn [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_neut [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_succ [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_zero [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_sub [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_eqrec [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_refl [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_eq [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_app [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_fn [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_pi [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_natrec [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_succ [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_zero [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_nat [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_var [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_typ [in Mctt.Core.Semantic.Evaluation.Definitions]
G
glu_ctx_env_cons [in Mctt.Core.Soundness.LogicalRelation.Definitions]glu_ctx_env_nil [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top_make [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top_make [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot_make [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_neut [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_eq [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_pi [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_nat [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_univ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_eq_neut [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_eq_refl [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_neut [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_succ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_zero [in Mctt.Core.Soundness.LogicalRelation.Definitions]
H
here [in Mctt.Core.Syntactic.System.Definitions]I
initial_env_cons [in Mctt.Core.Semantic.NbE]initial_env_nil [in Mctt.Core.Semantic.NbE]
M
mk_cons_per_ctx_env [in Mctt.Core.Semantic.PER.Definitions]mk_rel_mod_app [in Mctt.Core.Semantic.PER.Definitions]
mk_rel_mod_eval [in Mctt.Core.Semantic.PER.Definitions]
mk_rel_sub [in Mctt.Core.Completeness.LogicalRelation.Definitions]
mk_rel_exp [in Mctt.Core.Completeness.LogicalRelation.Definitions]
mk_glu_rel_sub_with_sub [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_glu_rel_exp_with_sub [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_cons_glu_sub_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_glu_rel_typ_with_sub [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_eq_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_eq_glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_pi_glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
mk_neut_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
N
nat_is_typ_constr [in Mctt.Core.Completeness.Consequences.Types]nbe_ty_run [in Mctt.Core.Semantic.NbE]
nbe_run [in Mctt.Core.Semantic.NbE]
ne_eqrec [in Mctt.Core.Syntactic.Syntax]
ne_var [in Mctt.Core.Syntactic.Syntax]
ne_app [in Mctt.Core.Syntactic.Syntax]
ne_natrec [in Mctt.Core.Syntactic.Syntax]
nf_neut [in Mctt.Core.Syntactic.Syntax]
nf_refl [in Mctt.Core.Syntactic.Syntax]
nf_eq [in Mctt.Core.Syntactic.Syntax]
nf_fn [in Mctt.Core.Syntactic.Syntax]
nf_pi [in Mctt.Core.Syntactic.Syntax]
nf_succ [in Mctt.Core.Syntactic.Syntax]
nf_zero [in Mctt.Core.Syntactic.Syntax]
nf_nat [in Mctt.Core.Syntactic.Syntax]
nf_typ [in Mctt.Core.Syntactic.Syntax]
P
per_ctx_subtyp_cons [in Mctt.Core.Semantic.PER.Definitions]per_ctx_subtyp_nil [in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_cons [in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_nil [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_neut [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_eq [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_pi [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_nat [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_univ [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_neut [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_eq [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_pi [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_nat [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_univ [in Mctt.Core.Semantic.PER.Definitions]
per_ne_neut [in Mctt.Core.Semantic.PER.Definitions]
per_eq_neut [in Mctt.Core.Semantic.PER.Definitions]
per_eq_refl [in Mctt.Core.Semantic.PER.Definitions]
per_nat_neut [in Mctt.Core.Semantic.PER.Definitions]
per_nat_succ [in Mctt.Core.Semantic.PER.Definitions]
per_nat_zero [in Mctt.Core.Semantic.PER.Definitions]
per_elem [in Mctt.LibTactics]
pi_is_typ_constr [in Mctt.Core.Completeness.Consequences.Types]
R
read_typ_neut [in Mctt.Core.Semantic.Readback.Definitions]read_typ_eq [in Mctt.Core.Semantic.Readback.Definitions]
read_typ_pi [in Mctt.Core.Semantic.Readback.Definitions]
read_typ_nat [in Mctt.Core.Semantic.Readback.Definitions]
read_typ_univ [in Mctt.Core.Semantic.Readback.Definitions]
read_ne_eqrec [in Mctt.Core.Semantic.Readback.Definitions]
read_ne_app [in Mctt.Core.Semantic.Readback.Definitions]
read_ne_natrec [in Mctt.Core.Semantic.Readback.Definitions]
read_ne_var [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_neut [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_eq_neut [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_refl [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_fn [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_nat_neut [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_succ [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_zero [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_type [in Mctt.Core.Semantic.Readback.Definitions]
T
there [in Mctt.Core.Syntactic.System.Definitions]typ_is_typ_constr [in Mctt.Core.Completeness.Consequences.Types]
V
var_is_typ_constr [in Mctt.Core.Completeness.Consequences.Types]W
wf_ctx_eq_extend [in Mctt.Core.Syntactic.System.Definitions]wf_ctx_eq_empty [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_pi [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_univ [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_trans [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_refl [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_subtyp [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_trans [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_sym [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_p_extend [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_compose [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_assoc [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_left [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_id_compose_right [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_extend_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_compose_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_weaken [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_id [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_trans [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sym [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_subtyp [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_compose [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_id [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sub_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_weaken [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_S_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var_0_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_var [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eqrec_beta [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eqrec_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_refl_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eq_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eqrec_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_refl_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_eq_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_eta [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_beta [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_app_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_fn_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_pi_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_succ [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_beta_zero [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_natrec_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_cong [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_succ_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_zero_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_nat_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_typ_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_subtyp [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_extend [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_compose [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_weaken [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_id [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_subtyp [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_eqrec [in Mctt.Core.Syntactic.System.Definitions]
wf_refl [in Mctt.Core.Syntactic.System.Definitions]
wf_eq [in Mctt.Core.Syntactic.System.Definitions]
wf_vlookup [in Mctt.Core.Syntactic.System.Definitions]
wf_app [in Mctt.Core.Syntactic.System.Definitions]
wf_fn [in Mctt.Core.Syntactic.System.Definitions]
wf_pi [in Mctt.Core.Syntactic.System.Definitions]
wf_natrec [in Mctt.Core.Syntactic.System.Definitions]
wf_succ [in Mctt.Core.Syntactic.System.Definitions]
wf_zero [in Mctt.Core.Syntactic.System.Definitions]
wf_nat [in Mctt.Core.Syntactic.System.Definitions]
wf_typ [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_extend [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_empty [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_extend [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_empty [in Mctt.Core.Syntactic.System.Definitions]
wk_p [in Mctt.Core.Soundness.Weakening.Definitions]
wk_id [in Mctt.Core.Soundness.Weakening.Definitions]
Inductive Index
C
canonical_nat [in Mctt.Core.Semantic.Consequences]cons_per_ctx_env [in Mctt.Core.Semantic.PER.Definitions]
cons_glu_sub_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
Cst.obj [in Mctt.Core.Syntactic.Syntax]
ctx_lookup [in Mctt.Core.Syntactic.System.Definitions]
D
domain [in Mctt.Core.Semantic.Domain]domain_nf [in Mctt.Core.Semantic.Domain]
domain_ne [in Mctt.Core.Semantic.Domain]
E
eq_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]eq_glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
eval_sub [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp [in Mctt.Core.Semantic.Evaluation.Definitions]
exp [in Mctt.Core.Syntactic.Syntax]
G
glu_rel_sub_with_sub [in Mctt.Core.Soundness.LogicalRelation.Definitions]glu_rel_exp_with_sub [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_typ_with_sub [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_typ_top [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_top [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_elem_bot [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_eq [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat [in Mctt.Core.Soundness.LogicalRelation.Definitions]
I
initial_env [in Mctt.Core.Semantic.NbE]is_typ_constr [in Mctt.Core.Completeness.Consequences.Types]
N
nbe [in Mctt.Core.Semantic.NbE]nbe_ty [in Mctt.Core.Semantic.NbE]
ne [in Mctt.Core.Syntactic.Syntax]
neut_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
nf [in Mctt.Core.Syntactic.Syntax]
P
PERElem [in Mctt.LibTactics]per_ctx_subtyp [in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core [in Mctt.Core.Semantic.PER.Definitions]
per_ne [in Mctt.Core.Semantic.PER.Definitions]
per_eq [in Mctt.Core.Semantic.PER.Definitions]
per_nat [in Mctt.Core.Semantic.PER.Definitions]
pi_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
pi_glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
R
read_typ [in Mctt.Core.Semantic.Readback.Definitions]read_ne [in Mctt.Core.Semantic.Readback.Definitions]
read_nf [in Mctt.Core.Semantic.Readback.Definitions]
rel_mod_app [in Mctt.Core.Semantic.PER.Definitions]
rel_mod_eval [in Mctt.Core.Semantic.PER.Definitions]
rel_sub [in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp [in Mctt.Core.Completeness.LogicalRelation.Definitions]
S
sub [in Mctt.Core.Syntactic.Syntax]W
weakening [in Mctt.Core.Soundness.Weakening.Definitions]wf_ctx_eq [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq [in Mctt.Core.Syntactic.System.Definitions]
wf_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_exp [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx [in Mctt.Core.Syntactic.System.Definitions]
Projection Index
P
per_elem [in Mctt.LibTactics]Section Index
C
completeness_fundamental [in Mctt.Core.Completeness.FundamentalTheorem]F
functional_eval [in Mctt.Core.Semantic.Evaluation.Lemmas]functional_read [in Mctt.Core.Semantic.Readback.Lemmas]
G
Gluing [in Mctt.Core.Soundness.LogicalRelation.Definitions]GluingInduction [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_cumulativity [in Mctt.Core.Soundness.LogicalRelation.Lemmas]
P
Per_univ_elem_ind_def [in Mctt.Core.Semantic.PER.Definitions]Per_univ_elem_core_def [in Mctt.Core.Semantic.PER.Definitions]
S
soundness_fundamental [in Mctt.Core.Soundness.FundamentalTheorem]Instance Index
P
PERProper [in Mctt.LibTactics]per_ctx_subtyp_trans_ins [in Mctt.Core.Semantic.PER.Lemmas]
per_env_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_ctx_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_subtyp_trans_ins [in Mctt.Core.Semantic.PER.Lemmas]
per_elem_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_PER' [in Mctt.Core.Semantic.PER.Lemmas]
per_univ_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_ne_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_eq_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_nat_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_top_typ_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_top_PER [in Mctt.Core.Semantic.PER.Lemmas]
per_bot_PER [in Mctt.Core.Semantic.PER.Lemmas]
predicate_implication_equivalence [in Mctt.LibTactics]
R
rel_exp_PER [in Mctt.Core.Completeness.TermStructureCases]rel_sub_PER [in Mctt.Core.Completeness.SubstitutionCases]
S
subtyp_Transitive [in Mctt.Core.Completeness.SubtypingCases]W
wf_sub_eq_per_elem [in Mctt.Core.Syntactic.System.Definitions]wf_exp_eq_per_elem [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_Transitive [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq_Symmetric [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_PER [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_PER [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_PER [in Mctt.Core.Syntactic.CtxEq]
wf_ctx_sub_trans_ins [in Mctt.Core.Syntactic.CtxSub]
Abbreviation Index
C
ctx [in Mctt.Core.Syntactic.Syntax]T
typ [in Mctt.Core.Syntactic.Syntax]Definition Index
C
canonical_nat_sind [in Mctt.Core.Semantic.Consequences]canonical_nat_ind [in Mctt.Core.Semantic.Consequences]
Cst.obj_sind [in Mctt.Core.Syntactic.Syntax]
Cst.obj_rec [in Mctt.Core.Syntactic.Syntax]
Cst.obj_ind [in Mctt.Core.Syntactic.Syntax]
Cst.obj_rect [in Mctt.Core.Syntactic.Syntax]
ctx_lookup_sind [in Mctt.Core.Syntactic.System.Definitions]
ctx_lookup_ind [in Mctt.Core.Syntactic.System.Definitions]
D
domain_nf_sind [in Mctt.Core.Semantic.Domain]domain_nf_rec [in Mctt.Core.Semantic.Domain]
domain_nf_ind [in Mctt.Core.Semantic.Domain]
domain_nf_rect [in Mctt.Core.Semantic.Domain]
domain_ne_sind [in Mctt.Core.Semantic.Domain]
domain_ne_rec [in Mctt.Core.Semantic.Domain]
domain_ne_ind [in Mctt.Core.Semantic.Domain]
domain_ne_rect [in Mctt.Core.Semantic.Domain]
domain_sind [in Mctt.Core.Semantic.Domain]
domain_rec [in Mctt.Core.Semantic.Domain]
domain_ind [in Mctt.Core.Semantic.Domain]
domain_rect [in Mctt.Core.Semantic.Domain]
drop_env [in Mctt.Core.Semantic.Domain]
E
empty_env [in Mctt.Core.Semantic.Domain]eval_sub_mut_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_mut_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_mut_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_mut_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_mut_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_sind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_sub_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_sind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_eqrec_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_sind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_app_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_sind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_natrec_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_sind [in Mctt.Core.Semantic.Evaluation.Definitions]
eval_exp_ind [in Mctt.Core.Semantic.Evaluation.Definitions]
exp_to_num [in Mctt.Core.Syntactic.Syntax]
exp_to_nat [in Mctt.Core.Syntactic.Syntax]
exp_sind [in Mctt.Core.Syntactic.Syntax]
exp_rec [in Mctt.Core.Syntactic.Syntax]
exp_ind [in Mctt.Core.Syntactic.Syntax]
exp_rect [in Mctt.Core.Syntactic.Syntax]
extend_env [in Mctt.Core.Semantic.Domain]
G
glu_rel_sub [in Mctt.Core.Soundness.LogicalRelation.Definitions]glu_rel_sub_resp_sub_env [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_exp_resp_sub_env [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_rel_ctx [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_sind [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_ctx_env_ind [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_ind [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_typ [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_sind [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_univ_elem_core_ind [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_sind [in Mctt.Core.Soundness.LogicalRelation.Definitions]
glu_nat_ind [in Mctt.Core.Soundness.LogicalRelation.Definitions]
I
initial_env_sind [in Mctt.Core.Semantic.NbE]initial_env_ind [in Mctt.Core.Semantic.NbE]
is_typ_constr_sind [in Mctt.Core.Completeness.Consequences.Types]
is_typ_constr_ind [in Mctt.Core.Completeness.Consequences.Types]
N
nat_to_exp [in Mctt.Core.Syntactic.Syntax]nat_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
nat_glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
nbe_ty_sind [in Mctt.Core.Semantic.NbE]
nbe_ty_ind [in Mctt.Core.Semantic.NbE]
nbe_sind [in Mctt.Core.Semantic.NbE]
nbe_ind [in Mctt.Core.Semantic.NbE]
neut_glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
ne_to_exp [in Mctt.Core.Syntactic.Syntax]
ne_sind [in Mctt.Core.Syntactic.Syntax]
ne_rec [in Mctt.Core.Syntactic.Syntax]
ne_ind [in Mctt.Core.Syntactic.Syntax]
ne_rect [in Mctt.Core.Syntactic.Syntax]
nf_to_exp [in Mctt.Core.Syntactic.Syntax]
nf_sind [in Mctt.Core.Syntactic.Syntax]
nf_rec [in Mctt.Core.Syntactic.Syntax]
nf_ind [in Mctt.Core.Syntactic.Syntax]
nf_rect [in Mctt.Core.Syntactic.Syntax]
nil_glu_sub_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
num_to_exp [in Mctt.Core.Syntactic.Syntax]
P
per_ctx_subtyp_sind [in Mctt.Core.Semantic.PER.Definitions]per_ctx_subtyp_ind [in Mctt.Core.Semantic.PER.Definitions]
per_ctx [in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_sind [in Mctt.Core.Semantic.PER.Definitions]
per_ctx_env_ind [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_sind [in Mctt.Core.Semantic.PER.Definitions]
per_subtyp_ind [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_ind [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_ind' [in Mctt.Core.Semantic.PER.Definitions]
per_univ [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_strong_ind [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_sind [in Mctt.Core.Semantic.PER.Definitions]
per_univ_elem_core_ind [in Mctt.Core.Semantic.PER.Definitions]
per_nat_sind [in Mctt.Core.Semantic.PER.Definitions]
per_nat_ind [in Mctt.Core.Semantic.PER.Definitions]
per_top_typ [in Mctt.Core.Semantic.PER.Definitions]
per_top [in Mctt.Core.Semantic.PER.Definitions]
per_bot [in Mctt.Core.Semantic.PER.Definitions]
Q
q [in Mctt.Core.Syntactic.Syntax]R
read_typ_mut_ind [in Mctt.Core.Semantic.Readback.Definitions]read_ne_mut_ind [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_mut_ind [in Mctt.Core.Semantic.Readback.Definitions]
read_typ_sind [in Mctt.Core.Semantic.Readback.Definitions]
read_typ_ind [in Mctt.Core.Semantic.Readback.Definitions]
read_ne_sind [in Mctt.Core.Semantic.Readback.Definitions]
read_ne_ind [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_sind [in Mctt.Core.Semantic.Readback.Definitions]
read_nf_ind [in Mctt.Core.Semantic.Readback.Definitions]
rel_typ [in Mctt.Core.Semantic.PER.Definitions]
rel_sub_under_ctx [in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_sind [in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_sub_ind [in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_under_ctx [in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_sind [in Mctt.Core.Completeness.LogicalRelation.Definitions]
rel_exp_ind [in Mctt.Core.Completeness.LogicalRelation.Definitions]
S
subtyp_under_ctx [in Mctt.Core.Completeness.LogicalRelation.Definitions]sub_sind [in Mctt.Core.Syntactic.Syntax]
sub_rec [in Mctt.Core.Syntactic.Syntax]
sub_ind [in Mctt.Core.Syntactic.Syntax]
sub_rect [in Mctt.Core.Syntactic.Syntax]
U
univ_glu_exp_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]univ_glu_exp_pred' [in Mctt.Core.Soundness.LogicalRelation.Definitions]
univ_glu_typ_pred [in Mctt.Core.Soundness.LogicalRelation.Definitions]
V
valid_ctx [in Mctt.Core.Semantic.PER.Definitions]valid_sub_under_ctx [in Mctt.Core.Completeness.LogicalRelation.Definitions]
valid_exp_under_ctx [in Mctt.Core.Completeness.LogicalRelation.Definitions]
W
weakening_sind [in Mctt.Core.Soundness.Weakening.Definitions]weakening_ind [in Mctt.Core.Soundness.Weakening.Definitions]
wf_ctx_eq_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_eq_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind' [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind' [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind' [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_mut_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_mut_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_mut_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_mut_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_mut_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_mut_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_mut_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_subtyp_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_eq_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_eq_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_sub_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_exp_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sub_ind [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_sind [in Mctt.Core.Syntactic.System.Definitions]
wf_ctx_ind [in Mctt.Core.Syntactic.System.Definitions]
_
__mark__ [in Mctt.LibTactics]Record Index
P
PERElem [in Mctt.LibTactics]| 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 | _ | other | (1314 entries) |
| Notation 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 | _ | other | (114 entries) |
| Module 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 | _ | other | (4 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 | _ | other | (22 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 | _ | other | (64 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 | _ | other | (615 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 | _ | other | (238 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 | _ | other | (60 entries) |
| Projection 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 | _ | other | (1 entry) |
| 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 | _ | other | (9 entries) |
| Instance 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 | _ | other | (26 entries) |
| Abbreviation 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 | _ | other | (2 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 | _ | other | (158 entries) |
| Record 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 | _ | other | (1 entry) |