-------------
--- Lists ---
-------------
defn list : prop -> prop
   | nil  = list A
   | cons = A -> list A -> list A

defn concatList : list A -> list A -> list A -> prop
  >| concatListNil  = concatList {A = T} nil L L
  >| concatListCons = concatList (cons (V : T) A) B (cons V C) <- concatList A B C