namespace http://cds.omdoc.org/examples❚

//   higher-order logic❚

theory HOL : ur:?LF =
  include ?TypedTerms❙
  bool: tp❙
  Bool = tm bool❙
  ded : Bool ⟶ type❘# ⊦ 1 prec -5❘role Judgment❙

  fun : tp ⟶ tp ⟶ tp❘# 1 → 2❙
  lambda: {A,B} (tm A ⟶ tm B) ⟶ tm A → B ❘# λ 3❙
  apply: {A,B} tm A → B ⟶ tm A ⟶ tm B ❘# 3 @ 4 prec 50❙

  equalConstant : {A} tm A → (A → bool)❙
  equal = [A,x,y:tm A] (equalConstant A) @ x @ y❘# 2 = 3 prec 30❙
  refl  : {A, X: tm A} ⊦ X = X❙
  cong  : {A,B,X,Y:tm A} ⊦ X = Y ⟶ {F: tm A ⟶ tm B} ⊦ F X = F Y❘# 1 cong 5 6❙ 

  beta : {A,B,F: tm A ⟶ tm B, X} ⊦ (λ F) @ X = F X❙
  
  true = (λ[x:Bool]x) = λ[x]x❙
  false = (λ[x]x) = λ[x]true❙
  not = λ[x]x=false❙
  forall = [A,p: tm A ⟶ Bool] (λ p) = λ[x]true❙
❚