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

theory ITP =
  proof # proof 1,…❙
  
  fix    # fix L1T,… 2❙
  assume # assume 1 2❙
  hence  # hence 1 by 2❙

  use # use 1,… ❙
  
  localref # ` L1❙
❚

theory Test : ?ITP =
  include ?FOLEQNatDed❙
  
//  test : {p: term ⟶ o} ⊦ ∀ [x] p x ⇒ p x❘
       = [p] proof (fix x assume p x; hence p x)❙ 
❚