import Base
import Nat
import Option
import Set
import MultiSet
import Pair
import Maps

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

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

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<Nat> {
  down_from(zero) = empty
  down_from(suc(n)) = node(n, down_from(n))
}

define up_to : fn Nat -> List<Nat> = λ 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<Nat> {
  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<Nat> = λ 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 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>, Nat) -> Option<T> {
  get(empty, i) = none
  get(node(x, xs), i) =
    if i = 0 then
       just(x)
    else
       get(xs, pred(i))
}

recursive take<T>(Nat, List<T>) -> List<T> {
  take(0, xs) = empty
  take(suc(n), xs) =
    switch xs {
      case empty { empty }
      case node(x, xs') { node(x, take(n, xs')) }
    }
}

recursive drop<T>(Nat, List<T>) -> List<T> {
  drop(0, xs) = xs
  drop(suc(n), xs) =
    switch xs {
      case empty { empty }
      case node(x, xs') { drop(n, xs') }
    }
}

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 evaluate
  }
  case node(n, xs') suppose IH {
    arbitrary ys :List<U>
    equations
      length(node(n,xs') ++ ys)
          = 1 + length(xs' ++ ys)              by evaluate
      ... = 1 + (length(xs') + length(ys))     by replace IH[ys].
      ... = length(node(n,xs')) + length(ys)   by evaluate
  }
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 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 {
    evaluate
  }
  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 evaluate
      ... = 1 + length(xs')                       by replace 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 { evaluate }
  case node(x, ls) suppose IH {
    equations
      map(map(node(x,ls),f),g)
    = node(g(f(x)), map(map(ls, f), g))        by evaluate
      ... = node(g(f(x)), map(ls, g ∘ f))      by replace IH.
      ... = map(node(x,ls), g .o. f)           by evaluate
  }
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]
      conclude false
        by apply empty_no_members
           to (replace (expand set_of in prem) in x_xxs)
    }
  }
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>
    suffices set_of(ys) = ∅ ∪ set_of(ys)
        by expand operator++ | set_of .
    replace empty_union<T>[set_of(ys)].
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<T>
    expand operator++ | set_of
    replace IH[ys] | union_assoc<T>[single(x), set_of(xs'), set_of(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<T> | cnt_empty | cnt_one in X1 // bug: change cnt_sum to cnt_sum
      conclude false by apply 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
    suffices (if y ∈ ∅ then false)  by expand remove_all | set_of.
    empty_no_members
  }
  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 apply member_union
              to (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 apply single_equal<U> to 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_append: all E:type, xs:List<E>, ys:List<E>.
  take(length(xs), xs ++ ys) = xs
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary ys:List<E>
    expand length | operator++ | take.
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<E>
    expand length | operator++ | operator+ | take
    replace zero_add[length(xs')] | IH[ys].
  }
end

theorem length_drop: all E:type, xs:List<E>, n:Nat.
  if n ≤ length(xs)
  then length(drop(n, xs)) + n = length(xs)
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary n:Nat
    assume prem
    have: n = 0 by apply zero_le_zero to evaluate in prem
    suffices length(drop(0, @[]<E>)) + 0 = length(@[]<E>)
      by replace recall n = 0.
    evaluate
  }
  case node(x, xs') assume IH: all n:Nat. (if n ≤ length(xs') then length(drop(n, xs')) + n = length(xs')) {
    arbitrary n:Nat
    assume prem
    switch n {
      case 0 {
        suffices suc(length(xs') + 0) = suc(length(xs')) by evaluate
        replace add_zero.
      }
      case suc(n') assume n_sn {
        suffices length(drop(n', xs')) + 1 + n' = 1 + length(xs')
          by expand length | drop replace suc_one_add | zero_add.
        have n_xs: n' ≤ length(xs') by evaluate in replace n_sn in prem
        have eq: length(drop(n', xs')) + n' = length(xs')
          by apply IH[n'] to n_xs
        conclude length(drop(n', xs')) + 1 + n' = 1 + length(xs')
          by replace (symmetric eq) | add_commute[1, length(drop(n',xs'))].
      }
    }
  }
end

theorem length_drop_zero: all E:type, xs:List<E>, n:Nat.
  if length(xs) < n
  then length(drop(n, xs)) = 0
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary n:Nat
    assume prem
    switch n {
      case 0 {
        conclude length(drop(0, @[]<E>)) = 0
          by evaluate
      }
      case suc(n') {
        conclude length(drop(suc(n'), @[]<E>)) = 0
          by evaluate
      }
    }
  }
  case node(x, xs') assume IH: all n:Nat. (if length(xs') < n then length(drop(n, xs')) = 0) {
    arbitrary n:Nat
    assume prem
    switch n {
      case 0 assume nz {
        conclude false 
          by evaluate in replace nz in prem
      }
      case suc(n') assume n_sn {
        suffices length(drop(n', xs')) = 0 by evaluate
        have xs_n: length(xs') < n' by {
          suffices suc(length(xs')) ≤ n' by expand operator<.
          expand operator< | length | 2*operator+ | operator≤ in
          replace n_sn in prem
        }
        conclude length(drop(n', xs')) = 0 by apply IH[n'] to xs_n
      }
    }
  }
end
  
theorem drop_append: all E:type, xs:List<E>, ys:List<E>.
  drop(length(xs), xs ++ ys) = ys
proof
  arbitrary E:type
  induction List<E>
  case empty {
    arbitrary ys:List<E>
    evaluate
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<E>
    expand length | operator++ | operator+ | drop
    replace zero_add[length(xs')] | IH[ys].
  }
end

theorem get_drop: all T:type, n:Nat, xs:List<T>, i:Nat, d:T.
  get(drop(n, xs), i) = get(xs, n + i)
proof
  arbitrary T:type
  induction Nat
  case zero {
    arbitrary xs:List<T>, i:Nat, d:T
    evaluate
  }
  case suc(n') suppose IH {
    arbitrary xs:List<T>, i:Nat, d:T
    switch xs for drop {
      case empty {
        evaluate
      }
      case node(x, xs') {
        have nsz: not (suc(n') + i = 0) by
        suppose sz conclude false by expand operator + in sz
        suffices get(drop(n', xs'), i) = get(xs', pred(suc(n') + i))
          by expand get replace (apply eq_false to nsz).
        suffices get(drop(n', xs'), i) = get(xs', n' + i)
          by expand operator + | pred.
        IH[xs',i,d]
      }
    }
  }
end

theorem get_append_front: all T:type, xs:List<T>, ys:List<T>, i:Nat.
  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:Nat
    suppose i_z: i < length(@empty<T>)
    conclude false by expand length | operator < | operator ≤ in i_z
  }
  case node(x, xs) suppose IH {
    arbitrary ys:List<T>, i:Nat
    suppose i_xxs: i < length(node(x,xs))
    switch i {
      case zero {
        evaluate
      }
      case suc(i') suppose i_si {
        suffices get(xs ++ ys, i') = get(xs, i')
          by expand operator++ | get | pred.
        have i_xs: i' < length(xs) by {
          apply less_suc_iff_suc_less to
          expand length | operator+ | operator+ in
          replace i_si 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:Nat.
  get(xs ++ ys, length(xs) + i) = get(ys, i)
proof
  arbitrary T:type
  induction List<T>
  case empty {
    arbitrary ys:List<T>, i:Nat
    evaluate
  }
  case node(x, xs) suppose IH {
    arbitrary ys:List<T>, i:Nat
    have X: not ((1 + length(xs)) + i = 0) by {
      suppose eq_z
      conclude false by evaluate in eq_z
    }
    suffices get(xs ++ ys, pred((1 + length(xs)) + i)) = get(ys, i)
       by expand operator++ | length | get
          replace (apply eq_false to X).
    suffices get(xs ++ ys, length(xs) + i) = get(ys, i)
       by expand 2*operator + | pred.
    IH[ys, i]
  }
end

theorem get_none: all T:type, xs:List<T>, i:Nat.
  if length(xs) <= i
  then get(xs, i) = none
proof
  arbitrary T:type
  induction List<T>
  case [] {
    arbitrary i:Nat
    assume xs_i
    conclude get(@[]<T>, i) = none by expand get.
  }
  case node(x, xs) assume IH {
    arbitrary i:Nat
    assume xxs_i
    have i_pos: 1 + length(xs) ≤ i
      by expand length in xxs_i
    switch i {
      case 0 assume iz {
        conclude false by expand operator+ |operator+ |operator≤ in
          replace iz in i_pos
      }
      case suc(i') assume isi {
        suffices get(xs, i') = none by expand get | pred.
        have xs_i: length(xs) ≤ i'
          by expand operator+ | operator+ | operator≤ in
             replace isi in i_pos
        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 | operator < | operator ≤ 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 | operator < | operator≤ in pos_len
  }
  case node(x, xs') suppose IH {
    arbitrary R:List<E>
    suppose pos_len
    evaluate
  }
end