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

fixmeta ur:?LF❚

theory ProverTest =

  a: type❙
  b: type❙
  c: type❙
  d: type❙

  k: a❙
  r: a ⟶ b❘ role ForwardRule❙
  s: a ⟶ b ⟶ c❘ role ForwardRule❙
  t: a ⟶ b ⟶ c ⟶ d❙
  
  q: d ⟶ d❙
  
  test : a ⟶ a ⟶ d ❘ = ≪a ⟶ a ⟶ d ≫❙
❚

theory PLProofs =
  include ?PLNatDed❙
  include ?ProofIrrelevance❙
  
  /T Not all of the automated proofs work at the moment. ❙

  test  : {a,b} ⊦ (a ∧ b) ⇒ (b ∧ a)❘ = _❙
  test2 : {a,b} ⊦ (a ∨ b) ⇒ (b ∨ a)❘ = _❙

  interactive_example : {A} ⊦ A ⇒ (A ∧ A)❘
                      = ≪{A:prop}⊦A⇒A∧A≫ ❙
❚

theory FOLProofs =
  include ?FOLNatDed❙
  test  : {f} ⊦ (forall [x] forall [y] f x y) ⇒ (forall [y] forall [x] f x y) ❘
  // = _❘❙
  test2 : {f} ⊦ (exists [x] exists [y] f x y) ⇒ (exists [y] exists [x] f x y) ❘
  // = _❘❙

❚