Mctt Core Core Core/Completeness Completeness Core/Completeness/Consequences Consequences Core/Completeness/LogicalRelation LogicalRelation Core/Semantic Semantic Core/Semantic/Evaluation Evaluation Core/Semantic/PER PER Core/Semantic/Readback Readback Core/Soundness Soundness Core/Soundness/LogicalRelation LogicalRelation Core/Soundness/Weakening Weakening Core/Syntactic Syntactic Core/Syntactic/System System Mctt.Core.Completeness.Consequences.Rules Rules Mctt.Core.Completeness.Consequences.Types Types Mctt.Core.Semantic.Consequences Consequences Mctt.Core.Completeness.Consequences.Types->Mctt.Core.Semantic.Consequences Mctt.Core.Completeness.LogicalRelation.Definitions Definitions Mctt.Core.Completeness.LogicalRelation.Lemmas Lemmas Mctt.Core.Completeness.LogicalRelation.Definitions->Mctt.Core.Completeness.LogicalRelation.Lemmas Mctt.Core.Completeness.LogicalRelation LogicalRelation Mctt.Core.Completeness.LogicalRelation.Lemmas->Mctt.Core.Completeness.LogicalRelation Mctt.Core.Completeness.LogicalRelation.Tactics Tactics Mctt.Core.Completeness.LogicalRelation.Tactics->Mctt.Core.Completeness.LogicalRelation.Lemmas Mctt.Core.Completeness Completeness Mctt.Core.Completeness->Mctt.Core.Completeness.Consequences.Rules Mctt.Core.Completeness->Mctt.Core.Completeness.Consequences.Types Mctt.Core.Completeness.FundamentalTheorem FundamentalTheorem Mctt.Core.Completeness.FundamentalTheorem->Mctt.Core.Completeness Mctt.Core.Soundness.LogicalRelation.Lemmas Lemmas Mctt.Core.Completeness.FundamentalTheorem->Mctt.Core.Soundness.LogicalRelation.Lemmas Mctt.Core.Completeness.ContextCases ContextCases Mctt.Core.Completeness.SubstitutionCases SubstitutionCases Mctt.Core.Completeness.ContextCases->Mctt.Core.Completeness.SubstitutionCases Mctt.Core.Completeness.UniverseCases UniverseCases Mctt.Core.Completeness.LogicalRelation->Mctt.Core.Completeness.UniverseCases Mctt.Core.Completeness.VariableCases VariableCases Mctt.Core.Completeness.LogicalRelation->Mctt.Core.Completeness.VariableCases Mctt.Core.Completeness.UniverseCases->Mctt.Core.Completeness.ContextCases Mctt.Core.Completeness.TermStructureCases TermStructureCases Mctt.Core.Completeness.UniverseCases->Mctt.Core.Completeness.TermStructureCases Mctt.Core.Completeness.EqualityCases EqualityCases Mctt.Core.Completeness.EqualityCases->Mctt.Core.Completeness.FundamentalTheorem Mctt.Core.Completeness.SubstitutionCases->Mctt.Core.Completeness.EqualityCases Mctt.Core.Completeness.NatCases NatCases Mctt.Core.Completeness.SubstitutionCases->Mctt.Core.Completeness.NatCases Mctt.Core.Completeness.SubtypingCases SubtypingCases Mctt.Core.Completeness.SubtypingCases->Mctt.Core.Completeness.EqualityCases Mctt.Core.Completeness.FunctionCases FunctionCases Mctt.Core.Completeness.TermStructureCases->Mctt.Core.Completeness.FunctionCases Mctt.Core.Completeness.TermStructureCases->Mctt.Core.Completeness.NatCases Mctt.Core.Completeness.VariableCases->Mctt.Core.Completeness.EqualityCases Mctt.Core.Completeness.FunctionCases->Mctt.Core.Completeness.SubtypingCases Mctt.Core.Completeness.NatCases->Mctt.Core.Completeness.FundamentalTheorem Mctt.Core.Semantic.Evaluation.Definitions Definitions Mctt.Core.Semantic.Evaluation.Lemmas Lemmas Mctt.Core.Semantic.Evaluation.Definitions->Mctt.Core.Semantic.Evaluation.Lemmas Mctt.Core.Semantic.Evaluation.Tactics Tactics Mctt.Core.Semantic.Evaluation.Lemmas->Mctt.Core.Semantic.Evaluation.Tactics Mctt.Core.Semantic.Evaluation Evaluation Mctt.Core.Semantic.Evaluation.Tactics->Mctt.Core.Semantic.Evaluation Mctt.Core.Semantic.PER.CoreTactics CoreTactics Mctt.Core.Semantic.PER.Lemmas Lemmas Mctt.Core.Semantic.PER.CoreTactics->Mctt.Core.Semantic.PER.Lemmas Mctt.Core.Semantic.PER.Definitions Definitions Mctt.Core.Semantic.PER.Definitions->Mctt.Core.Semantic.PER.CoreTactics Mctt.Core.Semantic.PER PER Mctt.Core.Semantic.PER.Lemmas->Mctt.Core.Semantic.PER Mctt.Core.Semantic.Readback.Definitions Definitions Mctt.Core.Semantic.Readback.Lemmas Lemmas Mctt.Core.Semantic.Readback.Definitions->Mctt.Core.Semantic.Readback.Lemmas Mctt.Core.Semantic.Readback Readback Mctt.Core.Semantic.Readback.Lemmas->Mctt.Core.Semantic.Readback Mctt.Core.Semantic.Realizability Realizability Mctt.Core.Semantic.Realizability->Mctt.Core.Completeness.EqualityCases Mctt.Core.Semantic.Realizability->Mctt.Core.Completeness.NatCases Mctt.Core.Soundness.Realizability Realizability Mctt.Core.Semantic.Realizability->Mctt.Core.Soundness.Realizability Mctt.Core.Semantic.NbE NbE Mctt.Core.Semantic.NbE->Mctt.Core.Semantic.Realizability Mctt.Core.Semantic.PER->Mctt.Core.Completeness.LogicalRelation.Definitions Mctt.Core.Semantic.PER->Mctt.Core.Completeness.LogicalRelation.Tactics Mctt.Core.Semantic.PER->Mctt.Core.Semantic.Realizability Mctt.Core.Soundness.LogicalRelation.Definitions Definitions Mctt.Core.Semantic.PER->Mctt.Core.Soundness.LogicalRelation.Definitions Mctt.Core.Semantic.Domain Domain Mctt.Core.Semantic.Domain->Mctt.Core.Semantic.Evaluation.Definitions Mctt.Core.Semantic.Evaluation->Mctt.Core.Semantic.Readback.Definitions Mctt.Core.Semantic.Readback->Mctt.Core.Semantic.PER.Definitions Mctt.Core.Semantic.Readback->Mctt.Core.Semantic.NbE Mctt.Core.Soundness.LogicalRelation.Core Core Mctt.Core.Soundness.LogicalRelation.Core->Mctt.Core.Soundness.Realizability Mctt.Core.Soundness.LogicalRelation LogicalRelation Mctt.Core.Soundness.LogicalRelation.Lemmas->Mctt.Core.Soundness.LogicalRelation Mctt.Core.Soundness.LogicalRelation.CoreLemmas CoreLemmas Mctt.Core.Soundness.LogicalRelation.CoreLemmas->Mctt.Core.Soundness.LogicalRelation.Core Mctt.Core.Soundness.LogicalRelation.CoreTactics CoreTactics Mctt.Core.Soundness.LogicalRelation.CoreTactics->Mctt.Core.Soundness.LogicalRelation.CoreLemmas Mctt.Core.Soundness.LogicalRelation.Definitions->Mctt.Core.Soundness.LogicalRelation.CoreTactics Mctt.Core.Soundness.Weakening.Lemmas Lemmas Mctt.Core.Soundness.Weakening.Lemmas->Mctt.Core.Soundness.LogicalRelation.CoreLemmas Mctt.Core.Soundness.Weakening.Definitions Definitions Mctt.Core.Soundness.Weakening.Definitions->Mctt.Core.Soundness.LogicalRelation.Definitions Mctt.Core.Soundness.Weakening.Definitions->Mctt.Core.Soundness.Weakening.Lemmas Mctt.Core.Soundness Soundness Mctt.Core.Soundness->Mctt.Core.Semantic.Consequences Mctt.Core.Soundness.FundamentalTheorem FundamentalTheorem Mctt.Core.Soundness.FundamentalTheorem->Mctt.Core.Soundness Mctt.Core.Soundness.ContextCases ContextCases Mctt.Core.Soundness.FunctionCases FunctionCases Mctt.Core.Soundness.ContextCases->Mctt.Core.Soundness.FunctionCases Mctt.Core.Soundness.NatCases NatCases Mctt.Core.Soundness.ContextCases->Mctt.Core.Soundness.NatCases Mctt.Core.Soundness.EqualityCases EqualityCases Mctt.Core.Soundness.ContextCases->Mctt.Core.Soundness.EqualityCases Mctt.Core.Soundness.LogicalRelation->Mctt.Core.Soundness.ContextCases Mctt.Core.Soundness.SubtypingCases SubtypingCases Mctt.Core.Soundness.LogicalRelation->Mctt.Core.Soundness.SubtypingCases Mctt.Core.Soundness.TermStructureCases TermStructureCases Mctt.Core.Soundness.LogicalRelation->Mctt.Core.Soundness.TermStructureCases Mctt.Core.Soundness.FunctionCases->Mctt.Core.Soundness.FundamentalTheorem Mctt.Core.Soundness.SubstitutionCases SubstitutionCases Mctt.Core.Soundness.SubstitutionCases->Mctt.Core.Soundness.FunctionCases Mctt.Core.Soundness.SubstitutionCases->Mctt.Core.Soundness.NatCases Mctt.Core.Soundness.SubstitutionCases->Mctt.Core.Soundness.EqualityCases Mctt.Core.Soundness.UniverseCases UniverseCases Mctt.Core.Soundness.SubtypingCases->Mctt.Core.Soundness.UniverseCases Mctt.Core.Soundness.TermStructureCases->Mctt.Core.Soundness.UniverseCases Mctt.Core.Soundness.UniverseCases->Mctt.Core.Soundness.SubstitutionCases Mctt.Core.Soundness.NatCases->Mctt.Core.Soundness.FundamentalTheorem Mctt.Core.Soundness.EqualityCases->Mctt.Core.Soundness.FundamentalTheorem Mctt.Core.Soundness.Realizability->Mctt.Core.Soundness.LogicalRelation.Lemmas Mctt.Core.Syntactic.System.Definitions Definitions Mctt.Core.Syntactic.System.Lemmas Lemmas Mctt.Core.Syntactic.System.Definitions->Mctt.Core.Syntactic.System.Lemmas Mctt.Core.Syntactic.System.Tactics Tactics Mctt.Core.Syntactic.System.Lemmas->Mctt.Core.Syntactic.System.Tactics Mctt.Core.Syntactic.System System Mctt.Core.Syntactic.System.Tactics->Mctt.Core.Syntactic.System Mctt.Core.Syntactic.SystemOpt SystemOpt Mctt.Core.Syntactic.SystemOpt->Mctt.Core.Completeness.VariableCases Mctt.Core.Syntactic.SystemOpt->Mctt.Core.Soundness.Weakening.Definitions Mctt.Core.Syntactic.Corollaries Corollaries Mctt.Core.Syntactic.SystemOpt->Mctt.Core.Syntactic.Corollaries Mctt.Core.Syntactic.Syntax Syntax Mctt.Core.Syntactic.Syntax->Mctt.Core.Semantic.Domain Mctt.Core.Syntactic.Syntax->Mctt.Core.Syntactic.System.Definitions Mctt.Core.Syntactic.System->Mctt.Core.Semantic.NbE Mctt.Core.Syntactic.CtxSub CtxSub Mctt.Core.Syntactic.System->Mctt.Core.Syntactic.CtxSub Mctt.Core.Syntactic.Corollaries->Mctt.Core.Soundness.Weakening.Lemmas Mctt.Core.Syntactic.CoreInversions CoreInversions Mctt.Core.Syntactic.CoreInversions->Mctt.Core.Syntactic.SystemOpt Mctt.Core.Syntactic.CtxEq CtxEq Mctt.Core.Syntactic.CtxEq->Mctt.Core.Syntactic.CoreInversions Mctt.Core.Syntactic.Presup Presup Mctt.Core.Syntactic.CtxEq->Mctt.Core.Syntactic.Presup Mctt.Core.Syntactic.CtxSub->Mctt.Core.Syntactic.CtxEq Mctt.Core.Syntactic.Presup->Mctt.Core.Syntactic.SystemOpt Mctt.Core.Base Base Mctt.Core.Base->Mctt.Core.Syntactic.Syntax Mctt.LibTactics LibTactics Mctt.LibTactics->Mctt.Core.Semantic.Evaluation.Lemmas Mctt.LibTactics->Mctt.Core.Syntactic.System.Definitions