namespace http://gl.mathhub.info/MMT/LFX/IntersectionTypes 

import rules scala://LFIntersectionTypes.LFX.mmt.kwarc.info 
import lfrules scala://lf.mmt.kwarc.info

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

theory Symbols =
	typeintersection # 1 prec -9999 


theory Rules =
  include ☞ur:?TermsTypesKinds 

  rule rules?IntersectionTypeRule 
  rule rules?IntersectionTyping 
  rule rules?IntersectionSubtypeRuleLeft 
  rule rules?IntersectionSubtypeRuleRight 

	
theory LFIntersectionTypes = 
	include ☞ur:?LambdaPi 
	include ?Symbols 
	include ?Rules 
	
	rule lfrules?PiType
	rule lfrules?PiTerm
	// rule lfrules?ApplyTerm❙
	rule lfrules?LambdaTerm
   
	rule lfrules?Beta
	rule lfrules?Extensionality
	rule lfrules?PiCongruence
	rule lfrules?LambdaCongruence
   
	rule lfrules?Solve
	rule lfrules?SolveType

	rule lfrules?TheoryTypeWithLF
   
	rule lfrules?PiIntroduction
	rule lfrules?ForwardPiElimination
	rule lfrules?BackwardPiElimination
	rule lfrules?LFHOAS
	rule rules?ApplyIntersection