namespace http://gl.mathhub.info/MMT/LFX/Equality ❚
import rules scala://Equality.LFX.mmt.kwarc.info❚

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

theory Symbols =
	eqtype # 1 ≐ 2 on 3 prec -500 ❘ role Eq ❙
	refl # refl 1❙
	ind # ind 4 . V1 , V2 , V3 ⟹ 5 to 6❙
❚

theory Rules =
	rule rules?EqFormation ❙
	rule rules?ReflIntro ❙
	rule rules?EqIndElim ❙
	rule rules?EqIndComp ❙
❚
	
theory TypedEquality =
  include ☞ur:?TermsTypesKinds ❙
  include ?Symbols ❙
  include ?Rules ❙
❚
	
theory LFEquality =
	include ?TypedEquality ❙
	include ☞ur:?LF ❙
❚