(fth ELT is
 sort Elt .
endfth)

(fmod LIST{X :: ELT} is 
 sorts Nil NList List .
 subsort Nil NList < List .
 op nil : -> Nil [ctor].
 op _|_ : X$Elt List -> NList [ctor].
 var E : X$Elt . vars L L' : List .
---
 op _@_ : List List -> List [assoc].
 eq nil @ L = L .
 eq (E | L) @ L' = E | (L @ L').
---
 op rev1 : List -> List .
 eq rev1(nil) = nil .
 eq rev1(E | L) = rev1(L) @ (E | nil).
---
 op rev2 : List List -> List .
 eq rev2(nil,L') = L' .
 eq rev2(E | L,L') = rev2(L,E | L').
endfm)

(goal LIST |- eq L:List @ nil = L:List ;)
(set ind on L:List .)
(apply SI RD .)
--- -------------------------------------------
--- -------------------------------------------
(fmod LIST@{X :: ELT} is
 pr LIST{X} .
 var L : List .
 eq L @ nil = L .
endfm)
--- -------------------------------------------
--- -------------------------------------------
(goal LIST@ |- eq rev1(L:List @ L':List) = rev1(L':List) @ rev1(L:List) ;)
(set ind on L:List .)
(apply SI TC RD .)
--- -------------------------------------------
--- -------------------------------------------
(fmod LIST@{X :: ELT} is
 pr LIST{X} .
 vars L L' : List .
 eq L @ nil = L .
 eq rev1(L @ L') = rev1(L') @ rev1(L) .
endfm)
--- -------------------------------------------
--- -------------------------------------------
(goal LIST@ |- eq rev1(rev1(L:List))= L:List ;)
--
-- 1. Prove rev1(rev1(L)) = L.
--

(goal LIST@ |- eq rev2(L:List,E:X$Elt | L':List) = rev2(L:List,nil)@ E:X$Elt | L':List ;)
--
-- 2. Prove rev2(L,E | L') = rev2(L,nil) @ E | L'
--

--- -------------------------------------------
--- -------------------------------------------
(fmod LIST@{X :: ELT} is
 pr LIST{X} .
 vars L L' : List . var E : X$Elt .
 eq L @ nil = L .
 eq rev1(L @ L') = rev1(L') @ rev1(L) .
 eq rev2(L,E | L') = rev2(L,nil)@ E | L' .
endfm)
--- -------------------------------------------
--- -------------------------------------------
(goal LIST@ |- eq rev1(L:List) = rev2(L:List,nil) ;)
--
-- 3. Prove rev1(L) = rev2(L,nil).
--