namespace http://gl.mathhub.info/MMT/LFX/Finite 
import rules scala://FiniteTypes.LFX.mmt.kwarc.info

fixmeta http://cds.omdoc.org/mmt?mmt 

theory Symbols =
  include ☞ur:?LambdaPi 
	emptyType #  
	emptyFun # 1 ∅f 2 prec -900 
	UNIT 
	unite #  


theory TypedRules =
  include ☞ur:?Typed 
  include ☞ur:?Kinded 
  rule rules?EmptyTypeFormation 
  rule rules?UnitTypeFormation 
  rule rules?UnitIntro 
  rule rules?EmptyElim 
  rule rules?UnitIrrelevance 


theory SubTypedRules =
	include ?TypedRules 
	rule rules?EmptySub 
	rule rules?EmptyFunComputation 


theory EnumSymbols =
	ENUM # ENUM 1 
	CASE # CASE 1 


theory EnumRules =
   include ☞ur:?NatLiteralsOnly 
   include ?SubTypedRules 
   rule rules?EnumFormation 
   rule rules?CaseIntroduction 
   rule rules?CaseTyping 
   rule rules?CaseSubtyping 


theory EnumCoprodRules =
	include ?EnumRules 
	include ☞http://gl.mathhub.info/MMT/LFX/Coproducts?TypedCoproduct 
	rule rules?EnumComputation 
	rule rules?CaseComputation 


theory DefinedUnitRules =
	include ?TypedRules 
	rule rules?UnitComputation 
	rule rules?UnitElemComputation 


theory LFFiniteBase =
  include ?Symbols 
  include ?EnumSymbols 
  include ☞ur:?LF 
  include ?DefinedUnitRules 
  include ?EnumRules 
  include ☞ur:?Ded 
  include ☞ur:?NatRels 

	
theory LFFinite =
  include ?LFFiniteBase 
  include ?EnumCoprodRules 
	include ☞http://gl.mathhub.info/MMT/LFX/Coproducts?LFCoprod