import Base
import UInt
import Option
import Set
import MultiSet
import Pair
import Maps

union List<T> {
  empty
  node(T, List<T>)
}

recursive length<E>(List<E>) -> UInt {
  length(empty) = 0
  length(node(n, next)) = 1 + length(next)
}

recursive contains<E>(List<E>, E) -> bool {
  contains(empty, x) = false
  contains(node(y, next), x) = (y = x) or contains(next, x)
}

recursive operator ++ <E>(List<E>, List<E>) -> List<E> {
  operator ++([], ys) = ys
  operator ++(node(n, xs), ys) = node(n, xs ++ ys)
}

recursive reverse<E>(List<E>) -> List<E> {
  reverse([]) = []
  reverse(node(n, next)) = reverse(next) ++ [n]
}

recursive set_of<T>(List<T>) -> Set<T> {
  set_of(empty) = ∅
  set_of(node(x, xs)) = single(x) ∪ set_of(xs)
}

recursive mset_of<T>(List<T>) -> MultiSet<T> {
  mset_of(empty) = m_empty()
  mset_of(node(x, xs)) = m_one(x) ⨄ mset_of(xs)
}

recursive map<T,U>(List<T>, fn T->U) -> List<U> {
  map(empty, f) = empty
  map(node(x, ls), f) = node(f(x), map(ls, f))
}

recursive foldr<T,U>(List<T>, U, fn T,U->U) -> U {
  foldr(empty, u, c) = u
  foldr(node(t, ls), u, c) = c(t, foldr(ls, u, c))
}

recursive foldl<T,U>(List<T>, U, fn U,T->U) -> U {
  foldl(empty, u, c) = u
  foldl(node(t, ls), u, c) = foldl(ls, c(u, t), c)
}

/*
recursive down_from(Nat) -> List {
  down_from(zero) = empty
  down_from(suc(n)) = node(n, down_from(n))
}

define up_to : fn Nat -> List = λ n { reverse(down_from(n)) }
*/
/* interval(num, begin) returns the list of numbers in the half-open
   interval: [begin, begin+num).
 */
 /*
recursive interval(Nat, Nat) -> List {
  interval(zero, begin) = empty
  interval(suc(num), begin) = node(begin, interval(num, suc(begin)))
}
*/

/* range(begin, end) returns the list of numbers in the half-open
   interval: [begin, end).
 */
 /*
define range : fn Nat,Nat -> List = λ b, e { interval(e ∸ b, b) }
*/

recursive zip<T,U>(List<T>, List<U>) -> List< Pair<T, U> > {
  zip(empty, ys) = empty
  zip(node(x, xs'), ys) =
    switch ys {
      case empty { empty }
      case node(y, ys') { node(pair(x,y), zip(xs', ys')) }
    }
}

recursive unzip<T,U>(List< Pair<T, U> >) -> Pair< List<T>, List<U> > {
  unzip(empty) = pair(@empty<T>, @empty<U>)
  unzip(node(p, ps)) =
    define xys = unzip(ps);
    pair(node(first(p), first(xys)), node(second(p), second(xys)))
}

recursive filter<E>(List<E>, fn (E)->bool) -> List<E> {
  filter(empty, P) = empty
  filter(node(x, ls), P) =
    if P(x) then node(x, filter(ls, P))
    else filter(ls, P)
}

recursive remove<T>(List<T>, T) -> List<T> {
  remove(empty, y) = empty
  remove(node(x, xs'), y) =
    if x = y then
      xs'
    else
      node(x, remove(xs', y))
}

recursive remove_all<T>(List<T>, T) -> List<T> {
  remove_all(empty, y) = empty
  remove_all(node(x, xs'), y) =
    if x = y then
      remove_all(xs', y)
    else
      node(x, remove_all(xs', y))
}

recursive get<T>(List<T>, UInt) -> Option<T> {
  get(empty, i) = none
  get(node(x, xs), i) =
    if i = 0 then
       just(x)
    else
       get(xs, i ∸ 1)
}

recursive take<T>(List<T>, UInt) -> List<T> {
  take(empty, n) = empty
  take(node(x, xs), n) =
    if n = 0 then empty
    else node(x, take(xs, n ∸ 1))
}

recursive drop<T>(List<T>, UInt) -> List<T> {
  drop(empty, n) = empty
  drop(node(x, xs'), n) =
    if n = 0 then node(x, xs')
    else drop(xs', n ∸ 1)
}

fun head<T>(ls : List<T>) {
  switch ls {
    case empty { @none<T> }
    case node(x, xs) { just(x) }
  }
}

fun tail<T>(ls : List<T>) {
  switch ls {
    case empty { @empty<T> }
    case node(x, xs) { xs }
  }
}

/********************** Theorems *********************************/

theorem length_append: all U :type, xs :List<U>, ys :List<U>.
  length(xs ++ ys) = length(xs) + length(ys)
proof
  arbitrary U :type
  induction List<U>
  case [] {
    arbitrary ys:List<U>
    conclude length(@[]<U> ++ ys) = length(@[]<U>) + length(ys)  by {
      expand operator++ | length.
    }
  }
  case node(n, xs') suppose IH {
    arbitrary ys :List<U>
    equations
      length(node(n,xs') ++ ys)
          = 1 + length(xs' ++ ys)              by expand operator++ | length.
      ... = 1 + (length(xs') + length(ys))     by replace IH[ys].
      ... = #length(node(n,xs'))# + length(ys) by expand length.
  }
end

theorem length_zero_empty: all T:type, xs:List<T>.
  if length(xs) = 0
  then xs = empty
proof
  arbitrary T:type
  arbitrary xs:List<T>
  switch xs {
    case empty { . }
    case node(x, xs') {
      suppose len_z
      conclude false
          by apply uint_not_one_add_zero[length(xs')] to
             expand length in len_z
    }
  }
end

theorem append_assoc: all U :type, xs :List<U>, ys :List<U>, zs:List<U>.
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
proof
  arbitrary U :type
  induction List<U>
  case empty {
    expand operator++.
  }
  case node(n, xs') suppose IH {
    arbitrary ys :List<U>, zs :List<U>
    equations
      (node(n,xs') ++ ys) ++ zs
          = node(n, (xs' ++ ys) ++ zs)     by expand operator++.
      ... = node(n, xs' ++ (ys ++ zs))     by replace IH[ys, zs].
      ... = # node(n,xs') ++ (ys ++ zs) #  by expand operator++.
  }
end

associative operator++ <T> in List<T>

theorem append_empty: all U :type, xs :List<U>.
  xs ++ [] = xs
proof
  arbitrary U:type
  induction List<U>
  case empty {
    conclude (empty : List<U>) ++ empty = empty  by expand operator++.
  }
  case node(n, xs') suppose IH: xs' ++ empty = xs' {
    equations
      node(n,xs') ++ empty
          = node(n, xs' ++ empty)    by expand operator++.
      ... = node(n,xs')              by replace IH.
  }
end

theorem length_reverse: all U :type, xs :List<U>.
  length(reverse(xs)) = length(xs)
proof
  arbitrary U : type
  induction List<U>
  case empty {
    conclude length(reverse(@empty<U>)) = length(@empty<U>)
        by expand reverse.
  }
  case node(n, xs') suppose IH {
    equations
      length(reverse(node(n,xs')))
          = length(reverse(xs') ++ node(n,empty)) by expand reverse.
      ... = length(reverse(xs')) + length(node(n,empty))
                    by replace length_append<U>[reverse(xs')][node(n,empty)].
      ... = length(xs') + length(node(n,empty))   by replace IH.
      ... = length(xs') + 1                       by expand 2*length.
      ... = 1 + length(xs')                       by uint_add_commute
      ... = # length(node(n,xs')) #               by expand length.
  }
end

lemma reverse_append: all U :type, xs :List<U>, ys :List<U>.
  reverse(xs ++ ys) = reverse(ys) ++ reverse(xs)
proof
  arbitrary U :type
  induction List<U>
  case [] {
    arbitrary ys :List<U>
    equations
          reverse(@[]<U> ++ ys)
        = reverse(ys)                     by expand operator++.
    ... = # reverse(ys) ++ [] #           by replace append_empty<U>[reverse(ys)].
    ... = # reverse(ys) ++ reverse([]) #  by expand reverse.
  }
  case node(n, xs') suppose IH {
    arbitrary ys :List<U>
    equations
          reverse(node(n,xs') ++ ys)
        = reverse(node(n, xs' ++ ys))                by expand operator++.
    ... = reverse(xs' ++ ys) ++ [n]                  by expand reverse.
    ... = (reverse(ys) ++ reverse(xs')) ++ [n]       by replace IH[ys].
    ... = reverse(ys) ++ (reverse(xs') ++ [n])       by append_assoc<U>[reverse(ys)][reverse(xs'), [n]]
    ... = # reverse(ys) ++ reverse(node(n,xs')) #    by expand reverse.
  }
end

theorem length_map: all T:type, f:fn T->T, xs:List<T>.
  length(map(xs, f)) = length(xs)
proof
  arbitrary T:type
  arbitrary f:fn T->T
  induction List<T>
  case empty {
    expand map.
  }
  case node(x, ls') suppose IH {
    equations
      length(map(node(x,ls'),f))
          = 1 + length(map(ls',f))  by expand map | length.
      ... = 1 + length(ls')         by replace IH.
      ... =# length(node(x,ls')) #  by expand length.
  }
end

theorem map_id: all T:type, f:fn T->T. if (all x:T. f(x) = x) then
   all xs:List<T>. map(xs, f) = xs
proof
  arbitrary T:type
  arbitrary f:fn T->T
  suppose fxx: (all x:T. f(x) = x)
  induction List<T>
  case empty {
    conclude map(@empty<T>, f) = empty      by expand map.
  }
  case node(x, ls) suppose IH {
    equations
      map(node(x,ls),f)
          = node(f(x), map(ls, f)) by expand map.
      ... = node(x, map(ls, f))    by replace fxx[x].
      ... = node(x,ls)             by replace IH.
  }
end

theorem map_append: all T:type, f: fn T->T, ys:List<T>, xs:List<T>.
  map(xs ++ ys, f) = map(xs,f) ++ map(ys, f)
proof
  arbitrary T:type
  arbitrary f:fn T->T, ys:List<T>
  induction List<T>
  case empty {
    equations
      map(@empty<T> ++ ys, f)
          = map(ys, f)                          by expand operator++.
      ... =# @empty<T> ++ map(ys, f) #          by expand operator++.
      ... =# map(@empty<T>, f) ++ map(ys, f) #  by expand map.
  }
  case node(x, xs')
    suppose IH: map(xs' ++ ys, f) = map(xs',f) ++ map(ys, f)
  {
    equations
      map((node(x,xs') ++ ys), f)
          = node(f(x), map(xs' ++ ys, f))         by expand operator++ | map.
      ... = node(f(x), map(xs',f) ++ map(ys,f))   by replace IH.
      ... = # map(node(x,xs'),f) ++ map(ys,f) #   by expand map | operator++.
  }
end

theorem map_compose: all T:type, U:type, V:type, f:fn T->U, g:fn U->V, ls :List<T>.
  map(map(ls, f), g) = map(ls, g ∘ f)
proof
  arbitrary T:type, U:type, V:type
  arbitrary f:fn T->U, g:fn U->V
  induction List<T>
  case empty { expand map. }
  case node(x, ls) suppose IH {
    equations
      map(map(node(x,ls),f),g)
        = node(g(f(x)), map(map(ls, f), g))     by expand map.
    ... = node(#g ∘ f#(x), map(map(ls, f), g))  by expand operator ∘.
    ... = node((g ∘ f)(x), map(ls, g ∘ f))      by replace IH.
    ... = #map(node(x,ls), g .o. f)#            by expand map.
  }
end

theorem zip_empty_right: all T:type, U:type, xs:List<T>.
    zip(xs, empty : List<U>) = empty
proof
  arbitrary T:type, U:type
  induction List<T>
  case empty { evaluate }
  case node(x, xs') { evaluate }
end

theorem zip_map: all T1:type, T2:type, U1:type, U2:type,
  f : fn T1 -> T2, g : fn U1 -> U2, xs:List<T1>, ys:List<U1>.
  zip(map(xs, f), map(ys, g)) = map(zip(xs,ys), pairfun(f,g))
proof
  arbitrary T1:type, T2:type, U1:type, U2:type
  arbitrary f:fn T1 -> T2, g:fn U1 -> U2
  induction List<T1>
  case empty {
    arbitrary ys:List<U1>
    conclude zip(map(@empty<T1>, f), map(ys,g))
           = map(zip(@empty<T1>,ys), pairfun(f,g))
        by expand map | zip.
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<U1>
    switch ys {
      case empty suppose EQ { evaluate }
      case node(y, ys') {
        equations
            zip(map(node(x,xs'),f),map(node(y,ys'),g))
              = node(pair(f(x), g(y)), zip(map(xs',f), map(ys',g)))       by expand map | zip.
          ... = node(pair(f(x), g(y)), map(zip(xs',ys'), pairfun(f,g)))   by replace IH[ys'].
          ... = node(pair(f(x), g(y)), map(zip(xs', ys'), λp{pair(f(first(p)), g(second(p)))}))
                      by expand pairfun.
          ... = map(zip(node(x,xs'),node(y,ys')), pairfun(f,g))   by evaluate
      }
    }
  }
end

/* update to remove use of all_elements
theorem filter_all: all T:type. all P:fn (T)->bool. all xs:List. 
  if all_elements(xs, P) then filter(xs, P) = xs
proof
  arbitrary T:type
  arbitrary P:fn (T)->bool
  induction List
  case empty {
    suppose cond: all_elements(@empty, P)
    conclude filter(@empty, P) = empty by expand filter
  }
  case node(x, xs') suppose IH: if all_elements(xs',P) then filter(xs',P) = xs' {
    suppose Pxs: all_elements(node(x,xs'),P)
    have Px: P(x) by expand all_elements in Pxs
    suffices node(x,filter(xs',P)) = node(x,xs')
        by expand filter and replace (apply eq_true to Px)
    have Pxs': all_elements(xs',P) by expand all_elements in Pxs
    have IH': filter(xs',P) = xs' by apply IH to Pxs'
    replace IH'
  }
end
*/

theorem set_of_empty: all T:type, xs:List<T>.
  if set_of(xs) = ∅
  then xs = empty
proof
  arbitrary T:type
  arbitrary xs:List<T>
  switch xs {
    case empty {
      .
    }
    case node(x, xs') {
      suppose prem
      have x_xxs: x ∈ (single(x) ∪ set_of(xs')) by {
        apply in_left_union<T>[set_of(xs')]
        to single_member<T>[x]
      }
      have prem2: single(x) ∪ set_of(xs') = ∅ by expand set_of in prem
      conclude false by prem2
    }
  }
end

theorem set_of_append: all T:type, xs:List<T>, ys:List<T>.
  set_of(xs ++ ys) = set_of(xs) ∪ set_of(ys)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>
    expand operator++ | set_of.
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<T>
    expand operator++ | set_of
    replace IH[ys].
  }
end

theorem mset_of_empty: all T:type, xs:List<T>.
  if mset_of(xs) = @m_empty<T>()
  then xs = empty
proof
  arbitrary T:type
  arbitrary xs:List<T>
  switch xs {
    case empty {
      .
    }
    case node(x, xs') {
      suppose prem
      have X1: cnt(m_one(x) ⨄ mset_of(xs'))(x) = cnt(@m_empty<T>())(x)
        by replace (expand mset_of in prem).
      have X2: 1 + cnt(mset_of(xs'))(x) = 0
        by replace cnt_sum in X1
      conclude false by apply uint_not_one_add_zero to X2
    }
  }
end

theorem som_mset_eq_set: all T:type, xs:List<T>.
  set_of_mset(mset_of(xs)) = set_of(xs)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    expand mset_of | set_of
    replace som_empty<T>.
  }
  case node(x, xs') suppose IH {
    suffices set_of_mset(m_one(x) ⨄ mset_of(xs')) = single(x) ∪ set_of(xs')
        by expand mset_of | set_of.
    suffices single(x) ∪ set_of_mset(mset_of(xs')) = single(x) ∪ set_of(xs')
        by replace som_union<T>[m_one(x), mset_of(xs')]
                 | som_one_single<T>[x].
    replace IH.
  }
end

theorem not_set_of_remove_all: all W:type, xs:List<W>, y:W.
  not (y ∈ set_of(remove_all(xs, y)))
proof
  arbitrary U:type
  induction List<U>
  case empty {
    arbitrary y:U
    expand remove_all | set_of.
  }
  case node(x, xs')
      suppose IH: all y:U. not (y ∈ set_of(remove_all(xs',y)))
  {
    arbitrary y:U
    switch x = y {
      case true suppose xy_true {
        have x_eq_y: x = y by replace xy_true.
        suffices not (y ∈ set_of(remove_all(node(y,xs'),y)))
            by replace x_eq_y.
        suffices not (y ∈ set_of(remove_all(xs',y)))
            by expand remove_all.
        IH[y]
      }
      case false suppose xy_false {
        suffices not (y ∈ set_of(if x = y then remove_all(xs',y)
                                 else node(x,remove_all(xs',y))))
            by expand remove_all.
         suppose y_in_sx_xsy
         have y_in_sx_or_xsy: y ∈ single(x) or y ∈ set_of(remove_all(xs',y))
           by expand set_of in replace xy_false in y_in_sx_xsy
         cases y_in_sx_or_xsy
         case y_in_sx {
           have xy: x = y by y_in_sx
           conclude false by replace xy_false in xy
         }
         case y_in_xsy {
           conclude false by apply IH[y] to y_in_xsy
         }
      }
    }
  }
end

theorem take_zero: all E:type, xs:List<E>.
  take(xs, 0) = []
proof
  arbitrary E:type, xs:List<E>
  switch xs {
    case empty {
      expand take.
    }
    case node(x, xs') {
      expand take.
    }
  }
end

theorem take_append: all E:type, xs:List<E>, ys:List<E>.
  take(xs ++ ys, length(xs)) = xs
proof
  arbitrary E:type
  induction List<E>
  case empty {
	  arbitrary ys:List<E>
    expand operator++ | length
    replace take_zero.
	}
	case node(x, xs') assume IH {
    arbitrary ys:List<E>
    expand operator++ | take | length
    replace IH[ys].
	}  
end
  
theorem length_drop: all E:type, xs:List<E>, n:UInt.
  if n ≤ length(xs)
  then length(drop(xs, n)) + n = length(xs)
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary n:UInt
    assume prem
    suffices n = 0 by expand drop | length.
    apply uint_zero_le_zero[n] to expand length in prem
  }
  case node(x, xs') assume IH: all n:UInt. (if n ≤ length(xs') then length(drop(xs', n)) + n = length(xs')) {
    arbitrary n:UInt
    assume prem
    cases uint_zero_or_add_one[n]
    case nz {
      replace nz
      evaluate
    }
    case n1 {
      obtain n' where n_sn from n1
      replace n_sn
      suffices length(drop(xs', n')) + 1 + n' = 1 + length(xs') by {
        expand length | drop.
      }
      have n_xs: n' ≤ length(xs') by {
        apply uint_add_both_sides_of_less_equal[1, n', length(xs')] to
        expand length in replace n_sn in prem
      }
      have eq: length(drop(xs', n')) + n' = length(xs')
        by apply IH[n'] to n_xs
      conclude length(drop(xs', n')) + 1 + n' = 1 + length(xs') by {
        replace (symmetric eq)
        replace uint_add_commute[length(drop(xs', n')), 1].
      }
    }
  }
end

postulate len_drop: all E:type, xs:List<E>, n:UInt.
  if n ≤ length(xs)
  then length(drop(xs, n)) + n = length(xs)
  
theorem length_drop_zero: all E:type, xs:List<E>, n:UInt.
  if length(xs) < n
  then length(drop(xs, n)) = 0
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary n:UInt
    assume prem
    evaluate
  }
  case node(x, xs') assume IH: all n:UInt. (if length(xs') < n then length(drop(xs', n)) = 0) {
    arbitrary n:UInt
    assume prem
    cases uint_zero_or_add_one[n]
    case nz {
      conclude false by {
        apply uint_not_less_zero
        to expand length in replace nz in prem
      }
    }
    case n1 {
      obtain n' where n_sn from n1
      replace n_sn
      expand drop
      have xs_n: length(xs') < n' by {
        apply uint_add_both_sides_of_less[1, length(xs'), n'] to
        expand length in replace n_sn in prem
      }
      conclude length(drop(xs', n')) = 0 by apply IH[n'] to xs_n
    }
  }
end

theorem drop_zero_identity: all E:type, xs:List<E>.
	drop(xs, 0) = xs
proof
  arbitrary E:type
  induction List<E>
  case empty {
    expand drop.
  }
  case node(x, xs') suppose IH {
    expand drop.
  }
end

theorem drop_append: all E:type, xs:List<E>, ys:List<E>.
  drop(xs ++ ys, length(xs)) = ys
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary ys:List<E>
    expand operator++ | length
    drop_zero_identity
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<E>
    expand length | operator++ | drop
    IH[ys]
  }
end

theorem get_drop: all T:type, xs:List<T>, n:UInt, i:UInt, d:T.
  get(drop(xs, n), i) = get(xs, n + i)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary n:UInt, i:UInt, d:T
    evaluate
  }
  case node(x, xs') suppose IH {
    arbitrary n:UInt, i:UInt, d:T
    expand drop
    cases uint_zero_or_add_one[n]
    case nz {
      replace nz.
    }
    case n1 {
      obtain n' where n_sn from n1
      replace n_sn
      expand get
      IH
    }
  }
end

theorem get_append_front: all T:type, xs:List<T>, ys:List<T>, i:UInt.
  if i < length(xs)
  then get(xs ++ ys, i) = get(xs, i)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>, i:UInt
    suppose i_z: i < length(@empty<T>)
    conclude false by {
      apply uint_not_less_zero to
      expand length in i_z
    }
  }
  case node(x, xs) suppose IH {
    arbitrary ys:List<T>, i:UInt
    suppose i_xxs: i < length(node(x,xs))
    cases uint_zero_or_add_one[i]
    case iz {
      replace iz
      expand operator++ | get.
    }
    case i1 {
      obtain i' where i_si from i1
      replace i_si
      expand operator++ | get
      have i_xs: i' < length(xs) by {
        apply uint_add_both_sides_of_less[1, i', length(xs)] to
        replace i_si in expand length in i_xxs
      }
      apply IH[ys, i'] to i_xs
    }
  }
end

theorem get_append_back: all T:type, xs:List<T>, ys:List<T>, i:UInt.
  get(xs ++ ys, length(xs) + i) = get(ys, i)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>, i:UInt
    expand operator++ | length.
  }
  case node(x, xs) suppose IH {
    arbitrary ys:List<T>, i:UInt
    expand operator++ | length | get
    IH[ys, i]
  }
end

theorem get_none: all T:type, xs:List<T>, i:UInt.
  if length(xs) <= i
  then get(xs, i) = none
proof
  arbitrary T:type
  induction List<T>
  case [] {
    arbitrary i:UInt
    assume xs_i
    conclude get(@[]<T>, i) = none by expand get.
  }
  case node(x, xs) assume IH {
    arbitrary i:UInt
    assume xxs_i
    have i_pos: 1 + length(xs) ≤ i
      by expand length in xxs_i
    cases uint_zero_or_add_one[i]
    case iz {
      replace iz
      conclude false by {
        apply uint_not_one_add_le_zero to
        expand length in replace iz in xxs_i
      }
    }
    case i1 {
      obtain i' where i_si from i1
      replace i_si
      have xs_i: length(xs) ≤ i' by {
        apply uint_add_both_sides_of_less_equal[1, length(xs), i'] to
        replace i_si in i_pos
      }
      expand get
      conclude get(xs, i') = none  by apply IH to xs_i
    }
  }
end

theorem mset_equal_implies_set_equal: all T:type, xs:List<T>, ys:List<T>.
  if mset_of(xs) = mset_of(ys)
  then set_of(xs) = set_of(ys)
proof
  arbitrary T:type
  arbitrary xs:List<T>, ys:List<T>
  suppose xs_ys
  equations
    set_of(xs) = #set_of_mset(mset_of(xs))#   by replace som_mset_eq_set<T>[xs].
           ... = set_of_mset(mset_of(ys))     by replace xs_ys.
           ... = set_of(ys)                   by som_mset_eq_set<T>[ys]
end

theorem head_append: all E:type, L:List<E>, R:List<E>.
  if 0 < length(L) 
  then head(L ++ R) = head(L)
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary R:List<E>
    suppose pos_len
    conclude false  by {
      expand length in pos_len
    }
  }
  case node(x, xs) suppose IH {
    arbitrary R:List<E>
    suppose pos_len
    equations
          head(node(x,xs) ++ R)
        = just(x)                        by expand operator++ | head.
    ... =# head(node(x,xs)) #            by expand head.
  }
end

theorem tail_append: all E:type, L:List<E>, R:List<E>.
  if 0 < length(L) 
  then tail(L ++ R) = tail(L) ++ R
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary R:List<E>
    suppose pos_len
    conclude false by {
      expand length in pos_len
    }
  }
  case node(x, xs') suppose IH {
    arbitrary R:List<E>
    suppose pos_len
    expand operator++ | tail.
  }
end