Proving a Property of Map in OBJ3

obj NAT is
  sorts Nat Pos .
  subsort Pos < Nat .
  op 0 : -> Nat .
  op 1 : -> Pos .
  op s_ : Nat -> Pos .
  eq 1 = s 0 .
  op _<=_ : Nat Nat -> Bool .
  vars M N : Nat .
  eq M <= M = true .
  eq s M <= 0 = false .
  eq 0 <= M = true .
  eq s M <= s N = M <= N .
endo

obj LIST[E :: TRIV] is
  sorts List NeList .
  subsort NeList < List .
  op nil : -> List .
  op cons : Elt List -> NeList .
  op car_ : NeList -> Elt .
  op cdr_: NeList -> List .
  var E : Elt .
  var L : List .
  eq car cons(E,L) = E .
  eq cdr cons(E,L) = L .
endo

obj NTH[E :: TRIV] is
  protecting LIST[E] + NAT .
  sort ErrElt .
  subsort Elt < ErrElt .
  op length_ : List -> Nat .
  op nth : Pos List -> Elt .
  op toolong : -> ErrElt .
  var E : Elt .
  var L : List .
  eq length nil = 0 .
  eq length cons(E,L) = s length L .
  var P : Pos .
  eq nth(P,nil) = toolong .
  eq nth(s 0,cons(E,L)) = E .
  eq nth(s P,cons(E,L)) = nth(P,L) .
endo

th FN is
  sort Elt .
  op f : Elt -> Elt .
endth
obj MAP[F :: FN] is
  protecting NTH[F] .
  op map_ : List -> List .
  var E : Elt .
  var L : List .
  eq map nil = nil .
  eq map cons(E,L) = cons(f(E),map L) .
endo

obj SETUPFN is
  sort Elt .  
  op f : Elt -> Elt .
endo
obj SETUP is
  extending MAP[SETUPFN] .
  op e : -> Elt .
  op l : -> List .
  op p : -> Pos .
  var P : Pos .
  ceq nth(P,map l) = f(nth(P,l)) if P <= length l .
  eq p <= length l = true .
endo

***> base case
reduce nth(1,map cons(e,nil)) == f(nth(1,cons(e,nil))) .

***> induction step, by case analysis on P: Pos
reduce nth(1,map cons(e,l)) == f(nth(1,cons(e,l))) .
reduce nth(s p,map cons(e,l)) == f(nth(s p,cons(e,l))) .

***> thus we can assert:
obj MAP-FACT[F :: FN] is
  protecting MAP[F] .
  var L : List .
  var P : Pos .
  ceq nth(P, map L) = f(nth(P,L)) if P <= length L .
endo