caledon-3.1.0.0: prelude/list.ncc

-------------
--- 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