Level: Lib Thy Top: 1 2
Hypotheses:

  1. Alph :

  2. R : Alph List Alph List

  3. n :

  4. L : Alph List

  5. m :

  6. x:Alph List. R x x

  7. x,y:Alph List. R x y R y x

  8. x,y,z:Alph List. R x y R y z R x z

  9. x,y,z:Alph List. R x y R (z @ x) (z @ y)

  10. w:n Alph List. l:Alph List. i:n. R l (w i)

  11. v:m Alph List. l:Alph List. (L l) (i:m. R l (v i))

  12. Fin(Alph)

  13. x : Alph List

  14. y : Alph List

Conclusion:

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

Applied Tactic: Reduce 0
Generated subgoals:

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