namespace latin:/❚

fixmeta ur:?LF❚

theory UndefinedTerms =
  include ?UntypedLogic❙
  defined : term ⟶ prop❘# 1 ↓ prec 70❙
  
  strict_equal : term ⟶ term ⟶ prop❘ # 1 ≚ 2 prec 50❙ 
❚

theory UndefinedTypedTerms =
  include ?TypedLogic❙
  defined : {A} tm A ⟶ prop❘# 2 ↓ prec 70❙

  strict_equal : {A} tm A ⟶ tm A ⟶ prop❘# 2 ≚ 3 prec 50❙ 
❚

theory UndefinedSoftTypedTerms =
  include ?SoftTypedTerms❙
  defined : term ⟶ tp ⟶ prop❘# 1 ↓ 2 prec 50❙
❚