
  0 | module BeTTI.Quantifier
  1 | 
  2 | import public BeTTI.Quotient as BeTTI.Quotient
  3 | 
  4 | public export
  5 | 0 Forall : (b : a -> Type) -> Type
  6 | Forall b = ((x : a) -> b x) // (\x,y => Unit)
  7 | 
  8 | public export
  9 | 0 Exists : (b : a -> Type) -> Type
 10 | Exists b = (x : a ** b x) // (\x,y => Unit)
 11 |