data Cat : Type where {
  Conj : Cat ;
  NP : Cat ;
  S : Cat ;
  VP : Cat 
} ;
data Tree : (_ : Cat)-> Type where {
  And : Tree Conj ;
  Bill : Tree NP ;
  ConjNP : (_ : Tree Conj)-> (_ : Tree NP)-> (_ : Tree NP)-> Tree NP ;
  ConjS : (_ : Tree Conj)-> (_ : Tree S)-> (_ : Tree S)-> Tree S ;
  ConjVP : (_ : Tree Conj)-> (_ : Tree VP)-> (_ : Tree VP)-> Tree VP ;
  John : Tree NP ;
  Mary : Tree NP ;
  Or : Tree Conj ;
  Pred : (_ : Tree NP)-> (_ : Tree VP)-> Tree S ;
  Run : Tree VP ;
  Swim : Tree VP ;
  Walk : Tree VP 
}