Level: Lib Thy Top: 1
Hypotheses:

  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

Conclusion:

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

Applied Tactic: D 6 THEN D 7 THEN D 8 THEN D 9 THEN D 10 THEN D 11
Generated subgoals:

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