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

theory FlexaryConnectives : ur:?LFS =
  include ?PL❙
  
  flexand  : {n} prop^n ⟶ prop❘# ⋀ 2❙
  flexandI : {n} {a: prop^n} ⟨' ⊦ a..i | i:n '⟩ ⟶ ⊦ ⋀ a❙
  flexandE : {n} {a: prop^n} ⊦ ⋀ a ⟶ {i} DED (succ i) LEQ n ⟶ ⊦ a..i❙
  
  flexor   : {n} prop^n ⟶ prop❘# ⋁ 2❙
  flexorI  : {n} {a: prop^n} {i} DED (succ i) LEQ n ⟶ ⊦ a..i ⟶ ⊦ ⋁ a❙
  flexorE  : {n} {a: prop^n} {C} ⊦ ⋁ a ⟶ ⟨' ⊦ a..i ⟶ ⊦ C |i:n '⟩ ⟶ ⊦ C❙
  
  fleximp  : {n} prop^n ⟶ prop ⟶ prop❘# 2 ⇒* 3 prec 10❙
  fleximpI : {n} {a: prop^n, b} (⟨' ⊦ a..i|i:n '⟩ ⟶ ⊦ b) ⟶ ⊦ a ⇒* b❙
  fleximpE : {n} {a: prop^n, b} ⊦ a ⇒* b ⟶ ⟨' ⊦ a..i|i:n '⟩ ⟶ ⊦ b❙

❚

theory FlexaryQuantifiers : ur:?LFS =
  include ?FOL❙

  flexforall : {n} (term^n ⟶ prop) ⟶ prop❘# ∀* 2❙
  flexforallI: {n, F: term^n ⟶ prop} ({x:term^n} ⊦ F x) ⟶ ⊦ ∀* [x] F x❙
  flexforallE: {n, F: term^n ⟶ prop} {x:term^n} ⊦ (∀* [x] F x) ⟶ ⊦ F x❙

  flexexists : {n} (term^n ⟶ prop) ⟶ prop❘# ∃* 2❙
  flexexistsI: {n, F: term^n ⟶ prop} {x:term^n} ⊦ F x ⟶ ⊦ ∃* [x] F x❙
  flexexistsE: {n, F: term^n ⟶ prop,C} ({x:term^n} ⊦ (∃* [x] F x) ⟶ ⊦ C) ⟶ ⊦ C❙
❚