1. Alph :

2. R : Alph List Alph List

3. n :

4. L : Alph List

5. m :

6. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (v:m Alph List. l:Alph List. (L l) (i:m. R l (v i))) Fin(Alph)

7. x : Alph List

8. y : Alph List

9. Dec(x@0:Alph List. (l.L (l @ x) = L (l @ y)) x@0)

Dec(l:Alph List. L (l @ x) = L (l @ y))

None