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

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

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

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

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

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

function mset_of<T>(List<T>) -> MultiSet<T> {
  mset_of(empty) = m_fun(λx{0})
  mset_of(node(x, xs)) = m_one(x) ⨄ mset_of(xs)
}

function 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))
}

function 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))
}

function 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)
}

function 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).
*/
function 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) }

function 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')) }
    }
}

function 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)
}

function 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))
}

function 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))
}

function 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))
}

function 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')) }
    }
}

function 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
             definition 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 definition operator++
      ... = node(n, xs' ++ (ys ++ zs)) by rewrite IH[ys, zs]
      ... = # node(n,xs') ++ (ys ++ zs) #  by definition 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 definition operator++
  }
  case node(n, xs') suppose IH: xs' ++ empty = xs' {
    equations
      node(n,xs') ++ empty
          = node(n, xs' ++ empty)    by definition operator++
      ... = node(n,xs')              by rewrite 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 definition reverse
  }
  case node(n, xs') suppose IH {
    equations
      length(reverse(node(n,xs')))
          = length(reverse(xs') ++ node(n,empty)) by definition reverse
      ... = length(reverse(xs')) + length(node(n,empty))
                    by rewrite length_append<U>[reverse(xs')][node(n,empty)]
      ... = length(xs') + length(node(n,empty))   by rewrite IH
      ... = length(xs') + 1                       by evaluate
      ... = 1 + length(xs')                       by rewrite add_commute
      ... = # length(node(n,xs')) #               by definition 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 definition operator++
    ... = # reverse(ys) ++ [] #           by rewrite append_empty<U>[reverse(ys)]
    ... = # reverse(ys) ++ reverse([]) #  by definition reverse
  }
  case node(n, xs') suppose IH {
    arbitrary ys :List<U>
    equations
          reverse(node(n,xs') ++ ys)
        = reverse(node(n, xs' ++ ys))                by definition operator++
    ... = reverse(xs' ++ ys) ++ [n]                  by definition reverse
    ... = (reverse(ys) ++ reverse(xs')) ++ [n]       by rewrite IH[ys]
    ... = reverse(ys) ++ (reverse(xs') ++ [n])       by append_assoc<U>[reverse(ys)][reverse(xs'), [n]]
    ... = # reverse(ys) ++ reverse(node(n,xs')) #    by definition 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 {
    definition map
  }
  case node(x, ls') suppose IH {
    equations
      length(map(node(x,ls'),f))
          = 1 + length(map(ls',f))  by definition {map, length}
      ... = 1 + length(ls')         by rewrite IH
      ... =# length(node(x,ls')) #     by definition {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 definition map
  }
  case node(x, ls) suppose IH {
    equations
      map(node(x,ls),f)
          = node(f(x), map(ls, f)) by definition map
      ... = node(x, map(ls, f))    by rewrite fxx[x]
      ... = node(x,ls)             by rewrite 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 definition operator++
      ... =# @empty<T> ++ map(ys, f) #        by definition operator++
      ... =# map(@empty<T>, f) ++ map(ys, f) #  by definition 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 definition operator++ | map
      ... = node(f(x), map(xs',f) ++ map(ys,f))   by rewrite IH
      ... = # map(node(x,xs'),f) ++ map(ys,f) #   by definition 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 { definition 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 evaluate
      ... = node(g(f(x)), map(ls, g ∘ f))      by rewrite 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 { definition zip }
  case node(x, xs') { definition zip }
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 definition 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 definition map | zip
	        ... = node(pair(f(x), g(y)), map(zip(xs',ys'), pairfun(f,g)))	  by rewrite IH[ys']
          ... = node(pair(f(x), g(y)), map(zip(xs', ys'), λp{pair(f(first(p)), g(second(p)))}))
                      by definition 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 definition 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 definition all_elements in Pxs
    suffices node(x,filter(xs',P)) = node(x,xs')
        by definition filter and rewrite (apply eq_true to Px)
    have Pxs': all_elements(xs',P) by definition all_elements in Pxs
    have IH': filter(xs',P) = xs' by apply IH to Pxs'
    rewrite 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 (rewrite (definition 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 definition {operator++, set_of}
    rewrite empty_union<T>[set_of(ys)]
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<T>
    definition {operator++, set_of}
    and rewrite 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_fun(λx{0})
  then xs = empty
proof
  arbitrary T:type
  arbitrary xs:List<T>
  switch xs {
    case empty {
      .
    }
    case node(x, xs') {
      suppose prem
      have cnt_x_z: cnt(m_fun(λx'{0} : fn T->Nat))(x) = 0
        by definition cnt
      have cnt_x_pos: 1 ≤ cnt(m_fun(λx'{0} : fn T->Nat))(x) by {
        suffices 1 ≤ cnt(mset_of(node(x,xs')))(x)
          by rewrite symmetric prem
        suffices 1 ≤ 1 + cnt(mset_of(xs'))(x)
          by evaluate
	      less_equal_add[1][cnt(mset_of(xs'))(x)]
      }
      conclude false by {
        definition cnt | operator ≤ in
	      cnt_x_pos
      }
    }
  }
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 {
    suffices char_fun(λx{(if cnt(m_fun(λx'{0}:fn T->Nat))(x) = 0
                          then false else true)} : fn T->bool)
           = char_fun(λ_{false})
        by definition {mset_of, set_of, set_of_mset}
    have eq:(λx{if cnt(m_fun(λx'{0} : fn T->Nat))(x) = 0 then false else true}
             : fn T->bool)
            = λ_{false}
        by extensionality  arbitrary x:T  definition cnt
    rewrite eq
  }
  case node(x, xs') suppose IH {
    suffices set_of_mset(m_one(x) ⨄ mset_of(xs')) = single(x) ∪ set_of(xs')
        by definition {mset_of, set_of}
    suffices single(x) ∪ set_of_mset(mset_of(xs')) = single(x) ∪ set_of(xs')
        by rewrite som_union<T>[m_one(x), mset_of(xs')]
                 | som_one_single<T>[x]
    rewrite 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 definition {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 rewrite xy_true
        suffices not (y ∈ set_of(remove_all(node(y,xs'),y)))
            by rewrite x_eq_y
        suffices not (y ∈ set_of(remove_all(xs',y)))
            by definition 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 definition 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 (definition set_of in rewrite 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 rewrite 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>
    definition {length, operator++, take}
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<E>
    definition {length, operator++, operator+, take}
    and rewrite 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 definition length | drop and 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 definition operator<
          definition 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>
    definition {length, operator++, drop}
  }
  case node(x, xs') suppose IH {
    arbitrary ys:List<E>
    definition {length, operator++, operator+, drop}
    and rewrite 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
    definition {drop, operator+}
  }
  case suc(n') suppose IH {
    arbitrary xs:List<T>, i:Nat, d:T
    switch xs for drop {
      case empty {
        definition get
      }
      case node(x, xs') {
	      have nsz: not (suc(n') + i = 0) by
	      suppose sz conclude false by definition operator + in sz
	      suffices get(drop(n', xs'), i) = get(xs', pred(suc(n') + i))
          by definition get and rewrite (apply eq_false to nsz)
	      suffices get(drop(n', xs'), i) = get(xs', n' + i)
          by definition {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 definition {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 {
        definition {operator++,get}
      }
      case suc(i') suppose i_si {
        suffices get(xs ++ ys, i') = get(xs, i')
           by definition {operator++, get, pred}
	have i_xs: i' < length(xs) by
      apply less_suc_iff_suc_less to
        definition {length, operator+, operator+} 
        in rewrite 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
    definition {operator++, length, operator +}
  }
  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 definition {operator++,length, get}
          and rewrite (apply eq_false to X)
    suffices get(xs ++ ys, length(xs) + i) = get(ys, i)
       by definition 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 definition get
  }
  case node(x, xs) assume IH {
    arbitrary i:Nat
    assume xxs_i
    have i_pos: 1 + length(xs) ≤ i
      by definition length in xxs_i
    switch i {
      case 0 assume iz {
        conclude false by definition {operator+,operator+,operator≤} in rewrite iz in i_pos
      }
      case suc(i') assume isi {
        suffices get(xs, i') = none by definition {get,pred}
        have xs_i: length(xs) ≤ i' by definition {operator+,operator+,operator≤} in rewrite 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 definition {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 definition {operator++,head}
    ... =# head(node(x,xs)) #            by definition 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 definition {length, operator <, operator≤} in pos_len
  }
  case node(x, xs') suppose IH {
    arbitrary R:List<E>
    suppose pos_len
    definition {operator++,tail}
  }
end